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

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 15
Let: mType -> nat -> expr V -> cmd V -> cmd V
| Ret: expr 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 REAL x (toREval e) (toREvalCmd g)
33 34 35
  |Ret e => Ret (toREval e)
  end.

36 37
(*
UNUSED!
38
   Small Step semantics for Flover language
39 40
Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
  let_s x e s E v eps:
41
    eval_expr eps E e v ->
42 43
    sstep (Let x e s) E eps s (updEnv x v E)
 |ret_s e E v eps:
44
    eval_expr eps E e v ->
45 46
    sstep (Ret e) E eps (Nop R) (updEnv 0 v E).
 *)
47 48

(**
49
  Define big step semantics for the Flover language, terminating on a "returned"
50
  result value
51
 **)
52 53
Inductive bstep : cmd R -> env -> (nat -> option mType) -> R -> mType -> Prop :=
  let_b m m' x e s E v res defVars:
54
    eval_expr E defVars e v m ->
55
    bstep s (updEnv x v E) (updDefVars x m defVars) res m' ->
56 57
    bstep (Let m x e s) E defVars res m'
 |ret_b m e E v defVars:
58
    eval_expr E defVars e v m ->
59
    bstep (Ret e) E defVars v m.
Heiko Becker's avatar
Heiko Becker committed
60

61
(**
62
  The free variables of a command are all used variables of exprressions
63 64
  without the let bound variables
**)
65
Fixpoint freeVars V (f:cmd V) :NatSet.t :=
Heiko Becker's avatar
Heiko Becker committed
66
  match f with
67 68
  | 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
69 70
  end.

71 72 73
(**
  The defined variables of a command are all let bound variables
**)
74
Fixpoint definedVars V (f:cmd V) :NatSet.t :=
Heiko Becker's avatar
Heiko Becker committed
75
  match f with
76
  | Let _ x _ g => NatSet.add x (definedVars g)
77
  | Ret _ => NatSet.empty
78 79 80 81 82 83 84 85
  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
86
  | Let _ _ e g => NatSet.union (usedVars e) (liveVars g)
87
  | Ret e => usedVars e
88
  end.
Heiko Becker's avatar
Heiko Becker committed
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104

Lemma bstep_eq_env f:
  forall E1 E2 Gamma v m,
  (forall x, E1 x = E2 x) ->
  bstep f E1 Gamma v m ->
  bstep f E2 Gamma v m.
Proof.
  induction f; intros * eq_envs bstep_E1;
    inversion bstep_E1; subst; simpl in *.
  -  eapply eval_eq_env in H7; eauto. eapply let_b; eauto.
     eapply IHf. instantiate (1:=(updEnv n v0 E1)).
     + intros; unfold updEnv.
       destruct (x=? n); auto.
     + auto.
  - apply ret_b. eapply eval_eq_env; eauto.
Qed.