Skip to content

Commit

Permalink
Fix some issues with how modules and overloads interact
Browse files Browse the repository at this point in the history
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
  • Loading branch information
Alasdair committed Nov 25, 2023
1 parent 8802efc commit 3df8eca
Show file tree
Hide file tree
Showing 6 changed files with 72 additions and 9 deletions.
17 changes: 13 additions & 4 deletions src/lib/project.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
21 changes: 17 additions & 4 deletions src/lib/type_check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
29 changes: 28 additions & 1 deletion src/lib/type_env.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions src/lib/type_env.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
8 changes: 8 additions & 0 deletions test/typecheck/fail/overload_bound.expect
Original file line number Diff line number Diff line change
@@ -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
4 changes: 4 additions & 0 deletions test/typecheck/fail/overload_bound.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@

val foo : unit -> unit

overload foo = {foo}

0 comments on commit 3df8eca

Please sign in to comment.