Library zoo.language.typeclasses
Require Import zoo.prelude.
Require Export zoo.common.list.
Require Export zoo.language.language.
Require Export zoo.language.metatheory.
Require Import zoo.language.tactics.
Require Import zoo.options.
Implicit Type e : expr.
Implicit Type v : val.
#[global] Instance val۰as_val v :
AsVal (Val v) v.
Section atomic.
#[local] Ltac solve_atomic :=
apply base_atomicｰatomic;
[ inversion 1; naive_solver
| apply sub_redexes_are_valuesｰalt; intros [] **; naive_solver
].
#[global] Instance pureｰatomic e v :
PureExec True 1 e (Val v) →
Atomic e.
#[global] Instance get_sizeｰatomic v :
Atomic (GetSize (Val v)).
#[global] Instance loadｰatomic v1 v2 :
Atomic (Load (Val v1) (Val v2)).
#[global] Instance storeｰatomic v1 v2 v3 :
Atomic (Store (Val v1) (Val v2) (Val v3)).
#[global] Instance xchgｰatomic v1 v2 :
Atomic (Xchg (Val v1) (Val v2)).
#[global] Instance casｰatomic v0 v1 v2 :
Atomic (CAS (Val v0) (Val v1) (Val v2)).
#[global] Instance faaｰatomic v1 v2 :
Atomic (FAA (Val v1) (Val v2)).
#[global] Instance resolveｰatomic e v1 v2 :
Atomic e →
Atomic (Resolve e (Val v1) (Val v2)).
End atomic.
Class AsValRec v f x e :=
as_ValRec : v = ValRec f x e.
#[global] Hint Mode AsValRec ! - - - : typeclass_instances.
Lemma ValRecｰas_ValRec f x e :
AsValRec (ValRec f x e) f x e.
#[global] Hint Extern 0 (
AsValRec (ValRec _ _ _) _ _ _
) ⇒
apply ValRecｰas_ValRec
: typeclass_instances.
Class AsValRecs v i recs vs :=
as_ValRecs :
Foralli (λ i v, v = ValRecs i recs) vs ∧
v = ValRecs i recs ∧
length recs = length vs.
#[global] Hint Mode AsValRecs ! - - - : typeclass_instances.
#[global] Instance as_ValRecｰas_ValRecs v f x e :
AsValRec v f x e →
AsValRecs v 0 [(f, x, e)] [v].
Class AsValRecs' v i recs vs :=
as_ValRecs' : AsValRecs v i recs vs.
Lemma as_ValRecs'ｰas_ValRecs v i recs vs :
AsValRecs' v i recs vs →
AsValRecs v i recs vs.
Section pure_exec.
#[local] Ltac solve_exec_safe :=
intros; subst;
eauto with zoo.
#[local] Ltac solve_exec_puredet :=
intros;
inv_base_step;
try naive_solver.
#[local] Ltac solve_pure_exec :=
intros ?; destruct_and?;
apply nsteps_once, pure_base_stepｰpure_step;
try (case_bool_decide; first subst);
(split; [solve_exec_safe | solve_exec_puredet]).
#[global] Instance pureｰrec f x e :
PureExec
True
1
(Rec f x e)
(Val $ ValRec f x e).
#[global] Instance pureｰapp v1 i recs rec vs v2 `{HAsValRecs : !AsValRecs v1 i recs vs} :
PureExec
(recs !! i = Some rec)
1
(App (Val v1) (Val v2))
(foldr2 (λ rec v, subst' rec.1.1 v) (subst' rec.1.2 v2 rec.2) recs vs).
#[global] Instance pureｰappｰrec f x v1 v2 :
PureExec True 1 (App (Val $ ValRec f x (Val v1)) (Val v2)) (Val v1).
#[global] Instance pureｰlet x v1 e2 :
PureExec
True
1
(Let x (Val v1) e2)
(subst' x v1 e2).
#[global] Instance pureｰunop op v v' :
PureExec
(eval_unop op v = Some v')
1
(Unop op (Val v))
(Val v').
#[global] Instance pureｰbinop op v1 v2 v' :
PureExec
(eval_binop op v1 v2 = Some v')
1
(Binop op (Val v1) (Val v2))
(Val v').
#[global] Instance pureｰequalｰbool b1 b2 :
PureExec
True
1
(Equal (Val $ ValBool b1) (Val $ ValBool b2))
(Val $ ValBool (bool_decide (b1 = b2))).
#[global] Instance pureｰequalｰint i1 i2 :
PureExec
True
1
(Equal (Val $ ValInt i1) (Val $ ValInt i2))
(Val $ ValBool (bool_decide (i1 = i2))).
#[global] Instance pureｰequalｰlocation l1 l2 :
PureExec
True
1
(Equal (Val $ ValLoc l1) (Val $ ValLoc l2))
(Val $ ValBool (bool_decide (l1 = l2))).
#[global] Instance pureｰequalｰlocationｰblock l gen tag vs :
PureExec
True
1
(Equal (Val $ ValLoc l) (Val $ ValBlock gen tag vs))
(Val $ ValBool false).
#[global] Instance pureｰequalｰblockｰlocation gen tag vs l :
PureExec
True
1
(Equal (Val $ ValBlock gen tag vs) (Val $ ValLoc l))
(Val $ ValBool false).
#[global] Instance pureｰequalｰblockｰgenerative bid tag vs :
PureExec
True
1
(Equal (Val $ ValBlock (Generative (Some bid)) tag vs) (Val $ ValBlock (Generative (Some bid)) tag vs))
(Val $ ValBool true).
#[global] Instance pureｰequalｰblockｰgenerativeｰnongenerative bid1 tag1 vs1 tag2 vs2 :
PureExec
(length vs1 ≠ 0 ∨ length vs2 ≠ 0)
1
(Equal (Val $ ValBlock (Generative bid1) tag1 vs1) (Val $ ValBlock Nongenerative tag2 vs2))
(Val $ ValBool false).
#[global] Instance pureｰequalｰblockｰnongenerativeｰgenerative tag1 vs1 bid2 tag2 vs2 :
PureExec
(length vs1 ≠ 0 ∨ length vs2 ≠ 0)
1
(Equal (Val $ ValBlock Nongenerative tag1 vs1) (Val $ ValBlock (Generative bid2) tag2 vs2))
(Val $ ValBool false).
#[global] Instance pureｰequalｰblockｰempty tag1 tag2 :
PureExec
True
1
(Equal (Val $ ValBlock Nongenerative tag1 []) (Val $ ValBlock Nongenerative tag2 []))
(Val $ ValBool (bool_decide (tag1 = tag2))).
#[global] Instance pureｰequalｰblockｰempty₁ gen1 tag1 gen2 tag2 v2 vs2 :
PureExec
True
1
(Equal (Val $ ValBlock gen1 tag1 []) (Val $ ValBlock gen2 tag2 (v2 :: vs2)))
(Val $ ValBool false).
#[global] Instance pureｰequalｰblockｰempty₂ gen1 tag1 v1 vs1 gen2 tag2 :
PureExec
True
1
(Equal (Val $ ValBlock gen1 tag1 (v1 :: vs1)) (Val $ ValBlock gen2 tag2 []))
(Val $ ValBool false).
#[global] Instance pureｰifｰtrue e1 e2 :
PureExec
True
1
(If (Val $ ValBool true) e1 e2)
e1.
#[global] Instance pureｰifｰfalse e1 e2 :
PureExec
True
1
(If (Val $ ValBool false) e1 e2)
e2.
Lemma pureｰfor n1 n2 e :
PureExec
True
1
(For (Val $ ValInt n1) (Val $ ValInt n2) e)
(if decide (n2 ≤ n1)%Z then Unit else Seq (App e (Val $ ValInt n1)) (For (Val $ ValInt (n1 + 1)) (Val $ ValInt n2) e)).
#[global] Instance pureｰblockｰimmutableｰnongenerative tag es vs :
PureExec
(to_vals es = Some vs)
1
(Block ImmutableNongenerative tag es)
(Val $ ValBlock Nongenerative tag vs).
#[global] Instance pureｰblockｰimmutableｰgenerative tag es vs :
PureExec
(to_vals es = Some vs)
1
(Block ImmutableGenerativeWeak tag es)
(Val $ ValBlock (Generative None) tag vs).
#[global] Instance pureｰmatch gen tag vs x_fb e_fb brs e :
PureExec
(eval_match tag (length vs) (SubjectBlock gen vs) x_fb e_fb brs = Some e)
1
(Match (Val $ ValBlock gen tag vs) x_fb e_fb brs)
e.
#[global] Instance pureｰget_tag gen tag vs :
PureExec
(0 < length vs)
1
(GetTag $ Val $ ValBlock gen tag vs)
(Val $ ValNat (encode_tag tag)).
#[global] Instance pureｰget_size gen tag vs :
PureExec
(0 < length vs)
1
(GetSize $ Val $ ValBlock gen tag vs)
(Val $ ValNat (length vs)).
#[global] Instance pureｰload gen tag vs (fld : nat) v :
PureExec
(vs !! fld = Some v)
1
(Load (Val $ ValBlock gen tag vs) (Val $ ValNat fld))
(Val v).
End pure_exec.
Require Export zoo.common.list.
Require Export zoo.language.language.
Require Export zoo.language.metatheory.
Require Import zoo.language.tactics.
Require Import zoo.options.
Implicit Type e : expr.
Implicit Type v : val.
#[global] Instance val۰as_val v :
AsVal (Val v) v.
Section atomic.
#[local] Ltac solve_atomic :=
apply base_atomicｰatomic;
[ inversion 1; naive_solver
| apply sub_redexes_are_valuesｰalt; intros [] **; naive_solver
].
#[global] Instance pureｰatomic e v :
PureExec True 1 e (Val v) →
Atomic e.
#[global] Instance get_sizeｰatomic v :
Atomic (GetSize (Val v)).
#[global] Instance loadｰatomic v1 v2 :
Atomic (Load (Val v1) (Val v2)).
#[global] Instance storeｰatomic v1 v2 v3 :
Atomic (Store (Val v1) (Val v2) (Val v3)).
#[global] Instance xchgｰatomic v1 v2 :
Atomic (Xchg (Val v1) (Val v2)).
#[global] Instance casｰatomic v0 v1 v2 :
Atomic (CAS (Val v0) (Val v1) (Val v2)).
#[global] Instance faaｰatomic v1 v2 :
Atomic (FAA (Val v1) (Val v2)).
#[global] Instance resolveｰatomic e v1 v2 :
Atomic e →
Atomic (Resolve e (Val v1) (Val v2)).
End atomic.
Class AsValRec v f x e :=
as_ValRec : v = ValRec f x e.
#[global] Hint Mode AsValRec ! - - - : typeclass_instances.
Lemma ValRecｰas_ValRec f x e :
AsValRec (ValRec f x e) f x e.
#[global] Hint Extern 0 (
AsValRec (ValRec _ _ _) _ _ _
) ⇒
apply ValRecｰas_ValRec
: typeclass_instances.
Class AsValRecs v i recs vs :=
as_ValRecs :
Foralli (λ i v, v = ValRecs i recs) vs ∧
v = ValRecs i recs ∧
length recs = length vs.
#[global] Hint Mode AsValRecs ! - - - : typeclass_instances.
#[global] Instance as_ValRecｰas_ValRecs v f x e :
AsValRec v f x e →
AsValRecs v 0 [(f, x, e)] [v].
Class AsValRecs' v i recs vs :=
as_ValRecs' : AsValRecs v i recs vs.
Lemma as_ValRecs'ｰas_ValRecs v i recs vs :
AsValRecs' v i recs vs →
AsValRecs v i recs vs.
Section pure_exec.
#[local] Ltac solve_exec_safe :=
intros; subst;
eauto with zoo.
#[local] Ltac solve_exec_puredet :=
intros;
inv_base_step;
try naive_solver.
#[local] Ltac solve_pure_exec :=
intros ?; destruct_and?;
apply nsteps_once, pure_base_stepｰpure_step;
try (case_bool_decide; first subst);
(split; [solve_exec_safe | solve_exec_puredet]).
#[global] Instance pureｰrec f x e :
PureExec
True
1
(Rec f x e)
(Val $ ValRec f x e).
#[global] Instance pureｰapp v1 i recs rec vs v2 `{HAsValRecs : !AsValRecs v1 i recs vs} :
PureExec
(recs !! i = Some rec)
1
(App (Val v1) (Val v2))
(foldr2 (λ rec v, subst' rec.1.1 v) (subst' rec.1.2 v2 rec.2) recs vs).
#[global] Instance pureｰappｰrec f x v1 v2 :
PureExec True 1 (App (Val $ ValRec f x (Val v1)) (Val v2)) (Val v1).
#[global] Instance pureｰlet x v1 e2 :
PureExec
True
1
(Let x (Val v1) e2)
(subst' x v1 e2).
#[global] Instance pureｰunop op v v' :
PureExec
(eval_unop op v = Some v')
1
(Unop op (Val v))
(Val v').
#[global] Instance pureｰbinop op v1 v2 v' :
PureExec
(eval_binop op v1 v2 = Some v')
1
(Binop op (Val v1) (Val v2))
(Val v').
#[global] Instance pureｰequalｰbool b1 b2 :
PureExec
True
1
(Equal (Val $ ValBool b1) (Val $ ValBool b2))
(Val $ ValBool (bool_decide (b1 = b2))).
#[global] Instance pureｰequalｰint i1 i2 :
PureExec
True
1
(Equal (Val $ ValInt i1) (Val $ ValInt i2))
(Val $ ValBool (bool_decide (i1 = i2))).
#[global] Instance pureｰequalｰlocation l1 l2 :
PureExec
True
1
(Equal (Val $ ValLoc l1) (Val $ ValLoc l2))
(Val $ ValBool (bool_decide (l1 = l2))).
#[global] Instance pureｰequalｰlocationｰblock l gen tag vs :
PureExec
True
1
(Equal (Val $ ValLoc l) (Val $ ValBlock gen tag vs))
(Val $ ValBool false).
#[global] Instance pureｰequalｰblockｰlocation gen tag vs l :
PureExec
True
1
(Equal (Val $ ValBlock gen tag vs) (Val $ ValLoc l))
(Val $ ValBool false).
#[global] Instance pureｰequalｰblockｰgenerative bid tag vs :
PureExec
True
1
(Equal (Val $ ValBlock (Generative (Some bid)) tag vs) (Val $ ValBlock (Generative (Some bid)) tag vs))
(Val $ ValBool true).
#[global] Instance pureｰequalｰblockｰgenerativeｰnongenerative bid1 tag1 vs1 tag2 vs2 :
PureExec
(length vs1 ≠ 0 ∨ length vs2 ≠ 0)
1
(Equal (Val $ ValBlock (Generative bid1) tag1 vs1) (Val $ ValBlock Nongenerative tag2 vs2))
(Val $ ValBool false).
#[global] Instance pureｰequalｰblockｰnongenerativeｰgenerative tag1 vs1 bid2 tag2 vs2 :
PureExec
(length vs1 ≠ 0 ∨ length vs2 ≠ 0)
1
(Equal (Val $ ValBlock Nongenerative tag1 vs1) (Val $ ValBlock (Generative bid2) tag2 vs2))
(Val $ ValBool false).
#[global] Instance pureｰequalｰblockｰempty tag1 tag2 :
PureExec
True
1
(Equal (Val $ ValBlock Nongenerative tag1 []) (Val $ ValBlock Nongenerative tag2 []))
(Val $ ValBool (bool_decide (tag1 = tag2))).
#[global] Instance pureｰequalｰblockｰempty₁ gen1 tag1 gen2 tag2 v2 vs2 :
PureExec
True
1
(Equal (Val $ ValBlock gen1 tag1 []) (Val $ ValBlock gen2 tag2 (v2 :: vs2)))
(Val $ ValBool false).
#[global] Instance pureｰequalｰblockｰempty₂ gen1 tag1 v1 vs1 gen2 tag2 :
PureExec
True
1
(Equal (Val $ ValBlock gen1 tag1 (v1 :: vs1)) (Val $ ValBlock gen2 tag2 []))
(Val $ ValBool false).
#[global] Instance pureｰifｰtrue e1 e2 :
PureExec
True
1
(If (Val $ ValBool true) e1 e2)
e1.
#[global] Instance pureｰifｰfalse e1 e2 :
PureExec
True
1
(If (Val $ ValBool false) e1 e2)
e2.
Lemma pureｰfor n1 n2 e :
PureExec
True
1
(For (Val $ ValInt n1) (Val $ ValInt n2) e)
(if decide (n2 ≤ n1)%Z then Unit else Seq (App e (Val $ ValInt n1)) (For (Val $ ValInt (n1 + 1)) (Val $ ValInt n2) e)).
#[global] Instance pureｰblockｰimmutableｰnongenerative tag es vs :
PureExec
(to_vals es = Some vs)
1
(Block ImmutableNongenerative tag es)
(Val $ ValBlock Nongenerative tag vs).
#[global] Instance pureｰblockｰimmutableｰgenerative tag es vs :
PureExec
(to_vals es = Some vs)
1
(Block ImmutableGenerativeWeak tag es)
(Val $ ValBlock (Generative None) tag vs).
#[global] Instance pureｰmatch gen tag vs x_fb e_fb brs e :
PureExec
(eval_match tag (length vs) (SubjectBlock gen vs) x_fb e_fb brs = Some e)
1
(Match (Val $ ValBlock gen tag vs) x_fb e_fb brs)
e.
#[global] Instance pureｰget_tag gen tag vs :
PureExec
(0 < length vs)
1
(GetTag $ Val $ ValBlock gen tag vs)
(Val $ ValNat (encode_tag tag)).
#[global] Instance pureｰget_size gen tag vs :
PureExec
(0 < length vs)
1
(GetSize $ Val $ ValBlock gen tag vs)
(Val $ ValNat (length vs)).
#[global] Instance pureｰload gen tag vs (fld : nat) v :
PureExec
(vs !! fld = Some v)
1
(Load (Val $ ValBlock gen tag vs) (Val $ ValNat fld))
(Val v).
End pure_exec.