From 3df8eca50b2159117fc5bdc5a3c063a87bac62e2 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Sat, 25 Nov 2023 01:12:17 +0000 Subject: [PATCH] Fix some issues with how modules and overloads interact Overloads are always defined in the global scope (so they can be overloaded from anywhere) Getting the overload members now only returns those in scope There is a custom error message when we try to use an overload, and none of it's members are in scope --- src/lib/project.ml | 17 +++++++++---- src/lib/type_check.ml | 21 ++++++++++++---- src/lib/type_env.ml | 29 ++++++++++++++++++++++- src/lib/type_env.mli | 2 ++ test/typecheck/fail/overload_bound.expect | 8 +++++++ test/typecheck/fail/overload_bound.sail | 4 ++++ 6 files changed, 72 insertions(+), 9 deletions(-) create mode 100644 test/typecheck/fail/overload_bound.expect create mode 100644 test/typecheck/fail/overload_bound.sail diff --git a/src/lib/project.ml b/src/lib/project.ml index c5d1557e1..5b12662b9 100644 --- a/src/lib/project.ml +++ b/src/lib/project.ml @@ -518,16 +518,25 @@ let run_tests defs (proj : project_structure) = let chan = match List.nth_opt args 0 with Some "stderr" -> stderr | Some "stdout" -> stdout | _ -> invalid_cmd () in + let reduce_req = match List.nth_opt args 1 with Some "reduce_req" -> true | _ -> false in + let darken id color = match ModMap.find_opt id proj.files with Some [] -> color | _ -> color ^ "3" in ModGraph.make_multi_dot ~node_color:(fun id -> - if ModSet.mem id proj.optional then "aquamarine" - else if ModSet.mem id proj.default then "lemonchiffon" - else "white" + darken id + ( if ModSet.mem id proj.optional then "aquamarine" + else if ModSet.mem id proj.default then "lemonchiffon" + else "chartreuse" + ) ) ~edge_color:(fun _ _ -> "black") ~string_of_node:(fun id -> fst proj.names.(id)) chan - [("dotted", ModGraph.transitive_reduction proj.deps); ("solid", proj.requires)] + [ + ("dotted", ModGraph.reverse (ModGraph.transitive_reduction proj.deps)); + ( "solid", + ModGraph.reverse (if reduce_req then ModGraph.transitive_reduction proj.requires else proj.requires) + ); + ] | _ -> () in List.iter (function Def_test (cmd :: args), l -> run_test_cmd l cmd args | _ -> ()) defs diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index 7a8791813..77f84bd78 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -1764,6 +1764,15 @@ let fresh_var = let () = counter := n + 1 in mk_id ("v#" ^ string_of_int n) +let check_overload_member_scope l f overloads env = + if Util.list_empty overloads then ( + let err_l = + List.nth_opt (Env.get_overload_locs f env) 0 + |> Option.fold ~none:l ~some:(fun o_l -> Parse_ast.Hint ("Overload defined here", o_l, l)) + in + typ_error err_l ("Overload " ^ string_of_id f ^ " is defined, but nothing it overloads is in scope") + ) + let rec exp_unconditionally_returns (E_aux (aux, _)) = match aux with | E_return _ -> true @@ -1957,7 +1966,9 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au typ_raise l (Err_no_overloading (mapping, [(forwards_id, err1); (backwards_id, err2)])) end end - | E_app (f, xs), _ when List.length (Env.get_overloads f env) > 0 -> + | E_app (f, xs), _ when Env.is_overload f env -> + let overloads = Env.get_overloads f env in + check_overload_member_scope l f overloads env; let rec try_overload = function | errs, [] -> typ_raise l (Err_no_overloading (f, errs)) | errs, f :: fs -> begin @@ -1968,7 +1979,7 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au try_overload (errs @ [(f, err)], fs) end in - try_overload ([], Env.get_overloads f env) + try_overload ([], overloads) | E_app (f, [x; y]), _ when string_of_id f = "and_bool" || string_of_id f = "or_bool" -> begin (* We have to ensure that the type of y in (x || y) and (x && y) is non-empty, otherwise it could force the entire type of the @@ -3136,7 +3147,9 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) = typ_raise l (Err_no_overloading (mapping, [(forwards_id, err1); (backwards_id, err2)])) end end - | E_app (f, xs) when List.length (Env.get_overloads f env) > 0 -> + | E_app (f, xs) when Env.is_overload f env -> + let overloads = Env.get_overloads f env in + check_overload_member_scope l f overloads env; let rec try_overload = function | errs, [] -> typ_raise l (Err_no_overloading (f, errs)) | errs, f :: fs -> begin @@ -3147,7 +3160,7 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) = try_overload (errs @ [(f, err)], fs) end in - try_overload ([], Env.get_overloads f env) + try_overload ([], overloads) | E_app (f, [x; y]) when string_of_id f = "and_bool" || string_of_id f = "or_bool" -> begin match destruct_exist (typ_of (irule infer_exp env y)) with | None | Some (_, NC_aux (NC_true, _), _) -> infer_funapp l env f [x; y] None diff --git a/src/lib/type_env.ml b/src/lib/type_env.ml index eeb417b31..d896af1ad 100644 --- a/src/lib/type_env.ml +++ b/src/lib/type_env.ml @@ -394,11 +394,38 @@ let already_bound_ctor_fn str id env = Reporting.unreachable (id_loc id) __POS__ ("Could not find original binding for duplicate " ^ str ^ " called " ^ string_of_id id) +let overload_item_in_scope env id = + match Bindings.find_opt id env.global.val_specs with + | Some item -> item_in_scope env item + | None -> ( + match Bindings.find_opt id env.global.union_ids with + | Some item -> item_in_scope env item + | None -> ( + match Bindings.find_opt id env.global.overloads with + | Some item -> item_in_scope env item + | None -> Reporting.unreachable (id_loc id) __POS__ "Does not appear to be a valid overload item" + ) + ) + +let is_overload id env = Bindings.mem id env.global.overloads + +let get_overload_locs id env = match Bindings.find_opt id env.global.overloads with Some item -> item.loc | None -> [] + let get_overloads id env = - try get_item_with_loc hd_opt (id_loc id) env (Bindings.find id env.global.overloads) with Not_found -> [] + match Bindings.find_opt id env.global.overloads with + | None -> [] + | Some item -> + let ids = get_item_with_loc hd_opt (id_loc id) env item in + List.filter (overload_item_in_scope env) ids let add_overloads l id ids env = typ_print (lazy (adding ^ "overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]")); + if bound_ctor_fn env id then ( + let bound_l = Option.get (get_ctor_fn_binding_loc env id) in + typ_error + (Hint ("Previous binding", bound_l, l)) + (string_of_id id ^ " cannot be defined as an overload, as it is already bound") + ); List.iter (fun overload -> if not (bound_ctor_fn env overload || Bindings.mem overload env.global.overloads) then diff --git a/src/lib/type_env.mli b/src/lib/type_env.mli index 388c5b3e1..c38b93481 100644 --- a/src/lib/type_env.mli +++ b/src/lib/type_env.mli @@ -179,6 +179,8 @@ val get_typ_synonyms : t -> (typquant * typ_arg) Bindings.t val bound_typ_id : t -> id -> bool +val is_overload : id -> t -> bool +val get_overload_locs : id -> t -> Ast.l list val add_overloads : l -> id -> id list -> t -> t val get_overloads : id -> t -> id list diff --git a/test/typecheck/fail/overload_bound.expect b/test/typecheck/fail/overload_bound.expect new file mode 100644 index 000000000..0f75a122a --- /dev/null +++ b/test/typecheck/fail/overload_bound.expect @@ -0,0 +1,8 @@ +Type error: +fail/overload_bound.sail:2.4-7: +2 |val foo : unit -> unit +  | ^-^ Previous binding +fail/overload_bound.sail:4.0-20: +4 |overload foo = {foo} +  |^------------------^ +  | foo cannot be defined as an overload, as it is already bound diff --git a/test/typecheck/fail/overload_bound.sail b/test/typecheck/fail/overload_bound.sail new file mode 100644 index 000000000..988dcdd4a --- /dev/null +++ b/test/typecheck/fail/overload_bound.sail @@ -0,0 +1,4 @@ + +val foo : unit -> unit + +overload foo = {foo}