(**************************************************************************)
(*                                                                        *)
(*                                 OCaml                                  *)
(*                                                                        *)
(*             Xavier Leroy, projet Cristal, INRIA Rocquencourt           *)
(*                                                                        *)
(*   Copyright 1996 Institut National de Recherche en Informatique et     *)
(*     en Automatique.                                                    *)
(*                                                                        *)
(*   All rights reserved.  This file is distributed under the terms of    *)
(*   the GNU Lesser General Public License version 2.1, with the          *)
(*   special exception on linking described in the file LICENSE.          *)
(*                                                                        *)
(**************************************************************************)

(* Operations on core types *)

open Asttypes
open Types

exception Unify of (type_expr * type_expr) list
exception Tags of label * label
exception Subtype of (type_expr * type_expr) list * (type_expr * type_expr) list
exception Cannot_expand
exception Cannot_apply
exception Recursive_abbrev
exception Unification_recursive_abbrev of (type_expr * type_expr) list

val init_def : int -> unit
(* Set the initial variable level *)

val begin_def : unit -> unit
(* Raise the variable level by one at the beginning of a definition. *)

val end_def : unit -> unit
(* Lower the variable level by one at the end of a definition *)

val begin_class_def : unit -> unit
val raise_nongen_level : unit -> unit
val reset_global_level : unit -> unit
(* Reset the global level before typing an expression *)

val increase_global_level : unit -> int
val restore_global_level : int -> unit
(* This pair of functions is only used in Typetexp *)

type levels = {
  current_level: int;
  nongen_level: int;
  global_level: int;
  saved_level: (int * int) list;
}
val save_levels : unit -> levels
val set_levels : levels -> unit

val newty : type_desc -> type_expr
val newvar : ?name:string -> unit -> type_expr
val newvar2 : ?name:string -> int -> type_expr
(* Return a fresh variable *)

val new_global_var : ?name:string -> unit -> type_expr
(* Return a fresh variable, bound at toplevel
   (as type variables ['a] in type constraints). *)

val newobj : type_expr -> type_expr
val newconstr : Path.t -> type_expr list -> type_expr
val none : type_expr
(* A dummy type expression *)

val repr : type_expr -> type_expr
(* Return the canonical representative of a type. *)

val object_fields : type_expr -> type_expr
val flatten_fields :
  type_expr -> (string * field_kind * type_expr) list * type_expr

(* Transform a field type into a list of pairs label-type *)
(* The fields are sorted *)
val associate_fields :
  (string * field_kind * type_expr) list ->
  (string * field_kind * type_expr) list ->
  (string * field_kind * type_expr * field_kind * type_expr) list
  * (string * field_kind * type_expr) list
  * (string * field_kind * type_expr) list
val opened_object : type_expr -> bool
val close_object : type_expr -> unit
val row_variable : type_expr -> type_expr
(* Return the row variable of an open object type *)

val set_object_name :
  Ident.t -> type_expr -> type_expr list -> type_expr -> unit
val remove_object_name : type_expr -> unit
val hide_private_methods : type_expr -> unit
val find_cltype_for_path : Env.t -> Path.t -> type_declaration * type_expr
val lid_of_path : ?hash:string -> Path.t -> Longident.t

val sort_row_fields : (label * row_field) list -> (label * row_field) list
val merge_row_fields :
  (label * row_field) list ->
  (label * row_field) list ->
  (label * row_field) list
  * (label * row_field) list
  * (label * row_field * row_field) list
val filter_row_fields :
  bool -> (label * row_field) list -> (label * row_field) list

val generalize : type_expr -> unit
(* Generalize in-place the given type *)

val generalize_expansive : Env.t -> type_expr -> unit
(* Generalize the covariant part of a type, making
   contravariant branches non-generalizable *)

val generalize_global : type_expr -> unit
(* Generalize the structure of a type, lowering variables
   to !global_level *)

val generalize_structure : type_expr -> unit
(* Same, but variables are only lowered to !current_level *)

val correct_levels : type_expr -> type_expr
(* Returns a copy with decreasing levels *)

val limited_generalize : type_expr -> type_expr -> unit
(* Only generalize some part of the type
   Make the remaining of the type non-generalizable *)

val instance : ?partial:bool -> Env.t -> type_expr -> type_expr

(* Take an instance of a type scheme *)
(* partial=None  -> normal
   partial=false -> newvar() for non generic subterms
   partial=true  -> newty2 ty.level Tvar for non generic subterms *)
val instance_def : type_expr -> type_expr
(* use defaults *)

val generic_instance : Env.t -> type_expr -> type_expr
(* Same as instance, but new nodes at generic_level *)

val instance_list : Env.t -> type_expr list -> type_expr list
(* Take an instance of a list of type schemes *)

val instance_constructor :
  ?in_pattern:Env.t ref * int ->
  constructor_description ->
  type_expr list * type_expr
(* Same, for a constructor *)

val instance_parameterized_type :
  ?keep_names:bool -> type_expr list -> type_expr -> type_expr list * type_expr
val instance_parameterized_type_2 :
  type_expr list ->
  type_expr list ->
  type_expr ->
  type_expr list * type_expr list * type_expr
val instance_declaration : type_declaration -> type_declaration
val instance_class : type_expr list -> class_type -> type_expr list * class_type
val instance_poly :
  ?keep_names:bool ->
  bool ->
  type_expr list ->
  type_expr ->
  type_expr list * type_expr
(* Take an instance of a type scheme containing free univars *)

val instance_label :
  bool -> label_description -> type_expr list * type_expr * type_expr
(* Same, for a label *)

val apply : Env.t -> type_expr list -> type_expr -> type_expr list -> type_expr
(* [apply [p1...pN] t [a1...aN]] match the arguments [ai] to
   the parameters [pi] and returns the corresponding instance of
   [t]. Exception [Cannot_apply] is raised in case of failure. *)

val expand_head_once : Env.t -> type_expr -> type_expr
val expand_head : Env.t -> type_expr -> type_expr
val try_expand_once_opt : Env.t -> type_expr -> type_expr

val expand_head_opt : Env.t -> type_expr -> type_expr
(** The compiler's own version of [expand_head] necessary for type-based
    optimisations. *)

val full_expand : Env.t -> type_expr -> type_expr
val extract_concrete_typedecl :
  Env.t -> type_expr -> Path.t * Path.t * type_declaration
(* Return the original path of the types, and the first concrete
   type declaration found expanding it.
   Raise [Not_found] if none appears or not a type constructor. *)

val enforce_constraints : Env.t -> type_expr -> unit

val unify : Env.t -> type_expr -> type_expr -> unit
(* Unify the two types given. Raise [Unify] if not possible. *)

val unify_gadt :
  newtype_level:int -> Env.t ref -> type_expr -> type_expr -> unit
(* Unify the two types given and update the environment with the
   local constraints. Raise [Unify] if not possible. *)

val unify_var : Env.t -> type_expr -> type_expr -> unit
(* Same as [unify], but allow free univars when first type
   is a variable. *)

val with_passive_variants : ('a -> 'b) -> 'a -> 'b
(* Call [f] in passive_variants mode, for exhaustiveness check. *)

val filter_arrow : Env.t -> type_expr -> arg_label -> type_expr * type_expr
(* A special case of unification (with l:'a -> 'b). *)

val filter_method : Env.t -> string -> private_flag -> type_expr -> type_expr
(* A special case of unification (with {m : 'a; 'b}). *)

val check_filter_method : Env.t -> string -> private_flag -> type_expr -> unit
(* A special case of unification (with {m : 'a; 'b}), returning unit. *)

val occur_in : Env.t -> type_expr -> type_expr -> bool
val deep_occur : type_expr -> type_expr -> bool
val filter_self_method :
  Env.t ->
  string ->
  private_flag ->
  (Ident.t * type_expr) Meths.t ref ->
  type_expr ->
  Ident.t * type_expr
val moregeneral : Env.t -> bool -> type_expr -> type_expr -> bool
(* Check if the first type scheme is more general than the second. *)

val rigidify : type_expr -> type_expr list
(* "Rigidify" a type and return its type variable *)

val all_distinct_vars : Env.t -> type_expr list -> bool
(* Check those types are all distinct type variables *)

val matches : Env.t -> type_expr -> type_expr -> bool
(* Same as [moregeneral false], implemented using the two above
   functions and backtracking. Ignore levels *)

type class_match_failure =
  | CM_Virtual_class
  | CM_Parameter_arity_mismatch of int * int
  | CM_Type_parameter_mismatch of Env.t * (type_expr * type_expr) list
  | CM_Class_type_mismatch of Env.t * class_type * class_type
  | CM_Parameter_mismatch of Env.t * (type_expr * type_expr) list
  | CM_Val_type_mismatch of string * Env.t * (type_expr * type_expr) list
  | CM_Meth_type_mismatch of string * Env.t * (type_expr * type_expr) list
  | CM_Non_mutable_value of string
  | CM_Non_concrete_value of string
  | CM_Missing_value of string
  | CM_Missing_method of string
  | CM_Hide_public of string
  | CM_Hide_virtual of string * string
  | CM_Public_method of string
  | CM_Private_method of string
  | CM_Virtual_method of string
val match_class_types :
  ?trace:bool -> Env.t -> class_type -> class_type -> class_match_failure list
(* Check if the first class type is more general than the second. *)

val equal : Env.t -> bool -> type_expr list -> type_expr list -> bool
(* [equal env [x1...xn] tau [y1...yn] sigma]
   checks whether the parameterized types
   [/\x1.../\xn.tau] and [/\y1.../\yn.sigma] are equivalent. *)

val match_class_declarations :
  Env.t ->
  type_expr list ->
  class_type ->
  type_expr list ->
  class_type ->
  class_match_failure list
(* Check if the first class type is more general than the second. *)

val enlarge_type : Env.t -> type_expr -> type_expr * bool
(* Make a type larger, flag is true if some pruning had to be done *)

val subtype : Env.t -> type_expr -> type_expr -> unit -> unit
(* [subtype env t1 t2] checks that [t1] is a subtype of [t2].
   It accumulates the constraints the type variables must
   enforce and returns a function that enforces this
   constraints. *)

val nondep_type : Env.t -> Ident.t -> type_expr -> type_expr
(* Return a type equivalent to the given type but without
   references to the given module identifier. Raise [Not_found]
   if no such type exists. *)

val nondep_type_decl :
  Env.t -> Ident.t -> Ident.t -> bool -> type_declaration -> type_declaration
(* Same for type declarations. *)

val nondep_extension_constructor :
  Env.t -> Ident.t -> extension_constructor -> extension_constructor
(* Same for extension constructor *)

val nondep_class_declaration :
  Env.t -> Ident.t -> class_declaration -> class_declaration
(* Same for class declarations. *)

val nondep_cltype_declaration :
  Env.t -> Ident.t -> class_type_declaration -> class_type_declaration

(* Same for class type declarations. *)
(*val correct_abbrev: Env.t -> Path.t -> type_expr list -> type_expr -> unit*)
val cyclic_abbrev : Env.t -> Ident.t -> type_expr -> bool
val is_contractive : Env.t -> Path.t -> bool
val normalize_type : Env.t -> type_expr -> unit

val closed_schema : Env.t -> type_expr -> bool
(* Check whether the given type scheme contains no non-generic
   type variables *)

val free_variables : ?env:Env.t -> type_expr -> type_expr list
(* If env present, then check for incomplete definitions too *)

val closed_type_decl : type_declaration -> type_expr option
val closed_extension_constructor : extension_constructor -> type_expr option
type closed_class_failure =
  | CC_Method of type_expr * bool * string * type_expr
  | CC_Value of type_expr * bool * string * type_expr
val closed_class :
  type_expr list -> class_signature -> closed_class_failure option
(* Check whether all type variables are bound *)

val unalias : type_expr -> type_expr
val signature_of_class_type : class_type -> class_signature
val self_type : class_type -> type_expr
val class_type_arity : class_type -> int
val arity : type_expr -> int
(* Return the arity (as for curried functions) of the given type. *)

val collapse_conj_params : Env.t -> type_expr list -> unit
(* Collapse conjunctive types in class parameters *)

val get_current_level : unit -> int
val wrap_trace_gadt_instances : Env.t -> ('a -> 'b) -> 'a -> 'b
val reset_reified_var_counter : unit -> unit

val maybe_pointer_type : Env.t -> type_expr -> bool
(* True if type is possibly pointer, false if definitely not a pointer *)

(* Stubs *)
val package_subtype :
  (Env.t ->
  Path.t ->
  Longident.t list ->
  type_expr list ->
  Path.t ->
  Longident.t list ->
  type_expr list ->
  bool)
  ref

val variant_is_subtype :
  (Env.t -> Types.row_desc -> Types.type_expr -> bool) ref
