Skip to content

Commit

Permalink
Add checking of module constraints on module decl
Browse files Browse the repository at this point in the history
  • Loading branch information
tjammer committed Sep 1, 2023
1 parent a1d5350 commit bcf82aa
Show file tree
Hide file tree
Showing 7 changed files with 147 additions and 21 deletions.
6 changes: 4 additions & 2 deletions lib/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -125,10 +125,12 @@ type top_item =
| Stmt of stmt
| Ext_decl of external_decl
| Typedef of loc * typedef
| Module of ident * signature list * top_item list
| Module_alias of ident * Path.t
| Module of module_decl * signature list * top_item list
| Module_alias of module_decl * Path.t
| Module_type of ident * signature list

and module_decl = loc * string * Path.t option

and signature =
| Stypedef of loc * typedef
| Svalue of loc * (ident * type_spec)
Expand Down
18 changes: 14 additions & 4 deletions lib/module.ml
Original file line number Diff line number Diff line change
Expand Up @@ -717,6 +717,13 @@ let scope_of_located env path =
| Located (filename, loc, regeneralize) ->
read_module env filename loc ~regeneralize path

let rec of_located env path =
match Hashtbl.find module_cache path with
| Cached (_, _, m) -> m
| Located (filename, loc, regeneralize) ->
ignore (read_module env filename loc ~regeneralize path);
of_located env path

let object_names () =
let ours =
Hashtbl.fold
Expand Down Expand Up @@ -777,18 +784,21 @@ let find_item name kind (n, _, _, tkind) =
| (Mvalue, Mvalue | Mtypedef, Mtypedef) when String.equal name n -> true
| _ -> false

let validate_intf env intf impl =
let validate_intf env loc intf impl =
(* Go through signature and check that the implemented types match.
Implementation is appended to a list, so the most current bindings are the ones we pick.
That's exactly what we want. Also, set correct unique name to signature binding. *)
let mbloc otherloc = match loc with Some loc -> loc | None -> otherloc in
let mn = Env.modpath env in
match intf with
| [] -> intf
| _ ->
let impl = List.filter_map (extract_name_type env) impl in
let f (name, loc, styp, kind) =
let loc = mbloc loc in
match (List.find_opt (find_item name kind) impl, kind) with
| Some (n, loc, ityp, ikind), _ ->
let loc = mbloc loc in
let subst, b =
Inference.types_match ~match_abstract:true Smap.empty styp ityp
in
Expand Down Expand Up @@ -829,11 +839,11 @@ let validate_intf env intf impl =
in
List.map f intf

let validate_signature env m = { m with s = validate_intf env m.s m.i }
let validate_signature env loc m = { m with s = validate_intf env loc m.s m.i }

let validate_intf env intf m =
let validate_intf env loc intf m =
match m.s with
| [] -> validate_intf env intf m.i |> ignore
| [] -> validate_intf env loc intf m.i |> ignore
| s ->
ignore s;
failwith "TODO"
Expand Down
5 changes: 3 additions & 2 deletions lib/module.mli
Original file line number Diff line number Diff line change
Expand Up @@ -51,10 +51,11 @@ val find_module :
Env.t -> Ast.loc -> regeneralize:(typ -> typ) -> string -> Env.cached_module

val scope_of_located : Env.t -> Path.t -> Env.scope
val of_located : Env.t -> Path.t -> t
val to_channel : out_channel -> outname:string -> t -> unit
val append_externals : Env.ext list -> Env.ext list
val validate_intf : Env.t -> Module_type.t -> t -> unit
val validate_signature : Env.t -> t -> t
val validate_intf : Env.t -> loc option -> Module_type.t -> t -> unit
val validate_signature : Env.t -> loc option -> t -> t

val to_module_type : t -> Module_type.t
(** Throws if [t] isn't a pure module type *)
19 changes: 13 additions & 6 deletions lib/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -171,15 +171,22 @@ signature: Signature; l = nonempty_list(sig_item) { l }
| Defexternal; ident; sexp_type_expr; option(String_lit) { $loc, $2, $3, $4 }

modul:
| Module; id = ident { Module_alias (id, Path.Pid (snd id)) }
| Module; id = ident; mname = path /* Use location of path */
{ Module_alias ((fst mname, snd id), snd mname) }
| Module; id = ident; hd = module_item; m = list(top_item) { Module (id, [], hd :: m) }
| Module; id = ident; s = parens(signature); m = list(top_item) { Module (id, s, m) }
| Module; id = module_decl { let _, alias, _ = id in Module_alias (id, Path.Pid alias) }
| Module; id = module_decl; mname = path /* Use location of path */
{ let _, id, annot = id in Module_alias ((fst mname, id, annot), snd mname) }
| Module; id = module_decl; hd = module_item; m = list(top_item) { Module (id, [], hd :: m) }
| Module; id = module_decl; s = parens(signature); m = list(top_item) { Module (id, s, m) }

module_type:
%inline module_type:
| Module_type; id = ident; l = nonempty_list(sig_item) { Module_type (id, l) }

%inline module_decl:
| id = ident { fst id, snd id, None }
| decl = parens(module_annot) { decl}

%inline module_annot:
| id = ident; annot = path { fst id, snd id, Some (snd annot) }

%inline path:
| id = ident { $loc, Path.Pid (snd id) }
| id = ident; Div_i; lst = separated_nonempty_list(Div_i, ident)
Expand Down
82 changes: 79 additions & 3 deletions lib/syntax_errors.messages
Original file line number Diff line number Diff line change
Expand Up @@ -1334,9 +1334,29 @@ prog: Lpar Module Wildcard

Expecting definition

prog: Lpar Module Kebab_id Wildcard
prog: Lpar Module Lpar Wildcard

Expecting definition
<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Lpar Kebab_id Wildcard

Expecting module type constraint

prog: Lpar Module Lpar Kebab_id Kebab_id Wildcard

Expecting ')'

prog: Lpar Module Lpar Kebab_id Kebab_id Div_i Wildcard

Expecting module type name

prog: Lpar Module Lpar Kebab_id Kebab_id Div_i Kebab_id String_lit

Expecting module type name

prog: Lpar Module Lpar Kebab_id Kebab_id Rpar Wildcard

Expecting type or value declaration

prog: Lpar Module Kebab_id Lpar Wildcard

Expand Down Expand Up @@ -1370,7 +1390,7 @@ prog: Lpar Module Kebab_id Kebab_id Div_i Kebab_id String_lit

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Kebab_id Lpar Signature Lpar Type Kebab_id Rpar Rpar Wildcard
prog: Lpar Module Lpar Kebab_id Kebab_id Rpar Lpar Signature Lpar Type Kebab_id Rpar Rpar Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

Expand All @@ -1386,6 +1406,62 @@ prog: False Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Lpar Kebab_id Kebab_id Rpar Lpar Rec Lpar Defn Kebab_id Lbrack Rbrack Rpar Lpar Defn Kebab_id Lbrack Rbrack Rpar Rpar Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Lpar Kebab_id Kebab_id Rpar Lpar Open Kebab_id Rpar Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Lpar Kebab_id Kebab_id Rpar Lpar Def Kebab_id False Rpar Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Lpar Kebab_id Kebab_id Rpar Lpar Defn Kebab_id Lbrack Rbrack Rpar Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Lpar Kebab_id Kebab_id Rpar Lpar Module_type Kebab_id Lpar Type Kebab_id Rpar Rpar Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Lpar Kebab_id Kebab_id Rpar Lpar Module Kebab_id Rpar Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Lpar Kebab_id Kebab_id Rpar Lpar Type Kebab_id Constructor Rpar Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Lpar Kebab_id Kebab_id Rpar Lpar Type Kebab_id Lbrac Keyword Kebab_id Rbrac Rpar Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Lpar Kebab_id Kebab_id Rpar Lpar Defexternal Kebab_id Kebab_id Rpar Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Lpar Kebab_id Kebab_id Rpar Lpar Type Kebab_id Kebab_id Rpar Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Lpar Kebab_id Kebab_id Rpar Kebab_id Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Lpar Kebab_id Kebab_id Rpar Kebab_id Div_i Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Kebab_id Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Kebab_id Lpar Signature Lpar Type Kebab_id Rpar Rpar Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>

prog: Lpar Module Kebab_id Lpar Rec Lpar Defn Kebab_id Lbrack Rbrack Rpar Lpar Defn Kebab_id Lbrack Rbrack Rpar Rpar Wildcard

<YOUR SYNTAX ERROR MESSAGE HERE>
Expand Down
18 changes: 15 additions & 3 deletions lib/typing/typing.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1310,6 +1310,15 @@ and catch_weak_expr env sub e =
(function Fstr _ -> () | Fexpr e -> catch_weak_expr env sub e)
fmt

let check_module_annot env loc m annot =
match annot with
| Some path -> (
match Env.find_module_type_opt loc path env with
| Some mtype -> Module.validate_intf env (Some loc) mtype m
| None -> raise (Error (loc, "Cannot find module type " ^ Path.show path))
)
| None -> ()

let rec convert_module env mname sign prog check_ret =
(* We create a new scope so we don't warn on unused imports *)
let env = Env.open_toplevel mname env in
Expand All @@ -1327,7 +1336,7 @@ let rec convert_module env mname sign prog check_ret =
(* Make sure to chose the signature env, not the impl one. Abstract types are
magically made complete by references. *)
let m = List.fold_left (add_signature_vals sigenv) m sign in
let m = Module.validate_signature env m in
let m = Module.validate_signature env None m in

(* Catch weak type variables *)
List.iter (catch_weak_vars env) items;
Expand Down Expand Up @@ -1383,7 +1392,7 @@ and convert_prog env items modul =
(env, items, m)
| Typedef (loc, Tabstract _) ->
raise (Error (loc, "Abstract types need a concrete implementation"))
| Module ((loc, id), sign, prog) ->
| Module ((loc, id, annot), sign, prog) ->
(* External function are added as side-effects, can be discarded here *)
let open Module in
let mname = Path.append id (Env.modpath env) in
Expand All @@ -1409,14 +1418,17 @@ and convert_prog env items modul =
in
raise (Error (loc, msg))
in
check_module_annot env loc newm annot;
let m = add_local_module loc id newm ~into:m in

let moditems = List.map (fun item -> (mname, item)) moditems in
let items = Tl_module moditems :: items in
(env, items, m)
| Module_alias ((loc, key), mname) ->
| Module_alias ((loc, key, annot), mname) ->
let env = Env.add_module_alias loc ~key ~mname env in
let mname = Env.find_module_opt loc (Path.Pid key) env |> Option.get in
if Option.is_some annot then
check_module_annot env loc (Module.of_located env mname) annot;
let m = Module.add_module_alias loc key mname ~into:m in
(env, items, m)
| Module_type ((loc, id), vals) ->
Expand Down
20 changes: 19 additions & 1 deletion test/typing.ml
Original file line number Diff line number Diff line change
Expand Up @@ -793,6 +793,19 @@ let test_type_decl_open_before () =
let test_mtype_define () =
test "unit" "(module-type tt (type t) (def random (fun unit int)))"

let test_mtype_no_match () =
test_exn "Abstract type tt/t not implemented"
{|(module-type tt (type t))
(module (test tt)
(type a unit))|}

let test_mtype_no_match_alias () =
test_exn "Abstract type tt/t not implemented"
{|(module-type tt (type t))
(module test
(type a unit))
(module (other tt) test)|}

let case str test = test_case str `Quick test

(* Run it *)
Expand Down Expand Up @@ -1160,5 +1173,10 @@ let () =
case "not unique" test_type_decl_not_unique;
case "open before" test_type_decl_open_before;
] );
("module type", [ case "define" test_mtype_define ]);
( "module type",
[
case "define" test_mtype_define;
case "no match" test_mtype_no_match;
case "no match alias" test_mtype_no_match_alias;
] );
]

0 comments on commit bcf82aa

Please sign in to comment.