Library zoo.language.syntax
From stdpp Require Import
countable.
From iris.algebra Require Import
ofe.
From zoo Require Import
prelude.
From zoo.common Require Import
countable
list.
From zoo.common Require Export
binder.
From zoo.language Require Export
location.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types i tag : nat.
Implicit Types n : Z.
Implicit Types l : location.
Implicit Types f x : binder.
Definition block_id :=
positive.
Implicit Types bid : option block_id.
Definition prophet_id :=
positive.
Implicit Types pid : prophet_id.
Variant mutability :=
| Mutable
| ImmutableNongenerative
| ImmutableGenerativeWeak
| ImmutableGenerativeStrong.
Implicit Types mut : mutability.
#[global] Instance mutability_eq_dec : EqDecision mutability :=
ltac:(solve_decision).
#[global] Instance mutability_countable :
Countable mutability.
Variant generativity :=
| Generative bid
| Nongenerative.
Implicit Types 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 Types 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 Types e : expr.
Implicit Types es : list expr.
Implicit Types v : val.
Implicit Types vs : list val.
Notation branch :=
(pattern × expr)%type.
Implicit Types br : branch.
Implicit Types brs : list branch.
Notation recursive :=
(binder × binder × expr)%type.
Implicit Types rec : recursive.
Implicit Types 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_of_val v :
to_val (of_val v) = Some v.
Lemma of_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_of_vals vs :
to_vals (of_vals vs) = Some vs.
Lemma of_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
: simpl_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.
countable.
From iris.algebra Require Import
ofe.
From zoo Require Import
prelude.
From zoo.common Require Import
countable
list.
From zoo.common Require Export
binder.
From zoo.language Require Export
location.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types i tag : nat.
Implicit Types n : Z.
Implicit Types l : location.
Implicit Types f x : binder.
Definition block_id :=
positive.
Implicit Types bid : option block_id.
Definition prophet_id :=
positive.
Implicit Types pid : prophet_id.
Variant mutability :=
| Mutable
| ImmutableNongenerative
| ImmutableGenerativeWeak
| ImmutableGenerativeStrong.
Implicit Types mut : mutability.
#[global] Instance mutability_eq_dec : EqDecision mutability :=
ltac:(solve_decision).
#[global] Instance mutability_countable :
Countable mutability.
Variant generativity :=
| Generative bid
| Nongenerative.
Implicit Types 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 Types 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 Types e : expr.
Implicit Types es : list expr.
Implicit Types v : val.
Implicit Types vs : list val.
Notation branch :=
(pattern × expr)%type.
Implicit Types br : branch.
Implicit Types brs : list branch.
Notation recursive :=
(binder × binder × expr)%type.
Implicit Types rec : recursive.
Implicit Types 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_of_val v :
to_val (of_val v) = Some v.
Lemma of_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_of_vals vs :
to_vals (of_vals vs) = Some vs.
Lemma of_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
: simpl_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.