jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

First try at updating Typing

Browse source
This commit is contained in:
Cédric Pasteur 2010-09-10 13:42:45 +02:00
parent e4e429d3fc
commit 1d1f398e8a
2 changed files with 44 additions and 108 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
compiler/global/modules.ml
View file

@ -156,6 +156,9 @@ let add_const f v =
_check_not_defined g_env.consts f;
g_env.consts <- QualEnv.add f v g_env.consts
(** Same as add_value but without checking for redefinition *)
let replace_value f v =
g_env.values <- QualEnv.add f v g_env.values
(** { 3 Find functions look in the global environnement, nothing more } *)
@ -177,6 +180,11 @@ let find_constrs = _find g_env.constrs
let find_field = _find g_env.fields
let find_const = _find g_env.consts
(** @return the fields of a record type. *)
let find_struct n =
match find_type n with
| Tstructure fields -> fields
| _ -> raise Not_found
(** { 3 Load_check functions }
Try to load the needed module and then to find it,

144
compiler/heptagon/analysis/typing.ml
View file

@ -28,7 +28,6 @@ type error =
| Emissingcase of name
| Eundefined of name
| Elast_undefined of name
| Eshould_be_last of name
| Etype_clash of ty * ty
| Earity_clash of int * int
| Estatic_arity_clash of int * int
@ -71,10 +70,6 @@ let message loc kind =
Format.eprintf "%aThe name %s does not have a last value.@."
print_location loc
s;
| Eshould_be_last(s) ->
Format.eprintf "%aOnly the last value of %s can be accessed.@."
print_location loc
s;
| Etype_clash(actual_ty, expected_ty) ->
Format.eprintf "%aType Clash: this expression has type %a, @\n\
but is expected to have type %a.@."
@ -176,15 +171,13 @@ let find_with_error find_fun f =
let add_value = add_with_error add_value
let add_type = add_with_error add_type
let add_constr = add_with_error add_constr
let add_struct = add_with_error add_struct
let add_constrs = add_with_error add_constrs
let add_field = add_with_error add_field
let add_const = add_with_error add_const
let find_value = find_with_error find_value
let find_constr = find_with_error find_constr
let find_constrs = find_with_error find_constrs
let find_field = find_with_error find_field
let find_struct = find_with_error find_struct
(** Constraints related functions *)
let (curr_size_constr : size_constraint list ref) = ref []
@ -197,7 +190,7 @@ let get_size_constraint () =
(** Helper functions to work with types *)
let get_number_of_fields ty =
let { info = tydesc } =
let tydesc =
match ty with
| Tid(f) -> find_type f
| _ -> assert false in
@ -250,28 +243,9 @@ let typ_of_name h x =
with
Not_found -> error (Eundefined(sourcename x))
let typ_of_varname h x =
try
let { ty = ty;last = last } = Env.find x h in
(* Don't understand that - GD 15/02/2009 *)
(* if last then error (Eshould_be_last(x)); *)
ty
with
Not_found -> error (Eundefined(sourcename x))
let typ_of_last h x =
try
let { ty = ty; last = last } = Env.find x h in
if not last then error (Elast_undefined(sourcename x));
(* v.last <- true;*)
ty
with
Not_found -> error (Eundefined(sourcename x))
let desc_of_ty = function
| Tid n when n = pbool -> Tenum ["true";"false"]
| Tid ty_name ->
let { info = tydesc } = find_type ty_name in tydesc
| Tid ty_name -> find_type ty_name
| _ -> Tabstract
let set_of_constr = function
| Tabstract | Tstruct _ -> assert false
@ -283,7 +257,7 @@ let name_mem n env =
in
Env.fold check_one env false
let rec simplify_type = function
(*let rec simplify_type = function
| Tid _ as t -> t
| Tarray(ty, e) ->
Tarray(simplify_type ty, simplify NamesEnv.empty e)
@ -294,7 +268,7 @@ let simplify_type loc ty =
try
simplify_type ty
with
Instanciation_failed -> message loc (Etype_should_be_static ty)
Instanciation_failed -> message loc (Etype_should_be_static ty) *)
let build_subst names values =
if List.length names <> List.length values
@ -407,9 +381,7 @@ let check_static_field_unicity l =
[loc] is the location used for error reporting.*)
let struct_info_from_name n =
try
let { qualname = q;
info = fields } = find_struct n in
q, fields
n, find_struct n
with
Not_found -> error (Erecord_type_expected (Tid n))
@ -426,20 +398,16 @@ let struct_info ty = match ty with
[loc] is the location used for error reporting.*)
let struct_info_from_field f =
try
let { qualname = q; info = n } = find_field f in
struct_info_from_name { qual = q.qual; name = n }
struct_info_from_name (find_field f)
with
Not_found -> error (Eundefined (fullname f))
(** [check_type t] checks that t exists *)
(*TODO should be already done in scoping *)
let rec check_type const_env = function
| Tarray(ty, e) ->
let typed_e = expect_static_exp const_env (Tid Initial.pint) e in
Tarray(check_type const_env ty, typed_e)
| Tid ty_name ->
(try Tid((find_type ty_name).qualname)
with Not_found -> error (Eundefined(fullname ty_name)))
| Tid ty_name -> Tid ty_name
| Tprod l ->
Tprod (List.map (check_type const_env) l)
@ -451,20 +419,18 @@ and typing_static_exp const_env se =
| Sfloat v -> Sfloat v, Tid Initial.pfloat
| Svar ln ->
(try (* this can be a global const*)
let { qualname = q; info = cd } = Modules.find_const ln in
Svar q, cd.Signature.c_type
let cd = Modules.find_const ln in
Svar ln, cd.Signature.c_type
(* TODO verifier... *)
with Not_found -> (* or a static parameter *)
(try Svar ln, QualEnv.find ln const_env
with Not_found -> error (Eundefined_const ln) ) )
Svar ln, QualEnv.find ln const_env)
| Sconstructor c ->
let { qualname = q; info = ty } = find_constr c in
Sconstructor q, ty
Sconstructor c, find_type (find_constrs c)
| Sop (op, se_list) ->
let { qualname = q; info = ty_desc } = find_value op in
let ty_desc = find_value op in
let typed_se_list = typing_static_args const_env
(types_of_arg_list ty_desc.node_inputs) se_list in
Sop (q, typed_se_list),
Sop (op, typed_se_list),
prod (types_of_arg_list ty_desc.node_outputs)
| Sarray_power (se, n) ->
let typed_n = expect_static_exp const_env (Tid Initial.pint) n in
@ -494,7 +460,7 @@ and typing_static_exp const_env se =
check_static_field_unicity f_se_list;
let f_se_list =
List.map (typing_static_field const_env fields
(Tid q) q.qual) f_se_list in
(Tid q)) f_se_list in
Srecord f_se_list, Tid q
in
{ se with se_ty = ty; se_desc = desc }, ty
@ -502,11 +468,11 @@ and typing_static_exp const_env se =
with
TypingError kind -> message se.se_loc kind
and typing_static_field const_env fields t1 modname (f,se) =
and typing_static_field const_env fields t1 (f,se) =
try
let ty = check_type const_env (field_assoc f fields) in
let typed_se = expect_static_exp const_env ty se in
{ qual = modname; name = shortname f }, typed_se
f, typed_se
with
Not_found -> message se.se_loc (Eno_such_field (t1, f))
@ -539,9 +505,9 @@ let rec typing const_env h e =
let typed_c, ty = typing_static_exp const_env c in
Econst typed_c, ty
| Evar x ->
Evar x, typ_of_varname h x
Evar x, typ_of_name h x
| Elast x ->
Elast x, typ_of_last h x
Elast x, typ_of_name h x
| Eapp(op, e_list, r) ->
let ty, op, typed_e_list =
@ -561,7 +527,7 @@ let rec typing const_env h e =
check_field_unicity l;
let l =
List.map (typing_field
const_env h fields (Tid q) q.qual) l in
const_env h fields (Tid q)) l in
Estruct l, Tid q
| Epre (None, e) ->
@ -581,7 +547,7 @@ let rec typing const_env h e =
| Eiterator (it, ({ a_op = (Enode f | Efun f);
a_params = params } as app),
n, e_list, reset) ->
let { qualname = q; info = ty_desc } = find_value f in
let ty_desc = find_value f in
let op, expected_ty_list, result_ty_list = kind q ty_desc in
(*TODO verifier....*)
let node_params =
@ -608,11 +574,11 @@ let rec typing const_env h e =
with
TypingError(kind) -> message e.e_loc kind
and typing_field const_env h fields t1 modname (f, e) =
and typing_field const_env h fields t1 (f, e) =
try
let ty = check_type const_env (field_assoc f fields) in
let typed_e = expect const_env h ty e in
{ qual = modname; name = shortname f }, typed_e
f, typed_e
with
Not_found -> message e.e_loc (Eno_such_field (t1, f))
@ -643,8 +609,8 @@ and typing_app const_env h op e_list =
t1, op, [typed_e1; typed_e2; typed_e3]
| { a_op = (Efun f | Enode f); a_params = params } as app, e_list ->
let { qualname = q; info = ty_desc } = find_value f in
let op, expected_ty_list, result_ty_list = kind q ty_desc in
let ty_desc = find_value f in
let op, expected_ty_list, result_ty_list = kind op ty_desc in
(*TODO verifier....*)
let node_params =
List.map (fun { p_name = n } -> local_qn n) ty_desc.node_params in
@ -682,9 +648,7 @@ and typing_app const_env h op e_list =
let typed_e, t1 = typing const_env h e in
let q, fields = struct_info t1 in
let t2 = field_type const_env fn fields t1 e.e_loc in
let fn = { qual = q.qual; name = shortname fn } in
let f = { f with se_desc = Sconstructor fn } in
t2, { op with a_params = [f] }, [typed_e]
t2, op, [typed_e]
| { a_op = Efield_update; a_params = [f] }, [e1; e2] ->
let typed_e1, t1 = typing const_env h e1 in
@ -693,11 +657,9 @@ and typing_app const_env h op e_list =
(match f.se_desc with
| Sconstructor fn -> fn
| _ -> assert false) in
let f = { f with se_desc =
Sconstructor { qual = q.qual; name = shortname fn } } in
let t2 = field_type const_env fn fields t1 e1.e_loc in
let typed_e2 = expect const_env h t2 e2 in
t1, { op with a_params = [f] } , [typed_e1; typed_e2]
t1, op, [typed_e1; typed_e2]
| { a_op = Earray_fill; a_params = [n] }, [e1] ->
let typed_n = expect_static_exp const_env (Tid Initial.pint) n in
@ -718,7 +680,7 @@ and typing_app const_env h op e_list =
typing_array_subscript_dyn const_env h idx_list t1 in
ty, op, typed_e1::typed_defe::typed_idx_list
| { a_op = Eupdate}, e1::e2::idx_list ->
| { a_op = Eupdate }, e1::e2::idx_list ->
let typed_e1, t1 = typing const_env h e1 in
let ty, typed_idx_list =
typing_array_subscript_dyn const_env h idx_list t1 in
@ -945,12 +907,9 @@ and typing_switch_handlers const_env h acc ty switch_handlers =
let d = diff_const (set_of_constr (desc_of_ty ty)) cases in
if not (S.is_empty d) then error (Epartial_switch(S.choose d));
let handler ({ w_block = b; w_name = name }) =
let handler ({ w_block = b } as sh) =
let typed_b, defined_names, _ = typing_block const_env h b in
{ w_block = typed_b;
(* Replace handler name with fully qualified name *)
w_name = (find_constr name).qualname},
defined_names in
{ sh with w_block = typed_b }, defined_names in
let typed_switch_handlers, defined_names_list =
List.split (List.map handler switch_handlers) in
@ -1035,16 +994,6 @@ let typing_contract const_env h contract =
c_assume = typed_e_a;
c_enforce = typed_e_g }, h
let signature statefull inputs returns params constraints =
let arg_dec_of_var_dec vd =
mk_arg (Some (name vd.v_ident)) (simplify_type vd.v_loc vd.v_type)
in
{ node_inputs = List.map arg_dec_of_var_dec inputs;
node_outputs = List.map arg_dec_of_var_dec returns;
node_statefull = statefull;
node_params = params;
node_params_constraints = constraints; }
let solve loc cl =
try
solve NamesEnv.empty cl
@ -1081,9 +1030,11 @@ let node ({ n_name = f; n_statefull = statefull;
included_env defined_names output_names;
included_env output_names defined_names;
(* update the node signature to add static params constraints *)
let cl = get_size_constraint () in
let cl = solve loc cl in
add_value f (signature statefull typed_i_list typed_o_list typed_params cl);
let s = find_value f in
replace_value f { s with node_params_constraints = cl };
{ n with
n_input = typed_i_list;
@ -1094,28 +1045,6 @@ let node ({ n_name = f; n_statefull = statefull;
with
| TypingError(error) -> message loc error
let deftype { t_name = n; t_desc = tdesc; t_loc = loc } =
try
match tdesc with
| Type_abs -> add_type n Tabstract
| Type_alias ln -> add_type n (Talias ln)
| Type_enum(tag_name_list) ->
add_type n (Tenum tag_name_list);
List.iter (fun tag -> add_constr tag (Tid (qualname n))) tag_name_list
| Type_struct(field_ty_list) ->
let field_ty_list =
List.map (fun f ->
mk_field f.f_name
(simplify_type loc
(check_type QualEnv.empty f.f_type)))
field_ty_list in
add_type n (Tstruct field_ty_list);
add_struct n field_ty_list;
List.iter
(fun f -> add_field f.f_name n) field_ty_list
with
TypingError(error) -> message loc error
let typing_const_dec cd =
let ty = check_type QualEnv.empty cd.c_type in
let se = expect_static_exp QualEnv.empty ty cd.c_value in
@ -1127,6 +1056,5 @@ let program
({ p_opened = opened; p_types = p_type_list;
p_nodes = p_node_list; p_consts = p_consts_list } as p) =
let typed_cd_list = List.map typing_const_dec p_consts_list in
List.iter deftype p_type_list;
let typed_node_list = List.map node p_node_list in
{ p with p_nodes = typed_node_list; p_consts = typed_cd_list }
let typed_node_list = List.map node p_node_list in
{ p with p_nodes = typed_node_list; p_consts = typed_cd_list }