From 412f037ec6614ee7fea3c42cc913e1f7b3adde7e Mon Sep 17 00:00:00 2001
From: Robert Sloan <varomodt@gmail.com>
Date: Thu, 2 Jun 2016 21:50:39 -0400
Subject: Running PipelineExample

---
 src/Assembly/PipelineExample.v  | 14 +++++++-------
 src/Assembly/Pseudo.v           | 10 ++++++++--
 src/Assembly/StringConversion.v |  2 +-
 3 files changed, 16 insertions(+), 10 deletions(-)

(limited to 'src/Assembly')

diff --git a/src/Assembly/PipelineExample.v b/src/Assembly/PipelineExample.v
index dcd09aa6c..8f7d43b9d 100644
--- a/src/Assembly/PipelineExample.v
+++ b/src/Assembly/PipelineExample.v
@@ -8,10 +8,10 @@ Require Import ExtrOcamlString ExtrOcamlBasic.
 Require Import Coq.Strings.String.
 
 Module Progs.
-  Module Arch := PseudoUnary64.
-  Module C64 := PseudoMedialConversion Arch.
+  Module Arch := PseudoUnary32.
+  Module C32 := PseudoMedialConversion Arch.
 
-  Import C64.P.
+  Import C32.P.
 
   Definition omap {A B} (f: A -> option B) (x: option A): option B :=
     match x with
@@ -19,18 +19,18 @@ Module Progs.
     | None => None
     end.
 
-  Definition prog0: C64.P.Program.
+  Definition prog0: C32.P.Program.
     refine
       (PBin _ Add (PComb _ _ _
         (PVar 1 (exist _ 0 _))
         (PConst _ (natToWord _ 1)))); abstract intuition.
   Defined.
 
-  Definition prog1: option C64.M.Program :=
-    C64.PseudoConversion.convertProgram prog0.
+  Definition prog1: option C32.M.Program :=
+    C32.PseudoConversion.convertProgram prog0.
 
   Definition prog2: option AlmostQhasm.Program :=
-    omap C64.MedialConversion.convertProgram prog1.
+    omap C32.MedialConversion.convertProgram prog1.
 
   Definition prog3: option Qhasm.Program :=
     omap AlmostConversion.convertProgram prog2.
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index 21cc11c4e..ce2c5878a 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -106,6 +106,13 @@ Module Pseudo (M: PseudoMachine) <: Language.
 
   Definition evaluatesTo := fun (p: Program) (st st': State) => (pseudoEval p st = Some st').
 
+  Module Notations.
+    Delimit Scope pseudo_notations with p.
+    Open Scope pseudo_notations.
+
+    Notation "'LET' A := B 'IN' C" (at level 60, right associativity) : pseudo_notations.
+  End Notations.
+
   (* world peace *)
 End Pseudo.
 
@@ -121,5 +128,4 @@ Module PseudoUnary64 <: PseudoMachine.
   Definition vars := 1.
   Definition width_spec := W64.
   Definition const: Type := word width.
-End PseudoUnary64.
- 
\ No newline at end of file
+End PseudoUnary64.
\ No newline at end of file
diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v
index 8d9549865..46fce9b60 100644
--- a/src/Assembly/StringConversion.v
+++ b/src/Assembly/StringConversion.v
@@ -372,7 +372,7 @@ Module StringConversion <: Conversion Qhasm QhasmString.
        decls 64 ++ inputs 64 ++ blank ++
        enter ++ blank ++
        stmts ++ blank ++
-       leave) EmptyString).
+       leave ++ blank) EmptyString).
 
   Lemma convert_spec: forall a a' b b' prog prog',
     convertProgram prog = Some prog' ->
-- 
cgit v1.2.3