Pushing through changes

3 files changed, 31 insertions, 54 deletions

diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index 7f19785f0..aaf72e65e 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: {w: word 32 | validFloat _ _ Float32 w} -> FConst 32
-  | constFloat64: {w: word 64 | validFloat _ _ Float64 w} -> FConst 64.
+  | constFloat32: word 23 -> FConst 32
+  | constFloat64: word 52 -> FConst 64.
 
 Inductive IReg: nat -> Type :=
   | regInt32: nat -> IReg 32.
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index 3e5804f21..2946f3cbb 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -76,72 +76,49 @@ Definition evalOperation (o: Operation) (state: State): option State.
     | Shr => NToWord 32 (N.shiftr_nat (wordToN x) n)
     end in
 
+  let liftOpt := fun {A B C} (f: A -> B -> option C) (xo: option A) (yo: option B) =>
+    match (xo, yo) with
+    | (Some x, Some y) => f x y
+    | _ => None
+    end in
+
   match o with
   | IOpConst o r c =>
-    match (getIntReg r state) with
-    | Some va =>
-      match c with
-      | constInt32 vb => setIntReg r (evalIOp o va vb) state
-      end
-    | None => None
-    end
+    liftOpt (fun x y => setIntReg r (evalIOp o x y) state)
+      (getIntReg r state) (match c with | constInt32 v => Some v end)
 
   | IOpReg o a b =>
-    match (getIntReg a state) with
-    | Some va =>
-      match (getIntReg b state) with
-      | Some vb => setIntReg a (evalIOp o va vb) state
-      | _ => None
-      end
-    | None => None
-    end
+    liftOpt (fun x y => setIntReg a (evalIOp o x y) state)
+      (getIntReg a state) (getIntReg b state)
 
   | FOpConst32 o r c =>
-    match (getFloatReg r state) with
-    | Some va =>
-      match c with
-      | constFloat32 vb => setFloatReg r (evalFOp o va (convert vb _)) state
-      end
-    | None => None
-    end
+    liftOpt (fun x y => setFloatReg r (evalFOp o x y) state) (getFloatReg r state)
+      (convert (match c with | constFloat32 v => Some v | _ => None end) _)
 
   | FOpReg32 o a b =>
-    match (getFloatReg a state) with
-    | Some va =>
-      match (getFloatReg b state) with
-      | Some vb => setFloatReg a (evalFOp o va (convert vb _)) state
-      | _ => None
-      end
-    | None => None
-    end
+    liftOpt (fun x y => setFloatReg a (evalFOp o x y) state)
+      (getFloatReg a state) (convert (getFloatReg b state) _)
 
   | FOpConst64 o r c =>
-    match (getFloatReg r state) with
-    | Some va =>
-      match c with
-      | constFloat64 vb => setFloatReg r (evalFOp o va (convert vb _)) state
-      end
-    | None => None
-    end
+    liftOpt (fun x y => setFloatReg r (evalFOp o x y) state)
+      (getFloatReg r state) (match c with | constFloat64 v => Some v | _ => None end)
 
   | FOpReg64 o a b =>
-    match (getFloatReg a state) with
-    | Some va =>
-      match (getFloatReg b state) with
-      | Some vb => setFloatReg a (evalFOp o va (convert vb _)) state
-      | _ => None
-      end
-    | None => None
-    end
+    liftOpt (fun x y => setFloatReg a (evalFOp o x y) state)
+      (getFloatReg a state) (convert (getFloatReg b state) _)
 
   | OpRot o r i =>
    match (getIntReg r state) with
     | Some va => setIntReg r (evalRotOp o va i) state
     | None => None
     end
-  end);
-    unfold evalIOp, evalFOp, evalRotOp, getFractionalBits;
-    simpl; intuition.
+  end); unfold evalIOp, evalFOp, evalRotOp, getFractionalBits.
+
+  elim r.
+  destruct r.
+
+    try destruct r; try destruct c; try destruct a; try destruct b; simpl;
+    intuition.
   (* TODO *)
 Defined.
 
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
index 60b3b49a0..07091831d 100644
--- a/src/Assembly/QhasmUtil.v
+++ b/src/Assembly/QhasmUtil.v
@@ -22,14 +22,14 @@ Module Util.
       refine match reg with
       | regFloat32 _ => (eq_rect _ id Float32 _ _)
       | regFloat64 _ => (eq_rect _ id Float64 _ _)
-      end; intuition.
+      end; abstract intuition.
     Defined.
 
     (* Magical Bitwise Manipulations *)
 
     (* Force w to be m bits long, by truncation or zero-extension *)
     Definition trunc {n} (m: nat) (w: word n): word m.
-    destruct (lt_eq_lt_dec n m) as [s|s]; try destruct s as [s|s].
+      destruct (lt_eq_lt_dec n m) as [s|s]; try destruct s as [s|s].
 
     - replace m with (n + (m - n)) by abstract intuition.
         refine (zext w (m - n)).
@@ -64,11 +64,11 @@ Module Util.
     Proof. intros; destruct x; simpl; intuition. Qed.
 
     Definition segmentStackWord {n} (x: Stack n) (w: word n): word (32 * (getStackWords x)).
-    intros; destruct x; simpl; intuition.
+      intros; destruct x; simpl; intuition.
     Defined.
 
     Definition desegmentStackWord {n} (x: Stack n) (w: word (32 * (getStackWords x))): word n.
-    intros; destruct x; simpl; intuition.
+      intros; destruct x; simpl; intuition.
     Defined.
 
  End Util.