Commit 1a95e749 authored by Janno's avatar Janno

Make use of `[#]` in `solve_…` heap_lang/tactics.

This saves another few billion instructions.

To avoid redundant `match_goal`s we use the new combinator
`TT.with_goal_prop`.
parent afdef913
......@@ -6,7 +6,7 @@ stages:
variables:
CPU_CORES: "10"
MTAC2_87_COMMIT: "45d249a111c506b2c9a3374a171217f06cacf7de"
MTAC2_88_COMMIT: "adc6b574bc9f1e10a4ae23d0e53da165949df1fc"
MTAC2_88_COMMIT: "ef46cb8b5f7ff013df20996f4fd3cbea2d0fbc19"
.template: &template
stage: build
......
......@@ -257,15 +257,16 @@ Qed.
End W.
Definition solve_closed : tactic :=
(match_goal with
| [[? X e |- Closed X e ]] =>
e' <- W.of_expr e;
TT.vm_change_dep (fun e => Closed X e) (W.to_expr e') (
TT.apply (W.is_closed_correct _ _)
<**> (TT.vm_compute
<**> TT.change True (TT.apply I))
)
end)%MC%TT.
(TT.with_goal_prop $ λ P,
mmatch P in Prop as P' return M (P' *m _) with
| [#] Closed | X e =n>
e' <- W.of_expr e;
TT.vm_change_dep (fun e => Closed X e) (W.to_expr e') (
TT.apply (W.is_closed_correct _ _)
<**> (TT.vm_compute
<**> TT.change True (TT.apply I))
)
end)%MC%TT.
Ltac solve_closed := mrun_static solve_closed.
(*
Ltac solve_closed :=
......@@ -280,8 +281,9 @@ Definition reflexivity {P} {A B : P} : TT.ttac (A = B) :=
(r <- M.coerce (eq_refl A); M.ret (m: r, [m:]))%MC.
Definition solve_into_val : tactic :=
(match_goal with
| [[? e v |- IntoVal e v ]] =>
(TT.with_goal_prop $ λ P,
mmatch P in Prop as P' return M (P' *m _) with
| [#] IntoVal | e v =n>
e' <- W.of_expr e;
TT.vm_change_dep (fun e => to_val e = Some v) (W.to_expr e') (
TT.apply (W.to_val_Some _ _)
......@@ -302,17 +304,20 @@ Ltac solve_into_val :=
Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
Definition solve_as_val : tactic :=
match_goal with
| [[? e |- AsVal e ]] =>
(TT.with_goal_prop $ λ P,
mmatch P in Prop as P' return M (P' *m _) with
| [#] AsVal | e =n>
e' <- W.of_expr e;
T.change (is_Some (to_val (W.to_expr e'))) &>
TT.vm_change_dep (fun e => is_Some (to_val e)) (W.to_expr e') (
(TT.apply (@W.to_val_is_Some e')
<**> (
dec <- M.solve_typeclass_or_fail _;
TT.apply (@bool_decide_unpack _ dec)
<**> TT.use (T.treduce RedVmCompute &> T.exact I)
) >>= TT.to_T)
end.
<**> (TT.vm_change_dep (fun P => P) True (TT.vm_compute <**> TT.apply I))
)
)
)
end)%MC%TT.
Ltac solve_as_val := mrun_static solve_as_val.
(*
Ltac solve_as_val :=
......@@ -325,14 +330,15 @@ Ltac solve_as_val :=
Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
Definition solve_atomic : tactic :=
match_goal with
| [[? s e |- Atomic s e ]] =>
(TT.with_goal_prop $ λ P,
mmatch P in Prop as P' return M (P' *m _) with
| [#] @Atomic heap_lang | s e =u>
e' <- W.of_expr e;
T.change (Atomic s (W.to_expr e')) &>
T.apply W.is_atomic_correct &>
T.treduce RedVmCompute &>
T.exact I
end.
TT.vm_change_dep (Atomic s) (W.to_expr e') (
TT.apply (W.is_atomic_correct _ _)
<**> (TT.vm_change_dep (fun P => P) True (TT.vm_compute <**> TT.apply I))
)
end)%MC%TT.
Ltac solve_atomic := mrun_static solve_atomic.
(*
Ltac solve_atomic :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment