Previous  Up  Next

Module Type

module Type: sig .. end

Types



Main Type representation

Types are represented using InnerTerm, with kind Type. Therefore, they are hashconsed and scoped.

Common representation of types, including higher-order and polymorphic types. All type variables are assumed to be universally quantified in the outermost possible scope (outside any other quantifier).

See TypeInference for inferring types from terms and formulas, and Signature to associate types with symbols.

TODO: think of a good way of representating AC operators (+, ...)

type t = private InnerTerm.t
Type is a subtype of the term structure (itself a subtype of InnerTerm.t), with explicit conversion
type ty = t 
type builtin =
| TType
| Prop
| Term
| Rat
| Int 
val pp_builtin : builtin CCFormat.printer
val builtin_conv : builtin -> Builtin.t
type view = private
| Builtin of builtin
| Var of t HVar.t
| DB of int
| App of ID.t * t list (*
parametrized type
*)
| Fun of t list * t (*
Function type (left to right, no left-nesting)
*)
| Forall of t (*
explicit quantification using De Bruijn index
*) 
val view : t -> view
Type-centric view of the head of this type.
Raises Assert_failure if the argument is not a type
include Interfaces.HASH
include Interfaces.ORD
val is_tType : t -> bool
val is_var : t -> bool
val is_bvar : t -> bool
val is_app : t -> bool
val is_fun : t -> bool
val is_forall : t -> bool

Constructors


val tType : t
val prop : t
val term : t
val int : t
val rat : t
val var : t HVar.t -> t
val var_of_int : int -> t
Build a type variable.
val app : ID.t -> t list -> t
Parametrized type
val builtin : builtin -> t
val const : ID.t -> t
Constant sort
val arrow : t list -> t -> t
arrow l r is the type l -> r.
val forall : t -> t
Quantify over one type variable. Careful with the De Bruijn indices!
val forall_n : int -> t -> t
Quantify over n type variable. Careful with the De Bruijn indices!
val bvar : int -> t
bound variable
val (==>) : t list -> t -> t
General function type. l ==> x is the same as x if l is empty. Invariant: the return type is never a function type.
val of_term_unsafe : InnerTerm.t -> t
NOTE: this can break the invariants and make Type.view fail. Only use with caution.
val of_terms_unsafe : InnerTerm.t list -> t list
val cast_var_unsafe : InnerTerm.t HVar.t -> t HVar.t

Containers


module Set: CCSet.S  with type elt = t
module Map: CCMap.S  with type key = t
module Tbl: CCHashtbl.S  with type key = t
module Seq: sig .. end

Utils


module VarSet: CCSet.S  with type elt = t HVar.t
module VarMap: CCMap.S  with type key = t HVar.t
module VarTbl: CCHashtbl.S  with type key = t HVar.t
val vars_set : VarSet.t -> t -> VarSet.t
Add the free variables to the given set
val vars : t -> t HVar.t list
List of free variables
val close_forall : t -> t
bind free variables
type arity_result =
| Arity of int * int
| NoArity 
val arity : t -> arity_result
Number of arguments the type expects. If arity ty returns Arity (a, b) that means that it expects a arguments to be used as arguments of Forall, and b arguments to be used for function application. If it returns NoArity then the arity is unknown (variable)
val expected_args : t -> t list
Types expected as function argument by ty. The length of the list expected_args ty is the same as snd (arity ty).
val expected_ty_vars : t -> int
Number of type parameters expected. 0 for monomorphic types.
val is_ground : t -> bool
Is the type ground? (means that no Var not BVar occurs in it)
val size : t -> int
Size of type, in number of "nodes"
val depth : t -> int
Depth of the type (length of the longest path to some leaf)
Since 0.5.3
val open_poly_fun : t -> int * t list * t
open_poly_fun ty "unrolls" polymorphic function arrows from the left, so that open_fun (forall a b. f a -> (g b -> (c -> d))) returns 2; [f a;g b;c], d.
Returns the return type, the number of type variables, and the list of all its arguments
val open_fun : t -> t list * t
open_fun ty "unrolls" function arrows from the left, so that open_fun (a -> (b -> (c -> d))) returns [a;b;c], d.
Returns the return type and the list of all its arguments
exception ApplyError of string
Error raised when Type.apply fails
val apply : t -> t list -> t
Given a function/forall type, and arguments, return the type that results from applying the function/forall to the arguments. No unification is done, types must check exactly.
Raises ApplyError if the types do not match
val apply1 : t -> t -> t
apply1 a b is short for apply a [b].
val apply_unsafe : t -> InnerTerm.t list -> t
Similar to Type.apply, but assumes its arguments are well-formed types without more ado.
Raises

IO


include Interfaces.PRINT_DE_BRUIJN
include Interfaces.PRINT
val pp_surrounded : t CCFormat.printer
val pp_typed_var : t HVar.t CCFormat.printer

TPTP

specific printer and types
module TPTP: sig .. end

Conversions


module Conv: sig .. end