Add a resugaring extension for Pulse

src/syntax_extension/PulseSyntaxExtension.Printing.fst

@@ -0,0 +1,119 @@
+(*
+   Copyright 2023 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module PulseSyntaxExtension.Printing
+
+open FStarC
+open FStarC.Effect
+
+module SW = PulseSyntaxExtension.SyntaxWrapper
+module A = FStarC.Parser.AST
+module S = FStarC.Syntax.Syntax
+module U = FStarC.Syntax.Util
+module SS = FStarC.Syntax.Subst
+module DsEnv = FStarC.Syntax.DsEnv
+
+open FStarC.Syntax.Syntax
+open FStarC.Syntax.Resugar
+open FStarC.Class.Show
+open FStarC.Class.PP
+open PulseSyntaxExtension.Env
+open FStarC.Pprint
+
+let hua (t:term) : option (S.fv & list S.universe & S.args) =
+  let t = U.unmeta t in
+  let hd, args = U.head_and_args_full t in
+  let hd = U.unmeta hd in
+  match (SS.compress hd).n with
+  | Tm_fvar fv -> Some (fv, [], args)
+  | Tm_uinst ({ n = Tm_fvar fv }, us) -> Some (fv, us, args)
+  | _ -> None
+
+let p = FStarC.Parser.ToDocument.term_to_document
+
+let vconcat (ds:list document) : document =
+  match ds with
+  | h::t ->
+    List.fold_left (fun l r -> if r = empty then l else l ^^ hardline ^^ r) h t
+  | [] ->
+    empty
+
+let print_pulse_computation_type
+  (rng : Range.t)
+  (e : DsEnv.env)
+  (tag : string)
+  (a opens pre post : term)
+  : A.term
+  =
+  let retname_opt, post =
+    match U.abs_formals post with
+    | [b], t, _ ->
+      let bv = b.binder_bv in
+      if FStarC.Class.Setlike.mem bv (Syntax.Free.names t) then
+        Some b.binder_bv, t
+      else
+        None, t
+    | _ ->
+      // If it returns unit, just apply the post to `()`
+      if U.term_eq a S.t_unit then
+        None, U.mk_app post [S.as_arg U.exp_unit]
+      else
+        let x = S.gen_bv "_ret" (Some rng) a in
+        Some x, U.mk_app post [S.as_arg (S.bv_to_name x)]
+  in
+  let d =
+    align <| hang 2 <| vconcat <| List.map (fun d -> group (hang 2 d)) [
+      (if tag <> ""
+        then doc_of_string tag ^/^ doc_of_string "fn"
+        else doc_of_string "fn");
+      doc_of_string "requires" ^/^ p (resugar_term' e pre);
+      (if U.term_eq opens SW.tm_emp_inames then empty
+       else
+        (doc_of_string "opens"    ^/^ p (resugar_term' e opens)));
+      (match retname_opt with
+       | None when U.term_eq a S.t_unit -> empty
+       | None ->
+        doc_of_string "returns" ^/^ p (resugar_term' e a)
+       | Some bv ->
+        doc_of_string "returns"  ^/^ pp bv.ppname ^/^ colon ^/^ p (resugar_term' e a));
+      doc_of_string "ensures"  ^/^ p (resugar_term' e post);
+    ]
+  in
+  A.mk_term (A.LitDoc d) rng A.Expr
+
+let resugar_pulse_type (e:DsEnv.env) (t:S.term) : A.term =
+  let r = hua t in
+  if None? r then raise SkipResugar;
+  let Some (fv, us, args) = r in
+  let tag, a, opens, pre, post =
+    match args with
+    | [(a, None); (pre, None); (post, None)]
+      when S.fv_eq_lid fv stt_lid ->
+        ("", a, SW.tm_emp_inames, pre, post)
+
+    | [(a, None); _obs; (opens, None); (pre, None); (post, None)]
+      when S.fv_eq_lid fv stt_atomic_lid ->
+        ("atomic", a, opens, pre, post)
+
+    | [(a, None); (opens, None); (pre, None); (post, None)]
+      when S.fv_eq_lid fv stt_ghost_lid ->
+        ("ghost", a, opens, pre, post)
+
+    | _ -> raise SkipResugar
+  in
+  print_pulse_computation_type (pos t) e tag a opens pre post
+
+let _ = register_pass resugar_pulse_type

test/LoopInvariants.fst.output.expected

@@ -1,3 +1,8 @@
+* Warning 274:
+  - Implicitly opening namespace 'fstar.tactics.' shadows module 'print' in file
+    "Print.fst".
+  - Rename "Print.fst" to avoid conflicts.
+
 * Info at LoopInvariants.fst(64,17-64,20):
   - Expected failure:
   - When using multiple invariants, they must all be in the "new" style without a binder.

test/MatchBasic.fst.output.expected

@@ -1,3 +1,8 @@
+* Warning 274:
+  - Implicitly opening namespace 'fstar.tactics.' shadows module 'print' in file
+    "Print.fst".
+  - Rename "Print.fst" to avoid conflicts.
+
 * Info at MatchBasic.fst(154,2-156,3):
   - Expected failure:
   - Could not verify that this match is exhaustive.

test/Print.fst

@@ -0,0 +1,25 @@
+module Print
+
+#lang-pulse
+open Pulse
+
+fn test (x : ref int)
+  requires x |-> 'v
+  returns  old : int
+  ensures  x |-> ('v + 1) ** pure (old == old)
+{
+  let old = !x;
+  x := !x + 1;
+  old
+}
+#check test
+
+assume val q : int -> slprop
+assume val test2 : stt_ghost int emp_inames emp q
+
+#check test2
+
+assume val r : unit -> slprop
+assume val test3 : stt_ghost unit emp_inames emp r
+
+#check test3

test/Print.fst.output.expected

@@ -0,0 +1,32 @@
+* Warning 274:
+  - Implicitly opening namespace 'fstar.tactics.' shadows module 'print' in file
+    "Print.fst".
+  - Rename "Print.fst" to avoid conflicts.
+
+* Info at Print.fst(15,0-15,11):
+  - Term
+    Print.test
+    has type
+    x: Pulse.Lib.Reference.ref Prims.int
+      -> fn
+           requires x |-> 'v
+           returns x : Prims.int
+           ensures x |-> ('v + 1) ** Pulse.Lib.Core.pure (x == x)
+
+* Info at Print.fst(20,0-20,12):
+  - Term
+    Print.test2
+    has type
+    ghost fn
+      requires Pulse.Lib.Core.emp
+      returns _ret : Prims.int
+      ensures Print.q _ret
+
+* Info at Print.fst(25,0-25,12):
+  - Term
+    Print.test3
+    has type
+    ghost fn
+      requires Pulse.Lib.Core.emp
+      ensures Print.r ()
+

test/Test.Recursion.fst.output.expected

@@ -1,11 +1,15 @@
+* Warning 274:
+  - Implicitly opening namespace 'fstar.tactics.' shadows module 'print' in file
+    "Print.fst".
+  - Rename "Print.fst" to avoid conflicts.
+
 * Info at Test.Recursion.fst(94,2-94,20):
   - Expected failure:
   - Ill-typed term: test_ghost_loop ()
   - Expected a term of type
-      Pulse.Lib.Core.stt_ghost Prims.unit
-        Pulse.Lib.Core.emp_inames
-        Pulse.Lib.Core.emp
-        (fun _ -> Pulse.Lib.Core.emp)
+      ghost fn
+        requires Pulse.Lib.Core.emp
+        ensures Pulse.Lib.Core.emp
   - Could not prove termination
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
@@ -14,10 +18,9 @@
   - Expected failure:
   - Ill-typed term: test5' (z - 1) (y - 1)
   - Expected a term of type
-      Pulse.Lib.Core.stt_ghost Prims.unit
-        Pulse.Lib.Core.emp_inames
-        Pulse.Lib.Core.emp
-        (fun _ -> Pulse.Lib.Core.emp)
+      ghost fn
+        requires Pulse.Lib.Core.emp
+        ensures Pulse.Lib.Core.emp
   - Could not prove termination
   - The SMT solver could not prove the query. Use --query_stats for more
     details.

test/bug-reports/Bug174.fst.output.expected

@@ -2,11 +2,11 @@
   - Expected failure:
   - Ill-typed term: !r
   - Expected a term of type
-      Pulse.Lib.Core.stt FStar.SizeT.t
-        (r |-> Pulse.Class.PtsTo.Frac 1.0R v)
-        (fun x ->
-            r |-> Pulse.Class.PtsTo.Frac 1.0R v **
-            Pulse.Lib.Core.rewrites_to x v)
+      fn
+        requires r |-> Pulse.Class.PtsTo.Frac 1.0R v
+        returns x : FStar.SizeT.t
+        ensures
+          r |-> Pulse.Class.PtsTo.Frac 1.0R v ** Pulse.Lib.Core.rewrites_to x v
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.

test/bug-reports/Bug206.fst.output.expected

@@ -2,9 +2,9 @@
   - Expected failure:
   - Ill-typed term: Bug206.test x
   - Expected a term of type
-      Pulse.Lib.Core.stt Prims.unit
-        Pulse.Lib.Core.emp
-        (fun _ -> Pulse.Lib.Core.emp)
+      fn
+        requires Pulse.Lib.Core.emp
+        ensures Pulse.Lib.Core.emp
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.

test/bug-reports/Bug266.fst.output.expected

@@ -13,9 +13,8 @@
   - In typing environment:
       __#65 : Prims.squash (__ == Bug266.my_intro Prims.l_False),
       __#64 :
-        Pulse.Lib.Core.stt_ghost Prims.unit
-          Pulse.Lib.Core.emp_inames
-          (Pulse.Lib.Core.pure Prims.l_False)
-          Bug266.post,
+        ghost fn
+          requires Pulse.Lib.Core.pure Prims.l_False
+          ensures Bug266.post (),
       uu___0#50 : Prims.unit
 

test/bug-reports/PartialApp.fst.output.expected

@@ -9,8 +9,8 @@
   - Tactic failed
   - This function is partially applied. Remaining type:
       y: t
-        -> Pulse.Lib.Core.stt Prims.unit
-            Pulse.Lib.Core.emp
-            (fun _ -> Pulse.Lib.Core.emp)
+        -> fn
+             requires Pulse.Lib.Core.emp
+             ensures Pulse.Lib.Core.emp
   - Did you forget to apply some arguments?
 

test/nolib/Check.fst.output.expected

@@ -3,8 +3,8 @@
     Check.test
     has type
     x: Prims.int
-      -> Pulse.Lib.Core.stt_ghost Prims.int
-          Pulse.Lib.Core.emp_inames
-          (Pulse.Lib.Core.pure (x == 'y))
-          (fun x -> Pulse.Lib.Core.pure (x == x))
+      -> ghost fn
+           requires Pulse.Lib.Core.pure (x == 'y)
+           returns x : Prims.int
+           ensures Pulse.Lib.Core.pure (x == x)