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

Heptcheck compiles !!

Browse source
This commit is contained in:
Cédric Pasteur 2010-07-08 14:56:49 +02:00
parent 68ecd0e781
commit b0a5a7f13e
19 changed files with 660 additions and 658 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
compiler/global/modules.ml
View file

@ -136,7 +136,7 @@ let add_struct f fields =
let add_field f n =
if NamesEnv.mem f current.fields then raise Already_defined;
current.fields <- NamesEnv.add f n current.fields
let add_const c n =
let add_const f n =
if NamesEnv.mem f current.consts then raise Already_defined;
current.consts <- NamesEnv.add f n current.consts

7
compiler/global/signature.ml
View file

@ -9,7 +9,6 @@
(* global data in the symbol tables *)
open Names
open Types
open Static
(** Warning: Whenever these types are modified,
interface_format_version should be incremented. *)
@ -21,6 +20,12 @@ type arg = { a_name : name option; a_type : ty }
(** Node static parameters *)
type param = { p_name : name; p_type : ty }
(** Constraints on size expressions. *)
type size_constraint =
| Cequal of static_exp * static_exp (* e1 = e2*)
| Clequal of static_exp * static_exp (* e1 <= e2 *)
| Cfalse
(** Node signature *)
type node =
{ node_inputs : arg list;

39
compiler/global/static.ml
View file

@ -17,13 +17,8 @@
open Names
open Format
open Types
(** Constraints on size expressions. *)
type size_constraint =
| Cequal of static_exp * static_exp (* e1 = e2*)
| Clequal of static_exp * static_exp (* e1 <= e2 *)
| Cfalse
open Signature
open Modules
(* unsatisfiable constraint *)
exception Instanciation_failed
@ -63,7 +58,7 @@ let rec simplify env se =
with
Not_found ->
(match ln with
| Name n -> (try simplify env (NamesEnv.find id env) with | _ -> se)
| Name n -> (try simplify env (NamesEnv.find n env) with | _ -> se)
| Modname _ -> se)
)
| Sop (op, [e1; e2]) ->
@ -134,21 +129,25 @@ let rec solve const_env =
(** Substitutes variables in the size exp with their value
in the map (mapping vars to size exps). *)
let rec static_exp_subst m se =
let desc = match se.e_desc with
match se.se_desc with
| Svar ln ->
(match ln with
| Name n -> (try List.assoc n m with | Not_found -> Svar n)
| Modname _ -> Svar ln)
| Sop (op, se_list) -> Sop (op, List.map (static_exp_subst m) se_list)
| Sarray_power (se, n) -> Sarray_power (static_exp_subst m se,
static_exp_subst m n)
| Sarray se_list -> Sarray (List.map (static_exp_subst m) se_list)
| Stuple se_list -> Stuple (List.map (static_exp_subst m) se_list)
| Name n -> (try List.assoc n m with | Not_found -> se)
| Modname _ -> se)
| Sop (op, se_list) ->
{ se with se_desc = Sop (op, List.map (static_exp_subst m) se_list) }
| Sarray_power (se, n) ->
{ se with se_desc = Sarray_power (static_exp_subst m se,
static_exp_subst m n) }
| Sarray se_list ->
{ se with se_desc = Sarray (List.map (static_exp_subst m) se_list) }
| Stuple se_list ->
{ se with se_desc = Stuple (List.map (static_exp_subst m) se_list) }
| Srecord f_se_list ->
Srecord (List.map (fun (f,se) -> f, static_exp_subst m se) f_se_list)
| s -> s
in
{ se with se_desc = desc }
{ se with se_desc =
Srecord (List.map
(fun (f,se) -> f, static_exp_subst m se) f_se_list) }
| _ -> se
(** Substitutes variables in the constraint list with their value
in the map (mapping vars to size exps). *)

40
compiler/heptagon/analysis/causality.ml
View file

@ -97,27 +97,24 @@ let build dec =
let rec typing e =
match e.e_desc with
| Econst(c) -> cempty
| Econstvar(x) -> cempty
| Evar(x) -> read x
| Elast(x) -> lastread x
| Etuple(e_list) ->
candlist (List.map typing e_list)
| Eapp({a_op = op}, e_list) -> apply op e_list
| Epre (_, e) -> pre (typing e)
| Efby (e1, e2) ->
let t1 = typing e1 in
let t2 = pre (typing e2) in
candlist [t1; t2]
| Eapp({ a_op = op }, e_list, _) -> apply op e_list
| Efield(e1, _) -> typing e1
| Estruct(l) ->
let l = List.map (fun (_, e) -> typing e) l in
candlist l
| Earray(e_list) ->
candlist (List.map typing e_list)
| Eiterator (_, _, _, e_list, _) ->
ctuplelist (List.map typing e_list)
(** Typing an application *)
and apply op e_list =
match op, e_list with
| Epre(_), [e] -> pre (typing e)
| Efby, [e1;e2] ->
let t1 = typing e1 in
let t2 = pre (typing e2) in
candlist [t1; t2]
| Earrow, [e1;e2] ->
let t1 = typing e1 in
let t2 = typing e2 in
@ -127,21 +124,12 @@ and apply op e_list =
let i2 = typing e2 in
let i3 = typing e3 in
cseq t1 (cor i2 i3)
| Ecall _, e_list ->
| (Efun _| Enode _ | Econcat | Eselect_slice
| Eselect_dyn | Eselect _ | Earray_fill), e_list ->
ctuplelist (List.map typing e_list)
| Efield_update _, [e1;e2] ->
let t1 = typing e1 in
let t2 = typing e2 in
cseq t2 t1
| Earray_op op, e_list ->
apply_array_op op e_list
and apply_array_op op e_list =
match op, e_list with
| (Eiterator (_, _, _) | Econcat | Eselect_slice
| Eselect_dyn | Eselect _ | Erepeat), e_list ->
ctuplelist (List.map typing e_list)
| Eupdate _, [e1;e2] ->
| (Earray | Etuple), e_list ->
candlist (List.map typing e_list)
| (Eupdate _ | Efield_update _), [e1;e2] ->
let t1 = typing e1 in
let t2 = typing e2 in
cseq t2 t1
@ -198,7 +186,7 @@ let typing_contract loc contract =
match contract with
| None -> cempty
| Some { c_local = l_list; c_eq = eq_list; c_assume = e_a;
c_enforce = e_g; c_controllables = c_list } ->
c_enforce = e_g } ->
let teq = typing_eqs eq_list in
let t_contract = cseq (typing e_a) (cseq teq (typing e_g)) in
Causal.check loc t_contract;

43
compiler/heptagon/analysis/initialization.ml
View file

@ -192,11 +192,20 @@ let less_exp e actual_ty expected_ty =
(** Main typing function *)
let rec typing h e =
match e.e_desc with
| Econst _ | Econstvar _ -> leaf izero
| Econst _ -> leaf izero
| Evar(x) | Elast(x) -> let { i_typ = i } = Env.find x h in leaf i
| Etuple(e_list) ->
| Epre(None, e) ->
initialized_exp h e;
skeleton ione e.e_ty
| Epre(Some _, e) ->
initialized_exp h e;
skeleton izero e.e_ty
| Efby (e1, e2) ->
initialized_exp h e2;
skeleton (itype (typing h e1)) e.e_ty
| Eapp({ a_op = Etuple }, e_list, _) ->
product (List.map (typing h) e_list)
| Eapp({a_op = op}, e_list) ->
| Eapp({ a_op = op }, e_list, _) ->
let i = apply h op e_list in
skeleton i e.e_ty
| Efield(e1, _) ->
@ -207,36 +216,27 @@ let rec typing h e =
List.fold_left
(fun acc (_, e) -> max acc (itype (typing h e))) izero l in
skeleton i e.e_ty
| Earray(e_list) ->
let i =
List.fold_left
(fun acc e -> max acc (itype (typing h e))) izero e_list in
skeleton i e.e_ty
| Eiterator (_, _, _, e_list, _) ->
List.iter (fun e -> initialized_exp h e) e_list;
skeleton izero e.e_ty
(** Typing an application *)
and apply h op e_list =
match op, e_list with
| Epre(None), [e] ->
initialized_exp h e;
ione
| Epre(Some _), [e] ->
initialized_exp h e;
izero
| Efby, [e1;e2] ->
initialized_exp h e2;
itype (typing h e1)
| Earrow, [e1;e2] ->
let ty1 = typing h e1 in
let _ = typing h e2 in
itype ty1
| Earray, e_list ->
List.fold_left
(fun acc e -> max acc (itype (typing h e))) izero e_list
| Eifthenelse, [e1; e2; e3] ->
let i1 = itype (typing h e1) in
let i2 = itype (typing h e2) in
let i3 = itype (typing h e3) in
max i1 (max i2 i3)
(* | Ecall ({ op_kind = Efun }, _), e_list ->
List.fold_left (fun acc e -> itype (typing h e)) izero e_list *)
| (Ecall _ | Earray_op _| Efield_update _) , e_list ->
(** TODO: init of safe/unsafe nodes *)
| _ , e_list ->
List.iter (fun e -> initialized_exp h e) e_list; izero
and expect h e expected_ty =
@ -337,8 +337,7 @@ let typing_contract h contract =
match contract with
| None -> h
| Some { c_local = l_list; c_eq = eq_list; c_assume = e_a;
c_enforce = e_g; c_controllables = c_list } ->
let h = sbuild h c_list in
c_enforce = e_g } ->
let h' = build h l_list in
typing_eqs h' eq_list;
(* assumption *)

8
compiler/heptagon/analysis/interface.ml
View file

@ -21,7 +21,7 @@ module Type =
struct
let sigtype { sig_name = name; sig_inputs = i_list; sig_statefull = statefull;
sig_outputs = o_list; sig_params = params } =
let const_env = build_node_params NamesEnv.empty node_params in
let const_env = build_node_params NamesEnv.empty params in
let check_arg a = { a with a_type = check_type const_env a.a_type } in
name, { node_inputs = List.map check_arg i_list;
node_outputs = List.map check_arg o_list;
@ -33,8 +33,8 @@ struct
try
match desc with
| Iopen(n) -> open_module n
| Itypedef(tydesc) -> deftype NamesEnv.empty NamesEnv.empty tydesc
| Iconstdef cd -> typing_const_dec cd
| Itypedef(tydesc) -> deftype tydesc
| Iconstdef cd -> ignore (typing_const_dec cd)
| Isignature(s) ->
let name, s = sigtype s in
add_value name s
@ -66,7 +66,7 @@ struct
print_type ff ty) "{" ";" "}" ff f_ty_list;
fprintf ff "@]@.@]"
let constdef ff c =
let constdef ff _ c =
fprintf ff "@[const ";
print_name ff c.c_name;
fprintf ff " : ";

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

@ -14,12 +14,12 @@ open Misc
open Names
open Ident
open Location
open Heptagon
open Signature
open Modules
open Initial
open Static
open Types
open Heptagon
type value = { ty: ty; mutable last: bool }
@ -46,6 +46,7 @@ type error =
| Erecord_type_expected of ty
| Eno_such_field of ty * longname
| Eempty_record
| Eempty_array
exception Unify
exception TypingError of error
@ -125,9 +126,9 @@ let message loc kind =
output_location loc
| Eundefined_const ln ->
Printf.eprintf
"%aThe const name '%a' is unbound.\n"
"%aThe const name '%s' is unbound.\n"
output_location loc
print_longname ln
(fullname ln)
| Econstraint_solve_failed c ->
Printf.eprintf
"%aThe following constraint cannot be satisified:\n %a.\n"
@ -153,6 +154,10 @@ let message loc kind =
Printf.eprintf
"%aThe record is empty.\n"
output_location loc
| Eempty_array ->
Printf.eprintf
"%aThe array is empty.\n"
output_location loc
end;
raise Error
@ -180,12 +185,12 @@ let find_field c =
let find_struct c =
try find_struct c with Not_found -> error (Eundefined(fullname c))
let (curr_size_constrs : size_constraint list ref) = ref []
let (curr_size_constr : size_constraint list ref) = ref []
let add_size_constraint c =
curr_size_constrs := c :: !curr_size_constrs
curr_size_constr := c::(!curr_size_constr)
let get_size_constraint () =
let l = !curr_size_constrs in
curr_size_constrs := [];
let l = !curr_size_constr in
curr_size_constr := [];
l
let get_number_of_fields ty =
@ -202,7 +207,7 @@ let element_type ty =
| Tarray (ty, _) -> ty
| _ -> error (Esubscripted_value_not_an_array ty)
let static_exp ty =
let array_size ty =
match ty with
| Tarray (_, e) -> e
| _ -> error (Esubscripted_value_not_an_array ty)
@ -228,14 +233,14 @@ let less_than statefull = if not statefull then error Estate_clash
let rec is_statefull_exp e =
match e.e_desc with
| Econst _ | Evar _-> false
| Elast _ -> true
| Etuple e_list -> List.exists is_statefull_exp e_list
| Eapp({ a_op = (Efby | Epre _ | Earrow) }, _) -> true
| Eapp({ a_op = Ecall ({ op_kind = Enode }, _)}, _) -> true
| Eapp(_, e_list) -> List.exists is_statefull_exp e_list
| Econst _ | Evar _ | Estruct _ -> false
| Elast _ | Efby _ | Epre _ -> true
| Eapp({ a_op = (Enode _ | Earrow) }, _, _) -> true
| Eapp(_, e_list, _) -> List.exists is_statefull_exp e_list
| Eiterator(_, { a_op = Enode _ }, _, _, _) -> true
| Eiterator(_, _, _, e_list, _) ->
List.exists is_statefull_exp e_list
| Efield(e, _) -> is_statefull_exp e
| Estruct _ | Earray _ -> false
let rec is_statefull_eq_desc = function
| Eautomaton(handlers) ->
@ -269,77 +274,20 @@ and is_statefull_state_handler sh =
and is_statefull_escape esc =
is_statefull_exp esc.e_cond
let kind f statefull k
let kind f statefull
{ node_inputs = ty_list1;
node_outputs = ty_list2;
node_statefull = n } =
let ty_of_arg v = v.a_type in
let k = if n then Enode else Efun in
let op = if n then Enode f else Efun f in
if n & not(statefull) then error (Eshould_be_a_node f)
else k, List.map ty_of_arg ty_list1, List.map ty_of_arg ty_list2
else op, 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
let typing_static_exp const_env se =
let desc, ty = match se.e_desc with
| Sint -> Sint, Initial.pint
| Sbool -> Sbool, Initial.pbool
| Sfloat -> Sfloat, Initial.pfloat
| Svar ln ->
(try (* this can be a global const*)
let { qualid = q; info = cd } = find_const ln in
Svar q, cd.c_type
with Not_found -> (* or a static parameter *)
(match ln with
| Name n ->
(try Svar ln, NamesEnv.find n const_env
with Not_found -> message se.se_loc (Eundefined_const ln))
| Modname _ -> message se.se_loc (Eundefined_const ln))
)
| Sconstructor c ->
let { qualid = q; info = ty } = find_constr c in
Sconstructor(Modname q), t
| Sop (op, se_list) ->
let { qualid = q; info = ty_desc } = find_value op in
let typed_se_list = List.map2 (typing_static_args const_env)
(types_of_arg_list ty_desc.inputs) se_list in
Sop (Modname q, typed_se_list), types_of_arg_list ty_desc.outputs
| Sarray_power (se, n) ->
let typed_n = expect_static_exp const_env
no_location (Tid Initial.pint) n in
let typed_se, ty = typing_static_exp const_env se in
Sarray_power (typed_se, typed_n), Tarray(ty, n)
| Sarray [] ->
message se.se_loc Eempty_array
| Sarray se::se_list ->
let typed_se, ty = typing_static_exp const_env se in
let typed_se_list = List.map (expect_static_exp const_env ty) se_list in
typed_se::typed_se_list,
Tarray(ty, mk_static_exp (Sint ((List.length se_list) + 1)))
| Stuple se_list ->
let typed_se_list, ty_list = List.split
(List.map (typing_static_exp const_env) se_list) in
typed_se_list, prod ty_list
in
{ se with se_type = ty; se_desc = desc }, ty
and typing_static_args const_env expected_ty_list e_list =
try
List.map2 (expect_static_exp const_env) expected_ty_list e_list
with Invalid_argument _ ->
error (Earity_clash(List.length e_list, List.length expected_ty_list))
and expect_static_exp const_env loc exp_ty se =
try
let se, ty = typing_static_exp const_env se in
unify ty exp_ty;
se
with
Unify -> message loc (Etype_clash(ty, exp_ty))
let typ_of_name h x =
try
let { ty = ty } = Env.find x h in ty
@ -379,27 +327,16 @@ let name_mem n env =
in
Env.fold check_one env false
(** [check_type t] checks that t exists *)
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(Modname((find_type ty_name).qualid))
with Not_found -> error (Eundefined(fullname ty_name)))
| Tprod l ->
Tprod (List.map (check_type const_env) l)
let rec simplify_type const_value_env = function
let rec simplify_type = function
| Tid _ as t -> t
| Tarray(ty, e) ->
Tarray(simplify_type const_value_env ty, simplify const_value_env e)
Tarray(simplify_type ty, simplify NamesEnv.empty e)
| Tprod l ->
Tprod (List.map (simplify_type const_value_env) l)
Tprod (List.map simplify_type l)
let simplify_type loc const_value_env ty =
let simplify_type loc ty =
try
simplify_type const_value_env ty
simplify_type ty
with
Instanciation_failed -> message loc (Etype_should_be_static ty)
@ -483,6 +420,17 @@ let check_field_unicity l =
in
ignore (List.fold_left add_field S.empty l)
(** Checks that a field is not defined twice in a list
of field name, exp.*)
let check_static_field_unicity l =
let add_field acc (f,se) =
if S.mem (shortname f) acc then
message se.se_loc (Ealready_defined (fullname f))
else
S.add (shortname f) acc
in
ignore (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.
@ -513,6 +461,96 @@ let struct_info_from_field loc f =
with
Not_found -> message loc (Eundefined (fullname f))
(** [check_type t] checks that t exists *)
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(Modname((find_type ty_name).qualid))
with Not_found -> error (Eundefined(fullname ty_name)))
| Tprod l ->
Tprod (List.map (check_type const_env) l)
and typing_static_exp const_env se =
let desc, ty = match se.se_desc with
| Sint v -> Sint v, Tid Initial.pint
| Sbool v-> Sbool v, Tid Initial.pbool
| Sfloat v -> Sfloat v, Tid Initial.pfloat
| Svar ln ->
(try (* this can be a global const*)
let { qualid = q; info = cd } = find_const ln in
Svar (Modname q), cd.Signature.c_type
with Not_found -> (* or a static parameter *)
(match ln with
| Name n ->
(try Svar ln, NamesEnv.find n const_env
with Not_found -> message se.se_loc (Eundefined_const ln))
| Modname _ -> message se.se_loc (Eundefined_const ln))
)
| Sconstructor c ->
let { qualid = q; info = ty } = find_constr c in
Sconstructor(Modname q), ty
| Sop (op, se_list) ->
let { qualid = q; info = 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 (Modname q, 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
let typed_se, ty = typing_static_exp const_env se in
Sarray_power (typed_se, typed_n), Tarray(ty, n)
| Sarray [] ->
message se.se_loc Eempty_array
| Sarray (se::se_list) ->
let typed_se, ty = typing_static_exp const_env se in
let typed_se_list = List.map (expect_static_exp const_env ty) se_list in
Sarray (typed_se::typed_se_list),
Tarray(ty, mk_static_exp (Sint ((List.length se_list) + 1)))
| Stuple se_list ->
let typed_se_list, ty_list = List.split
(List.map (typing_static_exp const_env) se_list) in
Stuple typed_se_list, prod ty_list
| Srecord f_se_list ->
(* find the record type using the first field *)
let q, fields =
(match f_se_list with
| [] -> message se.se_loc (Eempty_record)
| (f,_)::l -> struct_info_from_field se.se_loc f
) in
if List.length f_se_list <> List.length fields then
message se.se_loc Esome_fields_are_missing;
check_static_field_unicity f_se_list;
let f_se_list =
List.map (typing_static_field const_env fields
(Tid (Modname q)) q.qual) f_se_list in
Srecord f_se_list, Tid (Modname q)
in
{ se with se_ty = ty; se_desc = desc }, ty
and typing_static_field const_env fields t1 modname (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
Modname { qual = modname; id = shortname f }, typed_se
with
Not_found -> message se.se_loc (Eno_such_field (t1, f))
and typing_static_args const_env expected_ty_list e_list =
try
List.map2 (expect_static_exp const_env) expected_ty_list e_list
with Invalid_argument _ ->
error (Earity_clash(List.length e_list, List.length expected_ty_list))
and expect_static_exp const_env exp_ty se =
let se, ty = typing_static_exp const_env se in
try
unify ty exp_ty; se
with
Unify -> message se.se_loc (Etype_clash(ty, exp_ty))
(** @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. *)
@ -522,32 +560,26 @@ let field_type const_env f fields t1 loc =
with
Not_found -> message loc (Eno_such_field (t1, f))
let rec typing statefull h e =
let rec typing statefull const_env h e =
try
let typed_desc,ty = match e.e_desc with
| Econst(c) ->
| Econst c ->
let typed_c, ty = typing_static_exp const_env c in
Econst typed_c,
ty
| Evar(x) ->
Evar(x),
typ_of_varname h x
| Elast(x) ->
Elast(x),
typ_of_last h x
| Etuple(e_list) ->
let typed_e_list,ty_list =
List.split (List.map (typing statefull h) e_list) in
Etuple(typed_e_list),
Tprod(ty_list)
| Eapp({ a_op = op } as app, e_list ) ->
let ty, op, typed_e_list = typing_app statefull h op e_list in
Eapp({ app with a_op = op }, typed_e_list),
ty
Econst typed_c, ty
| Evar x ->
Evar x, typ_of_varname h x
| Elast x ->
Elast x, typ_of_last h x
| Eapp(op, e_list, r) ->
let ty, op, typed_e_list =
typing_app statefull const_env h op e_list in
Eapp(op, typed_e_list, r), ty
| Efield(e, f) ->
let typed_e, t1 = typing statefull h e in
let typed_e, t1 = typing statefull const_env h e in
let q, fields = struct_info e.e_loc t1 in
let t2 = field_type f fields t1 e.e_loc in
let t2 = field_type const_env f fields t1 e.e_loc in
Efield(typed_e, Modname { qual = q.qual; id = shortname f }), t2
| Estruct(l) ->
@ -562,27 +594,61 @@ let rec typing statefull h e =
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
List.map (typing_field statefull
const_env h fields (Tid (Modname q)) q.qual) 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),
Tarray(t1, mk_static_exp (Sint (List.length e_list + 1)))
(* Arity problems *)
| Earray [] ->
error (Earity_clash (0, 1))
| Epre (None, e) ->
less_than statefull;
let typed_e,ty = typing statefull const_env h e in
Epre (None, typed_e), ty
| Epre (Some c, e) ->
less_than statefull;
let typed_c, t1 = typing_static_exp const_env c in
let typed_e = expect statefull const_env h t1 e in
Epre(Some typed_c, typed_e), t1
| Efby (e1, e2) ->
less_than statefull;
let typed_e1, t1 = typing statefull const_env h e1 in
let typed_e2 = expect statefull const_env h t1 e2 in
Efby (typed_e1, typed_e2), t1
| Eiterator (it, ({ a_op = (Enode f | Efun f);
a_params = params } as app),
n, e_list, reset) ->
let { qualid = q; info = ty_desc } = find_value f in
let op, 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 result_ty_list = List.map (subst_type_vars m) result_ty_list in
let typed_n = expect_static_exp const_env (Tid Initial.pint) n in
let ty, typed_e_list = typing_iterator statefull const_env h it n
expected_ty_list result_ty_list e_list in
let typed_params = typing_node_params const_env
ty_desc.node_params params in
(* add size constraints *)
let size_constrs =
instanciate_constr m ty_desc.node_params_constraints in
add_size_constraint (Clequal (mk_static_exp (Sint 1), typed_n));
List.iter add_size_constraint size_constrs;
(* return the type *)
Eiterator(it, { app with a_op = op; a_params = typed_params }
, typed_n, typed_e_list, reset), ty
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 const_env h fields t1 (f, e) =
and typing_field statefull const_env h fields t1 modname (f, e) =
try
let ty = check_type const_env (field_assoc f fields) in
let typed_e = expect statefull const_env h ty e in
f, typed_e
Modname { qual = modname; id = shortname f }, typed_e
with
Not_found -> message e.e_loc (Eno_such_field (t1, f))
@ -595,156 +661,152 @@ and expect statefull const_env h expected_ty e =
and typing_app statefull const_env h op e_list =
match op, e_list with
| Epre(None), [e] ->
| { a_op = Earrow }, [e1;e2] ->
less_than statefull;
let typed_e,ty = typing statefull h e in
ty,op,[typed_e]
| Epre(Some c), [e] ->
less_than statefull;
let typed_c, t1 = typing_static_exp const_env c in
let typed_e = expect statefull h t1 e in
t1, Epre(Some(typed_c)), [typed_e]
| (Efby | Earrow), [e1;e2] ->
less_than statefull;
let typed_e1, t1 = typing statefull h e1 in
let typed_e2 = expect statefull h t1 e2 in
let typed_e1, t1 = typing statefull const_env h e1 in
let typed_e2 = expect statefull const_env h t1 e2 in
t1, op, [typed_e1;typed_e2]
| Eifthenelse, [e1;e2;e3] ->
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
| { a_op = Eifthenelse }, [e1;e2;e3] ->
let typed_e1 = expect statefull const_env h
(Tid Initial.pbool) e1 in
let typed_e2, t1 = typing statefull const_env h e2 in
let typed_e3 = expect statefull const_env h t1 e3 in
t1, op, [typed_e1; typed_e2; typed_e3]
| Ecall ( { op_name = f; op_params = params; op_kind = k } as op_desc
, reset), e_list ->
| { a_op = (Efun f | Enode f); a_params = params } as app, e_list ->
let { qualid = q; info = ty_desc } = find_value f in
let k, expected_ty_list, result_ty_list = kind f statefull k ty_desc in
let op, expected_ty_list, result_ty_list =
kind (Modname q) 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 typed_e_list = typing_args statefull const_env h
expected_ty_list e_list in
let result_ty_list = List.map (subst_type_vars m) result_ty_list in
(* Type static parameters and generate constraints *)
let typed_params = typing_node_params const_env h ty_desc.node_params params in
let typed_params = typing_node_params const_env
ty_desc.node_params params in
let size_constrs =
instanciate_constr m ty_desc.node_params_constraints in
List.iter add_size_constraint size_constrs;
(prod result_ty_list,
Ecall ( { op_desc with op_name = Modname q; op_kind = k;
op_params = typed_params }, 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
prod result_ty_list,
{ app with a_op = op; a_params = typed_params },
typed_e_list
| { a_op = Etuple }, e_list ->
let typed_e_list,ty_list =
List.split (List.map (typing statefull const_env h) e_list) in
prod ty_list, op, typed_e_list
| { a_op = Earray }, exp::e_list ->
let typed_exp, t1 = typing statefull const_env h exp in
let typed_e_list = List.map (expect statefull const_env h t1) e_list in
let n = mk_static_exp ~ty:(Tid Initial.pint)
(Sint (List.length e_list + 1)) in
Tarray(t1, n), op, typed_exp::typed_e_list
| { a_op = Efield_update; a_params = [f] }, [e1; e2] ->
let typed_e1, t1 = typing statefull const_env 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]
let fn =
(match f.se_desc with
| Sconstructor fn -> fn
| _ -> assert false) in
let f = { f with se_desc =
Sconstructor (Modname { qual = q.qual; id = shortname fn }) } in
let t2 = field_type const_env fn fields t1 e1.e_loc in
let typed_e2 = expect statefull const_env h t2 e2 in
t1, { op with a_params = [f] } , [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))
| { a_op = Earray_fill; a_params = [n] }, [e1] ->
let typed_n = expect_static_exp const_env (Tid Initial.pint) n in
let typed_e1, t1 = typing statefull const_env h e1 in
add_size_constraint (Clequal (mk_static_exp (Sint 1), typed_n));
Tarray (t1, typed_n), { op with a_params = [typed_n] }, [typed_e1]
(*Array operators*)
and typing_array_op statefull h op e_list =
match op, e_list with
| Earray_fill, [e1; e2] ->
let typed_e2 = expect statefull h (Tid Initial.pint) e2 in
let e2 = static_exp_of_exp e2 in
let typed_e1, t1 = typing statefull h e1 in
add_size_constraint (Clequal (mk_static_exp (Sint 1), 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]
| Eselect_dyn, e1::defe::idx_list ->
let typed_e1, t1 = typing statefull h e1 in
let typed_defe = expect statefull h (element_type t1) defe in
| { a_op = Eselect; a_params = idx_list }, [e1] ->
let typed_e1, t1 = typing statefull const_env h e1 in
let typed_idx_list, ty =
typing_array_subscript statefull const_env h idx_list t1 in
ty, { op with a_params = typed_idx_list }, [typed_e1]
| { a_op = Eselect_dyn }, e1::defe::idx_list ->
let typed_e1, t1 = typing statefull const_env h e1 in
let typed_defe = expect statefull const_env h (element_type t1) defe in
let ty, typed_idx_list =
typing_array_subscript_dyn statefull h idx_list t1 in
typing_array_subscript_dyn statefull const_env h idx_list t1 in
ty, op, typed_e1::typed_defe::typed_idx_list
| Eupdate idx_list, [e1;e2] ->
let typed_e1, t1 = typing statefull h e1 in
let ty = typing_array_subscript statefull h idx_list t1 in
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 (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
| { a_op = Eupdate; a_params = idx_list }, [e1;e2] ->
let typed_e1, t1 = typing statefull const_env h e1 in
let typed_idx_list, ty =
typing_array_subscript statefull const_env h idx_list t1 in
let typed_e2 = expect statefull const_env h ty e2 in
t1, { op with a_params = typed_idx_list }, [typed_e1; typed_e2]
| { a_op = Eselect_slice; a_params = [idx1; idx2] }, [e] ->
let typed_idx1 = expect_static_exp const_env (Tid Initial.pint) idx1 in
let typed_idx2 = expect_static_exp const_env (Tid Initial.pint) idx2 in
let typed_e, t1 = typing statefull const_env h e in
(*Create the expression to compute the size of the array *)
let e1 = mk_static_exp (Sop (mk_pervasives "-",
[static_exp_of_exp idx2;
static_exp_of_exp idx1])) in
let e2 = mk_static_exp (Sop (mk_pervasives "+", e1,
mk_static_exp (Sint 1))) in
add_size_constr (Clequal (mk_static_exp (Sint 1), e2));
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
[typed_idx2; typed_idx1])) in
let e2 = mk_static_exp (Sop (mk_pervasives "+",
[e1;mk_static_exp (Sint 1) ])) in
add_size_constraint (Clequal (mk_static_exp (Sint 1), e2));
Tarray (element_type t1, e2),
{ op with a_params = [typed_idx1; typed_idx2] }, [typed_e]
| { a_op = Econcat }, [e1; e2] ->
let typed_e1, t1 = typing statefull const_env h e1 in
let typed_e2, t2 = typing statefull const_env h e2 in
begin try
unify (element_type t1) (element_type t2)
with
TypingError(kind) -> message e1.e_loc kind
end;
let n = Sop (SPlus, static_exp t1, static_exp t2) in
let n = mk_static_exp (Sop (mk_pervasives "+",
[array_size t1; array_size t2])) in
Tarray (element_type t1, n), op, [typed_e1; typed_e2]
| Eiterator (it, app, n, e_list, reset),
let { qualid = q; info = ty_desc } = find_value f in
let f = Modname(q) in
let k, expected_ty_list, result_ty_list = kind f statefull k 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 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 ty, typed_e_list = typing_iterator statefull h it n
expected_ty_list result_ty_list e_list in
(* add size constraints *)
let size_constrs =
instanciate_constr m ty_desc.node_params_constraints in
add_size_constraint (Clequal (mk_static_exp (Sint 1), e));
List.iter add_size_constraint size_constrs;
(* return the type *)
ty, Eiterator(it, { op_desc with op_name = f; op_kind = k }, reset),
typed_e::typed_e_list
(*Arity problems*)
| Eiterator _, _ ->
error (Earity_clash(List.length e_list, 1))
| Econcat, _ ->
| { a_op = Earrow }, _ ->
error (Earity_clash(List.length e_list, 2))
| Eselect_slice, _ ->
| { a_op = Eifthenelse }, _ ->
error (Earity_clash(List.length e_list, 2))
| { a_op = Efield_update }, _ ->
error (Earity_clash(List.length e_list, 2))
| { a_op = Earray }, [] ->
error (Earity_clash (0, 1))
| { a_op = Econcat }, _ ->
error (Earity_clash(List.length e_list, 2))
| { a_op = Eselect_slice }, _ ->
error (Earity_clash(List.length e_list, 3))
| Eupdate _, _ ->
| { a_op = Eupdate }, _ ->
error (Earity_clash(List.length e_list, 2))
| Eselect _, _ ->
| { a_op = Eselect }, _ ->
error (Earity_clash(List.length e_list, 1))
| Eselect_dyn, _ ->
| { a_op = Eselect_dyn }, _ ->
error (Earity_clash(List.length e_list, 2))
| Erepeat _, _ ->
| { a_op = Earray_fill }, _ ->
error (Earity_clash(List.length e_list, 2))
and typing_iterator statefull h it n args_ty_list result_ty_list e_list =
and typing_iterator statefull const_env h
it n args_ty_list result_ty_list e_list =
match it with
| Imap ->
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
let typed_e_list = typing_args statefull const_env h
args_ty_list e_list in
prod result_ty_list, typed_e_list
| Ifold ->
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
let typed_e_list = typing_args statefull const_env 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);
@ -754,12 +816,14 @@ and typing_iterator statefull h it n args_ty_list result_ty_list e_list =
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 -> 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
let typed_e_list = typing_args statefull const_env 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)
@ -770,36 +834,39 @@ and typing_iterator statefull h it n args_ty_list result_ty_list e_list =
and typing_array_subscript statefull const_env h idx_list ty =
match ty, idx_list with
| ty, [] -> ty
| ty, [] -> [], ty
| Tarray(ty, exp), idx::idx_list ->
ignore (expect_static_exp const_env (Tid Initial.pint) exp);
let typed_idx = expect_static_exp const_env (Tid Initial.pint) idx in
add_size_constraint (Clequal (mk_static_exp (Sint 0), idx));
let bound = mk_static_exp (Sop(mk_pervasives "-",
[exp; mk_static_exp (Sint 1))) in
[exp; mk_static_exp (Sint 1)])) in
add_size_constraint (Clequal (idx,bound));
typing_array_subscript statefull h idx_list ty
let typed_idx_list, ty =
typing_array_subscript statefull const_env h idx_list ty in
typed_idx::typed_idx_list, ty
| _, _ -> error (Esubscripted_value_not_an_array ty)
(* This function checks that the array dimensions matches
the subscript. It returns the base type wrt the nb of indices. *)
and typing_array_subscript_dyn statefull h idx_list ty =
and typing_array_subscript_dyn statefull const_env h idx_list ty =
match ty, idx_list with
| ty, [] -> ty, []
| Tarray(ty, exp), idx::idx_list ->
let typed_idx = expect statefull h (Tid Initial.pint) idx in
let typed_idx = expect statefull const_env h (Tid Initial.pint) idx in
let ty, typed_idx_list =
typing_array_subscript_dyn statefull h idx_list ty in
typing_array_subscript_dyn statefull const_env 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 =
and typing_args statefull const_env h expected_ty_list e_list =
try
List.map2 (expect statefull h) expected_ty_list e_list
List.map2 (expect statefull const_env h) expected_ty_list e_list
with Invalid_argument _ ->
error (Earity_clash(List.length e_list, List.length expected_ty_list))
and typing_node_params const_env h params_sig params =
List.map2 (fun p_sig p -> expect_static_exp const_env no_location
and typing_node_params const_env params_sig params =
List.map2 (fun p_sig p -> expect_static_exp const_env
p_sig.p_type p) params_sig params
let rec typing_pat h acc = function
@ -818,33 +885,35 @@ let rec typing_pat h acc = function
pat_list (acc, []) in
acc, Tprod(ty_list)
let rec typing_eq statefull h acc eq =
let rec typing_eq statefull const_env h acc eq =
let typed_desc,acc = match eq.eq_desc with
| Eautomaton(state_handlers) ->
let typed_sh,acc =
typing_automaton_handlers statefull h acc state_handlers in
typing_automaton_handlers statefull const_env h acc state_handlers in
Eautomaton(typed_sh),
acc
| Eswitch(e, switch_handlers) ->
let typed_e,ty = typing statefull h e in
let typed_e,ty = typing statefull const_env h e in
let typed_sh,acc =
typing_switch_handlers statefull h acc ty switch_handlers in
typing_switch_handlers statefull const_env h acc ty switch_handlers in
Eswitch(typed_e,typed_sh),
acc
| Epresent(present_handlers, b) ->
let typed_b, def_names, _ = typing_block statefull h b in
let typed_b, def_names, _ = typing_block statefull const_env h b in
let typed_ph, acc =
typing_present_handlers statefull h acc def_names present_handlers in
typing_present_handlers statefull const_env h
acc def_names present_handlers in
Epresent(typed_ph,typed_b),
acc
| Ereset(eq_list, e) ->
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
let typed_e = expect statefull const_env h (Tid Initial.pbool) e in
let typed_eq_list, acc = typing_eq_list statefull
const_env h acc eq_list in
Ereset(typed_eq_list,typed_e),
acc
| Eeq(pat, e) ->
let acc, ty_pat = typing_pat h acc pat in
let typed_e = expect statefull h ty_pat e in
let typed_e = expect statefull const_env h ty_pat e in
Eeq(pat, typed_e),
acc in
{ eq with
@ -852,11 +921,11 @@ let rec typing_eq statefull h acc eq =
eq_desc = typed_desc },
acc
and typing_eq_list statefull h acc eq_list =
and typing_eq_list statefull const_env h acc eq_list =
let rev_typed_eq_list,acc =
List.fold_left
(fun (rev_eq_list,acc) eq ->
let typed_eq, acc = typing_eq statefull h acc eq in
let typed_eq, acc = typing_eq statefull const_env h acc eq in
(typed_eq::rev_eq_list),acc
)
([],acc)
@ -864,7 +933,7 @@ and typing_eq_list statefull h acc eq_list =
((List.rev rev_typed_eq_list),
acc)
and typing_automaton_handlers statefull h acc state_handlers =
and typing_automaton_handlers statefull const_env h acc state_handlers =
(* checks unicity of states *)
let addname acc { s_state = n } =
if S.mem n acc then error (Ealready_defined(n)) else S.add n acc in
@ -872,12 +941,12 @@ 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 (Tid Initial.pbool) e in
let typed_e = expect statefull const_env h (Tid Initial.pbool) e in
{ esc with e_cond = typed_e } in
let handler ({ s_state = n; s_block = b; s_until = e_list1;
s_unless = e_list2 } as s) =
let typed_b, defined_names, h0 = typing_block statefull h b in
let typed_b, defined_names, h0 = typing_block statefull const_env h b in
let typed_e_list1 = List.map (escape statefull h0) e_list1 in
let typed_e_list2 = List.map (escape false h) e_list2 in
{ s with
@ -893,7 +962,7 @@ and typing_automaton_handlers statefull h acc state_handlers =
typed_handlers,
(add total (add partial acc))
and typing_switch_handlers statefull h acc ty switch_handlers =
and typing_switch_handlers statefull const_env h acc ty switch_handlers =
(* checks unicity of states *)
let addname acc { w_name = n } =
let n = shortname(n) in
@ -903,7 +972,7 @@ and typing_switch_handlers statefull h acc ty switch_handlers =
if not (S.is_empty d) then error (Epartial_switch(S.choose d));
let handler ({ w_block = b; w_name = name }) =
let typed_b, defined_names, _ = typing_block statefull h b in
let typed_b, defined_names, _ = typing_block statefull const_env h b in
{ w_block = typed_b;
(* Replace handler name with fully qualified name *)
w_name = Modname((find_constr name).qualid)},
@ -916,10 +985,11 @@ and typing_switch_handlers statefull h acc ty switch_handlers =
(typed_switch_handlers,
add total (add partial acc))
and typing_present_handlers statefull h acc def_names present_handlers =
and typing_present_handlers statefull const_env h acc def_names
present_handlers =
let handler ({ p_cond = e; p_block = b }) =
let typed_e = expect false h (Tid Initial.pbool) e in
let typed_b, defined_names, _ = typing_block statefull h b in
let typed_e = expect false const_env h (Tid Initial.pbool) e in
let typed_b, defined_names, _ = typing_block statefull const_env h b in
{ p_cond = typed_e; p_block = typed_b },
defined_names
in
@ -931,12 +1001,12 @@ and typing_present_handlers statefull h acc def_names present_handlers =
(typed_present_handlers,
(add total (add partial acc)))
and typing_block statefull h
and typing_block statefull const_env h
({ b_local = l; b_equs = eq_list; b_loc = loc } as b) =
try
let typed_l, local_names, h0 = build h Env.empty l in
let typed_l, local_names, h0 = build const_env h Env.empty l in
let typed_eq_list, defined_names =
typing_eq_list statefull h0 Env.empty eq_list in
typing_eq_list statefull const_env h0 Env.empty eq_list in
let defnames = diff_env defined_names local_names in
{ b with
b_statefull = List.exists (fun eq -> eq.eq_statefull) typed_eq_list;
@ -965,39 +1035,35 @@ and build const_env h h0 dec =
| TypingError(kind) -> message loc kind)
([], Env.empty, h) dec
let typing_contract statefull h contract =
let typing_contract statefull const_env h contract =
match contract with
| None -> None,Env.empty,h
| None -> None,h
| Some ({ c_local = l_list;
c_eq = eq;
c_assume = e_a;
c_enforce = e_g;
c_controllables = c_list }) ->
let typed_c_list, controllable_names, h = build h h c_list in
let typed_l_list, local_names, h' = build h h l_list in
c_enforce = e_g }) ->
let typed_l_list, local_names, h' = build const_env h h l_list in
let typed_eq, defined_names =
typing_eq_list statefull h' Env.empty eq in
typing_eq_list statefull const_env h' Env.empty eq in
(* assumption *)
let typed_e_a = expect statefull h' (Tid Initial.pbool) e_a in
let typed_e_a = expect statefull const_env h' (Tid Initial.pbool) e_a in
(* property *)
let typed_e_g = expect statefull h' (Tid Initial.pbool) e_g in
let typed_e_g = expect statefull const_env h' (Tid Initial.pbool) e_g in
included_env local_names defined_names;
included_env defined_names local_names;
Some { c_local = typed_l_list;
c_controllables = List.rev typed_c_list;
c_eq = typed_eq;
c_assume = typed_e_a;
c_enforce = typed_e_g },
controllable_names, h
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 NamesEnv.empty vd.v_type)
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;
@ -1005,9 +1071,9 @@ let signature statefull inputs returns params constraints =
node_params = params;
node_params_constraints = constraints; }
let solve loc env cl =
let solve loc cl =
try
solve env cl
solve NamesEnv.empty cl
with
Solve_failed c -> message loc (Econstraint_solve_failed c)
@ -1027,8 +1093,8 @@ let node ({ n_name = f; n_statefull = statefull;
let typed_o_list, output_names, h = build const_env h h o_list in
(* typing contract *)
let typed_contract, controllable_names, h =
typing_contract statefull h contract in
let typed_contract, h =
typing_contract statefull const_env h contract in
let typed_l_list, local_names, h = build const_env h h l_list in
let typed_eq_list, defined_names =
@ -1063,8 +1129,8 @@ let deftype { t_name = n; t_desc = tdesc; t_loc = loc } =
let field_ty_list =
List.map (fun f ->
mk_field f.f_name
(simplify_type loc NamesEnv.empty
(check_type const_env f.f_type))
(simplify_type loc
(check_type NamesEnv.empty f.f_type)))
field_ty_list in
add_type n (Tstruct field_ty_list);
add_struct n field_ty_list;
@ -1074,15 +1140,16 @@ let deftype { t_name = n; t_desc = tdesc; t_loc = loc } =
TypingError(error) -> message loc error
let typing_const_dec cd =
let ty = expect_static_exp NamesEnv.empty cd.c_loc cd.c_type cd.c_value in
let cd = { cd with c_type = ty } in
add_const cd.c_name (mk_const_def cd.c_name cd.c_type cd.c_value)
let se = expect_static_exp NamesEnv.empty cd.c_type cd.c_value in
let cd = { cd with c_value = se } in
add_const cd.c_name (mk_const_def cd.c_name cd.c_type cd.c_value);
cd
let program
({ p_opened = opened; p_types = p_type_list;
p_nodes = p_node_list; p_consts = p_consts_list } as p) =
List.iter typing_const_dec p_consts_list;
let typed_cd_list = List.map typing_const_dec p_consts_list in
List.iter open_module opened;
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 = cd_list }
{ p with p_nodes = typed_node_list; p_consts = typed_cd_list }

117
compiler/heptagon/hept_printer.ml
View file

@ -12,13 +12,13 @@ open Location
open Misc
open Names
open Ident
open Heptagon
open Modules
open Static
open Format
open Pp_tools
open Types
open Signature
open Heptagon
let iterator_to_string i =
match i with
@ -34,15 +34,6 @@ let rec print_pat ff = function
| Etuplepat(pat_list) ->
print_list_r print_pat "(" "," ")" ff pat_list
and print_c ff = function
| Cint i -> fprintf ff "%d" i
| Cfloat f -> fprintf ff "%f" f
| Cconstr(tag) -> print_longname ff tag
| Carray (n, c) ->
print_c ff c;
fprintf ff "^";
print_static_exp ff n
and print_vd ff { v_ident = n; v_type = ty; v_last = last } =
fprintf ff "@[<v>";
begin match last with Last _ -> fprintf ff "last " | _ -> () end;
@ -50,7 +41,7 @@ and print_vd ff { v_ident = n; v_type = ty; v_last = last } =
fprintf ff ": ";
print_type ff ty;
begin
match last with Last(Some(v)) -> fprintf ff "= ";print_c ff v
match last with Last(Some(v)) -> fprintf ff "= ";print_static_exp ff v
| _ -> ()
end;
fprintf ff "@]"
@ -62,11 +53,17 @@ and print_exp ff e =
if !Misc.full_type_info then fprintf ff "(";
begin match e.e_desc with
| Evar x -> print_ident ff x
| Econstvar x -> print_name ff x
| 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) -> print_exps ff e_list
| Econst c -> print_static_exp ff c
| Epre(None, e) -> fprintf ff "pre "; print_exp ff e
| Epre(Some c, e) -> print_static_exp ff c; fprintf ff " fby "; print_exp ff e
| Efby(e1, e2) -> print_exp ff e1; fprintf ff " fby "; print_exp ff e2
| Eapp({ a_op = op; a_params = params }, e_list, r) ->
print_op ff op params e_list;
(match r with
| None -> ()
| Some r -> fprintf ff " every %a" print_exp r
)
| Efield(e, field) ->
print_exp ff e; fprintf ff ".";
print_longname ff field
@ -76,8 +73,27 @@ and print_exp ff e =
print_exp ff e)
"{" ";" "}" ff f_e_list;
fprintf ff "}@]"
| Earray e_list ->
print_list_r print_exp "[" "," "]" ff e_list
| Eiterator (it, { a_op = (Efun ln|Enode ln); a_params = params },
n, e_list, reset) ->
fprintf ff "(";
print_iterator ff it;
fprintf ff " ";
(match params with
| [] -> print_longname ff ln
| l ->
fprintf ff "(";
print_longname ff ln;
print_call_params ff params;
fprintf ff ")"
);
fprintf ff " <<";
print_static_exp ff n;
fprintf ff ">>) ";
print_exps ff e_list;
(match reset with
| None -> ()
| Some r -> fprintf ff " every %a" print_exp r
)
end;
if !Misc.full_type_info then fprintf ff " : %a)" print_type e.e_ty
@ -85,52 +101,43 @@ and print_call_params ff = function
| [] -> ()
| l -> print_list_r print_static_exp "<<" "," ">>" ff l
and print_op ff op e_list =
match op, e_list with
| Epre(None), [e] -> fprintf ff "pre "; print_exp ff e
| Epre(Some(c)), [e] -> print_c ff c; fprintf ff " fby "; print_exp ff e
| Efby, [e1;e2] -> print_exp ff e1; fprintf ff " fby "; print_exp ff e2
| Earrow, [e1;e2] -> print_exp ff e1; fprintf ff " -> "; print_exp ff e2
| Eifthenelse,[e1;e2;e3] ->
and print_op ff op params e_list =
match op, params, e_list with
| Earrow, _, [e1;e2] -> print_exp ff e1; fprintf ff " -> "; print_exp ff e2
| Eifthenelse, _, [e1;e2;e3] ->
fprintf ff "@["; fprintf ff "if "; print_exp ff e1;
fprintf ff "@ then@ "; print_exp ff e2;
fprintf ff "@ else@ "; print_exp ff e3;
fprintf ff "@]"
| Ecall({ op_name = f; op_params = params }, reset), e_list ->
| Etuple, _, e_list -> print_exps ff e_list
| Earray, _, e_list ->
print_list_r print_exp "[" "," "]" ff e_list
| (Efun f|Enode f), params, e_list ->
print_longname ff f;
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] ->
print_exps ff e_list
| Efield_update, [se], [e1;e2] ->
fprintf ff "(@[";
print_exp ff e1;
fprintf ff " with .";
print_longname ff f;
print_static_exp ff se;
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] ->
| Earray_fill, _, [e1; e2] ->
print_exp ff e1;
fprintf ff "^";
print_exp ff e2
| Eselect idx_list, [e] ->
| Eselect, idx_list, [e] ->
print_exp ff e;
print_list_r print_static_exp "[" "][" "]" ff idx_list
| Eselect_dyn, e::defe::idx_list ->
| Eselect_dyn, _, e::defe::idx_list ->
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] ->
| Eupdate, idx_list, [e1;e2] ->
fprintf ff "(@[";
print_exp ff e1;
fprintf ff " with ";
@ -138,34 +145,14 @@ and print_array_op ff op e_list =
fprintf ff " = ";
print_exp ff e2;
fprintf ff ")@]"
| Eselect_slice, [e; idx1; idx2] ->
| 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_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] ->
| Econcat, _, [e1;e2] ->
fprintf ff "@[";
print_exp ff e1;
fprintf ff " @@ ";
@ -299,8 +286,7 @@ let print_const_dec ff c =
let print_contract ff {c_local = l;
c_eq = eqs;
c_assume = e_a;
c_enforce = e_g;
c_controllables = cl } =
c_enforce = e_g } =
if l <> [] then begin
fprintf ff "@[<v 2>contract@\n";
fprintf ff "@[<hov 4>var ";
@ -315,7 +301,6 @@ 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_r print_vd "" ";" "" ff cl;
fprintf ff "@])@]@\n"
let print_node_params ff = function

7
compiler/heptagon/heptagon.ml
View file

@ -35,7 +35,6 @@ and desc =
| Eapp of app * exp list * exp option
| Eiterator of iterator_type * app * static_exp * exp list * exp option
and app = { a_op: op; a_params: static_exp list; a_unsafe: bool }
and op =
@ -44,7 +43,7 @@ and op =
| Enode of fun_name
| Eifthenelse
| Earrow
| Efield_update of field_name (* field name args would be [record ; value] *)
| Efield_update (* field name args would be [record ; value] *)
| Earray
| Earray_fill
| Eselect
@ -193,10 +192,10 @@ let op_from_app app =
| _ -> raise Not_static
(** Translates a Heptagon exp into a static size exp. *)
let rec static_exp_of_exp e =
(*let rec static_exp_of_exp e =
match e.e_desc with
| Econst se -> se
| _ -> raise Not_static
| _ -> raise Not_static *)
(** @return the set of variables defined in [pat]. *)
let vars_pat pat =

2
compiler/heptagon/main/hept_compiler.ml
View file

@ -86,7 +86,7 @@ let compile_interface modname filename =
let l = parse_interface lexbuf in
(* Convert the parse tree to Heptagon AST *)
let l = Scoping.translate_interface l in
let l = Hept_scoping.translate_interface l in
(* Compile*)
Interface.Type.main l;

68
compiler/heptagon/parsing/hept_parser.mly
View file

@ -3,6 +3,7 @@
open Signature
open Location
open Names
open Types
open Hept_parsetree
let mk_static_exp = mk_static_exp ~loc:(current_loc())
@ -77,10 +78,10 @@ let mk_static_exp = mk_static_exp ~loc:(current_loc())
%left DOT
%start program
%type <Parsetree.program> program
%type <Hept_parsetree.program> program
%start interface
%type <Parsetree.interface> interface
%type <Hept_parsetree.interface> interface
%%
@ -218,7 +219,7 @@ opt_equs:
;
opt_assume:
| /* empty */ { mk_exp (Econst (Sconstructor Initial.ptrue)) }
| /* empty */ { mk_exp (Econst (mk_static_exp (Sconstructor Initial.ptrue))) }
| ASSUME exp { $2 }
;
@ -389,81 +390,82 @@ simple_exp:
| LBRACE field_exp_list RBRACE
{ mk_exp (Estruct $2) }
| LBRACKET array_exp_list RBRACKET
{ mk_exp (Earray $2) }
{ mk_exp (mk_call Earray $2) }
| LPAREN tuple_exp RPAREN
{ mk_exp (Etuple $2) }
{ mk_exp (mk_call Etuple $2) }
| LPAREN exp RPAREN
{ $2 }
;
node_name:
| longname call_params
{ mk_op_desc $1 $2 Enode }
{ mk_app (Enode $1) $2 }
exp:
| simple_exp { $1 }
| simple_exp FBY exp
{ mk_exp (Eapp(mk_app Efby, [$1; $3])) }
{ mk_exp (Efby ($1, $3)) }
| PRE exp
{ mk_exp (Eapp(mk_app (Epre None), [$2])) }
{ mk_exp (Epre (None, $2)) }
| node_name LPAREN exps RPAREN
{ mk_exp (mk_call $1 $3) }
{ mk_exp (Eapp($1, $3)) }
| NOT exp
{ mk_exp (mk_op_call "not" [] [$2]) }
{ mk_exp (mk_op_call "not" [$2]) }
| exp INFIX4 exp
{ mk_exp (mk_op_call $2 [] [$1; $3]) }
{ mk_exp (mk_op_call $2 [$1; $3]) }
| exp INFIX3 exp
{ mk_exp (mk_op_call $2 [] [$1; $3]) }
{ mk_exp (mk_op_call $2 [$1; $3]) }
| exp INFIX2 exp
{ mk_exp (mk_op_call $2 [] [$1; $3]) }
{ mk_exp (mk_op_call $2 [$1; $3]) }
| exp INFIX1 exp
{ mk_exp (mk_op_call $2 [] [$1; $3]) }
{ mk_exp (mk_op_call $2 [$1; $3]) }
| exp INFIX0 exp
{ mk_exp (mk_op_call $2 [] [$1; $3]) }
{ mk_exp (mk_op_call $2 [$1; $3]) }
| exp EQUAL exp
{ mk_exp (mk_op_call "=" [] [$1; $3]) }
{ mk_exp (mk_op_call "=" [$1; $3]) }
| exp OR exp
{ mk_exp (mk_op_call "or" [] [$1; $3]) }
{ mk_exp (mk_op_call "or" [$1; $3]) }
| exp STAR exp
{ mk_exp (mk_op_call "*" [] [$1; $3]) }
{ mk_exp (mk_op_call "*" [$1; $3]) }
| exp AMPERSAND exp
{ mk_exp (mk_op_call "&" [] [$1; $3]) }
{ mk_exp (mk_op_call "&" [$1; $3]) }
| exp SUBTRACTIVE exp
{ mk_exp (mk_op_call $2 [] [$1; $3]) }
{ mk_exp (mk_op_call $2 [$1; $3]) }
| PREFIX exp
{ mk_exp (mk_op_call $1 [] [$2]) }
{ mk_exp (mk_op_call $1 [$2]) }
| SUBTRACTIVE exp %prec prec_uminus
{ mk_exp (mk_op_call ("~"^$1) [] [$2]) }
{ mk_exp (mk_op_call ("~"^$1) [$2]) }
| IF exp THEN exp ELSE exp
{ mk_exp (Eapp(mk_app Eifthenelse, [$2; $4; $6])) }
{ mk_exp (mk_call Eifthenelse [$2; $4; $6]) }
| simple_exp ARROW exp
{ mk_exp (Eapp(mk_app Earrow, [$1; $3])) }
{ mk_exp (mk_call Earrow [$1; $3]) }
| LAST IDENT
{ mk_exp (Elast $2) }
| simple_exp DOT longname
{ mk_exp (Efield ($1, $3)) }
/*Array operations*/
| exp POWER simple_exp
{ mk_exp (mk_call Erepeat [$1; $3]) }
{ mk_exp (mk_call ~params:[$3] Earray_fill [$1]) }
| simple_exp indexes
{ mk_exp (mk_array_op_call (Eselect $2) [$1]) }
{ mk_exp (mk_call ~params:$2 Eselect [$1]) }
| simple_exp DOT indexes DEFAULT exp
{ mk_exp (mk_array_op_call Eselect_dyn ([$1; $5]@$3)) }
{ mk_exp (mk_call Eselect_dyn ([$1; $5]@$3)) }
| LBRACKET exp WITH indexes EQUAL exp RBRACKET
{ mk_exp (mk_array_op_call (Eupdate $4) [$2; $6]) }
{ mk_exp (mk_call ~params:$4 Eupdate [$2; $6]) }
| simple_exp LBRACKET exp DOUBLE_DOT exp RBRACKET
{ mk_exp (mk_array_op_call Eselect_slice [$1; $3; $5]) }
{ mk_exp (mk_call ~params:[$3; $5] Eselect_slice [$1]) }
| exp AROBASE exp
{ mk_exp (mk_array_op_call Econcat [$1; $3]) }
{ mk_exp (mk_call Econcat [$1; $3]) }
/*Iterators*/
| iterator longname DOUBLE_LESS simple_exp DOUBLE_GREATER LPAREN exps RPAREN
{ mk_exp (mk_iterator_call $1 $2 [] ($4::$7)) }
{ mk_exp (mk_iterator_call $1 $2 [] $4 $7) }
| iterator LPAREN longname DOUBLE_LESS array_exp_list DOUBLE_GREATER
RPAREN DOUBLE_LESS simple_exp DOUBLE_GREATER LPAREN exps RPAREN
{ mk_exp (mk_iterator_call $1 $3 $5 ($9::$12)) }
{ mk_exp (mk_iterator_call $1 $3 $5 $9 $12) }
/*Records operators */
| LBRACE e=simple_exp WITH DOT ln=longname EQUAL nv=exp RBRACE
{ mk_exp (Eapp (mk_app (Efield_update ln), [e; nv])) }
{ let fn = mk_exp (Econst (mk_static_exp (Sconstructor ln))) in
mk_exp (mk_call ~params:[fn] Efield_update [e; nv]) }
;
call_params:

18
compiler/heptagon/parsing/hept_parsetree.ml
View file

@ -11,6 +11,7 @@
open Names
open Location
open Signature
open Types
type iterator_type =
| Imap
@ -35,16 +36,17 @@ and desc =
| Efield of exp * longname
| Estruct of (longname * exp) list
| Eapp of app * exp list
| Eiterator of iterator_type * app * static_exp * exp list
| Eiterator of iterator_type * app * exp * exp list
and app = { a_op: op; a_params: static_exp list; }
and app = { a_op: op; a_params: exp list; }
and op =
| Etuple
| Enode of longname
| Efun of longname
| Eifthenelse
| Earrow
| Efield_update of longname (* field name args would be [record ; value] *)
| Efield_update (* field name args would be [record ; value] *)
| Earray
| Earray_fill
| Eselect
@ -149,7 +151,7 @@ type signature =
sig_inputs : arg list;
sig_statefull : bool;
sig_outputs : arg list;
sig_params : name list; }
sig_params : var_dec list; }
type interface = interface_decl list
@ -173,11 +175,11 @@ let mk_app op params =
let mk_call ?(params=[]) op exps =
Eapp (mk_app op params, exps)
let mk_op_call ?(params=[])s exps =
mk_call (Efun (Name s)) params exps
let mk_op_call ?(params=[]) s exps =
mk_call ~params:params (Efun (Name s)) exps
let mk_iterator_call it ln params exps =
mk_array_op_call (Eiterator (it, mk_op_desc ln params Enode)) exps
let mk_iterator_call it ln params n exps =
Eiterator (it, mk_app (Enode ln) params, n, exps)
let mk_type_dec name desc =
{ t_name = name; t_desc = desc; t_loc = Location.current_loc () }

152
compiler/heptagon/parsing/hept_scoping.ml
View file

@ -2,6 +2,7 @@
names by qualified names *)
open Location
open Types
open Hept_parsetree
open Names
open Ident
@ -68,7 +69,7 @@ let add_const_var loc x env =
if NamesEnv.mem x env then
Error.message loc (Error.Econst_variable_already_defined x)
else (* create a new id for this var and add it to the env *)
NamesEnv.add x (ident_of_name x) env
NamesEnv.add x x env
let rec build_pat loc env = function
| Evarpat x -> add_var loc x env
@ -88,8 +89,8 @@ let build_cd_list env l =
List.fold_left build_cd env l
let build_id_list loc env l =
let build_id env id =
add_const_var loc id env
let build_id env vd =
add_const_var loc vd.v_name env
in
List.fold_left build_id env l
@ -99,35 +100,35 @@ let translate_iterator_type = function
| Ifold -> Heptagon.Ifold
| Imapfold -> Heptagon.Imapfold
let translate_op_kind = function
| Efun -> Heptagon.Efun
| Enode -> Heptagon.Enode
let op_from_app loc app =
match app.a_op with
| Ecall { op_name = op; op_kind = Efun } -> op_from_app_name op
| Efun op -> op_from_app_name op
| _ -> Error.message loc Error.Estatic_exp_expected
let rec static_exp_of_exp const_env e = match e.e_desc with
| Evar n ->
if NamesEnv.mem n const_env then
Svar n
else
raise Not_static
| Econst se -> se
| Eapp({ a_op = Earray_fill }, [e;n]) ->
Sarray_power (static_exp_of_exp const_env e,
static_exp_of_exp const_env n)
| Eapp({ a_op = Earray }, e_list) ->
Sarray (List.map (static_exp_of_exp const_env) e_list)
| Eapp({ a_op = Etuple }, e_list) ->
Stuple (List.map (static_exp_of_exp const_env) e_list)
| Eapp(app, e_list) ->
let op = op_from_app e.e_loc app in
Sop(op, List.map (static_exp_of_exp const_env) e_list)
| Estruct e_list ->
Srecord (List.map (fun (f,e) -> f, static_exp_of_exp const_env e) e_list)
| _ -> raise Not_static
let rec static_exp_of_exp const_env e =
let desc = match e.e_desc with
| Evar n ->
if NamesEnv.mem n const_env then
Svar (Name n)
else
raise Not_static
| Econst se -> se.se_desc
| Eapp({ a_op = Earray_fill }, [e;n]) ->
Sarray_power (static_exp_of_exp const_env e,
static_exp_of_exp const_env n)
| Eapp({ a_op = Earray }, e_list) ->
Sarray (List.map (static_exp_of_exp const_env) e_list)
| Eapp({ a_op = Etuple }, e_list) ->
Stuple (List.map (static_exp_of_exp const_env) e_list)
| Eapp(app, e_list) ->
let op = op_from_app e.e_loc app in
Sop(op, List.map (static_exp_of_exp const_env) e_list)
| Estruct e_list ->
Srecord (List.map (fun (f,e) -> f,
static_exp_of_exp const_env e) e_list)
| _ -> raise Not_static
in
mk_static_exp ~loc:e.e_loc desc
let expect_static_exp const_env e =
try
@ -140,73 +141,66 @@ let rec translate_type const_env = function
| Tid ln -> Types.Tid ln
| Tarray (ty, e) ->
let ty = translate_type const_env ty in
Types.Tarray (ty, expect_static_exp const_env e)
Types.Tarray (ty, expect_static_exp const_env e)
and translate_exp const_env env e =
let desc =
try (* try to see if the exp is a constant *)
Econst (translate_static_exp const_env e)
Heptagon.Econst (expect_static_exp const_env e)
with
Not_static -> translate_desc e.e_loc const_env env e.e_desc in
{ Heptagon.e_desc = desc;
Heptagon.e_ty = Types.invalid_type;
Heptagon.e_loc = e.e_loc }
and translate_app const_env env app =
let op = match app.a_op with
| Epre None -> Heptagon.Epre None
| Epre (Some e) ->
Heptagon.Epre (Some (expect_static_exp const_env e))
| Efby -> Heptagon.Efby
| Earrow -> Heptagon.Earrow
| Eifthenelse -> Heptagon.Eifthenelse
| Ecall desc -> Heptagon.Ecall (translate_op_desc const_env desc, None)
| Efield_update f -> Heptagon.Efield_update f
| Earray_op op -> Heptagon.Earray_op (translate_array_op const_env env op)
in
{ Heptagon.a_op = op; }
and translate_op_desc const_env desc =
{ Heptagon.op_name = desc.op_name;
Heptagon.op_params =
List.map (expect_static_exp const_env) desc.op_params;
Heptagon.op_kind = translate_op_kind desc.op_kind }
and translate_array_op const_env env = function
| Eselect e_list ->
Heptagon.Eselect (List.map (expect_static_exp const_env) e_list)
| Eupdate e_list ->
Heptagon.Eupdate (List.map (expect_static_exp const_env) e_list)
| Erepeat -> Heptagon.Erepeat
| Eselect_slice -> Heptagon.Eselect_slice
| Econcat -> Heptagon.Econcat
| Eselect_dyn -> Heptagon.Eselect_dyn
| Eiterator (it, desc) ->
Heptagon.Eiterator (translate_iterator_type it,
translate_op_desc const_env desc, None)
and translate_desc loc const_env env = function
| Econst c -> Heptagon.Econst c
| Evar x ->
if Rename.mem x env then (* defined var *)
Heptagon.Evar (Rename.name loc env x)
else if NamesEnv.mem x const_env then (* defined as const var *)
Heptagon.Econst (Svar x)
Heptagon.Econst (mk_static_exp (Svar (Modules.longname x)))
else (* undefined var *)
Error.message loc (Error.Evar x)
| Elast x -> Heptagon.Elast (Rename.name loc env x)
| Etuple e_list ->
Heptagon.Etuple (List.map (translate_exp const_env env) e_list)
| Eapp (app, e_list) ->
let e_list = List.map (translate_exp const_env env) e_list in
Heptagon.Eapp (translate_app const_env env app, e_list)
| Epre (None, e) -> Heptagon.Epre (None, translate_exp const_env env e)
| Epre (Some c, e) ->
Heptagon.Epre (Some (expect_static_exp const_env c),
translate_exp const_env env e)
| Efby (e1, e2) -> Heptagon.Efby (translate_exp const_env env e1,
translate_exp const_env env e2)
| Efield (e, field) -> Heptagon.Efield (translate_exp const_env env e, field)
| Estruct f_e_list ->
let f_e_list =
List.map (fun (f,e) -> f, translate_exp const_env env e) f_e_list in
Heptagon.Estruct f_e_list
| Earray e_list ->
Heptagon.Earray (List.map (translate_exp const_env env) e_list)
| Eapp ({ a_op = op; a_params = params }, e_list) ->
let e_list = List.map (translate_exp const_env env) e_list in
let params = List.map (expect_static_exp const_env) params in
let app = Heptagon.mk_op ~params:params (translate_op op) in
Heptagon.Eapp (app, e_list, None)
| Eiterator (it, { a_op = op; a_params = params }, n, e_list) ->
let e_list = List.map (translate_exp const_env env) e_list in
let n = expect_static_exp const_env n in
let params = List.map (expect_static_exp const_env) params in
let app = Heptagon.mk_op ~params:params (translate_op op) in
Heptagon.Eiterator (translate_iterator_type it,
app, n, e_list, None)
and translate_op = function
| Earrow -> Heptagon.Earrow
| Eifthenelse -> Heptagon.Eifthenelse
| Efield_update -> Heptagon.Efield_update
| Etuple -> Heptagon.Etuple
| Earray -> Heptagon.Earray
| Eselect -> Heptagon.Eselect
| Eupdate -> Heptagon.Eupdate
| Earray_fill -> Heptagon.Earray_fill
| Eselect_slice -> Heptagon.Eselect_slice
| Econcat -> Heptagon.Econcat
| Eselect_dyn -> Heptagon.Eselect_dyn
| Efun ln -> Heptagon.Efun ln
| Enode ln -> Heptagon.Enode ln
and translate_pat loc env = function
| Evarpat x -> Heptagon.Evarpat (Rename.name loc env x)
@ -281,13 +275,11 @@ and translate_last const_env env = function
let translate_contract const_env env ct =
{ Heptagon.c_assume = translate_exp const_env env ct.c_assume;
Heptagon.c_enforce = translate_exp const_env env ct.c_enforce;
Heptagon.c_controllables =
translate_vd_list const_env env ct.c_controllables;
Heptagon.c_local = translate_vd_list const_env env ct.c_local;
Heptagon.c_eq = List.map (translate_eq const_env env) ct.c_eq }
let param_of_var_dec vd =
mk_param vd.v_name vd.v_type
let param_of_var_dec const_env vd =
Signature.mk_param vd.v_name (translate_type const_env vd.v_type)
let translate_node const_env env node =
let const_env = build_id_list node.n_loc const_env node.n_params in
@ -301,7 +293,7 @@ let translate_node const_env env node =
(translate_contract const_env env) node.n_contract;
Heptagon.n_equs = List.map (translate_eq const_env env) node.n_equs;
Heptagon.n_loc = node.n_loc;
Heptagon.n_params = List.map param_of_var_dec node.n_params;
Heptagon.n_params = List.map (param_of_var_dec const_env) node.n_params;
Heptagon.n_params_constraints = []; }
let translate_typedec const_env ty =
@ -325,16 +317,14 @@ let translate_const_dec const_env cd =
let translate_program p =
let const_env = build_cd_list NamesEnv.empty p.p_consts in
{ Heptagon.p_pragmas = p.p_pragmas;
Heptagon.p_opened = p.p_opened;
{ Heptagon.p_opened = p.p_opened;
Heptagon.p_types = List.map (translate_typedec const_env) p.p_types;
Heptagon.p_nodes =
List.map (translate_node const_env Rename.empty) p.p_nodes;
Heptagon.p_consts = List.map (translate_const_dec const_env) p.p_consts; }
let translate_arg const_env a =
{ Signature.a_name = a.a_name;
Signature.a_type = translate_type const_env a.a_type }
Signature.mk_arg a.a_name (translate_type const_env a.a_type)
let translate_signature s =
let const_env = build_id_list no_location NamesEnv.empty s.sig_params in
@ -342,7 +332,7 @@ let translate_signature s =
Heptagon.sig_inputs = List.map (translate_arg const_env) s.sig_inputs;
Heptagon.sig_outputs = List.map (translate_arg const_env) s.sig_outputs;
Heptagon.sig_statefull = s.sig_statefull;
Heptagon.sig_params = List.map Signature.mk_param s.sig_params; }
Heptagon.sig_params = List.map (param_of_var_dec const_env) s.sig_params; }
let translate_interface_desc const_env = function
| Iopen n -> Heptagon.Iopen n

9
compiler/heptagon/transformations/automata.ml
View file

@ -20,7 +20,7 @@ let mk_var_exp n ty =
mk_exp (Evar n) ty
let mk_pair e1 e2 =
mk_exp (Etuple [e1;e2]) (Tprod [e1.e_ty; e2.e_ty])
mk_exp (mk_op_app Etuple [e1;e2]) (Tprod [e1.e_ty; e2.e_ty])
let mk_reset_equation eq_list e =
mk_equation (Ereset (eq_list, e))
@ -29,11 +29,11 @@ let mk_switch_equation e l =
mk_equation (Eswitch (e, l))
let mk_exp_fby_false e =
mk_exp (Eapp(mk_op (Epre (Some (Cconstr Initial.pfalse))), [e]))
mk_exp (Epre (Some (mk_static_exp (Sconstructor Initial.pfalse)), e))
(Tid Initial.pbool)
let mk_exp_fby_state initial e =
{ e with e_desc = Eapp(mk_op (Epre (Some (Cconstr initial))), [e]) }
{ e with e_desc = Epre (Some (mk_static_exp (Sconstructor initial)), e) }
(* the list of enumerated types introduced to represent states *)
let state_type_dec_list = ref []
@ -107,7 +107,8 @@ and translate_automaton v eq_list handlers =
let pre_next_resetname = Ident.fresh "pnr" in
let name n = Name(NamesEnv.find n states) in
let state n = mk_exp (Econst (Cconstr (name n))) tstatetype in
let state n = mk_exp (Econst (mk_static_exp
(Sconstructor (name n)))) tstatetype in
let statevar n = mk_var_exp n tstatetype in
let boolvar n = mk_var_exp n (Tid Initial.pbool) in

35
compiler/heptagon/transformations/every.ml
View file

@ -67,36 +67,25 @@ and translate_switch acc_eq_list switch_handlers =
and translate v acc_eq_list e =
match e.e_desc with
Econst _ | Evar _ | Econstvar _ | Elast _ -> v,acc_eq_list,e
| Etuple(e_list) ->
let v, acc_eq_list,e_list = translate_list v acc_eq_list e_list in
v,acc_eq_list,
{ e with e_desc = Etuple e_list }
| Eapp ({ a_op = Ecall(op_desc, Some re) } as op, e_list)
when not (is_var re) ->
Econst _ | Evar _ | Elast _ | Efby _ | Epre _ -> v,acc_eq_list,e
| Eapp (op, e_list, Some re) when not (is_var re) ->
let v, acc_eq_list,re = translate v acc_eq_list re in
let n, v, acc_eq_list = equation v acc_eq_list re in
let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in
let re = { re with e_desc = Evar(n) } in
v,acc_eq_list,
{ e with e_desc =
Eapp({ op with a_op = Ecall(op_desc,
Some { re with e_desc = Evar(n) }) },
e_list) }
| Eapp ({ a_op = Earray_op(Eiterator(it, op_desc, Some re)) } as op, e_list)
when not (is_var re) ->
{ e with e_desc = Eapp (op, e_list, Some re) }
| Eiterator(it, op, n, e_list, Some re) when not (is_var re) ->
let v, acc_eq_list,re = translate v acc_eq_list re in
let n, v, acc_eq_list = equation v acc_eq_list re in
let x, v, acc_eq_list = equation v acc_eq_list re in
let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in
let re = { re with e_desc = Evar n } in
let re = { re with e_desc = Evar x } in
v,acc_eq_list,
{ e with e_desc =
Eapp({ op with a_op =
Earray_op(Eiterator(it, op_desc, Some re)) },
e_list) }
| Eapp(f, e_list) ->
{ e with e_desc = Eiterator(it, op, n, e_list, Some re) }
| Eapp(op, e_list, None) ->
let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in
v, acc_eq_list,
{ e with e_desc = Eapp(f, e_list) }
{ e with e_desc = Eapp(op, e_list, None) }
| Efield(e', field) ->
let v, acc_eq_list, e' = translate v acc_eq_list e' in
v,acc_eq_list,
@ -110,10 +99,6 @@ and translate v acc_eq_list e =
(v,acc_eq_list,[]) e_f_list in
v,acc_eq_list,
{ e with e_desc = Estruct(List.rev e_f_list) }
| Earray(e_list) ->
let v, acc_eq_list,e_list = translate_list v acc_eq_list e_list in
v,acc_eq_list,
{ e with e_desc = Earray(e_list) }
and translate_list v acc_eq_list e_list =
let v,acc_eq_list,acc_e =

25
compiler/heptagon/transformations/last.ml
View file

@ -20,8 +20,8 @@ let last (eq_list, env, v) { v_ident = n; v_type = t; v_last = last } =
| Last(default) ->
let lastn = Ident.fresh ("last" ^ (sourcename n)) in
let eq = mk_equation (Eeq (Evarpat lastn,
mk_exp (Eapp (mk_op (Epre default),
[mk_exp (Evar n) t])) t)) in
mk_exp (Epre (default,
mk_exp (Evar n) t)) t)) in
eq:: eq_list,
Env.add n lastn env,
(mk_var_dec lastn t) :: v
@ -51,20 +51,20 @@ and translate_block env ({ b_local = v; b_equs = eq_list } as b) =
and translate env e =
match e.e_desc with
Econst _ | Evar _ | Econstvar _ -> e
| Econst _ | Evar _ -> e
| Elast(x) ->
let lx = Env.find x env in { e with e_desc = Evar(lx) }
| Etuple(e_list) ->
{ e with e_desc = Etuple(List.map (translate env) e_list) }
| Eapp(op, e_list) ->
{ e with e_desc = Eapp(op, List.map (translate env) e_list) }
| Epre(c, e) ->
{ e with e_desc = Epre(c, translate env e) }
| Efby (e1, e2) ->
{ e with e_desc = Efby(translate env e1, translate env e2) }
| Eapp(op, e_list, r) ->
{ e with e_desc = Eapp(op, List.map (translate env) e_list, r) }
| Efield(e', field) ->
{ e with e_desc = Efield(translate env e', field) }
| Estruct(e_f_list) ->
{ e with e_desc =
Estruct(List.map (fun (f, e) -> (f, translate env e)) e_f_list) }
| Earray(e_list) ->
{ e with e_desc = Earray(List.map (translate env) e_list) }
let translate_contract env contract =
match contract with
@ -72,9 +72,7 @@ let translate_contract env contract =
| Some { c_local = v;
c_eq = eq_list;
c_assume = e_a;
c_enforce = e_g;
c_controllables = cl } ->
let _, env, _ = extend_env env cl in
c_enforce = e_g } ->
let eq_lastn_n_list, env', last_v = extend_env env v in
let eq_list = translate_eqs env' eq_list in
let e_a = translate env' e_a in
@ -82,8 +80,7 @@ let translate_contract env contract =
Some { c_local = v @ last_v;
c_eq = eq_lastn_n_list @ eq_list;
c_assume = e_a;
c_enforce = e_g;
c_controllables = List.rev cl },
c_enforce = e_g },
env
let node ({ n_input = i; n_local = v; n_output = o;

84
compiler/heptagon/transformations/reset.ml
View file

@ -45,11 +45,11 @@ let mk_bool_var n =
let mk_bool_param n =
mk_var_dec n (Tid Initial.pbool)
let or_op_call = mk_op ( Ecall(mk_op_desc Initial.por [] Efun, None) )
let or_op_call = mk_op (Efun Initial.por)
let pre_true e = {
e with e_desc = Eapp(mk_op (Epre (Some (Cconstr Initial.ptrue))), [e])
}
let pre_true e =
{ e with e_desc = Epre (Some (mk_static_exp ~ty:(Tid Initial.pbool)
(Sconstructor Initial.ptrue)), e) }
let init e = pre_true { dfalse with e_loc = e.e_loc }
(* the boolean condition for a structural reset *)
@ -68,7 +68,7 @@ let rec or_op res e =
match res with
| Rfalse -> e
| Rorthen(res, n) ->
or_op res { e with e_desc = Eapp(or_op_call, [mk_bool_var n; e]) }
or_op res { e with e_desc = Eapp(or_op_call, [mk_bool_var n; e], None) }
let default e =
match e.e_desc with
@ -198,69 +198,61 @@ and translate_switch res locals acc_eq_list switch_handlers =
and translate res e =
match e.e_desc with
| Econst _ | Evar _ | Econstvar _ | Elast _ -> e
| Etuple(e_list) ->
{ e with e_desc = Etuple(List.map (translate res) e_list) }
| Eapp({a_op = Efby } as op, [e1;e2]) ->
| Econst _ | Evar _ | Elast _ -> e
| Efby (e1, e2) ->
let e1 = translate res e1 in
let e2 = translate res e2 in
begin
match res, e1 with
| Rfalse, { e_desc = Econst(c) } ->
| Rfalse, { e_desc = Econst c } ->
(* no reset *)
{ e with e_desc =
Eapp({ op with a_op = Epre(Some c) }, [e2]) }
{ e with e_desc = Epre(Some c, e2) }
| _ ->
ifres res e1
{ e with e_desc =
Eapp({ op with a_op = Epre(default e1) }, [e2]) }
{ e with e_desc = Epre(default e1, e2) }
end
| Eapp({ a_op = Earrow }, [e1;e2]) ->
| Eapp({ a_op = Earrow }, [e1;e2], _) ->
let e1 = translate res e1 in
let e2 = translate res e2 in
ifres res e1 e2
| Epre (c, e1) ->
{ e with e_desc = Epre (c, translate res e1)}
(* add reset to the current reset exp. *)
| Eapp({ a_op = Ecall(op_desc, Some re) } as op, e_list) ->
| Eapp({ a_op = Enode _ } as op, e_list, Some re) ->
let re = translate res re in
let e_list = List.map (translate res) e_list in
let op = { op with a_op = Ecall(op_desc, Some (or_op res re))} in
{ e with e_desc = Eapp(op, e_list) }
(* create a new reset exp if necessary *)
| Eapp({ a_op = Ecall(op_desc, None) } as op, e_list) ->
let e_list = List.map (translate res) e_list in
if true_reset res & op_desc.op_kind = Enode then
let op = { op with a_op = Ecall(op_desc, Some (exp_of_res res)) } in
{ e with e_desc = Eapp(op, e_list) }
else
{ e with e_desc = Eapp(op, e_list ) }
(* add reset to the current reset exp. *)
| Eapp( { a_op = Earray_op (Eiterator(it, op_desc, Some re)) } as op,
e_list) ->
let re = translate res re in
let e_list = List.map (translate res) e_list in
let r = Some (or_op res re) in
let op = { op with a_op = Earray_op (Eiterator(it, op_desc, r)) } in
{ e with e_desc = Eapp(op, e_list) }
(* create a new reset exp if necessary *)
| Eapp({ a_op = Earray_op (Eiterator(it, op_desc, None)) } as op, e_list) ->
{ e with e_desc = Eapp(op, e_list, Some (or_op res re)) }
(* create a new reset exp if necessary *)
| Eapp({ a_op = Enode _ } as op, e_list, None) ->
let e_list = List.map (translate res) e_list in
if true_reset res then
let r = Some (exp_of_res res) in
let op = { op with a_op = Earray_op (Eiterator(it, op_desc, r)) } in
{ e with e_desc = Eapp(op, e_list) }
{ e with e_desc = Eapp(op, e_list, Some (exp_of_res res)) }
else
{ e with e_desc = Eapp(op, e_list) }
{ e with e_desc = Eapp(op, e_list, None) }
(* add reset to the current reset exp. *)
| Eiterator(it, ({ a_op = Enode _ } as op), n, e_list, Some re) ->
let re = translate res re in
let e_list = List.map (translate res) e_list in
{ e with e_desc = Eiterator(it, op, n, e_list, Some (or_op res re)) }
(* create a new reset exp if necessary *)
| Eiterator(it, ({ a_op = Enode _ } as op), n, e_list, None) ->
let e_list = List.map (translate res) e_list in
if true_reset res then
{ e with e_desc = Eiterator(it, op, n, e_list, Some (exp_of_res res)) }
else
{ e with e_desc = Eiterator(it, op, n, e_list, None) }
| Eiterator(it, op, n, e_list, r) ->
let e_list = List.map (translate res) e_list in
{ e with e_desc = Eiterator(it, op, n, e_list, None) }
| Eapp(op, e_list) ->
{ e with e_desc = Eapp(op, List.map (translate res) e_list) }
| Eapp(op, e_list, _) ->
{ e with e_desc = Eapp(op, List.map (translate res) e_list, None) }
| Efield(e', field) ->
{ e with e_desc = Efield(translate res e', field) }
| Estruct(e_f_list) ->
{ e with e_desc =
Estruct(List.map (fun (f, e) -> (f, translate res e)) e_f_list) }
| Earray(e_list) ->
{ e with e_desc = Earray(List.map (translate res) e_list) }
let translate_contract ({ c_local = v;
c_eq = eq_list;
@ -271,10 +263,10 @@ let translate_contract ({ c_local = v;
let e_g = translate rfalse e_g in
{ c with c_local = v; c_eq = eq_list; c_assume = e_a; c_enforce = e_g }
let node (n) =
let node n =
let c = optional translate_contract n.n_contract in
let var, eqs = translate_eqs rfalse n.n_local [] n.n_equs in
{ n with n_local = var; n_equs = eqs; n_contract = c }
let program (p) =
let program p =
{ p with p_nodes = List.map node p.p_nodes }

10
compiler/minils/minils.ml
View file

@ -114,7 +114,7 @@ type node_dec = {
n_equs : eq list;
n_loc : location;
n_params : param list; (** TODO CP mettre des petits commentaires *)
n_params_constraints : size_constr list;
n_params_constraints : size_constraint list;
n_params_instances : (static_exp list) list }
type const_dec = {
@ -154,10 +154,10 @@ let mk_node
n_params_instances = pinst; }
let mk_type_dec ?(type_desc = Type_abs) ?(loc = no_location) name =
t_name = name; t_desc = type_desc; t_loc = loc }
{ t_name = name; t_desc = type_desc; t_loc = loc }
let mk_op ?(op_params = []) ?(op_kind = Enode) lname =
{ op_name = lname; op_params = op_params; op_kind = op_kind }
let mk_app ?(params=[]) ?(unsafe=false) op =
{ a_op = op; a_params = params; a_unsafe = unsafe }
let void = mk_exp (Etuple [])
let void = mk_exp (Eapp (mk_app Etuple, [], None))

9
compiler/minils/mls_printer.ml
View file

@ -47,12 +47,6 @@ let print_local_vars ff = function
| [] -> ()
| l -> fprintf ff "@[<4>%a@]@\n" (print_list_r print_vd "var "";"";") l
let rec print_c ff = function
| Cint i -> fprintf ff "%d" i
| Cfloat f -> fprintf ff "%f" f
| Cconstr tag -> print_longname ff tag
| Carray (n, c) -> fprintf ff "%a^%a" print_c c print_static_exp n
let rec print_params ff l =
fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "<<"","">>") l
@ -71,9 +65,6 @@ and print_index ff idx =
and print_dyn_index ff idx =
fprintf ff "@[<2>%a@]" (print_list print_exp "[""][""]") idx
and print_op ff op =
fprintf ff "%a%a" print_longname op.op_name print_params op.op_params
and print_exp ff e =
if !Misc.full_type_info then
fprintf ff "%a : %a" print_exp_desc e.e_desc print_type e.e_ty