Module Shared_ast.Type

type t = Shared_ast__.Definitions.naked_typ Catala_utils.Mark.pos
type var = Shared_ast__.Definitions.naked_typ Bindlib.var
val format : Stdlib.Format.formatter -> t -> unit
module Map : Catala_utils.Map.S with type key = t
val equal : t -> t -> bool
val equal_list : t list -> t list -> bool
val compare : t -> t -> int
val map : (t -> t Bindlib.box) -> t -> t Bindlib.box

Shallow mapping on types

val shallow_fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
val hash : strip:Catala_utils.Uid.Module.t option -> t -> Catala_utils.Hash.t

The strip argument strips the given leading path components in included identifiers before hashing

val unifiable : t -> t -> bool
val unifiable_list : t list -> t list -> bool

Similar to equal, but allows TForAll holes

val is_arrow : t -> bool

Matches both direct arrow types and quantified arrow types

val arrow_return : t -> t

Returns the last member in nested TArrow types

val has_arrow : Shared_ast__.Definitions.decl_ctx -> t -> bool

Checks in depth, contrary to is_arrow. Fails (with Invalid_argument) on TForAll and TClosureEnv

Handling of variables

module Var : sig ... end
val free_vars : t -> Var.Set.t
val free_vars_pos : t -> Catala_utils.Pos.t Var.Map.t

Only the first position where the variable appeared is kept

val rebox : t -> t Bindlib.box
val unquantify : t -> t

Removes the outermost quantifiers from the given type, if any. The returned type is guaranteed to not have the form TForAll _ and may contain free variables

val unbind : t -> Var.t list * t

Recursively unbinds nested quantifiers and merges their variables (this is similar to unquantify, but also returns the bound variables)

val forall : Var.t list -> t Bindlib.box -> Catala_utils.Pos.t -> t

The opposite of unbind: constructs a TForAll quantified type

val fresh_var : Catala_utils.Pos.t -> t
val error : Catala_utils.Pos.t -> t
val any : Catala_utils.Pos.t -> t

deprecated, TODO replace with fresh_var

val universal : Catala_utils.Pos.t -> t
val is_universal : t -> bool
val fully_known : t -> bool

true iff the type doesn't contain any unknowns (free variables or quantified types outside of arrows)