Library zoo.language.syntax
Require Import stdpp.countable.
Require Import iris.algebra.ofe.
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.list.
Require Export zoo.common.binder.
Require Export zoo.language.location.
Require Import zoo.options.
Implicit Type b : bool.
Implicit Type i tag : nat.
Implicit Type n : Z.
Implicit Type l : location.
Implicit Type f x : binder.
Definition block_id :=
positive.
Implicit Type bid : option block_id.
Definition prophet_id :=
positive.
Implicit Type pid : prophet_id.
Variant mutability :=
| Mutable
| ImmutableNongenerative
| ImmutableGenerativeWeak
| ImmutableGenerativeStrong.
Implicit Type mut : mutability.
#[global] Instance mutabilityｰeq_dec : EqDecision mutability :=
ltac:(solve_decision).
#[global] Instance mutabilityｰcountable :
Countable mutability.
Variant generativity :=
| Generative bid
| Nongenerative.
Implicit Type gen : generativity.
#[global] Instance generativityｰeq_dec : EqDecision generativity :=
ltac:(solve_decision).
#[global] Instance generativityｰcountable :
Countable generativity.
Variant literal :=
| LitBool b
| LitInt n
| LitLoc l
| LitProph pid
| LitPoison.
Implicit Type lit : literal.
#[global] Instance literalｰeq_dec : EqDecision literal :=
ltac:(solve_decision).
#[global] Instance literalｰcountable :
Countable literal.
Variant unop :=
| UnopNeg
| UnopMinus
| UnopIsImmediate.
#[global] Instance unopｰeq_dec : EqDecision unop :=
ltac:(solve_decision).
#[global] Instance unopｰcountable :
Countable unop.
Variant binop :=
| BinopPlus | BinopMinus | BinopMult | BinopQuot | BinopRem
| BinopLand | BinopLor | BinopLsl | BinopLsr
| BinopLe | BinopLt | BinopGe | BinopGt.
#[global] Instance binopｰeq_dec : EqDecision binop :=
ltac:(solve_decision).
#[global] Instance binopｰcountable :
Countable binop.
Record pattern :=
{ pattern۰tag : nat
; pattern۰fields : list binder
; pattern۰as : binder
}.
#[global] Instance patternｰinhabited : Inhabited pattern :=
populate
{|pattern۰tag := inhabitant
; pattern۰fields := inhabitant
; pattern۰as := inhabitant
|}.
#[global] Instance patternｰeq_dec : EqDecision pattern :=
ltac:(solve_decision).
#[global] Instance patternｰcountable :
Countable pattern.
Inductive expr :=
| Val (v : val)
| Var (x : string)
| Rec f x (e : expr)
| App (e1 e2 : expr)
| Let x (e1 e2 : expr)
| Unop (op : unop) (e : expr)
| Binop (op : binop) (e1 e2 : expr)
| Equal (e1 e2 : expr)
| If (e0 e1 e2 : expr)
| For (e1 e2 e3 : expr)
| Alloc (e1 e2 : expr)
| Block mut tag (es : list expr)
| Match (e0 : expr) x (e1 : expr) (brs : list (pattern × expr))
| GetTag (e : expr)
| GetSize (e : expr)
| Load (e1 e2 : expr)
| Store (e1 e2 e3 : expr)
| Xchg (e1 e2 : expr)
| CAS (e0 e1 e2 : expr)
| FAA (e1 e2 : expr)
| Fork (e : expr)
| GetLocal
| SetLocal (e : expr)
| Proph
| Resolve (e0 e1 e2 : expr)
with val :=
| ValLit lit
| ValRecs i (recs : list (binder × binder × expr))
| ValBlock gen tag (vs : list val).
Implicit Type e : expr.
Implicit Type es : list expr.
Implicit Type v : val.
Implicit Type vs : list val.
Notation branch :=
(pattern × expr)%type.
Implicit Type br : branch.
Implicit Type brs : list branch.
Notation recursive :=
(binder × binder × expr)%type.
Implicit Type rec : recursive.
Implicit Type recs : list recursive.
Section expr_ind.
Variable P : expr → Prop.
Variable HVal :
∀ v,
P (Val v).
Variable HVar :
∀ (x : string),
P (Var x).
Variable HRec :
∀ f x,
∀ e, P e →
P (Rec f x e).
Variable HApp :
∀ e1, P e1 →
∀ e2, P e2 →
P (App e1 e2).
Variable HLet :
∀ x,
∀ e1, P e1 →
∀ e2, P e2 →
P (Let x e1 e2).
Variable HUnop :
∀ op,
∀ e, P e →
P (Unop op e).
Variable HBinop :
∀ op,
∀ e1, P e1 →
∀ e2, P e2 →
P (Binop op e1 e2).
Variable HEqual :
∀ e1, P e1 →
∀ e2, P e2 →
P (Equal e1 e2).
Variable HIf :
∀ e0, P e0 →
∀ e1, P e1 →
∀ e2, P e2 →
P (If e0 e1 e2).
Variable HFor :
∀ e1, P e1 →
∀ e2, P e2 →
∀ e3, P e3 →
P (For e1 e2 e3).
Variable HAlloc :
∀ e1, P e1 →
∀ e2, P e2 →
P (Alloc e1 e2).
Variable HBlock :
∀ mut tag,
∀ es, Forall P es →
P (Block mut tag es).
Variable HMatch :
∀ e0, P e0 →
∀ x,
∀ e1, P e1 →
∀ brs, Forall (λ br, P br.2) brs →
P (Match e0 x e1 brs).
Variable HGetTag :
∀ e, P e →
P (GetTag e).
Variable HGetSize :
∀ e, P e →
P (GetSize e).
Variable HLoad :
∀ e1, P e1 →
∀ e2, P e2 →
P (Load e1 e2).
Variable HStore :
∀ e1, P e1 →
∀ e2, P e2 →
∀ e3, P e3 →
P (Store e1 e2 e3).
Variable HXchg :
∀ e1, P e1 →
∀ e2, P e2 →
P (Xchg e1 e2).
Variable HCAS :
∀ e0, P e0 →
∀ e1, P e1 →
∀ e2, P e2 →
P (CAS e0 e1 e2).
Variable HFAA :
∀ e1, P e1 →
∀ e2, P e2 →
P (FAA e1 e2).
Variable HFork :
∀ e, P e →
P (Fork e).
Variable HGetLocal :
P GetLocal.
Variable HSetLocal :
∀ e, P e →
P (SetLocal e).
Variable HProph :
P Proph.
Variable HResolve :
∀ e0, P e0 →
∀ e1, P e1 →
∀ e2, P e2 →
P (Resolve e0 e1 e2).
Fixpoint expr_ind e :=
match e with
| Val v ⇒
HVal
v
| Var x ⇒
HVar
x
| Rec f x e ⇒
HRec
f x
e (expr_ind e)
| App e1 e2 ⇒
HApp
e1 (expr_ind e1)
e2 (expr_ind e2)
| Let x e1 e2 ⇒
HLet
x
e1 (expr_ind e1)
e2 (expr_ind e2)
| Unop op e ⇒
HUnop
op
e (expr_ind e)
| Binop op e1 e2 ⇒
HBinop
op
e1 (expr_ind e1)
e2 (expr_ind e2)
| Equal e1 e2 ⇒
HEqual
e1 (expr_ind e1)
e2 (expr_ind e2)
| If e0 e1 e2 ⇒
HIf
e0 (expr_ind e0)
e1 (expr_ind e1)
e2 (expr_ind e2)
| For e1 e2 e3 ⇒
HFor
e1 (expr_ind e1)
e2 (expr_ind e2)
e3 (expr_ind e3)
| Alloc e1 e2 ⇒
HAlloc
e1 (expr_ind e1)
e2 (expr_ind e2)
| Block mut tag es ⇒
HBlock
mut tag
es (Forall_true P es expr_ind)
| Match e0 x e1 brs ⇒
HMatch
e0 (expr_ind e0)
x
e1 (expr_ind e1)
brs (Forall_true (λ br, P br.2) brs (λ br, expr_ind br.2))
| GetTag e ⇒
HGetTag
e (expr_ind e)
| GetSize e ⇒
HGetSize
e (expr_ind e)
| Load e1 e2 ⇒
HLoad
e1 (expr_ind e1)
e2 (expr_ind e2)
| Store e1 e2 e3 ⇒
HStore
e1 (expr_ind e1)
e2 (expr_ind e2)
e3 (expr_ind e3)
| Xchg e1 e2 ⇒
HXchg
e1 (expr_ind e1)
e2 (expr_ind e2)
| CAS e0 e1 e2 ⇒
HCAS
e0 (expr_ind e0)
e1 (expr_ind e1)
e2 (expr_ind e2)
| FAA e1 e2 ⇒
HFAA
e1 (expr_ind e1)
e2 (expr_ind e2)
| Fork e ⇒
HFork
e (expr_ind e)
| GetLocal ⇒
HGetLocal
| SetLocal e ⇒
HSetLocal
e (expr_ind e)
| Proph ⇒
HProph
| Resolve e0 e1 e2 ⇒
HResolve
e0 (expr_ind e0)
e1 (expr_ind e1)
e2 (expr_ind e2)
end.
End expr_ind.
Section val_ind.
Variable P : val → Prop.
Variable HValLit :
∀ lit,
P (ValLit lit).
Variable HValRecs :
∀ i recs,
P (ValRecs i recs).
Variable HValBlock :
∀ gen tag,
∀ vs, Forall P vs →
P (ValBlock gen tag vs).
Fixpoint val_ind v :=
match v with
| ValLit lit ⇒
HValLit
lit
| ValRecs i recs ⇒
HValRecs
i recs
| ValBlock gen tag vs ⇒
HValBlock
gen tag
vs (Forall_true P vs val_ind)
end.
End val_ind.
Section exprｰvalｰmutind.
Variable Pexpr : expr → Prop.
Variable Pval : val → Prop.
Variable HVal :
∀ v, Pval v →
Pexpr (Val v).
Variable HVar :
∀ (x : string),
Pexpr (Var x).
Variable HRec :
∀ f x,
∀ e, Pexpr e →
Pexpr (Rec f x e).
Variable HApp :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (App e1 e2).
Variable HLet :
∀ x,
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (Let x e1 e2).
Variable HUnop :
∀ op,
∀ e, Pexpr e →
Pexpr (Unop op e).
Variable HBinop :
∀ op,
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (Binop op e1 e2).
Variable HEqual :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (Equal e1 e2).
Variable HIf :
∀ e0, Pexpr e0 →
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (If e0 e1 e2).
Variable HFor :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
∀ e3, Pexpr e3 →
Pexpr (For e1 e2 e3).
Variable HAlloc :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (Alloc e1 e2).
Variable HBlock :
∀ mut tag,
∀ es, Forall Pexpr es →
Pexpr (Block mut tag es).
Variable HMatch :
∀ e0, Pexpr e0 →
∀ x,
∀ e1, Pexpr e1 →
∀ brs, Forall (λ br, Pexpr br.2) brs →
Pexpr (Match e0 x e1 brs).
Variable HGetTag :
∀ e, Pexpr e →
Pexpr (GetTag e).
Variable HGetSize :
∀ e, Pexpr e →
Pexpr (GetSize e).
Variable HLoad :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (Load e1 e2).
Variable HStore :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
∀ e3, Pexpr e3 →
Pexpr (Store e1 e2 e3).
Variable HXchg :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (Xchg e1 e2).
Variable HCAS :
∀ e0, Pexpr e0 →
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (CAS e0 e1 e2).
Variable HFAA :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (FAA e1 e2).
Variable HFork :
∀ e, Pexpr e →
Pexpr (Fork e).
Variable HGetLocal :
Pexpr GetLocal.
Variable HSetLocal :
∀ e, Pexpr e →
Pexpr (SetLocal e).
Variable HProph :
Pexpr Proph.
Variable HResolve :
∀ e0, Pexpr e0 →
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (Resolve e0 e1 e2).
Variable HValLit :
∀ lit,
Pval (ValLit lit).
Variable HValRecs :
∀ i,
∀ recs, Forall (λ rec, Pexpr rec.2) recs →
Pval (ValRecs i recs).
Variable HValBlock :
∀ gen tag,
∀ vs, Forall Pval vs →
Pval (ValBlock gen tag vs).
Fixpoint exprｰvalｰind e :=
match e with
| Val v ⇒
HVal
v (valｰexprｰind v)
| Var x ⇒
HVar
x
| Rec f x e ⇒
HRec
f x
e (exprｰvalｰind e)
| App e1 e2 ⇒
HApp
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| Let x e1 e2 ⇒
HLet
x
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| Unop op e ⇒
HUnop
op
e (exprｰvalｰind e)
| Binop op e1 e2 ⇒
HBinop
op
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| Equal e1 e2 ⇒
HEqual
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| If e0 e1 e2 ⇒
HIf
e0 (exprｰvalｰind e0)
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| For e1 e2 e3 ⇒
HFor
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
e3 (exprｰvalｰind e3)
| Alloc e1 e2 ⇒
HAlloc
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| Block mut tag es ⇒
HBlock
mut tag
es (Forall_true Pexpr es exprｰvalｰind)
| Match e0 x e1 brs ⇒
HMatch
e0 (exprｰvalｰind e0)
x
e1 (exprｰvalｰind e1)
brs (Forall_true (λ br, Pexpr br.2) brs (λ br, exprｰvalｰind br.2))
| GetTag e ⇒
HGetTag
e (exprｰvalｰind e)
| GetSize e ⇒
HGetSize
e (exprｰvalｰind e)
| Load e1 e2 ⇒
HLoad
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| Store e1 e2 e3 ⇒
HStore
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
e3 (exprｰvalｰind e3)
| Xchg e1 e2 ⇒
HXchg
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| CAS e0 e1 e2 ⇒
HCAS
e0 (exprｰvalｰind e0)
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| FAA e1 e2 ⇒
HFAA
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| Fork e ⇒
HFork
e (exprｰvalｰind e)
| GetLocal ⇒
HGetLocal
| SetLocal e ⇒
HSetLocal
e (exprｰvalｰind e)
| Proph ⇒
HProph
| Resolve e0 e1 e2 ⇒
HResolve
e0 (exprｰvalｰind e0)
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
end
with valｰexprｰind v :=
match v with
| ValLit lit ⇒
HValLit
lit
| ValRecs i recs ⇒
HValRecs
i
recs (Forall_true (λ rec, Pexpr rec.2) recs (λ rec, exprｰvalｰind rec.2))
| ValBlock gen tag vs ⇒
HValBlock
gen tag
vs (Forall_true Pval vs valｰexprｰind)
end.
Definition exprｰvalｰmutind :=
conj
exprｰvalｰind
valｰexprｰind.
End exprｰvalｰmutind.
Canonical val_O {SI : sidx} :=
leibnizO val.
Canonical expr_O {SI : sidx} :=
leibnizO expr.
Notation Fun x e := (
Rec BAnon x e
)(only parsing
).
Notation ValRec f x e := (
ValRecs 0
( @cons recursive
( @pair (prod binder binder) expr
(@pair binder binder f x)
e
)
(@nil recursive)
)
)(only parsing
).
Notation ValFun x e := (
ValRecs 0
( @cons recursive
( @pair (prod binder binder) expr
(@pair binder binder BAnon x)
e
)
(@nil recursive)
)
)(only parsing
).
Notation Seq e1 e2 := (
Let BAnon e1 e2
)(only parsing
).
Notation ValBool b := (
ValLit (LitBool b)
)(only parsing
).
Notation ValInt n := (
ValLit (LitInt n)
)(only parsing
).
Notation ValNat i := (
ValLit (LitInt (Z.of_nat i))
)(only parsing
).
Notation ValLoc l := (
ValLit (LitLoc l)
)(only parsing
).
Notation ValProph pid := (
ValLit (LitProph pid)
)(only parsing
).
Notation ValPoison := (
ValLit LitPoison
)(only parsing
).
Notation Tuple := (
Block ImmutableNongenerative 0
)(only parsing
).
Notation ValTuple := (
ValBlock Nongenerative 0
)(only parsing
).
Notation ValUnit := (
ValTuple []
)(only parsing
).
Notation Unit := (
Val ValUnit
)(only parsing
).
Notation Fail := (
App Unit Unit
).
Notation Skip := (
App (Val (ValFun BAnon Unit)) Unit
).
Notation IsImmediate := (
Unop UnopIsImmediate
).
Definition val۰of_int :=
ValLit ∘ LitInt.
Definition val۰to_int v :=
match v with
| ValInt n ⇒
Some n
| _ ⇒
None
end.
Definition val۰to_int' :=
default inhabitant ∘ val۰to_int.
Definition val۰to_nat' :=
Z.to_nat ∘ val۰to_int'.
Notation of_val :=
Val
( only parsing
).
Definition to_val e :=
match e with
| Val v ⇒
Some v
| _ ⇒
None
end.
Lemma to_valｰof_val v :
to_val (of_val v) = Some v.
Lemma of_valｰto_val e v :
to_val e = Some v →
of_val v = e.
#[global] Instance of_valｰinj :
Inj (=) (=) of_val.
Definition of_vals vs :=
of_val <$> vs.
Fixpoint to_vals es :=
match es with
| [] ⇒
Some []
| e :: es ⇒
v ← to_val e ;
es ← to_vals es ;
mret $ v :: es
end.
Lemma to_valsｰof_vals vs :
to_vals (of_vals vs) = Some vs.
Lemma of_valsｰto_vals es vs :
to_vals es = Some vs →
of_vals vs = es.
#[global] Instance of_valsｰinj :
Inj (=) (=) of_vals.
Lemma lengthｰof_vals vs :
length (of_vals vs) = length vs.
Hint Rewrite
@lengthｰof_vals
: simp_length.
#[global] Instance valｰinhabited : Inhabited val :=
populate ValUnit.
#[global] Instance exprｰinhabited : Inhabited expr :=
populate (Val inhabitant).
#[global] Instance exprｰeq_dec :
EqDecision expr.
#[global] Instance valｰeq_dec :
EqDecision val.
Variant encode_leaf :=
| EncodeNat tag
| EncodeBinder x
| EncodeGenerativity gen
| EncodeMutability mut
| EncodeLit lit
| EncodeUnop (op : unop)
| EncodeBinop (op : binop)
| EncodePattern (pat : pattern).
#[local] Instance encode_leafｰeq_dec : EqDecision encode_leaf :=
ltac:(solve_decision).
#[local] Instance encode_leafｰcountable :
Countable encode_leaf.
Notation EncodeString str := (
EncodeBinder (BNamed str)
).
#[global] Instance exprｰcountable :
Countable expr.
#[local] Notation code_Val :=
0.
#[local] Notation code_Rec :=
1.
#[local] Notation code_App :=
2.
#[local] Notation code_Let :=
3.
#[local] Notation code_Unop :=
4.
#[local] Notation code_Binop :=
5.
#[local] Notation code_Equal :=
6.
#[local] Notation code_If :=
7.
#[local] Notation code_For :=
8.
#[local] Notation code_Alloc :=
9.
#[local] Notation code_Block :=
10.
#[local] Notation code_Match :=
11.
#[local] Notation code_branch :=
12.
#[local] Notation code_GetTag :=
13.
#[local] Notation code_GetSize :=
14.
#[local] Notation code_Load :=
15.
#[local] Notation code_Store :=
16.
#[local] Notation code_Xchg :=
17.
#[local] Notation code_CAS :=
18.
#[local] Notation code_FAA :=
19.
#[local] Notation code_Fork :=
20.
#[local] Notation code_GetLocal :=
21.
#[local] Notation code_SetLocal :=
22.
#[local] Notation code_Proph :=
23.
#[local] Notation code_Resolve :=
24.
#[local] Notation code_ValRecs :=
0.
#[local] Notation code_recursive :=
1.
#[local] Notation code_ValBlock :=
2.
#[global] Instance valｰcountable :
Countable val.
Require Import iris.algebra.ofe.
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.list.
Require Export zoo.common.binder.
Require Export zoo.language.location.
Require Import zoo.options.
Implicit Type b : bool.
Implicit Type i tag : nat.
Implicit Type n : Z.
Implicit Type l : location.
Implicit Type f x : binder.
Definition block_id :=
positive.
Implicit Type bid : option block_id.
Definition prophet_id :=
positive.
Implicit Type pid : prophet_id.
Variant mutability :=
| Mutable
| ImmutableNongenerative
| ImmutableGenerativeWeak
| ImmutableGenerativeStrong.
Implicit Type mut : mutability.
#[global] Instance mutabilityｰeq_dec : EqDecision mutability :=
ltac:(solve_decision).
#[global] Instance mutabilityｰcountable :
Countable mutability.
Variant generativity :=
| Generative bid
| Nongenerative.
Implicit Type gen : generativity.
#[global] Instance generativityｰeq_dec : EqDecision generativity :=
ltac:(solve_decision).
#[global] Instance generativityｰcountable :
Countable generativity.
Variant literal :=
| LitBool b
| LitInt n
| LitLoc l
| LitProph pid
| LitPoison.
Implicit Type lit : literal.
#[global] Instance literalｰeq_dec : EqDecision literal :=
ltac:(solve_decision).
#[global] Instance literalｰcountable :
Countable literal.
Variant unop :=
| UnopNeg
| UnopMinus
| UnopIsImmediate.
#[global] Instance unopｰeq_dec : EqDecision unop :=
ltac:(solve_decision).
#[global] Instance unopｰcountable :
Countable unop.
Variant binop :=
| BinopPlus | BinopMinus | BinopMult | BinopQuot | BinopRem
| BinopLand | BinopLor | BinopLsl | BinopLsr
| BinopLe | BinopLt | BinopGe | BinopGt.
#[global] Instance binopｰeq_dec : EqDecision binop :=
ltac:(solve_decision).
#[global] Instance binopｰcountable :
Countable binop.
Record pattern :=
{ pattern۰tag : nat
; pattern۰fields : list binder
; pattern۰as : binder
}.
#[global] Instance patternｰinhabited : Inhabited pattern :=
populate
{|pattern۰tag := inhabitant
; pattern۰fields := inhabitant
; pattern۰as := inhabitant
|}.
#[global] Instance patternｰeq_dec : EqDecision pattern :=
ltac:(solve_decision).
#[global] Instance patternｰcountable :
Countable pattern.
Inductive expr :=
| Val (v : val)
| Var (x : string)
| Rec f x (e : expr)
| App (e1 e2 : expr)
| Let x (e1 e2 : expr)
| Unop (op : unop) (e : expr)
| Binop (op : binop) (e1 e2 : expr)
| Equal (e1 e2 : expr)
| If (e0 e1 e2 : expr)
| For (e1 e2 e3 : expr)
| Alloc (e1 e2 : expr)
| Block mut tag (es : list expr)
| Match (e0 : expr) x (e1 : expr) (brs : list (pattern × expr))
| GetTag (e : expr)
| GetSize (e : expr)
| Load (e1 e2 : expr)
| Store (e1 e2 e3 : expr)
| Xchg (e1 e2 : expr)
| CAS (e0 e1 e2 : expr)
| FAA (e1 e2 : expr)
| Fork (e : expr)
| GetLocal
| SetLocal (e : expr)
| Proph
| Resolve (e0 e1 e2 : expr)
with val :=
| ValLit lit
| ValRecs i (recs : list (binder × binder × expr))
| ValBlock gen tag (vs : list val).
Implicit Type e : expr.
Implicit Type es : list expr.
Implicit Type v : val.
Implicit Type vs : list val.
Notation branch :=
(pattern × expr)%type.
Implicit Type br : branch.
Implicit Type brs : list branch.
Notation recursive :=
(binder × binder × expr)%type.
Implicit Type rec : recursive.
Implicit Type recs : list recursive.
Section expr_ind.
Variable P : expr → Prop.
Variable HVal :
∀ v,
P (Val v).
Variable HVar :
∀ (x : string),
P (Var x).
Variable HRec :
∀ f x,
∀ e, P e →
P (Rec f x e).
Variable HApp :
∀ e1, P e1 →
∀ e2, P e2 →
P (App e1 e2).
Variable HLet :
∀ x,
∀ e1, P e1 →
∀ e2, P e2 →
P (Let x e1 e2).
Variable HUnop :
∀ op,
∀ e, P e →
P (Unop op e).
Variable HBinop :
∀ op,
∀ e1, P e1 →
∀ e2, P e2 →
P (Binop op e1 e2).
Variable HEqual :
∀ e1, P e1 →
∀ e2, P e2 →
P (Equal e1 e2).
Variable HIf :
∀ e0, P e0 →
∀ e1, P e1 →
∀ e2, P e2 →
P (If e0 e1 e2).
Variable HFor :
∀ e1, P e1 →
∀ e2, P e2 →
∀ e3, P e3 →
P (For e1 e2 e3).
Variable HAlloc :
∀ e1, P e1 →
∀ e2, P e2 →
P (Alloc e1 e2).
Variable HBlock :
∀ mut tag,
∀ es, Forall P es →
P (Block mut tag es).
Variable HMatch :
∀ e0, P e0 →
∀ x,
∀ e1, P e1 →
∀ brs, Forall (λ br, P br.2) brs →
P (Match e0 x e1 brs).
Variable HGetTag :
∀ e, P e →
P (GetTag e).
Variable HGetSize :
∀ e, P e →
P (GetSize e).
Variable HLoad :
∀ e1, P e1 →
∀ e2, P e2 →
P (Load e1 e2).
Variable HStore :
∀ e1, P e1 →
∀ e2, P e2 →
∀ e3, P e3 →
P (Store e1 e2 e3).
Variable HXchg :
∀ e1, P e1 →
∀ e2, P e2 →
P (Xchg e1 e2).
Variable HCAS :
∀ e0, P e0 →
∀ e1, P e1 →
∀ e2, P e2 →
P (CAS e0 e1 e2).
Variable HFAA :
∀ e1, P e1 →
∀ e2, P e2 →
P (FAA e1 e2).
Variable HFork :
∀ e, P e →
P (Fork e).
Variable HGetLocal :
P GetLocal.
Variable HSetLocal :
∀ e, P e →
P (SetLocal e).
Variable HProph :
P Proph.
Variable HResolve :
∀ e0, P e0 →
∀ e1, P e1 →
∀ e2, P e2 →
P (Resolve e0 e1 e2).
Fixpoint expr_ind e :=
match e with
| Val v ⇒
HVal
v
| Var x ⇒
HVar
x
| Rec f x e ⇒
HRec
f x
e (expr_ind e)
| App e1 e2 ⇒
HApp
e1 (expr_ind e1)
e2 (expr_ind e2)
| Let x e1 e2 ⇒
HLet
x
e1 (expr_ind e1)
e2 (expr_ind e2)
| Unop op e ⇒
HUnop
op
e (expr_ind e)
| Binop op e1 e2 ⇒
HBinop
op
e1 (expr_ind e1)
e2 (expr_ind e2)
| Equal e1 e2 ⇒
HEqual
e1 (expr_ind e1)
e2 (expr_ind e2)
| If e0 e1 e2 ⇒
HIf
e0 (expr_ind e0)
e1 (expr_ind e1)
e2 (expr_ind e2)
| For e1 e2 e3 ⇒
HFor
e1 (expr_ind e1)
e2 (expr_ind e2)
e3 (expr_ind e3)
| Alloc e1 e2 ⇒
HAlloc
e1 (expr_ind e1)
e2 (expr_ind e2)
| Block mut tag es ⇒
HBlock
mut tag
es (Forall_true P es expr_ind)
| Match e0 x e1 brs ⇒
HMatch
e0 (expr_ind e0)
x
e1 (expr_ind e1)
brs (Forall_true (λ br, P br.2) brs (λ br, expr_ind br.2))
| GetTag e ⇒
HGetTag
e (expr_ind e)
| GetSize e ⇒
HGetSize
e (expr_ind e)
| Load e1 e2 ⇒
HLoad
e1 (expr_ind e1)
e2 (expr_ind e2)
| Store e1 e2 e3 ⇒
HStore
e1 (expr_ind e1)
e2 (expr_ind e2)
e3 (expr_ind e3)
| Xchg e1 e2 ⇒
HXchg
e1 (expr_ind e1)
e2 (expr_ind e2)
| CAS e0 e1 e2 ⇒
HCAS
e0 (expr_ind e0)
e1 (expr_ind e1)
e2 (expr_ind e2)
| FAA e1 e2 ⇒
HFAA
e1 (expr_ind e1)
e2 (expr_ind e2)
| Fork e ⇒
HFork
e (expr_ind e)
| GetLocal ⇒
HGetLocal
| SetLocal e ⇒
HSetLocal
e (expr_ind e)
| Proph ⇒
HProph
| Resolve e0 e1 e2 ⇒
HResolve
e0 (expr_ind e0)
e1 (expr_ind e1)
e2 (expr_ind e2)
end.
End expr_ind.
Section val_ind.
Variable P : val → Prop.
Variable HValLit :
∀ lit,
P (ValLit lit).
Variable HValRecs :
∀ i recs,
P (ValRecs i recs).
Variable HValBlock :
∀ gen tag,
∀ vs, Forall P vs →
P (ValBlock gen tag vs).
Fixpoint val_ind v :=
match v with
| ValLit lit ⇒
HValLit
lit
| ValRecs i recs ⇒
HValRecs
i recs
| ValBlock gen tag vs ⇒
HValBlock
gen tag
vs (Forall_true P vs val_ind)
end.
End val_ind.
Section exprｰvalｰmutind.
Variable Pexpr : expr → Prop.
Variable Pval : val → Prop.
Variable HVal :
∀ v, Pval v →
Pexpr (Val v).
Variable HVar :
∀ (x : string),
Pexpr (Var x).
Variable HRec :
∀ f x,
∀ e, Pexpr e →
Pexpr (Rec f x e).
Variable HApp :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (App e1 e2).
Variable HLet :
∀ x,
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (Let x e1 e2).
Variable HUnop :
∀ op,
∀ e, Pexpr e →
Pexpr (Unop op e).
Variable HBinop :
∀ op,
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (Binop op e1 e2).
Variable HEqual :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (Equal e1 e2).
Variable HIf :
∀ e0, Pexpr e0 →
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (If e0 e1 e2).
Variable HFor :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
∀ e3, Pexpr e3 →
Pexpr (For e1 e2 e3).
Variable HAlloc :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (Alloc e1 e2).
Variable HBlock :
∀ mut tag,
∀ es, Forall Pexpr es →
Pexpr (Block mut tag es).
Variable HMatch :
∀ e0, Pexpr e0 →
∀ x,
∀ e1, Pexpr e1 →
∀ brs, Forall (λ br, Pexpr br.2) brs →
Pexpr (Match e0 x e1 brs).
Variable HGetTag :
∀ e, Pexpr e →
Pexpr (GetTag e).
Variable HGetSize :
∀ e, Pexpr e →
Pexpr (GetSize e).
Variable HLoad :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (Load e1 e2).
Variable HStore :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
∀ e3, Pexpr e3 →
Pexpr (Store e1 e2 e3).
Variable HXchg :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (Xchg e1 e2).
Variable HCAS :
∀ e0, Pexpr e0 →
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (CAS e0 e1 e2).
Variable HFAA :
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (FAA e1 e2).
Variable HFork :
∀ e, Pexpr e →
Pexpr (Fork e).
Variable HGetLocal :
Pexpr GetLocal.
Variable HSetLocal :
∀ e, Pexpr e →
Pexpr (SetLocal e).
Variable HProph :
Pexpr Proph.
Variable HResolve :
∀ e0, Pexpr e0 →
∀ e1, Pexpr e1 →
∀ e2, Pexpr e2 →
Pexpr (Resolve e0 e1 e2).
Variable HValLit :
∀ lit,
Pval (ValLit lit).
Variable HValRecs :
∀ i,
∀ recs, Forall (λ rec, Pexpr rec.2) recs →
Pval (ValRecs i recs).
Variable HValBlock :
∀ gen tag,
∀ vs, Forall Pval vs →
Pval (ValBlock gen tag vs).
Fixpoint exprｰvalｰind e :=
match e with
| Val v ⇒
HVal
v (valｰexprｰind v)
| Var x ⇒
HVar
x
| Rec f x e ⇒
HRec
f x
e (exprｰvalｰind e)
| App e1 e2 ⇒
HApp
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| Let x e1 e2 ⇒
HLet
x
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| Unop op e ⇒
HUnop
op
e (exprｰvalｰind e)
| Binop op e1 e2 ⇒
HBinop
op
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| Equal e1 e2 ⇒
HEqual
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| If e0 e1 e2 ⇒
HIf
e0 (exprｰvalｰind e0)
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| For e1 e2 e3 ⇒
HFor
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
e3 (exprｰvalｰind e3)
| Alloc e1 e2 ⇒
HAlloc
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| Block mut tag es ⇒
HBlock
mut tag
es (Forall_true Pexpr es exprｰvalｰind)
| Match e0 x e1 brs ⇒
HMatch
e0 (exprｰvalｰind e0)
x
e1 (exprｰvalｰind e1)
brs (Forall_true (λ br, Pexpr br.2) brs (λ br, exprｰvalｰind br.2))
| GetTag e ⇒
HGetTag
e (exprｰvalｰind e)
| GetSize e ⇒
HGetSize
e (exprｰvalｰind e)
| Load e1 e2 ⇒
HLoad
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| Store e1 e2 e3 ⇒
HStore
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
e3 (exprｰvalｰind e3)
| Xchg e1 e2 ⇒
HXchg
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| CAS e0 e1 e2 ⇒
HCAS
e0 (exprｰvalｰind e0)
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| FAA e1 e2 ⇒
HFAA
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
| Fork e ⇒
HFork
e (exprｰvalｰind e)
| GetLocal ⇒
HGetLocal
| SetLocal e ⇒
HSetLocal
e (exprｰvalｰind e)
| Proph ⇒
HProph
| Resolve e0 e1 e2 ⇒
HResolve
e0 (exprｰvalｰind e0)
e1 (exprｰvalｰind e1)
e2 (exprｰvalｰind e2)
end
with valｰexprｰind v :=
match v with
| ValLit lit ⇒
HValLit
lit
| ValRecs i recs ⇒
HValRecs
i
recs (Forall_true (λ rec, Pexpr rec.2) recs (λ rec, exprｰvalｰind rec.2))
| ValBlock gen tag vs ⇒
HValBlock
gen tag
vs (Forall_true Pval vs valｰexprｰind)
end.
Definition exprｰvalｰmutind :=
conj
exprｰvalｰind
valｰexprｰind.
End exprｰvalｰmutind.
Canonical val_O {SI : sidx} :=
leibnizO val.
Canonical expr_O {SI : sidx} :=
leibnizO expr.
Notation Fun x e := (
Rec BAnon x e
)(only parsing
).
Notation ValRec f x e := (
ValRecs 0
( @cons recursive
( @pair (prod binder binder) expr
(@pair binder binder f x)
e
)
(@nil recursive)
)
)(only parsing
).
Notation ValFun x e := (
ValRecs 0
( @cons recursive
( @pair (prod binder binder) expr
(@pair binder binder BAnon x)
e
)
(@nil recursive)
)
)(only parsing
).
Notation Seq e1 e2 := (
Let BAnon e1 e2
)(only parsing
).
Notation ValBool b := (
ValLit (LitBool b)
)(only parsing
).
Notation ValInt n := (
ValLit (LitInt n)
)(only parsing
).
Notation ValNat i := (
ValLit (LitInt (Z.of_nat i))
)(only parsing
).
Notation ValLoc l := (
ValLit (LitLoc l)
)(only parsing
).
Notation ValProph pid := (
ValLit (LitProph pid)
)(only parsing
).
Notation ValPoison := (
ValLit LitPoison
)(only parsing
).
Notation Tuple := (
Block ImmutableNongenerative 0
)(only parsing
).
Notation ValTuple := (
ValBlock Nongenerative 0
)(only parsing
).
Notation ValUnit := (
ValTuple []
)(only parsing
).
Notation Unit := (
Val ValUnit
)(only parsing
).
Notation Fail := (
App Unit Unit
).
Notation Skip := (
App (Val (ValFun BAnon Unit)) Unit
).
Notation IsImmediate := (
Unop UnopIsImmediate
).
Definition val۰of_int :=
ValLit ∘ LitInt.
Definition val۰to_int v :=
match v with
| ValInt n ⇒
Some n
| _ ⇒
None
end.
Definition val۰to_int' :=
default inhabitant ∘ val۰to_int.
Definition val۰to_nat' :=
Z.to_nat ∘ val۰to_int'.
Notation of_val :=
Val
( only parsing
).
Definition to_val e :=
match e with
| Val v ⇒
Some v
| _ ⇒
None
end.
Lemma to_valｰof_val v :
to_val (of_val v) = Some v.
Lemma of_valｰto_val e v :
to_val e = Some v →
of_val v = e.
#[global] Instance of_valｰinj :
Inj (=) (=) of_val.
Definition of_vals vs :=
of_val <$> vs.
Fixpoint to_vals es :=
match es with
| [] ⇒
Some []
| e :: es ⇒
v ← to_val e ;
es ← to_vals es ;
mret $ v :: es
end.
Lemma to_valsｰof_vals vs :
to_vals (of_vals vs) = Some vs.
Lemma of_valsｰto_vals es vs :
to_vals es = Some vs →
of_vals vs = es.
#[global] Instance of_valsｰinj :
Inj (=) (=) of_vals.
Lemma lengthｰof_vals vs :
length (of_vals vs) = length vs.
Hint Rewrite
@lengthｰof_vals
: simp_length.
#[global] Instance valｰinhabited : Inhabited val :=
populate ValUnit.
#[global] Instance exprｰinhabited : Inhabited expr :=
populate (Val inhabitant).
#[global] Instance exprｰeq_dec :
EqDecision expr.
#[global] Instance valｰeq_dec :
EqDecision val.
Variant encode_leaf :=
| EncodeNat tag
| EncodeBinder x
| EncodeGenerativity gen
| EncodeMutability mut
| EncodeLit lit
| EncodeUnop (op : unop)
| EncodeBinop (op : binop)
| EncodePattern (pat : pattern).
#[local] Instance encode_leafｰeq_dec : EqDecision encode_leaf :=
ltac:(solve_decision).
#[local] Instance encode_leafｰcountable :
Countable encode_leaf.
Notation EncodeString str := (
EncodeBinder (BNamed str)
).
#[global] Instance exprｰcountable :
Countable expr.
#[local] Notation code_Val :=
0.
#[local] Notation code_Rec :=
1.
#[local] Notation code_App :=
2.
#[local] Notation code_Let :=
3.
#[local] Notation code_Unop :=
4.
#[local] Notation code_Binop :=
5.
#[local] Notation code_Equal :=
6.
#[local] Notation code_If :=
7.
#[local] Notation code_For :=
8.
#[local] Notation code_Alloc :=
9.
#[local] Notation code_Block :=
10.
#[local] Notation code_Match :=
11.
#[local] Notation code_branch :=
12.
#[local] Notation code_GetTag :=
13.
#[local] Notation code_GetSize :=
14.
#[local] Notation code_Load :=
15.
#[local] Notation code_Store :=
16.
#[local] Notation code_Xchg :=
17.
#[local] Notation code_CAS :=
18.
#[local] Notation code_FAA :=
19.
#[local] Notation code_Fork :=
20.
#[local] Notation code_GetLocal :=
21.
#[local] Notation code_SetLocal :=
22.
#[local] Notation code_Proph :=
23.
#[local] Notation code_Resolve :=
24.
#[local] Notation code_ValRecs :=
0.
#[local] Notation code_recursive :=
1.
#[local] Notation code_ValBlock :=
2.
#[global] Instance valｰcountable :
Countable val.