Commit 4db07a5e authored by Robbert Krebbers's avatar Robbert Krebbers

And another universe inconsistency, even with type-in-type...

parent 9c529e7e
......@@ -60,36 +60,36 @@ Fixpoint to_expr (e : expr) : heap_lang.expr :=
| CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
end.
Definition of_expr : heap_lang.expr M expr :=
mfix1 go (e : _) : M expr :=
Definition of_expr : heap_lang.expr gtactic expr :=
mfix1 go (e : _) : gtactic expr :=
mtry
match e with
| heap_lang.Var x => ret (Var x)
| heap_lang.Rec f x e => e <- go e; ret (Rec f x e)
| heap_lang.App e1 e2 => e1 <- go e1; e2 <- go e2; ret (App e1 e2)
| heap_lang.Lit l => ret (Lit l)
| heap_lang.UnOp op e => e <- go e; ret (UnOp op e)
| heap_lang.BinOp op e1 e2 => e1 <- go e1; e2 <- go e2; ret (BinOp op e1 e2)
| heap_lang.Var x => T.ret (Var x)
| heap_lang.Rec f x e => e <- go e; T.ret (Rec f x e)
| heap_lang.App e1 e2 => e1 <- go e1; e2 <- go e2; T.ret (App e1 e2)
| heap_lang.Lit l => T.ret (Lit l)
| heap_lang.UnOp op e => e <- go e; T.ret (UnOp op e)
| heap_lang.BinOp op e1 e2 => e1 <- go e1; e2 <- go e2; T.ret (BinOp op e1 e2)
| heap_lang.If e0 e1 e2 =>
e0 <- go e0; e1 <- go e1; e2 <- go e2; ret (If e0 e1 e2)
| heap_lang.Pair e1 e2 => e1 <- go e1; e2 <- go e2; ret (Pair e1 e2)
| heap_lang.Fst e => e <- go e; ret (Fst e)
| heap_lang.Snd e => e <- go e; ret (Snd e)
| heap_lang.InjL e => e <- go e; ret (InjL e)
| heap_lang.InjR e => e <- go e; ret (InjR e)
e0 <- go e0; e1 <- go e1; e2 <- go e2; T.ret (If e0 e1 e2)
| heap_lang.Pair e1 e2 => e1 <- go e1; e2 <- go e2; T.ret (Pair e1 e2)
| heap_lang.Fst e => e <- go e; T.ret (Fst e)
| heap_lang.Snd e => e <- go e; T.ret (Snd e)
| heap_lang.InjL e => e <- go e; T.ret (InjL e)
| heap_lang.InjR e => e <- go e; T.ret (InjR e)
| heap_lang.Case e0 e1 e2 =>
e0 <- go e0; e1 <- go e1; e2 <- go e2; ret (Case e0 e1 e2)
| heap_lang.Fork e => e <- go e; ret (Fork e)
| heap_lang.Alloc e => e <- go e; ret (Alloc e)
| heap_lang.Load e => e <- go e; ret (Load e)
| heap_lang.Store e1 e2 => e1 <- go e1; e2 <- go e2; ret (Store e1 e2)
e0 <- go e0; e1 <- go e1; e2 <- go e2; T.ret (Case e0 e1 e2)
| heap_lang.Fork e => e <- go e; T.ret (Fork e)
| heap_lang.Alloc e => e <- go e; T.ret (Alloc e)
| heap_lang.Load e => e <- go e; T.ret (Load e)
| heap_lang.Store e1 e2 => e1 <- go e1; e2 <- go e2; T.ret (Store e1 e2)
| heap_lang.CAS e0 e1 e2 =>
e0 <- go e0; e1 <- go e1; e2 <- go e2; ret (CAS e0 e1 e2)
e0 <- go e0; e1 <- go e1; e2 <- go e2; T.ret (CAS e0 e1 e2)
end
with StuckTerm =>
mmatch e return M expr with
| [? e] to_expr e => ret e
| [? v] of_val v => ret (Val v)
| [? e] to_expr e => T.ret e
| [? v] of_val v => T.ret (Val v)
(* TODO: In the Ltac code, I had this special case where I would look for a
proof of Closed [] e so I could reify it into a ClosedExpr. Since [of_expr] is
not a tactic, I cannot use [match_goal]... Not sure how to solve this in a nice
......@@ -101,7 +101,7 @@ monad. If we would only want to use the hypotheses, we probably can, but that
would still result in duplicating it, which is aweful. *)
(* | _ => constr:(ltac:(
match goal with H : Closed [] e |- _ => exact (@ClosedExpr e H) end)) *)
| _ => raise WrongTerm
| _ => T.raise WrongTerm
end
end.
......
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