Tuple-ization tactics work

Most of Medial, less the conversions

Most of Medial, less the conversions

Most of Medial, less the conversions

Most of Medial, less the conversions

More of Medial

MedialConversions done

1 files changed, 31 insertions, 87 deletions

diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index f5baa96c6..6bb619910 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -13,58 +13,18 @@ Module Pseudo (M: PseudoMachine) <: Language.
 
   Definition const: Type := word width.
 
-  Definition width_dec: {width = 32} + {width = 64}.
-    destruct width_spec.
-    - left; abstract intuition.
-    - right; abstract intuition.
-  Defined.
-
-  Definition ireg (x: nat): IReg width :=
-    match width_spec with
-    | I32 => regInt32 x
-    | I64 => regInt64 x
-    end.
-
-  Definition iconst (x: word width): IConst width.
-    refine (
-      if width_dec
-      then (convert constInt32 _) x
-      else (convert constInt64 _) x);
-    abstract (rewrite _H; intuition).
-  Defined.
-
-  Definition stack (x: nat): Stack width :=
-    match width_spec with
-    | I32 => stack32 x
-    | I64 => stack64 (2 * x)
-    end.
-
   (* Program Types *)
   Definition State := list const.
 
-  Inductive WBinOp: Set :=
-    | Wplus: WBinOp    | Wminus: WBinOp   | Wand: WBinOp.
-
-  Inductive WDualOp: Set :=
-    | Wmult: WDualOp.
-
-  Inductive WNatOp: Set :=
-    | Wones: WNatOp    | Wzeros: WNatOp.
-
-  Inductive WShiftOp: Set :=
-    | Wshl: WShiftOp   | Wshr: WShiftOp.
-
   Inductive Pseudo: nat -> nat -> Type :=
     | PVar: forall n, Index n -> Pseudo n 1
     | PConst: forall n, const -> Pseudo n 1
 
-    | PBin: forall n, WBinOp -> Pseudo n 1 -> Pseudo n 1 -> Pseudo n 1
-    | PNat: forall n, WNatOp -> Index width -> Pseudo n 1
-    | PDual: forall n, WDualOp -> Pseudo n 1 -> Pseudo n 1 -> Pseudo n 2
-    | PShift: forall n, WShiftOp -> Pseudo n 1 -> Index width -> Pseudo n 1
+    | PBin: forall n, IntOp -> Pseudo n 2 -> Pseudo n 1
+    | PDual: forall n, DualOp -> Pseudo n 2 -> Pseudo n 2
+    | PShift: forall n, RotOp -> Index width -> Pseudo n 1 -> Pseudo n 1
 
     | PLet: forall n k m, Pseudo n k -> Pseudo (n + k) m -> Pseudo n m
-    | PComp: forall n k m, Pseudo n k -> Pseudo k m -> Pseudo n m
     | PComb: forall n a b, Pseudo n a -> Pseudo n b -> Pseudo n (a + b)
 
     | PIf: forall n m, TestOp -> Index n -> Index n -> Pseudo n m -> Pseudo n m -> Pseudo n m
@@ -74,14 +34,16 @@ Module Pseudo (M: PseudoMachine) <: Language.
 
   Definition Program := Pseudo vars vars.
 
-  Definition applyBin (op: WBinOp) (a b: word width): const :=
+  Definition applyBin (op: IntOp) (a b: word width): const :=
     match op with
-    | Wplus => wplus a b
-    | Wminus => wminus a b
-    | Wand => wand a b
+    | IPlus => wplus a b
+    | IMinus => wminus a b
+    | IAnd => wand a b
+    | IXor => wxor a b
+    | IOr => wor a b
     end.
 
-  Definition applyDual (op: WDualOp) (a b: word width): list const :=
+  Definition applyDual (op: DualOp) (a b: word width): list const :=
     match op with
     | Wmult =>
       let wres := natToWord (width + width)
@@ -89,20 +51,10 @@ Module Pseudo (M: PseudoMachine) <: Language.
       [split1 _ _ wres; split2 _ _ wres]
     end.
 
-  Definition applyNat (op: WNatOp) (v: Index width): const.
-    refine match op with
-    | Wones => convert (zext (wones v) (width - v)) _
-    | Wzeros => wzero width
-    end; abstract (
-      destruct v; simpl;
-      replace (x + (width - x)) with width;
-      intuition ).
-  Defined.
-
-  Definition applyShift (op: WShiftOp) (v: const) (n: Index width): const.
+  Definition applyShift (op: RotOp) (v: const) (n: Index width): const.
     refine match op with
-    | Wshl => convert (Word.combine (wzero n) (split1 (width - n) n (convert v _))) _
-    | Wshr => convert (Word.combine (split2 n (width - n) (convert v _)) (wzero n)) _
+    | Shl => convert (Word.combine (wzero n) (split1 (width - n) n (convert v _))) _
+    | Shr => convert (Word.combine (split2 n (width - n) (convert v _)) (wzero n)) _
     end; abstract (
       unfold const;
       destruct n; simpl;
@@ -125,41 +77,33 @@ Module Pseudo (M: PseudoMachine) <: Language.
     match prog with
     | PVar n i => option_map' (nth_error st i) (fun x => Some [x])
     | PConst n c => Some ([c])
-    | PNat n o i => Some [applyNat o i]
-
-    | PBin n o a b =>
-      option_map' (pseudoEval a st) (fun sa =>
-        option_map' (pseudoEval b st) (fun sb =>
-          match (sa, sb) with
-          | ([wa], [wb]) => Some [applyBin o wa wb]
-          | _ => None
-          end ))
-
-    | PDual n o a b =>
-      option_map' (pseudoEval a st) (fun sa =>
-        option_map' (pseudoEval b st) (fun sb =>
-          match (sa, sb) with
-          | ([wa], [wb]) => Some (applyDual o wa wb)
-          | _ => None
-          end ))
-
-    | PShift n o x y =>
+
+    | PBin n o p =>
+      option_map' (pseudoEval p st) (fun sp =>
+        match sp with
+        | [wa; wb] => Some [applyBin o wa wb]
+        | _ => None
+        end)
+
+    | PDual n o p =>
+      option_map' (pseudoEval p st) (fun sp =>
+        match sp with
+        | [wa; wb] => Some (applyDual o wa wb)
+        | _ => None
+        end)
+
+    | PShift n o a x =>
       option_map' (pseudoEval x st) (fun sx =>
         match sx with
-        | [wx] => Some [applyShift o wx y]
+        | [wx] => Some [applyShift o wx a]
         | _ => None
-        end )
+        end)
 
     | PLet n k m f g =>
       option_map' (pseudoEval f st) (fun sf =>
         option_map' (pseudoEval g (st ++ sf))
           (fun sg => Some sg))
 
-    | PComp n k m f g => 
-      option_map' (pseudoEval f st) (fun sf =>
-        option_map' (pseudoEval g sf)
-          (fun sg => Some sg))
-
     | PComb n a b f g =>
       option_map' (pseudoEval f st) (fun sf =>
         option_map' (pseudoEval g st) (fun sg =>