diff --git a/compiler/global/global_printer.ml b/compiler/global/global_printer.ml index 2414e5d..6e8be1b 100644 --- a/compiler/global/global_printer.ml +++ b/compiler/global/global_printer.ml @@ -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 "@[val %a%a@[%a@] returns @[%a@]@,@[%a@]@]" + fprintf ff "@[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 diff --git a/compiler/global/signature.ml b/compiler/global/signature.ml index 970589e..6db616c 100644 --- a/compiler/global/signature.ml +++ b/compiler/global/signature.ml @@ -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 diff --git a/compiler/global/static.ml b/compiler/global/static.ml index 4196e39..de0c557 100644 --- a/compiler/global/static.ml +++ b/compiler/global/static.ml @@ -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 - +*) diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index ffb0395..69681db 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -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) -> diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 4a1d5e8..b8fe72b 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -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; diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index cea9782..1e96ed3 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -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@]" diff --git a/compiler/heptagon/hept_utils.ml b/compiler/heptagon/hept_utils.ml index c793242..3fe7b30 100644 --- a/compiler/heptagon/hept_utils.ml +++ b/compiler/heptagon/hept_utils.ml @@ -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 } diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 3a3f99b..3aadc1b 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -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 diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 75506ae..a20d9b3 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -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)) }) } ; diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index 6394fb9..27800cc 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -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 diff --git a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml index 29e6824..91b252f 100644 --- a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml +++ b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml @@ -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; } diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 397bd30..5c08e42 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -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 diff --git a/compiler/heptagon/parsing/hept_static_scoping.ml b/compiler/heptagon/parsing/hept_static_scoping.ml index 418c9b4..40e998b 100644 --- a/compiler/heptagon/parsing/hept_static_scoping.ml +++ b/compiler/heptagon/parsing/hept_static_scoping.ml @@ -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 diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 2f328e8..f5b191c 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -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} = diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 4aae37d..9214ed7 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -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 } diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml index 8db4f19..5dc009a 100644 --- a/compiler/minils/mls_utils.ml +++ b/compiler/minils/mls_utils.ml @@ -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 } diff --git a/compiler/minils/transformations/callgraph.ml b/compiler/minils/transformations/callgraph.ml index 22e23f2..2299b7a 100644 --- a/compiler/minils/transformations/callgraph.ml +++ b/compiler/minils/transformations/callgraph.ml @@ -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) diff --git a/compiler/minils/transformations/checkpass.ml b/compiler/minils/transformations/checkpass.ml index 2a023a2..8b375fd 100644 --- a/compiler/minils/transformations/checkpass.ml +++ b/compiler/minils/transformations/checkpass.ml @@ -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 diff --git a/lib/pervasives.epi b/lib/pervasives.epi index e0aded0..36ec716 100644 --- a/lib/pervasives.epi +++ b/lib/pervasives.epi @@ -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 () \ No newline at end of file +val fun assert(bool) returns ()