Pushing through changes

4 files changed, 53 insertions, 33 deletions

diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index aaf72e65e..aeeb0746f 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -71,8 +71,8 @@ Inductive IConst: nat -> Type :=
   | constInt32: word 32 -> IConst 32.
 
 Inductive FConst: nat -> Type :=
-  | constFloat32: word 23 -> FConst 32
-  | constFloat64: word 52 -> FConst 64.
+  | constFloat32: word 32 -> FConst 32
+  | constFloat64: word 64 -> FConst 64.
 
 Inductive IReg: nat -> Type :=
   | regInt32: nat -> IReg 32.
@@ -90,11 +90,14 @@ Definition CarryState := option bool.
 
 (* Assignments *)
 Inductive Assignment : Type :=
-  | AStackInt: forall n, IReg n -> Stack n -> Assignment
-  | AStackFloat: forall n, FReg n -> Stack n -> Assignment
+  | ARegStackInt: forall n, IReg n -> Stack n -> Assignment
+  | ARegStackFloat: forall n, FReg n -> Stack n -> Assignment
 
-  | ARegInt: forall n, IReg n -> IReg n -> Assignment
-  | ARegFloat: forall n, FReg n -> FReg n -> Assignment
+  | AStackRegInt: forall n, Stack n -> IReg n -> Assignment
+  | AStackRegFloat: forall n, Stack n -> FReg n -> Assignment
+
+  | ARegRegInt: forall n, IReg n -> IReg n -> Assignment
+  | ARegRegFloat: forall n, FReg n -> FReg n -> Assignment
 
   | AConstInt: forall n, IReg n -> IConst n -> Assignment
   | AConstFloat: forall n, FReg n -> FConst n -> Assignment
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index 0bde226e7..c7077e3b3 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -85,14 +85,16 @@ Definition evalOperation (o: Operation) (state: State): option State.
   match o with
   | IOpConst o r c =>
     liftOpt (fun x y => setIntReg r (evalIOp o x y) state)
-      (getIntReg r state) (match c with | constInt32 v => Some v end)
+      (getIntReg r state)
+      (match c with | constInt32 v => Some v end)
 
   | IOpReg o a b =>
     liftOpt (fun x y => setIntReg a (evalIOp o x y) state)
       (getIntReg a state) (getIntReg b state)
 
   | FOpConst32 o r c =>
-    liftOpt (fun x y => setFloatReg r (evalFOp o x y) state) (getFloatReg r state)
+    liftOpt (fun x y => setFloatReg r (evalFOp o x y) state)
+      (getFloatReg r state)
       (match c with | constFloat32 v => Some (convert v _) end)
 
   | FOpReg32 o a b =>
@@ -100,7 +102,8 @@ Definition evalOperation (o: Operation) (state: State): option State.
       (getFloatReg a state) (convert (getFloatReg b state) _)
 
   | FOpConst64 o r c =>
-    liftOpt (fun x y => setFloatReg r (evalFOp o x y) state) (getFloatReg r state)
+    liftOpt (fun x y => setFloatReg r (evalFOp o x y) state)
+      (getFloatReg r state)
       (match c with | constFloat64 v => Some (convert v _) end)
 
   | FOpReg64 o a b =>
@@ -116,7 +119,33 @@ Definition evalOperation (o: Operation) (state: State): option State.
 Defined.
 
 Definition evalAssignment (a: Assignment) (state: State): option State :=
+  let liftOpt := fun {A B} (f: A -> option B) (xo: option A) =>
+    match x with
+    | (Some x') => f x'
+    | _ => None
+    end in
+
   match a with
+  | AStackInt n r s =>
+    liftOpt (fun x y => setIntReg r x state)
+      (match c with | constInt32 v => Some v end)
+
+  | AStackFloat n r s =>
+
+  | ARegInt n a b =>
+
+  | ARegFloat n a b =>
+
+  | AConstInt n r c =>
+
+  | AConstFloat n r c =>
+
+  | AIndex n m i =>
+
+  | APtr n r s =>
+
+  end.
+
   | Assign32Stack32 r s =>
     match (getReg r state) with
     | Some v0 =>
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
index daeb9573b..70c3e4218 100644
--- a/src/Assembly/QhasmUtil.v
+++ b/src/Assembly/QhasmUtil.v
@@ -10,14 +10,11 @@ Module Util.
     Definition indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i.
     Coercion indexToNat : Index >-> nat.
 
-    (* Float Manipulations*)
+    (* Float Manipulations *)
 
     Definition getFractionalBits {n} (reg: FReg n): nat :=
-      match n with
-      | 32 => 23
-      | 64 => 52
-      | _ => 0
-      end.
+      if (Nat.eq_dec n 32) then 23 else
+      if (Nat.eq_dec n 64) then 52 else 0.
 
     Definition getFloatInstance {n} (reg: FReg n): Float n (getFractionalBits reg).
       refine match reg with
diff --git a/src/Assembly/State.v b/src/Assembly/State.v
index 1a6982db0..2e030d242 100644
--- a/src/Assembly/State.v
+++ b/src/Assembly/State.v
@@ -62,41 +62,32 @@ Module State.
         end
       end.
 
-    Definition getFloatReg {n} (reg: FReg n) (state: State):
-        option (word (getFractionalBits reg)).
-      refine match state with
+    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 m =>
-            let f := getFloatInstance reg in
-            let b := getFractionalBits reg in
-            Some (floatToWord n b f (deserialize n b f m))
-          | _ => None
+          | Some v => Some (NToWord n v)
+          | None => None
           end
         | None => None
         end
-      end; abstract (unfold getFractionalBits, f, b; destruct reg; simpl; intuition).
-    Defined.
+      end.
 
-    Definition setFloatReg {n} (reg: FReg n) (value: word (getFractionalBits reg)) (state: State): option State.
-      refine match state with
+    Definition setFloatReg {n} (reg: FReg n) (value: word n) (state: State): option State :=
+      match state with
       | fullState intRegState floatRegState stackState carryState =>
         match (NatM.find n floatRegState) with
         | Some map =>
-            let f := getFloatInstance reg in
-            let b := getFractionalBits reg in
             Some (fullState
               intRegState
-              (NatM.add n (NatM.add (getFRegIndex reg)
-                 (serialize n b f (wordToFloat n b f value)) map) floatRegState)
+              (NatM.add n (NatM.add (getFRegIndex reg) (wordToN value) map) floatRegState)
               stackState
               carryState)
         | None => None
         end
-      end; abstract (unfold getFractionalBits, f, b; destruct reg; simpl; intuition).
-    Defined.
+      end.
 
     (* Carry State Manipulations *)