blob: dcd09aa6c433ecd8900045a5d7ff5616c47fc0f5 (
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
42
43
44
45
46
47
48
49
50
51
52
53
|
Require Import QhasmCommon QhasmEvalCommon.
Require Import Pseudo Qhasm AlmostQhasm Medial Conversion Language.
Require Import PseudoMedialConversion AlmostConversion StringConversion.
Extraction Language Ocaml.
Require Import ExtrOcamlString ExtrOcamlBasic.
Require Import Coq.Strings.String.
Module Progs.
Module Arch := PseudoUnary64.
Module C64 := PseudoMedialConversion Arch.
Import C64.P.
Definition omap {A B} (f: A -> option B) (x: option A): option B :=
match x with
| Some v => f v
| None => None
end.
Definition prog0: C64.P.Program.
refine
(PBin _ Add (PComb _ _ _
(PVar 1 (exist _ 0 _))
(PConst _ (natToWord _ 1)))); abstract intuition.
Defined.
Definition prog1: option C64.M.Program :=
C64.PseudoConversion.convertProgram prog0.
Definition prog2: option AlmostQhasm.Program :=
omap C64.MedialConversion.convertProgram prog1.
Definition prog3: option Qhasm.Program :=
omap AlmostConversion.convertProgram prog2.
Definition prog4: option string :=
omap StringConversion.convertProgram prog3.
End Progs.
Definition Result: string.
let res := eval vm_compute in (
match Progs.prog4 with
| Some x => x
| None => EmptyString
end) in exact res.
Defined.
Open Scope string_scope.
Print Result.
Extraction "Result.ml" Result.
|
