Full pipeline working again

8 files changed, 246 insertions, 274 deletions

diff --git a/src/Assembly/AlmostConversion.v b/src/Assembly/AlmostConversion.v
index e1fc988f1..878aa37bf 100644
--- a/src/Assembly/AlmostConversion.v
+++ b/src/Assembly/AlmostConversion.v
@@ -6,7 +6,7 @@ Module AlmostConversion <: Conversion AlmostQhasm Qhasm.
   Import QhasmCommon AlmostQhasm Qhasm.
   Import ListNotations.
 
-  Fixpoint almostToQhasm' (prog: AlmostProgram) (lblStart: N): Qhasm.Program :=
+  Fixpoint almostToQhasm' (prog: AlmostProgram) (lblStart: N): list QhasmStatement :=
     let label0 := (lblStart * 2)%N in
     let label1 := (label0 + 1)%N in
 
@@ -44,13 +44,21 @@ Module AlmostConversion <: Conversion AlmostQhasm Qhasm.
     | ACall lbl => [QCall lbl]
     end.
 
-  Definition convertProgram (prog: AlmostQhasm.Program) := Some (almostToQhasm' prog 0%N).
-  Definition convertState (st: Qhasm.State): option AlmostQhasm.State := Some st.
+  Transparent Qhasm.Program AlmostQhasm.Program.
 
-  Lemma convert_spec:  forall a a' b b' prog prog',
-    convertProgram prog = Some prog' ->
-    convertState a = Some a' -> convertState b = Some b' ->
-    Qhasm.evaluatesTo prog' a b <-> AlmostQhasm.evaluatesTo prog a' b'.
+  Definition convertProgram x y (prog: AlmostQhasm.Program x):
+      option (Qhasm.Program y) :=
+    Some (almostToQhasm' prog 0%N).
+
+  Definition convertState x y (st: Qhasm.State y):
+      option (AlmostQhasm.State x) :=
+    Some st.
+
+  Lemma convert_spec: forall pa pb a a' b b' prog prog',
+    convertProgram pa pb prog = Some prog' ->
+    convertState pa pb a = Some a' ->
+    convertState pa pb b = Some b' ->
+    Qhasm.evaluatesTo pb prog' a b <-> AlmostQhasm.evaluatesTo pa prog a' b'.
   Admitted.
 
 End AlmostConversion.
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
index b0cd4018e..acdfc3b03 100644
--- a/src/Assembly/Pipeline.v
+++ b/src/Assembly/Pipeline.v
@@ -4,16 +4,20 @@ Require Import Pseudo Qhasm AlmostQhasm Conversion Language.
 Require Import PseudoConversion AlmostConversion StringConversion.
 
 Module Pipeline.
-  Export Pseudo Util.
+  Export Util AlmostQhasm Qhasm QhasmString.
+  Export Pseudo.
 
-  Definition toAlmost (p: Pseudo inVars outVars): option AlmostQhasm.Program :=
-    PseudoConversion.convertProgram p.
+  Transparent Pseudo.Program AlmostQhasm.Program Qhasm.Program QhasmString.Program.
+  Transparent Pseudo.Params AlmostQhasm.Params Qhasm.Params QhasmString.Params.
 
-  Definition toQhasm (p: Pseudo inVars outVars): option Qhasm.Program :=
-    omap (toAlmost p) AlmostConversion.convertProgram.
+  Definition toAlmost {w s n m} (p: @Pseudo w s n m) : option AlmostProgram :=
+    PseudoConversion.convertProgram (mkParams w s n m) tt p.
 
-  Definition toString (p: Pseudo inVars outVars): option string :=
-    omap (toQhasm p) StringConversion.convertProgram.
+  Definition toQhasm {w s n m} (p: @Pseudo w s n m) : option (list QhasmStatement) :=
+    omap (toAlmost p) (AlmostConversion.convertProgram tt tt).
+
+  Definition toString {w s n m} (p: @Pseudo w s n m) : option string :=
+    omap (toQhasm p) (StringConversion.convertProgram tt tt).
 End Pipeline.
 
 Module PipelineExample.
@@ -21,13 +25,7 @@ Module PipelineExample.
 
   Program Definition asdf: Program Unary32 := ($0 :+: $0)%p.
 
-  Definition exStr := Pipeline.toString ex.
-    | Some x => x
-    | None => EmptyString
-    end.
-  Defined.
-
-Open Scope string_scope.
-Print Result.
+  Definition exStr := Pipeline.toString asdf.
 
-Extraction "Result.ml" Result.
+  Eval vm_compute in exStr.
+End PipelineExample.
diff --git a/src/Assembly/PipelineExample.v b/src/Assembly/PipelineExample.v
deleted file mode 100644
index 8f7d43b9d..000000000
--- a/src/Assembly/PipelineExample.v
+++ /dev/null
@@ -1,53 +0,0 @@
-
-Require Import QhasmCommon QhasmEvalCommon.
-Require Import Pseudo Qhasm AlmostQhasm Medial Conversion Language.
-Require Import PseudoMedialConversion AlmostConversion StringConversion.
-
-Extraction Language Ocaml.
-Require Import ExtrOcamlString ExtrOcamlBasic.
-Require Import Coq.Strings.String.
-
-Module Progs.
-  Module Arch := PseudoUnary32.
-  Module C32 := PseudoMedialConversion Arch.
-
-  Import C32.P.
-
-  Definition omap {A B} (f: A -> option B) (x: option A): option B :=
-    match x with
-    | Some v => f v
-    | None => None
-    end.
-
-  Definition prog0: C32.P.Program.
-    refine
-      (PBin _ Add (PComb _ _ _
-        (PVar 1 (exist _ 0 _))
-        (PConst _ (natToWord _ 1)))); abstract intuition.
-  Defined.
-
-  Definition prog1: option C32.M.Program :=
-    C32.PseudoConversion.convertProgram prog0.
-
-  Definition prog2: option AlmostQhasm.Program :=
-    omap C32.MedialConversion.convertProgram prog1.
-
-  Definition prog3: option Qhasm.Program :=
-    omap AlmostConversion.convertProgram prog2.
-
-  Definition prog4: option string :=
-    omap StringConversion.convertProgram prog3.
-End Progs.
-
-Definition Result: string.
-  let res := eval vm_compute in (
-    match Progs.prog4 with
-    | Some x => x
-    | None => EmptyString
-    end) in exact res.
-Defined.
-
-Open Scope string_scope.
-Print Result.
-
-Extraction "Result.ml" Result.
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index c4249804d..ede9607cf 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -5,19 +5,20 @@ Require Import List.
 Module Pseudo <: Language.
   Import EvalUtil ListState Util.
 
-  Inductive Pseudo {w: nat} {spec: Width w}: nat -> nat -> Type :=
+  Inductive Pseudo {w: nat} {s: Width w}: nat -> nat -> Type :=
     | PVar: forall n, option bool -> Index n -> Pseudo n 1
-    | PMem: forall n m, Index n -> Index m -> Pseudo n 1
+    | PMem: forall n m , Index n -> Index m -> Pseudo n 1
     | PConst: forall n, word w -> Pseudo n 1
     | PBin: forall n, IntOp -> Pseudo n 2 -> Pseudo n 1
     | PDual: forall n, DualOp -> Pseudo n 2 -> Pseudo n 2
     | PCarry: forall n, CarryOp -> Pseudo n 2 -> Pseudo n 1
     | PShift: forall n, RotOp -> Index w -> Pseudo n 1 -> Pseudo n 1
-    | PIf: forall n m, TestOp -> Index n -> Index n -> Pseudo n m -> Pseudo n m -> Pseudo n m
     | PFunExp: forall n, Pseudo n n -> nat -> Pseudo n n
     | PLet: forall n k m, Pseudo n k -> Pseudo (n + k) m -> Pseudo n m
     | PComb: forall n a b, Pseudo n a -> Pseudo n b -> Pseudo n (a + b)
-    | PCall: forall n m, Label -> Pseudo n m -> Pseudo n m.
+    | PCall: forall n m, Label -> Pseudo n m -> Pseudo n m
+    | PIf: forall n m, TestOp -> Index n -> Index n ->
+                  Pseudo n m -> Pseudo n m -> Pseudo n m.
 
   Hint Constructors Pseudo.
 
@@ -110,7 +111,6 @@ Module Pseudo <: Language.
       pseudoEval prog st = Some st'.
 
   Delimit Scope pseudo_notations with p.
-  Open Scope pseudo_notations.
 
   Definition indexize (n: nat) (p: (n > 0)%nat) (x: nat): Index n.
     intros; exists (x mod n);
@@ -123,7 +123,7 @@ Module Pseudo <: Language.
   Notation "$ A" := (PVar _ (Some true) (indexize _ _ A))
     (at level 20, right associativity) : pseudo_notations.
 
-  Notation "'MEM' ( A , B )" :=  (PMem _ _ (indexize _ _ A) (indexize _ _ B))
+  Notation "A :[ B ]:" :=  (PMem _ _ (indexize _ _ A) (indexize _ _ B))
     (at level 20, right associativity) : pseudo_notations.
 
   Notation "# A" := (PConst _ (natToWord _ A))
@@ -144,35 +144,32 @@ Module Pseudo <: Language.
   Notation "A :^: B" := (PBin _ Xor (PComb _ _ _ A B))
     (at level 45, right associativity) : pseudo_notations.
 
-  Notation "A :|: B" := (PBin _ Or (PComb _ _ _ A B))
-    (at level 60, right associativity) : pseudo_notations.
-
   Notation "A :>>: B" := (PShift _ Shr (indexize _ _ B) A)
     (at level 60, right associativity) : pseudo_notations.
 
   Notation "A :<<: B" := (PShift _ Shl (indexize _ _ B) A)
     (at level 60, right associativity) : pseudo_notations.
 
-  Notation "A :**: B" := (PDual _ Mult (PComb _ _ _ A B))
+  Notation "A :*: B" := (PDual _ Mult (PComb _ _ _ A B))
     (at level 55, right associativity) : pseudo_notations.
 
-  Notation "'IF' O ( A , B ) 'THEN' L 'ELSE' R" :=
+  Notation "O :( A , B ): :?: L ::: R" :=
     (PIf _ _ O (indexize _ _ A) (indexize _ _ B) L R)
-    (at level 70, left associativity) : pseudo_notations.
+    (at level 70, right associativity) : pseudo_notations.
 
-  Notation "'EXP' ( e ) ( F )" :=
+  Notation "F :**: e" :=
     (PFunExp _ F e)
-    (at level 70, left associativity) : pseudo_notations.
+    (at level 70, right associativity) : pseudo_notations.
 
-  Notation "'LET' E 'IN' F" :=
+  Notation "E :->: F" :=
     (PLet _ _ _ E F)
-    (at level 70, left associativity) : pseudo_notations.
+    (at level 70, right associativity) : pseudo_notations.
 
-  Notation "A | B" :=
+  Notation "A :|: B" :=
     (PComb _ _ _ A B)
     (at level 65, left associativity) : pseudo_notations.
 
-  Notation "'CALL' n ::: A" :=
+  Notation "n ::: A :():" :=
     (PCall _ _ n A)
     (at level 65, left associativity) : pseudo_notations.
 End Pseudo.
diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v
index 39b655e47..65c80a960 100644
--- a/src/Assembly/PseudoConversion.v
+++ b/src/Assembly/PseudoConversion.v
@@ -1,185 +1,202 @@
-
 Require Export Language Conversion QhasmEvalCommon QhasmUtil.
 Require Export Pseudo AlmostQhasm State.
-Require Export Bedrock.Word NArith NPeano Euclid.
-Require Export List Sumbool Vector.
+Require Import Bedrock.Word NArith NPeano Euclid.
+Require Import List Sumbool Vector.
 
 Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
-  Import QhasmCommon AlmostQhasm EvalUtil Util Pseudo StateCommon.
-  Import ListNotations.
-
-  Definition MMap {w} := NatM.t (Mapping w).
-  Definition mempty {w} := NatM.empty (Mapping w).
-
-  Definition FMap {w} := NatM.t (AlmostProgram * (list (Mapping w))).
-  Definition fempty {w} := NatM.empty (AlmostProgram * (list (Mapping w))).
-
-  Definition getStart {w s n m} (prog: @Pseudo w s n m) :=
-    let ns := (fix getStart' {n' m'} (p': @Pseudo w s n' m') :=
-      match p' with
-      | PVar _ _ i => [proj1_sig i]
-      | PBin _ _ p => getStart' p
-      | PDual _ _ p => getStart' p
-      | PCarry _ _ p => getStart' p
-      | PShift _ _ _ p => getStart' p
-      | PIf _ _ _ _ _ l r => (getStart' l) ++ (getStart' r)
-      | PFunExp _ p _ => getStart' p
-      | PLet _ k _ a b => (n + k) :: (getStart' a) ++ (getStart' b)
-      | PComb _ _ _ a b => (getStart' a) ++ (getStart' b)
-      | PCall _ _ _ p => getStart' p
-      | _ => []
-      end) _ _ prog in
-
-    maxN (n :: m :: ns).
-
-  Definition addMap {T} (a b: NatM.t T): NatM.t T :=
-    (fix add' (m: NatM.t T) (elts: list (nat * T)%type) :=
-      match elts with
-      | [] => m
-      | (k, v) :: elts' => add' (NatM.add k v m) elts'
-      end) a (NatM.elements b).
-
-  Fixpoint convertProgram' {n m} (prog: Pseudo n m) (start: nat) (M: MMap) (F: FMap):
-      option (AlmostProgram * (list (Mapping width)) * MMap * FMap) :=
-    let rM := fun (x: nat) => regM _ (reg width_spec x) in
-    let sM := fun (x: nat) => stackM _ (stack width_spec x) in
-
-    let reg' := reg width_spec in
-    let stack' := stack width_spec in
-    let const' := const width_spec in
-
-    let G := fun (k: nat) =>
-      match (NatM.find k M) with
-      | Some v => v
-      | _ => rM k (* TODO: more intelligent defaults *)
-      end in
-
-    let madd := fun (k: nat) (f: nat -> Mapping width) => NatM.add k (f k) in
-    let fadd := fun (k: nat) (f: AlmostProgram) (r: list (Mapping width)) => NatM.add k (f, r) in
-
-    match prog with
-    | PVar n (Some true) i => Some (ASkip, [rM i], madd i rM M, F)
-    | PVar n (Some false) i => Some (ASkip, [sM i], madd i sM M, F)
-    | PVar n None i => Some (ASkip, [G i], M, F) 
-
-    | PConst n c => Some (AAssign (AConstInt (reg' start) (const' c)),
-                         [rM start], madd start rM M, F)
-
-    | PMem n m v i => Some (AAssign (ARegMem (reg' start) (mem width_spec v) i),
-                           [rM start], madd start rM M, F)
-
-    | PBin n o p =>
-      match (convertProgram' p start M F) with
-      | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
-        Some (ASeq p' (AOp (IOpReg o (reg' a) (reg' b))),
-              [rM a], madd a rM (madd b rM M'), F')
-
-      | Some (p', [regM (reg _ _ a); constM c], M', F') =>
-        Some (ASeq p' (AOp (IOpConst o (reg' a) c)),
-              [rM a], madd a rM M', F')
-
-      | Some (p', [regM (reg _ _ a); memM _ b i], M', F') =>
-        Some (ASeq p' (AOp (IOpMem o (reg' a) b i)),
-              [rM a], madd a rM M', F')
-
-      | Some (p', [regM (reg _ _ a); stackM (stack _ _ b)], M', F') =>
-        Some (ASeq p' (AOp (IOpStack o (reg' a) (stack' b))),
-              [rM a], madd a rM (madd b sM M'), F')
-
-      | _ => None
-      end
+  Import AlmostQhasm EvalUtil ListState Util Pseudo ListNotations.
+
+  Section Conv.
+    Variable w: nat.
+    Variable s: Width w.
+
+    Definition MMap := NatM.t (Mapping w).
+    Definition mempty := NatM.empty (Mapping w).
+
+    Definition FMap := NatM.t (AlmostProgram * (list (Mapping w))).
+    Definition fempty := NatM.empty (AlmostProgram * (list (Mapping w))).
+
+    Definition getStart {n m} (prog: @Pseudo w s n m) :=
+      let ns := (fix getStart' {n' m'} (prog': @Pseudo w s n' m') :=
+        match prog' with
+        | PVar _ _ i => [proj1_sig i]
+        | PBin _ _ p => getStart' p
+        | PDual _ _ p => getStart' p
+        | PCarry _ _ p => getStart' p
+        | PShift _ _ _ p => getStart' p
+        | PFunExp _ p _ => getStart' p
+        | PCall _ _ _ p => getStart' p
+        | PIf _ _ _ _ _ l r => (getStart' l) ++ (getStart' r)
+        | PLet _ k _ a b => (n + k) :: (getStart' a) ++ (getStart' b)
+        | PComb _ _ _ a b => (getStart' a) ++ (getStart' b)
+        | _ => []
+        end) _ _ prog in
+
+      (fix maxN (lst: list nat) :=
+        match lst with
+        | [] => O
+        | x :: xs => max x (maxN xs)
+        end) (n :: m :: ns).
+
+    Definition addMap {T} (a b: (NatM.t T)) : NatM.t T :=
+      (fix add' (m: NatM.t T) (elts: list (nat * T)%type) :=
+        match elts with
+        | [] => m
+        | (k, v) :: elts' => add' (NatM.add k v m) elts'
+        end) a (NatM.elements b).
+
+    Fixpoint convertProgram' {n m} (prog: @Pseudo w s n m) (start: nat) (M: MMap) (F: FMap) :
+        option (AlmostProgram * (list (Mapping w)) * MMap * FMap) :=
+
+      let rM := fun (x: nat) => regM _ (reg s x) in
+      let sM := fun (x: nat) => stackM _ (stack s x) in
+      let reg' := reg s in
+      let stack' := stack s in
+      let const' := constant s in
+
+      let G := fun (k: nat) =>
+        match (NatM.find k M) with
+        | Some v => v
+        | _ => rM k (* TODO: more intelligent defaults *)
+        end in
+
+      let madd := fun (k: nat) (f: nat -> Mapping w) =>
+        NatM.add k (f k) in
+
+      let fadd := fun (k: nat) (f: AlmostProgram) (r: list (Mapping w)) =>
+        NatM.add k (f, r) in
+
+      match prog with
+      | PVar n (Some true) i => Some (ASkip, [rM i], madd i rM M, F)
+      | PVar n (Some false) i => Some (ASkip, [sM i], madd i sM M, F)
+      | PVar n None i => Some (ASkip, [G i], M, F) 
+
+      | PConst n c =>
+        Some (AAssign (AConstInt (reg' start) (const' c)),
+                       [rM start], madd start rM M, F)
+
+      | PMem n m v i =>
+        Some (AAssign (ARegMem (reg' start) (mem s v) i),
+                       [rM start], madd start rM M, F)
+
+      | PBin n o p =>
+        match (convertProgram' p start M F) with
+        | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
+            Some (ASeq p' (AOp (IOpReg o (reg' a) (reg' b))),
+                [rM a], madd a rM (madd b rM M'), F')
+
+        | Some (p', [regM (reg _ _ a); constM c], M', F') =>
+            Some (ASeq p' (AOp (IOpConst o (reg' a) c)),
+                [rM a], madd a rM M', F')
+
+        | Some (p', [regM (reg _ _ a); memM _ b i], M', F') =>
+            Some (ASeq p' (AOp (IOpMem o (reg' a) b i)),
+                [rM a], madd a rM M', F')
+
+        | Some (p', [regM (reg _ _ a); stackM (stack _ _ b)], M', F') =>
+            Some (ASeq p' (AOp (IOpStack o (reg' a) (stack' b))),
+                [rM a], madd a rM (madd b sM M'), F')
+
+        | _ => None
+        end
 
-    | PCarry n o p =>
-      match (convertProgram' p start M F) with
-      | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
-        Some (ASeq p' (AOp (COp o (reg' a) (reg' b))),
-              [rM a], madd a rM (madd b rM M'), F')
+      | PCarry n o p =>
+        match (convertProgram' p start M F) with
+        | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
+            Some (ASeq p' (AOp (COp o (reg' a) (reg' b))),
+                [rM a], madd a rM (madd b rM M'), F')
 
-      | _ => None
-      end
+        | _ => None
+        end
 
-    | PDual n o p =>
-      match (convertProgram' p (S start) M F) with
-      | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
-        Some (ASeq p' (AOp (DOp o (reg' a) (reg' b) (Some (reg' start)))),
-              [rM a; rM start], madd a rM (madd b rM (madd start rM M')), F')
+      | PDual n o p =>
+        match (convertProgram' p (S start) M F) with
+        | Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
+            Some (ASeq p' (AOp (DOp o (reg' a) (reg' b) (Some (reg' start)))),
+                [rM a; rM start], madd a rM (madd b rM (madd start rM M')), F')
 
-      | _ => None
-      end
+        | _ => None
+        end
 
-    | PShift n o x p =>
-      match (convertProgram' p start M F) with
-      | Some (p', [regM (reg _ _ a)], M', F') =>
-        Some (ASeq p' (AOp (ROp o (reg' a) x)),
-              [rM a], madd a rM M', F')
+      | PShift n o x p =>
+        match (convertProgram' p start M F) with
+        | Some (p', [regM (reg _ _ a)], M', F') =>
+            Some (ASeq p' (AOp (ROp o (reg' a) x)),
+                [rM a], madd a rM M', F')
 
-      | _ => None
-      end
+        | _ => None
+        end
 
-    | PLet n k m f g =>
-      match (convertProgram' f start M F) with
-      | None => None
-      | Some (fp, fm, M', F') =>
-        match (convertProgram' g (start + (length fm)) M' F') with
+      | PLet n k m f g =>
+        match (convertProgram' f start M F) with
         | None => None
-        | Some (gp, gm, M'', F'') => Some (ASeq fp gp, gm, M'', F'')
+        | Some (fp, fm, M', F') =>
+            match (convertProgram' g (start + (length fm)) M' F') with
+            | None => None
+            | Some (gp, gm, M'', F'') => Some (ASeq fp gp, gm, M'', F'')
+            end
         end
-      end
 
-    | PComb n a b f g => 
-      match (convertProgram' f start M F) with
-      | None => None
-      | Some (fp, fm, M', F') =>
-        match (convertProgram' g (start + (length fm)) M' F') with
+      | PComb n a b f g => 
+        match (convertProgram' f start M F) with
         | None => None
-        | Some (gp, gm, M'', F'') => Some (ASeq fp gp, fm ++ gm, M'', F'')
+        | Some (fp, fm, M', F') =>
+            match (convertProgram' g (start + (length fm)) M' F') with
+            | None => None
+            | Some (gp, gm, M'', F'') => Some (ASeq fp gp, fm ++ gm, M'', F'')
+            end
         end
-      end
 
-    | PIf n m o i0 i1 l r => 
-      match (convertProgram' l start M F) with
-      | None => None
-      | Some (lp, lr, lM, lF) =>
-
-        match (convertProgram' r start lM lF) with
+      | PIf n m o i0 i1 l r => 
+        match (convertProgram' l start M F) with
         | None => None
-        | Some (rp, rr, M', F') =>
-
-          if (list_eq_dec mapping_dec lr rr)
-          then
-            match (G (proj1_sig i0), G (proj1_sig i1)) with
-            | (regM r0, regM r1) => Some (ACond (CReg _ o r0 r1) lp rp, lr, M', F')
-            | (regM r, constM c) => Some (ACond (CConst _ o r c) lp rp, lr, M', F')
-            | _ => None
+        | Some (lp, lr, lM, lF) =>
+
+            match (convertProgram' r start lM lF) with
+            | None => None
+            | Some (rp, rr, M', F') =>
+
+            if (list_eq_dec mapping_dec lr rr)
+            then
+                match (G (proj1_sig i0), G (proj1_sig i1)) with
+                | (regM r0, regM r1) => Some (ACond (CReg _ o r0 r1) lp rp, lr, M', F')
+                | (regM r, constM c) => Some (ACond (CConst _ o r c) lp rp, lr, M', F')
+                | _ => None
+                end
+            else None
             end
-          else None
         end
-      end
 
-    | PFunExp n f e => 
-      match (convertProgram' f (S start) M F) with
-      | Some (fp, fr, M', F') => 
-        let a := start in
-        Some (ASeq
-          (AAssign (AConstInt (reg' a) (const' (natToWord _ O))))
-          (AWhile (CConst _ TLt (reg' a) (const' (natToWord _ e)))
-            (ASeq fp (AOp (IOpConst Add (reg' a) (const' (natToWord _ 1)))))),
-          fr, madd a rM M', F')
+      | PFunExp n f e => 
+        match (convertProgram' f (S start) M F) with
+        | Some (fp, fr, M', F') => 
+            let a := start in
+            Some (ASeq
+            (AAssign (AConstInt (reg' a) (const' (natToWord _ O))))
+            (AWhile (CConst _ TLt (reg' a) (const' (natToWord _ e)))
+                (ASeq fp (AOp (IOpConst Add (reg' a) (const' (natToWord _ 1)))))),
+            fr, madd a rM M', F')
+
+        | _ => None
+        end
 
-      | _ => None
-      end
- 
-    | PCall n m lbl f =>
-      match (convertProgram' f start M F) with
-      | Some (fp, fr, M', F') =>
-        let F'' := NatM.add lbl (fp, fr) F' in
-        Some (ACall lbl, fr, M', F'')
-      | None => None
+      | PCall n m lbl f =>
+        match (convertProgram' f start M F) with
+        | Some (fp, fr, M', F') =>
+            let F'' := NatM.add lbl (fp, fr) F' in
+            Some (ACall lbl, fr, M', F'')
+        | None => None
       end
     end.
 
-  Definition convertProgram (prog: Pseudo inVars outVars): option AlmostProgram := 
-    match (convertProgram' prog (max inVars outVars) mempty fempty) with
+  End Conv.
+
+  Definition convertProgram x y (prog: Program x) : option (AlmostQhasm.Program y) := 
+    let vs := max (inputs x) (outputs x) in
+    let M0 := mempty (width x) in
+    let F0 := fempty (width x) in
+
+    match (convertProgram' (width x) (spec x) prog vs M0 F0) with
     | Some (prog', _, M, F) =>
       Some (fold_left
            (fun p0 t => match t with | (k, (v, _)) => ADef k v p0 end)
@@ -188,15 +205,15 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
     | _ => None
     end.
 
-  Fixpoint convertState (st: AlmostQhasm.State): option State :=
-    let vars := max inVars outVars in
+  Fixpoint convertState x y (st: AlmostQhasm.State y) : option (State x) :=
+    let vars := max (inputs x) (outputs x) in
 
     let try_cons := fun {T} (x: option T) (l: list T) =>
       match x with | Some x' => x' :: l | _ => l end in
 
     let get := fun i =>
-      match (FullState.getReg (reg width_spec i) st,
-             FullState.getStack (stack width_spec i) st) with
+      match (FullState.getReg (reg (spec x) i) st,
+             FullState.getStack (stack (spec x) i) st) with
       | (Some v, _) => Some v
       | (_, Some v) => Some v
       | _ => None
@@ -212,9 +229,10 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
       else None
     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 <-> evaluatesTo prog a' b'.
+  Lemma convert_spec: forall pa pb a a' b b' prog prog',
+    convertProgram pa pb prog = Some prog' ->
+    convertState pa pb a = Some a' ->
+    convertState pa pb b = Some b' ->
+    AlmostQhasm.evaluatesTo pb prog' a b <-> evaluatesTo pa prog a' b'.
   Admitted.
 End PseudoConversion.
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index 21f846cb5..654f109f3 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -19,7 +19,7 @@ Inductive Width: nat -> Type := | W32: Width 32 | W64: Width 64.
 
 (* A constant value *)
 Inductive Const: nat -> Type :=
-  | const: forall {n}, Width n -> word n -> Const n.
+  | constant: forall {n}, Width n -> word n -> Const n.
 
 (* A variable in any register *)
 Inductive Reg: nat -> Type :=
@@ -109,10 +109,10 @@ Definition memWidth {n m} (x: Mem n m): nat := n.
 Definition memLength {n m} (x: Mem n m): nat := m.
 
 Definition constValueW {n} (x: Const n): word n :=
-  match x with | @const n _ v => v end.
+  match x with | @constant n _ v => v end.
 
 Definition constValueN {n} (x: Const n): nat :=
-  match x with | @const n _ v => wordToNat v end.
+  match x with | @constant n _ v => wordToNat v end.
 
 Definition regName {n} (x: Reg n): nat :=
   match x with | @reg n _ v => v end.
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index b12e27e19..566d7b892 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -88,7 +88,7 @@ Module EvalUtil.
   (* Mapping Conversions *)
 
   Definition wordToM {n: nat} {spec: Width n} (w: word n): Mapping n :=
-    constM _ (const spec w).
+    constM _ (constant spec w).
 
   Definition regToM {n: nat} {spec: Width n} (r: Reg n): Mapping n :=
     regM _ r.
diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v
index 151eaa3f7..f3ff40ff7 100644
--- a/src/Assembly/StringConversion.v
+++ b/src/Assembly/StringConversion.v
@@ -5,17 +5,18 @@ Require Import NArith NPeano.
 Require Export Bedrock.Word.
 
 Module QhasmString <: Language.
-  Definition Program := string.
-  Definition State := unit.
+  Definition Params := unit.
+  Definition Program := fun (_: Params) => string.
+  Definition State := fun (_: Params) => unit.
 
-  Definition evaluatesTo (p: Program) (i o: State): Prop := True.
+  Definition evaluatesTo x (p: Program x) (i o: State x): Prop := True.
 End QhasmString.
 
 Module StringConversion <: Conversion Qhasm QhasmString.
   Import Qhasm ListNotations.
 
   (* The easy one *)
-  Definition convertState (st: QhasmString.State): option Qhasm.State := None.
+  Definition convertState x y (st: QhasmString.State y): option (Qhasm.State x) := None.
 
   (* Hexadecimal Primitives *)
 
@@ -62,7 +63,7 @@ Module StringConversion <: Conversion Qhasm QhasmString.
       "0x" ++ (nToHex (wordToN w)).
 
     Coercion constToString {n} (c: Const n): string :=
-      match c with | const _ _ w => wordToString w end.
+      match c with | constant _ _ w => wordToString w end.
 
     Coercion regToString {n} (r: Reg n): string :=
       match r with
@@ -191,7 +192,7 @@ Module StringConversion <: Conversion Qhasm QhasmString.
     Arguments memM [n m] x i.
     Arguments constM [n] x.
 
-    Fixpoint entries (width: nat) (prog: Program): list (Mapping width) :=
+    Fixpoint entries (width: nat) (prog: list QhasmStatement): list (Mapping width) :=
       match prog with
       | cons s next =>
         match s with
@@ -354,7 +355,9 @@ Module StringConversion <: Conversion Qhasm QhasmString.
     | QRet => [("pop %eip")%string]
     end.
 
-  Definition convertProgram (prog: Qhasm.Program): option string :=
+  Transparent Qhasm.Program QhasmString.Program.
+
+  Definition convertProgram x y (prog: Qhasm.Program x): option (QhasmString.Program y) :=
     let decls := fun x => flatMapList (dedup (entries x prog))
       (compose optionToList mappingDeclaration) in
 
@@ -374,10 +377,11 @@ Module StringConversion <: Conversion Qhasm QhasmString.
        stmts ++ blank ++
        leave ++ blank) EmptyString).
 
-  Lemma convert_spec: forall a a' b b' prog prog',
-    convertProgram prog = Some prog' ->
-    convertState a = Some a' -> convertState b = Some b' ->
-    QhasmString.evaluatesTo prog' a b <-> Qhasm.evaluatesTo prog a' b'.
+  Lemma convert_spec: forall pa pb a a' b b' prog prog',
+    convertProgram pa pb prog = Some prog' ->
+    convertState pa pb a = Some a' ->
+    convertState pa pb b = Some b' ->
+    QhasmString.evaluatesTo pb prog' a b <-> Qhasm.evaluatesTo pa prog a' b'.
   Admitted.
 
 End StringConversion.