blob: 878aa37bf8899bbd0ef435213151a638d3697af6 (
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
54
55
56
57
58
59
60
61
62
63
64
|
Require Import NArith.
Require Export Qhasm AlmostQhasm Conversion.
Module AlmostConversion <: Conversion AlmostQhasm Qhasm.
Import QhasmCommon AlmostQhasm Qhasm.
Import ListNotations.
Fixpoint almostToQhasm' (prog: AlmostProgram) (lblStart: N): list QhasmStatement :=
let label0 := (lblStart * 2)%N in
let label1 := (label0 + 1)%N in
match prog with
| ASkip => []
| ASeq a b => (almostToQhasm' a label0) ++ (almostToQhasm' b label1)
| AAssign a => [ QAssign a ]
| AOp a => [ QOp a ]
| ACond c a b =>
let start := N.shiftl 2 label0 in
let finish := (start + 1)%N in
[QCond c (N.to_nat start)] ++
(almostToQhasm' b (start + 2)) ++
[QCond CTrue (N.to_nat finish)] ++
[QLabel (N.to_nat start)] ++
(almostToQhasm' a (start + 3)) ++
[QLabel (N.to_nat finish)]
| AWhile c a =>
let start := N.to_nat (N.shiftl 1 label0) in
let test := S start in
[ QCond CTrue test ;
QLabel start ] ++
(almostToQhasm' a label1) ++
[ QLabel test;
QCond c start ]
| ADef lbl f x =>
let start' := N.shiftl 1 label0 in
let start'' := (1 + start')%N in
[ QLabel lbl ] ++
(almostToQhasm' f start') ++
[ QRet ] ++
(almostToQhasm' x start'')
| ACall lbl => [QCall lbl]
end.
Transparent Qhasm.Program AlmostQhasm.Program.
Definition convertProgram x y (prog: AlmostQhasm.Program x):
option (Qhasm.Program y) :=
Some (almostToQhasm' prog 0%N).
Definition convertState x y (st: Qhasm.State y):
option (AlmostQhasm.State x) :=
Some st.
Lemma convert_spec: forall pa pb a a' b b' prog prog',
convertProgram pa pb prog = Some prog' ->
convertState pa pb a = Some a' ->
convertState pa pb b = Some b' ->
Qhasm.evaluatesTo pb prog' a b <-> AlmostQhasm.evaluatesTo pa prog a' b'.
Admitted.
End AlmostConversion.
|
