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

Ported Typing and Interface

Browse source
This commit is contained in:
Cédric Pasteur 2010-06-17 13:05:16 +02:00 committed by Léonard Gérard
parent fe1588af5c
commit dfe5901c6c
5 changed files with 465 additions and 550 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
global/modules.ml
View file

@ -26,7 +26,7 @@ type env =
mutable types: type_def NamesEnv.t;
mutable constr: ty NamesEnv.t;
mutable structs : structure NamesEnv.t;
mutable fields: name NamesEnv.t;
mutable fields : name NamesEnv.t;
format_version : string;
}
@ -132,11 +132,15 @@ let add_constr f ty_res =
let add_struct f fields =
if NamesEnv.mem f current.structs then raise Already_defined;
current.structs <- NamesEnv.add f fields current.structs
let add_field f n =
if NamesEnv.mem f current.fields then raise Already_defined;
current.fields <- NamesEnv.add f n current.fields
let find_value = find (fun ident m -> NamesEnv.find ident m.values)
let find_type = find (fun ident m -> NamesEnv.find ident m.types)
let find_constr = find (fun ident m -> NamesEnv.find ident m.constr)
let find_struct = find (fun ident m -> NamesEnv.find ident m.structs)
let find_field = find (fun ident m -> NamesEnv.find ident m.fields)
let replace_value f signature =
current.values <- NamesEnv.remove f current.values;

10
global/signature.ml
View file

@ -43,3 +43,13 @@ let mk_arg name ty =
let mk_param name =
{ p_name = name }
let mk_field n ty =
{ f_name = n; f_type = ty }
let rec field_assoc f = function
| [] -> raise Not_found
| { f_name = n; f_type = ty }::l ->
if shortname f = n then
ty
else
field_assoc f l

135
heptagon/analysis/interface.ml
View file

@ -8,59 +8,33 @@
(**************************************************************************)
(* Read an interface *)
(* $Id$ *)
open Misc
open Ident
open Names
open Linearity
open Heptagon
open Global
open Signature
open Modules
open Typing
let rec split3 = function
| [] -> [], [], []
| (a,b,c)::l ->
let a_list, b_list, c_list = split3 l in
a::a_list, b::b_list, c::c_list
let rec combine3 l1 l2 l3 = match l1, l2, l3 with
| [], [], [] -> []
| a::a_list, b::b_list, c::c_list ->
(a,b,c)::(combine3 a_list b_list c_list)
module Type =
struct
let sigtype { sig_name = name; sig_inputs = i_list; sig_outputs = o_list;
sig_node = node; sig_safe = safe; sig_params = params } =
let arg_dec_of_tuple (n, ty, l) =
{ a_name = n;
a_type = Tbase(check_type ty);
a_linearity = l;
a_pass_by_ref = false } in
let i_inputs, t_inputs, l_inputs = split3 i_list in
let o_outputs, t_outputs, l_outputs = split3 o_list in
name, { inputs = List.map arg_dec_of_tuple i_list;
outputs = List.map arg_dec_of_tuple o_list;
contract = None;
node = node;
safe = safe;
targeting = [];
params = params;
params_constraints = []; }
let sigtype { sig_name = name; sig_inputs = i_list;
sig_outputs = o_list; sig_params = params } =
name, { node_inputs = i_list;
node_outputs = o_list;
node_params = params;
node_params_constraints = []; }
let read { interf_desc = desc; interf_loc = loc } =
try
match desc with
| Iopen(n) -> open_module n
| Itypedef(tydesc) -> deftype NamesEnv.empty tydesc
| Isignature(s) ->
let name, s = sigtype s in
add_value name s
match desc with
| Iopen(n) -> open_module n
| Itypedef(tydesc) -> deftype NamesEnv.empty tydesc
| Isignature(s) ->
let name, s = sigtype s in
add_value name s
with
TypingError(error) -> message loc error
TypingError(error) -> message loc error
let main l =
List.iter read l
end
@ -74,56 +48,53 @@ struct
match tdesc with
| Tabstract -> fprintf ff "@[type %s@.@]" name
| Tenum(tag_name_list) ->
fprintf ff "@[<hov 2>type %s = " name;
print_list ff print_name " |" tag_name_list;
fprintf ff "@.@]"
fprintf ff "@[<hov 2>type %s = " name;
print_list ff print_name " |" tag_name_list;
fprintf ff "@.@]"
| Tstruct(f_ty_list) ->
fprintf ff "@[<hov 2>type %s = " name;
fprintf ff "@[<hov 1>{";
print_list ff
(fun ff (field, ty) -> print_name ff field;
fprintf ff ": ";
print_type ff ty) ";" f_ty_list;
fprintf ff "}@]@.@]"
fprintf ff "@[<hov 2>type %s = " name;
fprintf ff "@[<hov 1>{";
print_list ff
(fun ff (field, ty) -> print_name ff field;
fprintf ff ": ";
print_type ff ty) ";" f_ty_list;
fprintf ff "}@]@.@]"
let signature ff name { inputs = inputs;
outputs = outputs;
contract = contract; node = node;
safe = safe; params = params; params_constraints = constr } =
let signature ff name { node_inputs = inputs;
node_outputs = outputs;
node_params = params;
node_params_constraints = constr } =
let print ff arg =
match arg.a_name with
| None -> print_type ff arg.a_type
| Some(name) ->
print_name ff name; fprintf ff ":"; print_type ff arg.a_type;
fprintf ff " "; print_lin ff arg.a_linearity in
| None -> print_type ff arg.a_type
| Some(name) ->
print_name ff name; fprintf ff ":"; print_type ff arg.a_type
in
let print_node_params ff = function
| [] -> ()
| l ->
fprintf ff "<<";
print_list ff print_name "," l;
fprintf ff ">>" in
fprintf ff "<<";
print_list ff print_name "," l;
fprintf ff ">>" in
fprintf ff "@[<v 2>val ";
if safe then fprintf ff "safe ";
if node then fprintf ff "node " else fprintf ff "fun ";
print_name ff name;
print_node_params ff params;
fprintf ff "(@[";
print_list ff print ";" inputs;
fprintf ff "@]) returns (@[";
print_list ff print ";" outputs;
fprintf ff "@])";
(match constr with
| [] -> ()
| constr ->
fprintf ff "\n with: @[";
print_list ff Static.print_size_constr "," constr;
fprintf ff "@]"
);
optunit (print_contract ff) contract;
fprintf ff "@.@]"
fprintf ff "@[<v 2>val ";
print_name ff name;
print_node_params ff params;
fprintf ff "(@[";
print_list ff print ";" inputs;
fprintf ff "@]) returns (@[";
print_list ff print ";" outputs;
fprintf ff "@])";
(match constr with
| [] -> ()
| constr ->
fprintf ff "\n with: @[";
print_list ff Static.print_size_constr "," constr;
fprintf ff "@]"
);
fprintf ff "@.@]"
let print oc =
let ff = formatter_of_out_channel oc in
NamesEnv.iter (fun key typdesc -> deftype ff key typdesc) current.types;

557
heptagon/analysis/typing.ml
View file

@ -15,10 +15,11 @@ open Names
open Ident
open Location
open Heptagon
open Global
open Signature
open Modules
open Initial
open Static
open Types
type value = { ty: ty; mutable last: bool }
@ -35,13 +36,16 @@ type error =
| Enon_exaustive
| Estate_clash
| Epartial_switch of name
| Etwo_many_outputs
| Etoo_many_outputs
| Esome_fields_are_missing
| Esubscripted_value_not_an_array of ty
| Earray_subscript_should_be_const
| Eundefined_const of name
| Econstraint_solve_failed of size_constr
| Etype_should_be_static of ty
| Erecord_type_expected of ty
| Eno_such_field of ty * longname
| Eempty_record
exception Unify
exception TypingError of error
@ -102,7 +106,7 @@ let message loc kind =
"%aThe case %s is missing.\n"
output_location loc
s
| Etwo_many_outputs ->
| Etoo_many_outputs ->
Printf.eprintf
"%aA function may only returns a basic value.\n"
output_location loc
@ -134,6 +138,21 @@ let message loc kind =
"%aThis type should be static : %a.\n"
output_location loc
Printer.ptype ty
| Erecord_type_expected ty ->
Printf.eprintf
"%aA record was expected (found %a).\n"
output_location loc
Printer.ptype ty
| Eno_such_field (ty, f) ->
Printf.eprintf
"%aThe record type '%a' does not have a '%s' field.\n"
output_location loc
Printer.ptype ty
(shortname f)
| Eempty_record ->
Printf.eprintf
"%aThe record is empty.\n"
output_location loc
end;
raise Error
@ -143,9 +162,10 @@ let add_type f type_def =
try add_type f type_def with Already_defined -> error (Ealready_defined f)
let add_constr f ty_res =
try add_constr f ty_res with Already_defined -> error (Ealready_defined f)
let add_field f ty_arg ty_res =
try add_field f ty_arg ty_res
with Already_defined -> error (Ealready_defined f)
let add_struct f fields =
try add_struct f fields with Already_defined -> error (Ealready_defined f)
let add_field f n =
try add_field f n with Already_defined -> error (Ealready_defined f)
let find_value f =
try find_value f with Not_found -> error (Eundefined(fullname f))
@ -155,6 +175,8 @@ let find_constr c =
try find_constr c with Not_found -> error (Eundefined(fullname c))
let find_field c =
try find_field c with Not_found -> error (Eundefined(fullname c))
let find_struct c =
try find_struct c with Not_found -> error (Eundefined(fullname c))
let (curr_size_constr : size_constr list ref) = ref []
let add_size_constr c =
@ -175,33 +197,26 @@ let get_number_of_fields ty =
let element_type ty =
match ty with
| Tbase (Tarray (ty, _)) -> Tbase ty
| Tarray (ty, _) -> ty
| _ -> error (Esubscripted_value_not_an_array ty)
let size_exp ty =
match ty with
| Tbase (Tarray (_, e)) -> e
| Tarray (_, e) -> e
| _ -> error (Esubscripted_value_not_an_array ty)
let rec unify t1 t2 =
match t1, t2 with
| Tprod(t1_list), Tprod(t2_list) ->
begin
try List.iter2 unify t1_list t2_list with _ -> raise Unify
end
| Tbase(b1), Tbase(b2) when b1 = b2 -> ()
| Tbase(Tbool), Tbase(Tid name_bool)
| Tbase(Tid name_bool), Tbase(Tbool)
when name_bool = pbool -> ()
| Tbase(Tint), Tbase(Tid name_int)
| Tbase(Tid name_int), Tbase(Tint)
when name_int = pint -> ()
| Tbase(Tfloat), Tbase(Tid name_float)
| Tbase(Tid name_float), Tbase(Tfloat)
when name_float = pfloat -> ()
| Tbase(Tarray (ty1, e1)), Tbase(Tarray (ty2, e2)) ->
add_size_constr (Equal(e1,e2));
unify (Tbase ty1) (Tbase ty2)
| Tprod t1_list, Tprod t2_list ->
(try
List.iter2 unify t1_list t2_list
with
_ -> raise Unify
)
| b1, b2 when b1 = b2 -> ()
| Tarray (ty1, e1), Tarray (ty2, e2) ->
add_size_constr (Equal(e1,e2));
unify ty1 ty2
| _ -> raise Unify
let unify t1 t2 =
@ -210,30 +225,26 @@ let unify t1 t2 =
let less_than statefull = if not statefull then error Estate_clash
let kind f statefull = function
| { inputs = ty_list1;
outputs = ty_list2;
node = n } ->
let ty_of_arg_dec v = v.a_type in
if n & not(statefull) then error (Eshould_be_a_node(f))
else n, List.map ty_of_arg_dec ty_list1, List.map ty_of_arg_dec ty_list2
| { node_inputs = ty_list1;
node_outputs = ty_list2 } ->
let ty_of_arg v = v.a_type in
(*if n & not(statefull) then error (Eshould_be_a_node(f)) *)
(*else n,*) List.map ty_of_arg ty_list1, List.map ty_of_arg ty_list2
let prod = function
| [] -> assert false
| [ty] -> ty
| ty_list -> Tprod(ty_list)
| ty_list -> Tprod ty_list
let rec typing_const c =
let typed_c, ty = match c with
| Cint _ -> c, Tid(pint)
| Cfloat _ -> c, Tid(pfloat)
| Cconstr(c) ->
let { qualid = q; info = ty } = find_constr c in
Cconstr(Modname(q)), ty
| Carray(n, c) ->
let c, ty = typing_const c in
Carray(n,c), Tarray(type ty, n)
in
typed_c, Tbase(ty)
let rec typing_const c = match c with
| Cint _ -> c, Tid(pint)
| Cfloat _ -> c, Tid(pfloat)
| Cconstr(c) ->
let { qualid = q; info = ty } = find_constr c in
Cconstr(Modname q), ty
| Carray(n, c) ->
let c, ty = typing_const c in
Carray(n,c), Tarray(ty, n)
let typ_of_name h x =
try
@ -260,13 +271,13 @@ let typ_of_last h x =
Not_found -> error (Eundefined(sourcename x))
let desc_of_ty = function
| Tbase(Tid(ty_name)) ->
| Tid ty_name ->
let { info = tydesc } = find_type ty_name in tydesc
| Tbase(Tbool) -> Tenum ["true";"false"]
| Tid n when n = pbool -> Tenum ["true";"false"]
| _ -> Tabstract
let set_of_constr = function
| Tabstract | Tstruct _ -> assert false
| Tenum(tag_list) -> List.fold_right S.add tag_list S.empty
| Tenum tag_list -> List.fold_right S.add tag_list S.empty
let name_mem n env =
let check_one id _ acc =
@ -274,40 +285,40 @@ let name_mem n env =
in
Env.fold check_one env false
(* [check_type t] checks that t exists *)
(** [check_type t] checks that t exists *)
let rec check_type = function
| Tint | Tfloat | Tbool as t -> t
| Tarray(ty, e) ->
Tarray(check_type ty, e)
| Tid(ty_name) ->
try Tid(Modname((find_type ty_name).qualid))
with Not_found -> error (Eundefined(fullname ty_name))
(try Tid(Modname((find_type ty_name).qualid))
with Not_found -> error (Eundefined(fullname ty_name)))
| Tprod l ->
Tprod (List.map check_type l)
let rec simplify_type const_env = function
| Tint | Tfloat | Tbool | Tid _ as t -> t
| Tid _ as t -> t
| Tarray(ty, e) ->
Tarray(simplify_type const_env ty, simplify const_env e)
| Tprod l ->
Tprod (List.map (simplify_type const_env) l)
let simplify_type loc const_env ty =
try
simplify_type const_env ty
with
Instanciation_failed -> message loc (Etype_should_be_static (Tbase ty))
Instanciation_failed -> message loc (Etype_should_be_static ty)
let rec subst_type_vars m = function
| Tarray(ty, e) -> Tarray(subst_type_vars m ty, size_exp_subst m e)
| t -> t
let rec subst_type_vars m = function
| Tbase ty -> Tbase (subst_type_vars m ty)
| Tprod l -> Tprod (List.map (subst_type_vars m) l)
| t -> t
let equal expected_tag_list actual_tag_list =
if not (List.for_all
(fun tag -> List.mem tag actual_tag_list) expected_tag_list)
then error Enon_exaustive
(* add two sets of names provided they are distinct *)
(** Add two sets of names provided they are distinct *)
let add env1 env2 =
Env.fold
(fun elt ty env ->
@ -315,7 +326,7 @@ let add env1 env2 =
then Env.add elt ty env
else error (Ealready_defined(sourcename elt))) env1 env2
(* checks that constructors are included in constructor list from type
(** Checks that constructors are included in constructor list from type
def and returns the difference *)
let included_const s1 s2 =
S.iter
@ -326,8 +337,8 @@ let diff_const defined_names local_names =
included_const local_names defined_names;
S.diff defined_names local_names
(* checks that local_names are included in defined_names and returns *)
(* the difference *)
(** Checks that local_names are included in defined_names and returns
the difference *)
let included_env s1 s2 =
Env.iter
(fun elt _ -> if not (Env.mem elt s2) then error (Emissing(sourcename elt)))
@ -337,8 +348,8 @@ let diff_env defined_names local_names =
included_env local_names defined_names;
Env.diff defined_names local_names
(* [merge [set1;...;setn]] returns a set of names defined in every seti *)
(* and only partially defined names *)
(** [merge [set1;...;setn]] returns a set of names defined in every seti
and only partially defined names *)
let rec merge local_names_list =
let two s1 s2 =
let total, partial = Env.partition (fun elt -> Env.mem elt s2) s1 in
@ -356,7 +367,7 @@ let rec merge local_names_list =
let total, partial2 = two s total in
total, Env.union partial1 partial2
(* checks that every partial name has a last value *)
(** Checks that every partial name has a last value *)
let all_last h env =
Env.iter
(fun elt _ ->
@ -365,6 +376,56 @@ let all_last h env =
let last = function | Var -> false | Last _ -> true
(** Checks that a field is not defined twice in a list
of field name, exp.*)
let check_field_unicity l =
let add_field acc (f,e) =
if S.mem (shortname f) acc then
message e.e_loc (Ealready_defined (fullname f))
else
S.add (shortname f) acc
in
List.fold_left add_field S.empty l
(** @return the qualified name and list of fields of
the type with name [n].
Prints an error message if the type is not a record type.
[loc] is the location used for error reporting.*)
let struct_info_from_name loc n =
try
let { qualid = q;
info = fields } = find_struct n in
q, fields
with
Not_found -> message loc (Erecord_type_expected (Tid n))
(** @return the qualified name and list of fields of a record type.
Prints an error message if the type is not a record type.
[loc] is the location used for error reporting.*)
let struct_info loc ty = match ty with
| Tid n -> struct_info_from_name loc n
| _ -> message loc (Erecord_type_expected ty)
(** @return the qualified name and list of fields of the
record type corresponding to the field named [n].
Prints an error message if the type is not a record type.
[loc] is the location used for error reporting.*)
let struct_info_from_field loc f =
try
let { qualid = q; info = n } = find_field f in
struct_info_from_name loc (Modname { qual = q.qual; id = n })
with
Not_found -> message loc (Eundefined (fullname f))
(** @return the type of the field with name [f] in the list
[fields]. [t1] is the corresponding record type and [loc] is
the location, both used for error reporting. *)
let field_type f fields t1 loc =
try
check_type (field_assoc f fields)
with
Not_found -> message loc (Eno_such_field (t1, f))
let rec typing statefull h e =
try
let typed_desc,ty = match e.e_desc with
@ -372,7 +433,7 @@ let rec typing statefull h e =
let typed_c, ty = typing_const c in
Econst(c),
ty
| Econstvar(x) -> Econstvar x, Tbase Tint
| Econstvar(x) -> Econstvar x, Tid Initial.pint
| Evar(x) ->
Evar(x),
typ_of_varname h x
@ -388,52 +449,47 @@ let rec typing statefull h e =
let ty, op, typed_e_list = typing_app statefull h op e_list in
Eapp({ app with a_op = op }, typed_e_list),
ty
| Efield(e, field) ->
let { qualid = q;
info = { arg = ty_arg; res = ty_res } } = find_field field in
let typed_e = expect statefull h (Tbase(ty_arg)) e in
Efield(typed_e, Modname(q)),
Tbase(ty_res)
| Efield(e, f) ->
let typed_e, t1 = typing statefull h e in
let q, fields = struct_info e.e_loc t1 in
let t2 = field_type f fields t1 e.e_loc in
Efield(typed_e, Modname { qual = q.qual; id = shortname f }), t2
| Estruct(l) ->
let { qualid = q;
info = { arg = ty_arg } } = find_field (fst (List.hd l)) in
let size = get_number_of_fields ty_arg in
let rec fieldrec acc_l acc = function
| [] ->
List.rev acc_l,
Tbase(ty_arg)
| (field, e) :: l ->
if S.mem (shortname field) acc
then error (Ealready_defined(fullname field));
let { qualid = q;
info = { arg = ty; res = ty_res } } = find_field field in
let typed_e = expect statefull h (Tbase(ty_res)) e in
unify (Tbase(ty)) (Tbase(ty_arg));
fieldrec
((Modname(q),typed_e)::acc_l)
(S.add (shortname field) acc)
l in
let typed_l, ty = fieldrec [] S.empty l in
(* check that no field is missing *)
if List.length l <> size then error Esome_fields_are_missing;
Estruct(typed_l),
ty
(* find the record type using the first field *)
let q, fields =
(match l with
| [] -> message e.e_loc (Eempty_record)
| (f,_)::l -> struct_info_from_field e.e_loc f
) in
if List.length l <> List.length fields then
message e.e_loc Esome_fields_are_missing;
check_field_unicity l;
let l = List.map (typing_field statefull h fields (Tid (Modname q))) l in
Estruct l, Tid (Modname q)
| Earray (exp::e_list) ->
let typed_exp, t1 = typing statefull h exp in
let typed_e_list = List.map (expect statefull h t1) e_list in
Earray(typed_exp::typed_e_list),
const_array_of t1 (List.length e_list + 1)
let typed_exp, t1 = typing statefull h exp in
let typed_e_list = List.map (expect statefull h t1) e_list in
Earray(typed_exp::typed_e_list),
const_array_of t1 (List.length e_list + 1)
(* Arity problems *)
| Earray [] ->
error (Earity_clash (0, 1))
| Ereset_mem _ -> assert false
error (Earity_clash (0, 1))
in
{ e with
e_desc = typed_desc;
e_ty = ty; },
ty
{ e with e_desc = typed_desc; e_ty = ty; }, ty
with
TypingError(kind) -> message e.e_loc kind
and typing_field statefull h fields t1 (f, e) =
try
let ty = check_type (field_assoc f fields) in
let typed_e = expect statefull h ty e in
f, typed_e
with
Not_found -> message e.e_loc (Eno_such_field (t1, f))
and expect statefull h expected_ty e =
let typed_e, actual_ty = typing statefull h e in
try
@ -458,30 +514,52 @@ and typing_app statefull h op e_list =
let typed_e2 = expect statefull h t1 e2 in
t1, op, [typed_e1;typed_e2]
| Eifthenelse, [e1;e2;e3] ->
let typed_e1 = expect statefull h (Tbase tbool) e1 in
let typed_e1 = expect statefull h (Tid Initial.pbool) e1 in
let typed_e2, t1 = typing statefull h e2 in
let typed_e3 = expect statefull h t1 e3 in
t1, op, [typed_e1; typed_e2; typed_e3]
| (Enode(f, params) | Eevery(f, params) | Eop(f, params)), e_list ->
let { qualid = q; info = ty_desc } = find_value f in
let k, expected_ty_list, result_ty_list = kind f statefull ty_desc in
let m = List.combine ty_desc.params params in
let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in
let typed_e_list = typing_args statefull h expected_ty_list e_list in
let size_constrs = instanciate_constr m ty_desc.params_constraints in
let result_ty_list = List.map (subst_type_vars m) result_ty_list in
List.iter add_size_constr size_constrs;
let f = Modname(q) in
(prod result_ty_list,
(if k then Enode(f, params) else Eop(f, params)),
typed_e_list)
t1, op, [typed_e1; typed_e2; typed_e3]
| Ecall ( { op_name = f; op_params = params } as op_desc , reset), e_list ->
let { qualid = q; info = ty_desc } = find_value f in
let expected_ty_list, result_ty_list = kind f statefull ty_desc in
let m = List.combine (List.map (fun p -> p.p_name) ty_desc.node_params)
params in
let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in
let typed_e_list = typing_args statefull h expected_ty_list e_list in
let size_constrs = instanciate_constr m ty_desc.node_params_constraints in
let result_ty_list = List.map (subst_type_vars m) result_ty_list in
List.iter add_size_constr size_constrs;
(prod result_ty_list,
Ecall ( { op_desc with op_name = Modname(q) }, reset),
typed_e_list)
| Earray_op op, e_list ->
let ty, op, e_list = typing_array_op statefull h op e_list in
ty, Earray_op op, e_list
| Efield_update f, [e1; e2] ->
let typed_e1, t1 = typing statefull h e1 in
let q, fields = struct_info e1.e_loc t1 in
let t2 = field_type f fields t1 e1.e_loc in
let typed_e2 = expect statefull h t2 e2 in
t1, op, [typed_e1; typed_e2]
(*Arity problems*)
| Epre _, _ ->
error (Earity_clash(List.length e_list, 1))
| (Efby | Earrow), _ ->
error (Earity_clash(List.length e_list, 2))
| Eifthenelse, _ ->
error (Earity_clash(List.length e_list, 2))
| Efield_update field, _ ->
error (Earity_clash(List.length e_list, 2))
(*Array operators*)
and typing_array_op statefull h op e_list =
match op, e_list with
| Erepeat, [e1; e2] ->
let typed_e2 = expect statefull h (Tbase(Tint)) e2 in
let typed_e2 = expect statefull h (Tid Initial.pint) e2 in
let e2 = size_exp_of_exp e2 in
let typed_e1, t1 = typing statefull h e1 in
add_size_constr (LEqual (SConst 1, e2));
array_of t1 e2, op, [typed_e1; typed_e2]
Tarray (t1, e2), op, [typed_e1; typed_e2]
| Eselect idx_list, [e1] ->
let typed_e1, t1 = typing statefull h e1 in
typing_array_subscript statefull h idx_list t1, op, [typed_e1]
@ -496,14 +574,14 @@ and typing_app statefull h op e_list =
let typed_e2 = expect statefull h ty e2 in
t1, op, [typed_e1; typed_e2]
| Eselect_slice, [e; idx1; idx2] ->
let typed_idx1 = expect statefull h (Tbase(Tint)) idx1 in
let typed_idx2 = expect statefull h (Tbase(Tint)) idx2 in
let typed_idx1 = expect statefull h (Tid Initial.pint) idx1 in
let typed_idx2 = expect statefull h (Tid Initial.pint) idx2 in
let typed_e, t1 = typing statefull h e in
(*Create the expression to compute the size of the array *)
let e1 = SOp (SMinus, size_exp_of_exp idx2, size_exp_of_exp idx1) in
let e2 = SOp (SPlus, e1, SConst 1) in
add_size_constr (LEqual (SConst 1, e2));
array_of (element_type t1) e2, op, [typed_e; typed_idx1; typed_idx2]
Tarray (element_type t1, e2), op, [typed_e; typed_idx1; typed_idx2]
| Econcat, [e1; e2] ->
let typed_e1, t1 = typing statefull h e1 in
let typed_e2, t2 = typing statefull h e2 in
@ -513,52 +591,27 @@ and typing_app statefull h op e_list =
TypingError(kind) -> message e1.e_loc kind
end;
let n = SOp (SPlus, size_exp t1, size_exp t2) in
array_of (element_type t1) n, op, [typed_e1; typed_e2]
| Eiterator (it, f, params, reset), e::e_list ->
let { qualid = q; info = ty_desc } = find_value f in
let f = Modname(q) in
let _, expected_ty_list, result_ty_list = kind f statefull ty_desc in
let m = List.combine ty_desc.params params in
let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in
let size_constrs = instanciate_constr m ty_desc.params_constraints in
let result_ty_list = List.map (subst_type_vars m) result_ty_list in
let typed_e = expect statefull h (Tbase Tint) e in
let e = size_exp_of_exp e in
let ty, typed_e_list = typing_iterator statefull h it e
expected_ty_list result_ty_list e_list in
add_size_constr (LEqual (SConst 1, e));
List.iter add_size_constr size_constrs;
ty, Eiterator(it, f, params, reset), typed_e::typed_e_list
| Ecopy, [e] ->
let typed_e, ty = typing statefull h e in
ty, op, [typed_e]
| Efield_update field, [e1; e2] ->
let { qualid = q;
info = { arg = ty_arg; res = ty_res } } = find_field field in
let typed_e1 = expect statefull h (Tbase(ty_arg)) e1 in
let typed_e2 = expect statefull h (Tbase(ty_res)) e2 in
Tbase(ty_arg), op, [typed_e1; typed_e2]
| Eflatten n, [e] ->
let { qualid = q;
info = { fields = fields } } = find_struct n in
let typed_e = expect statefull h (Tbase(Tid (Modname q))) e in
prod (List.map (fun (_, ty) -> Tbase (check_type ty)) fields), op, [typed_e]
| Emake n, e_list ->
let { qualid = q;
info = { fields = fields } } = find_struct n in
if List.length e_list <> List.length fields then
error (Earity_clash(List.length e_list, List.length fields));
let typed_e_list = List.map2
(fun e (_,ty) -> expect statefull h (Tbase (check_type ty)) e)
e_list fields in
Tbase (Tid (Modname q)), op, typed_e_list
(*Arity problems*)
| Epre _, _ ->
error (Earity_clash(List.length e_list, 1))
| (Efby | Earrow), _ ->
error (Earity_clash(List.length e_list, 2))
| Eifthenelse, _ ->
error (Earity_clash(List.length e_list, 2))
Tarray (element_type t1, n), op, [typed_e1; typed_e2]
| Eiterator (it, ({ op_name = f; op_params = params } as op_desc), reset),
e::e_list ->
let { qualid = q; info = ty_desc } = find_value f in
let f = Modname(q) in
let expected_ty_list, result_ty_list = kind f statefull ty_desc in
let m = List.combine (List.map (fun p -> p.p_name) ty_desc.node_params)
params in
let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in
let size_constrs = instanciate_constr m ty_desc.node_params_constraints in
let result_ty_list = List.map (subst_type_vars m) result_ty_list in
let typed_e = expect statefull h (Tid Initial.pint) e in
let e = size_exp_of_exp e in
let ty, typed_e_list = typing_iterator statefull h it e
expected_ty_list result_ty_list e_list in
add_size_constr (LEqual (SConst 1, e));
List.iter add_size_constr size_constrs;
ty, Eiterator(it, { op_desc with op_name = f }, reset),
typed_e::typed_e_list
(*Arity problems*)
| Eiterator _, _ ->
error (Earity_clash(List.length e_list, 1))
| Econcat, _ ->
@ -573,49 +626,45 @@ and typing_app statefull h op e_list =
error (Earity_clash(List.length e_list, 2))
| Erepeat _, _ ->
error (Earity_clash(List.length e_list, 2))
| Ecopy, _ ->
error (Earity_clash(List.length e_list, 1))
| Efield_update field, _ ->
error (Earity_clash(List.length e_list, 2))
and typing_iterator statefull h it n args_ty_list result_ty_list e_list =
match it with
| Imap ->
let args_ty_list = List.map (fun ty -> array_of ty n) args_ty_list in
let result_ty_list = List.map (fun ty -> array_of ty n) result_ty_list in
let typed_e_list = typing_args statefull h args_ty_list e_list in
prod result_ty_list, typed_e_list
let args_ty_list = List.map (fun ty -> Tarray(ty, n)) args_ty_list in
let result_ty_list = List.map (fun ty -> Tarray(ty, n)) result_ty_list in
let typed_e_list = typing_args statefull h args_ty_list e_list in
prod result_ty_list, typed_e_list
| Ifold ->
let args_ty_list = incomplete_map (fun ty -> array_of ty n) args_ty_list in
let typed_e_list = typing_args statefull h args_ty_list e_list in
(*check accumulator type matches in input and output*)
if List.length result_ty_list > 1 then
error (Etwo_many_outputs);
begin try
unify (last_element args_ty_list) (List.hd result_ty_list)
with
TypingError(kind) -> message (List.hd e_list).e_loc kind
end;
(List.hd result_ty_list), typed_e_list
let args_ty_list = incomplete_map (fun ty -> Tarray (ty, n)) args_ty_list in
let typed_e_list = typing_args statefull h args_ty_list e_list in
(*check accumulator type matches in input and output*)
if List.length result_ty_list > 1 then
error (Etoo_many_outputs);
begin try
unify (last_element args_ty_list) (List.hd result_ty_list)
with
TypingError(kind) -> message (List.hd e_list).e_loc kind
end;
(List.hd result_ty_list), typed_e_list
| Imapfold ->
let args_ty_list = incomplete_map (fun ty -> array_of ty n) args_ty_list in
let result_ty_list = incomplete_map (fun ty -> array_of ty n) result_ty_list in
let typed_e_list = typing_args statefull h args_ty_list e_list in
(*check accumulator type matches in input and output*)
begin try
unify (last_element args_ty_list) (last_element result_ty_list)
with
TypingError(kind) -> message (List.hd e_list).e_loc kind
end;
prod result_ty_list, typed_e_list
let args_ty_list = incomplete_map (fun ty -> Tarray (ty, n)) args_ty_list in
let result_ty_list = incomplete_map (fun ty -> Tarray (ty, n)) result_ty_list in
let typed_e_list = typing_args statefull h args_ty_list e_list in
(*check accumulator type matches in input and output*)
begin try
unify (last_element args_ty_list) (last_element result_ty_list)
with
TypingError(kind) -> message (List.hd e_list).e_loc kind
end;
prod result_ty_list, typed_e_list
and typing_array_subscript statefull h idx_list ty =
match ty, idx_list with
| ty, [] -> ty
| Tbase(Tarray(ty, exp)), idx::idx_list ->
add_size_constr (LEqual (SConst 0, idx));
add_size_constr (LEqual (idx, SOp(SMinus, exp, SConst 1)));
typing_array_subscript statefull h idx_list (Tbase ty)
| Tarray(ty, exp), idx::idx_list ->
add_size_constr (LEqual (SConst 0, idx));
add_size_constr (LEqual (idx, SOp(SMinus, exp, SConst 1)));
typing_array_subscript statefull h idx_list ty
| _, _ -> error (Esubscripted_value_not_an_array ty)
(* This function checks that the array dimensions matches
@ -623,11 +672,11 @@ and typing_array_subscript statefull h idx_list ty =
and typing_array_subscript_dyn statefull h idx_list ty =
match ty, idx_list with
| ty, [] -> ty, []
| Tbase(Tarray(ty, exp)), idx::idx_list ->
let typed_idx = expect statefull h (Tbase(Tint)) idx in
let ty, typed_idx_list =
typing_array_subscript_dyn statefull h idx_list (Tbase ty) in
ty, typed_idx::typed_idx_list
| Tarray(ty, exp), idx::idx_list ->
let typed_idx = expect statefull h (Tid Initial.pint) idx in
let ty, typed_idx_list =
typing_array_subscript_dyn statefull h idx_list ty in
ty, typed_idx::typed_idx_list
| _, _ -> error (Esubscripted_value_not_an_array ty)
and typing_args statefull h expected_ty_list e_list =
@ -672,7 +721,7 @@ let rec typing_eq statefull h acc eq =
Epresent(typed_ph,typed_b),
acc
| Ereset(eq_list, e) ->
let typed_e = expect statefull h (Tbase(tbool)) e in
let typed_e = expect statefull h (Tid Initial.pbool) e in
let typed_eq_list, acc = typing_eq_list statefull h acc eq_list in
Ereset(typed_eq_list,typed_e),
acc
@ -706,7 +755,7 @@ and typing_automaton_handlers statefull h acc state_handlers =
let escape statefull h ({ e_cond = e; e_next_state = n } as esc) =
if not (S.mem n states) then error (Eundefined(n));
let typed_e = expect statefull h (Tbase(tbool)) e in
let typed_e = expect statefull h (Tid Initial.pbool) e in
{ esc with e_cond = typed_e } in
let handler
@ -752,7 +801,7 @@ and typing_switch_handlers statefull h acc ty switch_handlers =
and typing_present_handlers statefull h acc def_names present_handlers =
let handler ({ p_cond = e; p_block = b }) =
let typed_e = expect false h (Tbase(tbool)) e in
let typed_e = expect false h (Tid Initial.pbool) e in
let typed_b, defined_names, _ = typing_block statefull h b in
{ p_cond = typed_e; p_block = typed_b },
defined_names
@ -793,8 +842,8 @@ and build h h0 dec =
then error (Ealready_defined(sourcename n))
else
({ v with v_type = ty }::acc_dec,
Env.add n (Tbase(ty)) acc_defined,
Env.add n { ty = Tbase(ty); last = last l } h)
Env.add n ty acc_defined,
Env.add n { ty = ty; last = last l } h)
with
| TypingError(kind) -> message loc kind)
([], Env.empty, h) dec
@ -803,7 +852,7 @@ let build_params h params =
let add_one h param =
if Env.mem param h then
error (Ealready_defined(name param));
Env.add param { ty = Tbase Tint; last = false } h
Env.add param { ty = Tid Initial.pint; last = false } h
in
List.fold_left add_one h params
@ -822,9 +871,9 @@ let typing_contract statefull h contract =
let typed_eq, defined_names = typing_eq_list statefull h' Env.empty eq in
(* assumption *)
let typed_e_a = expect statefull h' (Tbase(tbool)) e_a in
let typed_e_a = expect statefull h' (Tid Initial.pbool) e_a in
(* property *)
let typed_e_g = expect statefull h' (Tbase(tbool)) e_g in
let typed_e_g = expect statefull h' (Tid Initial.pbool) e_g in
included_env local_names defined_names;
included_env defined_names local_names;
@ -836,21 +885,14 @@ let typing_contract statefull h contract =
c_enforce = typed_e_g },
controllable_names, h
let signature const_env statefull params returns contract node_params constraints =
let signature const_env inputs returns params constraints =
let arg_dec_of_var_dec vd =
{ a_name = Some (sourcename vd.v_name);
a_type = Tbase(check_type vd.v_type);
a_linearity = vd.v_linearity;
a_pass_by_ref = false; }
mk_arg (Some (name vd.v_name)) (check_type vd.v_type)
in
{ inputs = List.map arg_dec_of_var_dec params;
outputs = List.map arg_dec_of_var_dec returns;
contract = contract;
node = statefull;
safe = false;
targeting = [];
params = node_params;
params_constraints = constraints; }
{ node_inputs = List.map arg_dec_of_var_dec inputs;
node_outputs = List.map arg_dec_of_var_dec returns;
node_params = List.map mk_param params;
node_params_constraints = constraints; }
let solve loc env cl =
try
@ -858,7 +900,7 @@ let solve loc env cl =
with
Solve_failed c -> message loc (Econstraint_solve_failed c)
let node const_env ({ n_name = f; n_statefull = statefull;
let node const_env ({ n_name = f;
n_input = i_list; n_output = o_list;
n_contract = contract;
n_local = l_list; n_equs = eq_list; n_loc = loc;
@ -868,36 +910,26 @@ let node const_env ({ n_name = f; n_statefull = statefull;
let typed_o_list, output_names, h = build h h o_list in
(* typing contract *)
let typed_contract, controllable_names, h = typing_contract statefull h contract in
let typed_contract, controllable_names, h = typing_contract false h contract in
let typed_l_list, local_names, h = build h h l_list in
let typed_eq_list, defined_names = typing_eq_list statefull h Env.empty eq_list in
if not (statefull) & (List.length o_list <> 1)
then error (Etwo_many_outputs);
let typed_eq_list, defined_names = typing_eq_list false h Env.empty eq_list in
(* if not (statefull) & (List.length o_list <> 1)
then error (Etoo_many_outputs);*)
let expected_names = add local_names output_names in
included_env expected_names defined_names;
included_env defined_names expected_names;
let cl = get_size_constr () in
let ff = Format.formatter_of_out_channel stdout in
Format.fprintf ff "Gathered constraints before solving for %s: %d\n " f (List.length cl);
print_list ff print_size_constr ", " cl;
Format.fprintf ff "\n";
let cl = solve loc const_env cl in
Format.fprintf ff "Constraints after solving for %s: %d\n " f (List.length cl);
print_list ff print_size_constr ", " cl;
Format.fprintf ff "\n";
Format.fprintf ff "@?" ;
add_value f (signature const_env statefull i_list o_list contract node_params cl);
let cl = solve loc const_env cl in
add_value f (signature const_env i_list o_list node_params cl);
{ n with
n_input = List.rev typed_i_list;
n_output = List.rev typed_o_list;
n_local = typed_l_list;
n_contract = typed_contract;
n_equs = typed_eq_list }
n_input = List.rev typed_i_list;
n_output = List.rev typed_o_list;
n_local = typed_l_list;
n_contract = typed_contract;
n_equs = typed_eq_list }
with
| TypingError(error) -> message loc error
@ -906,21 +938,24 @@ let deftype const_env { t_name = n; t_desc = tdesc; t_loc = loc } =
match tdesc with
| Type_abs -> add_type n Tabstract
| Type_enum(tag_name_list) ->
add_type n (Tenum(tag_name_list));
List.iter (fun tag -> add_constr tag (Tid(longname n))) tag_name_list
add_type n (Tenum tag_name_list);
List.iter (fun tag -> add_constr tag (Tid (longname n))) tag_name_list
| Type_struct(field_ty_list) ->
let field_ty_list =
List.map (fun (n,ty) -> n, simplify_type loc const_env ty) field_ty_list in
add_type n (Tstruct(field_ty_list));
add_struct n field_ty_list;
List.iter
(fun (field, ty) ->
add_field field (Tid(longname n)) (check_type ty)) field_ty_list
let field_ty_list =
List.map (fun f ->
mk_field f.f_name
(simplify_type loc const_env 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 build_const_env cd_list =
List.fold_left (fun env cd -> NamesEnv.add cd.c_name cd.c_value env) NamesEnv.empty cd_list
List.fold_left (fun env cd -> NamesEnv.add cd.c_name cd.c_value env)
NamesEnv.empty cd_list
let program
({ p_opened = opened; p_types = p_type_list;

307
heptagon/printer.ml
View file

@ -18,8 +18,9 @@ open Heptagon
open Modules
open Static
open Format
open Pp_tools
open Types
open Signature
let iterator_to_string i =
match i with
@ -27,73 +28,13 @@ let iterator_to_string i =
| Ifold -> "fold"
| Imapfold -> "mapfold"
let rec print_list ff print sep l =
match l with
| [] -> ()
| [x] -> print ff x
| x :: l ->
print ff x;
fprintf ff "%s@ " sep;
print_list ff print sep l
(* Infix chars are surrounded by parenthesis *)
let is_infix =
let module StrSet = Set.Make(String) in
let set_infix =
List.fold_right
StrSet.add
["or"; "quo"; "mod"; "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr"]
StrSet.empty in
fun s -> StrSet.mem s set_infix
let print_name ff s =
let c = String.get s 0 in
let s = if is_infix s then "(" ^ s ^ ")"
else match c with
| 'a' .. 'z' | 'A' .. 'Z' | '_' | '`' -> s
| '*' -> "( " ^ s ^ " )"
| _ -> if s = "()" then s else "(" ^ s ^ ")" in
fprintf ff "%s" s
let print_longname ff ln =
let ln = currentname ln in
match ln with
| Name(m) -> print_name ff m
| Modname({ qual = "Pervasives"; id = m }) ->
print_name ff m
| Modname({ qual = m1; id = m2 }) ->
fprintf ff "%s." m1; print_name ff m2
let print_ident ff id =
fprintf ff "%s" (name id)
let print_iterator ff it =
fprintf ff "%s" (iterator_to_string it)
let rec print_pat ff = function
| Evarpat(n) -> print_ident ff n
| Etuplepat(pat_list) ->
fprintf ff "@[(";
print_list ff print_pat "," pat_list;
fprintf ff ")@]"
let rec print_type ff = function
| Tint -> fprintf ff "int"
| Tbool -> fprintf ff "bool"
| Tfloat -> fprintf ff "float"
| Tid(id) -> print_longname ff id
| Tarray(ty, e) ->
print_type ff ty;
fprintf ff "^";
print_size_exp ff e;
and print_type ff = function
| Tbase(ty) -> print_type ff ty
| Tprod(ty_list) ->
fprintf ff "@[(";
print_list ff print_type " *" ty_list;
fprintf ff ")@]"
print_list_r print_pat "(" "," ")" ff pat_list
and print_c ff = function
| Cint i -> fprintf ff "%d" i
@ -117,7 +58,7 @@ and print_vd ff { v_name = n; v_type = ty; v_last = last } =
fprintf ff "@]"
and print_exps ff e_list =
fprintf ff "@[("; print_list ff print_exp "," e_list; fprintf ff ")@]"
print_list_r print_exp "(" "," ")" ff e_list
and print_exp ff e =
if !Misc.full_type_info then fprintf ff "(";
@ -127,41 +68,24 @@ and print_exp ff e =
| Elast x -> fprintf ff "last "; print_ident ff x
| Econst c -> print_c ff c
| Eapp({ a_op = op }, e_list) -> print_op ff op e_list
| Etuple(e_list) ->
fprintf ff "@[(";
print_list ff print_exp "," e_list;
fprintf ff ")@]"
| Etuple(e_list) -> print_exps ff e_list
| Efield(e, field) ->
print_exp ff e; fprintf ff ".";
print_longname ff field
| Estruct(f_e_list) ->
fprintf ff "@[<v 1>{";
print_list ff
print_list_r
(fun ff (field, e) -> print_longname ff field;fprintf ff " = ";
print_exp ff e)
";" f_e_list;
"{" ";" "}" ff f_e_list;
fprintf ff "}@]"
| Earray(e_list) ->
fprintf ff "@[[";
print_list ff print_exp "," e_list;
fprintf ff "]@]"
| Ereset_mem(y,v,res) ->
fprintf ff "@[reset_mem ";
print_ident ff y;
fprintf ff " = ";
print_exp ff v;
fprintf ff " every ";
print_ident ff res;
fprintf ff "@]"
| Earray e_list ->
print_list_r print_exp "[" "," "]" ff e_list
end;
if !Misc.full_type_info then fprintf ff " : %a)" print_type e.e_ty
and print_call_params ff = function
| [] -> ()
| l ->
fprintf ff "<<";
print_list ff print_size_exp "," l;
fprintf ff ">>"
| l -> print_list_r print_size_exp "<<" "," ">>" ff l
and print_op ff op e_list =
match op, e_list with
@ -174,105 +98,81 @@ and print_op ff op e_list =
fprintf ff "@ then@ "; print_exp ff e2;
fprintf ff "@ else@ "; print_exp ff e3;
fprintf ff "@]"
| Enode(f, params), e_list ->
| Ecall({ op_name = f; op_params = params }, reset), e_list ->
print_longname ff f;
print_call_params ff params;
fprintf ff "(@["; print_list ff print_exp "," e_list;
fprintf ff ")@]"
| Eevery(f,params), e_list ->
print_longname ff f;
print_call_params ff params;
fprintf ff "(@["; print_list ff print_exp "," e_list;
fprintf ff ")@]"
| Eop(f, params), e_list ->
print_longname ff f;
print_call_params ff params;
fprintf ff "(@["; print_list ff print_exp "," e_list;
fprintf ff ")@]"
print_call_params ff params;
print_exps ff e_list;
(match reset with
| None -> ()
| Some r -> fprintf ff " every %a" print_exp r
)
| Efield_update f, [e1;e2] ->
fprintf ff "(@[";
print_exp ff e1;
fprintf ff " with .";
print_longname ff f;
fprintf ff " = ";
print_exp ff e2;
fprintf ff ")@]"
| Earray_op op, e_list ->
print_array_op ff op e_list
and print_array_op ff op e_list =
match op, e_list with
| Erepeat, [e1; e2] ->
print_exp ff e1;
fprintf ff "^";
print_exp ff e2
print_exp ff e1;
fprintf ff "^";
print_exp ff e2
| Eselect idx_list, [e] ->
print_exp ff e;
fprintf ff "[";
print_list ff print_size_exp "][" idx_list;
fprintf ff "]"
print_exp ff e;
print_list_r print_size_exp "[" "][" "]" ff idx_list
| Eselect_dyn, e::defe::idx_list ->
fprintf ff "@[(";
print_exp ff e;
fprintf ff "[";
print_list ff print_exp "][" idx_list;
fprintf ff "] default ";
print_exp ff defe;
fprintf ff ")@]"
fprintf ff "@[(";
print_exp ff e;
print_list_r print_exp "[" "][" "] default " ff idx_list;
print_exp ff defe;
fprintf ff ")@]"
| Eupdate idx_list, [e1;e2] ->
fprintf ff "(@[";
print_exp ff e1;
fprintf ff " with [";
print_list ff print_size_exp "][" idx_list;
fprintf ff "] = ";
print_exp ff e2;
fprintf ff ")@]"
fprintf ff "(@[";
print_exp ff e1;
fprintf ff " with ";
print_list_r print_size_exp "[" "][" "]" ff idx_list;
fprintf ff " = ";
print_exp ff e2;
fprintf ff ")@]"
| Eselect_slice, [e; idx1; idx2] ->
print_exp ff e;
fprintf ff "[";
print_exp ff idx1;
fprintf ff "..";
print_exp ff idx2;
fprintf ff "]"
| Eiterator (it, op, params, reset), e::e_list ->
fprintf ff "(";
print_iterator ff it;
fprintf ff " ";
(match params with
| [] -> print_longname ff op
| l ->
fprintf ff "(";
print_longname ff op;
print_call_params ff params;
fprintf ff ")"
);
fprintf ff " <<";
print_exp ff e;
fprintf ff ">>) (@[";
print_list ff print_exp "," e_list;
fprintf ff ")@]";
(match reset with
| None -> ()
| Some r -> fprintf ff " every %a" print_exp r
)
print_exp ff e;
fprintf ff "[";
print_exp ff idx1;
fprintf ff "..";
print_exp ff idx2;
fprintf ff "]"
| Eiterator (it, { op_name = op; op_params = params } , reset), e::e_list ->
fprintf ff "(";
print_iterator ff it;
fprintf ff " ";
(match params with
| [] -> print_longname ff op
| l ->
fprintf ff "(";
print_longname ff op;
print_call_params ff params;
fprintf ff ")"
);
fprintf ff " <<";
print_exp ff e;
fprintf ff ">>) ";
print_exps ff e_list;
(match reset with
| None -> ()
| Some r -> fprintf ff " every %a" print_exp r
)
| Econcat, [e1;e2] ->
fprintf ff "@[";
print_exp ff e1;
fprintf ff " @@ ";
print_exp ff e2;
fprintf ff "@]"
| Ecopy, [e] ->
fprintf ff "@[copy (";
print_exp ff e;
fprintf ff ")@]"
| Efield_update f, [e1;e2] ->
fprintf ff "(@[";
print_exp ff e1;
fprintf ff " with .";
print_longname ff f;
fprintf ff " = ";
print_exp ff e2;
fprintf ff ")@]"
| Eflatten n, e_list ->
fprintf ff "@[(flatten ";
print_longname ff n;
fprintf ff ")(";
print_list ff print_exp "," e_list;
fprintf ff ")@]"
| Emake n, e_list ->
fprintf ff "@[(make ";
print_longname ff n;
fprintf ff ")(";
print_list ff print_exp "," e_list;
fprintf ff ")@]"
| _ -> assert false
fprintf ff "@[";
print_exp ff e1;
fprintf ff " @@ ";
print_exp ff e2;
fprintf ff "@]"
let rec print_eq ff eq =
match eq.eq_desc with
@ -285,19 +185,19 @@ let rec print_eq ff eq =
| Eautomaton(state_handler_list) ->
fprintf ff "@[<v>automaton@,";
fprintf ff "@[<v>";
print_list ff print_state_handler "" state_handler_list;
print_list print_state_handler ff state_handler_list;
fprintf ff "@]@,";
fprintf ff "end@]"
| Eswitch(e, switch_handler_list) ->
fprintf ff "@[<v>switch ";
print_exp ff e;
fprintf ff "@,@[<v>";
print_list ff print_switch_handler "" switch_handler_list;
print_list print_switch_handler ff switch_handler_list;
fprintf ff "@]@,";
fprintf ff "end@]"
| Epresent(present_handler_list, b) ->
fprintf ff "@[<v>present@,";
print_list ff print_present_handler "" present_handler_list;
print_list print_present_handler ff present_handler_list;
if b.b_equs <> [] then begin
fprintf ff " @[<v 2>default@,";
print_block ff b;
@ -326,13 +226,13 @@ and print_state_handler ff
if until <> [] then
begin
fprintf ff "@,@[<v 2>until ";
print_list ff print_escape "" until;
print_list print_escape ff until;
fprintf ff "@]"
end;
if unless <> [] then
begin
fprintf ff "@,@[<v 2>unless ";
print_list ff print_escape " " unless;
print_list_r print_escape "" " " "" ff unless;
fprintf ff "@]"
end;
fprintf ff "@]"
@ -361,7 +261,7 @@ and print_block ff { b_local = v_list; b_equs = eqs; b_defnames = defnames } =
if v_list <> [] then
begin
fprintf ff "@[<v 2>var ";
print_list ff print_vd ";" v_list;
print_list_r print_vd "" ";" "" ff v_list;
fprintf ff "@]@,"
end;
(* (\* DEBUG *\) *)
@ -378,17 +278,16 @@ let print_type_def ff { t_name = name; t_desc = tdesc } =
| Type_abs -> fprintf ff "@[type %s@\n@]" name
| Type_enum(tag_name_list) ->
fprintf ff "@[type %s = " name;
print_list ff print_name "| " tag_name_list;
print_list_r print_name "" "| " "" ff tag_name_list;
fprintf ff "@\n@]"
| Type_struct(f_ty_list) ->
fprintf ff "@[type %s = " name;
fprintf ff "@[<v 1>{";
print_list ff
(fun ff (field, ty) ->
print_list_r
(fun ff { f_name = field; f_type = ty } ->
print_name ff field;
fprintf ff ": ";
print_type ff ty) ";" f_ty_list;
fprintf ff "}@]@.@]"
print_type ff ty) "{" ";" "}" ff f_ty_list;
fprintf ff "@.@]"
let print_const_dec ff c =
fprintf ff "@[const ";
@ -407,7 +306,7 @@ let print_contract ff {c_local = l;
if l <> [] then begin
fprintf ff "@[<v 2>contract@\n";
fprintf ff "@[<hov 4>var ";
print_list ff print_vd ";" l;
print_list_r print_vd "" ";" "" ff l;
fprintf ff ";@]@\n"
end;
if eqs <> [] then begin
@ -418,32 +317,28 @@ let print_contract ff {c_local = l;
fprintf ff "assume %a@;enforce %a@;with (@[<hov>"
print_exp e_a
print_exp e_g;
print_list ff print_vd ";" cl;
print_list_r print_vd "" ";" "" ff cl;
fprintf ff "@])@]@\n"
let print_node_params ff = function
| [] -> ()
| l ->
fprintf ff "<<";
print_list ff print_name "," l;
fprintf ff ">>"
| l -> print_list_r print_name "<<" "," ">>" ff l
let print_node ff
{ n_name = n; n_statefull = statefull; n_input = ni;
{ n_name = n; n_input = ni;
n_local = nl; n_output = no; n_contract = contract; n_equs = ne;
n_params = params; } =
fprintf ff "@[<v 2>%s " (if statefull then "node" else "fun");
fprintf ff "@[<v 2>node ";
print_name ff n;
print_node_params ff params;
fprintf ff "(@[";
print_list ff print_vd ";" ni;
fprintf ff "@]) returns (@[";
print_list ff print_vd ";" no;
fprintf ff "@])@,";
print_list_r print_vd "(" ";" ")" ff ni;
fprintf ff " returns ";
print_list_r print_vd "(" ";" ")" ff no;
fprintf ff "@,";
optunit (print_contract ff) contract;
if nl <> [] then begin
fprintf ff "@[<hov 4>var ";
print_list ff print_vd ";" nl;
print_list_r print_vd "" ";" "" ff nl;
fprintf ff ";@]@,"
end;
fprintf ff "@[<v 2>let @,";
@ -457,7 +352,7 @@ let print_open_module ff name =
let ptype oc ty =
let ff = formatter_of_out_channel oc in
print_type ff ty; fprintf ff "@?"
print_type ff ty; fprintf ff "@?"
let print oc { p_opened = po; p_types = pt; p_nodes = pn; p_consts = pc } =
let ff = formatter_of_out_channel oc in