<commit_before>(** Type checking of the metalanguage. *)

type meta

type param

module MetaOrd : sig
  type t = meta

  val compare : t -> t -> int
end

module MetaSet : Set.S with type elt = meta

type ty =
  | Jdg
  | String
  | Meta of meta
  | Param of param
  | Prod of ty list
  | Arrow of ty * ty
  | Handler of ty * ty
  | App of Name.ident * Syntax.level * ty list
  | Ref of ty

(** The unit type encoded as an empty product. *)
val unit_ty : ty

(** Generate a fresh meta variable *)
val fresh_meta : unit -> meta

(** Generate a fresh type parameter *)
val fresh_param : unit -> param

(** Generate a fresh meta variable as a type *)
val fresh_type : unit -> ty

(** The metavariables are generalised in the following values. *)
type 'a forall = param list * 'a

type ty_schema = ty forall

type constructor = Name.constructor * ty list

type ty_def =
  | Alias of ty forall
  | Sum of constructor list forall

(** Make a schema from a type without generalizing anything. *)
val ungeneralized_schema : ty -> ty_schema


(** The errors reported by type inference. *)
type error =
  | InvalidApplication of ty * ty * ty
  | TypeMismatch of ty * ty
  | UnsolvedApp of ty * ty * ty
  | HandlerExpected of ty
  | RefExpected of ty
  | UnknownExternal of string
  | ValueRestriction
  | Ungeneralizable of param list * ty

exception Error of error Location.located

val error : loc:Location.t -> error -> 'a

type print_env

val fresh_penv : unit -> print_env

val print_ty : penv:print_env -> ?max_level:Level.t -> ty -> Format.formatter -> unit

val print_ty_schema :  penv:print_env -> ?max_level:Level.t -> ty_schema -> Format.formatter -> unit

val print_error : error -> Format.formatter -> unit


val occurs : meta -> ty -> bool

val occuring : ty -> MetaSet.t

val occuring_schema : ty_schema -> MetaSet.t

(** Instantiate the type parameters with the given types. *)
val instantiate : (param * ty) list -> ty -> ty

(** Do any of the given parameters appear in the given type? *)
val params_occur : param list -> ty -> bool<commit_msg>comment mlty.mli<commit_after>(** ML types and basic operations on them. *)

(** The type of metavariables. *)
type meta

(** The type of type parameters. *)
type param

(** Metavariables are an ordered type. Used for [Map.Make]. *)
module MetaOrd : sig
  type t = meta

  val compare : t -> t -> int
end

(** Sets of metavariables. *)
module MetaSet : Set.S with type elt = meta

(** The type of ML types. *)
type ty =
  | Jdg
  | String
  | Meta of meta
  | Param of param
  | Prod of ty list
  | Arrow of ty * ty
  | Handler of ty * ty
  | App of Name.ident * Syntax.level * ty list
  | Ref of ty

(** The unit type encoded as an empty product. *)
val unit_ty : ty

(** Generate a fresh metavariable *)
val fresh_meta : unit -> meta

(** Generate a fresh type parameter *)
val fresh_param : unit -> param

(** Generate a fresh metavariable as a type *)
val fresh_type : unit -> ty

(** The parameters are bound in the following values. *)
type 'a forall = param list * 'a

(** The type of type schemas, i.e. polymorphic types. *)
type ty_schema = ty forall

(** A constructor name and the expected types of its arguments. *)
type constructor = Name.constructor * ty list

(** The type of type definitions. *)
type ty_def =
  | Alias of ty forall
  | Sum of constructor list forall

(** Make a schema from a type without generalizing anything. *)
val ungeneralized_schema : ty -> ty_schema


(** The errors reported by type inference. *)
type error =
  | InvalidApplication of ty * ty * ty
  | TypeMismatch of ty * ty
  | UnsolvedApp of ty * ty * ty
  | HandlerExpected of ty
  | RefExpected of ty
  | UnknownExternal of string
  | ValueRestriction
  | Ungeneralizable of param list * ty

exception Error of error Location.located

(** Convenience function to raise an error. *)
val error : loc:Location.t -> error -> 'a

(** The type of printing environments, which ensure readable printing of metavariables and type parameters. Mutable. *)
type print_env

(** Get a fresh printing environment. *)
val fresh_penv : unit -> print_env

(** Print a type according to the given printing environment, which may be modified. *)
val print_ty : penv:print_env -> ?max_level:Level.t -> ty -> Format.formatter -> unit

(** Print a type schema according to the given printing environment, which may be modified. *)
val print_ty_schema :  penv:print_env -> ?max_level:Level.t -> ty_schema -> Format.formatter -> unit

(** Print a typing error according to the given printing environment, which may be modified. *)
val print_error : error -> Format.formatter -> unit

(** Does the given metavariable occur in the given type? *)
val occurs : meta -> ty -> bool

(** Get the set of metavariables which occur in the given type. *)
val occuring : ty -> MetaSet.t

(** Get the set of metavariables which occur in the given type schema. *)
val occuring_schema : ty_schema -> MetaSet.t

(** Instantiate the type parameters with the associated types in the given type. *)
val instantiate : (param * ty) list -> ty -> ty

(** Do any of the given parameters appear in the given type? *)
val params_occur : param list -> ty -> bool

{'fraction_non_alphanumeric': 0.0986051917861294, 'fraction_numerical': 0.0, 'mean_word_length': 3.364327979712595, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 57, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3667505', 'n_tokens_mistral': 1585, 'n_tokens_neox': 1507, 'n_words': 681}