Previous  Up  Next

Module Logtk.Type (.ml)

module Type: LogtkType

Main LogtkType representation

LogtkTypes are represented using LogtkScopedTerm, with kind LogtkType. 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 LogtkTypeInference for inferring types from terms and formulas, and LogtkSignature to associate types with symbols.

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

exception Error of string
Generic error on types.

Main signature


type symbol = LogtkSymbol.t 
type t = private LogtkScopedTerm.t
LogtkType is a subtype of the general structure LogtkScopedTerm.t, with explicit conversion
type ty = t 
type view = private
| Var of int (*
LogtkType variable
*)
| BVar of int (*
Bound variable (De Bruijn index)
*)
| App of symbol * t list (*
parametrized type
*)
| Fun of t * t (*
Function type (left to right)
*)
| Record of (string * t) list * t option (*
Record type
*)
| Forall of t (*
explicit quantification using De Bruijn index
*) 
val view : t -> view
LogtkType-centric view of the head of this type.
Raises Invalid_argument if the argument is not a type.
val kind : LogtkScopedTerm.Kind.t
include LogtkInterfaces.HASH
include LogtkInterfaces.ORD
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
Pseudo-type of types
val var : int -> t
Build a type variable.
Raises LogtkScopedTerm.IllFormedTerm if the integer is negative
val app : symbol -> t list -> t
Parametrized type
val const : symbol -> t
Constant sort
val arrow : t -> t -> t
arrow l r is the type l -> r.
val arrow_list : t list -> t -> t
n-ary version of LogtkType.arrow
val forall : t list -> t -> t
forall vars ty quantifies ty over vars. If vars is the empty list, returns ty.
Raises Invalid_argument if some element of vars is not a variable
val record : (string * t) list -> rest:t option -> t
Record type, with an optional extension
val __forall : t -> t
not documented.
val __bvar : int -> t
not documented.
val (@@) : symbol -> t list -> t
s @@ args applies the sort s to arguments args.
val (<==) : t -> t list -> t
General function type. x <== l is the same as x if l is empty. Invariant: the return type is never a function type.
val (<=.) : t -> t -> t
Unary function type. x <=. y is the same as x <== [y].
val multiset : t -> t
LogtkType of multiset
val of_term : LogtkScopedTerm.t -> t option
Conversion from a term, if structure matches
val of_term_exn : LogtkScopedTerm.t -> t
Same as of_term, but without option
Raises Invalid_argument if the term is not a type
val is_type : LogtkScopedTerm.t -> bool
Is the term a representation of a type?

Containers


module Set: Sequence.Set.S  with type elt = t
module Map: Sequence.Map.S  with type key = t
module Tbl: Hashtbl.S  with type key = t
module Seq: sig .. end

LogtkUtils


val vars_set : Set.t -> t -> Set.t
Add the free variables to the given set
val vars : t -> t list
List of free variables (Var)
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
LogtkTypes expected as function argument by ty. The length of the list expected_args ty is the same as snd (arity ty).
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_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
val apply : t -> t -> t
Given a function/forall type, and an argument, return the type that results from applying the function/forall to the arguments. No unification is done, types must check exactly.
Raises Error if the types do not match
val apply_list : t -> t list -> t
List version of LogtkType.apply
Raises Error if the types do not match

IO


include LogtkInterfaces.PRINT_DE_BRUIJN
include LogtkInterfaces.PRINT
val pp_surrounded : Buffer.t -> t -> unit

TPTP

specific printer and types
module TPTP: sig .. end

Conversions


module Conv: sig .. end

Misc


val fresh_var : unit -> t
Fresh var, with negative index