blob: b0cd4018e72bccd05f7e6315a1df1baf4be957af (
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
31
32
33
|
Require Import QhasmCommon QhasmEvalCommon.
Require Import Pseudo Qhasm AlmostQhasm Conversion Language.
Require Import PseudoConversion AlmostConversion StringConversion.
Module Pipeline.
Export Pseudo Util.
Definition toAlmost (p: Pseudo inVars outVars): option AlmostQhasm.Program :=
PseudoConversion.convertProgram p.
Definition toQhasm (p: Pseudo inVars outVars): option Qhasm.Program :=
omap (toAlmost p) AlmostConversion.convertProgram.
Definition toString (p: Pseudo inVars outVars): option string :=
omap (toQhasm p) StringConversion.convertProgram.
End Pipeline.
Module PipelineExample.
Import Pipeline.
Program Definition asdf: Program Unary32 := ($0 :+: $0)%p.
Definition exStr := Pipeline.toString ex.
| Some x => x
| None => EmptyString
end.
Defined.
Open Scope string_scope.
Print Result.
Extraction "Result.ml" Result.
|
