Lvc.IL.ILN
Require Import List.
Require Export Util Var Val Exp Env Map CSet AutoIndTac IL Bisim Infra.Status Pos.
Set Implicit Arguments.
Inductive nstmt : Type :=
| nstmtLet (x : var) (e: exp) (s : nstmt)
| nstmtIf (e : exp) (s : nstmt) (t : nstmt)
| nstmtApp (l : lab) (Y:args)
| nstmtReturn (e : exp)
| nstmtExtern (x : var) (f:external) (Y:args) (s:nstmt)
| nstmtFun (l : lab) (Z:params) (s : nstmt) (t : nstmt).
Fixpoint freeVars (s:nstmt) : set var :=
match s with
| nstmtLet x e s0 ⇒ (freeVars s0 \ {{x}}) ∪ Exp.freeVars e
| nstmtIf e s1 s2 ⇒ freeVars s1 ∪ freeVars s2 ∪ Exp.freeVars e
| nstmtApp l Y ⇒ list_union (List.map Exp.freeVars Y)
| nstmtReturn e ⇒ Exp.freeVars e
| nstmtExtern x f Y s ⇒ (freeVars s \ {{x}}) ∪ list_union (List.map Exp.freeVars Y)
| nstmtFun l Z s1 s2 ⇒ (freeVars s1 \ of_list Z) ∪ freeVars s2
end.
Require Export Util Var Val Exp Env Map CSet AutoIndTac IL Bisim Infra.Status Pos.
Set Implicit Arguments.
Inductive nstmt : Type :=
| nstmtLet (x : var) (e: exp) (s : nstmt)
| nstmtIf (e : exp) (s : nstmt) (t : nstmt)
| nstmtApp (l : lab) (Y:args)
| nstmtReturn (e : exp)
| nstmtExtern (x : var) (f:external) (Y:args) (s:nstmt)
| nstmtFun (l : lab) (Z:params) (s : nstmt) (t : nstmt).
Fixpoint freeVars (s:nstmt) : set var :=
match s with
| nstmtLet x e s0 ⇒ (freeVars s0 \ {{x}}) ∪ Exp.freeVars e
| nstmtIf e s1 s2 ⇒ freeVars s1 ∪ freeVars s2 ∪ Exp.freeVars e
| nstmtApp l Y ⇒ list_union (List.map Exp.freeVars Y)
| nstmtReturn e ⇒ Exp.freeVars e
| nstmtExtern x f Y s ⇒ (freeVars s \ {{x}}) ∪ list_union (List.map Exp.freeVars Y)
| nstmtFun l Z s1 s2 ⇒ (freeVars s1 \ of_list Z) ∪ freeVars s2
end.
Module F.
Inductive block : Type :=
blockI {
block_L : onv block;
block_E : onv val;
block_F : lab × params × nstmt
}.
Definition labenv := onv block.
Definition state : Type := (labenv × onv val × nstmt)%type.
Inductive step : state → event → state → Prop :=
| nstepExp L E x e b v
(def:exp_eval E e = Some v)
: step (L, E, nstmtLet x e b) EvtTau (L, E[x<-Some v], b)
| nstepIfT L E
(e:exp) b1 b2 v
(def:exp_eval E e = Some v)
(condTrue: val2bool v = true)
: step (L, E, nstmtIf e b1 b2) EvtTau (L, E, b1)
| nstepIfF L E
(e:exp) b1 b2 v
(def:exp_eval E e = Some v)
(condFalse:val2bool v = false)
: step (L, E, nstmtIf e b1 b2) EvtTau (L, E, b2)
| nstepGoto (L:labenv) (E:onv val) (l l´:lab) Y Z (s:nstmt) L´ E´
(len:length Z = length Y)
(lEQ:l = l´)
(Ldef:L (counted l) = Some (blockI L´ E´ (l´,Z,s))) E´´ vl
(def:omap (exp_eval E) Y = Some vl)
(updOk:E´[Z <-- List.map Some vl] = E´´)
: step (L, E, nstmtApp l Y)
EvtTau
(L´[(counted l) <- Some (blockI L´ E´ (l,Z,s))], E´´, s)
| stepLet L E f s Z t
: step (L, E, nstmtFun f Z s t) EvtTau (L[counted f <- Some (blockI L E (f,Z,s))], E, t)
| stepExtern L E x f Y s vl v
(def:omap (exp_eval E) Y = Some vl)
: step (L, E, nstmtExtern x f Y s)
(EvtExtern (ExternI f vl v))
(L, E[x <- Some v], s).
Lemma step_internally_deterministic :
internally_deterministic step.
Lemma step_dec
: reddec step.
End F.
Inductive block : Type :=
blockI {
block_L : onv block;
block_E : onv val;
block_F : lab × params × nstmt
}.
Definition labenv := onv block.
Definition state : Type := (labenv × onv val × nstmt)%type.
Inductive step : state → event → state → Prop :=
| nstepExp L E x e b v
(def:exp_eval E e = Some v)
: step (L, E, nstmtLet x e b) EvtTau (L, E[x<-Some v], b)
| nstepIfT L E
(e:exp) b1 b2 v
(def:exp_eval E e = Some v)
(condTrue: val2bool v = true)
: step (L, E, nstmtIf e b1 b2) EvtTau (L, E, b1)
| nstepIfF L E
(e:exp) b1 b2 v
(def:exp_eval E e = Some v)
(condFalse:val2bool v = false)
: step (L, E, nstmtIf e b1 b2) EvtTau (L, E, b2)
| nstepGoto (L:labenv) (E:onv val) (l l´:lab) Y Z (s:nstmt) L´ E´
(len:length Z = length Y)
(lEQ:l = l´)
(Ldef:L (counted l) = Some (blockI L´ E´ (l´,Z,s))) E´´ vl
(def:omap (exp_eval E) Y = Some vl)
(updOk:E´[Z <-- List.map Some vl] = E´´)
: step (L, E, nstmtApp l Y)
EvtTau
(L´[(counted l) <- Some (blockI L´ E´ (l,Z,s))], E´´, s)
| stepLet L E f s Z t
: step (L, E, nstmtFun f Z s t) EvtTau (L[counted f <- Some (blockI L E (f,Z,s))], E, t)
| stepExtern L E x f Y s vl v
(def:omap (exp_eval E) Y = Some vl)
: step (L, E, nstmtExtern x f Y s)
(EvtExtern (ExternI f vl v))
(L, E[x <- Some v], s).
Lemma step_internally_deterministic :
internally_deterministic step.
Lemma step_dec
: reddec step.
End F.
Module I.
Inductive block : Type :=
blockI {
block_L : onv block;
block_F : lab × params × nstmt
}.
Definition labenv := onv block.
Definition state : Type := (labenv × onv val × nstmt)%type.
Definition labenv_empty : labenv := fun _ ⇒ None.
Inductive step : state → event → state → Prop :=
| nstepExp L E x e b v
(def:exp_eval E e = Some v)
: step (L, E, nstmtLet x e b) EvtTau (L, E[x<-Some v], b)
| nstepIfT L E
(e:exp) b1 b2 v
(def:exp_eval E e = Some v)
(condTrue: val2bool v = true)
: step (L, E, nstmtIf e b1 b2) EvtTau (L, E, b1)
| nstepIfF L E
(e:exp) b1 b2 v
(def:exp_eval E e = Some v)
(condFalse:val2bool v = false)
: step (L, E, nstmtIf e b1 b2) EvtTau (L, E, b2)
| nstepGoto (L:labenv) (E:onv val) (l l´:lab) Y Z (s:nstmt) L´ vl
(len:length Z = length Y)
(lEQ: l = l´)
(Ldef:L (counted l) = Some (blockI L´ (l´,Z,s))) E´´
(def:omap (exp_eval E) Y = Some vl)
(updOk:E [Z <-- List.map Some vl] = E´´)
: step (L, E, nstmtApp l Y)
EvtTau
(L´[(counted l) <- Some (blockI L´ (l,Z,s))], E´´, s)
| stepLet L E f s Z t
: step (L, E, nstmtFun f Z s t)
EvtTau
(L[counted f <- Some (blockI L (f,Z,s))], E, t)
| stepExtern L E x f Y s vl v
(def:omap (exp_eval E) Y = Some vl)
: step (L, E, nstmtExtern x f Y s)
(EvtExtern (ExternI f vl v))
(L, E[x <- Some v], s).
Lemma step_internally_deterministic :
internally_deterministic step.
Lemma step_externally_determined
: externally_determined step.
Lemma step_dec
: reddec step.
End I.
Fixpoint labIndices (s:nstmt) (symb: list lab) : status stmt :=
match s with
| nstmtLet x e s ⇒ sdo s´ <- (labIndices s symb); Success (stmtLet x e s´)
| nstmtIf x s1 s2 ⇒
sdo s1´ <- (labIndices s1 symb);
sdo s2´ <- (labIndices s2 symb);
Success (stmtIf x s1´ s2´)
| nstmtApp l Y ⇒
sdo f <- option2status (pos symb l 0) "labIndices: Undeclared function" ; Success (stmtApp (LabI f) Y)
| nstmtReturn x ⇒ Success (stmtReturn x)
| nstmtExtern x f Y s ⇒
sdo s´ <- (labIndices s symb); Success (stmtExtern x f Y s´)
| nstmtFun l Z s1 s2 ⇒
sdo s1´ <- labIndices s1 (l::symb);
sdo s2´ <- labIndices s2 (l::symb);
Success (stmtFun Z s1´ s2´)
end.
Definition state_result X (s:X×onv val×nstmt) : option val :=
match s with
| (_, E, nstmtReturn e) ⇒ exp_eval E e
| _ ⇒ None
end.
Instance statetype_I : StateType I.state := {
step := I.step;
result := (@state_result I.labenv);
step_dec := I.step_dec;
step_internally_deterministic := I.step_internally_deterministic;
step_externally_determined := I.step_externally_determined
}.
Inductive lab_approx : list lab → env (option I.block) → list IL.I.block → Prop :=
Lai symb L L´
(LEQ: ∀ f f´ s Z Lb,
L (counted f) = Some (I.blockI Lb (f´,Z,s))
→ ∃ i s´,
get L´ i (IL.I.blockI Z s´)
∧ labIndices s (drop i symb) = Success s´
∧ pos symb f 0 = Some i ∧ lab_approx (drop (S i) symb) (Lb ) (drop (S i) L´)
∧ (∀ l b, Lb (counted l) = Some b → fst (fst (I.block_F b)) = l)
∧ (∀ f i´ k, pos (drop (S i) symb) f k = Some i´ → Lb (counted f) ≠ None)
∧ f = f´)
: lab_approx symb L L´.
Inductive labIndicesSim : I.state → IL.I.state → Prop :=
| labIndicesSimI (L:env (option I.block)) L´ E s s´ symb
(EQ:labIndices s symb = Success s´)
(LA:lab_approx symb L L´)
(LL:∀ l b, L (counted l) = Some b → fst (fst (I.block_F b)) = l)
(EX:∀ f i k, pos symb f k = Some i → L (counted f) ≠ None)
: labIndicesSim (L, E, s) (L´, E, s´).
Lemma pos_drop_eq symb (l:lab) x
: pos symb l 0 = Some x
→ drop x symb = l::tl (drop x symb).
Lemma pos_plus symb (f:lab) n i
: pos symb f 0 = Some (n + i)
→ pos (drop n symb) f 0 = Some i.
Lemma labIndicesSim_sim σ1 σ2
: labIndicesSim σ1 σ2 → bisim σ1 σ2.
Inductive block : Type :=
blockI {
block_L : onv block;
block_F : lab × params × nstmt
}.
Definition labenv := onv block.
Definition state : Type := (labenv × onv val × nstmt)%type.
Definition labenv_empty : labenv := fun _ ⇒ None.
Inductive step : state → event → state → Prop :=
| nstepExp L E x e b v
(def:exp_eval E e = Some v)
: step (L, E, nstmtLet x e b) EvtTau (L, E[x<-Some v], b)
| nstepIfT L E
(e:exp) b1 b2 v
(def:exp_eval E e = Some v)
(condTrue: val2bool v = true)
: step (L, E, nstmtIf e b1 b2) EvtTau (L, E, b1)
| nstepIfF L E
(e:exp) b1 b2 v
(def:exp_eval E e = Some v)
(condFalse:val2bool v = false)
: step (L, E, nstmtIf e b1 b2) EvtTau (L, E, b2)
| nstepGoto (L:labenv) (E:onv val) (l l´:lab) Y Z (s:nstmt) L´ vl
(len:length Z = length Y)
(lEQ: l = l´)
(Ldef:L (counted l) = Some (blockI L´ (l´,Z,s))) E´´
(def:omap (exp_eval E) Y = Some vl)
(updOk:E [Z <-- List.map Some vl] = E´´)
: step (L, E, nstmtApp l Y)
EvtTau
(L´[(counted l) <- Some (blockI L´ (l,Z,s))], E´´, s)
| stepLet L E f s Z t
: step (L, E, nstmtFun f Z s t)
EvtTau
(L[counted f <- Some (blockI L (f,Z,s))], E, t)
| stepExtern L E x f Y s vl v
(def:omap (exp_eval E) Y = Some vl)
: step (L, E, nstmtExtern x f Y s)
(EvtExtern (ExternI f vl v))
(L, E[x <- Some v], s).
Lemma step_internally_deterministic :
internally_deterministic step.
Lemma step_externally_determined
: externally_determined step.
Lemma step_dec
: reddec step.
End I.
Fixpoint labIndices (s:nstmt) (symb: list lab) : status stmt :=
match s with
| nstmtLet x e s ⇒ sdo s´ <- (labIndices s symb); Success (stmtLet x e s´)
| nstmtIf x s1 s2 ⇒
sdo s1´ <- (labIndices s1 symb);
sdo s2´ <- (labIndices s2 symb);
Success (stmtIf x s1´ s2´)
| nstmtApp l Y ⇒
sdo f <- option2status (pos symb l 0) "labIndices: Undeclared function" ; Success (stmtApp (LabI f) Y)
| nstmtReturn x ⇒ Success (stmtReturn x)
| nstmtExtern x f Y s ⇒
sdo s´ <- (labIndices s symb); Success (stmtExtern x f Y s´)
| nstmtFun l Z s1 s2 ⇒
sdo s1´ <- labIndices s1 (l::symb);
sdo s2´ <- labIndices s2 (l::symb);
Success (stmtFun Z s1´ s2´)
end.
Definition state_result X (s:X×onv val×nstmt) : option val :=
match s with
| (_, E, nstmtReturn e) ⇒ exp_eval E e
| _ ⇒ None
end.
Instance statetype_I : StateType I.state := {
step := I.step;
result := (@state_result I.labenv);
step_dec := I.step_dec;
step_internally_deterministic := I.step_internally_deterministic;
step_externally_determined := I.step_externally_determined
}.
Inductive lab_approx : list lab → env (option I.block) → list IL.I.block → Prop :=
Lai symb L L´
(LEQ: ∀ f f´ s Z Lb,
L (counted f) = Some (I.blockI Lb (f´,Z,s))
→ ∃ i s´,
get L´ i (IL.I.blockI Z s´)
∧ labIndices s (drop i symb) = Success s´
∧ pos symb f 0 = Some i ∧ lab_approx (drop (S i) symb) (Lb ) (drop (S i) L´)
∧ (∀ l b, Lb (counted l) = Some b → fst (fst (I.block_F b)) = l)
∧ (∀ f i´ k, pos (drop (S i) symb) f k = Some i´ → Lb (counted f) ≠ None)
∧ f = f´)
: lab_approx symb L L´.
Inductive labIndicesSim : I.state → IL.I.state → Prop :=
| labIndicesSimI (L:env (option I.block)) L´ E s s´ symb
(EQ:labIndices s symb = Success s´)
(LA:lab_approx symb L L´)
(LL:∀ l b, L (counted l) = Some b → fst (fst (I.block_F b)) = l)
(EX:∀ f i k, pos symb f k = Some i → L (counted f) ≠ None)
: labIndicesSim (L, E, s) (L´, E, s´).
Lemma pos_drop_eq symb (l:lab) x
: pos symb l 0 = Some x
→ drop x symb = l::tl (drop x symb).
Lemma pos_plus symb (f:lab) n i
: pos symb f 0 = Some (n + i)
→ pos (drop n symb) f 0 = Some i.
Lemma labIndicesSim_sim σ1 σ2
: labIndicesSim σ1 σ2 → bisim σ1 σ2.