blob: ba76f3585732721588a899f7109d9dc20dcb769d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
Require Import QhasmCommon QhasmEvalCommon.
Require Import Pseudo Qhasm AlmostQhasm Conversion Language.
Require Import PseudoConversion AlmostConversion StringConversion.
Module Pipeline.
Export AlmostQhasm Qhasm QhasmString.
Export Pseudo.
Transparent Pseudo.Program AlmostQhasm.Program Qhasm.Program QhasmString.Program.
Transparent Pseudo.Params AlmostQhasm.Params Qhasm.Params QhasmString.Params.
Definition toAlmost {w s n m} (p: @Pseudo w s n m) : option AlmostProgram :=
PseudoConversion.convertProgram (mkParams w s n m) tt p.
Definition toQhasm {w s n m} (p: @Pseudo w s n m) : option (list QhasmStatement) :=
omap (toAlmost p) (AlmostConversion.convertProgram tt tt).
Definition toString {w s n m} (p: @Pseudo w s n m) : option string :=
omap (toQhasm p) (StringConversion.convertProgram tt tt).
End Pipeline.
Module PipelineExample.
Import Pipeline.
Program Definition asdf: Program Unary32 := ($0 :+: $0)%p.
Definition exStr := Pipeline.toString asdf.
(* Eval vm_compute in exStr. *)
End PipelineExample.
|
