Lvc.IL.ILDB
Require Import List.
Require Export Util Var Val Exp Env Map CSet AutoIndTac IL Bisim Infra.Status Pos.
Set Implicit Arguments.
Inductive bstmt : Type :=
| bstmtLet (e: exp) (s : bstmt)
| bstmtIf (e : exp) (s : bstmt) (t : bstmt)
| bstmtApp (l : lab) (Y:args)
| bstmtReturn (e : exp)
| bstmtExtern (f:external) (Y:args) (s:bstmt)
| bstmtFun (Z: nat) (s : bstmt) (t : bstmt).
Fixpoint exp_eval (E:list val) (e:exp) : option val :=
match e with
| Con v ⇒ Some v
| Var x ⇒ nth_error E x
| UnOp o e ⇒ mdo v <- exp_eval E e;
unop_eval o v
| BinOp o e1 e2 ⇒ mdo v1 <- exp_eval E e1;
mdo v2 <- exp_eval E e2;
binop_eval o v1 v2
end.
Require Export Util Var Val Exp Env Map CSet AutoIndTac IL Bisim Infra.Status Pos.
Set Implicit Arguments.
Inductive bstmt : Type :=
| bstmtLet (e: exp) (s : bstmt)
| bstmtIf (e : exp) (s : bstmt) (t : bstmt)
| bstmtApp (l : lab) (Y:args)
| bstmtReturn (e : exp)
| bstmtExtern (f:external) (Y:args) (s:bstmt)
| bstmtFun (Z: nat) (s : bstmt) (t : bstmt).
Fixpoint exp_eval (E:list val) (e:exp) : option val :=
match e with
| Con v ⇒ Some v
| Var x ⇒ nth_error E x
| UnOp o e ⇒ mdo v <- exp_eval E e;
unop_eval o v
| BinOp o e1 e2 ⇒ mdo v1 <- exp_eval E e1;
mdo v2 <- exp_eval E e2;
binop_eval o v1 v2
end.
Module F.
Inductive block : Type :=
blockI {
block_E : list val;
block_Z : nat;
block_s : bstmt
}.
Definition labenv := list block.
Definition state : Type := (labenv × list val × bstmt)%type.
Inductive step : state → event → state → Prop :=
| stepExp L E e b v
(def:exp_eval E e = Some v)
: step (L, E, bstmtLet e b) EvtTau (L, v::E, b)
| stepIfT L E
e b1 b2 v
(def:exp_eval E e = Some v)
(condTrue: val2bool v = true)
: step (L, E, bstmtIf e b1 b2) EvtTau (L, E, b1)
| stepIfF L E
e b1 b2 v
(def:exp_eval E e = Some v)
(condFalse: val2bool v = false)
: step (L, E, bstmtIf e b1 b2) EvtTau (L, E, b2)
| stepGoto L E l Y blk vl
(Ldef:get L (counted l) blk)
(len:block_Z blk = length Y)
(def:omap (exp_eval E) Y = Some vl) E´
(updOk:(List.app vl (block_E blk)) = E´)
: step (L, E, bstmtApp l Y)
EvtTau
(drop (counted l) L, E´, block_s blk)
| stepLet L E
s Z t
: step (L, E, bstmtFun Z s t) EvtTau (blockI E Z s::L, E, t)
| stepExtern L E f Y s vl v
(def:omap (exp_eval E) Y = Some vl)
: step (L, E, bstmtExtern f Y s)
(EvtExtern (ExternI f vl v))
(L, v::E, s).
Lemma step_internally_deterministic
: internally_deterministic step.
Lemma step_externally_determined
: externally_determined step.
Lemma step_dec
: reddec step.
End F.
Fixpoint exp_idx (symb:list var) (e:exp) : status exp :=
match e with
| Con v ⇒ Success (Con v)
| Var x ⇒ sdo x <- option2status (pos symb x 0) "labIndices: Undeclared variable";
Success (Var x)
| UnOp o e ⇒ sdo e <- exp_idx symb e;
Success (UnOp o e)
| BinOp o e1 e2 ⇒ sdo e1 <- exp_idx symb e1;
sdo e2 <- exp_idx symb e2;
Success (BinOp o e1 e2)
end.
Fixpoint stmt_idx (s:stmt) (symb: list var) : status bstmt :=
match s with
| stmtLet x e s ⇒
sdo e <- exp_idx symb e;
sdo s´ <- (stmt_idx s (x::symb)); Success (bstmtLet e s´)
| stmtIf e s1 s2 ⇒
sdo e <- exp_idx symb e;
sdo s1´ <- (stmt_idx s1 symb);
sdo s2´ <- (stmt_idx s2 symb);
Success (bstmtIf e s1´ s2´)
| stmtApp l Y ⇒
sdo Y <- smap (exp_idx symb) Y;
Success (bstmtApp l Y)
| stmtReturn e ⇒
sdo e <- exp_idx symb e;
Success (bstmtReturn e)
| stmtExtern x f Y s ⇒
sdo Y <- smap (exp_idx symb) Y;
sdo s´ <- (stmt_idx s (x::symb)); Success (bstmtExtern f Y s´)
| stmtFun Z s1 s2 ⇒
sdo s1´ <- stmt_idx s1 (Z ++ symb);
sdo s2´ <- stmt_idx s2 (symb);
Success (bstmtFun (length Z) s1´ s2´)
end.
Definition state_result X (s:X×list val×bstmt) : option val :=
match s with
| (_, E, bstmtReturn e) ⇒ exp_eval E e
| _ ⇒ None
end.
Instance statetype_F : StateType F.state := {
step := F.step;
result := (@state_result F.labenv);
step_dec := F.step_dec;
step_internally_deterministic := F.step_internally_deterministic;
step_externally_determined := F.step_externally_determined
}.
Lemma exp_idx_ok E E´ e e´ (symb:list var)
(Edef:∀ x v, E x = Some v → ∃ n, get symb n x)
(Eagr:∀ x n, pos symb x 0 = Some n → ∃ v, get E´ n v ∧ E x = Some v)
(EQ:exp_idx symb e = Success e´)
: Exp.exp_eval E e = exp_eval E´ e´.
Definition vars_exist (E:onv val) symb := ∀ x v, E x = Some v → ∃ n, get symb n x.
Definition defs_agree symb (E:onv val) E´ :=
∀ x n, pos symb x 0 = Some n → ∃ v, get E´ n v ∧ E x = Some v.
Inductive approx : IL.F.block → F.block → Prop :=
| Approx E (Z:list var) s E´ s´ symb :
stmt_idx s (Z ++ symb) = Success s´
→ vars_exist E symb
→ defs_agree symb E E´
→ approx (IL.F.blockI E Z s) (F.blockI E´ (length Z) s´).
Inductive stmtIdxSim : IL.F.state → F.state → Prop :=
| labIndicesSimI (L:IL.F.labenv) L´ E E´ s s´ symb
(EQ:stmt_idx s symb = Success s´)
(LA:PIR2 approx L L´)
(Edef:vars_exist E symb)
(Eagr:defs_agree symb E E´)
: stmtIdxSim (L, E, s) (L´, E´, s´).
Lemma vars_exist_update (E:onv val) symb x v
: vars_exist E symb
→ vars_exist (E [x <- ⎣v ⎦]) (x :: symb).
Lemma vars_exist_update_list (E:onv val) symb Z vl
: length Z = length vl
→ vars_exist E symb
→ vars_exist (E [Z <-- List.map Some vl]) (Z ++ symb).
Lemma defs_agree_update symb E E´ x v
: defs_agree symb E E´
→ defs_agree (x :: symb) (E [x <- ⎣v ⎦]) (v :: E´).
Lemma defs_agree_update_list (E:onv val) E´ symb Z vl
: length Z = length vl
→ defs_agree symb E E´
→ defs_agree (Z ++ symb) (E [Z <-- List.map Some vl]) (vl ++ E´).
Lemma stmt_idx_sim σ1 σ2
: stmtIdxSim σ1 σ2 → bisim σ1 σ2.
Inductive block : Type :=
blockI {
block_E : list val;
block_Z : nat;
block_s : bstmt
}.
Definition labenv := list block.
Definition state : Type := (labenv × list val × bstmt)%type.
Inductive step : state → event → state → Prop :=
| stepExp L E e b v
(def:exp_eval E e = Some v)
: step (L, E, bstmtLet e b) EvtTau (L, v::E, b)
| stepIfT L E
e b1 b2 v
(def:exp_eval E e = Some v)
(condTrue: val2bool v = true)
: step (L, E, bstmtIf e b1 b2) EvtTau (L, E, b1)
| stepIfF L E
e b1 b2 v
(def:exp_eval E e = Some v)
(condFalse: val2bool v = false)
: step (L, E, bstmtIf e b1 b2) EvtTau (L, E, b2)
| stepGoto L E l Y blk vl
(Ldef:get L (counted l) blk)
(len:block_Z blk = length Y)
(def:omap (exp_eval E) Y = Some vl) E´
(updOk:(List.app vl (block_E blk)) = E´)
: step (L, E, bstmtApp l Y)
EvtTau
(drop (counted l) L, E´, block_s blk)
| stepLet L E
s Z t
: step (L, E, bstmtFun Z s t) EvtTau (blockI E Z s::L, E, t)
| stepExtern L E f Y s vl v
(def:omap (exp_eval E) Y = Some vl)
: step (L, E, bstmtExtern f Y s)
(EvtExtern (ExternI f vl v))
(L, v::E, s).
Lemma step_internally_deterministic
: internally_deterministic step.
Lemma step_externally_determined
: externally_determined step.
Lemma step_dec
: reddec step.
End F.
Fixpoint exp_idx (symb:list var) (e:exp) : status exp :=
match e with
| Con v ⇒ Success (Con v)
| Var x ⇒ sdo x <- option2status (pos symb x 0) "labIndices: Undeclared variable";
Success (Var x)
| UnOp o e ⇒ sdo e <- exp_idx symb e;
Success (UnOp o e)
| BinOp o e1 e2 ⇒ sdo e1 <- exp_idx symb e1;
sdo e2 <- exp_idx symb e2;
Success (BinOp o e1 e2)
end.
Fixpoint stmt_idx (s:stmt) (symb: list var) : status bstmt :=
match s with
| stmtLet x e s ⇒
sdo e <- exp_idx symb e;
sdo s´ <- (stmt_idx s (x::symb)); Success (bstmtLet e s´)
| stmtIf e s1 s2 ⇒
sdo e <- exp_idx symb e;
sdo s1´ <- (stmt_idx s1 symb);
sdo s2´ <- (stmt_idx s2 symb);
Success (bstmtIf e s1´ s2´)
| stmtApp l Y ⇒
sdo Y <- smap (exp_idx symb) Y;
Success (bstmtApp l Y)
| stmtReturn e ⇒
sdo e <- exp_idx symb e;
Success (bstmtReturn e)
| stmtExtern x f Y s ⇒
sdo Y <- smap (exp_idx symb) Y;
sdo s´ <- (stmt_idx s (x::symb)); Success (bstmtExtern f Y s´)
| stmtFun Z s1 s2 ⇒
sdo s1´ <- stmt_idx s1 (Z ++ symb);
sdo s2´ <- stmt_idx s2 (symb);
Success (bstmtFun (length Z) s1´ s2´)
end.
Definition state_result X (s:X×list val×bstmt) : option val :=
match s with
| (_, E, bstmtReturn e) ⇒ exp_eval E e
| _ ⇒ None
end.
Instance statetype_F : StateType F.state := {
step := F.step;
result := (@state_result F.labenv);
step_dec := F.step_dec;
step_internally_deterministic := F.step_internally_deterministic;
step_externally_determined := F.step_externally_determined
}.
Lemma exp_idx_ok E E´ e e´ (symb:list var)
(Edef:∀ x v, E x = Some v → ∃ n, get symb n x)
(Eagr:∀ x n, pos symb x 0 = Some n → ∃ v, get E´ n v ∧ E x = Some v)
(EQ:exp_idx symb e = Success e´)
: Exp.exp_eval E e = exp_eval E´ e´.
Definition vars_exist (E:onv val) symb := ∀ x v, E x = Some v → ∃ n, get symb n x.
Definition defs_agree symb (E:onv val) E´ :=
∀ x n, pos symb x 0 = Some n → ∃ v, get E´ n v ∧ E x = Some v.
Inductive approx : IL.F.block → F.block → Prop :=
| Approx E (Z:list var) s E´ s´ symb :
stmt_idx s (Z ++ symb) = Success s´
→ vars_exist E symb
→ defs_agree symb E E´
→ approx (IL.F.blockI E Z s) (F.blockI E´ (length Z) s´).
Inductive stmtIdxSim : IL.F.state → F.state → Prop :=
| labIndicesSimI (L:IL.F.labenv) L´ E E´ s s´ symb
(EQ:stmt_idx s symb = Success s´)
(LA:PIR2 approx L L´)
(Edef:vars_exist E symb)
(Eagr:defs_agree symb E E´)
: stmtIdxSim (L, E, s) (L´, E´, s´).
Lemma vars_exist_update (E:onv val) symb x v
: vars_exist E symb
→ vars_exist (E [x <- ⎣v ⎦]) (x :: symb).
Lemma vars_exist_update_list (E:onv val) symb Z vl
: length Z = length vl
→ vars_exist E symb
→ vars_exist (E [Z <-- List.map Some vl]) (Z ++ symb).
Lemma defs_agree_update symb E E´ x v
: defs_agree symb E E´
→ defs_agree (x :: symb) (E [x <- ⎣v ⎦]) (v :: E´).
Lemma defs_agree_update_list (E:onv val) E´ symb Z vl
: length Z = length vl
→ defs_agree symb E E´
→ defs_agree (Z ++ symb) (E [Z <-- List.map Some vl]) (vl ++ E´).
Lemma stmt_idx_sim σ1 σ2
: stmtIdxSim σ1 σ2 → bisim σ1 σ2.