FStarLang / steel

The Steel separation logic library for F*
Apache License 2.0
31 stars 5 forks source link

Support for local function definitions #133

Closed nikswamy closed 11 months ago

nikswamy commented 11 months ago

This PR provides support for (non-recursive) function definitions nested within a Pulse statement block.

e.g.,

ghost
fn yields_idem (p:vprop)
   requires emp
   ensures p @==> p
{
    ghost fn intro_stick_aux (u:unit)
    requires emp ** p
    ensures p
    { () };
    Pulse.Lib.Stick.intro_stick _ _ _ intro_stick_aux;
    fold (p @==> p);
}

Adding this involved a few steps:

  1. A refactoring of the Pulse syntax extension

  2. Adding a new Pulse typing rule T_BindFn, which is similar to T_TotBind, except the head of T_BindFn is an st_term with a C_Tot type, whereas the T_TotBind expects a head to be term.

  3. Along the way I enhanced a few things related to the handling of post_hints and post_hint typing. This uncovered a two instances of the same bug in WithLocal and WithLocalArray where the postcondition was admitted to be typechecked in a context with the wrong type for the locally bound variable.