blob: f3ed925c7bf1cf2a332a298f0ad59df51bc24f54 (
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
65
66
67
68
69
70
71
72
73
74
75
76
77
|
Require Import QhasmCommon QhasmEvalCommon.
Require Import Language.
Require Import List.
Module AlmostQhasm <: Language.
Import QhasmEval.
(* Program Types *)
Definition Params := unit.
Definition State := fun (_: Params) => State.
Inductive AlmostProgram: Set :=
| ASkip: AlmostProgram
| ASeq: AlmostProgram -> AlmostProgram -> AlmostProgram
| AAssign: Assignment -> AlmostProgram
| AOp: Operation -> AlmostProgram
| ACond: Conditional -> AlmostProgram -> AlmostProgram -> AlmostProgram
| AWhile: Conditional -> AlmostProgram -> AlmostProgram
| ADef: Label -> AlmostProgram -> AlmostProgram -> AlmostProgram
| ACall: Label -> AlmostProgram.
Hint Constructors AlmostProgram.
Definition Program := fun (_: Params) => AlmostProgram.
Fixpoint inline (l: nat) (f prog: AlmostProgram) :=
match prog with
| ASeq a b => ASeq (inline l f a) (inline l f b)
| ACond c a b => ACond c (inline l f a) (inline l f b)
| AWhile c a => AWhile c (inline l f a)
| ADef l' f' p' =>
if (Nat.eq_dec l l')
then prog
else ADef l' (inline l f f') (inline l f p')
| ACall l' =>
if (Nat.eq_dec l l')
then f
else prog
| _ => prog
end.
Inductive AlmostEval {x: Params}: Program x -> State x -> State x -> Prop :=
| AESkip: forall s, AlmostEval ASkip s s
| AESeq: forall p p' s s' s'',
AlmostEval p s s'
-> AlmostEval p' s' s''
-> AlmostEval (ASeq p p') s s''
| AEAssign a: forall s s',
evalAssignment a s = Some s'
-> AlmostEval (AAssign a) s s'
| AEOp: forall s s' a,
evalOperation a s = Some s'
-> AlmostEval (AOp a) s s'
| AECondFalse: forall c a b s s',
evalCond c s = Some false
-> AlmostEval b s s'
-> AlmostEval (ACond c a b) s s'
| AECondTrue: forall c a b s s',
evalCond c s = Some true
-> AlmostEval a s s'
-> AlmostEval (ACond c a b) s s'
| AEWhileRun: forall c a s s' s'',
evalCond c s = Some true
-> AlmostEval a s s'
-> AlmostEval (AWhile c a) s' s''
-> AlmostEval (AWhile c a) s s''
| AEWhileSkip: forall c a s,
evalCond c s = Some false
-> AlmostEval (AWhile c a) s s
| AEFun: forall l f p s s',
AlmostEval (inline l f p) s s'
-> AlmostEval (ADef l f p) s s'.
Definition evaluatesTo := @AlmostEval.
(* world peace *)
End AlmostQhasm.
|
