More refactors that will make this whole thing very unstable

2 files changed, 165 insertions, 13 deletions

diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index ce2c5878a..1f127f665 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -15,7 +15,8 @@ Module Pseudo (M: PseudoMachine) <: Language.
 
   (* Program Types *)
   Inductive Pseudo: nat -> nat -> Type :=
-    | PVar: forall n, Index n -> Pseudo n 1
+    (* Some true for registers, false for stack, None for default *)
+    | PVar: forall n, option bool -> Index n -> Pseudo n 1
     | PMem: forall n m, Index n -> Index m -> Pseudo n 1
     | PConst: forall n, const -> Pseudo n 1
 
@@ -38,7 +39,7 @@ Module Pseudo (M: PseudoMachine) <: Language.
 
   Fixpoint pseudoEval {n m} (prog: Pseudo n m) (st: State): option State :=
     match prog with
-    | PVar n i => omap (getVar i st) (fun x => Some (setList [x] st))
+    | PVar n _ i => omap (getVar i st) (fun x => Some (setList [x] st))
     | PMem n m v i => omap (getMem v i st) (fun x => Some (setList [x] st))
     | PConst n c => Some (setList [c] st)
     | PBin n o p =>
@@ -110,7 +111,73 @@ Module Pseudo (M: PseudoMachine) <: Language.
     Delimit Scope pseudo_notations with p.
     Open Scope pseudo_notations.
 
-    Notation "'LET' A := B 'IN' C" (at level 60, right associativity) : pseudo_notations.
+    Definition indexize (n: nat) (p: (n > 0)%nat) (x: nat): Index n.
+      intros; exists (x mod n);
+        abstract (pose proof (mod_bound_pos x n); omega).
+    Defined.
+
+    Notation "% A" := (PVar _ (Some false) (indexize _ _ A))
+      (at level 20, right associativity) : pseudo_notations.
+
+    Notation "$ A" := (PVar _ (Some true) (indexize _ _ A))
+      (at level 20, right associativity) : pseudo_notations.
+
+    Notation "'MEM' ( A , B )" :=  (PMem _ _ (indexize _ _ A) (indexize _ _ B))
+      (at level 20, right associativity) : pseudo_notations.
+
+    Notation "# A" := (PConst _ (natToWord _ A))
+      (at level 20, right associativity) : pseudo_notations.
+
+    Notation "A :+: B" := (PBin _ Add (PComb _ _ _ A B))
+      (at level 60, right associativity) : pseudo_notations.
+
+    Notation "A :+c: B" := (PCarry _ AddWithCarry (PComb _ _ _ A B))
+      (at level 60, right associativity) : pseudo_notations.
+
+    Notation "A :-: B" := (PBin _ Sub (PComb _ _ _ A B))
+      (at level 60, right associativity) : pseudo_notations.
+
+    Notation "A :&: B" := (PBin _ And (PComb _ _ _ A B))
+      (at level 45, right associativity) : pseudo_notations.
+
+    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))
+      (at level 55, right associativity) : pseudo_notations.
+
+    Notation "'IF' O ( A , B ) 'THEN' L 'ELSE' R" :=
+      (PIf _ _ O (indexize _ _ A) (indexize _ _ B) L R)
+      (at level 70, left associativity) : pseudo_notations.
+
+    Notation "'EXP' ( e ) ( F )" :=
+      (PFunExp _ F e)
+      (at level 70, left associativity) : pseudo_notations.
+
+    Notation "'LET' E 'IN' F" :=
+      (PLet _ _ _ E F)
+      (at level 70, left associativity) : pseudo_notations.
+
+    Notation "A | B" :=
+      (PComb _ _ _ A B)
+      (at level 65, left associativity) : pseudo_notations.
+
+    Notation "'CALL' n ::: A" :=
+      (PCall _ _ n A)
+      (at level 65, left associativity) : pseudo_notations.
+
+    Definition p0: Pseudo 1 2.
+      refine (CALL 0 ::: %0 :**: $0); intuition.
+    Defined.
   End Notations.
 
   (* world peace *)
diff --git a/src/Assembly/PseudoMedialConversion.v b/src/Assembly/PseudoMedialConversion.v
index 055c6d1bf..a2ec6fe40 100644
--- a/src/Assembly/PseudoMedialConversion.v
+++ b/src/Assembly/PseudoMedialConversion.v
@@ -1,24 +1,22 @@
 
 Require Export Language Conversion QhasmEvalCommon QhasmUtil.
-Require Export Pseudo Medial AlmostQhasm State.
+Require Export Pseudo AlmostQhasm State.
 Require Export Bedrock.Word NArith NPeano Euclid.
-Require Export List Sumbool.
-Require Import FMapAVL FMapList JMeq.
-Require Import Vector.
+Require Export List Sumbool Vector.
 
-Module PseudoMedialConversion (Arch: PseudoMachine).
+Module PseudoConversion (Arch: PseudoMachine).
   Import QhasmCommon AlmostQhasm EvalUtil Util.
   Import ListNotations.
 
   Module P := Pseudo Arch.
-  Module M := Medial Arch.
+  (* Module M := Medial Arch. *)
 
   (******************    Material Conversions    ************************)
 
-  Module PseudoConversion <: Conversion P M.
-    Import P M Arch StateCommon.
+  Module PseudoConversion <: Conversion P AlmostQhasm.
+    Import P (* M *) Arch StateCommon.
 
-    Fixpoint convertState (st: M.State): option P.State :=
+    (* Fixpoint convertState (st: M.State): option P.State :=
       let try_cons := fun {T} (x: option T) (l: list T) =>
         match x with | Some x' => x' :: l | _ => l end in
 
@@ -31,7 +29,7 @@ Module PseudoMedialConversion (Arch: PseudoMachine).
         if (Nat.eq_dec (length varList) vars)
         then Some (varList, m, c)
         else None
-      end.
+      end. *)
 
     Fixpoint range (start len: nat): list nat :=
       match len with
@@ -58,6 +56,93 @@ Module PseudoMedialConversion (Arch: PseudoMachine).
       | [] => O
       end.
 
+    Definition MMap := NatM.t (Mapping width).
+    Definition mempty := NatM.empty (Mapping width).
+
+    Fixpoint convertProgram' {n m} (prog: Pseudo n m) (start: nat) (M: MMap):
+        option (AlmostProgram * (list (Mapping width)) * MMap) :=
+      let rM := fun (x: nat) => regM _ (reg width_spec x) in
+      let sM := fun (x: nat) => stackM _ (stack width_spec x) 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) M in
+
+      match prog with
+      | PVar n (Some true) i => Some (ASkip, [rM i], madd i rM)
+      | PVar n (Some false) i => Some (ASkip, [sM i], madd i sM)
+      | PVar n None i => Some (ASkip, [g i], M) 
+      | PConst n c => Some (AAssign (AConstInt (rM start) c), [rM start], madd start rM)
+      | PMem n m v i => Some (AAssign (ARegMem (rM start) v i), madd start rM)
+      | _ => None
+      end.
+
+
+      | PBin n o p =>
+        match (convertProgram' p start) with
+        | Some (p', [a; b]) =>
+          Some (MSeq p' (MOp (MIOpReg o a b)), [a])
+        | _ => None
+        end
+
+      | PCarry n o p =>
+        match (convertProgram' p start) with
+        | Some (p', [a; b]) =>
+          Some (MSeq p' (MOp (MCOpReg o a b)), [a])
+        | _ => None
+        end
+
+      | PDual n o p =>
+        match (convertProgram' p start) with
+        | Some (p', [a; b]) =>
+          let nextOpen := S (maxN [a; b]) in
+          Some (MSeq p' (MOp (MDOpReg o a b (Some nextOpen))), [a; nextOpen])
+        | _ => None
+        end
+
+      | PShift n o a x =>
+        match (convertProgram' x start) with
+        | Some (p', [r]) =>
+          Some (MSeq p' (MOp (MOpRot o r a)), [proj1_sig a])
+        | _ => None
+        end
+
+      | PLet n k m f g =>
+        ft <- convertProgram' f (start + k);
+        gt <- convertProgram' g (S (maxN (snd ft)));
+
+        match (ft, gt) with
+        | ((fp, fr), (gp, gr)) => Some (MSeq fp gp, gr)
+        end
+
+      | PComb n a b f g => 
+        ft <- convertProgram' f start;
+        gt <- convertProgram' g (S (maxN (snd ft)));
+        match (ft, gt) with
+        | ((fp, fr), (gp, gr)) => Some (MSeq fp gp, fr ++ gr)
+        end
+
+      | PIf n m o i0 i1 l r => 
+        lt <- convertProgram' l start;
+        rt <- convertProgram' r start;
+        match (lt, rt) with
+        | ((lp, lr), (rp, rr)) => Some (MCond (MCReg o i0 i1) lp rp, lr)
+        end
+        (* TODO: prove that all (Pseudo n m) will return the same list *)
+
+      | PFunExp n f e => 
+        match (convertProgram' f start) with
+        | Some (fp, fr) => Some (MFunexp e fp, fr)
+        | _ => None
+        end
+ 
+      | PCall n m lbl _ => Some (MCall lbl, range n m)
+      end.
+
     (* Results are in the locations described by the
        returned list. start is the next known open address *)
     Fixpoint convertProgram' {n m} (prog: Pseudo n m) (start: nat):