diff options
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/Pipeline.v | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index ba76f3585..da4df63b7 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -1,6 +1,7 @@ Require Import QhasmCommon QhasmEvalCommon. Require Import Pseudo Qhasm AlmostQhasm Conversion Language. Require Import PseudoConversion AlmostConversion StringConversion. +Require Import Wordize Vectorize Pseudize. Module Pipeline. Export AlmostQhasm Qhasm QhasmString. @@ -22,9 +23,19 @@ End Pipeline. Module PipelineExample. Import Pipeline. - Program Definition asdf: Program Unary32 := ($0 :+: $0)%p. + Local Notation "v [[ i ]]" := (nth i v (wzero _)) (at level 40). + Local Notation "$$ v" := (natToWord _ v) (at level 40). - Definition exStr := Pipeline.toString asdf. + Definition example: @pseudeq 32 W32 1 1 (fun v => + Let_In ($$ 1) (fun a => + Let_In (v[[0]]) (fun b => [ + a ^& b + ]))). + + pseudo_solve. + Defined. + + Definition exStr := Pipeline.toString example. (* Eval vm_compute in exStr. *) End PipelineExample. |