A little progress on PseudoConversion

2 files changed, 75 insertions, 37 deletions

diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index 9e0fda947..ae7ccbf60 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -2,18 +2,17 @@ Require Import QhasmEvalCommon QhasmUtil.
 Require Import Language.
 Require Import List.
 
-Module Type Pseudo <: Language.
-  Import ListNotations State Util.
-
-  (* Input/output specification *)
+Module Type PseudoMachine.
   Parameter width: nat.
   Parameter vars: nat.
+  Parameter izero: IConst width.
+End PseudoMachine.
+
+Module Pseudo (M: PseudoMachine) <: Language.
+  Import ListNotations State Util M.
 
   Definition const: Type := word width.
 
-  (* Qhasm primitives we'll use *)
-  Parameter izero: IConst width.
-  
   Definition ireg: nat -> IReg width :=
     match izero with
     | constInt32 _ => regInt32
@@ -147,3 +146,18 @@ Module Type Pseudo <: Language.
 
   (* world peace *)
 End Pseudo.
+
+Module PseudoUnary32 <: PseudoMachine.
+  Definition width := 32.
+  Definition vars := 1.
+  Definition izero := constInt32 (wzero 32).
+  Definition const: Type := word width.
+End PseudoUnary32.
+
+Module PseudoUnary64 <: PseudoMachine.
+  Definition width := 64.
+  Definition vars := 1.
+  Definition izero := constInt64 (wzero 64).
+  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 c3f03195a..5fd324522 100644
--- a/src/Assembly/PseudoConversion.v
+++ b/src/Assembly/PseudoConversion.v
@@ -1,46 +1,70 @@
 
-Require Export Language Conversion QhasmCommon.
+Require Export Language Conversion QhasmCommon QhasmUtil.
 Require Export AlmostQhasm Pseudo State.
 Require Export Bedrock.Word.
 Require Export List.
 Require Vector.
 
-Module PseudoConversion (P: Pseudo) <: Conversion P AlmostQhasm.
-  Import QhasmCommon AlmostQhasm P State.
+Module PseudoConversion (M: PseudoMachine).
+  Import QhasmCommon AlmostQhasm State.
   Import ListNotations.
 
-  Definition convertState (st: AlmostQhasm.State): P.State :=
-    match st with
-    | fullState _ _ stackState _ =>
-      map (fun x => NToWord width (snd x)) (NatM.elements stackState)
+  Module P := Pseudo M.
+
+  Fixpoint take {A} (n: nat) (lst: list A) :=
+    match n with
+    | O => []
+    | S m =>
+      match lst with
+      | [] => []
+      | l :: ls => l :: (take m ls)
+      end
     end.
 
-  Fixpoint convertProgram' (prog: Pseudo): option AlmostQhasm.Program :=
-    match prog with
-    | PVar n i =>
-      (AAssign 
-    | PConst n c =>
-      (AAssign 
+  Module Conv <: Conversion P AlmostQhasm.
+    Import P M.
 
-    (* TODO (rsloan) *)
-    | PBin n m o a b => None
-    | PNat n o v => None
-    | PShift n o a x => None
+    Definition activeRegisters := 6.
+    Definition overflowReg := ireg 6.
 
-    | PLet n k m f g => None
-    | PComp n k m f g => None
-    | PComb n a b f g => None
+    Definition convertState (st: AlmostQhasm.State): P.State :=
+      match st with
+      | fullState _ stackState _ =>
+        take vars (map (fun x => NToWord width (snd x))
+                       (NatM.elements stackState))
+      end.
 
-    | PIf n m o i0 i1 l r => None
-    | PFunExp n f e => None
-    end.
+    Fixpoint convertProgram' {n m} (prog: Pseudo n m): option AlmostQhasm.Program :=
+      match prog with
+      | PVar n i =>
+        (AAssign (ARegRegInt width (ireg 0) (ireg i)))
+
+      | PConst n c =>
+        (AAssign (AConstInt (ireg n) (iconst c)))
+
+      | PBin n m o a b => None
+
+      | PNat n o v => None
+
+      | PShift n o a x => None
+
+      | PLet n k m f g => None
+
+      | PComp n k m f g => None
+
+      | PComb n a b f g => None
+
+      | PIf n m o i0 i1 l r => None
+
+      | PFunExp n f e => None
 
-  convertProgram (prog: S.Program): option AlmostQhasm.Program :=
+      end.
 
-  Lemma convert_spec:  forall a a' b b' prog prog',
-    convertProgram prog = Some prog' ->
-    convertState a = Some a' -> convertState b = Some b' ->
-    AlmostQhasm.evaluatesTo prog' a b <-> Pseudo.evaluatesTo prog a' b'.
-  Admitted.
+    Lemma convert_spec:  forall a a' b b' prog prog',
+      convertProgram prog = Some prog' ->
+      convertState a = Some a' -> convertState b = Some b' ->
+      AlmostQhasm.evaluatesTo prog' a b <-> P.evaluatesTo prog a' b'.
+    Admitted.
 
-End GallinaConversion.
+  End Conv.
+End PseudoConversions.