module Type: LogtkType
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
typesymbol =
LogtkSymbol.t
typet = private
LogtkScopedTerm.t
typety =
t
type
view = private
| |
Var of |
(* |
LogtkType variable
| *) |
| |
BVar of |
(* |
Bound variable (De Bruijn index)
| *) |
| |
App of |
(* |
parametrized type
| *) |
| |
Fun of |
(* |
Function type (left to right)
| *) |
| |
Record of |
(* |
Record type
| *) |
| |
Forall of |
(* |
explicit quantification using De Bruijn index
| *) |
val view : t -> view
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
val tType : t
val var : int -> t
LogtkScopedTerm.IllFormedTerm
if the integer is negativeval app : symbol -> t list -> t
val const : symbol -> t
val arrow : t -> t -> t
arrow l r
is the type l -> r
.val arrow_list : t list -> t -> t
LogtkType.arrow
val forall : t list -> t -> t
forall vars ty
quantifies ty
over vars
.
If vars
is the empty list, returns ty
.Invalid_argument
if some element of vars
is not a variableval record : (string * t) list -> rest:t option -> t
val __forall : t -> t
val __bvar : int -> t
val (@@) : symbol -> t list -> t
s @@ args
applies the sort s
to arguments args
.val (<==) : t -> t list -> t
x <== l
is the same as x
if l
is empty. Invariant: the return type is never a function type.val (<=.) : t -> t -> t
x <=. y
is the same as x <== [y]
.val multiset : t -> t
val of_term : LogtkScopedTerm.t -> t option
val of_term_exn : LogtkScopedTerm.t -> t
of_term
, but without optionInvalid_argument
if the term is not a typeval is_type : LogtkScopedTerm.t -> bool
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
val vars_set : Set.t -> t -> Set.t
val vars : t -> t list
Var
)val close_forall : t -> t
type
arity_result =
| |
Arity of |
| |
NoArity |
val arity : t -> arity_result
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
ty
. The length of the
list expected_args ty
is the same as snd (arity ty)
.val is_ground : t -> bool
Var
not BVar
occurs in it)val size : t -> int
val depth : t -> int
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
.val apply : t -> t -> t
Error
if the types do not matchval apply_list : t -> t list -> t
include LogtkInterfaces.PRINT_DE_BRUIJN
include LogtkInterfaces.PRINT
val pp_surrounded : Buffer.t -> t -> unit
module TPTP:sig
..end
module Conv:sig
..end
val fresh_var : unit -> t