Add let predicate.

Author: gebner

src/checker/Pulse.Main.fst

@@ -33,6 +33,46 @@ let debug_main g (s: unit -> T.Tac string) : T.Tac unit =
   if RU.debug_at_level (fstar_env g) "pulse.main" then
     T.print (s ())
 
+let rec elab_slprop_defn (g: env) (binders: list (option qualifier & binder & bv)) (body: term) : T.Tac term =
+  match binders with
+  | [] ->
+    Pulse.Checker.ImpureSpec.purify_spec g { ctxt_now = tm_emp; ctxt_old = None } body
+  | (quals, b, bv)::binders ->
+    let b_ty, b_u = Pulse.Checker.Pure.tc_type_phase1 g b.binder_ty in
+    assume freshv g bv.bv_index;
+    let g' = push_binding g bv.bv_index b.binder_ppname b_ty in
+    let body = elab_slprop_defn g' binders body in
+    R.pack_ln (R.Tv_Abs (R.pack_binder {
+      sort = b_ty;
+      qual = elab_qual quals;
+      ppname = b.binder_ppname.name;
+      attrs = [];
+    }) (close_term body bv.bv_index))
+
+let check_slprop_defn
+    (d : decl{SlpropDefn? d.d})
+    (g : stt_env{bindings g == []})
+    (expected_t : option term)
+    (* Both of these unused: *)
+    (pre : term)
+  : T.Tac (RT.dsl_tac_result_t (fstar_env g) expected_t)
+= 
+  let SlpropDefn { id; bs; body } = d.d in
+  let nm = fst (inspect_ident id) in
+
+  let cur_module = T.cur_module () in
+
+  let body: term = elab_slprop_defn g bs body in
+
+  [], (false, R.pack_sigelt (R.Sg_Let false [
+    R.pack_lb {
+      lb_fv = R.pack_fv (cur_module @ [nm]);
+      lb_us = [];
+      lb_typ = tm_unknown;
+      lb_def = body;
+    }
+  ]), None), []
+
 let set_impl src_g #g #t (se: RT.sigelt_for g t) (r: bool) (impl: R.term) : T.Tac (RT.sigelt_for g t) =
   let checked, se, blob = se in
   debug_main src_g (fun _ ->
@@ -229,6 +269,7 @@ let main' (d:decl) (pre:term) (g:RT.fstar_top_env) (expected_t:option term)
           check_fndecl d g
         else
           fail g (Some d.range) "pulse main: expected type provided for a FnDecl?"
+      | SlpropDefn {} -> check_slprop_defn d g expected_t pre
 
 let join_smt_goals () : Tac unit =
   let open FStar.Tactics.V2 in

src/checker/Pulse.Syntax.Base.fsti

@@ -357,10 +357,22 @@ type fn_decl = {
   comp : comp_st; (* bs in scope *)
 }
 
+noeq
+type slprop_defn = {
+  id : R.ident;
+  // isrec : bool;
+  // us : list R.univ_name;
+  bs : list (option qualifier & binder & bv);
+  // meas : (meas:option term{Some? meas ==> isrec}); (* bs in scope *)
+  body : term; (* bs in scope *)
+}
+
+
 noeq
 type decl' =
   | FnDefn of fn_defn
   | FnDecl of fn_decl
+  | SlpropDefn of slprop_defn
 
 and decl = {
   d : decl';

src/checker/Pulse.Syntax.Builder.fst

@@ -63,6 +63,7 @@ let mk_rename_hint_type pairs goal tac_opt = RENAME { pairs; goal; tac_opt=map_o
 let mk_rewrite_hint_type t1 t2 tac_opt = REWRITE { t1; t2; tac_opt=map_opt tac_opt thunk; elaborated=false }
 let mk_fn_defn id isrec us bs comp meas body : decl' = FnDefn { id; isrec; us; bs; comp; meas; body }
 let mk_fn_decl id us bs comp : decl' = FnDecl { id; us; bs; comp; }
+let mk_slprop_defn id bs body : decl' = SlpropDefn { id; bs; body }
 let mk_decl d range : decl = {d; range}
 let mark_statement_sequence (s : st_term) : st_term = { s with seq_lhs = Sealed.seal true }
 let mark_not_source         (s : st_term) : st_term = { s with source = Sealed.seal false }

src/checker/Pulse.Syntax.Printer.fst

@@ -587,3 +587,8 @@ let decl_to_string (d:decl) : T.Tac string =
     "fn " ^
     fst (R.inspect_ident id) ^ " " ^
     String.concat " " (T.map (fun (_, b, _) -> binder_to_string b) bs)
+  | SlpropDefn {id;  bs; body} ->
+    "let predicate " ^
+     fst (R.inspect_ident id) ^ " " ^ 
+     String.concat " " (T.map (fun (_, b, _) -> binder_to_string b) bs) ^
+      " = " ^ term_to_string body ^ "\n"

src/ml/PulseSyntaxExtension_Parser.ml

@@ -13,6 +13,7 @@ let rewrite_token (tok:FP.token)
   = match tok with
     | IDENT "mut" -> PP.MUT
     | IDENT "invariant" -> PP.INVARIANT
+    | IDENT "predicate" -> PP.PREDICATE
     | IDENT "while" -> PP.WHILE
     | IDENT "fn" -> PP.FN
     | IDENT "each" -> PP.EACH

src/ml/PulseSyntaxExtension_SyntaxWrapper.ml

@@ -270,3 +270,5 @@ let fn_defn rng id isrec us bs comp meas body =
   PSB.mk_decl (PSB.mk_fn_defn id isrec us bs comp meas body) rng
 let fn_decl rng id us bs comp =
   PSB.mk_decl (PSB.mk_fn_decl id us bs comp) rng
+let slprop_defn rng id bs body =
+  PSB.mk_decl (PSB.mk_slprop_defn id bs body) rng

src/ml/pulseparser.mly

@@ -60,6 +60,9 @@ let mk_fn_defn q id is_rec us bs body range =
     | Inr (lambda, typ) ->
       PulseSyntaxExtension_Sugar.mk_fn_defn id is_rec us (List.flatten bs) (Inr typ) None (Inr lambda) range
 
+let mk_slprop_defn id bs body decors range =
+  PulseSyntaxExtension_Sugar.mk_slprop_defn id (List.flatten bs) body decors range
+
 let add_decorations decors ds =
   List.map (function
     | Inl p -> Inl (PulseSyntaxExtension_Sugar.add_decorations p decors)
@@ -68,7 +71,7 @@ let add_decorations decors ds =
 %}
 
 /* pulse specific tokens; rest are inherited from F* */
-%token MUT FN INVARIANT WHILE REF REWRITE FOLD EACH NOREWRITE
+%token MUT FN INVARIANT WHILE REF REWRITE FOLD EACH NOREWRITE PREDICATE
 %token GHOST ATOMIC UNOBSERVABLE
 %token OPENS  SHOW_PROOF_STATE
 %token PRESERVES
@@ -144,6 +147,12 @@ pulseDecl:
       | Inr (typ, None) ->
         raise_error_text (rr $loc) Fatal_SyntaxError "Ascriptions of lambdas without bodies are not yet supported"
     }
+  
+  | LET PREDICATE lid=lidentOrOperator bs=pulseBinderList EQUALS body=term
+    {
+      let decors = [] in
+      PulseSyntaxExtension_Sugar.SlpropDefn (mk_slprop_defn lid bs body decors (rr $loc))
+    }
 
 (* defining this as two tokens, option(qual) FN, seems to cause menhir to report an
    incorrect range when the first token is empty *)

src/syntax_extension/PulseSyntaxExtension.ASTBuilder.fst

@@ -145,9 +145,16 @@ let parse_extension_lang (contents:string) (r:FStarC.Range.range)
     match maybe_report_error first_error decls with
     | Inl err -> Inl err
     | Inr decls ->
+      let should_be_irreducible (d:PulseSyntaxExtension.Sugar.decl) =
+        let open PulseSyntaxExtension.Sugar in
+        match d with
+        | SlpropDefn {} -> false
+        | FnDefn {} | FnDecl {} -> true
+      in
       let id_and_range_of_decl (d:PulseSyntaxExtension.Sugar.decl) =
         let open PulseSyntaxExtension.Sugar in
         match d with
+        | SlpropDefn { id; range }
         | FnDefn { id; range }
         | FnDecl { id; range } -> id, range
       in
@@ -159,9 +166,20 @@ let parse_extension_lang (contents:string) (r:FStarC.Range.range)
         let decors =
           let open PulseSyntaxExtension.Sugar in
           match d with
+          | SlpropDefn { decorations }
           | FnDefn { decorations }
           | FnDecl { decorations } -> decorations
         in
+        let decors =
+          if not (should_be_irreducible d) then decors else
+          let attrs, quals = List.partition DeclAttributes? decors in
+          let attrs =
+            match attrs with
+            | [] -> [DeclAttributes[ str "uninterpreted_by_smt" r ]]
+            | DeclAttributes attrs :: tl -> DeclAttributes (str "uninterpreted_by_smt" r::attrs) :: tl
+          in
+          Qualifier Irreducible::quals@attrs
+        in
         let d =
           let open FStarC.Dyn in
           DeclToBeDesugared {
@@ -173,17 +191,7 @@ let parse_extension_lang (contents:string) (r:FStarC.Range.range)
             dep_scan=(fun cbs d -> PulseSyntaxExtension.Sugar.scan_decl cbs (undyn d));
           }
         in
-        let d =
-          let attrs, quals = List.partition DeclAttributes? decors in
-          let attrs =
-            match attrs with
-            | [] -> [DeclAttributes[ str "uninterpreted_by_smt" r ]]
-            | DeclAttributes attrs :: tl -> DeclAttributes (str "uninterpreted_by_smt" r::attrs) :: tl
-          in
-          let decors = Qualifier Irreducible::quals@attrs in
-          mk_decl d r decors
-        in
-        d
+        mk_decl d r decors
       in
       Inr <|
       List.map

src/syntax_extension/PulseSyntaxExtension.Desugar.fst

@@ -1007,6 +1007,12 @@ and desugar_decl (env:env_t)
   | Sugar.FnDecl { id; us; binders; ascription=Inr ascription; range } ->
     fail "Unexpected FnDecl with F* type" range
 
+  | Sugar.SlpropDefn { id; binders; body; range } ->
+    let! env, bs, bvs = desugar_binders env binders in
+    let! body = desugar_term env body in
+    let! qbs = map2 faux bs bvs in
+    return (SW.slprop_defn range id qbs body)
+
   | _ ->
     fail "Unexpected Pulse declaration" (Sugar.range_of_decl d)
 

src/syntax_extension/PulseSyntaxExtension.Sugar.fst

@@ -223,6 +223,17 @@ and fn_defn = {
   range:rng
 }
 
+and slprop_defn = {
+  id:ident;
+  // is_rec:bool;
+  // us:list ident;
+  binders:binders;
+  // measure:option A.term; // with binders in scope
+  body:A.term;
+  decorations:list A.decoration;  
+  range:rng
+}
+
 and let_init =
   | Array_initializer of array_init
   | Default_initializer of option A.term & list lambda
@@ -367,6 +378,7 @@ instance showable_stmt : showable stmt = {
 type decl =
   | FnDefn of fn_defn
   | FnDecl of fn_decl
+  | SlpropDefn of slprop_defn
 open FStarC.Class.Deq
 let eq_ident (i1 i2:Ident.ident) = i1 =? i2
 let eq_lident (i1 i2:Ident.lident) = i1 =? i2
@@ -395,6 +407,7 @@ let rec eq_decl (d1 d2:decl) =
   match d1, d2 with
   | FnDefn f1, FnDefn f2 -> eq_fn_defn f1 f2
   | FnDecl d1, FnDecl d2 -> eq_fn_decl d1 d2
+  | SlpropDefn d1, SlpropDefn d2 -> eq_slprop_defn d1 d2
   | _ -> false
 and eq_fn_decl (f1 f2:fn_decl) =
   eq_ident f1.id f2.id &&
@@ -409,6 +422,13 @@ and eq_fn_defn (f1 f2:fn_defn) =
   eq_ascription f1.ascription f2.ascription &&
   eq_opt AD.eq_term f1.measure f2.measure &&
   eq_body f1.body f2.body
+and eq_slprop_defn (f1 f2:slprop_defn) =
+  eq_ident f1.id f2.id &&
+  // f1.is_rec = f2.is_rec &&
+  // forall2 eq_ident f1.us f2.us &&
+  forall2 AD.eq_binder f1.binders f2.binders &&
+  // eq_opt AD.eq_term f1.measure f2.measure &&
+  AD.eq_term f1.body f2.body
 and eq_ascription (a1 a2:either computation_type (option A.term)) =
   match a1, a2 with
   | Inl c1, Inl c2 -> eq_computation_type c1 c2
@@ -543,6 +563,7 @@ let rec scan_decl (cbs:A.dep_scan_callbacks) (d:decl) : unit =
   match d with
   | FnDefn f -> scan_fn_defn cbs f
   | FnDecl d -> scan_fn_decl cbs d
+  | SlpropDefn d -> scan_slprop_defn cbs d
 and scan_fn_decl (cbs:A.dep_scan_callbacks) (f:fn_decl) =
   iter (scan_binder cbs) f.binders;
   scan_ascription cbs f.ascription
@@ -551,6 +572,10 @@ and scan_fn_defn (cbs:A.dep_scan_callbacks) (f:fn_defn) =
   ieither (scan_computation_type cbs) (iopt cbs.scan_term) f.ascription;
   iopt cbs.scan_term f.measure;
   ieither (scan_stmt cbs) (scan_lambda cbs) f.body
+and scan_slprop_defn (cbs:A.dep_scan_callbacks) (f:slprop_defn) =
+  iter (scan_binder cbs) f.binders;
+  // iopt cbs.scan_term f.measure;
+  cbs.scan_term f.body
 and scan_binder (cbs:A.dep_scan_callbacks) (b:binder) =
   cbs.scan_binder b
 and scan_ascription (cbs:A.dep_scan_callbacks) (a:either computation_type (option A.term)) =
@@ -645,6 +670,7 @@ let range_of_decl (d:decl) =
   match d with
   | FnDefn f -> f.range
   | FnDecl d -> d.range
+  | SlpropDefn d -> d.range
 (* Convenience builders for use from OCaml/Menhir, since field names get mangled in OCaml *)
 let mk_comp tag literally annots range =
   {
@@ -657,6 +683,7 @@ let add_decorations d ds =
   match d with
   | FnDefn f -> FnDefn { f with decorations=ds @ f.decorations }
   | FnDecl f -> FnDecl { f with decorations=ds @ f.decorations }
+  | SlpropDefn f -> SlpropDefn { f with decorations=ds @ f.decorations }
 
 // let mk_slprop_exists binders body = SLPropExists { binders; body }
 let mk_expr e args = Expr { e; args }
@@ -676,6 +703,9 @@ let mk_fn_defn id is_rec us binders ascription measure body decorations range
 let mk_fn_decl id us binders ascription decorations range
 : fn_decl
 = { id; us; binders; ascription; decorations; range }
+let mk_slprop_defn id binders body decorations range
+: slprop_defn
+= { id; binders; body; decorations; range }
 let mk_open lid = Open lid
 let mk_proof_hint_with_binders ht bs =  ProofHintWithBinders { hint_type=ht; binders=bs }
 let mk_lambda bs ascription body range : lambda = { binders=bs; ascription; body; range }