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

Static constraints in the source. Equal removed

Browse source 
( = ) in pervasives is a stub, it will be typed in a polymorphic way.
This is necessary to have a simple way to transform exp into a static_exp
even when there is the = operator.
This commit is contained in:
Léonard Gérard 2011-06-09 14:38:58 +02:00
parent c3382e4284
commit 108981c0eb
19 changed files with 503 additions and 442 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
compiler/global/global_printer.ml
View file

@ -106,12 +106,10 @@ let print_field ff field =
let print_struct ff field_list = print_record print_field ff field_list
let print_size_constraint ff = function
| Cequal (e1, e2) ->
fprintf ff "@[%a = %a@]" print_static_exp e1 print_static_exp e2
| Clequal (e1, e2) ->
fprintf ff "@[%a <= %a@]" print_static_exp e1 print_static_exp e2
| Cfalse -> fprintf ff "Cfalse"
let print_constrnt ff c = print_static_exp ff c
let print_constraints ff c_l =
fprintf ff "@[%a@]" (print_list_r print_constrnt "|"";"";") c_l
let print_param ff p =
fprintf ff "%a:%a" Names.print_name p.p_name print_type p.p_type
@ -143,16 +141,16 @@ let print_sarg ff arg = match arg.a_name with
print_sck arg.a_clock
let print_interface_value ff (name,node) =
let print_node_params ff p_list =
print_list_r (fun ff p -> print_name ff p.p_name) "<<" "," ">>" ff p_list
let print_node_params ff (p_list, constraints) =
fprintf ff "@[<2><<@[%a@]%a>>@]"
(print_list_r (fun ff p -> print_name ff p.p_name) "" "," "") p_list
print_constraints constraints
in
fprintf ff "@[<v 2>val %a%a@[%a@] returns @[%a@]@,@[%a@]@]"
fprintf ff "@[<v 2>val %a%a@[%a@] returns @[%a@]@]"
print_name name
print_node_params node.node_params
print_node_params (node.node_params, node.node_param_constraints)
(print_list_r print_sarg "(" ";" ")") node.node_inputs
(print_list_r print_sarg "(" ";" ")") node.node_outputs
(print_list_r print_size_constraint " with: " "," "") node.node_params_constraints
let print_interface ff =
let m = Modules.current_module () in

9
compiler/global/signature.ml
View file

@ -30,10 +30,7 @@ type arg = {
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
type constrnt = static_exp
(** Node signature *)
type node = {
@ -41,7 +38,7 @@ type node = {
node_outputs : arg list;
node_stateful : bool;
node_params : param list;
node_params_constraints : size_constraint list;
node_param_constraints : constrnt list;
node_loc : location}
type field = { f_name : field_name; f_type : ty }
@ -137,7 +134,7 @@ let mk_node ?(constraints = []) loc ins outs stateful params =
node_outputs = outs;
node_stateful = stateful;
node_params = params;
node_params_constraints = constraints;
node_param_constraints = constraints;
node_loc = loc}
let rec field_assoc f = function

90
compiler/global/static.ml
View file

@ -61,29 +61,45 @@ let message exn =
@raise Partial_evaluation when the application of the operator can't be evaluated.
Otherwise keep as it is unknown operators. *)
let apply_op partial loc op se_list =
match se_list with
| [{ se_desc = Sint n1 }; { se_desc = Sint n2 }] ->
(match op with
| { qual = Pervasives; name = "+" } ->
Sint (n1 + n2)
| { qual = Pervasives; name = "-" } ->
Sint (n1 - n2)
| { qual = Pervasives; name = "*" } ->
Sint (n1 * n2)
| { qual = Pervasives; name = "/" } ->
if n2 = 0 then raise (Evaluation_failed (Division_by_zero, loc));
Sint (n1 / n2)
| { qual = Pervasives; name = "=" } ->
Sbool (n1 = n2)
| _ -> assert false (*TODO: add missing operators*)
)
| [{ se_desc = Sint n }] ->
(match op with
| { qual = Pervasives; name = "~-" } -> Sint (-n)
| _ -> assert false (*TODO: add missing operators*)
)
| _ -> if partial then Sop(op, se_list) (* partial evaluation *)
else raise (Partial_evaluation (Unknown_op op, loc))
let has_var_desc acc se =
let has_var _ _ sed = match sed with
| Svar _ -> sed,true
| _ -> raise Errors.Fallback
in
let se, acc =
Global_mapfold.static_exp_it
{Global_mapfold.defaults with Global_mapfold.static_exp_desc = has_var}
acc se
in
se.se_desc, acc
in
let sed_l, has_var = Misc.mapfold has_var_desc false se_list in
if (op.qual = Pervasives) && not has_var
then (
match op.name, sed_l with
| "+", [Sint n1; Sint n2] -> Sint (n1 + n2)
| "-", [Sint n1; Sint n2] -> Sint (n1 - n2)
| "*", [Sint n1; Sint n2] -> Sint (n1 * n2)
| "/", [Sint n1; Sint n2] ->
if n2 = 0 then raise (Evaluation_failed (Division_by_zero, loc));
Sint (n1 / n2)
| "=", [Sint n1; Sint n2] -> Sbool (n1 = n2)
| "<=", [Sint n1; Sint n2] -> Sbool (n1 <= n2)
| ">=", [Sint n1; Sint n2] -> Sbool (n1 >= n2)
| "<", [Sint n1; Sint n2] -> Sbool (n1 < n2)
| ">", [Sint n1; Sint n2] -> Sbool (n1 > n2)
| "&", [Sbool b1; Sbool b2] -> Sbool (b1 && b2)
| "or", [Sbool b1; Sbool b2] -> Sbool (b1 || b2)
| "not", [Sbool b] -> Sbool (not b)
| "~-", [Sint n] -> Sint (-n)
| f,_ -> Misc.internal_error ("Static evaluation failed of the pervasive operator "^f)
)
else
if partial
then Sop(op, se_list) (* partial evaluation *)
else raise (Partial_evaluation (Unknown_op op, loc))
(** When not [partial],
@ -149,25 +165,13 @@ let int_of_static_exp env se = match (eval env se).se_desc with
(** [is_true env constr] returns whether the constraint is satisfied
in the environment (or None if this can be decided)
and a simplified constraint. *)
let is_true env =
function
| Cequal (e1, e2) when e1 = e2 ->
Some true, Cequal (simplify env e1, simplify env e2)
| Cequal (e1, e2) ->
let e1 = simplify env e1 in
let e2 = simplify env e2 in
(match e1.se_desc, e2.se_desc with
| Sint n1, Sint n2 -> Some (n1 = n2), Cequal (e1, e2)
| (_, _) -> None, Cequal (e1, e2))
| Clequal (e1, e2) ->
let e1 = simplify env e1 in
let e2 = simplify env e2 in
(match e1.se_desc, e2.se_desc with
| Sint n1, Sint n2 -> Some (n1 <= n2), Clequal (e1, e2)
| _, _ -> None, Clequal (e1, e2))
| Cfalse -> None, Cfalse
let is_true env c =
let c = simplify env c in
match c.se_desc with
| Sbool b -> Some b, c
| _ -> None, c
exception Solve_failed of size_constraint
exception Solve_failed of constrnt
(** [solve env constr_list solves a list of constraints. It
removes equations that can be decided and simplify others.
@ -181,7 +185,7 @@ let rec solve const_env =
(match res with
| None -> c :: l
| Some v -> if not v then raise (Solve_failed c) else l)
(*
(** Substitutes variables in the size exp with their value
in the map (mapping vars to size exps). *)
let rec static_exp_subst m se =
@ -210,5 +214,5 @@ let instanciate_constr m constr =
| Clequal (e1, e2) -> Clequal (static_exp_subst m e1, static_exp_subst m e2)
| Cfalse -> Cfalse in
List.map (replace_one m) constr
*)

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

@ -135,7 +135,7 @@ and apply op e_list =
let i2 = typing e2 in
let i3 = typing e3 in
cseq t1 (cor i2 i3)
| (Eequal | Efun _| Enode _ | Econcat | Eselect_slice
| ( Efun _| Enode _ | Econcat | Eselect_slice
| Eselect_dyn | Eselect_trunc | Eselect _ | Earray_fill) ->
ctuplelist (List.map typing e_list)
| (Earray | Etuple) ->

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

@ -41,7 +41,7 @@ type error =
| Esubscripted_value_not_an_array of ty
| Earray_subscript_should_be_const
| Eundefined_const of qualname
| Econstraint_solve_failed of size_constraint
| Econstraint_solve_failed of constrnt
| Etype_should_be_static of ty
| Erecord_type_expected of ty
| Eno_such_field of ty * qualname
@ -52,6 +52,7 @@ type error =
| Emerge_missing_constrs of QualSet.t
| Emerge_uniq of qualname
| Emerge_mix of qualname
| Estatic_constraint of constrnt
exception Unify
exception TypingError of error
@ -136,7 +137,7 @@ let message loc kind =
| Econstraint_solve_failed c ->
eprintf "%aThe following constraint cannot be satisified:@\n%a.@."
print_location loc
print_size_constraint c
print_constrnt c
| Etype_should_be_static ty ->
eprintf "%aThis type should be static : %a.@."
print_location loc
@ -168,6 +169,10 @@ let message loc kind =
as the last argument (found: %a).@."
print_location loc
print_type ty
| Estatic_constraint c ->
eprintf "%aThis application doesn't respect the static constraint :@\n%a.@."
print_location loc
print_location c.se_loc
end;
raise Errors.Error
@ -181,14 +186,6 @@ let find_value v = find_with_error find_value v
let find_constrs c = find_with_error find_constrs c
let find_field f = find_with_error find_field f
(** Constraints related functions *)
let (curr_size_constr : size_constraint list ref) = ref []
let add_size_constraint c =
curr_size_constr := c::(!curr_size_constr)
let get_size_constraint () =
let l = !curr_size_constr in
curr_size_constr := [];
l
(** Helper functions to work with types *)
let element_type ty =
@ -209,25 +206,6 @@ let flatten_ty_list l =
List.fold_right
(fun arg args -> match arg with Tprod l -> l@args | a -> a::args ) l []
let rec unify t1 t2 =
match t1, t2 with
| b1, b2 when b1 = b2 -> ()
| Tprod t1_list, Tprod t2_list ->
(try
List.iter2 unify t1_list t2_list
with
_ -> raise Unify
)
| Tarray (ty1, e1), Tarray (ty2, e2) ->
add_size_constraint (Cequal(e1,e2));
unify ty1 ty2
| _ -> raise Unify
let unify t1 t2 =
let ut1 = unalias_type t1 in
let ut2 = unalias_type t2 in
try unify ut1 ut2 with Unify -> error (Etype_clash(t1, t2))
let kind f ty_desc =
let ty_of_arg v = v.a_type in
let op = if ty_desc.node_stateful then Enode f else Efun f in
@ -383,17 +361,64 @@ let struct_info_from_field f =
with
Not_found -> error (Eundefined (fullname f))
let rec _unify cenv t1 t2 =
match t1, t2 with
| b1, b2 when b1 = b2 -> ()
| Tprod t1_list, Tprod t2_list ->
(try
List.iter2 (_unify cenv) t1_list t2_list
with
_ -> raise Unify
)
| Tarray (ty1, e1), Tarray (ty2, e2) ->
add_constraint_eq cenv e1 e2;
_unify cenv ty1 ty2
| _ -> raise Unify
(** { 3 Constraints related functions } *)
and (curr_constrnt : constrnt list ref) = ref []
and solve c_l =
try Static.solve Names.QualEnv.empty c_l
with Solve_failed c -> error (Estatic_constraint c)
(** [cenv] is the constant env which will be used to simplify the given constraints *)
and add_constraint cenv c =
let c = expect_static_exp cenv Initial.tbool c in
curr_constrnt := (solve [c])@(!curr_constrnt)
(** Add the constraint [c1=c2] *)
and add_constraint_eq cenv c1 c2 =
let c = mk_static_exp tbool (Sop (mk_pervasives "=",[c1;c2])) in
add_constraint cenv c
(** Add the constraint [c1<=c2] *)
and add_constraint_leq cenv c1 c2 =
let c = mk_static_exp tbool (Sop (mk_pervasives "<=",[c1;c2])) in
add_constraint cenv c
and get_constraints () =
let l = !curr_constrnt in
curr_constrnt := [];
l
and unify cenv t1 t2 =
let ut1 = unalias_type t1 in
let ut2 = unalias_type t2 in
try _unify cenv ut1 ut2 with Unify -> error (Etype_clash(t1, t2))
(** [check_type t] checks that t exists *)
let rec check_type const_env = function
and check_type cenv = 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)
let typed_e = expect_static_exp cenv (Tid Initial.pint) e in
Tarray(check_type cenv ty, typed_e)
| Tid ty_name -> Tid ty_name (* TODO bug ? should check that ty_name exists ? *)
| Tprod l ->
Tprod (List.map (check_type const_env) l)
| Tprod l -> Tprod (List.map (check_type cenv) l)
| Tinvalid -> Tinvalid
and typing_static_exp const_env se =
and typing_static_exp cenv se =
try
let desc, ty = match se.se_desc with
| Sint v -> Sint v, Tid Initial.pint
@ -405,29 +430,35 @@ and typing_static_exp const_env se =
let cd = Modules.find_const ln in
Svar ln, cd.Signature.c_type
with Not_found -> (* or a static parameter *)
Svar ln, QualEnv.find ln const_env)
Svar ln, QualEnv.find ln cenv)
| Sconstructor c -> Sconstructor c, find_constrs c
| Sfield c -> Sfield c, Tid (find_field c)
| Sop ({name = "="} as op, se_list) ->
let se1, se2 = assert_2 se_list in
let typed_se1, t1 = typing_static_exp cenv se1 in
let typed_se2 = expect_static_exp cenv t1 se2 in
Sop (op, [typed_se1;typed_se2]), Tid Initial.pbool
| Sop (op, se_list) ->
let ty_desc = find_value op in
let typed_se_list = typing_static_args const_env
(types_of_arg_list ty_desc.node_inputs) se_list in
Sop (op, typed_se_list),
let typed_se_list = typing_static_args cenv
(types_of_arg_list ty_desc.node_inputs) se_list
in
Sop (op, typed_se_list),
prod (types_of_arg_list ty_desc.node_outputs)
| Sarray_power (se, n) ->
let typed_n = expect_static_exp const_env (Tid Initial.pint) n in
let typed_se, ty = typing_static_exp const_env se in
Sarray_power (typed_se, typed_n), Tarray(ty, typed_n)
let typed_n = expect_static_exp cenv (Tid Initial.pint) n in
let typed_se, ty = typing_static_exp cenv se in
Sarray_power (typed_se, typed_n), Tarray(ty, typed_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),
let typed_se, ty = typing_static_exp cenv se in
let typed_se_list = List.map (expect_static_exp cenv ty) se_list in
Sarray (typed_se::typed_se_list),
Tarray(ty, mk_static_int ((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
(List.map (typing_static_exp cenv) se_list) in
Stuple typed_se_list, prod ty_list
| Srecord f_se_list ->
(* find the record type using the first field *)
@ -440,7 +471,7 @@ and typing_static_exp const_env se =
if List.length f_se_list <> List.length fields then
message se.se_loc Esome_fields_are_missing;
let f_se_list =
List.map (typing_static_field const_env fields
List.map (typing_static_field cenv fields
(Tid q)) f_se_list in
Srecord f_se_list, Tid q
in
@ -449,41 +480,43 @@ and typing_static_exp const_env se =
with
TypingError kind -> message se.se_loc kind
and typing_static_field const_env fields t1 (f,se) =
and typing_static_field cenv fields t1 (f,se) =
try
let ty = check_type const_env (field_assoc f fields) in
let typed_se = expect_static_exp const_env ty se in
let ty = check_type cenv (field_assoc f fields) in
let typed_se = expect_static_exp cenv ty se in
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 =
and typing_static_args cenv expected_ty_list e_list =
try
List.map2 (expect_static_exp const_env) expected_ty_list e_list
List.map2 (expect_static_exp cenv) 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
and expect_static_exp cenv exp_ty se =
let se, ty = typing_static_exp cenv se in
try
unify ty exp_ty; se
unify cenv ty exp_ty; se
with
_ -> 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. *)
let field_type const_env f fields t1 loc =
let field_type cenv f fields t1 loc =
try
check_type const_env (field_assoc f fields)
check_type cenv (field_assoc f fields)
with
Not_found -> message loc (Eno_such_field (t1, f))
let rec typing const_env h e =
let rec typing cenv h e =
try
let typed_desc,ty = match e.e_desc with
| Econst c ->
let typed_c, ty = typing_static_exp const_env c in
let typed_c, ty = typing_static_exp cenv c in
Econst typed_c, ty
| Evar x ->
Evar x, typ_of_name h x
@ -492,7 +525,7 @@ let rec typing const_env h e =
| Eapp(op, e_list, r) ->
let ty, op, typed_e_list =
typing_app const_env h op e_list in
typing_app cenv h op e_list in
Eapp(op, typed_e_list, r), ty
| Estruct(l) ->
@ -503,26 +536,24 @@ let rec typing const_env h e =
| (f,_)::_ -> struct_info_from_field f
) in
if List.length l <> List.length fields then
message e.e_loc Esome_fields_are_missing;
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
const_env h fields (Tid q)) l in
let l = List.map (typing_field cenv h fields (Tid q)) l in
Estruct l, Tid q
| Epre (None, e) ->
let typed_e,ty = typing const_env h e in
let typed_e,ty = typing cenv h e in
Epre (None, typed_e), ty
| Epre (Some c, e) ->
let typed_c, t1 = typing_static_exp const_env c in
let typed_e = expect const_env h t1 e in
let typed_c, t1 = typing_static_exp cenv c in
let typed_e = expect cenv h t1 e in
Epre(Some typed_c, typed_e), t1
| Efby (e1, e2) ->
let typed_e1, t1 = typing const_env h e1 in
let typed_e2 = expect const_env h t1 e2 in
let typed_e1, t1 = typing cenv h e1 in
let typed_e2 = expect cenv h t1 e2 in
Efby (typed_e1, typed_e2), t1
| Eiterator (it, ({ a_op = (Enode f | Efun f);
@ -536,31 +567,30 @@ let rec typing const_env h e =
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 typed_n = expect_static_exp cenv (Tid Initial.pint) n in
(*typing of partial application*)
let p_ty_list, expected_ty_list =
Misc.split_at (List.length pe_list) expected_ty_list in
let typed_pe_list = typing_args const_env h p_ty_list pe_list in
let typed_pe_list = typing_args cenv h p_ty_list pe_list in
(*typing of other arguments*)
let ty, typed_e_list = typing_iterator const_env h it n
let ty, typed_e_list = typing_iterator cenv h it n
expected_ty_list result_ty_list e_list in
let typed_params = typing_node_params const_env
let typed_params = typing_node_params cenv
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_int 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_pe_list, typed_e_list, reset), ty
(* add size constraints *)
let constrs = List.map (simplify m) ty_desc.node_param_constraints in
add_constraint_leq cenv (mk_static_int 1) typed_n;
List.iter (add_constraint cenv) constrs;
(* return the type *)
Eiterator(it, { app with a_op = op; a_params = typed_params }
, typed_n, typed_pe_list, typed_e_list, reset), ty
| Eiterator _ -> assert false
| Ewhen (e, c, x) ->
let typed_e, t = typing const_env h e in
let typed_e, t = typing cenv h e in
let tn_expected = find_constrs c in
let tn_actual = typ_of_name h x in
unify tn_actual tn_expected;
unify cenv tn_actual tn_expected;
Ewhen (typed_e, c, x), t
| Emerge (x, (c1,e1)::c_e_list) ->
@ -572,7 +602,7 @@ let rec typing const_env h e =
List.fold_left
(fun c_set (c, _) ->
if QualSet.mem c c_set then message e.e_loc (Emerge_uniq c);
(try unify c_type (find_constrs c)
(try unify cenv c_type (find_constrs c)
with
TypingError(Etype_clash _) -> message e.e_loc (Emerge_mix c));
QualSet.add c c_set) c_set c_e_list in
@ -588,11 +618,11 @@ let rec typing const_env h e =
if not (QualSet.is_empty c_set_diff)
then message e.e_loc (Emerge_missing_constrs c_set_diff);
(* verify [x] is of the right type *)
unify (typ_of_name h x) c_type;
unify cenv (typ_of_name h x) c_type;
(* type *)
let typed_e1, t = typing const_env h e1 in
let typed_e1, t = typing cenv h e1 in
let typed_c_e_list =
List.map (fun (c, e) -> (c, expect const_env h t e)) c_e_list in
List.map (fun (c, e) -> (c, expect cenv h t e)) c_e_list in
Emerge (x, (c1,typed_e1)::typed_c_e_list), t
| Emerge (_, []) -> assert false
in
@ -600,68 +630,68 @@ let rec typing const_env h e =
with
TypingError(kind) -> message e.e_loc kind
and typing_field const_env h fields t1 (f, e) =
and typing_field cenv h fields t1 (f, e) =
try
let ty = check_type const_env (field_assoc f fields) in
let typed_e = expect const_env h ty e in
let ty = check_type cenv (field_assoc f fields) in
let typed_e = expect cenv h ty e in
f, typed_e
with
Not_found -> message e.e_loc (Eno_such_field (t1, f))
and expect const_env h expected_ty e =
let typed_e, actual_ty = typing const_env h e in
and expect cenv h expected_ty e =
let typed_e, actual_ty = typing cenv h e in
try
unify actual_ty expected_ty;
unify cenv actual_ty expected_ty;
typed_e
with TypingError(kind) -> message e.e_loc kind
and typing_app const_env h app e_list =
and typing_app cenv h app e_list =
match app.a_op with
| Eequal ->
let e1, e2 = assert_2 e_list in
let typed_e1, t1 = typing const_env h e1 in
let typed_e2 = expect const_env h t1 e2 in
Tid Initial.pbool, app, [typed_e1; typed_e2]
| Earrow ->
let e1, e2 = assert_2 e_list in
let typed_e1, t1 = typing const_env h e1 in
let typed_e2 = expect const_env h t1 e2 in
let typed_e1, t1 = typing cenv h e1 in
let typed_e2 = expect cenv h t1 e2 in
t1, app, [typed_e1;typed_e2]
| Eifthenelse ->
let e1, e2, e3 = assert_3 e_list in
let typed_e1 = expect const_env h
let typed_e1 = expect cenv h
(Tid Initial.pbool) e1 in
let typed_e2, t1 = typing const_env h e2 in
let typed_e3 = expect const_env h t1 e3 in
let typed_e2, t1 = typing cenv h e2 in
let typed_e3 = expect cenv h t1 e3 in
t1, app, [typed_e1; typed_e2; typed_e3]
| Efun {name = "="} ->
let e1, e2 = assert_2 e_list in
let typed_e1, t1 = typing cenv h e1 in
let typed_e2 = expect cenv h t1 e2 in
Tid Initial.pbool, app, [typed_e1; typed_e2]
| (Efun f | Enode f) ->
let ty_desc = find_value f in
let op, expected_ty_list, result_ty_list = kind f ty_desc in
let node_params = List.map (fun { p_name = n } -> local_qn n) ty_desc.node_params in
let m = build_subst node_params app.a_params in
let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in
let typed_e_list = typing_args const_env h expected_ty_list e_list in
let typed_e_list = typing_args cenv 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 ty_desc.node_params app.a_params in
let size_constrs = instanciate_constr m ty_desc.node_params_constraints in
List.iter add_size_constraint size_constrs;
let typed_params = typing_node_params cenv ty_desc.node_params app.a_params in
let constrs = List.map (simplify m) ty_desc.node_param_constraints in
List.iter (add_constraint cenv) constrs;
prod result_ty_list,
{ app with a_op = op; a_params = typed_params },
typed_e_list
| Etuple ->
let typed_e_list,ty_list =
List.split (List.map (typing const_env h) e_list) in
List.split (List.map (typing cenv h) e_list) in
prod ty_list, app, typed_e_list
| Earray ->
let exp, e_list = assert_1min e_list in
let typed_exp, t1 = typing const_env h exp in
let typed_e_list = List.map (expect const_env h t1) e_list in
let typed_exp, t1 = typing cenv h exp in
let typed_e_list = List.map (expect cenv h t1) e_list in
let n = mk_static_int (List.length e_list + 1) in
Tarray(t1, n), app, typed_exp::typed_e_list
@ -672,83 +702,81 @@ and typing_app const_env h app e_list =
(match f.se_desc with
| Sfield fn -> fn
| _ -> assert false) in
let typed_e, t1 = typing const_env h e in
let typed_e, t1 = typing cenv h e in
let fields = struct_info t1 in
let t2 = field_type const_env fn fields t1 e.e_loc in
let t2 = field_type cenv fn fields t1 e.e_loc in
t2, app, [typed_e]
| Efield_update ->
let e1, e2 = assert_2 e_list in
let f = assert_1 app.a_params in
let typed_e1, t1 = typing const_env h e1 in
let typed_e1, t1 = typing cenv h e1 in
let fields = struct_info t1 in
let fn =
(match f.se_desc with
| Sfield fn -> fn
| _ -> assert false) in
let t2 = field_type const_env fn fields t1 e1.e_loc in
let typed_e2 = expect const_env h t2 e2 in
let t2 = field_type cenv fn fields t1 e1.e_loc in
let typed_e2 = expect cenv h t2 e2 in
t1, app, [typed_e1; typed_e2]
| Earray_fill ->
let n = assert_1 app.a_params in
let e1 = assert_1 e_list in
let typed_n = expect_static_exp const_env (Tid Initial.pint) n in
let typed_e1, t1 = typing const_env h e1 in
add_size_constraint (Clequal (mk_static_int 1, typed_n));
Tarray (t1, typed_n), { app with a_params = [typed_n] }, [typed_e1]
let typed_n = expect_static_exp cenv (Tid Initial.pint) n in
let typed_e1, t1 = typing cenv h e1 in
add_constraint_leq cenv (mk_static_int 1) typed_n;
Tarray (t1, typed_n), { app with a_params = [typed_n] }, [typed_e1]
| Eselect ->
let e1 = assert_1 e_list in
let typed_e1, t1 = typing const_env h e1 in
let typed_e1, t1 = typing cenv h e1 in
let typed_idx_list, ty =
typing_array_subscript const_env h app.a_params t1 in
typing_array_subscript cenv h app.a_params t1 in
ty, { app with a_params = typed_idx_list }, [typed_e1]
| Eselect_dyn ->
let e1, defe, idx_list = assert_2min e_list in
let typed_e1, t1 = typing const_env h e1 in
let typed_defe = expect const_env h (element_type t1) defe in
let typed_e1, t1 = typing cenv h e1 in
let typed_defe = expect cenv h (element_type t1) defe in
let ty, typed_idx_list =
typing_array_subscript_dyn const_env h idx_list t1 in
typing_array_subscript_dyn cenv h idx_list t1 in
ty, app, typed_e1::typed_defe::typed_idx_list
| Eselect_trunc ->
let e1, idx_list = assert_1min e_list in
let typed_e1, t1 = typing const_env h e1 in
let typed_e1, t1 = typing cenv h e1 in
let ty, typed_idx_list =
typing_array_subscript_dyn const_env h idx_list t1 in
typing_array_subscript_dyn cenv h idx_list t1 in
ty, app, typed_e1::typed_idx_list
| Eupdate ->
let e1, e2, idx_list = assert_2min e_list in
let typed_e1, t1 = typing const_env h e1 in
let typed_e1, t1 = typing cenv h e1 in
let ty, typed_idx_list =
typing_array_subscript_dyn const_env h idx_list t1 in
let typed_e2 = expect const_env h ty e2 in
typing_array_subscript_dyn cenv h idx_list t1 in
let typed_e2 = expect cenv h ty e2 in
t1, app, typed_e1::typed_e2::typed_idx_list
| Eselect_slice ->
let e = assert_1 e_list in
let idx1, idx2 = assert_2 app.a_params in
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 const_env h e in
let typed_idx1 = expect_static_exp cenv (Tid Initial.pint) idx1 in
let typed_idx2 = expect_static_exp cenv (Tid Initial.pint) idx2 in
let typed_e, t1 = typing cenv h e in
(*Create the expression to compute the size of the array *)
let e1 =
mk_static_int_op (mk_pervasives "-") [typed_idx2; typed_idx1] in
let e2 =
mk_static_int_op (mk_pervasives "+") [e1;mk_static_int 1 ] in
add_size_constraint (Clequal (mk_static_int 1, e2));
let e1 = mk_static_int_op (mk_pervasives "-") [typed_idx2; typed_idx1] in
let e2 = mk_static_int_op (mk_pervasives "+") [e1;mk_static_int 1 ] in
add_constraint_leq cenv (mk_static_int 1) e2;
Tarray (element_type t1, e2),
{ app with a_params = [typed_idx1; typed_idx2] }, [typed_e]
| Econcat ->
let e1, e2 = assert_2 e_list in
let typed_e1, t1 = typing const_env h e1 in
let typed_e2, t2 = typing const_env h e2 in
let typed_e1, t1 = typing cenv h e1 in
let typed_e2, t2 = typing cenv h e2 in
begin try
unify (element_type t1) (element_type t2)
unify cenv (element_type t1) (element_type t2)
with
TypingError(kind) -> message e1.e_loc kind
end;
@ -758,13 +786,13 @@ and typing_app const_env h app e_list =
and typing_iterator const_env h
and typing_iterator cenv 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 const_env h
let typed_e_list = typing_args cenv h
args_ty_list e_list in
prod result_ty_list, typed_e_list
@ -774,9 +802,9 @@ and typing_iterator const_env h
let result_ty_list =
List.map (fun ty -> Tarray(ty, n)) result_ty_list in
(* Last but one arg of the function should be integer *)
( try unify idx_ty (Tid Initial.pint)
( try unify cenv idx_ty (Tid Initial.pint)
with TypingError _ -> raise (TypingError (Emapi_bad_args idx_ty)));
let typed_e_list = typing_args const_env h
let typed_e_list = typing_args cenv h
args_ty_list e_list in
prod result_ty_list, typed_e_list
@ -784,10 +812,10 @@ and typing_iterator const_env h
let args_ty_list =
map_butlast (fun ty -> Tarray (ty, n)) args_ty_list in
let typed_e_list =
typing_args const_env h args_ty_list e_list in
typing_args cenv 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;
( try unify (last_element args_ty_list) (List.hd result_ty_list)
( try unify cenv (last_element args_ty_list) (List.hd result_ty_list)
with TypingError(kind) -> message (List.hd e_list).e_loc kind );
(List.hd result_ty_list), typed_e_list
@ -795,15 +823,15 @@ and typing_iterator const_env h
let args_ty_list, acc_ty = split_last args_ty_list in
let args_ty_list, idx_ty = split_last args_ty_list in
(* Last but one arg of the function should be integer *)
( try unify idx_ty (Tid Initial.pint)
( try unify cenv idx_ty (Tid Initial.pint)
with TypingError _ -> raise (TypingError (Efoldi_bad_args idx_ty)));
let args_ty_list =
map_butlast (fun ty -> Tarray (ty, n)) (args_ty_list@[acc_ty]) in
let typed_e_list =
typing_args const_env h args_ty_list e_list in
typing_args cenv 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;
( try unify (last_element args_ty_list) (List.hd result_ty_list)
( try unify cenv (last_element args_ty_list) (List.hd result_ty_list)
with TypingError(kind) -> message (List.hd e_list).e_loc kind );
(List.hd result_ty_list), typed_e_list
@ -812,52 +840,51 @@ and typing_iterator const_env h
map_butlast (fun ty -> Tarray (ty, n)) args_ty_list in
let result_ty_list =
map_butlast (fun ty -> Tarray (ty, n)) result_ty_list in
let typed_e_list = typing_args const_env h
let typed_e_list = typing_args cenv h
args_ty_list e_list in
(*check accumulator type matches in input and output*)
( try unify (last_element args_ty_list) (last_element result_ty_list)
( try unify cenv (last_element args_ty_list) (last_element result_ty_list)
with TypingError(kind) -> message (List.hd e_list).e_loc kind );
prod result_ty_list, typed_e_list
and typing_array_subscript const_env h idx_list ty =
and typing_array_subscript cenv h idx_list ty =
match unalias_type ty, idx_list with
| 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_int 0, idx));
let bound =
mk_static_int_op (mk_pervasives "-") [exp; mk_static_int 1] in
add_size_constraint (Clequal (idx,bound));
let typed_idx_list, ty =
typing_array_subscript const_env h idx_list ty in
ignore (expect_static_exp cenv (Tid Initial.pint) exp);
let typed_idx = expect_static_exp cenv (Tid Initial.pint) idx in
add_constraint_leq cenv (mk_static_int 0) idx;
let bound = mk_static_int_op (mk_pervasives "-") [exp; mk_static_int 1] in
add_constraint_leq cenv idx bound;
let typed_idx_list, ty = typing_array_subscript cenv 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 const_env h idx_list ty =
and typing_array_subscript_dyn cenv h idx_list ty =
match unalias_type ty, idx_list with
| ty, [] -> ty, []
| Tarray(ty, _), idx::idx_list ->
let typed_idx = expect const_env h (Tid Initial.pint) idx in
let typed_idx = expect cenv h (Tid Initial.pint) idx in
let ty, typed_idx_list =
typing_array_subscript_dyn const_env h idx_list ty in
typing_array_subscript_dyn cenv h idx_list ty in
ty, typed_idx::typed_idx_list
| _, _ -> error (Esubscripted_value_not_an_array ty)
and typing_args const_env h expected_ty_list e_list =
and typing_args cenv h expected_ty_list e_list =
let typed_e_list, args_ty_list =
List.split (List.map (typing const_env h) e_list) in
List.split (List.map (typing cenv h) e_list)
in
let args_ty_list = flatten_ty_list args_ty_list in
(match args_ty_list, expected_ty_list with
| [], [] -> ()
| _, _ ->
unify (prod args_ty_list) (prod expected_ty_list));
(match args_ty_list, expected_ty_list with
| [], [] -> ()
| _, _ -> unify cenv (prod args_ty_list) (prod expected_ty_list)
);
typed_e_list
and typing_node_params const_env params_sig params =
List.map2 (fun p_sig p -> expect_static_exp const_env
and typing_node_params cenv params_sig params =
List.map2 (fun p_sig p -> expect_static_exp cenv
p_sig.p_type p) params_sig params
@ -874,46 +901,46 @@ let rec typing_pat h acc = function
pat_list (acc, []) in
acc, Tprod(ty_list)
let rec typing_eq const_env h acc eq =
let rec typing_eq cenv h acc eq =
let typed_desc,acc = match eq.eq_desc with
| Eautomaton(state_handlers) ->
let typed_sh,acc =
typing_automaton_handlers const_env h acc state_handlers in
typing_automaton_handlers cenv h acc state_handlers in
Eautomaton(typed_sh),
acc
| Eswitch(e, switch_handlers) ->
let typed_e,ty = typing const_env h e in
let typed_e,ty = typing cenv h e in
let typed_sh,acc =
typing_switch_handlers const_env h acc ty switch_handlers in
typing_switch_handlers cenv h acc ty switch_handlers in
Eswitch(typed_e,typed_sh),
acc
| Epresent(present_handlers, b) ->
let typed_b, def_names, _ = typing_block const_env h b in
let typed_b, def_names, _ = typing_block cenv h b in
let typed_ph, acc =
typing_present_handlers const_env h
typing_present_handlers cenv h
acc def_names present_handlers in
Epresent(typed_ph,typed_b),
acc
| Ereset(b, e) ->
let typed_e = expect const_env h (Tid Initial.pbool) e in
let typed_b, def_names, _ = typing_block const_env h b in
let typed_e = expect cenv h (Tid Initial.pbool) e in
let typed_b, def_names, _ = typing_block cenv h b in
Ereset(typed_b, typed_e),
Env.union def_names acc
| Eblock b ->
let typed_b, def_names, _ = typing_block const_env h b in
let typed_b, def_names, _ = typing_block cenv h b in
Eblock typed_b,
Env.union def_names acc
| Eeq(pat, e) ->
let acc, ty_pat = typing_pat h acc pat in
let typed_e = expect const_env h ty_pat e in
let typed_e = expect cenv h ty_pat e in
Eeq(pat, typed_e),
acc in
{ eq with eq_desc = typed_desc }, acc
and typing_eq_list const_env h acc eq_list =
mapfold (typing_eq const_env h) acc eq_list
and typing_eq_list cenv h acc eq_list =
mapfold (typing_eq cenv h) acc eq_list
and typing_automaton_handlers const_env h acc state_handlers =
and typing_automaton_handlers cenv h acc state_handlers =
(* checks unicity of states *)
let addname acc { s_state = n } =
add_distinct_S n acc in
@ -921,12 +948,12 @@ and typing_automaton_handlers const_env h acc state_handlers =
let escape h ({ e_cond = e; e_next_state = n } as esc) =
if not (NamesSet.mem n states) then error (Eundefined(n));
let typed_e = expect const_env h (Tid Initial.pbool) e in
let typed_e = expect cenv h (Tid Initial.pbool) e in
{ esc with e_cond = typed_e } in
let handler ({ s_block = b; s_until = e_list1;
s_unless = e_list2 } as s) =
let typed_b, defined_names, h0 = typing_block const_env h b in
let typed_b, defined_names, h0 = typing_block cenv h b in
let typed_e_list1 = List.map (escape h0) e_list1 in
let typed_e_list2 = List.map (escape h) e_list2 in
{ s with
@ -942,7 +969,7 @@ and typing_automaton_handlers const_env h acc state_handlers =
typed_handlers,
(add total (add partial acc))
and typing_switch_handlers const_env h acc ty switch_handlers =
and typing_switch_handlers cenv h acc ty switch_handlers =
(* checks unicity of states *)
let addname acc { w_name = n } = add_distinct_qualset n acc in
let cases = List.fold_left addname QualSet.empty switch_handlers in
@ -951,7 +978,7 @@ and typing_switch_handlers const_env h acc ty switch_handlers =
error (Epartial_switch (fullname (QualSet.choose d)));
let handler ({ w_block = b } as sh) =
let typed_b, defined_names, _ = typing_block const_env h b in
let typed_b, defined_names, _ = typing_block cenv h b in
{ sh with w_block = typed_b }, defined_names in
let typed_switch_handlers, defined_names_list =
@ -961,11 +988,11 @@ and typing_switch_handlers const_env h acc ty switch_handlers =
(typed_switch_handlers,
add total (add partial acc))
and typing_present_handlers const_env h acc def_names
and typing_present_handlers cenv h acc def_names
present_handlers =
let handler ({ p_cond = e; p_block = b }) =
let typed_e = expect const_env h (Tid Initial.pbool) e in
let typed_b, defined_names, _ = typing_block const_env h b in
let typed_e = expect cenv h (Tid Initial.pbool) e in
let typed_b, defined_names, _ = typing_block cenv h b in
{ p_cond = typed_e; p_block = typed_b },
defined_names
in
@ -977,12 +1004,12 @@ and typing_present_handlers const_env h acc def_names
(typed_present_handlers,
(add total (add partial acc)))
and typing_block const_env h
and typing_block cenv h
({ b_local = l; b_equs = eq_list; b_loc = loc } as b) =
try
let typed_l, (local_names, h0) = build const_env h l in
let typed_l, (local_names, h0) = build cenv h l in
let typed_eq_list, defined_names =
typing_eq_list const_env h0 Env.empty eq_list in
typing_eq_list cenv h0 Env.empty eq_list in
let defnames = diff_env defined_names local_names in
{ b with
b_defnames = defnames;
@ -997,13 +1024,13 @@ and typing_block const_env h
@return the typed list of var_dec, an environment mapping
names to their types (aka defined names) and the environment
mapping names to types and last that will be used for typing (aka h).*)
and build const_env h dec =
and build cenv h dec =
let var_dec (acc_defined, h) vd =
try
let ty = check_type const_env vd.v_type in
let ty = check_type cenv vd.v_type in
let last_dec = match vd.v_last with
| Last (Some se) -> Last (Some (expect_static_exp const_env ty se))
| Last (Some se) -> Last (Some (expect_static_exp cenv ty se))
| Var | Last None -> vd.v_last in
if Env.mem vd.v_ident h then
@ -1017,70 +1044,63 @@ and build const_env h dec =
in
mapfold var_dec (Env.empty, h) dec
let typing_contract const_env h contract =
let typing_contract cenv h contract =
match contract with
| None -> None,h
| Some ({ c_block = b;
c_assume = e_a;
c_enforce = e_g;
c_controllables = c }) ->
let typed_b, defined_names, _ = typing_block const_env h b in
let typed_b, defined_names, _ = typing_block cenv h b in
(* check that the equations do not define other unexpected names *)
included_env defined_names Env.empty;
(* assumption *)
let typed_e_a = expect const_env h (Tid Initial.pbool) e_a in
let typed_e_a = expect cenv h (Tid Initial.pbool) e_a in
(* property *)
let typed_e_g = expect const_env h (Tid Initial.pbool) e_g in
let typed_e_g = expect cenv h (Tid Initial.pbool) e_g in
let typed_c, (c_names, h) = build const_env h c in
let typed_c, (c_names, h) = build cenv h c in
Some { c_block = typed_b;
c_assume = typed_e_a;
c_enforce = typed_e_g;
c_controllables = typed_c }, h
let solve loc cl =
try
solve QualEnv.empty cl
with
Solve_failed c -> message loc (Econstraint_solve_failed c)
let build_node_params const_env l =
let build_node_params cenv l =
let check_param env p =
let ty = check_type const_env p.p_type in
let ty = check_type cenv p.p_type in
let p = { p with p_type = ty } in
let n = Names.local_qn p.p_name in
p, QualEnv.add n ty env
in
mapfold check_param const_env l
mapfold check_param cenv l
let node ({ n_name = f; n_input = i_list; n_output = o_list;
n_contract = contract;
n_block = b; n_loc = loc;
n_params = node_params; } as n) =
try
let typed_params, const_env =
let typed_params, cenv =
build_node_params QualEnv.empty node_params in
let typed_i_list, (input_names, h) =
build const_env Env.empty i_list in
let typed_o_list, (output_names, h) = build const_env h o_list in
let typed_i_list, (input_names, h) = build cenv Env.empty i_list in
let typed_o_list, (output_names, h) = build cenv h o_list in
(* typing contract *)
let typed_contract, h =
typing_contract const_env h contract in
let typed_contract, h = typing_contract cenv h contract in
let typed_b, defined_names, _ = typing_block const_env h b in
(* check that the defined names match exactly the outputs and locals *)
included_env defined_names output_names;
included_env output_names defined_names;
let typed_b, defined_names, _ = typing_block cenv h b in
(* check that the defined names match exactly the outputs and locals *)
included_env defined_names output_names;
included_env output_names defined_names;
(* update the node signature to add static params constraints *)
let cl = get_size_constraint () in
let cl = solve loc cl in
let s = find_value f in
replace_value f { s with node_params_constraints = cl };
let cl = List.map (expect_static_exp cenv Initial.tbool) s.node_param_constraints in
let cl = cl @ get_constraints () in
let cl = solve cl in
replace_value f { s with node_param_constraints = cl };
{ n with
n_input = typed_i_list;

3
compiler/heptagon/hept_printer.ml
View file

@ -137,9 +137,6 @@ and print_every ff reset =
and print_app ff (app, args) =
match app.a_op with
| Eequal ->
let e1, e2 = assert_2 args in
fprintf ff "@[<2>%a@ = %a@]" print_exp e1 print_exp e2
| Etuple -> print_exp_tuple ff args
| Efun f | Enode f ->
fprintf ff "@[%a@,%a@,%a@]"

9
compiler/heptagon/hept_utils.ml
View file

@ -61,16 +61,17 @@ let mk_simple_equation pat e =
let mk_switch_equation e l =
mk_equation (Eswitch (e, l))
let mk_signature name ins outs stateful params loc =
let mk_signature name ins outs stateful params constraints loc =
{ sig_name = name;
sig_inputs = ins;
sig_stateful = stateful;
sig_outputs = outs;
sig_params = params;
sig_param_constraints = constraints;
sig_loc = loc }
let mk_node
?(input = []) ?(output = []) ?(contract = None) ?(local = [])
?(input = []) ?(output = []) ?(contract = None)
?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = [])
name block =
{ n_name = name;
@ -81,7 +82,7 @@ let mk_node
n_block = block;
n_loc = loc;
n_params = param;
n_params_constraints = constraints }
n_param_constraints = constraints }
(** @return the set of variables defined in [pat]. *)
let vars_pat pat =
@ -109,6 +110,6 @@ let signature_of_node n =
node_outputs = args_of_var_decs n.n_output;
node_stateful = n.n_stateful;
node_params = n.n_params;
node_params_constraints = n.n_params_constraints;
node_param_constraints = n.n_param_constraints;
node_loc = n.n_loc }

32
compiler/heptagon/heptagon.ml
View file

@ -55,7 +55,6 @@ and app = {
a_unsafe : bool }
and op =
| Eequal
| Etuple
| Efun of fun_name
| Enode of fun_name
@ -142,15 +141,15 @@ type contract = {
c_block : block }
type node_dec = {
n_name : qualname;
n_stateful : bool;
n_input : var_dec list;
n_output : var_dec list;
n_contract : contract option;
n_block : block;
n_loc : location;
n_params : param list;
n_params_constraints : size_constraint list }
n_name : qualname;
n_stateful : bool;
n_input : var_dec list;
n_output : var_dec list;
n_contract : contract option;
n_block : block;
n_loc : location;
n_params : param list;
n_param_constraints : constrnt list }
type const_dec = {
c_name : qualname;
@ -170,12 +169,13 @@ and program_desc =
type signature = {
sig_name : qualname;
sig_inputs : arg list;
sig_stateful : bool;
sig_outputs : arg list;
sig_params : param list;
sig_loc : location }
sig_name : qualname;
sig_inputs : arg list;
sig_stateful : bool;
sig_outputs : arg list;
sig_params : param list;
sig_param_constraints : constrnt list;
sig_loc : location }
type interface = interface_decl list

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

@ -160,16 +160,17 @@ label_ty:
;
node_dec:
| node_or_fun ident node_params LPAREN in_params RPAREN
RETURNS LPAREN out_params RPAREN
contract b=block(LET) TEL
{{ n_name = $2;
n_stateful = $1;
n_input = $5;
n_output = $9;
n_contract = $11;
| n=node_or_fun f=ident pc=node_params LPAREN i=in_params RPAREN
RETURNS LPAREN o=out_params RPAREN
c=contract b=block(LET) TEL
{{ n_name = f;
n_stateful = n;
n_input = i;
n_output = o;
n_contract = c;
n_block = b;
n_params = $3;
n_params = fst pc;
n_constraints = snd pc;
n_loc = (Loc($startpos,$endpos)) }}
;
@ -207,9 +208,13 @@ nonmt_out_params:
| var_last SEMICOL nonmt_out_params { $1 @ $3 }
;
constraints:
| /*empty*/ {[]}
| BAR l=slist(SEMICOL, exp) { l }
node_params:
| /* empty */ { [] }
| DOUBLE_LESS nonmt_params DOUBLE_GREATER { $2 }
| /* empty */ { [],[] }
| DOUBLE_LESS p=nonmt_params c=constraints DOUBLE_GREATER { p,c }
;
contract:
@ -474,9 +479,9 @@ _exp:
| exp INFIX0 exp
{ mk_op_call $2 [$1; $3] }
| exp EQUAL exp
{ mk_call Eequal [$1; $3] }
{ mk_op_call "=" [$1; $3] }
| exp LESS_GREATER exp
{ let e = mk_exp (mk_call Eequal [$1; $3]) (Loc($startpos,$endpos)) in
{ let e = mk_exp (mk_op_call "=" [$1; $3]) (Loc($startpos,$endpos)) in
mk_op_call "not" [e] }
| exp OR exp
{ mk_op_call "or" [$1; $3] }
@ -633,13 +638,14 @@ _interface_decl:
| type_dec { Itypedef $1 }
| const_dec { Iconstdef $1 }
| OPEN modul { Iopen $2 }
| VAL node_or_fun ident node_params LPAREN params_signature RPAREN
RETURNS LPAREN params_signature RPAREN
{ Isignature({ sig_name = $3;
sig_inputs = $6;
sig_stateful = $2;
sig_outputs = $10;
sig_params = $4;
| VAL n=node_or_fun f=ident pc=node_params LPAREN i=params_signature RPAREN
RETURNS LPAREN o=params_signature RPAREN
{ Isignature({ sig_name = f;
sig_inputs = i;
sig_stateful = n;
sig_outputs = o;
sig_params = fst pc;
sig_param_constraints = snd pc;
sig_loc = (Loc($startpos,$endpos)) }) }
;

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

@ -89,7 +89,6 @@ and edesc =
and app = { a_op: op; a_params: exp list; }
and op =
| Eequal
| Etuple
| Enode of qualname
| Efun of qualname
@ -173,14 +172,15 @@ type contract =
c_block : block }
type node_dec =
{ n_name : dec_name;
n_stateful : bool;
n_input : var_dec list;
n_output : var_dec list;
n_contract : contract option;
n_block : block;
n_loc : location;
n_params : var_dec list; }
{ n_name : dec_name;
n_stateful : bool;
n_input : var_dec list;
n_output : var_dec list;
n_contract : contract option;
n_block : block;
n_loc : location;
n_params : var_dec list;
n_constraints : exp list; }
type const_dec =
{ c_name : dec_name;
@ -206,12 +206,13 @@ type arg =
a_name : var_name option }
type signature =
{ sig_name : dec_name;
sig_inputs : arg list;
sig_stateful : bool;
sig_outputs : arg list;
sig_params : var_dec list;
sig_loc : location }
{ sig_name : dec_name;
sig_inputs : arg list;
sig_stateful : bool;
sig_outputs : arg list;
sig_params : var_dec list;
sig_param_constraints : exp list;
sig_loc : location }
type interface = interface_decl list

161
compiler/heptagon/parsing/hept_parsetree_mapfold.ml
View file

@ -10,39 +10,38 @@
open Misc
open Errors
open Global_mapfold
(*open Global_mapfold*)
open Hept_parsetree
type 'a hept_it_funs = {
ty : 'a hept_it_funs -> 'a -> Hept_parsetree.ty -> Hept_parsetree.ty * 'a;
static_exp : 'a hept_it_funs -> 'a -> Hept_parsetree.static_exp -> static_exp * 'a;
static_exp_desc : 'a hept_it_funs -> 'a -> Hept_parsetree.static_exp_desc
-> Hept_parsetree.static_exp_desc * 'a;
app: 'a hept_it_funs -> 'a -> Hept_parsetree.app -> Hept_parsetree.app * 'a;
block: 'a hept_it_funs -> 'a -> Hept_parsetree.block -> Hept_parsetree.block * 'a;
edesc: 'a hept_it_funs -> 'a -> Hept_parsetree.edesc -> Hept_parsetree.edesc * 'a;
eq: 'a hept_it_funs -> 'a -> Hept_parsetree.eq -> Hept_parsetree.eq * 'a;
eqdesc: 'a hept_it_funs -> 'a -> Hept_parsetree.eqdesc -> Hept_parsetree.eqdesc * 'a;
escape_unless : 'a hept_it_funs -> 'a -> Hept_parsetree.escape -> Hept_parsetree.escape * 'a;
escape_until: 'a hept_it_funs -> 'a -> Hept_parsetree.escape -> Hept_parsetree.escape * 'a;
exp: 'a hept_it_funs -> 'a -> Hept_parsetree.exp -> Hept_parsetree.exp * 'a;
pat: 'a hept_it_funs -> 'a -> pat -> Hept_parsetree.pat * 'a;
present_handler: 'a hept_it_funs -> 'a -> Hept_parsetree.present_handler
-> Hept_parsetree.present_handler * 'a;
state_handler: 'a hept_it_funs -> 'a -> Hept_parsetree.state_handler
-> Hept_parsetree.state_handler * 'a;
switch_handler: 'a hept_it_funs -> 'a -> Hept_parsetree.switch_handler
-> Hept_parsetree.switch_handler * 'a;
var_dec: 'a hept_it_funs -> 'a -> Hept_parsetree.var_dec -> Hept_parsetree.var_dec * 'a;
last: 'a hept_it_funs -> 'a -> Hept_parsetree.last -> Hept_parsetree.last * 'a;
contract: 'a hept_it_funs -> 'a -> Hept_parsetree.contract -> Hept_parsetree.contract * 'a;
node_dec: 'a hept_it_funs -> 'a -> Hept_parsetree.node_dec -> Hept_parsetree.node_dec * 'a;
const_dec: 'a hept_it_funs -> 'a -> Hept_parsetree.const_dec -> Hept_parsetree.const_dec * 'a;
type_dec: 'a hept_it_funs -> 'a -> Hept_parsetree.type_dec -> Hept_parsetree.type_dec * 'a;
type_desc: 'a hept_it_funs -> 'a -> Hept_parsetree.type_desc -> Hept_parsetree.type_desc * 'a;
program: 'a hept_it_funs -> 'a -> Hept_parsetree.program -> Hept_parsetree.program * 'a;
program_desc: 'a hept_it_funs -> 'a -> Hept_parsetree.program_desc
-> Hept_parsetree.program_desc * 'a; }
ty : 'a hept_it_funs -> 'a -> ty -> ty * 'a;
static_exp : 'a hept_it_funs -> 'a -> static_exp -> static_exp * 'a;
static_exp_desc : 'a hept_it_funs -> 'a -> static_exp_desc -> static_exp_desc * 'a;
app : 'a hept_it_funs -> 'a -> app -> app * 'a;
block : 'a hept_it_funs -> 'a -> block -> block * 'a;
edesc : 'a hept_it_funs -> 'a -> edesc -> edesc * 'a;
eq : 'a hept_it_funs -> 'a -> eq -> eq * 'a;
eqdesc : 'a hept_it_funs -> 'a -> eqdesc -> eqdesc * 'a;
escape_unless : 'a hept_it_funs -> 'a -> escape -> escape * 'a;
escape_until : 'a hept_it_funs -> 'a -> escape -> escape * 'a;
exp : 'a hept_it_funs -> 'a -> exp -> exp * 'a;
pat : 'a hept_it_funs -> 'a -> pat -> pat * 'a;
present_handler : 'a hept_it_funs -> 'a -> present_handler -> present_handler * 'a;
state_handler : 'a hept_it_funs -> 'a -> state_handler -> state_handler * 'a;
switch_handler : 'a hept_it_funs -> 'a -> switch_handler -> switch_handler * 'a;
var_dec : 'a hept_it_funs -> 'a -> var_dec -> var_dec * 'a;
arg : 'a hept_it_funs -> 'a -> arg -> arg * 'a;
last : 'a hept_it_funs -> 'a -> last -> last * 'a;
contract : 'a hept_it_funs -> 'a -> contract -> contract * 'a;
node_dec : 'a hept_it_funs -> 'a -> node_dec -> node_dec * 'a;
const_dec : 'a hept_it_funs -> 'a -> const_dec -> const_dec * 'a;
type_dec : 'a hept_it_funs -> 'a -> type_dec -> type_dec * 'a;
type_desc : 'a hept_it_funs -> 'a -> type_desc -> type_desc * 'a;
program : 'a hept_it_funs -> 'a -> program -> program * 'a;
program_desc : 'a hept_it_funs -> 'a -> program_desc -> program_desc * 'a;
interface : 'a hept_it_funs -> 'a -> interface -> interface * 'a;
interface_desc : 'a hept_it_funs -> 'a -> interface_desc -> interface_desc * 'a;
signature : 'a hept_it_funs -> 'a -> signature -> signature * 'a; }
let rec static_exp_it funs acc se = funs.static_exp funs acc se
and static_exp funs acc se =
@ -217,6 +216,10 @@ and var_dec funs acc vd =
let v_last, acc = last_it funs acc vd.v_last in
{ vd with v_last = v_last; v_type = v_type }, acc
and arg_it funs acc a = funs.arg funs acc a
and arg funs acc a =
let a_type, acc = ty_it funs acc a.a_type in
{ a with a_type = a_type }, acc
and last_it funs acc l =
try funs.last funs acc l
@ -237,12 +240,6 @@ and contract funs acc c =
c_assume = c_assume; c_enforce = c_enforce; c_block = c_block }
, acc
(*
and param_it funs acc vd = funs.param funs acc vd
and param funs acc vd =
let v_last, acc = last_it funs acc vd.v_last in
{ vd with v_last = v_last }, acc
*)
and node_dec_it funs acc nd = funs.node_dec funs acc nd
and node_dec funs acc nd =
@ -250,12 +247,14 @@ and node_dec funs acc nd =
let n_output, acc = mapfold (var_dec_it funs) acc nd.n_output in
let n_params, acc = mapfold (var_dec_it funs) acc nd.n_params in
let n_contract, acc = optional_wacc (contract_it funs) acc nd.n_contract in
let n_constraints, acc = mapfold (exp_it funs) acc nd.n_constraints in
let n_block, acc = block_it funs acc nd.n_block in
{ nd with
n_input = n_input;
n_output = n_output;
n_block = n_block;
n_params = n_params;
n_constraints = n_constraints;
n_contract = n_contract }
, acc
@ -298,7 +297,7 @@ and type_desc funs acc td = match td with
and program_it funs acc p = funs.program funs acc p
and program funs acc p =
let p_desc, acc = mapfold (program_desc funs) acc p.p_desc in
let p_desc, acc = mapfold (program_desc_it funs) acc p.p_desc in
{ p with p_desc = p_desc }, acc
and program_desc_it funs acc pd =
@ -310,6 +309,36 @@ and program_desc funs acc pd = match pd with
| Pnode n -> let n, acc = node_dec_it funs acc n in Pnode n, acc
| Ppragma _ -> pd, acc
and interface_desc_it funs acc id =
try funs.interface_desc funs acc id
with Fallback -> interface_desc funs acc id
and interface_desc funs acc id = match id with
| Iopen _ -> id, acc
| Itypedef t -> let t, acc = type_dec_it funs acc t in Itypedef t, acc
| Iconstdef c -> let c, acc = const_dec_it funs acc c in Iconstdef c, acc
| Isignature s -> let s, acc = signature_it funs acc s in Isignature s, acc
and interface_it funs acc i = funs.interface funs acc i
and interface funs acc i =
let decl acc id =
let idc, acc = interface_desc_it funs acc id.interf_desc in
{ id with interf_desc = idc }, acc
in
mapfold decl acc i
and signature_it funs acc s = funs.signature funs acc s
and signature funs acc s =
let sig_inputs, acc = mapfold (arg_it funs) acc s.sig_inputs in
let sig_outputs, acc = mapfold (arg_it funs) acc s.sig_outputs in
let sig_params, acc = mapfold (var_dec_it funs) acc s.sig_params in
let sig_param_constraints, acc = mapfold (exp_it funs) acc s.sig_param_constraints in
{ s with sig_inputs = sig_inputs;
sig_outputs = sig_outputs;
sig_params = sig_params;
sig_param_constraints = sig_param_constraints; }
, acc
let defaults = {
ty = ty;
static_exp = static_exp;
@ -334,33 +363,41 @@ let defaults = {
type_dec = type_dec;
type_desc = type_desc;
program = program;
program_desc = program_desc }
program_desc = program_desc;
interface = interface;
interface_desc = interface_desc;
signature = signature;
arg = arg; }
let defaults_stop = {
ty = stop;
static_exp = stop;
static_exp_desc = stop;
app = stop;
block = stop;
edesc = stop;
eq = stop;
eqdesc = stop;
escape_unless = stop;
escape_until = stop;
exp = stop;
pat = stop;
present_handler = stop;
state_handler = stop;
switch_handler = stop;
var_dec = stop;
last = stop;
contract = stop;
node_dec = stop;
const_dec = stop;
type_dec = stop;
type_desc = stop;
program = stop;
program_desc = stop }
ty = Global_mapfold.stop;
static_exp = Global_mapfold.stop;
static_exp_desc = Global_mapfold.stop;
app = Global_mapfold.stop;
block = Global_mapfold.stop;
edesc = Global_mapfold.stop;
eq = Global_mapfold.stop;
eqdesc = Global_mapfold.stop;
escape_unless = Global_mapfold.stop;
escape_until = Global_mapfold.stop;
exp = Global_mapfold.stop;
pat = Global_mapfold.stop;
present_handler = Global_mapfold.stop;
state_handler = Global_mapfold.stop;
switch_handler = Global_mapfold.stop;
var_dec = Global_mapfold.stop;
last = Global_mapfold.stop;
contract = Global_mapfold.stop;
node_dec = Global_mapfold.stop;
const_dec = Global_mapfold.stop;
type_dec = Global_mapfold.stop;
type_desc = Global_mapfold.stop;
program = Global_mapfold.stop;
program_desc = Global_mapfold.stop;
interface = Global_mapfold.stop;
interface_desc = Global_mapfold.stop;
signature = Global_mapfold.stop;
arg = Global_mapfold.stop; }

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

@ -153,12 +153,13 @@ end
let mk_app ?(params=[]) ?(unsafe=false) op =
{ Heptagon.a_op = op; Heptagon.a_params = params; Heptagon.a_unsafe = unsafe }
let mk_signature name ins outs stateful params loc =
let mk_signature name ins outs stateful params constraints loc =
{ Heptagon.sig_name = name;
Heptagon.sig_inputs = ins;
Heptagon.sig_stateful = stateful;
Heptagon.sig_outputs = outs;
Heptagon.sig_params = params;
Heptagon.sig_param_constraints = constraints;
Heptagon.sig_loc = loc }
@ -301,7 +302,6 @@ and translate_desc loc env = function
and translate_op = function
| Eequal -> Heptagon.Eequal
| Earrow -> Heptagon.Earrow
| Eifthenelse -> Heptagon.Eifthenelse
| Efield -> Heptagon.Efield
@ -405,16 +405,18 @@ let translate_contract env ct =
Heptagon.c_controllables = translate_vd_list env ct.c_controllables;
Heptagon.c_block = b }
let params_of_var_decs =
List.map (fun vd -> Signature.mk_param
vd.v_name
(translate_type vd.v_loc vd.v_type))
let params_of_var_decs p_l =
let pofvd vd = Signature.mk_param vd.v_name (translate_type vd.v_loc vd.v_type) in
List.map pofvd p_l
let translate_constrnt e = expect_static_exp e
let translate_node node =
let n = current_qual node.n_name in
Idents.enter_node n;
let params = params_of_var_decs node.n_params in
let constraints = List.map translate_constrnt node.n_constraints in
let input_env = Rename.append Rename.empty (node.n_input) in
(* inputs should refer only to inputs *)
let inputs = translate_vd_list input_env node.n_input in
@ -433,7 +435,7 @@ let translate_node node =
Heptagon.n_block = b;
Heptagon.n_loc = node.n_loc;
Heptagon.n_params = params;
Heptagon.n_params_constraints = []; }
Heptagon.n_param_constraints = constraints; }
in
add_value n (Hept_utils.signature_of_node node);
node
@ -480,7 +482,7 @@ let translate_const_dec cd =
let translate_program p =
let translate_program_desc pd = match pd with
| Ppragma _ -> Misc.unsupported "pragma in scoping" 1
| Ppragma _ -> Misc.unsupported "pragma in scoping"
| Pconst c -> Heptagon.Pconst (translate_const_dec c)
| Ptype t -> Heptagon.Ptype (translate_typedec t)
| Pnode n -> Heptagon.Pnode (translate_node n)
@ -506,10 +508,11 @@ let translate_signature s =
let i = List.map translate_arg s.sig_inputs in
let o = List.map translate_arg s.sig_outputs in
let p = params_of_var_decs s.sig_params in
let c = List.map translate_constrnt s.sig_param_constraints in
let sig_node = Signature.mk_node s.sig_loc i o s.sig_stateful p in
Signature.check_signature sig_node;
add_value n sig_node;
mk_signature n i o s.sig_stateful p s.sig_loc
mk_signature n i o s.sig_stateful p c s.sig_loc
let translate_interface_desc = function

20
compiler/heptagon/parsing/hept_static_scoping.ml
View file

@ -36,30 +36,28 @@ let exp funs local_const e =
let sed =
match e.e_desc with
| Evar n ->
(try
Svar (Q (qualify_const local_const (ToQ n)))
with
| Error.ScopingError _ -> raise Not_static)
(try Svar (Q (qualify_const local_const (ToQ n)))
with Error.ScopingError _ -> raise Not_static)
| Eapp({ a_op = Earray_fill; a_params = [n] }, [e]) ->
Sarray_power (assert_se e, assert_se n)
Sarray_power (assert_se e, assert_se n)
| Eapp({ a_op = Earray }, e_list) ->
Sarray (List.map assert_se e_list)
Sarray (List.map assert_se e_list)
| Eapp({ a_op = Etuple }, e_list) ->
Stuple (List.map assert_se e_list)
Stuple (List.map assert_se e_list)
| Eapp(app, e_list) ->
let op, e_list = static_app_from_app app e_list in
let op, e_list = static_app_from_app app e_list in
Sop (op, List.map assert_se e_list)
| Estruct e_list ->
Srecord (List.map (fun (f,e) -> f, assert_se e) e_list)
Srecord (List.map (fun (f,e) -> f, assert_se e) e_list)
| _ -> raise Not_static
in
{ e with e_desc = Econst (mk_static_exp sed e.e_loc) }, local_const
{ e with e_desc = Econst (mk_static_exp sed e.e_loc) }, local_const
with
Not_static -> e, local_const
let node funs _ n =
let local_const = Hept_scoping.build_const n.n_loc n.n_params in
Hept_parsetree_mapfold.node_dec funs local_const n
Hept_parsetree_mapfold.node_dec funs local_const n
let const_dec funs local_const cd =
let cd, _ = Hept_parsetree_mapfold.const_dec funs local_const cd in

3
compiler/main/hept2mls.ml
View file

@ -62,7 +62,6 @@ let translate_iterator_type = function
| Heptagon.Imapfold -> Imapfold
let rec translate_op = function
| Heptagon.Eequal -> Eequal
| Heptagon.Eifthenelse -> Eifthenelse
| Heptagon.Efun f -> Efun f
| Heptagon.Enode f -> Enode f
@ -176,7 +175,7 @@ let node n =
n_equs = List.map translate_eq n.Heptagon.n_block.Heptagon.b_equs;
n_loc = n.Heptagon.n_loc ;
n_params = n.Heptagon.n_params;
n_params_constraints = n.Heptagon.n_params_constraints }
n_param_constraints = n.Heptagon.n_param_constraints }
let typedec
{Heptagon.t_name = n; Heptagon.t_desc = tdesc; Heptagon.t_loc = loc} =

4
compiler/minils/minils.ml
View file

@ -126,7 +126,7 @@ type node_dec = {
n_equs : eq list;
n_loc : location;
n_params : param list;
n_params_constraints : size_constraint list }
n_param_constraints : constrnt list }
type const_dec = {
c_name : qualname;
@ -173,7 +173,7 @@ let mk_node
n_equs = eq;
n_loc = loc;
n_params = param;
n_params_constraints = constraints }
n_param_constraints = constraints }
let mk_type_dec type_desc name loc =
{ t_name = name; t_desc = type_desc; t_loc = loc }

4
compiler/minils/mls_utils.ml
View file

@ -72,7 +72,7 @@ struct
| Con(_, _, n) -> add n acc
| Cbase | Cvar { contents = Cindex _ } -> acc
| Cvar { contents = Clink ck } -> vars_ck acc ck
let rec vars_ct acc = function
| Ck ck -> vars_ck acc ck
| Cprod c_l -> List.fold_left vars_ct acc c_l
@ -208,5 +208,5 @@ let signature_of_node n =
node_outputs = args_of_var_decs n.n_output;
node_stateful = n.n_stateful;
node_params = n.n_params;
node_params_constraints = n.n_params_constraints;
node_param_constraints = n.n_param_constraints;
node_loc = n.n_loc }

4
compiler/minils/transformations/callgraph.ml
View file

@ -182,12 +182,12 @@ struct
let node_sig = find_value n.n_name in
let node_sig, _ = Global_mapfold.node_it global_funs m node_sig in
let node_sig = { node_sig with node_params = [];
node_params_constraints = [] } in
node_param_constraints = [] } in
(* Find the name that was associated to this instance *)
let ln = node_for_params_call n.n_name params in
if not (check_value ln) then
Modules.add_value ln node_sig;
{ n with n_name = ln; n_params = []; n_params_constraints = []; }
{ n with n_name = ln; n_params = []; n_param_constraints = []; }
let node_dec n =
List.map (node_dec_instance n) (get_node_instances n.n_name)

2
compiler/minils/transformations/checkpass.ml
View file

@ -48,7 +48,7 @@ let add_check prefix pass nd nd_list =
node_outputs = [{ a_name = None; a_type = Tid Initial.pbool; }];
node_stateful = true;
node_params = [];
node_params_constraints = [] };
node_param_constraints = [] };
Compiler_options.add_assert nd_check.n_name.name;
nd :: nd' :: nd_check :: nd_list

8
lib/pervasives.epi
View file

@ -1,6 +1,5 @@
(* the core module *)
(* $Id: pervasives.epi 77 2009-03-11 16:07:00Z delaval $ *)
(* pour debugger set arguments -nopervasives -i lib/pervasives.epi *)
(* The core module *)
(* To compile : heptc -nopervasives pervasives.epi *)
type bool = true | false
type int
type float
@ -15,6 +14,7 @@ val fun (-)(int;int) returns (int)
val fun (-.)(float;float) returns (float)
val fun (/)(int;int) returns (int)
val fun (/.)(float;float) returns (float)
val fun ( = )(int;int) returns (bool)
val fun ( <= )(int;int) returns (bool)
val fun ( <=. )(float;float) returns (bool)
val fun ( < )(int;int) returns (bool)
@ -32,4 +32,4 @@ val fun do_stuff(int) returns (int)
val fun between(int;int) returns (int)
val fun exit(bool) returns ()
val fun assert(bool) returns ()
val fun assert(bool) returns ()