merge VLIW proofs

Merge branch 'mppa-mul' into mppa-ternary

1 files changed, 11 insertions, 10 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index eb35ac99..2fe27143 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -178,7 +178,8 @@ Inductive ex_instruction : Type :=
   | Pbtbl   (r: ireg)  (tbl: list label)            (**r N-way branch through a jump table *) *)
 
   | Pbuiltin: external_function -> list (builtin_arg preg)
-              -> builtin_res preg -> ex_instruction   (**r built-in function (pseudo) *).
+              -> builtin_res preg -> ex_instruction   (**r built-in function (pseudo) *)
+.
 
 (** FIXME: comment not up to date !
 
@@ -842,10 +843,10 @@ Section RELSEM.
   set and memory state after execution of the instruction at [rs#PC],
   or [Stuck] if the processor is stuck. *)
 
-Inductive outcome {rgset}: Type :=
-  | Next (rs:rgset) (m:mem)
+Inductive outcome: Type :=
+  | Next (rs:regset) (m:mem)
   | Stuck.
-Arguments outcome: clear implicits.
+(* Arguments outcome: clear implicits. *)
 
 
 (** ** Arithmetic Expressions (including comparisons) *)
@@ -1323,7 +1324,7 @@ Definition store_chunk n :=
 
 (** * basic instructions *)
 
-Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome regset :=
+Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome :=
   match bi with
   | PArith ai => Next (exec_arith_instr ai rs) m
 
@@ -1365,7 +1366,7 @@ Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome regset :
   | Pnop => Next rs m
 end.
 
-Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome regset :=
+Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
   match body with
   | nil => Next rs m
   | bi::body' => 
@@ -1425,7 +1426,7 @@ Fixpoint label_pos (lbl: label) (pos: Z) (lb: bblocks) {struct lb} : option Z :=
   | b :: lb' => if is_label lbl b then Some pos else label_pos lbl (pos + (size b)) lb'
   end.
 
-Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome regset :=
+Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome :=
   match label_pos lbl 0 (fn_blocks f) with
   | None => Stuck
   | Some pos =>
@@ -1440,7 +1441,7 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome
 Warning: in m PC is assumed to be already pointing on the next instruction !
 
 *)
-Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome regset :=
+Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome :=
   match res with
     | Some true  => goto_label f l rs m
     | Some false => Next rs m
@@ -1464,7 +1465,7 @@ Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: opti
     we generate cannot use those registers to hold values that must
     survive the execution of the pseudo-instruction. *)
 
-Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome regset :=
+Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome :=
   match oc with
   | Some ic =>
 (** Get/Set system registers *)
@@ -1504,7 +1505,7 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem)
   | None => Next rs m
 end.
 
-Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome regset :=
+Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome :=
   match exec_body (body b) rs0 m with
   | Next rs' m' =>
     let rs1 := nextblock b rs' in exec_control f (exit b) rs1 m'