Revision ca7ff3f7
Added by Lélio Brun 7 months ago
| src/checks/init_calculus.ml | ||
|---|---|---|
| 12 | 12 |
(** Main typing module. Classic inference algorithm with destructive |
| 13 | 13 |
unification. *) |
| 14 | 14 |
|
| 15 |
(* Though it shares similarities with the clock calculus module, no code |
|
| 16 |
is shared. Simple environments, very limited identifier scoping, no
|
|
| 17 |
identifier redefinition allowed. *)
|
|
| 15 |
(* Though it shares similarities with the clock calculus module, no code is
|
|
| 16 |
shared. Simple environments, very limited identifier scoping, no identifier
|
|
| 17 |
redefinition allowed. *) |
|
| 18 | 18 |
|
| 19 | 19 |
open Utils |
| 20 |
(* Yes, opening both modules is dirty as some type names will be |
|
| 21 |
overwritten, yet this makes notations far lighter.*) |
|
| 20 |
|
|
| 21 |
(* Yes, opening both modules is dirty as some type names will be overwritten, |
|
| 22 |
yet this makes notations far lighter.*) |
|
| 22 | 23 |
open Corelang |
| 23 | 24 |
open Init |
| 24 | 25 |
open Format |
| 25 | 26 |
|
| 26 |
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in |
|
| 27 |
type [ty]. False otherwise. *)
|
|
| 27 |
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in type
|
|
| 28 |
[ty]. False otherwise. *) |
|
| 28 | 29 |
let rec occurs tvar ty = |
| 29 | 30 |
let ty = repr ty in |
| 30 | 31 |
match ty.tdesc with |
| 31 |
| Ivar -> ty=tvar |
|
| 32 |
| Ivar -> |
|
| 33 |
ty = tvar |
|
| 32 | 34 |
| Iarrow (t1, t2) -> |
| 33 |
(occurs tvar t1) || (occurs tvar t2)
|
|
| 35 |
occurs tvar t1 || occurs tvar t2
|
|
| 34 | 36 |
| Ituple tl -> |
| 35 |
List.exists (occurs tvar) tl |
|
| 36 |
| Ilink t -> occurs tvar t |
|
| 37 |
| Isucc t -> occurs tvar t |
|
| 38 |
| Iunivar -> false |
|
| 37 |
List.exists (occurs tvar) tl |
|
| 38 |
| Ilink t -> |
|
| 39 |
occurs tvar t |
|
| 40 |
| Isucc t -> |
|
| 41 |
occurs tvar t |
|
| 42 |
| Iunivar -> |
|
| 43 |
false |
|
| 39 | 44 |
|
| 40 |
(** Promote monomorphic type variables to polymorphic type variables. *) |
|
| 41 | 45 |
(* Generalize by side-effects *) |
| 46 |
|
|
| 47 |
(** Promote monomorphic type variables to polymorphic type variables. *) |
|
| 42 | 48 |
let rec generalize ty = |
| 43 | 49 |
match ty.tdesc with |
| 44 | 50 |
| Ivar -> |
| 45 |
(* No scopes, always generalize *) |
|
| 46 |
ty.idesc <- Iunivar |
|
| 47 |
| Iarrow (t1,t2) -> |
|
| 48 |
generalize t1; generalize t2 |
|
| 51 |
(* No scopes, always generalize *) |
|
| 52 |
ty.idesc <- Iunivar |
|
| 53 |
| Iarrow (t1, t2) -> |
|
| 54 |
generalize t1; |
|
| 55 |
generalize t2 |
|
| 49 | 56 |
| Ituple tlist -> |
| 50 |
List.iter generalize tlist
|
|
| 57 |
List.iter generalize tlist |
|
| 51 | 58 |
| Ilink t -> |
| 52 |
generalize t
|
|
| 59 |
generalize t |
|
| 53 | 60 |
| Isucc t -> |
| 54 |
generalize t |
|
| 55 |
| Tunivar -> () |
|
| 61 |
generalize t |
|
| 62 |
| Tunivar -> |
|
| 63 |
() |
|
| 56 | 64 |
|
| 57 | 65 |
(** Downgrade polymorphic type variables to monomorphic type variables *) |
| 58 | 66 |
let rec instanciate inst_vars ty = |
| 59 | 67 |
let ty = repr ty in |
| 60 | 68 |
match ty.idesc with |
| 61 |
| Ivar -> ty |
|
| 62 |
| Iarrow (t1,t2) -> |
|
| 63 |
{ty with idesc =
|
|
| 64 |
Iarrow ((instanciate inst_vars t1), (instanciate inst_vars t2))} |
|
| 69 |
| Ivar -> |
|
| 70 |
ty |
|
| 71 |
| Iarrow (t1, t2) -> |
|
| 72 |
{
|
|
| 73 |
ty with |
|
| 74 |
idesc = Iarrow (instanciate inst_vars t1, instanciate inst_vars t2); |
|
| 75 |
} |
|
| 65 | 76 |
| Ituple tlist -> |
| 66 |
{ty with idesc = Ituple (List.map (instanciate inst_vars) tlist)}
|
|
| 77 |
{ ty with idesc = Ituple (List.map (instanciate inst_vars) tlist) }
|
|
| 67 | 78 |
| Isucc t -> |
| 68 |
(* should not happen *)
|
|
| 69 |
{ty with idesc = Isucc (instanciate inst_vars t)}
|
|
| 79 |
(* should not happen *)
|
|
| 80 |
{ ty with idesc = Isucc (instanciate inst_vars t) }
|
|
| 70 | 81 |
| Ilink t -> |
| 71 |
(* should not happen *) |
|
| 72 |
{ty with idesc = Ilink (instanciate inst_vars t)}
|
|
| 73 |
| Iunivar -> |
|
| 74 |
try |
|
| 75 |
List.assoc ty.iid !inst_vars |
|
| 76 |
with Not_found -> |
|
| 77 |
let var = new_var () in |
|
| 78 |
inst_vars := (ty.iid, var)::!inst_vars; |
|
| 79 |
var |
|
| 82 |
(* should not happen *) |
|
| 83 |
{ ty with idesc = Ilink (instanciate inst_vars t) }
|
|
| 84 |
| Iunivar -> ( |
|
| 85 |
try List.assoc ty.iid !inst_vars |
|
| 86 |
with Not_found -> |
|
| 87 |
let var = new_var () in |
|
| 88 |
inst_vars := (ty.iid, var) :: !inst_vars; |
|
| 89 |
var) |
|
| 80 | 90 |
|
| 81 |
(** [unify env t1 t2] unifies types [t1] and [t2]. Raises [Unify |
|
| 82 |
(t1,t2)] if the types are not unifiable.*)
|
|
| 91 |
(** [unify env t1 t2] unifies types [t1] and [t2]. Raises [Unify (t1,t2)] if the
|
|
| 92 |
types are not unifiable.*) |
|
| 83 | 93 |
|
| 84 | 94 |
(* Standard destructive unification *) |
| 85 | 95 |
(* may loop for omega types *) |
| 86 | 96 |
let rec unify t1 t2 = |
| 87 | 97 |
let t1 = repr t1 in |
| 88 | 98 |
let t2 = repr t2 in |
| 89 |
if t1=t2 then |
|
| 90 |
() |
|
| 99 |
if t1 = t2 then () |
|
| 91 | 100 |
else |
| 92 | 101 |
(* No type abbreviations resolution for now *) |
| 93 |
match t1.idesc,t2.idesc with |
|
| 94 |
(* This case is not mandory but will keep "older" types *)
|
|
| 102 |
match t1.idesc, t2.idesc with
|
|
| 103 |
(* This case is not mandory but will keep "older" types *) |
|
| 95 | 104 |
| Ivar, Ivar -> |
| 96 |
if t1.iid < t2.iid then |
|
| 97 |
t2.idesc <- Ilink t1 |
|
| 98 |
else |
|
| 99 |
t1.idesc <- Ilink t2 |
|
| 100 |
| (Ivar, _) when (not (occurs t1 t2)) -> |
|
| 101 |
t1.idesc <- Ilink t2 |
|
| 102 |
| (_,Ivar) when (not (occurs t2 t1)) -> |
|
| 103 |
t2.idesc <- Ilink t1 |
|
| 104 |
| Isucc t1, Isucc t1' -> unify t1 t1' |
|
| 105 |
| Iarrow (t1,t2), Iarrow (t1',t2') -> |
|
| 106 |
unify t1 t1'; unify t2 t2' |
|
| 105 |
if t1.iid < t2.iid then t2.idesc <- Ilink t1 else t1.idesc <- Ilink t2 |
|
| 106 |
| Ivar, _ when not (occurs t1 t2) -> |
|
| 107 |
t1.idesc <- Ilink t2 |
|
| 108 |
| _, Ivar when not (occurs t2 t1) -> |
|
| 109 |
t2.idesc <- Ilink t1 |
|
| 110 |
| Isucc t1, Isucc t1' -> |
|
| 111 |
unify t1 t1' |
|
| 112 |
| Iarrow (t1, t2), Iarrow (t1', t2') -> |
|
| 113 |
unify t1 t1'; |
|
| 114 |
unify t2 t2' |
|
| 107 | 115 |
| Ituple tlist1, Ituple tlist2 -> |
| 108 |
if (List.length tlist1) <> (List.length tlist2) then |
|
| 109 |
raise (Unify (t1, t2)) |
|
| 110 |
else |
|
| 111 |
List.iter2 unify tlist1 tlist2 |
|
| 112 |
| Iunivar,_ | _, Iunivar -> |
|
| 113 |
() |
|
| 114 |
| _,_ -> raise (Unify (t1, t2)) |
|
| 116 |
if List.length tlist1 <> List.length tlist2 then raise (Unify (t1, t2)) |
|
| 117 |
else List.iter2 unify tlist1 tlist2 |
|
| 118 |
| Iunivar, _ | _, Iunivar -> |
|
| 119 |
() |
|
| 120 |
| _, _ -> |
|
| 121 |
raise (Unify (t1, t2)) |
|
| 115 | 122 |
|
| 116 |
let init_of_const c = |
|
| 117 |
Init_predef.init_zero |
|
| 123 |
let init_of_const c = Init_predef.init_zero |
|
| 118 | 124 |
|
| 119 | 125 |
let rec init_expect env in_main expr ty = |
| 120 | 126 |
let texpr = init_expr env in_main expr in |
| 121 |
try |
|
| 122 |
unify texpr ty |
|
| 123 |
with Unify (t1,t2) -> |
|
| 124 |
raise (Error (expr.expr_loc, Init_clash (t1,t2))) |
|
| 127 |
try unify texpr ty |
|
| 128 |
with Unify (t1, t2) -> raise (Error (expr.expr_loc, Init_clash (t1, t2))) |
|
| 125 | 129 |
|
| 126 |
and init_ident env in_main id loc = |
|
| 127 |
init_expr env in_main (expr_of_ident id loc) |
|
| 130 |
and init_ident env in_main id loc = init_expr env in_main (expr_of_ident id loc) |
|
| 128 | 131 |
|
| 129 |
(** [type_expr env in_main expr] types expression [expr] in environment |
|
| 130 |
[env]. *) |
|
| 132 |
(** [type_expr env in_main expr] types expression [expr] in environment [env]. *) |
|
| 131 | 133 |
and init_expr env in_main expr = |
| 132 | 134 |
match expr.expr_desc with |
| 133 | 135 |
| Expr_const c -> |
| 134 |
let ty = init_of_const c in
|
|
| 135 |
expr.expr_init <- ty;
|
|
| 136 |
ty
|
|
| 136 |
let ty = init_of_const c in |
|
| 137 |
expr.expr_init <- ty; |
|
| 138 |
ty |
|
| 137 | 139 |
| Expr_ident v -> |
| 138 |
let tyv = |
|
| 139 |
try |
|
| 140 |
Env.lookup_value env v |
|
| 141 |
with Not_found -> |
|
| 142 |
raise (Error (expr.expr_loc, Unbound_value v)) |
|
| 143 |
in |
|
| 144 |
let ty = instanciate (ref []) tyv in |
|
| 145 |
expr.expr_init <- ty; |
|
| 146 |
ty |
|
| 140 |
let tyv = |
|
| 141 |
try Env.lookup_value env v |
|
| 142 |
with Not_found -> raise (Error (expr.expr_loc, Unbound_value v)) |
|
| 143 |
in |
|
| 144 |
let ty = instanciate (ref []) tyv in |
|
| 145 |
expr.expr_init <- ty; |
|
| 146 |
ty |
|
| 147 | 147 |
| Expr_tuple elist -> |
| 148 |
let ty = new_ty (Ttuple (List.map (type_expr env in_main) elist)) in
|
|
| 149 |
expr.expr_init <- ty;
|
|
| 150 |
ty
|
|
| 148 |
let ty = new_ty (Ttuple (List.map (type_expr env in_main) elist)) in |
|
| 149 |
expr.expr_init <- ty; |
|
| 150 |
ty |
|
| 151 | 151 |
| Expr_appl (id, args, r) -> |
| 152 | 152 |
(match r with |
| 153 |
| None -> () |
|
| 154 |
| Some x -> let expr_x = expr_of_ident x expr.expr_loc in |
|
| 155 |
init_expect env in_main expr_x Init_predef.init_zero); |
|
| 156 |
let tfun = type_ident env in_main id expr.expr_loc in |
|
| 157 |
let tins,touts= split_arrow tfun in |
|
| 158 |
type_expect env in_main args tins; |
|
| 159 |
expr.expr_type <- touts; |
|
| 160 |
touts |
|
| 161 |
| Expr_arrow (e1,e2) -> |
|
| 162 |
let ty = type_expr env in_main e1 in |
|
| 163 |
type_expect env in_main e2 ty; |
|
| 164 |
expr.expr_type <- ty; |
|
| 165 |
ty |
|
| 166 |
| Expr_fby (init,e) -> |
|
| 167 |
let ty = type_of_const init in |
|
| 168 |
type_expect env in_main e ty; |
|
| 169 |
expr.expr_type <- ty; |
|
| 170 |
ty |
|
| 171 |
| Expr_concat (hd,e) -> |
|
| 172 |
let ty = type_of_const hd in |
|
| 173 |
type_expect env in_main e ty; |
|
| 174 |
expr.expr_type <- ty; |
|
| 175 |
ty |
|
| 153 |
| None -> |
|
| 154 |
() |
|
| 155 |
| Some x -> |
|
| 156 |
let expr_x = expr_of_ident x expr.expr_loc in |
|
| 157 |
init_expect env in_main expr_x Init_predef.init_zero); |
|
| 158 |
let tfun = type_ident env in_main id expr.expr_loc in |
|
| 159 |
let tins, touts = split_arrow tfun in |
|
| 160 |
type_expect env in_main args tins; |
|
| 161 |
expr.expr_type <- touts; |
|
| 162 |
touts |
|
| 163 |
| Expr_arrow (e1, e2) -> |
|
| 164 |
let ty = type_expr env in_main e1 in |
|
| 165 |
type_expect env in_main e2 ty; |
|
| 166 |
expr.expr_type <- ty; |
|
| 167 |
ty |
|
| 168 |
| Expr_fby (init, e) -> |
|
| 169 |
let ty = type_of_const init in |
|
| 170 |
type_expect env in_main e ty; |
|
| 171 |
expr.expr_type <- ty; |
|
| 172 |
ty |
|
| 173 |
| Expr_concat (hd, e) -> |
|
| 174 |
let ty = type_of_const hd in |
|
| 175 |
type_expect env in_main e ty; |
|
| 176 |
expr.expr_type <- ty; |
|
| 177 |
ty |
|
| 176 | 178 |
| Expr_tail e -> |
| 177 |
let ty = type_expr env in_main e in
|
|
| 178 |
expr.expr_type <- ty;
|
|
| 179 |
ty
|
|
| 179 |
let ty = type_expr env in_main e in |
|
| 180 |
expr.expr_type <- ty; |
|
| 181 |
ty |
|
| 180 | 182 |
| Expr_pre e -> |
| 181 |
let ty = type_expr env in_main e in
|
|
| 182 |
expr.expr_type <- ty;
|
|
| 183 |
ty
|
|
| 184 |
| Expr_when (e1,c) | Expr_whennot (e1,c) ->
|
|
| 185 |
let expr_c = expr_of_ident c expr.expr_loc in
|
|
| 186 |
type_expect env in_main expr_c Type_predef.type_bool;
|
|
| 187 |
let tlarg = type_expr env in_main e1 in
|
|
| 188 |
expr.expr_type <- tlarg;
|
|
| 189 |
tlarg
|
|
| 190 |
| Expr_merge (c,e2,e3) ->
|
|
| 191 |
let expr_c = expr_of_ident c expr.expr_loc in
|
|
| 192 |
type_expect env in_main expr_c Type_predef.type_bool;
|
|
| 193 |
let te2 = type_expr env in_main e2 in
|
|
| 194 |
type_expect env in_main e3 te2;
|
|
| 195 |
expr.expr_type <- te2;
|
|
| 196 |
te2
|
|
| 197 |
| Expr_uclock (e,k) | Expr_dclock (e,k) ->
|
|
| 198 |
let ty = type_expr env in_main e in
|
|
| 199 |
expr.expr_type <- ty;
|
|
| 200 |
ty
|
|
| 201 |
| Expr_phclock (e,q) -> |
|
| 202 |
let ty = type_expr env in_main e in
|
|
| 203 |
expr.expr_type <- ty;
|
|
| 204 |
ty
|
|
| 183 |
let ty = type_expr env in_main e in |
|
| 184 |
expr.expr_type <- ty; |
|
| 185 |
ty |
|
| 186 |
| Expr_when (e1, c) | Expr_whennot (e1, c) ->
|
|
| 187 |
let expr_c = expr_of_ident c expr.expr_loc in |
|
| 188 |
type_expect env in_main expr_c Type_predef.type_bool; |
|
| 189 |
let tlarg = type_expr env in_main e1 in |
|
| 190 |
expr.expr_type <- tlarg; |
|
| 191 |
tlarg |
|
| 192 |
| Expr_merge (c, e2, e3) ->
|
|
| 193 |
let expr_c = expr_of_ident c expr.expr_loc in |
|
| 194 |
type_expect env in_main expr_c Type_predef.type_bool; |
|
| 195 |
let te2 = type_expr env in_main e2 in |
|
| 196 |
type_expect env in_main e3 te2; |
|
| 197 |
expr.expr_type <- te2; |
|
| 198 |
te2 |
|
| 199 |
| Expr_uclock (e, k) | Expr_dclock (e, k) ->
|
|
| 200 |
let ty = type_expr env in_main e in |
|
| 201 |
expr.expr_type <- ty; |
|
| 202 |
ty |
|
| 203 |
| Expr_phclock (e, q) ->
|
|
| 204 |
let ty = type_expr env in_main e in |
|
| 205 |
expr.expr_type <- ty; |
|
| 206 |
ty |
|
| 205 | 207 |
|
| 206 | 208 |
(** [type_eq env eq] types equation [eq] in environment [env] *) |
| 207 | 209 |
let type_eq env in_main undefined_vars eq = |
| 208 | 210 |
(* Check multiple variable definitions *) |
| 209 | 211 |
let define_var id uvars = |
| 210 | 212 |
try |
| 211 |
ignore(IMap.find id uvars); |
|
| 213 |
ignore (IMap.find id uvars);
|
|
| 212 | 214 |
IMap.remove id uvars |
| 213 |
with Not_found -> |
|
| 214 |
raise (Error (eq.eq_loc, Already_defined id)) |
|
| 215 |
with Not_found -> raise (Error (eq.eq_loc, Already_defined id)) |
|
| 215 | 216 |
in |
| 216 | 217 |
let undefined_vars = |
| 217 |
List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in |
|
| 218 |
List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs |
|
| 219 |
in |
|
| 218 | 220 |
(* Type lhs *) |
| 219 | 221 |
let get_value_type id = |
| 220 |
try |
|
| 221 |
Env.lookup_value env id |
|
| 222 |
with Not_found -> |
|
| 223 |
raise (Error (eq.eq_loc, Unbound_value id)) |
|
| 222 |
try Env.lookup_value env id |
|
| 223 |
with Not_found -> raise (Error (eq.eq_loc, Unbound_value id)) |
|
| 224 | 224 |
in |
| 225 | 225 |
let tyl_lhs = List.map get_value_type eq.eq_lhs in |
| 226 | 226 |
let ty_lhs = type_of_type_list tyl_lhs in |
| 227 |
(* Type rhs *)
|
|
| 227 |
(* Type rhs *) |
|
| 228 | 228 |
type_expect env in_main eq.eq_rhs ty_lhs; |
| 229 | 229 |
undefined_vars |
| 230 | 230 |
|
| 231 | 231 |
(* [type_coretype cty] types the type declaration [cty] *) |
| 232 | 232 |
let type_coretype cty = |
| 233 | 233 |
match cty with |
| 234 |
| Tydec_any -> new_var () |
|
| 235 |
| Tydec_int -> Type_predef.type_int |
|
| 236 |
| Tydec_real -> Type_predef.type_real |
|
| 237 |
| Tydec_float -> Type_predef.type_real |
|
| 238 |
| Tydec_bool -> Type_predef.type_bool |
|
| 239 |
| Tydec_clock -> Type_predef.type_clock |
|
| 234 |
| Tydec_any -> |
|
| 235 |
new_var () |
|
| 236 |
| Tydec_int -> |
|
| 237 |
Type_predef.type_int |
|
| 238 |
| Tydec_real -> |
|
| 239 |
Type_predef.type_real |
|
| 240 |
| Tydec_float -> |
|
| 241 |
Type_predef.type_real |
|
| 242 |
| Tydec_bool -> |
|
| 243 |
Type_predef.type_bool |
|
| 244 |
| Tydec_clock -> |
|
| 245 |
Type_predef.type_clock |
|
| 240 | 246 |
|
| 241 |
(* [type_coreclock env ck id loc] types the type clock declaration [ck] |
|
| 242 |
in environment [env] *)
|
|
| 247 |
(* [type_coreclock env ck id loc] types the type clock declaration [ck] in
|
|
| 248 |
environment [env] *) |
|
| 243 | 249 |
let type_coreclock env ck id loc = |
| 244 | 250 |
match ck.ck_dec_desc with |
| 245 |
| Ckdec_any | Ckdec_pclock (_,_) -> () |
|
| 251 |
| Ckdec_any | Ckdec_pclock (_, _) -> |
|
| 252 |
() |
|
| 246 | 253 |
| Ckdec_bool cl -> |
| 247 |
let dummy_id_expr = expr_of_ident id loc in |
|
| 248 |
let when_expr = |
|
| 249 |
List.fold_left |
|
| 250 |
(fun expr c -> |
|
| 251 |
match c with |
|
| 252 |
| Wtrue id -> |
|
| 253 |
{expr_tag = new_tag ();
|
|
| 254 |
expr_desc=Expr_when (expr,id); |
|
| 255 |
expr_type = new_var (); |
|
| 256 |
expr_clock = Clocks.new_var true; |
|
| 257 |
expr_loc=loc} |
|
| 258 |
| Wfalse id -> |
|
| 259 |
{expr_tag = new_tag ();
|
|
| 260 |
expr_desc=Expr_whennot (expr,id); |
|
| 261 |
expr_type = new_var (); |
|
| 262 |
expr_clock = Clocks.new_var true; |
|
| 263 |
expr_loc=loc}) |
|
| 264 |
dummy_id_expr cl |
|
| 265 |
in |
|
| 266 |
ignore (type_expr env false when_expr) |
|
| 254 |
let dummy_id_expr = expr_of_ident id loc in |
|
| 255 |
let when_expr = |
|
| 256 |
List.fold_left |
|
| 257 |
(fun expr c -> |
|
| 258 |
match c with |
|
| 259 |
| Wtrue id -> |
|
| 260 |
{
|
|
| 261 |
expr_tag = new_tag (); |
|
| 262 |
expr_desc = Expr_when (expr, id); |
|
| 263 |
expr_type = new_var (); |
|
| 264 |
expr_clock = Clocks.new_var true; |
|
| 265 |
expr_loc = loc; |
|
| 266 |
} |
|
| 267 |
| Wfalse id -> |
|
| 268 |
{
|
|
| 269 |
expr_tag = new_tag (); |
|
| 270 |
expr_desc = Expr_whennot (expr, id); |
|
| 271 |
expr_type = new_var (); |
|
| 272 |
expr_clock = Clocks.new_var true; |
|
| 273 |
expr_loc = loc; |
|
| 274 |
}) |
|
| 275 |
dummy_id_expr cl |
|
| 276 |
in |
|
| 277 |
ignore (type_expr env false when_expr) |
|
| 267 | 278 |
|
| 268 | 279 |
let type_var_decl env vdecl = |
| 269 |
if (Env.exists_value env vdecl.var_id) then
|
|
| 270 |
raise (Error (vdecl.var_loc,Already_bound vdecl.var_id)) |
|
| 280 |
if Env.exists_value env vdecl.var_id then
|
|
| 281 |
raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
|
|
| 271 | 282 |
else |
| 272 | 283 |
let ty = type_coretype vdecl.var_dec_type.ty_dec_desc in |
| 273 | 284 |
let new_env = Env.add_value env vdecl.var_id ty in |
| ... | ... | |
| 275 | 286 |
vdecl.var_type <- ty; |
| 276 | 287 |
new_env |
| 277 | 288 |
|
| 278 |
let type_var_decl_list env l = |
|
| 279 |
List.fold_left type_var_decl env l |
|
| 289 |
let type_var_decl_list env l = List.fold_left type_var_decl env l |
|
| 280 | 290 |
|
| 281 | 291 |
let type_of_vlist vars = |
| 282 | 292 |
let tyl = List.map (fun v -> v.var_type) vars in |
| 283 | 293 |
type_of_type_list tyl |
| 284 |
|
|
| 285 |
(** [type_node env nd loc] types node [nd] in environment env. The |
|
| 286 |
location is used for error reports. *)
|
|
| 294 |
|
|
| 295 |
(** [type_node env nd loc] types node [nd] in environment env. The location is
|
|
| 296 |
used for error reports. *) |
|
| 287 | 297 |
let type_node env nd loc = |
| 288 | 298 |
let is_main = nd.node_id = !Options.main_node in |
| 289 | 299 |
let delta_env = type_var_decl_list IMap.empty nd.node_inputs in |
| ... | ... | |
| 293 | 303 |
let undefined_vars_init = |
| 294 | 304 |
List.fold_left |
| 295 | 305 |
(fun uvs v -> IMap.add v.var_id () uvs) |
| 296 |
IMap.empty (nd.node_outputs@nd.node_locals) in |
|
| 306 |
IMap.empty |
|
| 307 |
(nd.node_outputs @ nd.node_locals) |
|
| 308 |
in |
|
| 297 | 309 |
let undefined_vars = |
| 298 | 310 |
List.fold_left (type_eq new_env is_main) undefined_vars_init nd.node_eqs |
| 299 | 311 |
in |
| 300 | 312 |
(* check that table is empty *) |
| 301 |
if (not (IMap.is_empty undefined_vars)) then
|
|
| 302 |
raise (Error (loc,Undefined_var undefined_vars)); |
|
| 313 |
if not (IMap.is_empty undefined_vars) then
|
|
| 314 |
raise (Error (loc, Undefined_var undefined_vars));
|
|
| 303 | 315 |
let ty_ins = type_of_vlist nd.node_inputs in |
| 304 | 316 |
let ty_outs = type_of_vlist nd.node_outputs in |
| 305 |
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in |
|
| 317 |
let ty_node = new_ty (Tarrow (ty_ins, ty_outs)) in
|
|
| 306 | 318 |
generalize ty_node; |
| 307 | 319 |
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *) |
| 308 | 320 |
nd.node_type <- ty_node; |
| ... | ... | |
| 310 | 322 |
|
| 311 | 323 |
let type_imported_node env nd loc = |
| 312 | 324 |
let new_env = type_var_decl_list env nd.nodei_inputs in |
| 313 |
ignore(type_var_decl_list new_env nd.nodei_outputs); |
|
| 325 |
ignore (type_var_decl_list new_env nd.nodei_outputs);
|
|
| 314 | 326 |
let ty_ins = type_of_vlist nd.nodei_inputs in |
| 315 | 327 |
let ty_outs = type_of_vlist nd.nodei_outputs in |
| 316 |
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in |
|
| 328 |
let ty_node = new_ty (Tarrow (ty_ins, ty_outs)) in
|
|
| 317 | 329 |
generalize ty_node; |
| 318 |
if (is_polymorphic ty_node) then
|
|
| 330 |
if is_polymorphic ty_node then
|
|
| 319 | 331 |
raise (Error (loc, Poly_imported_node nd.nodei_id)); |
| 320 | 332 |
let new_env = Env.add_value env nd.nodei_id ty_node in |
| 321 | 333 |
nd.nodei_type <- ty_node; |
| ... | ... | |
| 323 | 335 |
|
| 324 | 336 |
let type_top_decl env decl = |
| 325 | 337 |
match decl.top_decl_desc with |
| 326 |
| Node nd ->
|
|
| 327 |
type_node env nd decl.top_decl_loc
|
|
| 338 |
| Node nd -> |
|
| 339 |
type_node env nd decl.top_decl_loc |
|
| 328 | 340 |
| ImportedNode nd -> |
| 329 |
type_imported_node env nd decl.top_decl_loc |
|
| 330 |
| SensorDecl _ | ActuatorDecl _ | Consts _ -> env |
|
| 341 |
type_imported_node env nd decl.top_decl_loc |
|
| 342 |
| SensorDecl _ | ActuatorDecl _ | Consts _ -> |
|
| 343 |
env |
|
| 331 | 344 |
|
| 332 | 345 |
let type_top_consts env decl = |
| 333 | 346 |
match decl.top_decl_desc with |
| 334 |
| Consts clist -> |
|
| 335 |
List.fold_left (fun env (id, c) -> |
|
| 336 |
let ty = type_of_const c in |
|
| 337 |
Env.add_value env id ty |
|
| 338 |
) env clist |
|
| 339 |
| Node _ | ImportedNode _ | SensorDecl _ | ActuatorDecl _ -> env |
|
| 347 |
| Consts clist -> |
|
| 348 |
List.fold_left |
|
| 349 |
(fun env (id, c) -> |
|
| 350 |
let ty = type_of_const c in |
|
| 351 |
Env.add_value env id ty) |
|
| 352 |
env clist |
|
| 353 |
| Node _ | ImportedNode _ | SensorDecl _ | ActuatorDecl _ -> |
|
| 354 |
env |
|
| 340 | 355 |
|
| 341 | 356 |
let type_prog env decls = |
| 342 | 357 |
let new_env = List.fold_left type_top_consts env decls in |
| 343 |
ignore(List.fold_left type_top_decl new_env decls) |
|
| 358 |
ignore (List.fold_left type_top_decl new_env decls)
|
|
| 344 | 359 |
|
| 345 | 360 |
(* Local Variables: *) |
| 346 | 361 |
(* compile-command:"make -C .." *) |
Also available in: Unified diff
reformatting