Merge pull request #3626 from mtzguido/unfold_once

Add an `UnfoldOnce`/`delta_once` normalizer step

examples/data_structures/BinomialQueue.fst

@@ -360,7 +360,7 @@ let rec carry_repr (d:pos) (q:forest) (t:tree) (lq lt:ms)
       (ms_append (keys_of_tree hd) (keys_of_tree t))
 #pop-options
 
-#push-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+#push-options "--z3rlimit 75 --fuel 1 --ifuel 1"
 let rec join_repr (d:pos) (p q:forest) (c:tree)
   (lp lq lc:ms)
   : Lemma

examples/doublylinkedlist/DoublyLinkedList.fst

@@ -1964,7 +1964,7 @@ let dll_append (#t:Type) (d1 d2:dll t) :
 
 #reset-options
 
-#set-options "--z3rlimit 40 --max_fuel 2 --max_ifuel 1"
+#set-options "--z3rlimit 60 --max_fuel 2 --max_ifuel 1"
 
 let dll_split_using (#t:Type) (d:dll t) (e:pointer (node t)) :
   StackInline (dll t * dll t)

src/parser/FStarC.Parser.Const.fst

@@ -323,6 +323,7 @@ let steps_delta         = psconst "delta"
 let steps_reify         = psconst "reify_"
 let steps_norm_debug    = psconst "norm_debug"
 let steps_unfoldonly    = psconst "delta_only"
+let steps_unfoldonce    = psconst "delta_once"
 let steps_unfoldfully   = psconst "delta_fully"
 let steps_unfoldattr    = psconst "delta_attr"
 let steps_unfoldqual    = psconst "delta_qualifier"

src/syntax/FStarC.Syntax.Embeddings.fst

@@ -798,6 +798,7 @@ let steps_Iota          = tconst PC.steps_iota
 let steps_Reify         = tconst PC.steps_reify
 let steps_NormDebug     = tconst PC.steps_norm_debug
 let steps_UnfoldOnly    = tconst PC.steps_unfoldonly
+let steps_UnfoldOnce    = tconst PC.steps_unfoldonce
 let steps_UnfoldFully   = tconst PC.steps_unfoldonly
 let steps_UnfoldAttr    = tconst PC.steps_unfoldattr
 let steps_UnfoldQual    = tconst PC.steps_unfoldqual
@@ -848,6 +849,9 @@ let e_norm_step : embedding Pervasives.norm_step =
                 | UnfoldOnly l ->
                     S.mk_Tm_app steps_UnfoldOnly [S.as_arg (embed l rng None norm)]
                                 rng
+                | UnfoldOnce l ->
+                    S.mk_Tm_app steps_UnfoldOnce [S.as_arg (embed l rng None norm)]
+                                rng
                 | UnfoldFully l ->
                     S.mk_Tm_app steps_UnfoldFully [S.as_arg (embed l rng None norm)]
                                 rng
@@ -902,6 +906,9 @@ let e_norm_step : embedding Pervasives.norm_step =
                 | Tm_fvar fv, [(l, _)] when S.fv_eq_lid fv PC.steps_unfoldonly ->
                     BU.bind_opt (try_unembed l norm) (fun ss ->
                     Some <| UnfoldOnly ss)
+                | Tm_fvar fv, [(l, _)] when S.fv_eq_lid fv PC.steps_unfoldonce ->
+                    BU.bind_opt (try_unembed l norm) (fun ss ->
+                    Some <| UnfoldOnce ss)
                 | Tm_fvar fv, [(l, _)] when S.fv_eq_lid fv PC.steps_unfoldfully ->
                     BU.bind_opt (try_unembed l norm) (fun ss ->
                     Some <| UnfoldFully ss)

src/typechecker/FStarC.TypeChecker.Cfg.fst

@@ -46,6 +46,7 @@ let steps_to_string f =
     do_not_unfold_pure_lets = %s;\n\
     unfold_until = %s;\n\
     unfold_only = %s;\n\
+    unfold_once = %s;\n\
     unfold_fully = %s;\n\
     unfold_attr = %s;\n\
     unfold_qual = %s;\n\
@@ -78,6 +79,7 @@ let steps_to_string f =
     f.do_not_unfold_pure_lets |> show;
     f.unfold_until |> show;
     f.unfold_only |> show;
+    f.unfold_once |> show;
     f.unfold_fully |> show;
     f.unfold_attr |> show;
     f.unfold_qual |> show;
@@ -149,6 +151,7 @@ let default_steps : fsteps = {
     do_not_unfold_pure_lets = false;
     unfold_until = None;
     unfold_only = None;
+    unfold_once = None;
     unfold_fully = None;
     unfold_attr = None;
     unfold_qual = None;
@@ -191,6 +194,7 @@ let fstep_add_one s fs =
     | DoNotUnfoldPureLets ->  { fs with do_not_unfold_pure_lets = true }
     | UnfoldUntil d -> { fs with unfold_until = Some d }
     | UnfoldOnly  lids -> { fs with unfold_only  = Some lids }
+    | UnfoldOnce  lids -> { fs with unfold_once  = Some lids }
     | UnfoldFully lids -> { fs with unfold_fully = Some lids }
     | UnfoldAttr  lids -> { fs with unfold_attr  = Some lids }
     | UnfoldQual  strs ->
@@ -459,6 +463,8 @@ let translate_norm_step = function
     | Pervasives.NormDebug -> [NormDebug]
     | Pervasives.UnfoldOnly names ->
         [UnfoldUntil delta_constant; UnfoldOnly (List.map I.lid_of_str names)]
+    | Pervasives.UnfoldOnce names ->
+        [UnfoldUntil delta_constant; UnfoldOnce (List.map I.lid_of_str names)]
     | Pervasives.UnfoldFully names ->
         [UnfoldUntil delta_constant; UnfoldFully (List.map I.lid_of_str names)]
     | Pervasives.UnfoldAttr names ->

src/typechecker/FStarC.TypeChecker.Cfg.fsti

@@ -56,6 +56,7 @@ type fsteps = {
      do_not_unfold_pure_lets : bool;
      unfold_until : option S.delta_depth;
      unfold_only  : option (list I.lid);
+     unfold_once  : option (list I.lid);
      unfold_fully : option (list I.lid);
      unfold_attr  : option (list I.lid);
      unfold_qual  : option (list string);

src/typechecker/FStarC.TypeChecker.Env.fsti

@@ -44,6 +44,7 @@ type step =
   | DoNotUnfoldPureLets
   | UnfoldUntil of delta_depth
   | UnfoldOnly  of list FStarC.Ident.lid
+  | UnfoldOnce  of list FStarC.Ident.lid
   | UnfoldFully of list FStarC.Ident.lid
   | UnfoldAttr  of list FStarC.Ident.lid
   | UnfoldQual  of list string

src/typechecker/FStarC.TypeChecker.Normalize.Unfolding.fst

@@ -34,15 +34,16 @@ let should_unfold cfg should_reify fv qninfo : should_unfold_res =
       | None -> []
       | Some quals -> quals
     in
-    (* unfold or not, fully or not, reified or not *)
-    let yes   = true  , false , false in
-    let no    = false , false , false in
-    let fully = true  , true  , false in
-    let reif  = true  , false , true in
+    (* unfold or not, fully or not, reified or not, only once or not *)
+    let yes   = true  , false , false, false in
+    let no    = false , false , false, false in
+    let fully = true  , true  , false, false in
+    let reif  = true  , false , true,  false  in
+    let once  = true  , false , false, true in
 
     let yesno b = if b then yes else no in
     let fullyno b = if b then fully else no in
-    let comb_or l = List.fold_right (fun (a,b,c) (x,y,z) -> (a||x, b||y, c||z)) l (false, false, false) in
+    let comb_or l = List.fold_right (fun (a,b,c,d) (x,y,z,w) -> (a||x, b||y, c||z, d||w)) l (false, false, false, false) in
 
     let default_unfolding () =
         log_unfolding cfg (fun () -> BU.print3 "should_unfold: Reached a %s with delta_depth = %s\n >> Our delta_level is %s\n"
@@ -57,12 +58,13 @@ let should_unfold cfg should_reify fv qninfo : should_unfold_res =
     in
     let selective_unfold =
       Some? cfg.steps.unfold_only ||
+      Some? cfg.steps.unfold_once ||
       Some? cfg.steps.unfold_fully ||
       Some? cfg.steps.unfold_attr ||
       Some? cfg.steps.unfold_qual ||
       Some? cfg.steps.unfold_namespace
     in
-    let res : bool & bool & bool =
+    let res : bool & bool & bool & bool =
     match qninfo, selective_unfold with
     // We unfold dm4f actions if and only if we are reifying
     | _ when Env.qninfo_is_action qninfo ->
@@ -83,6 +85,11 @@ let should_unfold cfg should_reify fv qninfo : should_unfold_res =
         log_unfolding cfg (fun () -> BU.print_string " >> HasMaskedEffect, not unfolding\n");
         no
 
+    // Unfoldonce. NB: this is before the zeta case, so we unfold even if zeta is off
+    | _, true when Some? cfg.steps.unfold_once && BU.for_some (fv_eq_lid fv) (Some?.v cfg.steps.unfold_once) ->
+        log_unfolding cfg (fun () -> BU.print_string " >> UnfoldOnce\n");
+        once
+
     // Recursive lets may only be unfolded when Zeta is on
     | Some (Inr ({sigquals=qs; sigel=Sig_let {lbs=(is_rec, _)}}, _), _), _ when
             is_rec && not cfg.steps.zeta && not cfg.steps.zeta_full ->
@@ -160,10 +167,11 @@ let should_unfold cfg should_reify fv qninfo : should_unfold_res =
                     );
     let r =
       match res with
-      | false, _, _ -> Should_unfold_no
-      | true, false, false -> Should_unfold_yes
-      | true, true, false -> Should_unfold_fully
-      | true, false, true -> Should_unfold_reify
+      | false, _, _, _ -> Should_unfold_no
+      | true, false, false, false -> Should_unfold_yes
+      | true, false, false, true -> Should_unfold_once
+      | true, true, false, false -> Should_unfold_fully
+      | true, false, true, false -> Should_unfold_reify
       | _ ->
         failwith <| BU.format1 "Unexpected unfolding result: %s" (show res)
     in

src/typechecker/FStarC.TypeChecker.Normalize.Unfolding.fsti

@@ -13,6 +13,7 @@ val plugin_unfold_warn_ctr : ref int
 type should_unfold_res =
     | Should_unfold_no
     | Should_unfold_yes
+    | Should_unfold_once
     | Should_unfold_fully
     | Should_unfold_reify
 

src/typechecker/FStarC.TypeChecker.Normalize.fst

@@ -631,9 +631,19 @@ let decide_unfolding cfg stack fv qninfo (* : option (option cfg * stack) *) =
     | Should_unfold_no ->
         // No unfolding
         None
+
     | Should_unfold_yes ->
         // Usual unfolding, no change to cfg or stack
         Some (None, stack)
+
+    | Should_unfold_once ->
+        let Some once = cfg.steps.unfold_once in
+        let cfg' = { cfg with steps = {
+                     cfg.steps with unfold_once =
+                     Some <| List.filter (fun lid -> not (S.fv_eq_lid fv lid)) once } } in
+        // Unfold only once. Keep the stack, but remove the lid from the step.
+        Some (Some cfg', stack)
+
     | Should_unfold_fully ->
         // Unfolding fully, use new cfg with more steps and keep old one in stack
         let cfg' =

tests/error-messages/NegativeTests.Neg.fst.json_output.expected

@@ -20,7 +20,7 @@
 {"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.Native.option 'a {Some? _}\ngot type FStar.Pervasives.Native.option 'a","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.Native.fst","start_pos":{"line":33,"col":4},"end_pos":{"line":33,"col":8}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":46,"col":30},"end_pos":{"line":46,"col":31}}},"number":19,"ctx":["While typechecking the top-level declaration `let bad_projector`","While typechecking the top-level declaration `[@@expect_failure] let bad_projector`"]}
 >>]
 >> Got issues: [
-{"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.result Prims.int {V? _}\ngot type FStar.Pervasives.result Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.fsti","start_pos":{"line":520,"col":4},"end_pos":{"line":520,"col":5}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":50,"col":45},"end_pos":{"line":50,"col":47}}},"number":19,"ctx":["While typechecking the top-level declaration `val NegativeTests.Neg.test`","While typechecking the top-level declaration `[@@expect_failure] val NegativeTests.Neg.test`"]}
+{"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.result Prims.int {V? _}\ngot type FStar.Pervasives.result Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.fsti","start_pos":{"line":526,"col":4},"end_pos":{"line":526,"col":5}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":50,"col":45},"end_pos":{"line":50,"col":47}}},"number":19,"ctx":["While typechecking the top-level declaration `val NegativeTests.Neg.test`","While typechecking the top-level declaration `[@@expect_failure] val NegativeTests.Neg.test`"]}
 >>]
 >> Got issues: [
 {"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":55,"col":25},"end_pos":{"line":55,"col":26}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let h1`","While typechecking the top-level declaration `[@@expect_failure] let h1`"]}

tests/error-messages/NegativeTests.Neg.fst.output.expected

@@ -63,7 +63,7 @@
     got type FStar.Pervasives.result Prims.int
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also FStar.Pervasives.fsti(520,4-520,5)
+  - See also FStar.Pervasives.fsti(526,4-526,5)
 
 >>]
 >> Got issues: [

tests/micro-benchmarks/UnfoldOnce.fst

@@ -0,0 +1,29 @@
+module UnfoldOnce
+
+open FStar.Tactics.V2
+
+#push-options "--admit_smt_queries true"
+let rec f () : Tot int = 1 + f ()
+#pop-options
+
+let _ =
+  assert True by begin
+    let t = (`(f ())) in
+    let t' = norm_term [delta_once [`%f]] t in
+    let expected = (`(1 + f () <: Tot Prims.int)) in
+    (* print ("t' = " ^term_to_string t'); *)
+    (* print ("expected = " ^term_to_string expected); *)
+    guard (term_eq t' expected);
+    ()
+  end
+
+let _ =
+  assert True by begin
+    let t = (`(f () + f ())) in
+    let t' = norm_term [delta_once [`%f]] t in
+    let expected = (`((1 + f () <: Tot Prims.int) + f ())) in
+    (* print ("t' = " ^term_to_string t'); *)
+    (* print ("expected = " ^term_to_string expected); *)
+    guard (term_eq t' expected);
+    ()
+  end

ulib/FStar.Pervasives.fst

@@ -57,6 +57,7 @@ type norm_step =
   | Reify // Reify effectful definitions into their representations
   | NormDebug // Turn on debugging for this call
   | UnfoldOnly : list string -> norm_step // Unlike Delta, unfold definitions for only the given
+  | UnfoldOnce : list string -> norm_step
   // names, each string is a fully qualified name
   // like `A.M.f`
   // idem
@@ -103,6 +104,9 @@ let reify_ = Reify
 irreducible
 let delta_only s = UnfoldOnly s
 
+irreducible
+let delta_once s = UnfoldOnce s
+
 irreducible
 let delta_fully s = UnfoldFully s
 

ulib/FStar.Pervasives.fsti

@@ -217,6 +217,13 @@ val reify_ : norm_step
     list. Each string is a fully qualified name like [A.M.f] *)
 val delta_only (s: list string) : Tot norm_step
 
+(** Like [delta_only], unfold only the definitions in this list,
+but do so only once. This is useful for a controlled unfolding
+of recursive definitions. NOTE: if there are many occurrences
+of a variable in this list, it is unspecified which one will
+be unfolded (currently it depends on normalization order). *)
+val delta_once (s: list string) : Tot norm_step
+
 (** Unfold definitions for only the names in the given list, but
     unfold each definition encountered after unfolding as well.
 
@@ -328,9 +335,8 @@ val normalize_spec (a: Type0) : Lemma (normalize a == a)
 val norm_spec (s: list norm_step) (#a: Type) (x: a) : Lemma (norm s #a x == x)
 
 (** Use the following to expose an ["opaque_to_smt"] definition to the
-    solver as: [reveal_opaque (`%defn) defn]. NB: zeta is needed in
-    the case where the definition is recursive. *)
-let reveal_opaque (s: string) = norm_spec [delta_only [s]; zeta]
+    solver as: [reveal_opaque (`%defn) defn]. *)
+let reveal_opaque (s: string) = norm_spec [delta_once [s]]
 
 (** Wrappers over pure wp combinators that return a pure_wp type
     (with monotonicity refinement) *)