Commands.v 2.59 KB
Newer Older
1
2
3
(**
 Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
 **)
Heiko Becker's avatar
Heiko Becker committed
4
Require Import Coq.Reals.Reals Coq.QArith.QArith.
5
Require Import Daisy.Expressions.
6
7
Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet.

8
9
(**
  Next define what a program is.
10
11
  Currently no loops, or conditionals.
  Only assignments and return statement
12
13
**)
Inductive cmd (V:Type) :Type :=
14
Let: mType -> nat -> exp V -> cmd V -> cmd V
15
| Ret: exp V -> cmd V.
16

Raphaël Monat's avatar
Raphaël Monat committed
17
18
19
20
21
22
Fixpoint getRetExp (V:Type) (f:cmd V) :=
  match f with
  |Let m x e g => getRetExp g
  | Ret e => e
  end.

23
24
25
26
27
28
29
30
31

Fixpoint toRCmd (f:cmd Q) :=
  match f with
  |Let m x e g => Let m x (toRExp e) (toRCmd g)
  |Ret e => Ret (toRExp e)
  end.

Fixpoint toREvalCmd (f:cmd R) :=
  match f with
32
  |Let m x e g => Let M0 x (toREval e) (toREvalCmd g)
33
34
35
36
  |Ret e => Ret (toREval e)
  end.


37
(*| Nop: cmd V. *)
38

39
40
(*
UNUSED!
Heiko Becker's avatar
Heiko Becker committed
41
   Small Step semantics for Daisy language
42
43
44
45
46
47
48
49
Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
  let_s x e s E v eps:
    eval_exp eps E e v ->
    sstep (Let x e s) E eps s (updEnv x v E)
 |ret_s e E v eps:
    eval_exp eps E e v ->
    sstep (Ret e) E eps (Nop R) (updEnv 0 v E).
 *)
50
51

(**
52
53
  Define big step semantics for the Daisy language, terminating on a "returned"
  result value
54
 **)
Raphaël Monat's avatar
Raphaël Monat committed
55
56
57
58
59
60
61
62
63
64

(* meaning of this -> mType ??? *)
(* Inductive bstep : cmd R -> env -> R -> mType -> Prop := *)
(*   let_b m x e s E v res: *)
(*     eval_exp E e v m -> *)
(*     bstep s (updEnv x m v E) res m -> *)
(*     bstep (Let m x e s) E res m *)
(*  |ret_b m e E v: *)
(*     eval_exp E e v m -> *)
(*     bstep (Ret e) E v m. *)
65
Inductive bstep : cmd R -> env -> R -> mType -> Prop :=
Raphaël Monat's avatar
Raphaël Monat committed
66
  let_b m m' x e s E v res:
67
    eval_exp E e v m ->
Raphaël Monat's avatar
Raphaël Monat committed
68
69
    bstep s (updEnv x m v E) res m' ->
    bstep (Let m x e s) E res m'
70
71
72
 |ret_b m e E v:
    eval_exp E e v m ->
    bstep (Ret e) E v m.
Heiko Becker's avatar
Heiko Becker committed
73

Raphaël Monat's avatar
Raphaël Monat committed
74

Heiko Becker's avatar
Heiko Becker committed
75

76
77
78
79
(**
  The free variables of a command are all used variables of expressions
  without the let bound variables
**)
80
Fixpoint freeVars V (f:cmd V) :NatSet.t :=
Heiko Becker's avatar
Heiko Becker committed
81
  match f with
82
83
  | Let _ x e1 g => NatSet.remove x (NatSet.union (Expressions.usedVars e1) (freeVars g))
  | Ret e => Expressions.usedVars e
Heiko Becker's avatar
Heiko Becker committed
84
85
  end.

86
87
88
(**
  The defined variables of a command are all let bound variables
**)
89
Fixpoint definedVars V (f:cmd V) :NatSet.t :=
Heiko Becker's avatar
Heiko Becker committed
90
  match f with
91
  | Let _ x _ g => NatSet.add x (definedVars g)
92
  | Ret _ => NatSet.empty
93
94
95
96
97
98
99
100
  end.

(**
  The live variables of a command are all variables which occur on the right
  hand side of an assignment or at a return statement
 **)
Fixpoint liveVars V (f:cmd V) :NatSet.t :=
  match f with
101
  | Let _ _ e g => NatSet.union (usedVars e) (liveVars g)
102
  | Ret e => usedVars e
103
  end.