Skip to content

Commit

Permalink
sync with main
Browse files Browse the repository at this point in the history
  • Loading branch information
@aseemr
aseemr committed Jul 12, 2023
1 parent 1c9c7de commit aa7a9fa
Show file tree
Hide file tree
Showing 10 changed files with 312 additions and 447 deletions.
2 changes: 1 addition & 1 deletion lib/steel/pulse/Pulse.Checker.Abs.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ let check_effect_annotation g r (c_annot c_computed:comp) =
(P.tag_of_comp c_computed))


#push-options "--z3rlimit_factor 2"
#push-options "--z3rlimit_factor 2 --fuel 0 --ifuel 1"
let check_abs
(g:env)
(t:st_term{Tm_Abs? t.term})
Expand Down
214 changes: 60 additions & 154 deletions src/ocaml/plugin/generated/Pulse_Checker_Bind.ml
View file

Large diffs are not rendered by default.

55 changes: 27 additions & 28 deletions src/ocaml/plugin/generated/Pulse_Prover.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,9 @@ let (unsolved_equiv_pst :
Pulse_Prover_Common.ss = (pst.Pulse_Prover_Common.ss);
Pulse_Prover_Common.solved = (pst.Pulse_Prover_Common.solved);
Pulse_Prover_Common.unsolved = unsolved';
Pulse_Prover_Common.solved_typing = ();
Pulse_Prover_Common.k = (pst.Pulse_Prover_Common.k);
Pulse_Prover_Common.goals_inv = ()
Pulse_Prover_Common.goals_inv = ();
Pulse_Prover_Common.solved_inv = ()
}
let (remaining_ctxt_equiv_pst :
Pulse_Prover_Common.preamble ->
Expand All @@ -40,7 +40,6 @@ let (remaining_ctxt_equiv_pst :
Pulse_Prover_Common.ss = (pst.Pulse_Prover_Common.ss);
Pulse_Prover_Common.solved = (pst.Pulse_Prover_Common.solved);
Pulse_Prover_Common.unsolved = (pst.Pulse_Prover_Common.unsolved);
Pulse_Prover_Common.solved_typing = ();
Pulse_Prover_Common.k =
(Pulse_Prover_Common.k_elab_equiv
preamble.Pulse_Prover_Common.g0
Expand Down Expand Up @@ -71,7 +70,8 @@ let (remaining_ctxt_equiv_pst :
pst.Pulse_Prover_Common.ss
pst.Pulse_Prover_Common.solved))
pst.Pulse_Prover_Common.k () ());
Pulse_Prover_Common.goals_inv = ()
Pulse_Prover_Common.goals_inv = ();
Pulse_Prover_Common.solved_inv = ()
}
let rec (collect_exists :
Pulse_Typing_Env.env ->
Expand Down Expand Up @@ -551,7 +551,7 @@ let (prove :
Pulse_Syntax_Base.vprop ->
unit ->
((Pulse_Typing_Env.env, Pulse_Typing_Env.env,
Pulse_Prover_Substs.ss_t, Pulse_Syntax_Base.vprop,
Pulse_Prover_Substs.nt_substs, Pulse_Syntax_Base.vprop,
(unit, unit, unit, unit)
Pulse_Prover_Common.continuation_elaborator)
FStar_Pervasives.dtuple5,
Expand All @@ -573,7 +573,7 @@ let (prove :
(Obj.magic
(FStar_Range.mk_range "Pulse.Prover.fst"
(Prims.of_int (127)) (Prims.of_int (70))
(Prims.of_int (164)) (Prims.of_int (103)))))
(Prims.of_int (162)) (Prims.of_int (100)))))
(FStar_Tactics_Effect.lift_div_tac (fun uu___ -> ()))
(fun uu___ ->
(fun ctxt_frame_typing ->
Expand All @@ -587,8 +587,8 @@ let (prove :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range "Pulse.Prover.fst"
(Prims.of_int (136)) (Prims.of_int (59))
(Prims.of_int (164)) (Prims.of_int (103)))))
(Prims.of_int (136)) (Prims.of_int (41))
(Prims.of_int (162)) (Prims.of_int (100)))))
(FStar_Tactics_Effect.lift_div_tac
(fun uu___ ->
{
Expand All @@ -610,15 +610,15 @@ let (prove :
(Prims.of_int (138))
(Prims.of_int (4))
(Prims.of_int (147))
(Prims.of_int (25)))))
(Prims.of_int (19)))))
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
"Pulse.Prover.fst"
(Prims.of_int (148))
(Prims.of_int (6))
(Prims.of_int (164))
(Prims.of_int (103)))))
(Prims.of_int (162))
(Prims.of_int (100)))))
(FStar_Tactics_Effect.lift_div_tac
(fun uu___ ->
{
Expand All @@ -637,8 +637,6 @@ let (prove :
Pulse_Prover_Common.unsolved =
(Pulse_Checker_VPropEquiv.vprop_as_list
goals);
Pulse_Prover_Common.solved_typing
= ();
Pulse_Prover_Common.k =
(Pulse_Prover_Common.k_elab_equiv
g g ctxt
Expand All @@ -658,7 +656,9 @@ let (prove :
(Pulse_Prover_Common.k_elab_unit
g ctxt) () ());
Pulse_Prover_Common.goals_inv =
()
();
Pulse_Prover_Common.solved_inv
= ()
}))
(fun uu___ ->
(fun pst ->
Expand All @@ -678,8 +678,8 @@ let (prove :
"Pulse.Prover.fst"
(Prims.of_int (149))
(Prims.of_int (25))
(Prims.of_int (164))
(Prims.of_int (103)))))
(Prims.of_int (162))
(Prims.of_int (100)))))
(Obj.magic
(prover preamble pst))
(fun uu___ ->
Expand All @@ -700,8 +700,8 @@ let (prove :
"Pulse.Prover.fst"
(Prims.of_int (151))
(Prims.of_int (2))
(Prims.of_int (164))
(Prims.of_int (103)))))
(Prims.of_int (162))
(Prims.of_int (100)))))
(Obj.magic
(Pulse_Prover_Substs.ss_to_nt_substs
pst1.Pulse_Prover_Common.pg
Expand All @@ -726,8 +726,8 @@ let (prove :
"Pulse.Prover.fst"
(Prims.of_int (151))
(Prims.of_int (65))
(Prims.of_int (164))
(Prims.of_int (103)))))
(Prims.of_int (162))
(Prims.of_int (100)))))
(if
FStar_Pervasives_Native.uu___is_None
ropt
Expand All @@ -754,11 +754,11 @@ let (prove :
with
|
FStar_Pervasives_Native.Some
nt ->
nts ->
FStar_Pervasives.Mkdtuple5
((pst1.Pulse_Prover_Common.pg),
(pst1.Pulse_Prover_Common.uvs),
(pst1.Pulse_Prover_Common.ss),
nts,
(Pulse_Checker_VPropEquiv.list_as_vprop
pst1.Pulse_Prover_Common.remaining_ctxt),
(Pulse_Prover_Common.k_elab_equiv
Expand All @@ -773,13 +773,12 @@ let (prove :
(Pulse_Checker_VPropEquiv.list_as_vprop
pst1.Pulse_Prover_Common.remaining_ctxt)
Pulse_Syntax_Base.tm_emp)
(Pulse_Prover_Common.op_Array_Access
pst1.Pulse_Prover_Common.ss
pst1.Pulse_Prover_Common.solved))
(Pulse_Prover_Substs.nt_subst_term
pst1.Pulse_Prover_Common.solved
nts))
(Pulse_Prover_Common.op_Star
(Pulse_Prover_Common.op_Array_Access
pst1.Pulse_Prover_Common.ss
goals)
(Pulse_Prover_Substs.nt_subst_term
goals nts)
(Pulse_Checker_VPropEquiv.list_as_vprop
pst1.Pulse_Prover_Common.remaining_ctxt))
pst1.Pulse_Prover_Common.k
Expand Down
59 changes: 14 additions & 45 deletions src/ocaml/plugin/generated/Pulse_Prover_Common.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1545,7 +1545,6 @@ let (op_Star :
Pulse_Syntax_Base.vprop ->
Pulse_Syntax_Base.vprop -> Pulse_Syntax_Base.term)
= Pulse_Syntax_Base.tm_star
type ('ss, 'uvs, 'g) well_typed_ss = unit
type 'preamble1 prover_state =
{
pg: Pulse_Typing_Env.env ;
Expand All @@ -1555,53 +1554,52 @@ type 'preamble1 prover_state =
ss: Pulse_Prover_Substs.ss_t ;
solved: Pulse_Syntax_Base.vprop ;
unsolved: Pulse_Syntax_Base.vprop Prims.list ;
solved_typing: unit ;
k: (unit, unit, unit, unit) continuation_elaborator ;
goals_inv: unit }
goals_inv: unit ;
solved_inv: unit }
let (__proj__Mkprover_state__item__pg :
preamble -> unit prover_state -> Pulse_Typing_Env.env) =
fun preamble1 ->
fun projectee ->
match projectee with
| { pg; remaining_ctxt; remaining_ctxt_frame_typing; uvs; ss; solved;
unsolved; solved_typing; k; goals_inv;_} -> pg
unsolved; k; goals_inv; solved_inv;_} -> pg
let (__proj__Mkprover_state__item__remaining_ctxt :
preamble -> unit prover_state -> Pulse_Syntax_Base.vprop Prims.list) =
fun preamble1 ->
fun projectee ->
match projectee with
| { pg; remaining_ctxt; remaining_ctxt_frame_typing; uvs; ss; solved;
unsolved; solved_typing; k; goals_inv;_} -> remaining_ctxt
unsolved; k; goals_inv; solved_inv;_} -> remaining_ctxt

let (__proj__Mkprover_state__item__uvs :
preamble -> unit prover_state -> Pulse_Typing_Env.env) =
fun preamble1 ->
fun projectee ->
match projectee with
| { pg; remaining_ctxt; remaining_ctxt_frame_typing; uvs; ss; solved;
unsolved; solved_typing; k; goals_inv;_} -> uvs
unsolved; k; goals_inv; solved_inv;_} -> uvs
let (__proj__Mkprover_state__item__ss :
preamble -> unit prover_state -> Pulse_Prover_Substs.ss_t) =
fun preamble1 ->
fun projectee ->
match projectee with
| { pg; remaining_ctxt; remaining_ctxt_frame_typing; uvs; ss; solved;
unsolved; solved_typing; k; goals_inv;_} -> ss
unsolved; k; goals_inv; solved_inv;_} -> ss
let (__proj__Mkprover_state__item__solved :
preamble -> unit prover_state -> Pulse_Syntax_Base.vprop) =
fun preamble1 ->
fun projectee ->
match projectee with
| { pg; remaining_ctxt; remaining_ctxt_frame_typing; uvs; ss; solved;
unsolved; solved_typing; k; goals_inv;_} -> solved
unsolved; k; goals_inv; solved_inv;_} -> solved
let (__proj__Mkprover_state__item__unsolved :
preamble -> unit prover_state -> Pulse_Syntax_Base.vprop Prims.list) =
fun preamble1 ->
fun projectee ->
match projectee with
| { pg; remaining_ctxt; remaining_ctxt_frame_typing; uvs; ss; solved;
unsolved; solved_typing; k; goals_inv;_} -> unsolved

unsolved; k; goals_inv; solved_inv;_} -> unsolved
let (__proj__Mkprover_state__item__k :
preamble ->
unit prover_state -> (unit, unit, unit, unit) continuation_elaborator)
Expand All @@ -1610,7 +1608,7 @@ let (__proj__Mkprover_state__item__k :
fun projectee ->
match projectee with
| { pg; remaining_ctxt; remaining_ctxt_frame_typing; uvs; ss; solved;
unsolved; solved_typing; k; goals_inv;_} -> k
unsolved; k; goals_inv; solved_inv;_} -> k
type ('preamble1, 'st) is_terminal = unit
let (extend_post_hint_opt_g :
Pulse_Typing_Env.env ->
Expand Down Expand Up @@ -1645,13 +1643,13 @@ let (st_typing_subst :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range "Pulse.Prover.Common.fsti"
(Prims.of_int (141)) (Prims.of_int (16))
(Prims.of_int (141)) (Prims.of_int (43)))))
(Prims.of_int (135)) (Prims.of_int (16))
(Prims.of_int (135)) (Prims.of_int (43)))))
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range "Pulse.Prover.Common.fsti"
(Prims.of_int (142)) (Prims.of_int (2))
(Prims.of_int (149)) (Prims.of_int (10)))))
(Prims.of_int (136)) (Prims.of_int (2))
(Prims.of_int (143)) (Prims.of_int (10)))))
(Obj.magic (Pulse_Prover_Substs.ss_to_nt_substs g uvs ss))
(fun nts_opt ->
FStar_Tactics_Effect.lift_div_tac
Expand Down Expand Up @@ -1695,33 +1693,4 @@ type ('preamble1, 'pst1, 'pst2) pst_extends = unit
type prover_t =
preamble ->
unit prover_state ->
(unit prover_state, unit) FStar_Tactics_Effect.tac_repr
let (prove :
Pulse_Typing_Env.env ->
Pulse_Syntax_Base.vprop ->
unit ->
Pulse_Typing_Env.env ->
Pulse_Syntax_Base.vprop ->
unit ->
((Pulse_Typing_Env.env, Pulse_Prover_Substs.ss_t,
Pulse_Syntax_Base.vprop,
(unit, unit, unit, unit) continuation_elaborator)
FStar_Pervasives.dtuple4,
unit) FStar_Tactics_Effect.tac_repr)
=
fun uu___5 ->
fun uu___4 ->
fun uu___3 ->
fun uu___2 ->
fun uu___1 ->
fun uu___ ->
(fun g ->
fun ctxt ->
fun ctxt_typing ->
fun uvs ->
fun goals ->
fun goals_typing ->
Obj.magic
(FStar_Tactics_Effect.lift_div_tac
(fun uu___ -> Prims.admit ()))) uu___5 uu___4
uu___3 uu___2 uu___1 uu___
(unit prover_state, unit) FStar_Tactics_Effect.tac_repr
6 changes: 3 additions & 3 deletions src/ocaml/plugin/generated/Pulse_Prover_ElimExists.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,7 @@ let (elim_exists_pst :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range "Pulse.Prover.ElimExists.fst"
(Prims.of_int (58)) (Prims.of_int (74)) (Prims.of_int (97))
(Prims.of_int (58)) (Prims.of_int (74)) (Prims.of_int (96))
(Prims.of_int (3)))))
(Obj.magic
(elim_exists_frame pst.Pulse_Prover_Common.pg
Expand All @@ -186,7 +186,6 @@ let (elim_exists_pst :
(pst.Pulse_Prover_Common.solved);
Pulse_Prover_Common.unsolved =
(pst.Pulse_Prover_Common.unsolved);
Pulse_Prover_Common.solved_typing = ();
Pulse_Prover_Common.k =
(Pulse_Prover_Common.k_elab_trans
preamble.Pulse_Prover_Common.g0
Expand Down Expand Up @@ -243,5 +242,6 @@ let (elim_exists_pst :
(Pulse_Prover_Common.op_Array_Access
pst.Pulse_Prover_Common.ss
pst.Pulse_Prover_Common.solved)) k () ()));
Pulse_Prover_Common.goals_inv = ()
Pulse_Prover_Common.goals_inv = ();
Pulse_Prover_Common.solved_inv = ()
}))
6 changes: 3 additions & 3 deletions src/ocaml/plugin/generated/Pulse_Prover_ElimPure.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -202,7 +202,7 @@ let (elim_pure_pst :
(Obj.magic
(FStar_Range.mk_range "Pulse.Prover.ElimPure.fst"
(Prims.of_int (114)) (Prims.of_int (74))
(Prims.of_int (153)) (Prims.of_int (3)))))
(Prims.of_int (152)) (Prims.of_int (3)))))
(Obj.magic
(elim_pure_frame pst.Pulse_Prover_Common.pg
(Pulse_Checker_VPropEquiv.list_as_vprop
Expand All @@ -228,7 +228,6 @@ let (elim_pure_pst :
(pst.Pulse_Prover_Common.solved);
Pulse_Prover_Common.unsolved =
(pst.Pulse_Prover_Common.unsolved);
Pulse_Prover_Common.solved_typing = ();
Pulse_Prover_Common.k =
(Pulse_Prover_Common.k_elab_trans
preamble.Pulse_Prover_Common.g0
Expand Down Expand Up @@ -285,5 +284,6 @@ let (elim_pure_pst :
(Pulse_Prover_Common.op_Array_Access
pst.Pulse_Prover_Common.ss
pst.Pulse_Prover_Common.solved)) k () ()));
Pulse_Prover_Common.goals_inv = ()
Pulse_Prover_Common.goals_inv = ();
Pulse_Prover_Common.solved_inv = ()
}))
Loading

0 comments on commit aa7a9fa

Please sign in to comment.