1 files changed, 195 insertions, 10 deletions

diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
index 618f3ebe..cf46072f 100644
--- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
+++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
@@ -1,6 +1,7 @@
 (** Syntax and Sequential Semantics of Abstract Basic Blocks.
 *)
-
+Require Import Setoid.
+Require Import ImpPrelude.
 
 Module Type PseudoRegisters.
 
@@ -24,16 +25,8 @@ Parameter op: Type. (* type of operations *)
 
 Parameter genv: Type. (* environment to be used for evaluating an op *)
 
-(* NB: possible generalization
- - relation after/before.
-*)
 Parameter op_eval: genv -> op -> list value -> option value.
 
-Parameter is_constant: op -> bool.
-
-Parameter is_constant_correct: 
-  forall ge o, is_constant o = true -> op_eval ge o nil <> None.
-
 End LangParam.
 
 
@@ -54,6 +47,9 @@ Definition mem := R.t -> value.
 Definition assign (m: mem) (x:R.t) (v: value): mem 
   := fun y => if R.eq_dec x y then v else m y.
 
+
+(** expressions *)
+
 Inductive exp :=
   | PReg (x:R.t)
   | Op (o:op) (le: list_exp)
@@ -140,7 +136,7 @@ Proof.
 Qed.
 
 
-(** A small theory of bblock equality *)
+(** A small theory of bblock simulation *)
 
 (* equalities on bblock outputs *)
 Definition res_eq (om1 om2: option mem): Prop :=
@@ -240,6 +236,195 @@ Qed.
 
 End SEQLANG.
 
+Module Terms.
+
+(** terms in the symbolic evaluation 
+NB: such a term represents the successive computations in one given pseudo-register
+*)
+
+Inductive term :=
+  | Input (x:R.t) (hid:hashcode)
+  | App (o: op) (l: list_term) (hid:hashcode)
+with list_term :=
+  | LTnil (hid:hashcode)
+  | LTcons (t:term) (l:list_term) (hid:hashcode)
+  .
+
+Scheme term_mut := Induction for term Sort Prop
+with list_term_mut := Induction for list_term Sort Prop.
+
+Bind Scope pattern_scope with term.
+Delimit Scope term_scope with term.
+Delimit Scope pattern_scope with pattern.
+
+Notation "[ ]" := (LTnil _) (format "[ ]"): pattern_scope.
+Notation "[ x ]" := (LTcons x [] _): pattern_scope.
+Notation "[ x ; y ; .. ; z ]" := (LTcons x (LTcons y .. (LTcons z (LTnil _) _) .. _) _): pattern_scope.
+Notation "o @ l" := (App o l _) (at level 50, no associativity): pattern_scope.
+
+Import HConsingDefs.
+
+Notation "[ ]" := (LTnil unknown_hid) (format "[ ]"): term_scope.
+Notation "[ x ]" := (LTcons x [] unknown_hid): term_scope.
+Notation "[ x ; y ; .. ; z ]" := (LTcons x (LTcons y .. (LTcons z (LTnil unknown_hid) unknown_hid) .. unknown_hid) unknown_hid): term_scope.
+Notation "o @ l" := (App o l unknown_hid) (at level 50, no associativity): term_scope.
+
+Local Open Scope pattern_scope.
+
+Fixpoint term_eval (ge: genv) (t: term) (m: mem): option value :=
+  match t with
+  | Input x _ => Some (m x)
+  | o @ l =>
+     match list_term_eval ge l m with
+     | Some v => op_eval ge o v
+     | _ => None
+     end
+  end
+with list_term_eval ge (l: list_term) (m: mem) {struct l}: option (list value) :=
+  match l with
+  | [] => Some nil
+  | LTcons t l' _ => 
+    match term_eval ge t m, list_term_eval ge l' m with
+    | Some v, Some lv => Some (v::lv)
+    | _, _ => None
+    end
+  end.
+
+
+Definition term_get_hid (t: term): hashcode :=
+  match t with
+  | Input _ hid => hid
+  | App _ _ hid => hid
+  end.
+
+Definition list_term_get_hid (l: list_term): hashcode :=
+  match l with
+  | LTnil hid => hid
+  | LTcons _ _ hid => hid
+  end.
+
+
+Fixpoint allvalid ge (l: list term) m : Prop :=
+  match l with
+  | nil => True
+  | t::nil => term_eval ge t m <> None
+  | t::l' => term_eval ge t m <> None /\ allvalid ge l' m
+  end. 
+
+Lemma allvalid_extensionality ge (l: list term) m:
+  allvalid ge l m <-> (forall t, List.In t l -> term_eval ge t m <> None).
+Proof.
+  induction l as [|t l]; simpl; try (tauto).
+  destruct l.
+  - intuition (congruence || eauto).
+  - rewrite IHl; clear IHl. intuition (congruence || eauto).
+Qed.
+
+Record pseudo_term: Type := intro_fail {
+  mayfail: list term;
+  effect: term
+}.
+
+Lemma inf_option_equivalence (A:Type) (o1 o2: option A):
+  (o1 <> None -> o1 = o2) <-> (forall m1, o1 = Some m1 -> o2 = Some m1).
+Proof.
+  destruct o1; intuition (congruence || eauto).
+  symmetry; eauto.
+Qed.
+
+Definition match_pt (t: term) (pt: pseudo_term) :=
+      (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) m)
+   /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1).
+
+Lemma intro_fail_correct (l: list term) (t: term) :
+   (forall ge m, term_eval ge t m <> None <-> allvalid ge l m) -> match_pt t (intro_fail l t).
+Proof.
+  unfold match_pt; simpl; intros; intuition congruence.
+Qed.
+Hint Resolve intro_fail_correct: wlp.
+
+Definition identity_fail (t: term):= intro_fail [t] t.
+
+Lemma identity_fail_correct (t: term): match_pt t (identity_fail t).
+Proof.
+  eapply intro_fail_correct; simpl; tauto.
+Qed.
+Global Opaque identity_fail.
+Hint Resolve identity_fail_correct: wlp.
+
+Definition nofail (is_constant: op -> bool) (t: term):=
+    match t with
+    | Input x _ => intro_fail ([])%list t
+    | o @ [] => if is_constant o then (intro_fail ([])%list t) else (identity_fail t)
+    | _ => identity_fail t
+    end.
+
+Lemma nofail_correct (is_constant: op -> bool) t:
+ (forall ge o, is_constant o = true -> op_eval ge o nil <> None) -> match_pt t (nofail is_constant t).
+Proof.
+  destruct t; simpl.
+  + intros; eapply intro_fail_correct; simpl; intuition congruence.
+  + intros; destruct l; simpl; auto with wlp.
+    destruct (is_constant o) eqn:Heqo; simpl; intuition eauto with wlp.
+     eapply intro_fail_correct; simpl; intuition eauto with wlp.
+Qed.
+Global Opaque nofail.
+Hint Resolve nofail_correct: wlp.
+
+Definition term_equiv t1 t2:= forall ge m, term_eval ge t1 m = term_eval ge t2 m.
+
+Global Instance term_equiv_Equivalence : Equivalence term_equiv.
+Proof.
+  split; intro x; unfold term_equiv; intros; eauto.
+  eapply eq_trans; eauto.
+Qed.
+
+Lemma match_pt_term_equiv t1 t2 pt: term_equiv t1 t2 -> match_pt t1 pt -> match_pt t2 pt.
+Proof.
+  unfold match_pt, term_equiv.
+  intros H. intuition; try (erewrite <- H1 in * |- *; congruence).
+  erewrite <- H2; eauto; congruence.
+Qed.
+Hint Resolve match_pt_term_equiv: wlp.
+
+Definition app_fail (l: list term) (pt: pseudo_term): pseudo_term :=
+  {| mayfail := List.rev_append l pt.(mayfail); effect := pt.(effect) |}.
+
+Lemma app_fail_allvalid_correct l pt t1 t2: forall
+  (V1: forall (ge : genv) (m : mem), term_eval ge t1 m <> None <-> allvalid ge (mayfail pt) m)
+  (V2: forall (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail {| mayfail := t1 :: l; effect := t1 |}) m)
+  (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail (app_fail l pt)) m.
+Proof.
+  intros; generalize (V1 ge m) (V2 ge m); rewrite !allvalid_extensionality; simpl. clear V1 V2.
+  intuition subst.
+  + rewrite rev_append_rev, in_app_iff, <- in_rev in H3. destruct H3; eauto.
+  + eapply H3; eauto.
+    intros. intuition subst.
+    * eapply H2; eauto. intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff; auto.
+    * intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff, <- in_rev; auto.
+Qed.
+Local Hint Resolve app_fail_allvalid_correct: core.
+
+Lemma app_fail_correct l pt t1 t2: 
+  match_pt t1 pt -> 
+  match_pt t2 {| mayfail:=t1::l; effect:=t1 |} ->
+  match_pt t2 (app_fail l pt).
+Proof.
+  unfold match_pt in * |- *; intros (V1 & E1) (V2 & E2); split; intros ge m; try (eauto; fail).
+Qed.
+Extraction Inline app_fail.
+
+Import ImpCore.Notations.
+Local Open Scope impure_scope.
+
+Record reduction:= {
+  result:> term -> ?? pseudo_term;
+  result_correct: forall t, WHEN result t ~> pt THEN match_pt t pt;
+}.
+Hint Resolve result_correct: wlp.
+
+End Terms.
+
 End MkSeqLanguage.