Commit 92f6cec4 authored by Janno's avatar Janno

s/`[!APP] f $U x .. y =n>`/`[#] f | x .. y =U>`/g.

parent ffb1edea
......@@ -412,7 +412,7 @@ Program Definition wp_load : tactic :=
| [? l : loc] (Lit (LitLoc l)) =u>
(* We need to find the "real" context to be filled with `Load …` later *)
mmatch K as K return M (envs_entails _ (WP fill K _ @ _ ; _ {{ _ }}) *m _) with
| [!APP] cons LoadCtx $n K =n>
| [#] cons LoadCtx | K =n>
' v q i <- M.evar _;
TT.apply (tac_wp_load Δ Δ' s E i K l q v Φ)
<**> TT.apply_ (* IntoLaterEnvs *)
......
......@@ -75,31 +75,31 @@ Definition from_of_val : heap_lang.expr → M expr := fun e=>
Definition of_expr : heap_lang.expr M expr := (
mfix1 go (e : _) : M expr :=
mmatch e exhaustively_with
| [!APP] heap_lang.Var $n x =n> M.ret (Var x)
| [!APP] heap_lang.Rec $n f x e =n> e <- go e; M.ret (Rec f x e)
| [!APP] heap_lang.App $n e1 e2 =n> e1 <- go e1; e2 <- go e2; M.ret (App e1 e2)
| [!APP] heap_lang.Lit $n l =n> M.ret (Lit l)
| [!APP] heap_lang.UnOp $n op e =n> e <- go e; M.ret (UnOp op e)
| [!APP] heap_lang.BinOp $n op e1 e2 =n> e1 <- go e1; e2 <- go e2; M.ret (BinOp op e1 e2)
| [!APP] heap_lang.If $n e0 e1 e2 =n>
| [#] heap_lang.Var | x =n> M.ret (Var x)
| [#] heap_lang.Rec | f x e =n> e <- go e; M.ret (Rec f x e)
| [#] heap_lang.App | e1 e2 =n> e1 <- go e1; e2 <- go e2; M.ret (App e1 e2)
| [#] heap_lang.Lit | l =n> M.ret (Lit l)
| [#] heap_lang.UnOp | op e =n> e <- go e; M.ret (UnOp op e)
| [#] heap_lang.BinOp | op e1 e2 =n> e1 <- go e1; e2 <- go e2; M.ret (BinOp op e1 e2)
| [#] heap_lang.If | e0 e1 e2 =n>
e0 <- go e0; e1 <- go e1; e2 <- go e2; M.ret (If e0 e1 e2)
| [!APP] heap_lang.Pair $n e1 e2 =n> e1 <- go e1; e2 <- go e2; M.ret (Pair e1 e2)
| [!APP] heap_lang.Fst $n e =n> e <- go e; M.ret (Fst e)
| [!APP] heap_lang.Snd $n e =n> e <- go e; M.ret (Snd e)
| [!APP] heap_lang.InjL $n e =n> e <- go e; M.ret (InjL e)
| [!APP] heap_lang.InjR $n e =n> e <- go e; M.ret (InjR e)
| [!APP] heap_lang.Case $n e0 e1 e2 =n>
| [#] heap_lang.Pair | e1 e2 =n> e1 <- go e1; e2 <- go e2; M.ret (Pair e1 e2)
| [#] heap_lang.Fst | e =n> e <- go e; M.ret (Fst e)
| [#] heap_lang.Snd | e =n> e <- go e; M.ret (Snd e)
| [#] heap_lang.InjL | e =n> e <- go e; M.ret (InjL e)
| [#] heap_lang.InjR | e =n> e <- go e; M.ret (InjR e)
| [#] heap_lang.Case | e0 e1 e2 =n>
e0 <- go e0; e1 <- go e1; e2 <- go e2; M.ret (Case e0 e1 e2)
| [!APP] heap_lang.Fork $n e =n> e <- go e; M.ret (Fork e)
| [!APP] heap_lang.Alloc $n e =n> e <- go e; M.ret (Alloc e)
| [!APP] heap_lang.Load $n e =n> e <- go e; M.ret (Load e)
| [!APP] heap_lang.Store $n e1 e2 =n> e1 <- go e1; e2 <- go e2; M.ret (Store e1 e2)
| [!APP] heap_lang.CAS $n e0 e1 e2 =n>
| [#] heap_lang.Fork | e =n> e <- go e; M.ret (Fork e)
| [#] heap_lang.Alloc | e =n> e <- go e; M.ret (Alloc e)
| [#] heap_lang.Load | e =n> e <- go e; M.ret (Load e)
| [#] heap_lang.Store | e1 e2 =n> e1 <- go e1; e2 <- go e2; M.ret (Store e1 e2)
| [#] heap_lang.CAS | e0 e1 e2 =n>
e0 <- go e0; e1 <- go e1; e2 <- go e2; M.ret (CAS e0 e1 e2)
| [!APP] heap_lang.FAA $n e0 e1 =n>
| [#] heap_lang.FAA | e0 e1 =n>
e0 <- go e0; e1 <- go e1; M.ret (FAA e0 e1)
| [!APP] to_expr $n e =n> M.ret e
| [!APP] of_val $n v =n> M.ret (Val v (of_val v) (to_of_val v))
| [#] to_expr | e =n> M.ret e
| [#] of_val | v =n> M.ret (Val v (of_val v) (to_of_val v))
| _ =>
mtry
H <- M.select (Closed [] e); M.ret (@ClosedExpr e H)
......@@ -363,7 +363,7 @@ Definition simpl_subst : tactic :=
let helper :=
mfix4 helper (C : expr Type) x (er e : expr) : gtactic () :=
( mmatch e with
| [!APP] subst $n x' er' e' =n> helper (λ e, C (subst x er e)) x' er' e'
| [#] subst | x' er' e' =n> helper (λ e, C (subst x er e)) x' er' e'
end) || (
er' <- W.of_expr er;
e' <- W.of_expr e;
......@@ -420,7 +420,7 @@ Definition reshape_val_dep :
end
with StuckTerm =>
mmatch e as e' return M (B e') with
| [!APP] of_val $n v =n> tac v
| [#] of_val | v =n> tac v
| _ => M.raise ReshapeExprExc
end
end.
......@@ -438,7 +438,7 @@ Definition reshape_val : expr → M val :=
end
with StuckTerm =>
mmatch e return M val with
| [!APP] of_val $n v =n> M.ret v
| [#] of_val | v =n> M.ret v
| _ => M.raise ReshapeExprExc
end
end.
......
......@@ -138,7 +138,7 @@ Program Definition iStartProof (C : ∀ ig, TT.ttac (iPropOf ig)) : tactic :=
(match_goal with
| [[? (G : Prop) |- G ]] =>
mmatch G in Prop as G' return M (G' *m mlist goal) with
| [!APP] @envs_entails $n M Δ P =n> (C (IGoal M Δ P))
| [#] @envs_entails | M Δ P =n> (C (IGoal M Δ P))
| _ =>
`M P <- M.evar _;
TT.apply (@as_valid_2 G _ P)
......
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