From 8bd67f639f552b989d74da19712704ecf5ce5723 Mon Sep 17 00:00:00 2001
From: Robert Sloan <varomodt@gmail.com>
Date: Wed, 1 Jun 2016 22:43:17 -0400
Subject: Running PipelineExample

---
 src/Assembly/Output.ml          | 14 ++++++++++++++
 src/Assembly/PipelineExample.v  | 21 +++++++++++++--------
 src/Assembly/StringConversion.v |  6 ++----
 3 files changed, 29 insertions(+), 12 deletions(-)
 create mode 100644 src/Assembly/Output.ml

(limited to 'src/Assembly')

diff --git a/src/Assembly/Output.ml b/src/Assembly/Output.ml
new file mode 100644
index 000000000..d84aee0a2
--- /dev/null
+++ b/src/Assembly/Output.ml
@@ -0,0 +1,14 @@
+
+open Result
+
+let list_to_string s =
+  let rec loop s n =
+    match s with
+      [] -> String.make n '?'
+    | car :: cdr ->
+      let result = loop cdr (n + 1) in
+        Bytes.set result n car;
+        result
+    in loop s 0 ;;
+
+print_string (list_to_string result) ;;
diff --git a/src/Assembly/PipelineExample.v b/src/Assembly/PipelineExample.v
index b17a85c9b..dcd09aa6c 100644
--- a/src/Assembly/PipelineExample.v
+++ b/src/Assembly/PipelineExample.v
@@ -1,4 +1,5 @@
 
+Require Import QhasmCommon QhasmEvalCommon.
 Require Import Pseudo Qhasm AlmostQhasm Medial Conversion Language.
 Require Import PseudoMedialConversion AlmostConversion StringConversion.
 
@@ -20,7 +21,7 @@ Module Progs.
 
   Definition prog0: C64.P.Program.
     refine
-      (PBin _ IPlus (PComb _ _ _
+      (PBin _ Add (PComb _ _ _
         (PVar 1 (exist _ 0 _))
         (PConst _ (natToWord _ 1)))); abstract intuition.
   Defined.
@@ -36,13 +37,17 @@ Module Progs.
 
   Definition prog4: option string :=
     omap StringConversion.convertProgram prog3.
+End Progs.
 
-  Definition result: option string.
-    let res := eval vm_compute in prog4 in exact res.
-  Defined.
+Definition Result: string.
+  let res := eval vm_compute in (
+    match Progs.prog4 with
+    | Some x => x
+    | None => EmptyString
+    end) in exact res.
+Defined.
 
-  Open Scope string_scope.
-  Print result.
-End Progs.
+Open Scope string_scope.
+Print Result.
 
-Extraction "Progs.ml" Progs.
+Extraction "Result.ml" Result.
diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v
index 086976550..8d9549865 100644
--- a/src/Assembly/StringConversion.v
+++ b/src/Assembly/StringConversion.v
@@ -368,10 +368,8 @@ Module StringConversion <: Conversion Qhasm QhasmString.
     let newline := String (ascii_of_nat 10) EmptyString in
 
     Some (fold_left (fun x y => (x ++ newline ++ y)%string)
-      (decls 32 ++
-       inputs 32 ++ blank ++
-       decls 64 ++
-       inputs 64 ++ blank ++
+      (decls 32 ++ inputs 32 ++
+       decls 64 ++ inputs 64 ++ blank ++
        enter ++ blank ++
        stmts ++ blank ++
        leave) EmptyString).
-- 
cgit v1.2.3