diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-06-01 22:43:17 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-01 22:43:17 -0400 |
| commit | 8bd67f639f552b989d74da19712704ecf5ce5723 (patch) | |
| tree | 3de5c72292ab64a64ffae5614fe8868f8358c276 /src/Assembly | |
| parent | 9b6f91769ea2318a4e812f9be6479684b6b2be79 (diff) | |
Running PipelineExample
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/Output.ml | 14 | ||||
| -rw-r--r-- | src/Assembly/PipelineExample.v | 21 | ||||
| -rw-r--r-- | src/Assembly/StringConversion.v | 6 |
3 files changed, 29 insertions, 12 deletions
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). |