Add support for any type of constants
This commit is contained in:
parent
5cc57cd3b0
commit
24cea56666
|
@ -18,7 +18,7 @@ let interface_format_version = "8"
|
||||||
(** Node argument *)
|
(** Node argument *)
|
||||||
type arg = { a_name : name option; a_type : ty }
|
type arg = { a_name : name option; a_type : ty }
|
||||||
|
|
||||||
type param = { p_name : name }
|
type param = { p_name : name; p_type : ty }
|
||||||
|
|
||||||
(** Node signature *)
|
(** Node signature *)
|
||||||
type node =
|
type node =
|
||||||
|
@ -40,7 +40,7 @@ let types_of_arg_list l = List.map (fun ad -> ad.a_type) l
|
||||||
|
|
||||||
let mk_arg name ty = { a_type = ty; a_name = name }
|
let mk_arg name ty = { a_type = ty; a_name = name }
|
||||||
|
|
||||||
let mk_param name = { p_name = name }
|
let mk_param name ty = { p_name = name; p_type = ty }
|
||||||
|
|
||||||
let mk_field n ty = { f_name = n; f_type = ty }
|
let mk_field n ty = { f_name = n; f_type = ty }
|
||||||
|
|
||||||
|
|
|
@ -599,9 +599,11 @@ and typing_app statefull const_env h op e_list =
|
||||||
params in
|
params in
|
||||||
let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in
|
let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in
|
||||||
let typed_e_list = typing_args statefull h expected_ty_list e_list in
|
let typed_e_list = typing_args statefull 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 *)
|
||||||
|
typing_node_params const_env h ty_desc.node_params params;
|
||||||
let size_constrs =
|
let size_constrs =
|
||||||
instanciate_constr m ty_desc.node_params_constraints in
|
instanciate_constr m ty_desc.node_params_constraints in
|
||||||
let result_ty_list = List.map (subst_type_vars m) result_ty_list in
|
|
||||||
List.iter add_size_constraint size_constrs;
|
List.iter add_size_constraint size_constrs;
|
||||||
(prod result_ty_list,
|
(prod result_ty_list,
|
||||||
Ecall ( { op_desc with op_name = Modname q; op_kind = k }, reset),
|
Ecall ( { op_desc with op_name = Modname q; op_kind = k }, reset),
|
||||||
|
@ -767,6 +769,10 @@ and typing_args statefull h expected_ty_list e_list =
|
||||||
with Invalid_argument _ ->
|
with Invalid_argument _ ->
|
||||||
error (Earity_clash(List.length e_list, List.length expected_ty_list))
|
error (Earity_clash(List.length e_list, List.length expected_ty_list))
|
||||||
|
|
||||||
|
and typing_node_params const_env h params_sig params =
|
||||||
|
List.map2 (fun p_sig p -> expect_static_exp const_env no_location
|
||||||
|
p_sig.p_type p) params_sig params
|
||||||
|
|
||||||
let rec typing_pat h acc = function
|
let rec typing_pat h acc = function
|
||||||
| Evarpat(x) ->
|
| Evarpat(x) ->
|
||||||
let ty = typ_of_name h x in
|
let ty = typ_of_name h x in
|
||||||
|
@ -977,7 +983,7 @@ let solve loc env cl =
|
||||||
Solve_failed c -> message loc (Econstraint_solve_failed c)
|
Solve_failed c -> message loc (Econstraint_solve_failed c)
|
||||||
|
|
||||||
let build_node_params const_env l =
|
let build_node_params const_env l =
|
||||||
List.fold_left (fun env n -> NamesEnv.add n (Tid Initial.pint) env)
|
List.fold_left (fun env p -> NamesEnv.add p.p_name p.p_type env)
|
||||||
const_env l
|
const_env l
|
||||||
|
|
||||||
let node const_env const_value_env ({ n_name = f; n_statefull = statefull;
|
let node const_env const_value_env ({ n_name = f; n_statefull = statefull;
|
||||||
|
@ -1043,9 +1049,9 @@ let build_const_value_env cd_list =
|
||||||
NamesEnv.empty cd_list
|
NamesEnv.empty cd_list
|
||||||
|
|
||||||
let build_const_env cd_list =
|
let build_const_env cd_list =
|
||||||
let typing_const_dec const_envenv cd =
|
let typing_const_dec const_env cd =
|
||||||
expect_static_exp const_env cd.c_loc cd.c_type cd.c_value;
|
expect_static_exp const_env cd.c_loc cd.c_type cd.c_value;
|
||||||
NamesEnv.add cd.c_name cd.c_type env
|
NamesEnv.add cd.c_name cd.c_type const_env
|
||||||
in
|
in
|
||||||
List.fold_left typing_const_env NamesEnv.empty cd_list
|
List.fold_left typing_const_env NamesEnv.empty cd_list
|
||||||
|
|
||||||
|
|
|
@ -197,7 +197,7 @@ nonmt_out_params:
|
||||||
|
|
||||||
node_params:
|
node_params:
|
||||||
| /* empty */ { [] }
|
| /* empty */ { [] }
|
||||||
| DOUBLE_LESS ident_list DOUBLE_GREATER { $2 }
|
| DOUBLE_LESS nonmt_params DOUBLE_GREATER { $2 }
|
||||||
;
|
;
|
||||||
|
|
||||||
contract:
|
contract:
|
||||||
|
|
|
@ -127,7 +127,7 @@ type node_dec =
|
||||||
n_contract : contract option;
|
n_contract : contract option;
|
||||||
n_equs : eq list;
|
n_equs : eq list;
|
||||||
n_loc : location;
|
n_loc : location;
|
||||||
n_params : name list; }
|
n_params : var_dec list; }
|
||||||
|
|
||||||
type const_dec =
|
type const_dec =
|
||||||
{ c_name : name;
|
{ c_name : name;
|
||||||
|
|
|
@ -284,6 +284,9 @@ let translate_contract const_env env ct =
|
||||||
Heptagon.c_local = translate_vd_list const_env env ct.c_local;
|
Heptagon.c_local = translate_vd_list const_env env ct.c_local;
|
||||||
Heptagon.c_eq = List.map (translate_eq const_env env) ct.c_eq }
|
Heptagon.c_eq = List.map (translate_eq const_env env) ct.c_eq }
|
||||||
|
|
||||||
|
let param_of_var_dec vd =
|
||||||
|
mk_param vd.v_name vd.v_type
|
||||||
|
|
||||||
let translate_node const_env env node =
|
let translate_node const_env env node =
|
||||||
let const_env = build_id_list node.n_loc const_env node.n_params in
|
let const_env = build_id_list node.n_loc const_env node.n_params in
|
||||||
let env = build_vd_list env (node.n_input @ node.n_output @ node.n_local) in
|
let env = build_vd_list env (node.n_input @ node.n_output @ node.n_local) in
|
||||||
|
@ -296,7 +299,7 @@ let translate_node const_env env node =
|
||||||
(translate_contract const_env env) node.n_contract;
|
(translate_contract const_env env) node.n_contract;
|
||||||
Heptagon.n_equs = List.map (translate_eq const_env env) node.n_equs;
|
Heptagon.n_equs = List.map (translate_eq const_env env) node.n_equs;
|
||||||
Heptagon.n_loc = node.n_loc;
|
Heptagon.n_loc = node.n_loc;
|
||||||
Heptagon.n_params = List.map Signature.mk_param node.n_params;
|
Heptagon.n_params = List.map param_of_var_dec node.n_params;
|
||||||
Heptagon.n_params_constraints = []; }
|
Heptagon.n_params_constraints = []; }
|
||||||
|
|
||||||
let translate_typedec const_env ty =
|
let translate_typedec const_env ty =
|
||||||
|
|
Loading…
Reference in a new issue