Generalized and cleaned up state model

2 files changed, 81 insertions, 51 deletions

diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index a0ebf7255..21cc11c4e 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -29,7 +29,7 @@ Module Pseudo (M: PseudoMachine) <: Language.
 
     | 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, Pseudo n m -> Pseudo n m.
+    | PCall: forall n m, Label -> Pseudo n m -> Pseudo n m.
 
   Hint Constructors Pseudo.
 
@@ -101,7 +101,7 @@ Module Pseudo (M: PseudoMachine) <: Language.
             funexpseudo e'' st'')
         end) e st
 
-    | PCall n m p => pseudoEval p st
+    | PCall n m _ p => pseudoEval p st
     end.
 
   Definition evaluatesTo := fun (p: Program) (st st': State) => (pseudoEval p st = Some st').
diff --git a/src/Assembly/PseudoMedialConversion.v b/src/Assembly/PseudoMedialConversion.v
index 036ea6fd0..f93db87fc 100644
--- a/src/Assembly/PseudoMedialConversion.v
+++ b/src/Assembly/PseudoMedialConversion.v
@@ -4,7 +4,7 @@ Require Export Pseudo Medial AlmostQhasm State.
 Require Export Bedrock.Word NArith NPeano.
 Require Export List Sumbool.
 Require Import FMapAVL FMapList JMeq.
-Require Vector.
+Require Import Vector.
 
 Module PseudoMedialConversion (Arch: PseudoMachine).
   Import QhasmCommon AlmostQhasm EvalUtil Util.
@@ -20,7 +20,7 @@ Module PseudoMedialConversion (Arch: PseudoMachine).
 
     Fixpoint convertState (st: M.State): option P.State :=
       let try_cons := fun {T} (x: option T) (l: list T) =>
-        match x with | Some x' => cons x' l | _ => l end in
+        match x with | Some x' => x' :: l | _ => l end in
 
       match st with
       | (v, m, c) =>
@@ -47,90 +47,120 @@ Module PseudoMedialConversion (Arch: PseudoMachine).
         | [] => ([], [])
         | l :: ls =>
           match list_split m ls with
-          | (a, b) => (cons l a, b)
+          | (a, b) => (l :: a, b)
           end
         end
       end.
 
     Fixpoint maxN (lst: list nat): nat :=
       match lst with
-      | cons x xs => max x (maxN xs)
-      | nil => O
+      | x :: xs => max x (maxN xs)
+      | [] => O
       end.
 
-    Module NatM := FMapAVL.Make(Nat_as_OT).
-    Module ProgMap := NatM.t Medial.
-    Definition noProgs := NatM.empty Medial.
-
     (* 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) (funs: nat):
-        option (Medial * (list nat) * (NatM.t Medial)) :=
+    Fixpoint convertProgram' {n m} (prog: Pseudo n m) (start: nat):
+        option (Medial * (list nat)) :=
 
       match prog with
-      | PVar n i => Some (MSkip, [start], NatM.empty)
-      | PConst n c => Some (MAssign (MAConst start c), [start], [])
-      | PMem n m v i => Some (MAssign (MAMem start v i), [start], [])
+      | PVar n i => Some (MSkip, [start])
+      | PConst n c => Some (MAssign (MAConst start c), [start])
+      | PMem n m v i => Some (MAssign (MAMem start v i), [start])
 
-                            | _ => None end.
       | PBin n o p =>
-        t <- convertProgram' p start funs;
-        match (snd t) with
-        | [a; b] =>
-          Some (MSeq (fst t) (MOp (MIOpReg o a b)), [a])
+        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 =>
-        t <- convertProgram' p start funs;
-        match (snd t) with
-        | [a; b] =>
-          let nextOpen := S (maxN (snd t)) in
-          Some (MSeq (fst t) (MOp (MDOpReg o a b (Some nextOpen))),
-                [a; nextOpen])
+        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 =>
-        t <- convertProgram' x start funs;
-        match (snd t) with
-        | [r] => Some (MSeq (fst t) (MOp (MOpRot o r a)), [proj1_sig a])
+        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) funs;
-        gt <- convertProgram' g (S (maxN (snd ft))) funs;
+        ft <- convertProgram' f (start + k);
+        gt <- convertProgram' g (S (maxN (snd ft)));
 
-        Some (MSeq (fst ft) (fst gt), snd gt)
+        match (ft, gt) with
+        | ((fp, fr), (gp, gr)) => Some (MSeq fp gp, gr)
+        end
 
       | PComb n a b f g => 
-        ft <- convertProgram' f start funs;
-        gt <- convertProgram' g (S (maxN (snd ft))) funs;
-        Some (MSeq (fst ft) (fst gt), (snd ft) ++ (snd gt))
+        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 funs;
-        rt <- convertProgram' r start funs;
-        Some (MCond (MC o i0 i1) (fst lt) (fst rt), snd lt)
-             (* TODO: prove that all (Pseudo n m) will return the same list *)
+        lt <- convertProgram' l start;
+        rt <- convertProgram' r start;
+        match (lt, rt) with
+        | ((lp, lr), (rp, rr)) => Some (MCond (MC o i0 i1) lp rp, lr)
+        end
+        (* TODO: prove that all (Pseudo n m) will return the same list *)
 
       | PFunExp n f e => 
-        ft <- convertProgram' f start funs;
-        Some (MFunexp e (fst ft), snd ft)
+        match (convertProgram' f start) with
+        | Some (fp, fr) => Some (MFunexp e fp, fr)
+        | _ => None
+        end
  
-      | PCall n m f => 
-        ft <- convertProgram' f start funs;
-        Some (MCall funs (fst ft), snd ft)
-    | MDef: nat -> Medial -> Medial -> Medial
-    | MCall: nat -> Medial.
-
-
+      | PCall n m lbl _ => Some (MCall lbl, range n m)
       end.
 
+    Definition addFunMap {T} (a b: TripleM.t T): TripleM.t T :=
+      (fix add' (m: TripleM.t T) (elts: list ((nat * nat * nat) * T)%type) :=
+        match elts with
+        | [] => m
+        | (k, v) :: elts' => add' (TripleM.add k v m) elts'
+        end) a (TripleM.elements b).
+
     Definition convertProgram (prog: Pseudo vars vars): option M.Program :=
-      let m := range O vars in
-      option_map (@fst Medial nat) (convertProgram' prog m m vars).
+     let defs := (fix allDefs {n m} (prog: Pseudo n m): TripleM.t M.Program :=
+        match prog with
+        | PBin n o p => allDefs p
+        | PCarry n o p => allDefs p
+        | PDual n o p => allDefs p
+        | PShift n o a x => allDefs x
+        | PLet n k m f g => addFunMap (allDefs f) (allDefs g)
+        | PComb n a b f g => addFunMap (allDefs f) (allDefs g)
+        | PIf n m t i0 i1 l r => addFunMap (allDefs l) (allDefs r)
+        | PFunExp n p e => allDefs p
+        | PCall n m l p =>
+          match (convertProgram' p n) with
+          | Some (mp, _) => TripleM.add (n, m, l) mp (allDefs p)
+          | _ => allDefs p
+          end
+        | _ => TripleM.empty M.Program
+        end) prog in
+
+     let foldF := fun (t: (nat * nat * nat) * M.Program) (p: M.Program) =>
+       match t with
+       | ((n', m', lbl), p') => MDef lbl p' p
+       end in
+
+     option_map (fold_left _ _ foldF (TripleM.elements defs)) (convertProgram' prog _ _ vars).
 
     Lemma convert_spec:  forall a a' b b' prog prog',
       convertProgram prog = Some prog' ->