-
Notifications
You must be signed in to change notification settings - Fork 0
/
type_check.ml
161 lines (153 loc) · 3.78 KB
/
type_check.ml
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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
open Format
open Parsed
exception Not_found
exception Not_Math_Expr
exception Not_Int_Real
exception Not_Int_Real_Bool
type int_or_real_or_bool = Is_Int | Is_Real | Is_Bool
let fmt1 = std_formatter
let rec find_in_local_vars id l =
if List.mem id l.int_vars then Is_Int
else if List.mem id l.real_vars then Is_Real
else if List.mem id l.bool_vars then Is_Bool
else raise Not_found
let rec find_in_global_vars id g =
if List.mem id g.i_vars then Is_Int
else if List.mem id g.r_vars then Is_Real
else if List.mem id g.b_vars then Is_Bool
else raise Not_found
let rec find_in_global_funs id g =
if List.mem id g.i_funs then Is_Int
else if List.mem id g.r_funs then Is_Real
else if List.mem id g.b_funs then Is_Bool
else raise Not_found
let rec type_lexpr exp g l=
let {pp_loc;pp_desc} = exp in
match pp_desc with
| PPvar id ->
begin
try find_in_local_vars id l
with Not_found ->
begin
try find_in_global_vars id g
with Not_found ->
begin
Loc.report fmt1 pp_loc;
raise Not_Int_Real_Bool
end
end
end
| PPapp (id, exp_lst) ->
begin
try find_in_global_funs id g
with Not_found ->
begin
Loc.report fmt1 pp_loc;
raise Not_Int_Real_Bool
end
end
| PPconst const ->
begin
match const with
| ConstInt _ -> Is_Int
| ConstReal _ -> Is_Real
| ConstTrue | ConstFalse -> Is_Bool
| _ ->
begin
Loc.report fmt1 pp_loc;
raise Not_Int_Real_Bool
end
end
| PPinfix (lexp, op, rexp) ->
begin
match op with
| PPand | PPor | PPimplies | PPiff
| PPlt | PPle | PPgt | PPge | PPeq
| PPneq -> Is_Bool
| PPadd | PPsub
| PPmul | PPdiv -> type_lexpr lexp g l
| PPmod -> Is_Int
end
| PPprefix (op, exp) ->
begin
match op with
| PPneg -> type_lexpr exp g l
| PPnot -> Is_Bool
end
| PPget (lexp, rexp) ->
begin
match lexp.pp_desc with
| PPvar id ->
begin
try find_in_local_vars id l
with Not_found ->
begin
try find_in_global_vars id g
with Not_found ->
begin
Loc.report fmt1 lexp.pp_loc;
raise Not_Int_Real_Bool
end
end
end
| PPset (e1, e2, e3) ->
begin
match e1.pp_desc with
| PPvar id1 ->
begin
try find_in_local_vars id1 l
with Not_found ->
begin
try find_in_global_vars id1 g
with Not_found ->
begin
Loc.report fmt1 e1.pp_loc;
raise Not_Int_Real_Bool
end
end
end
| _ -> assert false
end
| _ -> assert false
end
| PPset (lexp,mexp,rexp) -> assert false
| PPdot (exp, id) -> assert false
(* begin
try find_in_local_vars id l
with Not_found ->
begin
try find_in_global_vars id g
with Not_found -> raise Not_Int_Real_Bool
end
end*)
| PPrecord lbl_lst -> assert false
| PPwith (exp, lbl_lst) -> assert false
| PPextract (lexp, mexp, rexp) -> assert false
| PPconcat (lexp, rexp) -> assert false
| PPif (lexp, mexp, rexp) -> assert false
| PPforall (vars, pp_ty, exp_lst_lst, exp) ->
assert false
| PPexists (vars, pp_ty, exp_lst_lst, exp) ->
assert false
| PPforall_named (id_lst, pp_ty, exp_lst_lst, exp) ->
assert false
| PPexists_named (id_lst, pp_ty, exp_lst_lst, exp) ->
assert false
| PPnamed (id, exp) -> assert false
| PPlet (id, lexp, rexp) -> assert false
| PPcheck exp -> assert false
| PPcut exp -> assert false
| PPcast (e, pp_ty) ->
begin
match pp_ty with
| PPTint -> Is_Int
| PPTreal -> Is_Real
| PPTbool -> Is_Bool
| _ ->
begin
Loc.report fmt1 e.pp_loc;
raise Not_Math_Expr
end
end
| PPinInterval _ -> assert false
| PPdistinct exp_lst -> assert false