Skip to content

Commit

Permalink
Typing for parameterised libraries (ocaml-flambda#1726)
Browse files Browse the repository at this point in the history
Typechecking of references to parameterised libraries, with or without arguments. Currently such references can't actually be compiled to working code because we don't have the `-instantiate` pass, but this contains all the typechecking logic to make sure that, for instance, a module `A` can't refer to a parameterised module `B` unless `A` takes all the parameters that `B` does (the subset rule) or the reference includes an argument for each missing parameter.
  • Loading branch information
lukemaurer authored Oct 28, 2024
1 parent 9a7cc9f commit 9768a53
Show file tree
Hide file tree
Showing 66 changed files with 1,514 additions and 175 deletions.
6 changes: 3 additions & 3 deletions bytecomp/bytelink.ml
Original file line number Diff line number Diff line change
Expand Up @@ -186,11 +186,11 @@ module Consistbl = Consistbl.Make (CU.Name) (Import_info.Intf.Nonalias.Kind)

let crc_interfaces = Consistbl.create ()
let interfaces = ref ([] : CU.Name.t list)
let implementations_defined = ref ([] : (CU.Name.t * string) list)
let implementations_defined = ref ([] : (CU.t * string) list)

let check_consistency file_name cu =
begin try
let source = List.assoc (CU.name cu.cu_name) !implementations_defined in
let source = List.assoc cu.cu_name !implementations_defined in
raise (Error (Multiple_definition(cu.cu_name, file_name, source)));
with Not_found -> ()
end;
Expand All @@ -213,7 +213,7 @@ let check_consistency file_name cu =
raise(Error(Inconsistent_import(name, user, auth)))
end;
implementations_defined :=
(CU.name cu.cu_name, file_name) :: !implementations_defined
(cu.cu_name, file_name) :: !implementations_defined

let extract_crc_interfaces () =
Consistbl.extract !interfaces crc_interfaces
Expand Down
1 change: 1 addition & 0 deletions dune
Original file line number Diff line number Diff line change
Expand Up @@ -199,6 +199,7 @@
mode
jkind_types
jkind_intf
signature_with_global_bindings
typedtree
printtyped
ctype
Expand Down
9 changes: 7 additions & 2 deletions file_formats/cmi_format.ml
Original file line number Diff line number Diff line change
Expand Up @@ -63,15 +63,17 @@ type flags = pers_flags list
type header = {
header_name : Compilation_unit.Name.t;
header_kind : kind;
header_globals : Global_module.t array;
header_sign : Serialized.signature;
header_params : Global_module.Name.t list;
header_params : Global_module.t list;
}

type 'sg cmi_infos_generic = {
cmi_name : Compilation_unit.Name.t;
cmi_kind : kind;
cmi_globals : Global_module.t array;
cmi_sign : 'sg;
cmi_params : Global_module.Name.t list;
cmi_params : Global_module.t list;
cmi_crcs : crcs;
cmi_flags : flags;
}
Expand Down Expand Up @@ -125,6 +127,7 @@ let input_cmi_lazy ic =
let {
header_name = name;
header_kind = kind;
header_globals = globals;
header_sign = sign;
header_params = params;
} = (input_value ic : header) in
Expand All @@ -134,6 +137,7 @@ let input_cmi_lazy ic =
{
cmi_name = name;
cmi_kind = kind;
cmi_globals = globals;
cmi_sign = deserialize data sign;
cmi_params = params;
cmi_crcs = crcs;
Expand Down Expand Up @@ -192,6 +196,7 @@ let output_cmi filename oc cmi =
{
header_name = cmi.cmi_name;
header_kind = cmi.cmi_kind;
header_globals = cmi.cmi_globals;
header_sign = sign;
header_params = cmi.cmi_params;
};
Expand Down
3 changes: 2 additions & 1 deletion file_formats/cmi_format.mli
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,9 @@ type kind =
type 'sg cmi_infos_generic = {
cmi_name : Compilation_unit.Name.t;
cmi_kind : kind;
cmi_globals : Global_module.t array;
cmi_sign : 'sg;
cmi_params : Global_module.Name.t list;
cmi_params : Global_module.t list; (* CR lmaurer: Should be [Parameter_name.t list] *)
cmi_crcs : Import_info.t array;
cmi_flags : pers_flags list;
}
Expand Down
1 change: 1 addition & 0 deletions otherlibs/dynlink/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -152,6 +152,7 @@ COMPILERLIBS_SOURCES=\
typing/typedtree.ml \
typing/btype.ml \
typing/subst.ml \
typing/signature_with_global_bindings.ml \
typing/predef.ml \
typing/datarepr.ml \
file_formats/cmi_format.ml \
Expand Down
7 changes: 7 additions & 0 deletions otherlibs/dynlink/dune
Original file line number Diff line number Diff line change
Expand Up @@ -127,6 +127,7 @@
lazy_backtrack
zero_alloc_utils
subst
signature_with_global_bindings
predef
datarepr
unit_info
Expand Down Expand Up @@ -300,6 +301,8 @@

(copy_files ../../typing/subst.ml)

(copy_files ../../typing/signature_with_global_bindings.ml)

(copy_files ../../typing/predef.ml)

(copy_files ../../typing/datarepr.ml)
Expand Down Expand Up @@ -456,6 +459,8 @@

(copy_files ../../typing/subst.mli)

(copy_files ../../typing/signature_with_global_bindings.mli)

(copy_files ../../typing/predef.mli)

(copy_files ../../typing/datarepr.mli)
Expand Down Expand Up @@ -606,6 +611,7 @@
.dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Jkind.cmo
.dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Btype.cmo
.dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Subst.cmo
.dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Signature_with_global_bindings.cmo
.dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Bytesections.cmo
.dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Cmi_format.cmo
.dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Debuginfo.cmo
Expand Down Expand Up @@ -703,6 +709,7 @@
.dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Jkind.cmx
.dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Btype.cmx
.dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Subst.cmx
.dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Signature_with_global_bindings.cmx
.dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Bytesections.cmx
.dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Cmi_format.cmx
.dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Debuginfo.cmx
Expand Down
4 changes: 3 additions & 1 deletion testsuite/tests/packs/inconsistent/main.compilers.reference
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
File "main.ml", line 1:
File "main.ml", line 28, characters 11-30:
28 | module _ = Use_member_directly
^^^^^^^^^^^^^^^^^^^
Error: The file subdir/use_member_directly.cmi
is imported both as "Pack.Member" and as "Member".
8 changes: 4 additions & 4 deletions testsuite/tests/parsetree/source_jane_street.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1005,10 +1005,10 @@ module Value1 : sig end
module Value2 : sig end -> sig end -> sig end
module Name2_1 : sig end
module Name2_1 : sig end
>> Fatal error: Unimplemented: instance identifier
Base[Name1:Value1][Name2:Value2[Name2_1:Value2_1]]
Uncaught exception: Misc.Fatal_error
Line 9, characters 11-64:
9 | module _ = Base(Name1)(Value1)(Name2)(Value2(Name2_1)(Value2_1)) [@jane.non_erasable.instances]
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module "Base[Name1:Value1][Name2:Value2[Name2_1:Value2_1]]"
|}](*********)
(* modes *)

Expand Down
2 changes: 2 additions & 0 deletions testsuite/tests/self-contained-toplevel/main.ml
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ let () =
cmi_kind;
cmi_params;
cmi_sign;
cmi_globals;
cmi_crcs;
cmi_flags
} =
Expand All @@ -41,6 +42,7 @@ let () =
cmi_kind;
cmi_params;
cmi_sign = Subst.Lazy.of_signature cmi_sign;
cmi_globals;
cmi_crcs;
cmi_flags
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
module Monoid_utils_of_banana =
Monoid_utils(Banana)(List_monoid) [@jane.non_erasable.instances]
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
File "bad_instance_arg_name_not_found.ml", line 2, characters 2-35:
2 | Monoid_utils(Banana)(List_monoid) [@jane.non_erasable.instances]
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The module "Monoid_utils" has no parameter "Banana".
Hint: Parameters for "Monoid_utils": "Monoid"
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
module Monoid_utils_of_int =
Monoid_utils(Monoid)(Monoid_utils(Monoid)(List_monoid)) [@jane.non_erasable.instances]
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
File "bad_instance_arg_value_not_arg.ml", line 2, characters 2-57:
2 | Monoid_utils(Monoid)(Monoid_utils(Monoid)(List_monoid)) [@jane.non_erasable.instances]
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The module "Monoid_utils[Monoid:List_monoid]"
cannot be used as an argument for parameter "Monoid".
Hint: Compile "monoid_utils.cmi" with "-as-argument-for Monoid".
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
module Monoid_utils_of_int =
Monoid_utils(Monoid)(Banana) [@jane.non_erasable.instances]
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
File "bad_instance_arg_value_not_found.ml", line 2, characters 2-30:
2 | Monoid_utils(Monoid)(Banana) [@jane.non_erasable.instances]
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module "Banana" in instance "Monoid_utils[Monoid:Banana]"
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
module Category_utils_of_list_monoid =
Category_utils(Category)(List_monoid) [@jane.non_erasable.instances]
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
File "bad_instance_arg_value_wrong_type.ml", line 2, characters 2-39:
2 | Category_utils(Category)(List_monoid) [@jane.non_erasable.instances]
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The module "List_monoid"
is used as an argument for the parameter "Category" but "List_monoid"
is an argument for "Monoid".
Hint: "list_monoid.cmi" was compiled with "-as-argument-for Category".
5 changes: 5 additions & 0 deletions testsuite/tests/templates/basic/bad_instance_wrong_mode.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
let (f @ portable) () =
let module Monoid_utils_of_list_monoid =
Monoid_utils(Monoid)(List_monoid) [@jane.non_erasable.instances]
in
()
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
File "bad_instance_wrong_mode.ml", line 3, characters 4-37:
3 | Monoid_utils(Monoid)(List_monoid) [@jane.non_erasable.instances]
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Modules are nonportable, so cannot be used inside a function that is portable.
9 changes: 6 additions & 3 deletions testsuite/tests/templates/basic/bad_param_not_param.reference
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
File "bad_param_not_param.mli", line 1:
Error: The module "Widget" is specified as a parameter, but "widget.cmi"
was not compiled with -as-parameter.
File "bad_param_not_param.mli", line 19, characters 17-25:
19 | val frobnicate : Widget.t -> Widget.t
^^^^^^^^
Error: The module "Widget"
is a parameter but is not declared as such for the current unit.
Hint: Compile the current unit with "-parameter Widget".
9 changes: 6 additions & 3 deletions testsuite/tests/templates/basic/bad_ref_direct.reference
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
File "bad_ref_direct.ml", line 1:
Error: The file "monoid.cmi" contains the interface of a parameter.
"Monoid" is not declared as a parameter for the current unit (-parameter "Monoid").
File "bad_ref_direct.ml", line 3, characters 12-21:
3 | let empty = Monoid.id
^^^^^^^^^
Error: The file "monoid.cmi" contains the interface of a parameter. "Monoid"
is not declared as a parameter for the current unit.
Hint: Compile the current unit with "-parameter Monoid".
7 changes: 7 additions & 0 deletions testsuite/tests/templates/basic/bad_ref_direct_imported.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
(* [Monoid] is not a parameter of this, but it _is_ imported because it's used
as a parameter *)

module Monoid_utils_of_semigroup =
Monoid_utils(Monoid)(Monoid_of_semigroup) [@jane.non_erasable.instances]

let empty = Monoid.empty
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
File "bad_ref_direct_imported.ml", line 7, characters 12-24:
7 | let empty = Monoid.empty
^^^^^^^^^^^^
Error: The file "monoid.cmi" contains the interface of a parameter. "Monoid"
is not declared as a parameter for the current unit.
Hint: Compile the current unit with "-parameter Monoid".
6 changes: 4 additions & 2 deletions testsuite/tests/templates/basic/bad_ref_indirect.reference
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
File "bad_ref_indirect.ml", line 1:
File "bad_ref_indirect.ml", line 2, characters 13-32:
2 | let concat = Monoid_utils.concat
^^^^^^^^^^^^^^^^^^^
Error: The module "Monoid_utils" is not accessible because it takes "Monoid"
as a parameter and the current unit does not.
Hint: Pass `-parameter "Monoid"` to add "Monoid" as a parameter
Hint: Pass "-parameter Monoid" to add "Monoid" as a parameter
of the current unit.
1 change: 1 addition & 0 deletions testsuite/tests/templates/basic/category.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
include Category_intf.S
1 change: 1 addition & 0 deletions testsuite/tests/templates/basic/category_b.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
include Category_intf.S
1 change: 1 addition & 0 deletions testsuite/tests/templates/basic/category_b_of_category.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
include Category
1 change: 1 addition & 0 deletions testsuite/tests/templates/basic/category_b_of_category.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
include Category_intf.S with type ('a, 'b) t = ('a, 'b) Category.t
6 changes: 6 additions & 0 deletions testsuite/tests/templates/basic/category_intf.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
module type S = sig
type ('a, 'b) t

val id : ('a, 'a) t
val compose : first:('a, 'b) t -> second:('b, 'c) t -> ('a, 'c) t
end
6 changes: 6 additions & 0 deletions testsuite/tests/templates/basic/category_of_monoid.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
type ('a, 'b) t = Monoid.t

let id = Monoid.empty
let compose ~first ~second = Monoid.append first second

let as_unit t = t
8 changes: 8 additions & 0 deletions testsuite/tests/templates/basic/category_of_monoid.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
type ('a, 'b) t = Monoid.t

val id : ('a, 'a) t
val compose : first:('a, 'b) t -> second:('b, 'c) t -> ('a, 'c) t

(* Demonstrate that we can have extra functions beyond what's required by the
.mli for the parameter type *)
val as_unit : (_, _) t -> (unit, unit) t
5 changes: 5 additions & 0 deletions testsuite/tests/templates/basic/category_utils.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
let rec concat : type a b. (a, b) Chain.t -> (a, b) Category.t =
fun chain ->
match chain with
| [] -> Category.id
| a_to_b :: b_to_c -> Category.compose ~first:a_to_b ~second:(concat b_to_c)
1 change: 1 addition & 0 deletions testsuite/tests/templates/basic/category_utils.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
val concat : ('a, 'b) Chain.t -> ('a, 'b) Category.t
3 changes: 3 additions & 0 deletions testsuite/tests/templates/basic/chain.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
type (_, _) t =
| [] : ('a, 'a) t
| (::) : ('a, 'b) Category.t * ('b, 'c) t -> ('a, 'c) t
3 changes: 3 additions & 0 deletions testsuite/tests/templates/basic/chain.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
type (_, _) t =
| [] : ('a, 'a) t
| (::) : ('a, 'b) Category.t * ('b, 'c) t -> ('a, 'c) t
7 changes: 7 additions & 0 deletions testsuite/tests/templates/basic/import.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
module Chain_of_semigroup =
Chain(Category)(Category_of_monoid(Monoid)(Monoid_of_semigroup))
[@jane.non_erasable.instances]

module Chain_of_lists =
Chain(Category)(Category_of_monoid(Monoid)(List_monoid))
[@jane.non_erasable.instances]
15 changes: 15 additions & 0 deletions testsuite/tests/templates/basic/import_multi_arg.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
module Category_of_semigroup_and_lists =
Product_category
(Category)(Category_of_monoid(Monoid)(Monoid_of_semigroup))
(Category_b)(Category_b_of_category
(Category)(Category_of_monoid(Monoid)(List_monoid)))
[@jane.non_erasable.instances]

module Chain_of_semigroup_and_lists =
Chain
(Category)
(Product_category
(Category)(Category_of_monoid(Monoid)(Monoid_of_semigroup))
(Category_b)(Category_b_of_category
(Category)(Category_of_monoid(Monoid)(List_monoid))))
[@jane.non_erasable.instances]
1 change: 1 addition & 0 deletions testsuite/tests/templates/basic/list_element.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
type t
4 changes: 4 additions & 0 deletions testsuite/tests/templates/basic/list_monoid.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
type t = List_element.t list

let empty = []
let append = List.append
4 changes: 4 additions & 0 deletions testsuite/tests/templates/basic/list_monoid.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
type t = List_element.t list

val empty : t
val append : t -> t -> t
27 changes: 27 additions & 0 deletions testsuite/tests/templates/basic/main.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
module Monoid_utils_of_semigroup =
Monoid_utils(Monoid)(Monoid_of_semigroup) [@jane.non_erasable.instances]

module Category_utils_of_semigroup =
Category_utils(Category)(Category_of_monoid(Monoid)(Monoid_of_semigroup))
[@jane.non_erasable.instances]

module Category_utils_of_list =
Category_utils(Category)(Category_of_monoid(Monoid)(List_monoid))
[@jane.non_erasable.instances]

module Category_of_list_monoid =
Category_of_monoid(Monoid)(List_monoid)
[@jane.non_erasable.instances]

let concat_semi : Monoid_utils_of_semigroup.ts -> Monoid_of_semigroup.t =
Monoid_utils_of_semigroup.concat

let concat_chain_semi = Category_utils_of_semigroup.concat

let append3_semi a b c = Category_utils_of_semigroup.concat [ a; b; c ]

let concat_lists = List.concat

let concat_chain_lists = Category_utils_of_list.concat

let append3_lists a b c = concat_chain_lists [ a; b; c ]
19 changes: 19 additions & 0 deletions testsuite/tests/templates/basic/main.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
open Import

val append3_semi
: Semigroup.t option
-> Semigroup.t option
-> Semigroup.t option
-> Semigroup.t option

val concat_semi : Semigroup.t option list -> Monoid_of_semigroup.t

val concat_chain_semi
: (unit, unit) Chain_of_semigroup.t -> Monoid_of_semigroup.t

val append3_lists
: List_monoid.t -> List_monoid.t -> List_monoid.t -> List_monoid.t

val concat_lists : List_monoid.t list -> List_element.t list

val concat_chain_lists : (_, _) Chain_of_lists.t -> List_element.t list
Loading

0 comments on commit 9768a53

Please sign in to comment.