definition of VLIW semantics

1 files changed, 9 insertions, 9 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 621ed8a7..b656789b 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -801,10 +801,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) *)
@@ -1221,7 +1221,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
 
@@ -1263,7 +1263,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' => 
@@ -1323,7 +1323,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 =>
@@ -1338,7 +1338,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
@@ -1362,7 +1362,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 *)
@@ -1403,7 +1403,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'