blob: 9d6c4c9dac4336c3d4d1c267d53363d8638a041d (
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
|
Require Import Bedrock.Word.
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 ListNotations StateCommon EvalUtil ListState.
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 =>
plet a := $$ 1 in
plet b := v[[0]] in
plet c := multHigh a b in
plet d := a ^* b in
[b ^& d]).
pseudo_solve.
Defined.
Eval vm_compute in (Pipeline.toString (proj1_sig example)).
End PipelineExample.
|
