renommages abstract_bb

  Resource -> PseudoReg
  macro -> inst

5 files changed, 156 insertions, 156 deletions

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index a98ab53a..7043bd32 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -542,7 +542,7 @@ Definition inv_ppos (p: R.t) : option preg :=
 
 Notation "a @ b" := (Econs a b) (at level 102, right associativity).
 
-Definition trans_control (ctl: control) : macro :=
+Definition trans_control (ctl: control) : inst :=
   match ctl with
   | Pret => [(#PC, Name (#RA))]
   | Pcall s => [(#RA, Name (#PC)); (#PC, Op (Arith (OArithR (Ploadsymbol s Ptrofs.zero))) Enil)]
@@ -558,14 +558,14 @@ Definition trans_control (ctl: control) : macro :=
   | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)]
   end.
 
-Definition trans_exit (ex: option control) : L.macro :=
+Definition trans_exit (ex: option control) : L.inst :=
   match ex with
   | None => []
   | Some ctl => trans_control ctl
   end
 .
 
-Definition trans_arith (ai: ar_instruction) : macro :=
+Definition trans_arith (ai: ar_instruction) : inst :=
   match ai with
   | PArithR n d => [(#d, Op (Arith (OArithR n)) Enil)]
   | PArithRR n d s => [(#d, Op (Arith (OArithRR n)) (Name (#s) @ Enil))]
@@ -582,7 +582,7 @@ Definition trans_arith (ai: ar_instruction) : macro :=
   end.
 
 
-Definition trans_basic (b: basic) : macro :=
+Definition trans_basic (b: basic) : inst :=
   match b with
   | PArith ai => trans_arith ai
   | PLoadRRO n d a ofs => [(#d, Op (Load (OLoadRRO n ofs)) (Name (#a) @ Name pmem @ Enil))]
@@ -603,13 +603,13 @@ Definition trans_basic (b: basic) : macro :=
   | Pnop => []
   end.
 
-Fixpoint trans_body (b: list basic) : list L.macro :=
+Fixpoint trans_body (b: list basic) : list L.inst :=
   match b with
   | nil => nil
   | b :: lb => (trans_basic b) :: (trans_body lb)
   end.
 
-Definition trans_pcincr (sz: Z) (k: L.macro) := (#PC, Op (Control (OIncremPC sz)) (Name (#PC) @ Enil)) :: k.
+Definition trans_pcincr (sz: Z) (k: L.inst) := (#PC, Op (Control (OIncremPC sz)) (Name (#PC) @ Enil)) :: k.
 
 Definition trans_block (b: Asmblock.bblock) : L.bblock :=
   trans_body (body b) ++ (trans_pcincr (size b) (trans_exit (exit b)) :: nil).
@@ -686,7 +686,7 @@ Lemma exec_app_some:
 Proof.
   induction c.
   - simpl. intros. congruence.
-  - intros. simpl in *. destruct (macro_run _ _ _ _); auto. eapply IHc; eauto. discriminate.
+  - intros. simpl in *. destruct (inst_run _ _ _ _); auto. eapply IHc; eauto. discriminate.
 Qed.
 
 Lemma exec_app_none:
@@ -696,7 +696,7 @@ Lemma exec_app_none:
 Proof.
   induction c.
   - simpl. discriminate.
-  - intros. simpl. simpl in H. destruct (macro_run _ _ _ _); auto.
+  - intros. simpl. simpl in H. destruct (inst_run _ _ _ _); auto.
 Qed.
 
 Lemma trans_arith_correct:
@@ -704,7 +704,7 @@ Lemma trans_arith_correct:
   exec_arith_instr ge i rs = rs' ->
   match_states (State rs m) s ->
   exists s',
-     macro_run (Genv ge fn) (trans_arith i) s s = Some s'
+     inst_run (Genv ge fn) (trans_arith i) s s = Some s'
   /\ match_states (State rs' m) s'.
 Proof.
   intros. unfold exec_arith_instr in H. destruct i.
@@ -793,12 +793,12 @@ Lemma forward_simu_basic:
   exec_basic_instr ge b rs m = Next rs' m' ->
   match_states (State rs m) s ->
   exists s',
-     macro_run (Genv ge fn) (trans_basic b) s s = Some s'
+     inst_run (Genv ge fn) (trans_basic b) s s = Some s'
   /\ match_states (State rs' m') s'.
 Proof.
   intros. destruct b.
 (* Arith *)
-  - simpl in H. inv H. simpl macro_run. eapply trans_arith_correct; eauto.
+  - simpl in H. inv H. simpl inst_run. eapply trans_arith_correct; eauto.
 (* Load *)
   - simpl in H. destruct i.
     unfold exec_load in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate;
@@ -1040,11 +1040,11 @@ Proof.
     eapply IHc; eauto.
 Qed.
 
-Lemma exec_trans_pcincr_exec_macrorun:
+Lemma exec_trans_pcincr_exec_instrun:
   forall rs m s b k,
   match_states (State rs m) s ->
   exists s',
-     macro_run Ge ((# PC, Op (OIncremPC (size b)) (Name (# PC) @ Enil)) :: k) s s = macro_run Ge k s' s
+     inst_run Ge ((# PC, Op (OIncremPC (size b)) (Name (# PC) @ Enil)) :: k) s s = inst_run Ge k s' s
   /\ match_states (State (nextblock b rs) m) s'.
 Proof.
   intros. inv H. eexists. split. simpl. pose (H1 PC); simpl in e; rewrite e. destruct Ge. simpl. eapply eq_refl.
@@ -1053,9 +1053,9 @@ Proof.
   - intros rr; destruct rr; Simpl.
 Qed.
 
-Lemma macro_run_trans_exit_noold:
+Lemma inst_run_trans_exit_noold:
   forall ex s s' s'',
-  macro_run Ge (trans_exit ex) s s' = macro_run Ge (trans_exit ex) s s''.
+  inst_run Ge (trans_exit ex) s s' = inst_run Ge (trans_exit ex) s s''.
 Proof.
   intros. destruct ex.
   - destruct c; destruct i; reflexivity.
@@ -1070,10 +1070,10 @@ Lemma exec_trans_pcincr_exec:
   /\ match_states (State (nextblock b rs) m) s'.
 Proof.
   intros.
-  exploit exec_trans_pcincr_exec_macrorun; eauto.
+  exploit exec_trans_pcincr_exec_instrun; eauto.
   intros (s' & MRUN & MS).
   eexists. split. unfold exec. unfold trans_pcincr. unfold run. rewrite MRUN.
-  erewrite macro_run_trans_exit_noold; eauto.
+  erewrite inst_run_trans_exit_noold; eauto.
   assumption.
 Qed.
 
@@ -1603,7 +1603,7 @@ End SECT.
 
 (** Parallelizability of a bblock *)
 
-Module PChk := ParallelChecks L PosResourceSet.
+Module PChk := ParallelChecks L PosPseudoRegSet.
 
 Definition bblock_para_check (p: Asmblock.bblock) : bool :=
   PChk.is_parallelizable (trans_block p).
@@ -1637,7 +1637,7 @@ Lemma trans_arith_par_correct ge fn rsr mr sr rsw mw sw rsw' i:
   match_states (State rsw mw) sw ->
   parexec_arith_instr ge i rsr rsw = rsw' ->
   exists sw',
-     macro_prun Ge (trans_arith i) sw sr sr = Some sw'
+     inst_prun Ge (trans_arith i) sw sr sr = Some sw'
   /\ match_states (State rsw' mw) sw'.
 Proof.
   intros GENV MSR MSW PARARITH. subst. inv MSR. inv MSW.
@@ -1720,7 +1720,7 @@ Theorem forward_simu_par_wio_basic_gen ge fn rsr rsw mr mw sr sw bi:
   Ge = Genv ge fn ->
   match_states (State rsr mr) sr ->
   match_states (State rsw mw) sw ->
-  match_outcome (parexec_basic_instr ge bi rsr rsw mr mw) (macro_prun Ge (trans_basic bi) sw sr sr).
+  match_outcome (parexec_basic_instr ge bi rsr rsw mr mw) (inst_prun Ge (trans_basic bi) sw sr sr).
 Proof.
   intros GENV MSR MSW; inversion MSR as (H & H0); inversion MSW as (H1 & H2).
   destruct bi; simpl.
@@ -1778,7 +1778,7 @@ Theorem forward_simu_par_wio_basic ge fn rsr rsw mr mw sr sw bi rsw' mw':
   match_states (State rsw mw) sw ->
   parexec_basic_instr ge bi rsr rsw mr mw = Next rsw' mw' ->
   exists sw',
-     macro_prun Ge (trans_basic bi) sw sr sr = Some sw'
+     inst_prun Ge (trans_basic bi) sw sr sr = Some sw'
   /\ match_states (State rsw' mw') sw'.
 Proof.
   intros H H0 H1 H2; exploit forward_simu_par_wio_basic_gen; [ eapply H | eapply H0 | eapply H1 | erewrite H2 ].
@@ -1790,7 +1790,7 @@ Theorem forward_simu_par_wio_basic_Stuck ge fn rsr rsw mr mw sr sw bi:
   match_states (State rsr mr) sr ->
   match_states (State rsw mw) sw ->
   parexec_basic_instr ge bi rsr rsw mr mw = Stuck ->
-  macro_prun Ge (trans_basic bi) sw sr sr = None.
+  inst_prun Ge (trans_basic bi) sw sr sr = None.
 Proof.
   intros H H0 H1 H2; exploit forward_simu_par_wio_basic_gen; [ eapply H | eapply H0 | eapply H1 | erewrite H2 ].
   simpl; auto.
@@ -1826,7 +1826,7 @@ Theorem forward_simu_par_control ge fn rsr rsw mr mw sr sw sz rs' ex m':
   match_states (State rsw mw) sw ->
   parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) rsw mw = Next rs' m' ->
   exists s',
-     macro_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = Some s'
+     inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = Some s'
   /\ match_states (State rs' m') s'.
 Proof.
   intros GENV MSR MSW H0.
@@ -1937,7 +1937,7 @@ Lemma forward_simu_par_control_Stuck ge fn rsr rsw mr mw sr sw sz ex:
   match_states (State rsr mr) sr ->
   match_states (State rsw mw) sw ->
   parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) rsw mw = Stuck ->
-  macro_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = None.
+  inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = None.
 Proof.
   intros GENV MSR MSW H0. inv MSR; inv MSW. destruct ex as [ctl|]; try discriminate.
   destruct ctl; destruct i; try discriminate; try (simpl; reflexivity).
diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
index 904fb72c..0bab9426 100644
--- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
+++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
@@ -2,19 +2,19 @@
 *)
 
 
-Module Type ResourceNames.
+Module Type PseudoRegisters.
 
 Parameter t: Type.
 
 Parameter eq_dec: forall (x y: t), { x = y } + { x<>y }.
 
-End ResourceNames.
+End PseudoRegisters.
 
 
 (** * Parameters of the language of Basic Blocks *)
 Module Type LangParam.
 
-Declare Module R: ResourceNames.
+Declare Module R: PseudoRegisters.
 
 Parameter value: Type.
 
@@ -85,25 +85,25 @@ with list_exp_eval (le: list_exp) (m old: mem): option (list value) :=
   | LOld le => list_exp_eval le old old
   end.
 
-Definition macro := list (R.t * exp). (* = a sequence of assignments *) 
+Definition inst := list (R.t * exp). (* = a sequence of assignments *) 
 
-Fixpoint macro_run (i: macro) (m old: mem): option mem :=
+Fixpoint inst_run (i: inst) (m old: mem): option mem :=
   match i with
   | nil => Some m
   | (x, e)::i' =>
      match exp_eval e m old with
-     | Some v' => macro_run i' (assign m x v') old
+     | Some v' => inst_run i' (assign m x v') old
      | None => None
      end
   end.
 
-Definition bblock := list macro.
+Definition bblock := list inst.
 
 Fixpoint run (p: bblock) (m: mem): option mem :=
   match p with
   | nil => Some m
   | i::p' =>
-     match macro_run i m m with
+     match inst_run i m m with
      | Some m' => run p' m'
      | None => None
      end
@@ -166,10 +166,10 @@ Qed.
 Definition bblock_equiv (p1 p2: bblock): Prop
   := forall m, res_eq (run p1 m) (run p2 m).
 
-Lemma alt_macro_equiv_refl i old1 old2: 
+Lemma alt_inst_equiv_refl i old1 old2: 
   (forall x, old1 x = old2 x) ->
   forall m1 m2, (forall x, m1 x = m2 x) -> 
-  res_eq (macro_run i m1 old1) (macro_run i m2 old2).
+  res_eq (inst_run i m1 old1) (inst_run i m2 old2).
 Proof.
   intro H; induction i as [ | [x e]]; simpl; eauto.
   intros m1 m2 H1. erewrite exp_equiv; eauto.
@@ -181,9 +181,9 @@ Qed.
 Lemma alt_bblock_equiv_refl p: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p m1) (run p m2).
 Proof.
   induction p as [ | i p']; simpl; eauto.
-  intros m1 m2 H; lapply (alt_macro_equiv_refl i m1 m2); auto.
+  intros m1 m2 H; lapply (alt_inst_equiv_refl i m1 m2); auto.
   intros X; lapply (X m1 m2); auto; clear X.
-  destruct (macro_run i m1 m1); simpl.
+  destruct (inst_run i m1 m1); simpl.
   - intros [m3 [H1 H2]]; rewrite H1; simpl; auto.
   - intros H1; rewrite H1; simpl; auto.
 Qed.
diff --git a/mppa_k1c/abstractbb/DepTreeTheory.v b/mppa_k1c/abstractbb/DepTreeTheory.v
index 353e9160..4d5c71b3 100644
--- a/mppa_k1c/abstractbb/DepTreeTheory.v
+++ b/mppa_k1c/abstractbb/DepTreeTheory.v
@@ -9,9 +9,9 @@ Require Setoid. (* in order to rewrite <-> *)
 Require Export AbstractBasicBlocksDef.
 
 
-Module Type ResourceDictionary.
+Module Type PseudoRegDictionary.
 
-Declare Module R: ResourceNames.
+Declare Module R: PseudoRegisters.
 
 Parameter t: Type -> Type.
 
@@ -30,12 +30,12 @@ Parameter empty: forall {A}, t A.
 Parameter empty_spec: forall A x,
   get (empty (A:=A)) x = None.
 
-End ResourceDictionary.
+End PseudoRegDictionary.
 
 
 (** * Computations of "bblock" Dependencies and application to the equality test *)
 
-Module DepTree (L: SeqLanguage) (Dict: ResourceDictionary with Module R:=L.LP.R).
+Module DepTree (L: SeqLanguage) (Dict: PseudoRegDictionary with Module R:=L.LP.R).
 
 Export L.
 Export LP.
@@ -142,21 +142,21 @@ Proof.
   eauto.
 Qed.
 
-Fixpoint macro_deps (i: macro) (d old: deps): deps :=
+Fixpoint inst_deps (i: inst) (d old: deps): deps :=
   match i with
   | nil => d
   | (x, e)::i' =>
      let t0:=deps_get d x in
      let t1:=exp_tree e d old in
      let v':=if failsafe t0 then t1 else (Terase t1 t0) in
-     macro_deps i' (Dict.set d x v') old
+     inst_deps i' (Dict.set d x v') old
   end.
 
 Fixpoint bblock_deps_rec (p: bblock) (d: deps): deps :=
   match p with
   | nil => d
   | i::p' =>
-     let d':=macro_deps i d d in
+     let d':=inst_deps i d d in
      bblock_deps_rec p' d'
   end.
 
@@ -177,9 +177,9 @@ Proof.
   - intros; erewrite IHe, IHe0; eauto. 
 Qed.
 
-Lemma tree_eval_macro_abort i m0 x old: forall d,
+Lemma tree_eval_inst_abort i m0 x old: forall d,
     tree_eval (deps_get d x) m0 = None ->
-    tree_eval (deps_get (macro_deps i d old) x) m0 = None.
+    tree_eval (deps_get (inst_deps i d old) x) m0 = None.
 Proof.
   induction i as [|[y e] i IHi]; simpl; auto.
   intros d H; erewrite IHi; eauto. clear IHi.
@@ -197,15 +197,15 @@ Lemma tree_eval_abort p m0 x: forall d,
 Proof.
   induction p; simpl; auto.
   intros d H; erewrite IHp; eauto. clear IHp.
-  eapply tree_eval_macro_abort; eauto.
+  eapply tree_eval_inst_abort; eauto.
 Qed.
 
-Lemma tree_eval_macro_Some_correct1 i m0 old od: 
+Lemma tree_eval_inst_Some_correct1 i m0 old od: 
   (forall x, tree_eval (deps_get od x) m0 = Some (old x)) ->
   forall (m1 m2: mem) d, 
-  macro_run ge i m1 old = Some m2 -> 
+  inst_run ge i m1 old = Some m2 -> 
   (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
-  (forall x, tree_eval (deps_get (macro_deps i d od) x) m0 = Some (m2 x)).
+  (forall x, tree_eval (deps_get (inst_deps i d od) x) m0 = Some (m2 x)).
 Proof.
   intro X; induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H.
   - inversion_clear H; eauto.
@@ -222,7 +222,7 @@ Proof.
     + inversion H. 
 Qed.
 
-Local Hint Resolve tree_eval_macro_Some_correct1 tree_eval_abort.
+Local Hint Resolve tree_eval_inst_Some_correct1 tree_eval_abort.
 
 Lemma tree_eval_Some_correct1 p m0: forall (m1 m2: mem) d, 
  run ge p m1 = Some m2 -> 
@@ -232,7 +232,7 @@ Proof.
   induction p as [ | i p]; simpl; intros m1 m2 d H.
   - inversion_clear H; eauto.
   - intros H0 x0.
-    remember (macro_run ge i m1 m1) as om.
+    remember (inst_run ge i m1 m1) as om.
     destruct om.
     + refine (IHp _ _ _ _ _ _); eauto.
     + inversion H. 
@@ -246,10 +246,10 @@ Proof.
   intros; autorewrite with dict_rw; simpl; eauto.
 Qed.
 
-Lemma tree_eval_macro_None_correct i m0 old od: 
+Lemma tree_eval_inst_None_correct i m0 old od: 
   (forall x, tree_eval (deps_get od x) m0 = Some (old x)) ->
   forall m1 d,  (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
-  macro_run ge i m1 old = None <-> exists x, tree_eval (deps_get (macro_deps i d od) x) m0 = None.
+  inst_run ge i m1 old = None <-> exists x, tree_eval (deps_get (inst_deps i d od) x) m0 = None.
 Proof.
   intro X; induction i as [|[x e] i IHi]; simpl; intros m1 d.
   - constructor 1; [discriminate | intros [x H']; rewrite H in H'; discriminate].
@@ -264,7 +264,7 @@ Proof.
       * rewrite set_spec_diff; auto.
     + intuition.
       constructor 1 with (x:=x); simpl.
-      apply tree_eval_macro_abort.
+      apply tree_eval_inst_abort.
       autorewrite with dict_rw.
       destruct (failsafe (deps_get d x)); simpl; try rewrite H0;
       erewrite tree_eval_exp; eauto.
@@ -278,12 +278,12 @@ Proof.
   induction p as [|i p IHp]; simpl; intros m1 d.
   - constructor 1; [discriminate | intros [x H']; rewrite H in H'; discriminate].
   - intros H0.
-    remember (macro_run ge i m1 m1) as om.
+    remember (inst_run ge i m1 m1) as om.
     destruct om.
     + refine (IHp _ _ _); eauto.
     + intuition.
-      assert (X: macro_run ge i m1 m1 = None); auto.
-      rewrite tree_eval_macro_None_correct in X; auto.
+      assert (X: inst_run ge i m1 m1 = None); auto.
+      rewrite tree_eval_inst_None_correct in X; auto.
       destruct X as [x H1].
       constructor 1 with (x:=x); simpl; auto.
 Qed.
@@ -295,12 +295,12 @@ Proof.
   intros; autorewrite with dict_rw; simpl; eauto.
 Qed.
 
-Lemma tree_eval_macro_Some_correct2 i m0 old od: 
+Lemma tree_eval_inst_Some_correct2 i m0 old od: 
   (forall x, tree_eval (deps_get od x) m0 = Some (old x)) ->
   forall (m1 m2: mem) d, 
   (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) ->
-    (forall x, tree_eval (deps_get (macro_deps i d od) x) m0 = Some (m2 x)) ->
-    res_eq (Some m2) (macro_run ge i m1 old).
+    (forall x, tree_eval (deps_get (inst_deps i d od) x) m0 = Some (m2 x)) ->
+    res_eq (Some m2) (inst_run ge i m1 old).
 Proof.
   intro X.
   induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H0.
@@ -317,7 +317,7 @@ Proof.
         erewrite tree_eval_exp; eauto.
       * rewrite set_spec_diff; auto.
     + generalize (H x).
-      rewrite tree_eval_macro_abort; try discriminate.
+      rewrite tree_eval_inst_abort; try discriminate.
       autorewrite with dict_rw. 
       destruct (failsafe (deps_get d x)); simpl; try rewrite H0;
       erewrite tree_eval_exp; eauto.
@@ -333,11 +333,11 @@ Proof.
     generalize (H0 x); rewrite H.
     congruence.
   - intros H.
-    remember (macro_run ge i m1 m1) as om.
+    remember (inst_run ge i m1 m1) as om.
     destruct om.
     + refine (IHp _ _ _ _ _); eauto.
-    + assert (X: macro_run ge i m1 m1 = None); auto.
-      rewrite tree_eval_macro_None_correct in X; auto.
+    + assert (X: inst_run ge i m1 m1 = None); auto.
+      rewrite tree_eval_inst_None_correct in X; auto.
       destruct X as [x H1].
       generalize (H x).
       rewrite tree_eval_abort; congruence.
@@ -377,7 +377,7 @@ End DepTree.
 Require Import PArith.
 Require Import FMapPositive.
 
-Module PosDict <: ResourceDictionary with Module R:=Pos.
+Module PosDict <: PseudoRegDictionary with Module R:=Pos.
 
 Module R:=Pos.
 
diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v
index 9051f6ad..3cc85fd5 100644
--- a/mppa_k1c/abstractbb/ImpDep.v
+++ b/mppa_k1c/abstractbb/ImpDep.v
@@ -42,7 +42,7 @@ End ISeqLanguage.
 
 Module Type ImpDict.
 
-Include ResourceDictionary.
+Include PseudoRegDictionary.
 
 Parameter eq_test: forall {A}, t A -> t A -> ?? bool.
 
@@ -209,7 +209,7 @@ Hint Resolve hexp_tree_correct: wlp.
 
 Variable debug_assign: R.t -> ?? option pstring.
 
-Fixpoint hmacro_deps (i: macro) (d od: hdeps): ?? hdeps :=
+Fixpoint hinst_deps (i: inst) (d od: hdeps): ?? hdeps :=
   match i with
   | nil => RET d
   | (x, e)::i' =>
@@ -221,7 +221,7 @@ Fixpoint hmacro_deps (i: macro) (d od: hdeps): ?? hdeps :=
       else
         DO t1 <~ hexp_tree e d od None;; 
         hTerase t1 t0 dbg);;
-     hmacro_deps i' (Dict.set d x v') od
+     hinst_deps i' (Dict.set d x v') od
   end.
 
 Lemma pset_spec_eq d x t:
@@ -244,11 +244,11 @@ Qed.
 Hint Rewrite pset_spec_eq pempty_spec: dict_rw.
 
 
-Lemma hmacro_deps_correct i: forall d1 od1,
-  WHEN hmacro_deps i d1 od1 ~> d1' THEN
+Lemma hinst_deps_correct i: forall d1 od1,
+  WHEN hinst_deps i d1 od1 ~> d1' THEN
     forall od2 d2, (forall x, pdeps_get od1 x = deps_get od2 x) ->
     (forall x, pdeps_get d1 x = deps_get d2 x) -> 
-    forall x, pdeps_get d1' x = deps_get (macro_deps i d2 od2) x.
+    forall x, pdeps_get d1' x = deps_get (inst_deps i d2 od2) x.
 Proof.
   induction i; simpl; wlp_simplify.
   + cutrewrite (failsafe (deps_get d2 a0) = failsafe (data exta0)). 
@@ -265,10 +265,10 @@ Proof.
       * rewrite set_spec_diff, pset_spec_diff; auto.
    - rewrite H, H5; auto.
 Qed.
-Global Opaque hmacro_deps.
-Hint Resolve hmacro_deps_correct: wlp.
+Global Opaque hinst_deps.
+Hint Resolve hinst_deps_correct: wlp.
 
-(* logging info: we log the number of macro-instructions passed ! *)
+(* logging info: we log the number of inst-instructions passed ! *)
 Variable log: unit -> ?? unit. 
 
 Fixpoint hbblock_deps_rec (p: bblock) (d: hdeps): ?? hdeps :=
@@ -276,7 +276,7 @@ Fixpoint hbblock_deps_rec (p: bblock) (d: hdeps): ?? hdeps :=
   | nil => RET d
   | i::p' =>
      log tt;;
-     DO d' <~ hmacro_deps i d d;;
+     DO d' <~ hinst_deps i d d;;
      hbblock_deps_rec p' d'
   end.
 
@@ -371,10 +371,10 @@ Local Hint Resolve hbblock_deps_correct Dict.eq_test_correct: wlp.
 
 Section Prog_Eq_Gen.
 
-Variable dbg1: R.t -> ?? option pstring. (* debugging of p1 macros *)
-Variable dbg2: R.t -> ?? option pstring. (* log of p2 macros *)
-Variable log1: unit -> ?? unit. (* log of p1 macros *)
-Variable log2: unit -> ?? unit. (* log of p2 macros *)
+Variable dbg1: R.t -> ?? option pstring. (* debugging of p1 insts *)
+Variable dbg2: R.t -> ?? option pstring. (* log of p2 insts *)
+Variable log1: unit -> ?? unit. (* log of p1 insts *)
+Variable log2: unit -> ?? unit. (* log of p2 insts *)
 
 
 Variable hco_tree: hashConsing tree.
diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v
index c2efd552..519e7e54 100644
--- a/mppa_k1c/abstractbb/Parallelizability.v
+++ b/mppa_k1c/abstractbb/Parallelizability.v
@@ -21,20 +21,20 @@ Local Open Scope list.
 Section PARALLEL.
 Variable ge: genv.
 
-(* parallel run of a macro *)
-Fixpoint macro_prun (i: macro) (m tmp old: mem): option mem :=
+(* parallel run of a inst *)
+Fixpoint inst_prun (i: inst) (m tmp old: mem): option mem :=
   match i with
   | nil => Some m
   | (x, e)::i' =>
      match exp_eval ge e tmp old with
-     | Some v' => macro_prun i' (assign m x v') (assign tmp x v') old
+     | Some v' => inst_prun i' (assign m x v') (assign tmp x v') old
      | None => None
      end
   end.
 
-(* [macro_prun] is generalization of [macro_run] *)   
-Lemma macro_run_prun i: forall m old,
-  macro_run ge i m old = macro_prun i m m old.
+(* [inst_prun] is generalization of [inst_run] *)   
+Lemma inst_run_prun i: forall m old,
+  inst_run ge i m old = inst_prun i m m old.
 Proof.
   induction i as [|[y e] i']; simpl; auto.
   intros m old; destruct (exp_eval ge e m old); simpl; auto.
@@ -46,7 +46,7 @@ Fixpoint prun_iw (p: bblock) m old: option mem :=
   match p with
   | nil => Some m
   | i::p' =>
-    match macro_prun i m old old with
+    match inst_prun i m old old with
     | Some m1 => prun_iw p' m1 old
     | None => None
     end
@@ -58,9 +58,9 @@ Definition prun (p: bblock) m (om: option mem) := exists p', res_eq om (prun_iw
 
 (* a few lemma on equality *)
 
-Lemma macro_prun_equiv i old: forall m1 m2 tmp,
+Lemma inst_prun_equiv i old: forall m1 m2 tmp,
   (forall x, m1 x = m2 x) ->
-  res_eq (macro_prun i m1 tmp old) (macro_prun i m2 tmp old).
+  res_eq (inst_prun i m1 tmp old) (inst_prun i m2 tmp old).
 Proof.
   induction i as [|[x e] i']; simpl; eauto.
   intros m1 m2 tmp H; destruct (exp_eval ge e tmp old); simpl; auto.
@@ -73,8 +73,8 @@ Lemma prun_iw_equiv p: forall m1 m2 old,
 Proof.
   induction p as [|i p']; simpl; eauto.
   - intros m1 m2 old H.
-    generalize (macro_prun_equiv i old m1 m2 old H);
-    destruct (macro_prun i m1 old old); simpl.
+    generalize (inst_prun_equiv i old m1 m2 old H);
+    destruct (inst_prun i m1 old old); simpl.
     + intros (m3 & H3 & H4); rewrite H3; simpl; eauto.
     + intros H1; rewrite H1; simpl; auto.
 Qed.
@@ -88,7 +88,7 @@ Lemma prun_iw_app p1: forall m1 old p2,
      end.
 Proof.
    induction p1; simpl; try congruence.
-   intros; destruct (macro_prun _ _ _); simpl; auto.
+   intros; destruct (inst_prun _ _ _); simpl; auto.
 Qed.
 
 Lemma prun_iw_app_None p1: forall m1 old p2,
@@ -272,15 +272,15 @@ Qed.
 
 (** * Writing frames *)
 
-Fixpoint macro_wframe(i:macro): list R.t := 
+Fixpoint inst_wframe(i:inst): list R.t := 
   match i with
   | nil => nil
-  | a::i' => (fst a)::(macro_wframe i') 
+  | a::i' => (fst a)::(inst_wframe i') 
   end.
 
-Lemma macro_wframe_correct i m' old: forall m tmp, 
-  macro_prun ge i m tmp old = Some m' -> 
-  forall x, notIn x (macro_wframe i) -> m' x  = m x.
+Lemma inst_wframe_correct i m' old: forall m tmp, 
+  inst_prun ge i m tmp old = Some m' -> 
+  forall x, notIn x (inst_wframe i) -> m' x  = m x.
 Proof.
   induction i as [|[y e] i']; simpl.
   - intros m tmp H x H0; inversion_clear H; auto.
@@ -289,47 +289,47 @@ Proof.
     rewrite assign_diff; auto.
 Qed.
 
-Lemma macro_prun_fequiv i old: forall m1 m2 tmp, 
-  frame_eq (fun x => In x (macro_wframe i)) (macro_prun ge i m1 tmp old) (macro_prun ge i m2 tmp old).
+Lemma inst_prun_fequiv i old: forall m1 m2 tmp, 
+  frame_eq (fun x => In x (inst_wframe i)) (inst_prun ge i m1 tmp old) (inst_prun ge i m2 tmp old).
 Proof.
   induction i as [|[y e] i']; simpl.
   - intros m1 m2 tmp; eexists; intuition eauto.
   - intros m1 m2 tmp. destruct (exp_eval ge e tmp old); simpl; auto.
     eapply frame_eq_list_split; eauto. clear IHi'.
     intros m1' m2' x H1 H2.
-    lapply (macro_wframe_correct i' m1' old (assign m1 y v) (assign tmp y v)); eauto.
-    lapply (macro_wframe_correct i' m2' old (assign m2 y v) (assign tmp y v)); eauto.
+    lapply (inst_wframe_correct i' m1' old (assign m1 y v) (assign tmp y v)); eauto.
+    lapply (inst_wframe_correct i' m2' old (assign m2 y v) (assign tmp y v)); eauto.
     intros Xm2 Xm1 H H0. destruct H. 
     + subst. rewrite Xm1, Xm2; auto. rewrite !assign_eq. auto.
     + rewrite <- notIn_iff in H0; tauto.
 Qed.
 
-Lemma macro_prun_None i m1 m2 tmp old: 
-  macro_prun ge i m1 tmp old = None -> 
-  macro_prun ge i m2 tmp old = None.
+Lemma inst_prun_None i m1 m2 tmp old: 
+  inst_prun ge i m1 tmp old = None -> 
+  inst_prun ge i m2 tmp old = None.
 Proof.
-  intros H; generalize (macro_prun_fequiv i old m1 m2 tmp).
+  intros H; generalize (inst_prun_fequiv i old m1 m2 tmp).
   rewrite H; simpl; auto.
 Qed.
 
-Lemma macro_prun_Some i m1 m2 tmp old m1': 
-  macro_prun ge i m1 tmp old = Some m1' -> 
-  res_eq (Some (frame_assign m2 (macro_wframe i) m1')) (macro_prun ge i m2 tmp old).
+Lemma inst_prun_Some i m1 m2 tmp old m1': 
+  inst_prun ge i m1 tmp old = Some m1' -> 
+  res_eq (Some (frame_assign m2 (inst_wframe i) m1')) (inst_prun ge i m2 tmp old).
 Proof.
-  intros H; generalize (macro_prun_fequiv i old m1 m2 tmp).
+  intros H; generalize (inst_prun_fequiv i old m1 m2 tmp).
   rewrite H; simpl.
   intros (m2' & H1 & H2).
   eexists; intuition eauto.
   rewrite frame_assign_def.
-  lapply (macro_wframe_correct i m2' old m2 tmp); eauto.
-  destruct (notIn_dec x (macro_wframe i)); auto.
+  lapply (inst_wframe_correct i m2' old m2 tmp); eauto.
+  destruct (notIn_dec x (inst_wframe i)); auto.
   intros X; rewrite X; auto.
 Qed.
 
 Fixpoint bblock_wframe(p:bblock): list R.t := 
   match p with
   | nil => nil
-  | i::p' => (macro_wframe i)++(bblock_wframe p') 
+  | i::p' => (inst_wframe i)++(bblock_wframe p') 
   end.
 
 Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_comm.
@@ -350,11 +350,11 @@ Proof.
   induction p as [|i p']; simpl.
   - intros m H; inversion_clear H; auto.
   - intros m H x; rewrite notIn_app; intros (H1 & H2). 
-    remember (macro_prun i m old old) as om.
+    remember (inst_prun i m old old) as om.
     destruct om as [m1|]; simpl.
     + eapply eq_trans.
       eapply IHp'; eauto.
-      eapply macro_wframe_correct; eauto.
+      eapply inst_wframe_correct; eauto.
     + inversion H.
 Qed.
 
@@ -363,13 +363,13 @@ Lemma prun_iw_fequiv p old: forall m1 m2,
 Proof.
   induction p as [|i p']; simpl.
   - intros m1 m2; eexists; intuition eauto.
-  - intros m1 m2; generalize (macro_prun_fequiv i old m1 m2 old).
-    remember (macro_prun i m1 old old) as om.
+  - intros m1 m2; generalize (inst_prun_fequiv i old m1 m2 old).
+    remember (inst_prun i m1 old old) as om.
     destruct om as [m1'|]; simpl.
     + intros (m2' & H1 & H2). rewrite H1; simpl.
     eapply frame_eq_list_split; eauto. clear IHp'.
     intros m1'' m2'' x H3 H4. rewrite in_app_iff.
-    intros X X2. assert (X1: In x (macro_wframe i)). { destruct X; auto. rewrite <- notIn_iff in X2; tauto. }
+    intros X X2. assert (X1: In x (inst_wframe i)). { destruct X; auto. rewrite <- notIn_iff in X2; tauto. }
     clear X.
     lapply (bblock_wframe_correct p' m1'' old m1'); eauto.
     lapply (bblock_wframe_correct p' m2'' old m2'); eauto.
@@ -397,7 +397,7 @@ Fixpoint is_det (p: bblock): Prop :=
   match p with
   | nil => True
   | i::p' =>
-       disjoint (macro_wframe i) (bblock_wframe p') (* no WRITE-AFTER-WRITE *)
+       disjoint (inst_wframe i) (bblock_wframe p') (* no WRITE-AFTER-WRITE *)
     /\ is_det p'
   end.
 
@@ -419,32 +419,32 @@ Theorem is_det_correct p p':
 Proof.
   induction 1 as [ | i p p' | i1 i2 p | p1 p2 p3 ]; simpl; eauto.
   - intros [H0 H1] m old.
-    remember (macro_prun ge i m old old) as om0.
+    remember (inst_prun ge i m old old) as om0.
     destruct om0 as [ m0 | ]; simpl; auto.
   - rewrite disjoint_app_r.
     intros ([Z1 Z2] & Z3 & Z4) m old.
-    remember (macro_prun ge i2 m old old) as om2.
+    remember (inst_prun ge i2 m old old) as om2.
     destruct om2 as [ m2 | ]; simpl; auto.
-    + remember (macro_prun ge i1 m old old) as om1.
+    + remember (inst_prun ge i1 m old old) as om1.
       destruct om1 as [ m1 | ]; simpl; auto.
-      * lapply (macro_prun_Some i2 m m1 old old m2); simpl; auto.
-        lapply (macro_prun_Some i1 m m2 old old m1); simpl; auto.
+      * lapply (inst_prun_Some i2 m m1 old old m2); simpl; auto.
+        lapply (inst_prun_Some i1 m m2 old old m1); simpl; auto.
         intros (m1' & Hm1' & Xm1') (m2' & Hm2' & Xm2').
         rewrite Hm1', Hm2'; simpl.
         eapply prun_iw_equiv.
         intros x; rewrite <- Xm1', <- Xm2'. clear Xm2' Xm1' Hm1' Hm2' m1' m2'.
         rewrite frame_assign_def.
         rewrite disjoint_sym in Z1; unfold disjoint in Z1.
-        destruct (notIn_dec x (macro_wframe i1)) as [ X1 | X1 ].
-        { rewrite frame_assign_def; destruct (notIn_dec x (macro_wframe i2)) as [ X2 | X2 ]; auto.
-          erewrite (macro_wframe_correct i2 m2 old m old); eauto.
-          erewrite (macro_wframe_correct i1 m1 old m old); eauto.
+        destruct (notIn_dec x (inst_wframe i1)) as [ X1 | X1 ].
+        { rewrite frame_assign_def; destruct (notIn_dec x (inst_wframe i2)) as [ X2 | X2 ]; auto.
+          erewrite (inst_wframe_correct i2 m2 old m old); eauto.
+          erewrite (inst_wframe_correct i1 m1 old m old); eauto.
         }
         rewrite frame_assign_notIn; auto.
-     * erewrite macro_prun_None; eauto. simpl; auto.
-   + remember (macro_prun ge i1 m old old) as om1.
+     * erewrite inst_prun_None; eauto. simpl; auto.
+   + remember (inst_prun ge i1 m old old) as om1.
      destruct om1 as [ m1 | ]; simpl; auto.
-     erewrite macro_prun_None; eauto.
+     erewrite inst_prun_None; eauto.
   - intros; eapply res_eq_trans.
     eapply IHPermutation1; eauto.
     eapply IHPermutation2; eauto.
@@ -479,23 +479,23 @@ Proof.
     intros; (eapply H1 || eapply H2); rewrite in_app_iff; auto.
 Qed.
 
-Fixpoint macro_frame (i: macro): list R.t :=
+Fixpoint inst_frame (i: inst): list R.t :=
   match i with
   | nil => nil
-  | a::i' => (fst a)::(exp_frame (snd a) ++ macro_frame i') 
+  | a::i' => (fst a)::(exp_frame (snd a) ++ inst_frame i') 
   end.
 
-Lemma macro_wframe_frame i x: In x (macro_wframe i) -> In x (macro_frame i).
+Lemma inst_wframe_frame i x: In x (inst_wframe i) -> In x (inst_frame i).
 Proof.
   induction i as [ | [y e] i']; simpl; intuition.
 Qed.
 
 
-Lemma macro_frame_correct i wframe old1 old2: forall m tmp1 tmp2,
-  (disjoint (macro_frame i) wframe) ->
+Lemma inst_frame_correct i wframe old1 old2: forall m tmp1 tmp2,
+  (disjoint (inst_frame i) wframe) ->
   (forall x, notIn x wframe -> old1 x = old2 x) ->
   (forall x, notIn x wframe -> tmp1 x = tmp2 x) ->
-  macro_prun ge i m tmp1 old1 = macro_prun ge i m tmp2 old2.
+  inst_prun ge i m tmp1 old1 = inst_prun ge i m tmp2 old2.
 Proof.
   induction i as [|[x e] i']; simpl; auto.
   intros m tmp1 tmp2; rewrite disjoint_cons_l, disjoint_app_l.
@@ -515,8 +515,8 @@ Fixpoint pararec (p: bblock) (wframe: list R.t): Prop :=
   match p with
   | nil => True
   | i::p' =>
-       disjoint (macro_frame i) wframe (* no USE-AFTER-WRITE *)
-    /\ pararec p' ((macro_wframe i) ++ wframe)
+       disjoint (inst_frame i) wframe (* no USE-AFTER-WRITE *)
+    /\ pararec p' ((inst_wframe i) ++ wframe)
   end.
 
 Lemma pararec_disjoint (p: bblock): forall wframe, pararec p wframe -> disjoint (bblock_wframe p) wframe.
@@ -527,7 +527,7 @@ Proof.
     generalize (IHp' _ H1).
     rewrite disjoint_app_r. intuition. 
     eapply disjoint_incl_l. 2: eapply H0.
-    unfold incl. eapply macro_wframe_frame; eauto.
+    unfold incl. eapply inst_wframe_frame; eauto.
 Qed.
 
 Lemma pararec_det p: forall wframe, pararec p wframe -> is_det p.
@@ -546,13 +546,13 @@ Lemma pararec_correct p old: forall wframe m,
 Proof.
   elim p; clear p; simpl; auto.
   intros i p' X wframe m [H H0] H1.
-  erewrite macro_run_prun, macro_frame_correct; eauto.
-  remember (macro_prun ge i m old old) as om0.
+  erewrite inst_run_prun, inst_frame_correct; eauto.
+  remember (inst_prun ge i m old old) as om0.
   destruct om0 as [m0 | ]; try congruence.
   eapply X; eauto.
   intro x; rewrite notIn_app. intros [H3 H4].
   rewrite <- H1; auto.
-  eapply macro_wframe_correct; eauto.
+  eapply inst_wframe_correct; eauto.
 Qed.
 
 Definition parallelizable (p: bblock) := pararec p nil.
@@ -576,9 +576,9 @@ End PARALLELI.
 End ParallelizablityChecking.
 
 
-Module Type ResourceSet.
+Module Type PseudoRegSet.
 
-Declare Module R: ResourceNames.
+Declare Module R: PseudoRegisters.
 
 (** We assume a datatype [t] refining (list R.t)
 
@@ -602,7 +602,7 @@ Parameter union_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_fram
 Parameter is_disjoint: t -> t -> bool.
 Parameter is_disjoint_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_frame s2 l2 -> (is_disjoint s1 s2)=true -> disjoint l1 l2. 
 
-End ResourceSet.
+End PseudoRegSet.
 
 
 Lemma lazy_andb_bool_true (b1 b2: bool): b1 &&& b2 = true <-> b1 = true /\ b2 = true.
@@ -613,7 +613,7 @@ Qed.
 
 
 
-Module ParallelChecks (L: SeqLanguage) (S:ResourceSet with Module R:=L.LP.R).
+Module ParallelChecks (L: SeqLanguage) (S:PseudoRegSet with Module R:=L.LP.R).
 
 Include ParallelizablityChecking L.
 
@@ -624,13 +624,13 @@ Local Hint Resolve S.empty_match_frame S.add_match_frame S.union_match_frame S.i
 
 (** Now, refinement of each operation toward parallelizable *)
 
-Fixpoint macro_wsframe(i:macro): S.t :=
+Fixpoint inst_wsframe(i:inst): S.t :=
   match i with
   | nil => S.empty
-  | a::i' => S.add (fst a) (macro_wsframe i') 
+  | a::i' => S.add (fst a) (inst_wsframe i') 
   end.
 
-Lemma macro_wsframe_correct i: S.match_frame (macro_wsframe i) (macro_wframe i).
+Lemma inst_wsframe_correct i: S.match_frame (inst_wsframe i) (inst_wframe i).
 Proof.
   induction i; simpl; auto.
 Qed.
@@ -653,27 +653,27 @@ Proof.
   induction e using exp_mut with (P0:=fun l => S.match_frame (list_exp_sframe l) (list_exp_frame l)); simpl; auto.
 Qed.
 
-Fixpoint macro_sframe (i: macro): S.t :=
+Fixpoint inst_sframe (i: inst): S.t :=
   match i with
   | nil => S.empty
-  | a::i' => S.add (fst a) (S.union (exp_sframe (snd a)) (macro_sframe i'))
+  | a::i' => S.add (fst a) (S.union (exp_sframe (snd a)) (inst_sframe i'))
   end.
 
 Local Hint Resolve exp_sframe_correct.
 
-Lemma macro_sframe_correct i: S.match_frame (macro_sframe i) (macro_frame i).
+Lemma inst_sframe_correct i: S.match_frame (inst_sframe i) (inst_frame i).
 Proof.
   induction i as [|[y e] i']; simpl; auto.
 Qed.
 
-Local Hint Resolve macro_wsframe_correct macro_sframe_correct.
+Local Hint Resolve inst_wsframe_correct inst_sframe_correct.
 
 Fixpoint is_pararec (p: bblock) (wsframe: S.t): bool :=
   match p with
   | nil => true
   | i::p' =>
-       S.is_disjoint (macro_sframe i) wsframe (* no USE-AFTER-WRITE *)
-    &&& is_pararec p' (S.union (macro_wsframe i) wsframe)
+       S.is_disjoint (inst_sframe i) wsframe (* no USE-AFTER-WRITE *)
+    &&& is_pararec p' (S.union (inst_wsframe i) wsframe)
   end.
 
 Lemma is_pararec_correct (p: bblock): forall s l, S.match_frame s l -> (is_pararec p s)=true -> (pararec p l).
@@ -706,7 +706,7 @@ End ParallelChecks.
 Require Import PArith.
 Require Import MSets.MSetPositive.
 
-Module PosResourceSet <: ResourceSet with Module R:=Pos.
+Module PosPseudoRegSet <: PseudoRegSet with Module R:=Pos.
 
 Module R:=Pos.
 
@@ -776,4 +776,4 @@ Proof.
   intros H4 H5; eapply is_disjoint_spec_true; eauto.
 Qed.
 
-End PosResourceSet.
+End PosPseudoRegSet.