From f63571c9a6b532f64b415de27bb0ee6cc358388d Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 11 Oct 2018 21:31:23 +0100 Subject: Change the function type in the AST Changes the representation of function types in the ast from Typ_fn : typ -> typ to Typ_fn : typ list -> typ to more accurately represent their use in the various backends, where we often compile functions to either their curried representations as in Lem and Isabelle, or just multiple argument functions in C. There's still some oddity because a single pattern in a function clause can bind against multiple arguments, and maybe we want to forbid this in the future. The syntax also hasn't changed (yet), so in theory this change shouldn't break anything (but it invariably will...). In the future we would ideally require that a function with N arguments has exactly N patterns in its declaration, one for each argument so f : (x, y) -> z f _ = ... would be disallowed (as _ matches both x and y), forcing f(_, _) = z this would simply quite a few things, Also we could have a different syntax for function argument lists and tuples, because it's rather hard to define a function that actually takes a tuple with the syntax how it is now. Some issues I noticed when doing this refactoring: Line 1926 of Coq translation. untuple_args_pat is maybe no longer needed? However there's still some funnyness where a pattern can be used to bind multiple function arguments so maybe it still is. Line 2306 of monomorphisation. I simplified the logic here. I think it's equivalent now, but I could be wrong. Line 4517 of rewrites. I'm not sure what make_cstr_mappings is doing here, but hopefully the simpler version is the same. --- src/initial_check.ml | 31 +++++++++++++++++++++---------- 1 file changed, 21 insertions(+), 10 deletions(-) (limited to 'src/initial_check.ml') diff --git a/src/initial_check.ml b/src/initial_check.ml index dcb7a925..4e6e941d 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -182,9 +182,16 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) | K_infer -> k.k <- K_Typ; Typ_var v | _ -> typ_error l "Required a variable with kind Type, encountered " None (Some v) (Some k)) | None -> typ_error l "Encountered an unbound variable" None (Some v) None) - | Parse_ast.ATyp_fn(arg,ret,efct) -> Typ_fn( (to_ast_typ k_env def_ord arg), - (to_ast_typ k_env def_ord ret), - (to_ast_effects k_env efct)) + | Parse_ast.ATyp_fn(arg,ret,efct) -> + begin match arg with + | Parse_ast.ATyp_aux (Parse_ast.ATyp_tup args, _) -> + Typ_fn (List.map (to_ast_typ k_env def_ord) args, + (to_ast_typ k_env def_ord ret), + (to_ast_effects k_env efct)) + | _ -> Typ_fn ([to_ast_typ k_env def_ord arg], + (to_ast_typ k_env def_ord ret), + (to_ast_effects k_env efct)) + end | Parse_ast.ATyp_bidir (typ1, typ2) -> Typ_bidir ( (to_ast_typ k_env def_ord typ1), (to_ast_typ k_env def_ord typ2)) | Parse_ast.ATyp_tup(typs) -> Typ_tup( List.map (to_ast_typ k_env def_ord) typs) @@ -1093,11 +1100,11 @@ let quant_item_arg = function let undefined_typschm id typq = let qis = quant_items typq in if qis = [] then - mk_typschm typq (mk_typ (Typ_fn (unit_typ, mk_typ (Typ_id id), mk_effect [BE_undef]))) + mk_typschm typq (function_typ [unit_typ] (mk_typ (Typ_id id)) (mk_effect [BE_undef])) else - let arg_typ = mk_typ (Typ_tup (List.concat (List.map quant_item_typ qis))) in + let arg_typs = List.concat (List.map quant_item_typ qis) in let ret_typ = app_typ id (List.concat (List.map quant_item_arg qis)) in - mk_typschm typq (mk_typ (Typ_fn (arg_typ, ret_typ, mk_effect [BE_undef]))) + mk_typschm typq (function_typ arg_typs ret_typ (mk_effect [BE_undef])) let have_undefined_builtins = ref false @@ -1132,6 +1139,10 @@ let generate_undefineds vs_ids (Defs defs) = mk_exp (E_app (id, List.map (fun _ -> mk_lit_exp L_undef) typs)) | Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_lit_exp L_undef])) in + let p_tup = function + | [pat] -> pat + | pats -> mk_pat (P_tup pats) + in let undefined_td = function | TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in @@ -1144,13 +1155,13 @@ let generate_undefineds vs_ids (Defs defs) = mk_exp (E_app (mk_id "internal_pick", [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]] | TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> - let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in + let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false)); mk_fundef [mk_funcl (prepend_id "undefined_" id) pat (mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]] | TD_variant (id, _, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> - let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in + let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in let body = if !opt_fast_undefined && List.length tus > 0 then undefined_tu (List.hd tus) @@ -1256,7 +1267,7 @@ let generate_enum_functions vs_ids (Defs defs) = else [ enum_val_spec name [mk_qi_id BK_int kid; mk_qi_nc (range_constraint kid)] - (function_typ (atom_typ (nvar kid)) (mk_typ (Typ_id id)) no_effect); + (function_typ [atom_typ (nvar kid)] (mk_typ (Typ_id id)) no_effect); mk_fundef [funcl] ] in @@ -1273,7 +1284,7 @@ let generate_enum_functions vs_ids (Defs defs) = in if IdSet.mem name vs_ids then [] else - [ enum_val_spec name [] (function_typ (mk_typ (Typ_id id)) to_typ no_effect); + [ enum_val_spec name [] (function_typ [mk_typ (Typ_id id)] to_typ no_effect); mk_fundef [funcl] ] in enum :: to_enum @ from_enum @ gen_enums defs -- cgit v1.2.3