Skip to content
Snippets Groups Projects
Commit 3cc68b98 authored by Janno's avatar Janno
Browse files

WIP generating mmatches.

parent da36f624
Branches
Tags
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/heap_lang/tactics.v
+ 282
− 181
View file @ 3cc68b98
...@@ -60,33 +60,45 @@ Fixpoint to_expr (e : expr) : heap_lang.expr := ...@@ -60,33 +60,45 @@ Fixpoint to_expr (e : expr) : heap_lang.expr :=
| CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2) | CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
end. end.
Require Import Mtac2.DepDestruct. From Mtac2 Require Import DepDestruct.
Close Scope tactic_scope.
Module Datatypes_are_so_annoying. Module Datatypes_are_so_annoying.
Import Mtac2.Datatypes. Import Mtac2.Datatypes.
Import Mtac2.List. Import Mtac2.List.
Import ListNotations.
From Mtac2 Require Import MTeleMatch.
(* Wrapper for get_ind that takes care of computing CTeles. (* Wrapper for get_ind that takes care of computing CTeles.
Instead of list dyn, we get list (CTele it). Instead of list dyn, we get list (CTele it).
This should go into DepDestruct.v. It's a partial copy of new_destrut. This should go into DepDestruct.v. It's a partial copy of new_destrut.
*) *)
Definition get_ind_cts (A : Type) : M (nat * {s : Sort & { it : ITele s & list (CTele it)}}) := Fixpoint Mmap {A B} (f : A -> M B) (l : list A) : M (list B) :=
match l with
| [m:] => M.ret ([m:])
| [m: a & la] => b <- f a; lb <- Mmap f la; M.ret (cons b lb)
end.
Definition get_ind_cts (A : Type) (offset : nat) : M (nat * {s : Sorts.Sort & { it : ITele s & list (NDCTele it)}}) :=
ind <- get_ind A; ind <- get_ind A;
let (nsortit, constrs) := ind in let (nsortit, constrs) := ind in
let (nindx, sortit) := nsortit in (* drop first `offset` constructors. they might be dependent *)
let (isort, it) := sortit in let constrs := skipn offset constrs in
atele <- get_ind_atele it nindx A; let (nindx, sortit) := nsortit in
let (isort, it) := sortit in
atele <- get_ind_atele it nindx A;
(* Compute CTeles *) (* Compute CTeles *)
cts <- M.map (fun c_dyn : dyn => cts <- Mmap (fun c_dyn : dyn =>
let (dtype, delem) := c_dyn in let (dtype, delem) := c_dyn in
ty <- M.evar (stype_of isort); ty <- M.evar (Sorts.stype_of isort);
b <- M.unify_cumul ty dtype UniCoq; b <- M.unify_cumul ty dtype UniCoq;
if b then if b then
el <- M.evar (selem_of ty); el <- M.evar (Sorts.selem_of ty);
M.unify_cumul el delem UniCoq;; M.unify_cumul el delem UniCoq;;
get_CTele it nindx ty el get_NDCTele it nindx ty el
else else
M.failwith "Couldn't unify the type of the inductive with the type of the constructor" M.failwith "Couldn't unify the type of the inductive with the type of the constructor"
) constrs; ) constrs;
...@@ -96,18 +108,11 @@ Module Datatypes_are_so_annoying. ...@@ -96,18 +108,11 @@ Module Datatypes_are_so_annoying.
Fixpoint base_rt Fixpoint base_rt
T2 (ct : CTele _) : (@get_type_of_branch SType SProp (iBase T2) (fun (t : T2) => M T2) ct) := T2 (ct : CTele _) : (@branch_of_CTele Sorts.SType Sorts.SProp (iBase T2) (fun (t : T2) => M T2) ct) :=
(fix f (ct : @CTele _ (iBase T2)) : (fix f (ct : @CTele _ (iBase T2)) :
@get_type_of_branch SType SProp (iBase T2) (fun _ => M T2) ct := @branch_of_CTele Sorts.SType Sorts.SProp (iBase T2) (fun _ => M T2) ct :=
match ct as ct' in CTele _ return selem_of (@get_type_of_branch SType SProp (iBase T2) (fun _ => M T2) ct') with match ct as ct' in CTele _ return Sorts.selem_of (@branch_of_CTele Sorts.SType Sorts.SProp (iBase T2) (fun _ => M T2) ct') with
| cBase at1 x => | cBase at1 x => M.ret x
match at1 as a' in ATele (iBase T') return
forall (x : selem_of (ITele_App a')),
selem_of (@get_type_of_branch SType SProp (iBase T') (fun _ => M T') (cBase a' x))
with
| aBase T => fun x => M.ret x
end x
| cProd A ct => fun a : A => f (ct a) | cProd A ct => fun a : A => f (ct a)
end) ct. end) ct.
...@@ -125,139 +130,268 @@ Fixpoint base_rt ...@@ -125,139 +130,268 @@ Fixpoint base_rt
tmp_n <- recursor t1_n; tmp_n <- recursor t1_n;
base (Cs2_i tmp_1 tmp_n) base (Cs2_i tmp_1 tmp_n)
*) *)
Definition eq_fst {A B} {a1 a2 : A} {b1 b2 : B} : (a1,b1) = (a2,b2) -> a1 = a2.
by inversion 1.
Defined. (** [match_eq E P A] takes an equality of [T = S] and an element [A]
Definition eq_snd {A B} {a1 a2 : A} {b1 b2 : B} : (a1,b1) = (a2,b2) -> b1 = b2. of type [T], and returns [A] casted to [P S], but without any match
by inversion 1. (it reduces it). *)
Defined. Notation match_eq E P A :=
(redMatch match E in _ = R return P R with eq_refl => A end).
Definition gen_mmap_from_to (T1 T2 : Type) X (offset : nat) (recursor : T1 -> M T2) (base : T2 -> M X) : M X :=
i1 <- get_ind_cts T1; Notation "'match_eq_pair' E ( R1 , R2 => P ) XA" :=
i2 <- get_ind_cts T2; (match E in _ = (R1, R2) return P with eq_refl => XA end) (R1, R2 at level 100, E at next level, at level 0).
(* (match E in _ = (R1, R2) return P R1 R2 with eq_refl => A end). *)
Local Notation lprod l := (fold_right (fun T b => T * b)%type unit l).
Definition Mnu {A B} (f : A -> M B) (s : string) : M B := (M.nu s None f).
Local Notation "\fnu x .. y , t" :=
(M.fresh_name "fnu_var" >>=
(Mnu
(fun x =>
..
(M.fresh_name "fnu_var" >>= Mnu (fun y => t))
..
)
)
)
(at level 81, x binder, y binder, right associativity) : M_scope.
Local Notation "'\sfnu' s 'for' x .. y , t" :=
(
(M.fresh_name s) >>=
(Mnu (fun x => ..
((M.fresh_name s) >>=
(Mnu (fun y =>
t
)
))
..
)
)
) (at level 82, x binder, y binder).
Definition gen_mmap_from_to (T1 T2 : Type) X (offset : nat) : M (forall recursor : T1 -> M T2, forall base : T2 -> M X, Unification -> T1 -> M X) :=
i1 <- get_ind_cts T1 O;
i2 <- get_ind_cts T2 offset;
mmatch (i1, i2) with mmatch (i1, i2) with
| [?(n1 : nat) (Cs1 : list (CTele (@iBase SType T1))) | [?(n1 : nat) (Cs1 : list (NDCTele (@iBase Sorts.SType T1)))
(n2 : nat) (Cs2 : list (CTele (@iBase SType T2)))] (n2 : nat) (Cs2 : list (NDCTele (@iBase Sorts.SType T2)))]
(((n1, existT SType (existT (@iBase SType T1) Cs1))), ((n2, existT SType (existT (@iBase SType T2) Cs2)))) => (
let it1 := @iBase SType T1 in ((n1, existT Sorts.SType (existT (@iBase Sorts.SType T1) Cs1))),
let it2 := @iBase SType T2 in ((n2, existT Sorts.SType (existT (@iBase Sorts.SType T2) Cs2)))
(* Compute functions to convert betweent T1 and it1 and T2 and it2, respectively *) ) =>
(* let from1 := (fun (at1 : ATele it1) (t1 : selem_of (ITele_App at1)) => *) let it1 := @iBase Sorts.SType T1 in
(* conv <- M.unify_univ (selem_of (ITele_App at1)) T1 UniCoq; *) let it2 := @iBase Sorts.SType T2 in
(* match conv with *) (if Nat.eqb (length Cs1) (length Cs2) then M.ret () else M.failwith "Number of remaining constructors of T2 does not match that of T1");;
(* | Some conv => let r := reduce (RedStrong RedAll) (conv t1) in M.ret r *) let Cs1 := reduce RedVmCompute Cs1 in
(* | None => M.raise exception *) let Cs2 := reduce RedVmCompute Cs2 in
(* end *)
(* ) in *)
(* let from2 := (fun (at2 : ATele it2) (t2 : selem_of (ITele_App at2)) => *)
(* conv <- M.unify_univ (selem_of (ITele_App at2)) T2 UniCoq; *)
(* match conv with *)
(* | Some conv => let r := reduce (RedStrong RedAll) (conv t2) in M.ret r *)
(* | None => M.raise exception *)
(* end *)
(* ) in *)
(* drop `offset` many items from Cs2 *)
let Cs2 := skipn offset Cs2 in
(if Nat.eqb (length Cs1) (length Cs2) then M.ret () else M.raise exception);;
let zipped := combine Cs1 Cs2 in let zipped := combine Cs1 Cs2 in
M.print_term (it1, it2);; \sfnu "recursor" for recursor : T1 -> M T2,
(* create RTele for our match. Return type is T2, which will be fed to base *) \sfnu "base" for base : T2 -> M X,
let rt : RTele SProp it2 := (fun _ => M T2) in \sfnu "U" for U : Unification,
(* make up a discriminant for the mmatch *) \sfnu "t1" for t1 : T1,
M.nu "discr" None (fun (t1 : T1) => (* Construct MTele *)
pats <- M.map let m := (fun Css =>
(fun Csi => let (Cs1_i, Cs2_i) := Csi : (CTele it1) * CTele (it2) in mTele (fun _ : (fold_right (fun T b => T * b)%type unit (Css.2) -> M X)
M.print_term Cs1_i;; => mBase (pattern M.t T1 (fun _ => X) t1))
M.print_term Cs2_i;; ) in
(mfix3 f (Cs1_i : CTele it1) (Cs2_i : CTele it2) (term_to_build : M (get_type_of_branch rt Cs2_i)) : M (pattern M.t T1 (fun _ => T2) t1) := pats <- Mmap
let stupid_name := (Cs1_i, Cs2_i) in (fun Csi =>
mmatch stupid_name return M (pattern M.t T1 (fun _ => T2) t1) with let (Cs1_i, Cs2_i) := Csi : (NDCTele it1) * NDCTele (it2) in
| [?(at1 : ATele it1) c1 at2 c2] (cBase at1 c1, cBase at2 c2) => [H] (* M.print_term (Cs1_i, Cs2_i);; *)
(* Base case *) let c21 := reduce (RedVmCompute) (projT1 Cs2_i) in
let ttb := match eq_snd H in _ = x return let c2 := reduce (RedVmCompute) (projT2 Cs2_i) in
M (get_type_of_branch rt Cs2_i) -> M (get_type_of_branch rt x) with (mfix3 f (Cs1_i : NDCTele it1) (Cs2_i : list Type) (Cs2_iF : lprod Cs2_i -> M X ) : M (pattern M.t T1 (fun _ => X) t1) :=
| eq_refl => id (* M.print "mfix top";; *)
end term_to_build in (MTeleMatch.mtmmatch' _ m
match at1 as at1' in @ATele _ (@iBase _ T') return (Cs1_i, Cs2_i)
selem_of (ITele_App at1') -> (with
forall (t1 : selem_of T'), | [? at1 c1]
M (pattern M.t T' (fun _ => T2) t1) mtpbase (m := fun x => MTele_ty M (m x))
with (existT nil (fun _ => existT at1 c1), nil)
| aBase c1 => fun c1 t1 => (fun F =>
M.ret (@pbase M _ (fun _ => T2) (c1) t1 (fun _ => x <- ttb; x) UniMatchNoRed) (* let c1 := reduce (RedVM) c1 in *)
end c1 t1 let c2 := reduce (RedVmCompute) (F tt) in
| [?(A : Type) (F1 : A -> CTele it1) (F2 : A -> CTele it2) M.ret (pbase c1 (fun _ => c2) U))
] (cProd F1, cProd F2) => [H] UniCoq
(* Shared non-recursive argument. Apply to both sides unchanged, recurse. *)
let ttb := match eq_snd H in _ = x return | [?(A : Type) l1' l2'
M (get_type_of_branch rt Cs2_i) -> M (get_type_of_branch rt x) with (F1 : NDCfold it1 (A::l1'))
| eq_refl => id ]
end term_to_build in mtpbase (m := fun x => MTele_ty M (m x))
M.nu "A" (None) (fun a : A => (existT (A::l1') F1, A::l2')
pat <- f (F1 a) (F2 a) (x <- ttb; M.ret (x a)); (fun F : (lprod (A::l2') -> M X) =>
g <- M.abs_fun a pat; (* M.print "shared non-recursive argument";; *)
M.ret (@ptele M.t _ _ _ _ g) b <- M.fresh_binder_name F1;
) M.nu b None (fun a : A =>
(* M.raise exception *) (* _ <- M.print "recurring"; *)
| [?(F1 : CTele it1) (F2 : CTele it2) (* _ <- M.print_term F; *)
] (cProd (fun (_ : T1) => F1), cProd (fun (_ : T2) => F2)) => [H] pat <- f (existT l1' (fun x=> F1 (a,x))) l2' (fun lp => F (a,lp));
(* Shared recursive argument. Insert one bind before `base`. (* _ <- M.print "after recurrence"; *)
The type of the constructors MUST NOT depend on these arguments. (* M.print "simplified pat:";; *)
*) (* M.print_term spat;; *)
let ttb := match eq_snd H in _ = x return g <- M.abs_fun (P:=fun _ => _) a pat;
M (get_type_of_branch rt Cs2_i) -> M (get_type_of_branch rt x) with (* M.print ("binder "++b);; *)
| eq_refl => id (* M.print "abstracted pat:";; *)
end term_to_build in M.ret (ptele g)
M.nu "A" (None) )
(fun a : T1 => )
pat <- f F1 F2 (tmp <- recursor a; x <- ttb; M.ret (x tmp)); UniCoq
g <- M.abs_fun a pat; (* M.ret (@ptele M.t _ _ _ _ g) *)
M.ret (ptele g) | [?l1' l2' F1
) ]
mtpbase (m := fun x => MTele_ty M (m x))
| _ => (* non-shared argument - not translatable. Fail *) (existT (T1::l1') F1, T2::l2')
M.raise ArgumentNotTranslatable (fun F =>
end) Cs1_i Cs2_i (M.ret (base_rt T2 Cs2_i)) (* M.print "shared recursive argument";; *)
) b <- M.fresh_binder_name F1;
(zipped); M.nu b None (fun a : T1 =>
M.abs_fun t1 pats pat <- f (existT l1' (fun x=> F1 (a,x))) l2'
);; (fun lp =>
M.raise exception b <- recursor a;
end F(b,lp));
(* M.print "simplified pat:";; *)
(* M.print_term spat;; *)
g <- M.abs_fun (P:=fun _ => _) a pat;
(* M.print ("binder "++b);; *)
(* M.print "abstracted pat:";; *)
(* M.print_term g;; *)
M.ret (ptele g)
)
)
UniCoq
(* M.raise ArgumentNotTranslatable *)
| [? _unused] _unused =m> (* non-shared argument - not translatable. Fail *)
fun _ => M.raise ArgumentNotTranslatable
end))%with_mtpattern Cs2_iF)
Cs1_i
c21
(fun x => let '(existT _ y) := c2 x in base y)
)
(zipped);
(* M.print_term pats;; *)
pats' <- M.abs_fun (P:=fun t1 => list (pattern M T1 (fun _ : T1 => X) t1)) t1 pats;
pats' <- M.abs_fun U pats';
pats' <- M.abs_fun base pats';
pats' <- M.abs_fun recursor pats';
M.ret (fun rec base U (t1 : T1) => M.mmatch' t1 (pats' rec base U t1))
end
. .
Definition bla : M ().
MProof. Set Printing Depth 1000.
(
x <- (mfix1 f (t1 : heap_lang.expr) : M expr := (* Set Printing Depth 100000. *)
@gen_mmap_from_to heap_lang.expr expr expr 2 f M.ret) (heap_lang.Var "bla"); (* Set Printing All. *)
M.ret ()
). Require Import Mtac2.Debugger.
end.
(* Let x : CTele (@iBase SType (heap_lang.expr)) := @cProd SType (@iBase SType (heap_lang.expr)) _ *)
(* (λ b : binder, *)
(* cProd (λ b_ : binder, cProd (λ b__ : heap_lang.expr, @cBase SType (@iBase SType _) () (heap_lang.Rec b b_ b__)))). *)
(* Let y := cProd (λ b : binder, cProd (λ b_ : binder, cProd (λ b__ : expr, @cBase SType (@iBase SType _) () (Rec b b_ b__)))). *)
(* Definition bla : M (). *)
(* MProof. *)
(* (* (* (x <- mmatch (x,y) with *) *) *)
(* (* (* | [?(A : Type) (F1 : A -> CTele _) (F2 : A -> CTele _)] *) *) *)
(* (* (* (cProd F1, cProd F2) => M.print "bla" *) *) *)
(* (* (* end; *) *) *)
(* (* (* M.raise exception *) *) *)
(* (* (* )%MC. *) *) *)
(* Time ( *)
(* let F := (mfix1 f (t1 : heap_lang.expr) : M expr := *)
(* g <- (@gen_mmap_from_to heap_lang.expr expr expr 2); *)
(* g f M.ret UniMatchNoRed t1 *)
(* ) in *)
(* t <- F (heap_lang.Var "blubb"); *)
(* M.print_term t;; *)
(* M.ret _ *)
(* )%MC. *)
(* Admitted. *)
End Datatypes_are_so_annoying. End Datatypes_are_so_annoying.
Definition blubb (it : Datatypes.prod nat ({s : Sort & ITele s})) : Import Datatypes_are_so_annoying.
M match it with Require Mtac2.List.
| Datatypes.pair _ (existT x it) => _ Import Mtac2.List.ListNotations.
end
:= (match it as p' return Require Import Mtac2.Debugger.
M match p' with Time Definition hl_expr_to_expr {X} : (heap_lang.expr → M expr) → (expr → M X) → Unification → heap_lang.expr → M X :=
| Datatypes.pair num (existT _ it') => fun f b U => ltac:(mrun((gen_mmap_from_to heap_lang.expr expr X 2))) f b U.
(Datatypes.list (CTele it'))
end Open Scope tactic_scope.
with
| Datatypes.pair _ (existT SProp _) => M.raise exception Definition mhead {A} := (fun (l : Datatypes.list A) => mmatch l with | [? (x : A) l] ([m: x & l]) =u> M.ret x end)%MC.
| Datatypes.pair _ (existT SType it) =>
(c <- M.constrs heap_lang.expr; Program Definition of_expr' : heap_lang.expr → gtactic expr :=
let (_, constrs) := c in mfix1 go (e : _) : gtactic (expr) :=
cs <- M.map (fun c_dyn => get_CTele it 0 _ (elem (c_dyn))) (constrs); mmatch e return gtactic expr with
M.ret cs) | [? e] to_expr e => T.ret e
end)%MC. | [? v] of_val v => T.ret (Val v)
| _ =>
Definition tmp : (). fun g =>
MProof. (mtry
Time (p <- bla; x <- blubb p; M.print_term x;; M.ret ())%MC. (T.select (Closed [] e) (fun H=>T.ret (@ClosedExpr e H))) g
with NoPatternMatchesGoal =>
e' <- hl_expr_to_expr (X := expr)
(fun t1 => go t1 g >>= mhead >>= (fun x => M.ret (fst x)) >>= M.ret)%MC (M.ret) UniMatchNoRed e;
M.ret [m:(e',g)]
end )%MC
end%tactic.
Ltac of_expr e :=
lazymatch e with
| heap_lang.Var ?x => constr:(Var x)
| heap_lang.Rec ?f ?x ?e => let e := of_expr e in constr:(Rec f x e)
| heap_lang.App ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(App e1 e2)
| heap_lang.Lit ?l => constr:(Lit l)
| heap_lang.UnOp ?op ?e => let e := of_expr e in constr:(UnOp op e)
| heap_lang.BinOp ?op ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op e1 e2)
| heap_lang.If ?e0 ?e1 ?e2 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(If e0 e1 e2)
| heap_lang.Pair ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Pair e1 e2)
| heap_lang.Fst ?e => let e := of_expr e in constr:(Fst e)
| heap_lang.Snd ?e => let e := of_expr e in constr:(Snd e)
| heap_lang.InjL ?e => let e := of_expr e in constr:(InjL e)
| heap_lang.InjR ?e => let e := of_expr e in constr:(InjR e)
| heap_lang.Case ?e0 ?e1 ?e2 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(Case e0 e1 e2)
| heap_lang.Fork ?e => let e := of_expr e in constr:(Fork e)
| heap_lang.Alloc ?e => let e := of_expr e in constr:(Alloc e)
| heap_lang.Load ?e => let e := of_expr e in constr:(Load e)
| heap_lang.Store ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Store e1 e2)
| heap_lang.CAS ?e0 ?e1 ?e2 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(CAS e0 e1 e2)
| to_expr ?e => e
| of_val ?v => constr:(Val v)
| _ => match goal with H : Closed [] e |- _ => constr:(@ClosedExpr e H) end
end.
Goal forall e, Closed [] e -> unit.
Proof.
intros.
pose er := ltac:(let er := eval vm_compute in (Nat.iter 10 (fun x => heap_lang.App x e) e) in exact er).
Time Compute ltac:(let x := (eval unfold er in (of_expr' er (Goal unit))) in mrun(x >>= mhead)%MC).
Time Compute ltac:(let x := (eval unfold er in er) in let e := of_expr x in exact e).
clear er.
pose er := ltac:(let er := eval vm_compute in (Nat.iter 100 (fun x => heap_lang.App x e) e) in exact er).
Time Compute ltac:(let x := (eval unfold er in (of_expr' er (Goal unit))) in mrun(x >>= mhead)%MC).
Time Compute ltac:(let x := (eval unfold er in er) in let e := of_expr x in exact e).
clear er.
(* pose er := ltac:(let er := eval vm_compute in (Nat.iter 200 (fun x => heap_lang.App x e) e) in exact er). *)
(* Time Compute ltac:(let x := (eval unfold er in (of_expr' er (Goal unit))) in mrun(x >>= mhead)%MC). *)
(* Time Compute ltac:(let x := (eval unfold er in er) in let e := of_expr x in exact e). *)
Admitted.
Definition of_expr : heap_lang.expr → gtactic expr := Definition of_expr : heap_lang.expr → gtactic expr :=
mfix1 go (e : _) : gtactic expr := mfix1 go (e : _) : gtactic expr :=
...@@ -293,39 +427,6 @@ Definition of_expr : heap_lang.expr → gtactic expr := ...@@ -293,39 +427,6 @@ Definition of_expr : heap_lang.expr → gtactic expr :=
end end
end. end.
(* lazymatch e with *)
(* | heap_lang.Var ?x => constr:(Var x) *)
(* | heap_lang.Rec ?f ?x ?e => let e := of_expr e in constr:(Rec f x e) *)
(* | heap_lang.App ?e1 ?e2 => *)
(* let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(App e1 e2) *)
(* | heap_lang.Lit ?l => constr:(Lit l) *)
(* | heap_lang.UnOp ?op ?e => let e := of_expr e in constr:(UnOp op e) *)
(* | heap_lang.BinOp ?op ?e1 ?e2 => *)
(* let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op e1 e2) *)
(* | heap_lang.If ?e0 ?e1 ?e2 => *)
(* let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in *)
(* constr:(If e0 e1 e2) *)
(* | heap_lang.Pair ?e1 ?e2 => *)
(* let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Pair e1 e2) *)
(* | heap_lang.Fst ?e => let e := of_expr e in constr:(Fst e) *)
(* | heap_lang.Snd ?e => let e := of_expr e in constr:(Snd e) *)
(* | heap_lang.InjL ?e => let e := of_expr e in constr:(InjL e) *)
(* | heap_lang.InjR ?e => let e := of_expr e in constr:(InjR e) *)
(* | heap_lang.Case ?e0 ?e1 ?e2 => *)
(* let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in *)
(* constr:(Case e0 e1 e2) *)
(* | heap_lang.Fork ?e => let e := of_expr e in constr:(Fork e) *)
(* | heap_lang.Alloc ?e => let e := of_expr e in constr:(Alloc e) *)
(* | heap_lang.Load ?e => let e := of_expr e in constr:(Load e) *)
(* | heap_lang.Store ?e1 ?e2 => *)
(* let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Store e1 e2) *)
(* | heap_lang.CAS ?e0 ?e1 ?e2 => *)
(* let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in *)
(* constr:(CAS e0 e1 e2) *)
(* | to_expr ?e => e *)
(* | of_val ?v => constr:(Val v) *)
(* | _ => match goal with H : Closed [] e |- _ => constr:(@ClosedExpr e H) end *)
(* end. *)
Fixpoint is_closed (X : list string) (e : expr) : bool := Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with match e with
...@@ -471,7 +572,7 @@ Ltac solve_to_val := ...@@ -471,7 +572,7 @@ Ltac solve_to_val :=
apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
end. end.
*) *)
Import MetaCoq.List.ListNotations. Import Mtac2.List.ListNotations.
Program Definition solve_to_val : tactic := Program Definition solve_to_val : tactic :=
match_goal with match_goal with
| [[? e v |- to_val e = Some v ]] => | [[? e v |- to_val e = Some v ]] =>
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment