diff options
author | Robert Sloan <varomodt@gmail.com> | 2016-06-02 21:50:39 -0400 |
---|---|---|
committer | Robert Sloan <varomodt@gmail.com> | 2016-06-02 21:50:39 -0400 |
commit | 412f037ec6614ee7fea3c42cc913e1f7b3adde7e (patch) | |
tree | 9fced76d1a1ad7f3b9637b16b0c407fd6915c6b8 /src/Assembly | |
parent | 8bd67f639f552b989d74da19712704ecf5ce5723 (diff) |
Running PipelineExample
Diffstat (limited to 'src/Assembly')
-rw-r--r-- | src/Assembly/PipelineExample.v | 14 | ||||
-rw-r--r-- | src/Assembly/Pseudo.v | 10 | ||||
-rw-r--r-- | src/Assembly/StringConversion.v | 2 |
3 files changed, 16 insertions, 10 deletions
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' -> |