Merge pull request #2896 from FStarLang/guido_misc

Introducing an `admit_termination` attribute

src/parser/FStar.Parser.Const.fst

@@ -359,6 +359,7 @@ let binder_strictly_positive_attr = psconst "strictly_positive"
 let binder_unused_attr = psconst "unused"
 let no_auto_projectors_attr = psconst "no_auto_projectors"
 let no_subtping_attr_lid = psconst "no_subtyping"
+let admit_termination_lid = psconst "admit_termination"
 let attr_substitute_lid = p2l ["FStar"; "Pervasives"; "Substitute"]
 
 

src/tosyntax/FStar.ToSyntax.ToSyntax.fst

@@ -3493,7 +3493,7 @@ and desugar_decl_aux env (d: decl): (env_t * sigelts) =
       let d = { d with attrs = [] } in
       let errs, r = Errors.catch_errors (fun () ->
                       Options.with_saved_options (fun () ->
-                        desugar_decl_noattrs env d)) in
+                        desugar_decl_noattrs attrs env d)) in
       begin match errs, r with
       | [], Some (env, ses) ->
         (* Succeeded desugaring, carry on, but make a Sig_fail *)
@@ -3529,7 +3529,7 @@ and desugar_decl_aux env (d: decl): (env_t * sigelts) =
         end
       end
     | None ->
-      desugar_decl_noattrs env d
+      desugar_decl_noattrs attrs env d
   in
 
   let rec val_attrs (ses:list sigelt) : list S.term =
@@ -3549,7 +3549,7 @@ and desugar_decl env (d:decl) :(env_t * sigelts) =
   let env, ses = desugar_decl_aux env d in
   env, ses |> List.map generalize_annotated_univs
 
-and desugar_decl_noattrs env (d:decl) : (env_t * sigelts) =
+and desugar_decl_noattrs top_attrs env (d:decl) : (env_t * sigelts) =
   let trans_qual = trans_qual d.drange in
   match d.d with
   | Pragma p ->
@@ -3729,6 +3729,13 @@ and desugar_decl_noattrs env (d:decl) : (env_t * sigelts) =
                 fvs
                 ([], [])
           in
+          (* Propagate top-level attrs to each lb. The lb.lbattrs field should be empty,
+           * but just being safe here. *)
+          let lbs =
+            let (isrec, lbs0) = lbs in
+            let lbs0 = lbs0 |> List.map (fun lb -> { lb with lbattrs = lb.lbattrs @ val_attrs @ top_attrs }) in
+            (isrec, lbs0)
+          in
           // BU.print3 "Desugaring %s, val_quals are %s, val_attrs are %s\n"
           //   (List.map Print.fv_to_string fvs |> String.concat ", ")
           //   (Print.quals_to_string val_quals)
@@ -3745,19 +3752,11 @@ and desugar_decl_noattrs env (d:decl) : (env_t * sigelts) =
             then S.Logic::quals
             else quals in
           let names = fvs |> List.map (fun fv -> fv.fv_name.v) in
-          (*
-           * AR: we first desugar the term with no attributes and then add attributes in the end, see desugar_decl above
-           *     this used to be fine, because subsequent typechecker then works on terms that have attributes
-           *     however this doesn't work if we want access to the attributes during desugaring, e.g. when warning about deprecated defns.
-           *     for now, adding attrs to Sig_let to make progress on the deprecated warning, but perhaps we should add attrs to all terms
-           *)
-          let attrs = List.map (desugar_term env) d.attrs in
-          (* GM: Plus the val attrs, concatenated below *)
           let s = { sigel = Sig_let(lbs, names);
                     sigquals = quals;
                     sigrng = d.drange;
-                    sigmeta = default_sigmeta  ;
-                    sigattrs = val_attrs @ attrs;
+                    sigmeta = default_sigmeta;
+                    sigattrs = val_attrs @ top_attrs;
                     sigopts = None; } in
           let env = push_sigelt env s in
           env, [s]

src/typechecker/FStar.TypeChecker.Tc.fst

@@ -425,7 +425,7 @@ let tc_sig_let env r se lbs lids : list sigelt * list sigelt * Env.env =
               if lb.lbunivs <> [] && List.length lb.lbunivs <> List.length uvs
               then raise_error (Errors.Fatal_IncoherentInlineUniverse, ("Inline universes are incoherent with annotation from val declaration")) r;
               false, //explicit annotation provided; do not generalize
-              mk_lb (Inr lbname, uvs, PC.effect_ALL_lid(), tval, def, [], lb.lbpos),
+              mk_lb (Inr lbname, uvs, PC.effect_Tot_lid, tval, def, lb.lbattrs, lb.lbpos),
               quals_opt
           in
           gen, lb::lbs, quals_opt)

src/typechecker/FStar.TypeChecker.TcTerm.fst

@@ -490,7 +490,8 @@ let guard_letrecs env actuals expected_c : list (lbname*typ*univ_names) =
           let cflags = U.comp_flags c in
           match cflags |> List.tryFind (function DECREASES _ -> true | _ -> false) with
                 | Some (DECREASES d) -> d
-                | _ -> bs |> filter_types_and_functions |> Decreases_lex in
+                | _ -> bs |> filter_types_and_functions |> Decreases_lex
+      in
 
       let precedes_t = TcUtil.fvar_const env Const.precedes_lid in
       let rec mk_precedes_lex env l l_prev : term =
@@ -4079,7 +4080,7 @@ and check_inner_let_rec env top =
 (******************************************************************************)
 and build_let_rec_env _top_level env lbs : list letbinding * env_t * guard_t =
    let env0 = env in
-   let termination_check_enabled (lbname:lbname) (lbdef:term) (lbtyp:term)
+   let termination_check_enabled (attrs:list attribute) (lbname:lbname) (lbdef:term) (lbtyp:term)
      : option (int * term) // when enabled returns recursion arity;
                             // plus the term elaborated with implicit binders
                             // (TODO: move all that logic to desugaring)
@@ -4119,7 +4120,10 @@ and build_let_rec_env _top_level env lbs : list letbinding * env_t * guard_t =
       * abstraction's body. So we can just check the effect `c` for
       * totality. Another way of seeing this check is that we take
       * the minimum amount of binders from the actuals and formals. *)
-     if U.comp_effect_name c |> Env.lookup_effect_quals env |> List.contains TotalEffect then
+     if U.has_attribute attrs Const.admit_termination_lid then (
+       log_issue env.range (Warning_WarnOnUse, "Admitting termination of " ^ Print.lbname_to_string lbname);
+       None
+     ) else if U.comp_effect_name c |> Env.lookup_effect_quals env |> List.contains TotalEffect then
        Some (nformals, U.abs actuals body body_lc)
      else
        None
@@ -4143,7 +4147,7 @@ and build_let_rec_env _top_level env lbs : list letbinding * env_t * guard_t =
         // this was a problem for 2-phase, if an implicit type was the type of a let rec (see bug056)
         // Removed that check. Rest of the code relies on env.letrecs = []
         let lb, env =
-            match termination_check_enabled lb.lbname lbdef lbtyp with
+            match termination_check_enabled lb.lbattrs lb.lbname lbdef lbtyp with
             // AR: we need to add the binding of the let rec after adding the
             // binders of the lambda term, and so, here we just note in the env that
             // we are typechecking a let rec, the recursive binding will be added in

tests/micro-benchmarks/AdmitTermination.fst

@@ -0,0 +1,65 @@
+module AdmitTermination
+
+// blah not used recursively, silence
+#set-options "--warn_error -328"
+
+[@@admit_termination]
+let rec f1 (x:nat) : nat = f1 x
+
+(* Even admitting termination, this is not type
+correct. *)
+[@@expect_failure [19]; admit_termination]
+let rec f2 (x:nat) : nat = f2 x - 1
+
+[@@admit_termination]
+let rec blah () = ()
+and f (x:int) : int = f x
+
+[@@admit_termination]
+let rec g (x:int) : int = g x
+
+val h : int -> int
+[@@admit_termination]
+let rec h (x:int) : int = h x
+
+[@@admit_termination]
+val i : int -> int
+
+let rec i (x:int) : int = i x
+
+let top1 () =
+  let rec blah () = ()
+  [@@admit_termination]
+  and f (x:int) : int = f x
+  in ()
+
+(* This admits the termination of blah, not of f! *)
+[@@expect_failure [19]]
+let top2 () =
+  [@@admit_termination]
+  let rec blah () = ()
+  and f (x:int) : int = f x
+  in ()
+
+(* Note that the admit_termination attribute applies to
+*calls* to the admitted binding, and not the definition
+of the binding. The difference is significant in mutual
+recursion, see ahead. *)
+
+(* Works: the body of f respects the termination argument
+for g. Since we admit the termination of f, the body of g
+has no obligation, and verifies. *)
+let top3 () =
+  [@@admit_termination]
+  let rec f (x:pos) : int = g (x-1)
+  and g (x:nat) : int = f (x+1)
+  in ()
+
+(* Fails: the body of g does not respect the termination
+argument for f, which is not admitted. *)
+[@@expect_failure [19]]
+let top4 () =
+  let rec f (x:pos) : int = g (x-1)
+  [@@admit_termination]
+  and g (x:nat) : int = f (x+1)
+  in ()

ulib/FStar.Pervasives.fst

@@ -182,4 +182,6 @@ let no_auto_projectors = ()
 
 let no_subtyping = ()
 
+let admit_termination = ()
+
 let singleton #_ x = x

ulib/FStar.Pervasives.fsti

@@ -1163,6 +1163,8 @@ val no_auto_projectors : unit
 *)
 val no_subtyping : unit
 
+val admit_termination : unit
+
 (** Pure and ghost inner let bindings are now always inlined during
     the wp computation, if: the return type is not unit and the head
     symbol is not marked irreducible.