-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathast_util.v
109 lines (79 loc) · 2.76 KB
/
ast_util.v
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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
(**
_AUTHOR_
<<
Zhi Zhang
Department of Computer and Information Sciences
Kansas State University
>>
*)
Require Export ast_rt.
(** * Auxiliary Functions for AST *)
Section AuxiliaryFunctions_For_AST.
End AuxiliaryFunctions_For_AST.
(** * Auxiliary Functions for AST_RT *)
Section AuxiliaryFunctions_For_AST_RT.
(** Check Flags Extraction Functions *)
Function name_exterior_checks (n: nameRT): exterior_checks :=
match n with
| IdentifierRT ast_num x ex_cks => ex_cks
| IndexedComponentRT ast_num x e ex_cks => ex_cks
| SelectedComponentRT ast_num x f ex_cks => ex_cks
end.
Function exp_exterior_checks (e: expRT): exterior_checks :=
match e with
| LiteralRT ast_num l in_cks ex_cks => ex_cks
| NameRT ast_num n => name_exterior_checks n
| BinOpRT ast_num op e1 e2 in_cks ex_cks => ex_cks
| UnOpRT ast_num op e in_cks ex_cks => ex_cks
end.
Definition update_exterior_checks_name n checks :=
match n with
| IdentifierRT ast_num x ex_checks => IdentifierRT ast_num x checks
| IndexedComponentRT ast_num x e ex_checks => IndexedComponentRT ast_num x e checks
| SelectedComponentRT ast_num x f ex_checks => SelectedComponentRT ast_num x f checks
end.
Definition update_exterior_checks_exp e checks :=
match e with
| LiteralRT ast_num l in_checks ex_checks => LiteralRT ast_num l in_checks checks
| NameRT ast_num n =>
let n' := update_exterior_checks_name n checks in
NameRT ast_num n'
| BinOpRT ast_num bop e1 e2 in_checks ex_checks => BinOpRT ast_num bop e1 e2 in_checks checks
| UnOpRT ast_num uop e in_checks ex_checks => UnOpRT ast_num uop e in_checks checks
end.
Lemma exp_updated_exterior_checks: forall e cks,
exp_exterior_checks (update_exterior_checks_exp e cks) = cks.
Proof.
intros; destruct e; smack;
destruct n; smack.
Qed.
Lemma name_updated_exterior_checks: forall n cks,
name_exterior_checks (update_exterior_checks_name n cks) = cks.
Proof.
intros; destruct n; smack.
Qed.
Lemma exp_exterior_checks_refl: forall e,
update_exterior_checks_exp e (exp_exterior_checks e) = e.
Proof.
destruct e; smack.
destruct n; simpl; smack.
Qed.
Lemma name_exterior_checks_refl: forall n,
update_exterior_checks_name n (name_exterior_checks n) = n.
Proof.
destruct n; smack.
Qed.
Lemma update_exterior_checks_exp_astnum_eq: forall e cks,
expression_astnum_rt (update_exterior_checks_exp e cks) = expression_astnum_rt e.
Proof.
intros;
destruct e; smack.
Qed.
Lemma update_exterior_checks_name_astnum_eq: forall n cks,
name_astnum_rt (update_exterior_checks_name n cks) = name_astnum_rt n.
Proof.
intros;
destruct n; smack.
Qed.
End AuxiliaryFunctions_For_AST_RT.