Skip to content

Commit

Permalink
snap
Browse files Browse the repository at this point in the history
  • Loading branch information
@aseemr
aseemr committed Jul 28, 2023
1 parent 6f4bf36 commit b55e813
Show file tree
Hide file tree
Showing 15 changed files with 865 additions and 1,352 deletions.
4 changes: 2 additions & 2 deletions src/ocaml/plugin/PulseSyntaxWrapper.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -124,8 +124,8 @@ let tm_if (head:term) (returns_annot:vprop option) (then_:st_term) (else_:st_ter
let tm_match (sc:term) (returns_:vprop option) (brs:branch list) r : st_term =
PSB.(with_range (tm_match sc returns_ brs) r)

let tm_intro_exists (erased:bool) (p:vprop) (witnesses:term list) r : st_term =
PSB.(with_range (tm_intro_exists erased p witnesses) r)
let tm_intro_exists (p:vprop) (witnesses:term list) r : st_term =
PSB.(with_range (tm_intro_exists p witnesses) r)

let is_tm_intro_exists (s:st_term) : bool =
match s.term1 with
Expand Down
4 changes: 2 additions & 2 deletions src/ocaml/plugin/generated/PulseDesugar.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -853,8 +853,8 @@ let rec (desugar_stmt :
op_let_Question uu___2
(fun witnesses1 ->
let uu___3 =
PulseSyntaxWrapper.tm_intro_exists false vp
witnesses1 s.PulseSugar.range1 in
PulseSyntaxWrapper.tm_intro_exists vp witnesses1
s.PulseSugar.range1 in
return uu___3)))
| PulseSugar.Parallel
{ PulseSugar.p1 = p1; PulseSugar.p2 = p2; PulseSugar.q1 = q1;
Expand Down
495 changes: 253 additions & 242 deletions src/ocaml/plugin/generated/Pulse_Checker.ml
View file

Large diffs are not rendered by default.

629 changes: 106 additions & 523 deletions src/ocaml/plugin/generated/Pulse_Checker_Exists.ml
View file

Large diffs are not rendered by default.

233 changes: 115 additions & 118 deletions src/ocaml/plugin/generated/Pulse_Checker_Prover_IntroExists.ml
View file

Large diffs are not rendered by default.

695 changes: 372 additions & 323 deletions src/ocaml/plugin/generated/Pulse_Checker_Pure.ml
View file

Large diffs are not rendered by default.

10 changes: 0 additions & 10 deletions src/ocaml/plugin/generated/Pulse_Elaborate_Core.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -396,16 +396,6 @@ let rec (elab_st_typing :
Pulse_Reflection_Util.mk_intro_exists ru rt
(Pulse_Reflection_Util.mk_abs rt
FStar_Reflection_V2_Data.Q_Explicit rp) re
| Pulse_Typing.T_IntroExistsErased
(uu___, u, b, p, e, uu___1, uu___2, uu___3) ->
let ru = u in
let rt =
Pulse_Elaborate_Pure.elab_term b.Pulse_Syntax_Base.binder_ty in
let rp = Pulse_Elaborate_Pure.elab_term p in
let re = Pulse_Elaborate_Pure.elab_term e in
Pulse_Reflection_Util.mk_intro_exists_erased ru rt
(Pulse_Reflection_Util.mk_abs rt
FStar_Reflection_V2_Data.Q_Explicit rp) re
| Pulse_Typing.T_While
(uu___, inv, uu___1, uu___2, uu___3, cond_typing, body_typing)
->
Expand Down
6 changes: 2 additions & 4 deletions src/ocaml/plugin/generated/Pulse_Syntax_Base.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -268,7 +268,6 @@ and st_term'__Tm_ElimExists__payload = {
p1: vprop }
and st_term'__Tm_IntroExists__payload =
{
erased: Prims.bool ;
p2: vprop ;
witnesses: term Prims.list }
and st_term'__Tm_While__payload =
Expand Down Expand Up @@ -506,9 +505,8 @@ let rec (eq_st_term : st_term -> st_term -> Prims.bool) =
{ head2 = t21; body2 = k2;_}) ->
(eq_tm t11 t21) && (eq_st_term k1 k2)
| (Tm_IntroPure { p = p1;_}, Tm_IntroPure { p = p2;_}) -> eq_tm p1 p2
| (Tm_IntroExists { erased = b1; p2 = p1; witnesses = l1;_},
Tm_IntroExists { erased = b2; p2; witnesses = l2;_}) ->
((b1 = b2) && (eq_tm p1 p2)) && (eq_tm_list l1 l2)
| (Tm_IntroExists { p2 = p1; witnesses = l1;_}, Tm_IntroExists
{ p2; witnesses = l2;_}) -> (eq_tm p1 p2) && (eq_tm_list l1 l2)
| (Tm_ElimExists { p1;_}, Tm_ElimExists { p1 = p2;_}) -> eq_tm p1 p2
| (Tm_If { b1 = g1; then_ = ethen1; else_ = eelse1; post1 = p1;_},
Tm_If { b1 = g2; then_ = ethen2; else_ = eelse2; post1 = p2;_}) ->
Expand Down
18 changes: 6 additions & 12 deletions src/ocaml/plugin/generated/Pulse_Syntax_Builder.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -114,19 +114,13 @@ let (tm_match :
let (tm_elim_exists : Pulse_Syntax_Base.vprop -> Pulse_Syntax_Base.st_term')
= fun p -> Pulse_Syntax_Base.Tm_ElimExists { Pulse_Syntax_Base.p1 = p }
let (tm_intro_exists :
Prims.bool ->
Pulse_Syntax_Base.vprop ->
Pulse_Syntax_Base.term Prims.list -> Pulse_Syntax_Base.st_term')
Pulse_Syntax_Base.vprop ->
Pulse_Syntax_Base.term Prims.list -> Pulse_Syntax_Base.st_term')
=
fun erased ->
fun p ->
fun witnesses ->
Pulse_Syntax_Base.Tm_IntroExists
{
Pulse_Syntax_Base.erased = erased;
Pulse_Syntax_Base.p2 = p;
Pulse_Syntax_Base.witnesses = witnesses
}
fun p ->
fun witnesses ->
Pulse_Syntax_Base.Tm_IntroExists
{ Pulse_Syntax_Base.p2 = p; Pulse_Syntax_Base.witnesses = witnesses }
let (tm_while :
Pulse_Syntax_Base.term ->
Pulse_Syntax_Base.st_term ->
Expand Down
7 changes: 3 additions & 4 deletions src/ocaml/plugin/generated/Pulse_Syntax_Naming.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ let rec (freevars_st :
| Pulse_Syntax_Base.Tm_ElimExists { Pulse_Syntax_Base.p1 = p;_} ->
freevars p
| Pulse_Syntax_Base.Tm_IntroExists
{ Pulse_Syntax_Base.erased = uu___; Pulse_Syntax_Base.p2 = p;
{ Pulse_Syntax_Base.p2 = p;
Pulse_Syntax_Base.witnesses = witnesses;_}
-> FStar_Set.union (freevars p) (freevars_list witnesses)
| Pulse_Syntax_Base.Tm_While
Expand Down Expand Up @@ -248,7 +248,7 @@ let rec (ln_st' : Pulse_Syntax_Base.st_term -> Prims.int -> Prims.bool) =
| Pulse_Syntax_Base.Tm_ElimExists { Pulse_Syntax_Base.p1 = p;_} ->
ln' p i
| Pulse_Syntax_Base.Tm_IntroExists
{ Pulse_Syntax_Base.erased = uu___; Pulse_Syntax_Base.p2 = p;
{ Pulse_Syntax_Base.p2 = p;
Pulse_Syntax_Base.witnesses = witnesses;_}
-> (ln' p i) && (ln_list' witnesses i)
| Pulse_Syntax_Base.Tm_While
Expand Down Expand Up @@ -600,12 +600,11 @@ let rec (subst_st_term :
Pulse_Syntax_Base.Tm_ElimExists
{ Pulse_Syntax_Base.p1 = (subst_term p ss) }
| Pulse_Syntax_Base.Tm_IntroExists
{ Pulse_Syntax_Base.erased = erased; Pulse_Syntax_Base.p2 = p;
{ Pulse_Syntax_Base.p2 = p;
Pulse_Syntax_Base.witnesses = witnesses;_}
->
Pulse_Syntax_Base.Tm_IntroExists
{
Pulse_Syntax_Base.erased = erased;
Pulse_Syntax_Base.p2 = (subst_term p ss);
Pulse_Syntax_Base.witnesses = (subst_term_list witnesses ss)
}
Expand Down
91 changes: 1 addition & 90 deletions src/ocaml/plugin/generated/Pulse_Syntax_Printer.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1938,7 +1938,7 @@ let rec (st_term_to_string' :
(fun uu___1 ->
Prims.strcat "elim_exists " (Prims.strcat uu___ "")))
| Pulse_Syntax_Base.Tm_IntroExists
{ Pulse_Syntax_Base.erased = false; Pulse_Syntax_Base.p2 = p;
{ Pulse_Syntax_Base.p2 = p;
Pulse_Syntax_Base.witnesses = witnesses;_}
->
FStar_Tactics_Effect.tac_bind
Expand Down Expand Up @@ -2026,95 +2026,6 @@ let rec (st_term_to_string' :
(fun uu___1 ->
FStar_Tactics_Effect.lift_div_tac
(fun uu___2 -> uu___1 uu___)))) uu___)
| Pulse_Syntax_Base.Tm_IntroExists
{ Pulse_Syntax_Base.erased = true; Pulse_Syntax_Base.p2 = p;
Pulse_Syntax_Base.witnesses = witnesses;_}
->
FStar_Tactics_Effect.tac_bind
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range "Pulse.Syntax.Printer.fst"
(Prims.of_int (212)) (Prims.of_int (8))
(Prims.of_int (212)) (Prims.of_int (43)))))
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range "Pulse.Syntax.Printer.fst"
(Prims.of_int (208)) (Prims.of_int (6))
(Prims.of_int (212)) (Prims.of_int (43)))))
(Obj.magic (term_list_to_string " " witnesses))
(fun uu___ ->
(fun uu___ ->
Obj.magic
(FStar_Tactics_Effect.tac_bind
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range "Pulse.Syntax.Printer.fst"
(Prims.of_int (208)) (Prims.of_int (6))
(Prims.of_int (212)) (Prims.of_int (43)))))
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range "Pulse.Syntax.Printer.fst"
(Prims.of_int (208)) (Prims.of_int (6))
(Prims.of_int (212)) (Prims.of_int (43)))))
(Obj.magic
(FStar_Tactics_Effect.tac_bind
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
"Pulse.Syntax.Printer.fst"
(Prims.of_int (208)) (Prims.of_int (6))
(Prims.of_int (212))
(Prims.of_int (43)))))
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
"Pulse.Syntax.Printer.fst"
(Prims.of_int (208)) (Prims.of_int (6))
(Prims.of_int (212))
(Prims.of_int (43)))))
(Obj.magic
(FStar_Tactics_Effect.tac_bind
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
"Pulse.Syntax.Printer.fst"
(Prims.of_int (210))
(Prims.of_int (8))
(Prims.of_int (210))
(Prims.of_int (42)))))
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
"FStar.Printf.fst"
(Prims.of_int (121))
(Prims.of_int (8))
(Prims.of_int (123))
(Prims.of_int (44)))))
(Obj.magic
(term_to_string' (indent level) p))
(fun uu___1 ->
FStar_Tactics_Effect.lift_div_tac
(fun uu___2 ->
fun x ->
fun x1 ->
Prims.strcat
(Prims.strcat
(Prims.strcat
(Prims.strcat
"introduce (erased)\n"
(Prims.strcat
(indent level)
""))
(Prims.strcat uu___1
"\n"))
(Prims.strcat x "with "))
(Prims.strcat x1 "")))))
(fun uu___1 ->
FStar_Tactics_Effect.lift_div_tac
(fun uu___2 -> uu___1 level))))
(fun uu___1 ->
FStar_Tactics_Effect.lift_div_tac
(fun uu___2 -> uu___1 uu___)))) uu___)
| Pulse_Syntax_Base.Tm_While
{ Pulse_Syntax_Base.invariant = invariant;
Pulse_Syntax_Base.condition = condition;
Expand Down
6 changes: 1 addition & 5 deletions src/ocaml/plugin/generated/Pulse_Typing.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -714,6 +714,7 @@ let (comp_admit :
type ('g, 'e, 't) typing =
(unit, unit, unit) FStar_Reflection_Typing.tot_typing
type ('g, 'e, 't) tot_typing = unit
type ('g, 'e, 't) ghost_typing = unit
type ('g, 't, 'u) universe_of = unit
type ('g, 'u, 't) non_informative_t =
(Pulse_Syntax_Base.term, unit) Prims.dtuple2
Expand Down Expand Up @@ -869,9 +870,6 @@ type ('dummyV0, 'dummyV1, 'dummyV2) st_typing =
| T_IntroExists of Pulse_Typing_Env.env * Pulse_Syntax_Base.universe *
Pulse_Syntax_Base.binder * Pulse_Syntax_Base.term * Pulse_Syntax_Base.term
* unit * unit * unit
| T_IntroExistsErased of Pulse_Typing_Env.env * Pulse_Syntax_Base.universe
* Pulse_Syntax_Base.binder * Pulse_Syntax_Base.term *
Pulse_Syntax_Base.term * unit * unit * unit
| T_While of Pulse_Typing_Env.env * Pulse_Syntax_Base.term *
Pulse_Syntax_Base.st_term * Pulse_Syntax_Base.st_term * unit * (unit,
unit, unit) st_typing * (unit, unit, unit) st_typing
Expand Down Expand Up @@ -932,8 +930,6 @@ let uu___is_T_ElimExists uu___2 uu___1 uu___ uu___3 =
match uu___3 with | T_ElimExists _ -> true | _ -> false
let uu___is_T_IntroExists uu___2 uu___1 uu___ uu___3 =
match uu___3 with | T_IntroExists _ -> true | _ -> false
let uu___is_T_IntroExistsErased uu___2 uu___1 uu___ uu___3 =
match uu___3 with | T_IntroExistsErased _ -> true | _ -> false
let uu___is_T_While uu___2 uu___1 uu___ uu___3 =
match uu___3 with | T_While _ -> true | _ -> false
let uu___is_T_Par uu___2 uu___1 uu___ uu___3 =
Expand Down
15 changes: 0 additions & 15 deletions src/ocaml/plugin/generated/Pulse_Typing_Metatheory_Base.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -416,12 +416,6 @@ let rec (st_typing_weakening :
((Pulse_Typing_Env.push_env
(Pulse_Typing_Env.push_env g g1) g'), u, b, p, e, (),
(), ())
| Pulse_Typing.T_IntroExistsErased
(uu___, u, b, p, e, uu___1, uu___2, uu___3) ->
Pulse_Typing.T_IntroExistsErased
((Pulse_Typing_Env.push_env
(Pulse_Typing_Env.push_env g g1) g'), u, b, p, e, (),
(), ())
| Pulse_Typing.T_While
(uu___, inv, cond, body, uu___1, cond_typing, body_typing)
->
Expand Down Expand Up @@ -912,15 +906,6 @@ let rec (st_typing_subst :
(Pulse_Syntax_Naming.subst_term p ss),
(Pulse_Syntax_Naming.subst_term e2 ss), (), (),
())
| Pulse_Typing.T_IntroExistsErased
(uu___, u, b, p, e2, uu___1, uu___2, uu___3) ->
Pulse_Typing.T_IntroExistsErased
((Pulse_Typing_Env.push_env g
(Pulse_Typing_Env.subst_env g' (nt x e))), u,
(Pulse_Syntax_Naming.subst_binder b ss),
(Pulse_Syntax_Naming.subst_term p ss),
(Pulse_Syntax_Naming.subst_term e2 ss), (), (),
())
| Pulse_Typing.T_While
(uu___, inv, cond, body, uu___1, cond_typing,
body_typing)
Expand Down
2 changes: 1 addition & 1 deletion src/syntax_extension/PulseDesugar.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -402,7 +402,7 @@ let rec desugar_stmt (env:env_t) (s:Sugar.stmt)
| VPropExists _ ->
let? vp = desugar_vprop env vprop in
let? witnesses = map_err (desugar_term env) witnesses in
return (SW.tm_intro_exists false vp witnesses s.range)
return (SW.tm_intro_exists vp witnesses s.range)
)


Expand Down
2 changes: 1 addition & 1 deletion src/syntax_extension/PulseSyntaxWrapper.fsti
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ val tm_let_mut (x:binder) (v:term) (k:st_term) (_:range) : st_term
val tm_while (head:st_term) (invariant: (ident & vprop)) (body:st_term) (_:range) : st_term
val tm_if (head:term) (returns_annot:option vprop) (then_ else_:st_term) (_:range) : st_term
val tm_match (head:term) (returns_:option vprop) (brs:list branch) (_:range) : st_term
val tm_intro_exists (erased:bool) (vp:vprop) (witnesses:list term) (_:range) : st_term
val tm_intro_exists (vp:vprop) (witnesses:list term) (_:range) : st_term
val is_tm_intro_exists (x:st_term) : bool
val tm_protect (s:st_term) : st_term
val tm_par (p1:term) (p2:term) (q1:term) (q2:term) (b1:st_term) (b2:st_term) (_:range) : st_term
Expand Down

0 comments on commit b55e813

Please sign in to comment.