diff --git a/share/pulse/examples/parix/TaskPool.fsti b/lib/pulse/lib/Pulse.Lib.Task.fsti similarity index 95% rename from share/pulse/examples/parix/TaskPool.fsti rename to lib/pulse/lib/Pulse.Lib.Task.fsti index 5f127f357..59fc731b7 100644 --- a/share/pulse/examples/parix/TaskPool.fsti +++ b/lib/pulse/lib/Pulse.Lib.Task.fsti @@ -14,10 +14,9 @@ limitations under the License. *) -module TaskPool +module Pulse.Lib.Task open Pulse.Lib.Pervasives -open Pulse.Lib.SpinLock open Pulse.Lib.Par.Pledge module T = FStar.Tactics @@ -109,6 +108,8 @@ val teardown_pool (p:pool) : stt unit (pool_alive #full_perm p) (fun _ -> pool_done p) +(* Or, have at least an epsilon of permission over it, and know that +the rest of it (1-e) is "sunk" into the pool itself. *) val teardown_pool' (#is : Pulse.Lib.InvList.invlist) (p:pool) (f:perm{f `lesser_perm` full_perm}) diff --git a/share/pulse/examples/MSort.fst b/share/pulse/examples/MSort.Base.fst similarity index 88% rename from share/pulse/examples/MSort.fst rename to share/pulse/examples/MSort.Base.fst index 6dc0b0371..bcee4951e 100644 --- a/share/pulse/examples/MSort.fst +++ b/share/pulse/examples/MSort.Base.fst @@ -1,4 +1,4 @@ -module MSort +module MSort.Base open FStar.Ghost open Pulse.Lib.Pervasives @@ -7,7 +7,6 @@ module S = FStar.Seq module SZ = FStar.SizeT open MSort.SeqLemmas - #set-options "--z3rlimit 20" ```pulse @@ -180,35 +179,3 @@ merge_impl A.free sw2; } ``` - - -```pulse -fn -rec -msort - (a : array int) - (lo hi : SZ.t) - (s : erased (S.seq int)) - requires pts_to_range a (SZ.v lo) (SZ.v hi) (reveal s) - ensures pts_to_range a (SZ.v lo) (SZ.v hi) (sort (reveal s)) -{ - pts_to_range_prop a; - if ((hi `SZ.sub` lo) `SZ.lt` 2sz) { - pts_to_range_prop a; - singl_is_sorted s; - () - } else { - let mid : SZ.t = lo `SZ.add` ((hi `SZ.sub` lo) `SZ.div` 2sz); - - pts_to_range_split a (SZ.v lo) (SZ.v mid) (SZ.v hi); - - with s1. assert (pts_to_range a (SZ.v lo) (SZ.v mid) s1); - with s2. assert (pts_to_range a (SZ.v mid) (SZ.v hi) s2); - - msort a lo mid s1; - msort a mid hi s2; - - merge_impl a lo mid hi () (sort s1) (sort s2); - } -} -``` diff --git a/share/pulse/examples/MSort.Parallel.fst b/share/pulse/examples/MSort.Parallel.fst new file mode 100644 index 000000000..1059e0e14 --- /dev/null +++ b/share/pulse/examples/MSort.Parallel.fst @@ -0,0 +1,43 @@ +module MSort.Parallel + +open Pulse.Lib.Pervasives +module S = FStar.Seq +module SZ = FStar.SizeT +open MSort.SeqLemmas +open MSort.Base + +```pulse +fn +rec +msort + (a : array int) + (lo hi : SZ.t) + (s : erased (S.seq int)) + requires pts_to_range a (SZ.v lo) (SZ.v hi) (reveal s) + ensures pts_to_range a (SZ.v lo) (SZ.v hi) (sort (reveal s)) +{ + pts_to_range_prop a; + if ((hi `SZ.sub` lo) `SZ.lt` 2sz) { + pts_to_range_prop a; + singl_is_sorted s; + () + } else { + let mid : SZ.t = lo `SZ.add` ((hi `SZ.sub` lo) `SZ.div` 2sz); + + pts_to_range_split a (SZ.v lo) (SZ.v mid) (SZ.v hi); + + with s1. assert (pts_to_range a (SZ.v lo) (SZ.v mid) s1); + with s2. assert (pts_to_range a (SZ.v mid) (SZ.v hi) s2); + + parallel + requires pts_to_range a (SZ.v lo) (SZ.v mid) (reveal s1) + and pts_to_range a (SZ.v mid) (SZ.v hi) (reveal s2) + ensures pts_to_range a (SZ.v lo) (SZ.v mid) (sort (reveal s1)) + and pts_to_range a (SZ.v mid) (SZ.v hi) (sort (reveal s2)) + { msort a lo mid s1; } + { msort a mid hi s2; }; + + merge_impl a lo mid hi () (sort s1) (sort s2); + } +} +``` diff --git a/share/pulse/examples/MSort.Sequential.fst b/share/pulse/examples/MSort.Sequential.fst new file mode 100644 index 000000000..e7adea255 --- /dev/null +++ b/share/pulse/examples/MSort.Sequential.fst @@ -0,0 +1,36 @@ +module MSort.Sequential + +open Pulse.Lib.Pervasives +module S = FStar.Seq +module SZ = FStar.SizeT +open MSort.SeqLemmas +open MSort.Base + +```pulse +fn rec msort + (a : array int) + (lo hi : SZ.t) + (s : erased (S.seq int)) + requires pts_to_range a (SZ.v lo) (SZ.v hi) (reveal s) + ensures pts_to_range a (SZ.v lo) (SZ.v hi) (sort (reveal s)) +{ + pts_to_range_prop a; + if ((hi `SZ.sub` lo) `SZ.lt` 2sz) { + pts_to_range_prop a; + singl_is_sorted s; + () + } else { + let mid : SZ.t = lo `SZ.add` ((hi `SZ.sub` lo) `SZ.div` 2sz); + + pts_to_range_split a (SZ.v lo) (SZ.v mid) (SZ.v hi); + + with s1. assert (pts_to_range a (SZ.v lo) (SZ.v mid) s1); + with s2. assert (pts_to_range a (SZ.v mid) (SZ.v hi) s2); + + msort a lo mid s1; + msort a mid hi s2; + + merge_impl a lo mid hi () (sort s1) (sort s2); + } +} +``` diff --git a/share/pulse/examples/MSortPar.fst b/share/pulse/examples/MSort.Task.fst similarity index 65% rename from share/pulse/examples/MSortPar.fst rename to share/pulse/examples/MSort.Task.fst index 066ece640..f92909e17 100644 --- a/share/pulse/examples/MSortPar.fst +++ b/share/pulse/examples/MSort.Task.fst @@ -1,20 +1,14 @@ -module MSortPar +module MSort.Task -open FStar.Ghost open Pulse.Lib.Pervasives -module A = Pulse.Lib.Array module S = FStar.Seq module SZ = FStar.SizeT - -open MSort open MSort.SeqLemmas -open TaskPool -open Pulse.Lib.Par.Pledge +open MSort.Base +open Pulse.Lib.Task ```pulse -fn -rec -t_msort_par +fn rec t_msort_par (p : pool) (f : perm) (a : array int) @@ -48,3 +42,21 @@ t_msort_par } } ``` + +```pulse +fn rec msort + (nthr : pos) + (a : array int) + (lo hi : SZ.t) + (s : erased (S.seq int)) + requires pts_to_range a (SZ.v lo) (SZ.v hi) (reveal s) + ensures pts_to_range a (SZ.v lo) (SZ.v hi) (sort (reveal s)) +{ + // No need for pledge reasoning here as t_msort_par is synchronous, even + // if it parallelizes internally. + let p = setup_pool nthr; + t_msort_par p full_perm a lo hi s; + teardown_pool p; + drop_ (pool_done p); +} +``` diff --git a/share/pulse/examples/PledgeArith.fst b/share/pulse/examples/PledgeArith.fst index 1daaec369..d70277849 100644 --- a/share/pulse/examples/PledgeArith.fst +++ b/share/pulse/examples/PledgeArith.fst @@ -4,7 +4,7 @@ module PledgeArith open Pulse.Lib.Pervasives open Pulse.Lib.InvList -module T = TaskPool +module T = Pulse.Lib.Task open Pulse.Lib.Par.Pledge ```pulse diff --git a/share/pulse/examples/Quicksort.Task.fst b/share/pulse/examples/Quicksort.Task.fst index 08b352464..4e107926a 100644 --- a/share/pulse/examples/Quicksort.Task.fst +++ b/share/pulse/examples/Quicksort.Task.fst @@ -23,14 +23,10 @@ module SZ = FStar.SizeT open Pulse.Lib.InvList -module T = TaskPool +module T = Pulse.Lib.Task open Quicksort.Base open Pulse.Lib.Par.Pledge - -let quicksort_pre a lo hi s0 lb rb : vprop = - A.pts_to_range a lo hi s0 ** pure (pure_pre_quicksort a lo hi lb rb s0) - let quicksort_post a lo hi s0 lb rb : vprop = exists* s. (A.pts_to_range a lo hi s ** pure (pure_post_quicksort a lo hi lb rb s0 s)) @@ -63,8 +59,8 @@ fn rec t_quicksort T.share_alive p f; T.share_alive p (half_perm f); - t_quicksort p (half_perm (half_perm f)) a r._2 hi pivot rb; T.spawn_ p #(half_perm f) (fun () -> t_quicksort p (half_perm (half_perm f)) a lo r._1 lb pivot); + t_quicksort p (half_perm (half_perm f)) a r._2 hi pivot rb; return_pledge [] (T.pool_done p) (T.pool_alive #(half_perm f) p ** A.pts_to_range a r._1 r._2 s2); squash_pledge _ _ _; diff --git a/share/pulse/examples/parix/ParallelFor.fst b/share/pulse/examples/parix/ParallelFor.fst index 7f90c645d..8dbcf0439 100644 --- a/share/pulse/examples/parix/ParallelFor.fst +++ b/share/pulse/examples/parix/ParallelFor.fst @@ -18,7 +18,7 @@ module ParallelFor open Pulse.Lib.Pervasives open Pulse.Lib.Fixpoints -open TaskPool +open Pulse.Lib.Task open FStar.Real open Pulse.Lib.Par.Pledge open Pulse.Lib.InvList @@ -238,18 +238,6 @@ assume val unfrac_n (n:pos) (p:pool) (e:perm) : stt unit (range (fun i -> pool_alive #(div_perm e n) p) 0 n) (fun () -> pool_alive #e p) -#set-options "--print_implicits --print_universes" - -// FIXME: arguments with defaults (i.e. metaargs with tactics) -// make functions not be recognized by Pulse -val gspawn_ - (#pre #post : _) - (#e : perm) - (p:pool) (f : unit -> stt unit pre (fun _ -> post)) - : stt unit (pool_alive #e p ** pre) - (fun prom -> pool_alive #e p ** pledge [] (pool_done p) post) -let gspawn_ p f = TaskPool.spawn_ p f - ```pulse fn spawned_f_i (p:pool) @@ -261,7 +249,7 @@ fn spawned_f_i requires emp ** (pre i ** pool_alive #e p) ensures emp ** (pledge [] (pool_done p) (post i) ** pool_alive #e p) { - gspawn_ #(pre i) #(post i) #e p (fun () -> f i) + spawn_ #(pre i) #(post i) p #e (fun () -> f i) } ``` @@ -351,7 +339,7 @@ fn spawned_f_i_alt requires pool_alive p ** pre i ensures pool_alive p ** pledge [] (pool_done p) (post i) { - gspawn_ #(pre i) #(post i) #full_perm p (fun () -> f i) + spawn_ #(pre i) #(post i) p #full_perm (fun () -> f i) } ``` @@ -555,16 +543,16 @@ fn h_for_task p_split pre lo mid hi (); - gspawn_ #(pool_alive #(half_perm (half_perm e)) p ** range pre lo mid) + spawn_ #(pool_alive #(half_perm (half_perm e)) p ** range pre lo mid) #(pledge [] (pool_done p) (range post lo mid)) - #(half_perm e) p + #(half_perm e) (h_for_task__ p (half_perm (half_perm e)) pre post f lo mid); - gspawn_ #(pool_alive #(half_perm (half_perm e)) p ** range pre mid hi) + spawn_ #(pool_alive #(half_perm (half_perm e)) p ** range pre mid hi) #(pledge [] (pool_done p) (range post mid hi)) - #(half_perm e) p + #(half_perm e) (h_for_task__ p (half_perm (half_perm e)) pre post f mid hi); (* We get this complicated pledge [] from the spawns above. We can @@ -625,10 +613,10 @@ parallel_for_hier assert (pool_alive #one_half p ** pool_alive #one_half p); - gspawn_ #(pool_alive #one_half p ** range pre 0 n) + spawn_ #(pool_alive #one_half p ** range pre 0 n) #(pledge [] (pool_done p) (range post 0 n)) - #one_half p + #one_half (h_for_task p one_half pre post f 0 n); (* We get this complicated pledge [] from the spawn above. We can diff --git a/share/pulse/examples/parix/TaskPool.Examples.fst b/share/pulse/examples/parix/TaskPool.Examples.fst index 77d13c919..6ee1cc949 100644 --- a/share/pulse/examples/parix/TaskPool.Examples.fst +++ b/share/pulse/examples/parix/TaskPool.Examples.fst @@ -18,7 +18,7 @@ module TaskPool.Examples open Pulse.Lib.Pervasives open Pulse.Lib.Par.Pledge -open TaskPool +open Pulse.Lib.Task assume val qsv : nat -> vprop diff --git a/share/pulse/examples/parix/TaskPool.fst b/share/pulse/examples/parix/TaskPool.fst deleted file mode 100644 index 65dfe8a37..000000000 --- a/share/pulse/examples/parix/TaskPool.fst +++ /dev/null @@ -1,91 +0,0 @@ -(* - 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 TaskPool - -open Pulse.Lib.Pervasives -open Pulse.Lib.SpinLock -open Pulse.Lib.Par.Pledge - -module T = FStar.Tactics.V2 - -let pool : Type0 = magic () -let pool_alive (#[T.exact (`full_perm)]p : perm) (pool:pool) : vprop - = magic() -let pool_done = magic () - -let setup_pool (n:nat) - = magic () - -let task_handle pool a post = magic () -let joinable #p #a #post th = magic () -let joined #p #a #post th = magic () - -let handle_solved #p #a #post th = magic() - -let spawn #a #pre #post p #e = magic () - -let spawn_ #pre #post p #e = magic () - -let must_be_done = magic () - -let join0 = magic () - -#set-options "--print_universes" - -#set-options "--print_universes" - -```pulse -fn __extract - (#p:pool) - (#a:Type0) - (#post : (a -> vprop)) - (th : task_handle p a post) - requires handle_solved th - returns x:a - ensures post x -{ - admit() -} -``` - -let extract = __extract - -let share_alive _ _ = admit() -let gather_alive _ _ = admit() - -```pulse -fn __join - (#p:pool) - (#a:Type0) - (#post : (a -> vprop)) - (th : task_handle p a post) - requires joinable th - returns x:a - ensures post x -{ - join0 th; - extract th -} -``` -let join = __join - -let teardown_pool - (p:pool) - : stt unit (pool_alive p) (fun _ -> pool_done p) - = magic () - -let teardown_pool' p e = magic () diff --git a/src/checker/Pulse.PP.fst b/src/checker/Pulse.PP.fst index 8bcbb0bc5..1e8377e02 100644 --- a/src/checker/Pulse.PP.fst +++ b/src/checker/Pulse.PP.fst @@ -28,7 +28,6 @@ open Pulse.Syntax.Printer open Pulse.Show (* A helper to create wrapped text *) -val text : string -> FStar.Stubs.Pprint.document let text (s:string) : FStar.Stubs.Pprint.document = flow (break_ 1) (words s) @@ -41,25 +40,20 @@ before the doc, so if you want to format something as you should write hdr ^^ indent (subdoc) ^/^ tail. Note the ^^ vs ^/^. *) -val indent : document -> document let indent d = nest 2 (hardline ^^ align d) -class printable (a:Type) = { - pp : a -> Tac document; -} - (* Repurposing a show instance *) let from_show #a {| d : tac_showable a |} : printable a = { pp = (fun x -> arbitrary_string (show x)); } -instance _ : printable string = from_show -instance _ : printable unit = from_show -instance _ : printable bool = from_show -instance _ : printable int = from_show +instance printable_string : printable string = from_show +instance printable_unit : printable unit = from_show +instance printable_bool : printable bool = from_show +instance printable_int : printable int = from_show -instance _ : printable ctag = from_show +instance printable_ctag : printable ctag = from_show instance printable_option (a:Type) (_ : printable a) : printable (option a) = { pp = (function None -> doc_of_string "None" @@ -74,15 +68,15 @@ let rec separate_map (sep: document) (f : 'a -> Tac document) (l : list 'a) : Ta | [x] -> f x | x::xs -> f x ^^ sep ^/^ separate_map sep f xs -instance showable_list (a:Type) (_ : printable a) : printable (list a) = { +instance printable_list (a:Type) (_ : printable a) : printable (list a) = { pp = (fun l -> brackets (separate_map comma pp l)) } -instance _ : printable term = from_show -instance _ : printable universe = from_show -instance _ : printable comp = from_show +instance printable_term : printable term = from_show +instance printable_universe : printable universe = from_show +instance printable_comp : printable comp = from_show -instance _ : printable env = { +instance printable_env : printable env = { pp = Pulse.Typing.Env.env_to_doc; } @@ -94,7 +88,7 @@ let pp_record (flds : list (string & document)) : Tac document = in braces (align flds_doc) -instance _ : printable post_hint_t = { +instance printable_post_hint_t : printable post_hint_t = { pp = (fun (h:post_hint_t) -> pp_record [ "g", pp h.g ; "effect_annot", pp h.effect_annot @@ -107,3 +101,18 @@ instance _ : printable post_hint_t = { instance printable_fstar_term : printable Reflection.V2.term = { pp = (fun t -> doc_of_string (Tactics.V2.term_to_string t)) } + +instance printable_tuple2 (a b:Type) + (_:printable a) (_:printable b) : printable (a * b) = { + pp = (fun (x, y) -> parens (separate comma [pp x; pp y])); + } + +instance printable_tuple3 (a b c:Type) + (_:printable a) (_:printable b) (_:printable c) : printable (a * b * c) = { + pp = (fun (x, y, z) -> parens (separate comma [pp x; pp y; pp z])); + } + +instance printable_tuple4 (a b c d:Type) + (_:printable a) (_:printable b) (_:printable c) (_:printable d) : printable (a * b * c * d) = { + pp = (fun (x, y, z, w) -> parens (separate comma [pp x; pp y; pp z; pp w])); + } diff --git a/src/checker/Pulse.PP.fsti b/src/checker/Pulse.PP.fsti new file mode 100644 index 000000000..d481f4245 --- /dev/null +++ b/src/checker/Pulse.PP.fsti @@ -0,0 +1,74 @@ +(* + 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 Pulse.PP + +include FStar.Stubs.Pprint + +open FStar.Tactics +open Pulse.Typing +open Pulse.Syntax.Base + +(* A helper to create wrapped text *) +val text : string -> FStar.Stubs.Pprint.document + +(* Nests a document 2 levels deep, as a block. It inserts a hardline +before the doc, so if you want to format something as + + hdr + subdoc + tail + + you should write hdr ^^ indent (subdoc) ^/^ tail. Note the ^^ vs ^/^. +*) +val indent : document -> document + +class printable (a:Type) = { + pp : a -> Tac document; +} + +instance val printable_string : printable string +instance val printable_unit : printable unit +instance val printable_bool : printable bool +instance val printable_int : printable int +instance val printable_ctag : printable ctag + +instance val printable_option (a:Type) (_ : printable a) : printable (option a) +instance val printable_list (a:Type) (_ : printable a) : printable (list a) + +instance val printable_term : printable term +instance val printable_universe : printable universe +instance val printable_comp : printable comp + +instance val printable_env : printable env + +instance val pp_effect_annot : printable effect_annot + +instance val printable_post_hint_t : printable post_hint_t + +instance val printable_fstar_term : printable Reflection.V2.term + +instance val printable_tuple2 (a b:Type) + (_:printable a) (_:printable b) + : printable (a * b) + +instance val printable_tuple3 (a b c:Type) + (_:printable a) (_:printable b) (_:printable c) + : printable (a * b * c) + +instance val printable_tuple4 (a b c d:Type) + (_:printable a) (_:printable b) (_:printable c) (_:printable d) + : printable (a * b * c * d) diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml b/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml index e8868fefe..da56ff8b5 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml @@ -1904,7 +1904,7 @@ let (check_effect_annotation : (Prims.of_int (80))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term i)) (fun uu___1 -> @@ -1977,7 +1977,7 @@ let (check_effect_annotation : (Prims.of_int (93))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term j)) (fun uu___2 -> @@ -2271,7 +2271,7 @@ let (check_effect_annotation : (Prims.of_int (80))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term i)) (fun uu___1 -> @@ -2344,7 +2344,7 @@ let (check_effect_annotation : (Prims.of_int (93))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term j)) (fun uu___2 -> diff --git a/src/ocaml/plugin/generated/Pulse_Checker_AssertWithBinders.ml b/src/ocaml/plugin/generated/Pulse_Checker_AssertWithBinders.ml index f73c88b60..065fc8e1e 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_AssertWithBinders.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_AssertWithBinders.ml @@ -3816,7 +3816,7 @@ let (check : (Prims.of_int (27))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term pre)) (fun uu___1 -> diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Prover.ml b/src/ocaml/plugin/generated/Pulse_Checker_Prover.ml index 79298bd46..906a91fec 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Prover.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Prover.ml @@ -216,7 +216,8 @@ let rec (prove_pures : (Prims.of_int (15))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 p)) + Pulse_PP.printable_term + p)) (fun uu___1 -> FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -1031,7 +1032,7 @@ let rec (prover : (Prims.of_int (29))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term q)) (fun uu___9 -> @@ -1129,7 +1130,7 @@ let rec (prover : (Prims.of_int (62))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term (Pulse_Typing_Combinators.list_as_vprop pst3.Pulse_Checker_Prover_Base.remaining_ctxt))) (fun @@ -1279,7 +1280,7 @@ let rec (prover : (Prims.of_int (46))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term preamble.Pulse_Checker_Prover_Base.goals)) (fun uu___11 @@ -1381,7 +1382,7 @@ let rec (prover : (Prims.of_int (45))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term preamble.Pulse_Checker_Prover_Base.ctxt)) (fun uu___12 @@ -2855,7 +2856,7 @@ let (prove_post_hint : (Prims.of_int (24))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term ty)) (fun uu___1 -> @@ -2924,7 +2925,7 @@ let (prove_post_hint : (Prims.of_int (38))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term post_hint1.Pulse_Typing.ret_ty)) (fun uu___2 -> @@ -3175,7 +3176,7 @@ let (prove_post_hint : (Prims.of_int (38))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term remaining_ctxt)) (fun uu___5 -> diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Pure.ml b/src/ocaml/plugin/generated/Pulse_Checker_Pure.ml index 9afb0895c..93abcfe79 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Pure.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Pure.ml @@ -230,7 +230,8 @@ let (check_ln : (Prims.of_int (45)) (Prims.of_int (49))))) (Obj.magic - (Pulse_PP.pp Pulse_PP.uu___19 + (Pulse_PP.pp + Pulse_PP.printable_string label)) (fun uu___1 -> FStar_Tactics_Effect.lift_div_tac @@ -2099,7 +2100,7 @@ let (ill_typed_term : (FStar_Range.mk_range "Pulse.Checker.Pure.fst" (Prims.of_int (171)) (Prims.of_int (5)) (Prims.of_int (171)) (Prims.of_int (36))))) - (Obj.magic (Pulse_PP.pp Pulse_PP.uu___44 t)) + (Obj.magic (Pulse_PP.pp Pulse_PP.printable_term t)) (fun uu___1 -> FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -2163,7 +2164,8 @@ let (ill_typed_term : (Prims.of_int (11)) (Prims.of_int (173)) (Prims.of_int (51))))) - (Obj.magic (Pulse_PP.pp Pulse_PP.uu___44 ty)) + (Obj.magic + (Pulse_PP.pp Pulse_PP.printable_term ty)) (fun uu___ -> FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -2230,7 +2232,8 @@ let (ill_typed_term : (Prims.of_int (174)) (Prims.of_int (37))))) (Obj.magic - (Pulse_PP.pp Pulse_PP.uu___44 t)) + (Pulse_PP.pp + Pulse_PP.printable_term t)) (fun uu___1 -> FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -2305,7 +2308,8 @@ let (ill_typed_term : (Prims.of_int (11)) (Prims.of_int (176)) (Prims.of_int (51))))) - (Obj.magic (Pulse_PP.pp Pulse_PP.uu___44 ty)) + (Obj.magic + (Pulse_PP.pp Pulse_PP.printable_term ty)) (fun uu___ -> FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -2391,7 +2395,8 @@ let (ill_typed_term : (Prims.of_int (37))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 t)) + Pulse_PP.printable_term + t)) (fun uu___1 -> FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -2461,7 +2466,7 @@ let (ill_typed_term : (Prims.of_int (38))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term ty')) (fun uu___2 -> FStar_Tactics_Effect.lift_div_tac @@ -2743,7 +2748,7 @@ let (instantiate_term_implicits : (Prims.of_int (31))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term t0)) (fun uu___2 -> @@ -2838,7 +2843,7 @@ let (instantiate_term_implicits : (Prims.of_int (31))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term t0)) (fun uu___2 -> @@ -3213,7 +3218,7 @@ let (instantiate_term_implicits_uvs : (Prims.of_int (31))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term t0)) (fun uu___2 -> @@ -5602,7 +5607,8 @@ let (get_non_informative_witness : (Prims.of_int (529)) (Prims.of_int (18))))) (Obj.magic - (Pulse_PP.pp Pulse_PP.uu___44 t)) + (Pulse_PP.pp + Pulse_PP.printable_term t)) (fun uu___1 -> FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -5753,7 +5759,7 @@ let (check_prop_validity : (Prims.of_int (63))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term p)) (fun uu___3 -> FStar_Tactics_Effect.lift_div_tac @@ -6117,7 +6123,7 @@ let (check_subtyping : (Prims.of_int (46))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term t1)) (fun uu___3 -> @@ -6161,7 +6167,7 @@ let (check_subtyping : (Prims.of_int (46))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term t2)) (fun uu___4 -> diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Rewrite.ml b/src/ocaml/plugin/generated/Pulse_Checker_Rewrite.ml index 54218b8f0..6ba119df8 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Rewrite.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Rewrite.ml @@ -151,7 +151,7 @@ let (check_vprop_equiv_ext : (Prims.of_int (17))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term p)) (fun uu___2 -> @@ -195,7 +195,7 @@ let (check_vprop_equiv_ext : (Prims.of_int (17))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term q)) (fun uu___3 -> diff --git a/src/ocaml/plugin/generated/Pulse_Checker_WithInv.ml b/src/ocaml/plugin/generated/Pulse_Checker_WithInv.ml index 0fea22e79..e5e3da794 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_WithInv.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_WithInv.ml @@ -269,7 +269,7 @@ let (check_iname_disjoint : (Prims.of_int (95))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term inames)) (fun uu___2 -> @@ -342,7 +342,7 @@ let (check_iname_disjoint : (Prims.of_int (91))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term inv)) (fun uu___3 -> @@ -596,7 +596,7 @@ let (add_remove_inverse : (Prims.of_int (17))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term (add_iname inv_p (remove_iname @@ -656,7 +656,7 @@ let (add_remove_inverse : (Prims.of_int (65))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term inames)) (fun uu___2 -> @@ -854,7 +854,7 @@ let (check : (Prims.of_int (57))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 + Pulse_PP.printable_term p)) (fun uu___2 -> @@ -925,7 +925,7 @@ let (check : (Prims.of_int (58))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___53 + Pulse_PP.printable_post_hint_t q)) (fun uu___3 -> diff --git a/src/ocaml/plugin/generated/Pulse_PP.ml b/src/ocaml/plugin/generated/Pulse_PP.ml index 427fa5b4c..745572d5a 100644 --- a/src/ocaml/plugin/generated/Pulse_PP.ml +++ b/src/ocaml/plugin/generated/Pulse_PP.ml @@ -28,24 +28,25 @@ let from_show : 'a . 'a Pulse_Show.tac_showable -> 'a printable = FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (54)) - (Prims.of_int (34)) (Prims.of_int (54)) + (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (48)) + (Prims.of_int (34)) (Prims.of_int (48)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (54)) - (Prims.of_int (17)) (Prims.of_int (54)) + (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (48)) + (Prims.of_int (17)) (Prims.of_int (48)) (Prims.of_int (42))))) (Obj.magic (Pulse_Show.show d x)) (fun uu___ -> FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> FStar_Pprint.arbitrary_string uu___))) } -let (uu___19 : Prims.string printable) = from_show Pulse_Show.uu___12 -let (uu___20 : unit printable) = from_show Pulse_Show.uu___14 -let (uu___21 : Prims.bool printable) = from_show Pulse_Show.uu___16 -let (uu___22 : Prims.int printable) = from_show Pulse_Show.uu___18 -let (uu___23 : Pulse_Syntax_Base.ctag printable) = +let (printable_string : Prims.string printable) = + from_show Pulse_Show.uu___12 +let (printable_unit : unit printable) = from_show Pulse_Show.uu___14 +let (printable_bool : Prims.bool printable) = from_show Pulse_Show.uu___16 +let (printable_int : Prims.int printable) = from_show Pulse_Show.uu___18 +let (printable_ctag : Pulse_Syntax_Base.ctag printable) = from_show Pulse_Show.uu___28 let printable_option : 'a . 'a printable -> 'a FStar_Pervasives_Native.option printable = @@ -67,13 +68,13 @@ let printable_option : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (66)) (Prims.of_int (54)) - (Prims.of_int (66)) (Prims.of_int (58))))) + (Prims.of_int (60)) (Prims.of_int (54)) + (Prims.of_int (60)) (Prims.of_int (58))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (66)) (Prims.of_int (29)) - (Prims.of_int (66)) (Prims.of_int (58))))) + (Prims.of_int (60)) (Prims.of_int (29)) + (Prims.of_int (60)) (Prims.of_int (58))))) (Obj.magic (pp uu___ v)) (fun uu___2 -> FStar_Tactics_Effect.lift_div_tac @@ -109,13 +110,13 @@ let rec separate_map : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (75)) (Prims.of_int (13)) - (Prims.of_int (75)) (Prims.of_int (16))))) + (Prims.of_int (69)) (Prims.of_int (13)) + (Prims.of_int (69)) (Prims.of_int (16))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (75)) (Prims.of_int (13)) - (Prims.of_int (75)) (Prims.of_int (49))))) + (Prims.of_int (69)) (Prims.of_int (13)) + (Prims.of_int (69)) (Prims.of_int (49))))) (Obj.magic (f x)) (fun uu___ -> (fun uu___ -> @@ -125,17 +126,17 @@ let rec separate_map : (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (75)) + (Prims.of_int (69)) (Prims.of_int (20)) - (Prims.of_int (75)) + (Prims.of_int (69)) (Prims.of_int (49))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (75)) + (Prims.of_int (69)) (Prims.of_int (13)) - (Prims.of_int (75)) + (Prims.of_int (69)) (Prims.of_int (49))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -143,17 +144,17 @@ let rec separate_map : (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (75)) + (Prims.of_int (69)) (Prims.of_int (28)) - (Prims.of_int (75)) + (Prims.of_int (69)) (Prims.of_int (49))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (75)) + (Prims.of_int (69)) (Prims.of_int (20)) - (Prims.of_int (75)) + (Prims.of_int (69)) (Prims.of_int (49))))) (Obj.magic (separate_map sep f xs)) @@ -168,7 +169,7 @@ let rec separate_map : FStar_Pprint.op_Hat_Hat uu___ uu___1)))) uu___)))) uu___2 uu___1 uu___ -let showable_list : 'a . 'a printable -> 'a Prims.list printable = +let printable_list : 'a . 'a printable -> 'a Prims.list printable = fun uu___ -> { pp = @@ -176,26 +177,26 @@ let showable_list : 'a . 'a printable -> 'a Prims.list printable = FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (78)) - (Prims.of_int (26)) (Prims.of_int (78)) + (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (72)) + (Prims.of_int (26)) (Prims.of_int (72)) (Prims.of_int (51))))) (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (78)) - (Prims.of_int (17)) (Prims.of_int (78)) + (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (72)) + (Prims.of_int (17)) (Prims.of_int (72)) (Prims.of_int (51))))) (Obj.magic (separate_map FStar_Pprint.comma (pp uu___) l)) (fun uu___1 -> FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> FStar_Pprint.brackets uu___1))) } -let (uu___44 : Pulse_Syntax_Base.term printable) = +let (printable_term : Pulse_Syntax_Base.term printable) = from_show Pulse_Show.uu___30 -let (uu___45 : Pulse_Syntax_Base.universe printable) = +let (printable_universe : Pulse_Syntax_Base.universe printable) = from_show Pulse_Show.uu___31 -let (uu___46 : Pulse_Syntax_Base.comp printable) = +let (printable_comp : Pulse_Syntax_Base.comp printable) = from_show Pulse_Show.uu___33 -let (uu___47 : Pulse_Typing_Env.env printable) = +let (printable_env : Pulse_Typing_Env.env printable) = { pp = Pulse_Typing_Env.env_to_doc } let (pp_effect_annot : Pulse_Syntax_Base.effect_annot printable) = from_show Pulse_Show.uu___37 @@ -207,12 +208,12 @@ let (pp_record : FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (93)) - (Prims.of_int (4)) (Prims.of_int (93)) (Prims.of_int (104))))) + (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (87)) + (Prims.of_int (4)) (Prims.of_int (87)) (Prims.of_int (104))))) (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (95)) - (Prims.of_int (2)) (Prims.of_int (95)) (Prims.of_int (25))))) + (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (89)) + (Prims.of_int (2)) (Prims.of_int (89)) (Prims.of_int (25))))) (Obj.magic (separate_map (FStar_Pprint.doc_of_string ";") (fun uu___ -> @@ -231,46 +232,46 @@ let (pp_record : (fun flds_doc -> FStar_Tactics_Effect.lift_div_tac (fun uu___ -> FStar_Pprint.braces (FStar_Pprint.align flds_doc))) -let (uu___53 : Pulse_Typing.post_hint_t printable) = +let (printable_post_hint_t : Pulse_Typing.post_hint_t printable) = { pp = (fun h -> FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (99)) - (Prims.of_int (20)) (Prims.of_int (103)) + (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (93)) + (Prims.of_int (20)) (Prims.of_int (97)) (Prims.of_int (41))))) (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (99)) - (Prims.of_int (10)) (Prims.of_int (103)) + (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (93)) + (Prims.of_int (10)) (Prims.of_int (97)) (Prims.of_int (41))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) (Prims.of_int (22)) - (Prims.of_int (99)) (Prims.of_int (33))))) + (Prims.of_int (93)) (Prims.of_int (22)) + (Prims.of_int (93)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) (Prims.of_int (20)) - (Prims.of_int (103)) (Prims.of_int (41))))) + (Prims.of_int (93)) (Prims.of_int (20)) + (Prims.of_int (97)) (Prims.of_int (41))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) (Prims.of_int (27)) - (Prims.of_int (99)) (Prims.of_int (33))))) + (Prims.of_int (93)) (Prims.of_int (27)) + (Prims.of_int (93)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) (Prims.of_int (22)) - (Prims.of_int (99)) (Prims.of_int (33))))) - (Obj.magic (pp uu___47 h.Pulse_Typing.g)) + (Prims.of_int (93)) (Prims.of_int (22)) + (Prims.of_int (93)) (Prims.of_int (33))))) + (Obj.magic (pp printable_env h.Pulse_Typing.g)) (fun uu___ -> FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> ("g", uu___))))) @@ -281,28 +282,28 @@ let (uu___53 : Pulse_Typing.post_hint_t printable) = (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) (Prims.of_int (20)) - (Prims.of_int (103)) (Prims.of_int (41))))) + (Prims.of_int (93)) (Prims.of_int (20)) + (Prims.of_int (97)) (Prims.of_int (41))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) (Prims.of_int (20)) - (Prims.of_int (103)) (Prims.of_int (41))))) + (Prims.of_int (93)) (Prims.of_int (20)) + (Prims.of_int (97)) (Prims.of_int (41))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (100)) + (Prims.of_int (94)) (Prims.of_int (22)) - (Prims.of_int (100)) + (Prims.of_int (94)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) + (Prims.of_int (93)) (Prims.of_int (20)) - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (41))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -310,17 +311,17 @@ let (uu___53 : Pulse_Typing.post_hint_t printable) = (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (100)) + (Prims.of_int (94)) (Prims.of_int (38)) - (Prims.of_int (100)) + (Prims.of_int (94)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (100)) + (Prims.of_int (94)) (Prims.of_int (22)) - (Prims.of_int (100)) + (Prims.of_int (94)) (Prims.of_int (55))))) (Obj.magic (pp pp_effect_annot @@ -337,17 +338,17 @@ let (uu___53 : Pulse_Typing.post_hint_t printable) = (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) + (Prims.of_int (93)) (Prims.of_int (20)) - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (41))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) + (Prims.of_int (93)) (Prims.of_int (20)) - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (41))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -355,17 +356,17 @@ let (uu___53 : Pulse_Typing.post_hint_t printable) = (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (101)) + (Prims.of_int (95)) (Prims.of_int (22)) - (Prims.of_int (101)) + (Prims.of_int (95)) (Prims.of_int (43))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) + (Prims.of_int (93)) (Prims.of_int (20)) - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (41))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -373,20 +374,21 @@ let (uu___53 : Pulse_Typing.post_hint_t printable) = (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (101)) + (Prims.of_int (95)) (Prims.of_int (32)) - (Prims.of_int (101)) + (Prims.of_int (95)) (Prims.of_int (43))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (101)) + (Prims.of_int (95)) (Prims.of_int (22)) - (Prims.of_int (101)) + (Prims.of_int (95)) (Prims.of_int (43))))) (Obj.magic - (pp uu___44 + (pp + printable_term h.Pulse_Typing.ret_ty)) (fun uu___2 -> FStar_Tactics_Effect.lift_div_tac @@ -402,18 +404,18 @@ let (uu___53 : Pulse_Typing.post_hint_t printable) = ( FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) + (Prims.of_int (93)) (Prims.of_int (20)) - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (41))))) (FStar_Sealed.seal (Obj.magic ( FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) + (Prims.of_int (93)) (Prims.of_int (20)) - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (41))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -422,18 +424,18 @@ let (uu___53 : Pulse_Typing.post_hint_t printable) = (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (102)) + (Prims.of_int (96)) (Prims.of_int (22)) - (Prims.of_int (102)) + (Prims.of_int (96)) (Prims.of_int (33))))) ( FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) + (Prims.of_int (93)) (Prims.of_int (20)) - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (41))))) ( Obj.magic @@ -442,21 +444,21 @@ let (uu___53 : Pulse_Typing.post_hint_t printable) = (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (102)) + (Prims.of_int (96)) (Prims.of_int (27)) - (Prims.of_int (102)) + (Prims.of_int (96)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (102)) + (Prims.of_int (96)) (Prims.of_int (22)) - (Prims.of_int (102)) + (Prims.of_int (96)) (Prims.of_int (33))))) (Obj.magic (pp - uu___45 + printable_universe h.Pulse_Typing.u)) (fun uu___3 -> @@ -476,17 +478,17 @@ let (uu___53 : Pulse_Typing.post_hint_t printable) = (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) + (Prims.of_int (93)) (Prims.of_int (20)) - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (41))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) + (Prims.of_int (93)) (Prims.of_int (20)) - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (41))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -494,17 +496,17 @@ let (uu___53 : Pulse_Typing.post_hint_t printable) = (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (22)) - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (39))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (99)) + (Prims.of_int (93)) (Prims.of_int (20)) - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (41))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -512,21 +514,21 @@ let (uu___53 : Pulse_Typing.post_hint_t printable) = (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (30)) - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (39))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.PP.fst" - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (22)) - (Prims.of_int (103)) + (Prims.of_int (97)) (Prims.of_int (39))))) (Obj.magic (pp - uu___44 + printable_term h.Pulse_Typing.post)) (fun uu___4 -> @@ -572,16 +574,494 @@ let (printable_fstar_term : FStar_Reflection_Types.term printable) = FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (108)) - (Prims.of_int (31)) (Prims.of_int (108)) + (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (102)) + (Prims.of_int (31)) (Prims.of_int (102)) (Prims.of_int (60))))) (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (108)) - (Prims.of_int (17)) (Prims.of_int (108)) + (FStar_Range.mk_range "Pulse.PP.fst" (Prims.of_int (102)) + (Prims.of_int (17)) (Prims.of_int (102)) (Prims.of_int (60))))) (Obj.magic (FStar_Tactics_V2_Builtins.term_to_string t)) (fun uu___ -> FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> FStar_Pprint.doc_of_string uu___))) - } \ No newline at end of file + } +let printable_tuple2 : + 'a 'b . 'a printable -> 'b printable -> ('a * 'b) printable = + fun uu___ -> + fun uu___1 -> + { + pp = + (fun uu___2 -> + match uu___2 with + | (x, y) -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (107)) (Prims.of_int (31)) + (Prims.of_int (107)) (Prims.of_int (60))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (107)) (Prims.of_int (24)) + (Prims.of_int (107)) (Prims.of_int (60))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (107)) (Prims.of_int (47)) + (Prims.of_int (107)) (Prims.of_int (59))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (107)) (Prims.of_int (31)) + (Prims.of_int (107)) (Prims.of_int (60))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (107)) + (Prims.of_int (48)) + (Prims.of_int (107)) + (Prims.of_int (52))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (107)) + (Prims.of_int (47)) + (Prims.of_int (107)) + (Prims.of_int (59))))) + (Obj.magic (pp uu___ x)) + (fun uu___3 -> + (fun uu___3 -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (107)) + (Prims.of_int (47)) + (Prims.of_int (107)) + (Prims.of_int (59))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (107)) + (Prims.of_int (47)) + (Prims.of_int (107)) + (Prims.of_int (59))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (107)) + (Prims.of_int (54)) + (Prims.of_int (107)) + (Prims.of_int (58))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (107)) + (Prims.of_int (47)) + (Prims.of_int (107)) + (Prims.of_int (59))))) + (Obj.magic (pp uu___1 y)) + (fun uu___4 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___5 -> [uu___4])))) + (fun uu___4 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___5 -> uu___3 :: + uu___4)))) uu___3))) + (fun uu___3 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___4 -> + FStar_Pprint.separate FStar_Pprint.comma + uu___3)))) + (fun uu___3 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___4 -> FStar_Pprint.parens uu___3))) + } +let printable_tuple3 : + 'a 'b 'c . + 'a printable -> 'b printable -> 'c printable -> ('a * 'b * 'c) printable + = + fun uu___ -> + fun uu___1 -> + fun uu___2 -> + { + pp = + (fun uu___3 -> + match uu___3 with + | (x, y, z) -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (112)) (Prims.of_int (34)) + (Prims.of_int (112)) (Prims.of_int (69))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (112)) (Prims.of_int (27)) + (Prims.of_int (112)) (Prims.of_int (69))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (112)) (Prims.of_int (50)) + (Prims.of_int (112)) (Prims.of_int (68))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (112)) (Prims.of_int (34)) + (Prims.of_int (112)) (Prims.of_int (69))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (112)) + (Prims.of_int (51)) + (Prims.of_int (112)) + (Prims.of_int (55))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (112)) + (Prims.of_int (50)) + (Prims.of_int (112)) + (Prims.of_int (68))))) + (Obj.magic (pp uu___ x)) + (fun uu___4 -> + (fun uu___4 -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (112)) + (Prims.of_int (50)) + (Prims.of_int (112)) + (Prims.of_int (68))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (112)) + (Prims.of_int (50)) + (Prims.of_int (112)) + (Prims.of_int (68))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (112)) + (Prims.of_int (57)) + (Prims.of_int (112)) + (Prims.of_int (61))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (112)) + (Prims.of_int (50)) + (Prims.of_int (112)) + (Prims.of_int (68))))) + (Obj.magic (pp uu___1 y)) + (fun uu___5 -> + (fun uu___5 -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (112)) + (Prims.of_int (50)) + (Prims.of_int (112)) + (Prims.of_int (68))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (112)) + (Prims.of_int (50)) + (Prims.of_int (112)) + (Prims.of_int (68))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (112)) + (Prims.of_int (63)) + (Prims.of_int (112)) + (Prims.of_int (67))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (112)) + (Prims.of_int (50)) + (Prims.of_int (112)) + (Prims.of_int (68))))) + (Obj.magic + (pp + uu___2 z)) + (fun + uu___6 -> + FStar_Tactics_Effect.lift_div_tac + (fun + uu___7 -> + [uu___6])))) + (fun uu___6 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___7 + -> uu___5 + :: uu___6)))) + uu___5))) + (fun uu___5 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___6 -> uu___4 :: + uu___5)))) uu___4))) + (fun uu___4 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___5 -> + FStar_Pprint.separate FStar_Pprint.comma + uu___4)))) + (fun uu___4 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___5 -> FStar_Pprint.parens uu___4))) + } +let printable_tuple4 : + 'a 'b 'c 'd . + 'a printable -> + 'b printable -> + 'c printable -> 'd printable -> ('a * 'b * 'c * 'd) printable + = + fun uu___ -> + fun uu___1 -> + fun uu___2 -> + fun uu___3 -> + { + pp = + (fun uu___4 -> + match uu___4 with + | (x, y, z, w) -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (117)) (Prims.of_int (37)) + (Prims.of_int (117)) (Prims.of_int (78))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (117)) (Prims.of_int (30)) + (Prims.of_int (117)) (Prims.of_int (78))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (53)) + (Prims.of_int (117)) + (Prims.of_int (77))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (37)) + (Prims.of_int (117)) + (Prims.of_int (78))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (54)) + (Prims.of_int (117)) + (Prims.of_int (58))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (53)) + (Prims.of_int (117)) + (Prims.of_int (77))))) + (Obj.magic (pp uu___ x)) + (fun uu___5 -> + (fun uu___5 -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (53)) + (Prims.of_int (117)) + (Prims.of_int (77))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (53)) + (Prims.of_int (117)) + (Prims.of_int (77))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (60)) + (Prims.of_int (117)) + (Prims.of_int (64))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (53)) + (Prims.of_int (117)) + (Prims.of_int (77))))) + (Obj.magic (pp uu___1 y)) + (fun uu___6 -> + (fun uu___6 -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (53)) + (Prims.of_int (117)) + (Prims.of_int (77))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (53)) + (Prims.of_int (117)) + (Prims.of_int (77))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (66)) + (Prims.of_int (117)) + (Prims.of_int (70))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (53)) + (Prims.of_int (117)) + (Prims.of_int (77))))) + (Obj.magic + (pp + uu___2 z)) + (fun + uu___7 -> + (fun + uu___7 -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (53)) + (Prims.of_int (117)) + (Prims.of_int (77))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (53)) + (Prims.of_int (117)) + (Prims.of_int (77))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (72)) + (Prims.of_int (117)) + (Prims.of_int (76))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.PP.fst" + (Prims.of_int (117)) + (Prims.of_int (53)) + (Prims.of_int (117)) + (Prims.of_int (77))))) + (Obj.magic + (pp + uu___3 w)) + (fun + uu___8 -> + FStar_Tactics_Effect.lift_div_tac + (fun + uu___9 -> + [uu___8])))) + (fun + uu___8 -> + FStar_Tactics_Effect.lift_div_tac + (fun + uu___9 -> + uu___7 :: + uu___8)))) + uu___7))) + (fun uu___7 -> + FStar_Tactics_Effect.lift_div_tac + ( + fun + uu___8 -> + uu___6 :: + uu___7)))) + uu___6))) + (fun uu___6 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___7 -> uu___5 :: + uu___6)))) uu___5))) + (fun uu___5 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___6 -> + FStar_Pprint.separate FStar_Pprint.comma + uu___5)))) + (fun uu___5 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___6 -> FStar_Pprint.parens uu___5))) + } \ No newline at end of file diff --git a/src/ocaml/plugin/generated/Pulse_Typing_Combinators.ml b/src/ocaml/plugin/generated/Pulse_Typing_Combinators.ml index 3e561ce6c..1789c861c 100644 --- a/src/ocaml/plugin/generated/Pulse_Typing_Combinators.ml +++ b/src/ocaml/plugin/generated/Pulse_Typing_Combinators.ml @@ -370,7 +370,8 @@ let (lift_ghost_atomic : (Prims.of_int (18))))) (Obj.magic (Pulse_PP.pp - Pulse_PP.uu___44 t)) + Pulse_PP.printable_term + t)) (fun uu___ -> FStar_Tactics_Effect.lift_div_tac (fun uu___1 ->