aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly/Pipeline.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Assembly/Pipeline.v')
-rw-r--r--src/Assembly/Pipeline.v33
1 files changed, 33 insertions, 0 deletions
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
new file mode 100644
index 000000000..b0cd4018e
--- /dev/null
+++ b/src/Assembly/Pipeline.v
@@ -0,0 +1,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.