blob: da4df63b7df1f550f3b40a5577b64569b3f2a727 (
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
34
35
36
37
38
39
40
41
|
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.
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.
Local Notation "v [[ i ]]" := (nth i v (wzero _)) (at level 40).
Local Notation "$$ v" := (natToWord _ v) (at level 40).
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.
|
