/
w_SchemeGenAndInst.mli
98 lines (87 loc) · 4.27 KB
/
w_SchemeGenAndInst.mli
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
(*
Copyright © 2011 MLstate
This file is part of Opa.
Opa is free software: you can redistribute it and/or modify it under the
terms of the GNU Affero General Public License, version 3, as published by
the Free Software Foundation.
Opa is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for
more details.
You should have received a copy of the GNU Affero General Public License
along with Opa. If not, see <http://www.gnu.org/licenses/>.
*)
(*
@author François Pessaux
*)
exception Private_type_not_opaque of W_Algebra.simple_type
(* ************************************************************************** *)
(** {b Descr}: Exception raised when during generalization, a non-generalizable
type variable was encountered although we were requested to forbid such
variables remaining.
This is used to prevent toplevel definition from having non-generalizable
variables (i.e. "weakly polymorphic" type variable, "_'a" variables à la
OCaml.
{b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
exception Non_generalizable_type_var of
(W_Algebra.simple_type * (** The global type hosting a non-generalizable type
variable. *)
W_Algebra.simple_type) (** The non-generalizable type variable. *)
(* ************************************************************************** *)
(** {b Descr}: Exception raised when during generalization, a non-generalizable
row variable was encountered although we were requested to forbid such
variables remaining.
This is used to prevent toplevel definition from having non-generalizable
variables (i.e. "weakly polymorphic" type variable, "_'a" variables à la
OCaml.
{b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
exception Non_generalizable_row_var of
(W_Algebra.simple_type * (** The global type hosting a non-generalizable row
variable. *)
W_Algebra.simple_type) (** The non-generalizable row variable embedded
in a type. *)
(* ************************************************************************** *)
(** {b Descr}: Exception raised when during generalization, a non-generalizable
column variable was encountered although we were requested to forbid such
variables remaining.
This is used to prevent toplevel definition from having non-generalizable
variables (i.e. "weakly polymorphic" type variable, "_'a" variables à la
OCaml.
{b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
exception Non_generalizable_column_var of
(W_Algebra.simple_type * (** The global type hosting a non-generalizable
column variable. *)
W_Algebra.simple_type) (** The non-generalizable column variable embedded
in a type. *)
val generalize:
forbid_non_gen_vars: bool ->W_Algebra.simple_type -> W_Algebra.types_scheme
val generalize2:
extra_variables:
(W_Algebra.simple_type list *
W_Algebra.row_type list *
W_Algebra.column_type list) -> W_Algebra.simple_type ->
W_Algebra.types_scheme
val trivial_scheme: W_Algebra.simple_type -> W_Algebra.types_scheme
val specialize: W_Algebra.types_scheme -> W_Algebra.simple_type
val specialize2:
deep: bool ->
W_Algebra.types_scheme ->
((W_Algebra.simple_type list *
W_Algebra.row_type list *
W_Algebra.column_type list) *
W_Algebra.simple_type)
val specialize_with_given_variables_mapping:
deep: bool ->
(W_Algebra.simple_type * W_Algebra.simple_type) list ->
(W_Algebra.row_variable * W_Algebra.row_variable) list ->
(W_Algebra.column_variable * W_Algebra.column_variable) list ->
W_Algebra.types_scheme -> W_Algebra.simple_type
val type_forall: W_Algebra.simple_type -> W_Algebra.simple_type
val get_type_forall_scheme:
W_Algebra.simple_type -> W_Algebra.types_scheme option
val automatically_instantiate_if_forall:
W_Algebra.simple_type ->
(W_Algebra.simple_type * (W_Algebra.types_scheme option))