Most of string conversions

1 files changed, 245 insertions, 79 deletions

diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v
index d44dbfcbf..54f0f8b00 100644
--- a/src/Assembly/StringConversion.v
+++ b/src/Assembly/StringConversion.v
@@ -8,10 +8,11 @@ Module QhasmString <: Language.
   Definition Program := string.
   Definition State := unit.
 
-  Definition eval (p: Program) (s: State): option State := Some tt.
+  Definition evaluatesTo (p: Program) (i o: State): Prop := True.
 End QhasmString.
 
 Module StringConversion <: Conversion Qhasm QhasmString.
+  Import Qhasm ListNotations.
 
   (* The easy one *)
   Definition convertState (st: QhasmString.State): option Qhasm.State := None.
@@ -60,31 +61,36 @@ Module StringConversion <: Conversion Qhasm QhasmString.
     Coercion wordToString {n} (w: word n): string := 
       "0x" ++ (nToHex (wordToN w)).
 
-    Coercion constToString {n} (c: Const n): string :=
+    Coercion intConstToString {n} (c: IConst n): string :=
       match c with
-      | const32 w => "0x" ++ w
-      | const64 w => "0x" ++ w
-      | const128 w => "0x" ++ w
+      | constInt32 w => "0x" ++ w
       end.
 
-    Coercion indexToString {n} (i: Index n): string :=
-      "0x" ++ (nToHex (N.of_nat i)).
+    Coercion floatConstToString {n} (c: FConst n): string :=
+      match c with
+      | constFloat32 w => "0x" ++ w
+      | constFloat64 w => "0x" ++ w
+      end.
+
+    Coercion intRegToString {n} (r: IReg n): string :=
+      match r with
+      | regInt32 n => "w" ++ (nameSuffix n)
+      end.
 
-    Coercion regToString {n} (r: Reg n): string :=
+    Coercion floatRegToString {n} (r: FReg n): string :=
       match r with
-      | reg32 n => "ex" ++ (nameSuffix n)
-      | reg3232 n => "mm" ++ (nameSuffix n)
-      | reg6464 n => "xmm" ++ (nameSuffix n)
-      | reg80 n => "st" ++ (nameSuffix n)
+      | regFloat32 n => "sf" ++ (nameSuffix n)
+      | regFloat64 n => "lf" ++ (nameSuffix n)
       end.
 
+    Coercion natToString (n: nat): string :=
+      "0x" ++ (nToHex (N.of_nat n)).
+
     Coercion stackToString {n} (s: Stack n): string :=
       match s with
-      | stack32 n => "word" ++ (nameSuffix n)
-      | stack64 n => "double" ++ (nameSuffix n)
-      | stack128 n => "quad" ++ (nameSuffix n)
-      | stack256 n => "stack256n" ++ (nameSuffix n)
-      | stack512 n => "stack512n" ++ (nameSuffix n)
+      | stack32 n => "ss" ++ (nameSuffix n)
+      | stack64 n => "ls" ++ (nameSuffix n)
+      | stack128 n => "qs" ++ (nameSuffix n)
       end.
 
     Coercion stringToSome (x: string): option string := Some x.
@@ -94,104 +100,264 @@ Module StringConversion <: Conversion Qhasm QhasmString.
 
     Definition assignmentToString (a: Assignment): option string :=
       match a with
+      | ARegStackInt n r s => r ++ " = *(int" ++ n ++ " *)" ++ s
+      | ARegStackFloat n r s => r ++ " = *(float" ++ n ++ " *)" ++ s
+      | AStackRegInt n s r => "*(int" ++ n ++ " *) " ++ s ++ " = " ++ r
+      | AStackRegFloat n s r => "*(float" ++ n ++ " *) " ++ s ++ " = " ++ r
+      | ARegRegInt n a b => a ++ " = " ++ b
+      | ARegRegFloat n a b => a ++ " = " ++ b
+      | AConstInt n r c => r ++ " = " ++ c
+      | AConstFloat n r c => r ++ " = " ++ c
+      | AIndex n m a b i =>
+        a ++ " = *(int" ++ n ++ " *) (" ++ b ++ " + " ++ (m/n) ++ ")"
+      | APtr n r s => r ++ " = " ++ s
+      end.
 
-      (* r = s *)
-      | Assign32Stack32 r s => r ++ " = " ++ s
-
-      | _ => None
+    Coercion intOpToString (b: IntOp): string :=
+      match b with
+      | IPlus => "+"
+      | IMinus => "-"
+      | IXor => "^"
+      | IAnd => "&"
+      | IOr => "|"
       end.
 
-    Coercion binOpToString (b: BinOp): string :=
+    Coercion floatOpToString (b: FloatOp): string :=
       match b with
-      | Plus => "+"
-      | Minus => "-"
-      | Mult => "*"
-      | Div => "/"
-      | Xor => "^"
-      | And => "&"
-      | Or => "|"
+      | FPlus => "+"
+      | FMult => "*"
+      | FAnd => "&"
       end.
 
     Coercion rotOpToString (r: RotOp): string :=
       match r with
       | Shl => "<<"
       | Shr => ">>"
-      | Rotl => "<<<"
-      | Rotr => ">>>"
       end.
-
-    Definition operationToString (o: Operation): option string :=
-      match o with
-      | OpReg32Constant b r c =>
-        r ++ " " ++ b ++ "= " ++ c
-      | OpReg32Reg32 b r0 r1 =>
-        r0 ++ " " ++ b ++ "= " ++ r1
-      | RotReg32 o r i =>
+ 
+    Definition operationToString (op: Operation): option string :=
+      match op with
+      | IOpConst o r c => 
+        r ++ " " ++ o ++ "= " ++ c
+      | IOpReg o a b =>
+        a ++ " " ++ o ++ "= " ++ b
+      | FOpConst32 o r c =>
+        r ++ " " ++ o ++ "= " ++ c
+      | FOpReg32 o a b =>
+        a ++ " " ++ o ++ "= " ++ b
+      | FOpConst64 o r c =>
+        r ++ " " ++ o ++ "= " ++ c
+      | FOpReg64 o a b =>
+        a ++ " " ++ o ++ "= " ++ b
+      | OpRot o r i =>
         r ++ " " ++ o ++ "= " ++ i
-      | OpReg64Constant b r c =>
-        r ++ " " ++ b ++ "= " ++ c
-      | OpReg64Reg64 b r0 r1 =>
-        r0 ++ " " ++ b ++ "= " ++ r1
-      | _ => None
       end.
 
-    Coercion testOpToString (t: TestOp): string :=
+    Definition testOpToString (t: TestOp): bool * string :=
       match t with
-      | TEq => "="
-      | TLt => "<"
-      | TUnsignedLt => "unsigned<"
-      | TGt => ">"
-      | TUnsignedGt => "unsigned>"
+      | TEq => (true, "=")
+      | TLt => (true, "<")
+      | TGt => (true, ">")
+      | TLe => (false, ">")
+      | TGe => (false, "<")
       end.
 
-    Definition conditionalToString (c: Conditional): string :=
-      let f := fun (i: bool) => if i then "!" else "" in
+    Definition conditionalToString (c: Conditional): string * string :=
       match c with
-      | TestTrue => ""
-      | TestFalse => ""
-      | TestReg32Reg32 o i r0 r1 => (f i) ++ o ++ "?" ++ r0 ++ " " ++ r1
-      | TestReg32Const o i r c =>(f i) ++ o ++ "?" ++ r ++ " " ++ c
+      | TestTrue => ("=? 0", ">") (* these will be elided later on*)
+      | TestFalse => (">? 0", ">")
+      | TestInt n o a b =>
+        match (testOpToString o) with
+        | (true, s) =>
+          (s ++ "? " ++ a ++ " - " ++ b, s)
+        | (false, s) =>
+          ("!" ++ s ++ "? " ++ a ++ " - " ++ b, "!" ++ s)
+        end
+      | TestFloat n o a b =>
+        match (testOpToString o) with
+        | (true, s) =>
+          (s ++ "? " ++ a ++ " - " ++ b, s)
+        | (false, s) =>
+          ("!" ++ s ++ "? " ++ a ++ " - " ++ b, "!" ++ s)
+        end
       end.
 
   End Elements.
 
   Section Parsing.
-
     Inductive Entry :=
-      | regEntry: forall n, Reg n -> Entry
-      | stackEntry: forall n, Stack n -> Entry
-      | constEntry: forall n, Const n -> Entry.
+      | intEntry: forall n, IReg n -> Entry
+      | floatEntry: forall n, FReg n -> Entry
+      | stackEntry: forall n, Stack n -> Entry.
+
+    Definition entryId (x: Entry): nat * nat * nat :=
+      match x with
+      | intEntry n (regInt32 v) => (0, n, v)
+      | floatEntry n (regFloat32 v) => (1, n, v)
+      | floatEntry n (regFloat64 v) => (2, n, v)
+      | stackEntry n (stack32 v) => (3, n, v)
+      | stackEntry n (stack64 v) => (4, n, v)
+      | stackEntry n (stack128 v) => (5, n, v)
+      end.
 
-    Definition allRegs (prog: Qhasm.Program): list Entry := [(* TODO *)]
+    Lemma id_equal: forall {x y}, x = y <-> entryId x = entryId y.
+    Proof.
+      intros; split; intros;
+        destruct x as [nx x | nx x | nx x];
+        destruct y as [ny y | ny y | ny y];
+        try rewrite H;
+
+        destruct x, y; subst;
+        destruct (Nat.eq_dec n n0); subst;
+
+        simpl in H; inversion H; intuition.
+    Qed.
+
+    Lemma triple_conv: forall {x0 x1 x2 y0 y1 y2: nat},
+      (x0 = y0 /\ x1 = y1 /\ x2 = y2) <-> (x0, x1, x2) = (y0, y1, y2).
+    Proof.
+      intros; split; intros.
+
+      - destruct H; destruct H0; subst; intuition.
+
+      - inversion_clear H; intuition.
+    Qed.
+
+    Definition triple_dec (x y: nat * nat * nat): {x = y} + {x <> y}.
+      refine (match x as x' return x' = _ -> _ with
+      | (x0, x1, x2) => fun _ =>
+        match y as y' return y' = _ -> _ with
+        | (y0, y1, y2) => fun _ =>
+           _ (Nat.eq_dec x0 y0) (Nat.eq_dec x1 y1) (Nat.eq_dec x2 y2)
+        end (eq_refl y)
+      end (eq_refl x));
+        rewrite <- _H, <- _H0;
+        clear _H _H0 x y p p0;
+        intros.
+
+      intros; destruct x6, x7, x8; first [
+        left; abstract (subst; intuition)
+      | right; abstract (intro;
+          apply triple_conv in H;
+          destruct H; destruct H0; intuition)
+      ].
+    Defined.
+
+    Definition entry_dec (x y: Entry): {x = y} + {x <> y}.
+      refine (_ (triple_dec (entryId x) (entryId y))).
+      intros; destruct x0.
+
+      - left; abstract (apply id_equal in e; intuition).
+      - right; abstract (intro; apply id_equal in H; intuition).
+    Defined.
+
+    Fixpoint entries (prog: Program): list Entry :=
+      match prog with
+      | cons s next =>
+        match s with
+        | QAssign a =>
+          match a with
+          | ARegStackInt n r s => [intEntry n r; stackEntry n s]
+          | ARegStackFloat n r s => [floatEntry n r; stackEntry n s]
+          | AStackRegInt n s r => [intEntry n r; stackEntry n s]
+          | AStackRegFloat n s r => [floatEntry n r; stackEntry n s]
+          | ARegRegInt n a b => [intEntry n a; intEntry n b]
+          | ARegRegFloat n a b => [floatEntry n a; floatEntry n b]
+          | AConstInt n r c => [intEntry n r]
+          | AConstFloat n r c => [floatEntry n r]
+          | AIndex n m a b i => [intEntry n a; intEntry m b]
+          | APtr n r s => [intEntry 32 r; stackEntry n s]
+          end
+        | QOp o =>
+          match o with
+          | IOpConst o r c => [intEntry 32 r]
+          | IOpReg o a b => [intEntry 32 a; intEntry 32 b]
+          | FOpConst32 o r c => [floatEntry 32 r]
+          | FOpReg32 o a b => [floatEntry 32 a; floatEntry 32 b]
+          | FOpConst64 o r c => [floatEntry 64 r]
+          | FOpReg64 o a b => [floatEntry 64 a; floatEntry 64 b]
+          | OpRot o r i => [intEntry 32 r]
+          end
+        | QJmp c _ =>
+          match c with
+          | TestInt n o a b => [intEntry n a; intEntry n b]
+          | TestFloat n o a b => [floatEntry n a; floatEntry n b]
+          | _ => []
+          end
+        | QLabel _ => []
+        end ++ (entries next)
+      | nil => nil
+      end.
+
+    Definition flatMap {A B} (lst: list A) (f: A -> option B): list B :=
+      fold_left
+        (fun lst a => match (f a) with | Some x => cons x lst | _ => lst end)
+        lst [].
+
+    Fixpoint dedup (l : list Entry) : list Entry :=
+      match l with
+      | [] => []
+      | x::xs =>
+        if in_dec entry_dec x xs
+        then dedup xs
+        else x::(dedup xs)
+      end.
 
+    Definition everyIReg32 (lst: list Entry): list (IReg 32) :=
+      flatMap (dedup lst) (fun e =>
+        match e with | intEntry 32 r => Some r | _ => None end).
+
+    Definition everyFReg32 (lst: list Entry): list (FReg 32) :=
+      flatMap (dedup lst) (fun e =>
+        match e with | floatEntry 32 r => Some r | _ => None end).
+
+    Definition everyFReg64 (lst: list Entry): list (FReg 64) :=
+      flatMap (dedup lst) (fun e =>
+        match e with | floatEntry 64 r => Some r | _ => None end).
+
+    Definition everyStack (n: nat) (lst: list Entry): list (Stack n).
+      refine (flatMap (dedup lst) (fun e =>
+        match e with
+        | stackEntry n' r =>
+          if (Nat.eq_dec n n') then Some (convert r _) else None
+        | _ => None
+        end)); subst; abstract intuition.
+    Defined.
   End Parsing.
 
   (* Macroscopic Conversion Methods *)
+  Definition optionToList {A} (o: option A): list A :=
+    match o with
+    | Some a => [a]
+    | None => []
+    end.
 
-  Definition convertStatement (statement: Qhasm.QhasmStatement): string :=
-    match prog with
-    | QAssign a =>
-    | QOp o =>
+  Definition convertStatement (statement: Qhasm.QhasmStatement): list string :=
+    match statement with
+    | QAssign a => optionToList (assignmentToString a)
+    | QOp o => optionToList (operationToString o)
     | QJmp c l =>
-    | QLabel l =>
+      match (conditionalToString c) with
+      | (s1, s2) =>
+        let s' := ("goto lbl" ++ l ++ " if " ++ s2)%string in
+        [s1; s']
+      end
+    | QLabel l => [("lbl" ++ l ++ ": ")%string]
     end.
 
-  Definition convertProgramPrologue (prog: Qhasm.Program): option string :=
+  Definition convertProgramPrologue (prog: Qhasm.Program): list string :=
+    [EmptyString].
 
-  Definition convertProgramEpilogue (prog: Qhasm.Program): option string :=
+  Definition convertProgramEpilogue (prog: Qhasm.Program): list string :=
+    [EmptyString].
 
   Definition convertProgram (prog: Qhasm.Program): option string :=
-    Some EmptyString.
-
-  Lemma convert_spec: forall st' prog,
-    match ((convertProgram prog), (convertState st')) with
-    | (Some prog', Some st) =>
-      match (QhasmString.eval prog' st') with
-      | Some st'' => Qhasm.eval prog st = (convertState st'')
-      | _ => True
-      end
-    | _ => True
-    end.
+    None.
+
+  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'.
   Admitted.
 
 End StringConversion.