actually-decent PseudoConversion semantics

3 files changed, 96 insertions, 24 deletions

diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index ae7ccbf60..df18bd402 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -5,7 +5,7 @@ Require Import List.
 Module Type PseudoMachine.
   Parameter width: nat.
   Parameter vars: nat.
-  Parameter izero: IConst width.
+  Parameter width_spec: ISize width.
 End PseudoMachine.
 
 Module Pseudo (M: PseudoMachine) <: Language.
@@ -13,22 +13,30 @@ Module Pseudo (M: PseudoMachine) <: Language.
 
   Definition const: Type := word width.
 
-  Definition ireg: nat -> IReg width :=
-    match izero with
-    | constInt32 _ => regInt32
-    | constInt64 _ => regInt64
-    end.
+  Definition width_dec: {width = 32} + {width = 64}.
+    destruct width_spec.
+    - left; abstract intuition.
+    - right; abstract intuition.
+  Defined.
 
-  Definition iconst: word width -> IConst width :=
-    match izero with
-    | constInt32 _ => constInt32
-    | constInt64 _ => constInt64
+  Definition ireg (x: nat): IReg width :=
+    match width_spec with
+    | I32 => regInt32 x
+    | I64 => regInt64 x
     end.
 
-  Definition stack: nat -> Stack width :=
-    match izero with
-    | constInt32 _ => stack32
-    | constInt64 _ => fun x => stack64 (2 * x)
+  Definition iconst (x: word width): IConst width.
+    refine (
+      if width_dec
+      then (convert constInt32 _) x
+      else (convert constInt64 _) x);
+    abstract (rewrite _H; intuition).
+  Defined.
+
+  Definition stack (x: nat): Stack width :=
+    match width_spec with
+    | I32 => stack32 x
+    | I64 => stack64 (2 * x)
     end.
 
   (* Program Types *)
@@ -150,14 +158,14 @@ End Pseudo.
 Module PseudoUnary32 <: PseudoMachine.
   Definition width := 32.
   Definition vars := 1.
-  Definition izero := constInt32 (wzero 32).
+  Definition width_spec := I32.
   Definition const: Type := word width.
 End PseudoUnary32.
 
 Module PseudoUnary64 <: PseudoMachine.
   Definition width := 64.
   Definition vars := 1.
-  Definition izero := constInt64 (wzero 64).
+  Definition width_spec := I64.
   Definition const: Type := word width.
 End PseudoUnary64.
  
\ No newline at end of file
diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v
index 5fd324522..359659343 100644
--- a/src/Assembly/PseudoConversion.v
+++ b/src/Assembly/PseudoConversion.v
@@ -1,12 +1,12 @@
 
 Require Export Language Conversion QhasmCommon QhasmUtil.
 Require Export AlmostQhasm Pseudo State.
-Require Export Bedrock.Word.
-Require Export List.
+Require Export Bedrock.Word NArith NPeano.
+Require Export List Sumbool.
 Require Vector.
 
 Module PseudoConversion (M: PseudoMachine).
-  Import QhasmCommon AlmostQhasm State.
+  Import QhasmCommon AlmostQhasm State Util.
   Import ListNotations.
 
   Module P := Pseudo M.
@@ -34,15 +34,75 @@ Module PseudoConversion (M: PseudoMachine).
                        (NatM.elements stackState))
       end.
 
-    Fixpoint convertProgram' {n m} (prog: Pseudo n m): option AlmostQhasm.Program :=
+    Definition dec_lt (a b: nat): {(a < b)%nat} + {(a >= b)%nat}.
+      assert ({(a <? b)%nat = true} + {(a <? b)%nat <> true})
+        by abstract (destruct (a <? b)%nat; intuition);
+        destruct H.
+
+      - left; abstract (apply Nat.ltb_lt in e; intuition).
+
+      - right; abstract (rewrite Nat.ltb_lt in n; intuition).
+    Defined.
+
+    Inductive Mapping :=
+      | regM: forall (r: IReg width) (v: nat), v = getIRegIndex r -> Mapping
+      | stackM: forall (r: Stack width) (v: nat), v = getStackIndex r -> Mapping.
+
+    Definition natM (x: nat): Mapping.
+      refine (
+        let N := activeRegisters in
+        let r := (ireg x) in
+        let s := (stack (x - N)) in
+
+        if (dec_lt x N)
+        then (regM r (getIRegIndex r) _)
+        else (stackM s (getStackIndex s) _));
+      abstract intuition.
+    Defined.
+
+    Definition freshN (cur: list nat): nat :=
+      let range := (fix f (x: nat) :=
+        match x with
+        | O => []
+        | S x' => cons ((length cur) - x) (f x')
+        end) in
+
+      let curRange := (range (length cur)) in
+
+      let notInCur := fun x =>
+        negb (proj1_sig (bool_of_sumbool
+          (in_dec Nat.eq_dec x cur))) in
+
+      let options := filter notInCur curRange in
+
+      match options with
+      | cons x xs => x
+      | nil => O (* will never happen. TODO (rsloan): False_rec this *)
+      end.
+
+    Fixpoint convertProgram' {n m} (prog: Pseudo n m) (mapping: list nat): option AlmostQhasm.Program :=
+      let option_map' := fun x f => option_map f x in
       match prog with
       | PVar n i =>
-        (AAssign (ARegRegInt width (ireg 0) (ireg i)))
+        option_map' (nth_error mapping n) (fun v =>
+          match (natM v) with
+          | regM r v _ =>
+            AAssign (ARegRegInt width (ireg 0) r)
+          | stackM s v _ =>
+            AAssign (ARegStackInt width (ireg 0) s)
+          end)
 
       | PConst n c =>
-        (AAssign (AConstInt (ireg n) (iconst c)))
-
-      | PBin n m o a b => None
+        Some (AAssign (AConstInt width (ireg 0) (iconst c)))
+
+      | PBin n m o a b =>
+        option_map' (nth_error mapping n) (fun v =>
+          match (natM v) with
+          | regM r v _ =>
+            AAssign (ARegRegInt width (ireg 0) r)
+          | stackM s v _ =>
+            AAssign (ARegStackInt width (ireg 0) s)
+          end)
 
       | PNat n o v => None
 
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index c2b68bc77..65831d80a 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -19,6 +19,10 @@ Notation "'contra'" := (False_rec _ _) : state_scope.
 Obligation Tactic := abstract intuition.
 
 (* Asm Types *)
+Inductive ISize: nat -> Type :=
+  | I32: ISize 32
+  | I64: ISize 64.
+
 Inductive IConst: nat -> Type :=
   | constInt32: word 32 -> IConst 32
   | constInt64: word 64 -> IConst 64.