1 files changed, 62 insertions, 27 deletions
diff --git a/src/Assembly/State.v b/src/Assembly/State.v
index 16b9b12d3..2e030d242 100644
--- a/src/Assembly/State.v
+++ b/src/Assembly/State.v
@@ -23,33 +23,24 @@ Module State.
     Delimit Scope state_scope with state.
     Local Open Scope state_scope.
 
-    (* Sugar and Tactics *)
-
-    Definition convert {A B: Type} (x: A) (H: A = B): B :=
-    eq_rect A (fun B0 : Type => B0) x B H.
-
-    Notation "'always' A" := (fun _ => A) (at level 90) : state_scope.
-    Notation "'cast' e" := (convert e _) (at level 20) : state_scope.
-    Notation "'lift' e" := (exist _ e _) (at level 20) : state_scope.
-    Notation "'contra'" := (False_rec _ _) : state_scope.
-
-    Obligation Tactic := abstract intuition.
-
     (* The Big Definition *)
 
     Inductive State :=
-      | fullState (regState: StateMap) (stackState: DefMap): State.
+    | fullState (intRegState: StateMap)
+                (floatRegState: StateMap)
+                (stackState: DefMap)
+                (carryBit: CarryState): State.
 
-    Definition emptyState: State := fullState (NatM.empty DefMap) (NatM.empty N).
+    Definition emptyState: State := fullState (NatM.empty DefMap) (NatM.empty DefMap) (NatM.empty N) None.
 
     (* Register State Manipulations *)
 
-    Definition getReg {n} (reg: Reg n) (state: State): option (word n) :=
+    Definition getIntReg {n} (reg: IReg n) (state: State): option (word n) :=
       match state with
-      | fullState regState stackState =>
-        match (NatM.find n regState) with
+      | fullState intRegState _ _ _ =>
+        match (NatM.find n intRegState) with
         | Some map =>
-            match (NatM.find (getRegIndex reg) map) with
+            match (NatM.find (getIRegIndex reg) map) with
             | Some m => Some (NToWord n m)
             | _ => None
             end
@@ -57,23 +48,66 @@ Module State.
         end
       end.
 
-    Definition setReg {n} (reg: Reg n) (value: word n) (state: State): option State :=
+    Definition setIntReg {n} (reg: IReg n) (value: word n) (state: State): option State :=
+      match state with
+      | fullState intRegState floatRegState stackState carryState =>
+        match (NatM.find n intRegState) with
+        | Some map =>
+            Some (fullState
+                    (NatM.add n (NatM.add (getIRegIndex reg) (wordToN value) map) intRegState)
+                    floatRegState
+                    stackState
+                    carryState)
+        | None => None
+        end
+      end.
+
+    Definition getFloatReg {n} (reg: FReg n) (state: State): option (word n) :=
+      match state with
+      | fullState _ floatRegState _ _ =>
+        match (NatM.find n floatRegState) with
+        | Some map =>
+          match (NatM.find (getFRegIndex reg) map) with
+          | Some v => Some (NToWord n v)
+          | None => None
+          end
+        | None => None
+        end
+      end.
+
+    Definition setFloatReg {n} (reg: FReg n) (value: word n) (state: State): option State :=
       match state with
-      | fullState regState stackState =>
-        match (NatM.find n regState) with
+      | fullState intRegState floatRegState stackState carryState =>
+        match (NatM.find n floatRegState) with
         | Some map =>
             Some (fullState
-                    (NatM.add n (NatM.add (getRegIndex reg) (wordToN value) map) regState)
-                    stackState)
+              intRegState
+              (NatM.add n (NatM.add (getFRegIndex reg) (wordToN value) map) floatRegState)
+              stackState
+              carryState)
         | None => None
         end
       end.
 
+    (* Carry State Manipulations *)
+
+    Definition getCarry (state: State): CarryState :=
+      match state with
+      | fullState _ _ _ b => b
+      end.
+
+    Definition setCarry (value: bool) (state: State): State :=
+      match state with
+      | fullState intRegState floatRegState stackState carryState =>
+        fullState intRegState floatRegState stackState (Some value)
+      end.
+
+
     (* Per-word Stack Operations *)
 
     Definition getStack32 (entry: Stack 32) (state: State): option (word 32) :=
       match state with
-      | fullState regState stackState =>
+      | fullState _ _ stackState _ =>
         match entry with
         | stack32 loc =>
           match (NatM.find loc stackState) with
@@ -85,11 +119,12 @@ Module State.
 
     Definition setStack32 (entry: Stack 32) (value: word 32) (state: State): option State :=
     match state with
-    | fullState regState stackState =>
+    | fullState intRegState floatRegState stackState carryState =>
         match entry with
         | stack32 loc =>
-        (Some (fullState regState
-              (NatM.add loc (wordToN value) stackState)))
+          (Some (fullState intRegState floatRegState
+                   (NatM.add loc (wordToN value) stackState)
+                   carryState))
         end
     end.