package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.TypeSource

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 representing AC operators (+, ...)

Sourcetype t = private InnerTerm.t

Type is a subtype of the term structure (itself a subtype of InnerTerm.t), with explicit conversion

Sourcetype ty = t
Sourcetype builtin =
  1. | TType
  2. | Prop
  3. | Term
  4. | Rat
  5. | Int
Sourceval builtin_conv : builtin -> Builtin.t
Sourcetype view = private
  1. | Builtin of builtin
  2. | Var of t HVar.t
  3. | DB of int
  4. | App of ID.t * t list
    (*

    parametrized type

    *)
  5. | Fun of t list * t
    (*

    Function type (left to right, no left-nesting)

    *)
  6. | Forall of t
    (*

    explicit quantification using De Bruijn index

    *)
Sourceval view : t -> view

Type-centric view of the head of this type.

include Interfaces.HASH with type t := t
include Interfaces.EQ with type t := t
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
include Interfaces.ORD with type t := t
Sourceval compare : t -> t -> int
Sourceval is_tType : t -> bool
Sourceval is_var : t -> bool
Sourceval is_bvar : t -> bool
Sourceval is_app : t -> bool
Sourceval is_const : t -> bool
Sourceval is_fun : t -> bool
Sourceval is_forall : t -> bool
Sourceval is_prop : t -> bool
Sourceval hash_mod_alpha : t -> int

Hash invariant w.r.t variable renaming

Constructors

Sourceval tType : t
Sourceval prop : t
Sourceval term : t
Sourceval int : t
Sourceval rat : t
Sourceval var : t HVar.t -> t
Sourceval var_of_int : int -> t

Build a type variable.

Sourceval app : ID.t -> t list -> t

Parametrized type

Sourceval builtin : builtin -> t
Sourceval const : ID.t -> t

Constant sort

Sourceval arrow : t list -> t -> t

arrow l r is the type l -> r.

Sourceval forall : t -> t

Quantify over one type variable. Careful with the De Bruijn indices!

Sourceval forall_n : int -> t -> t

Quantify over n type variable. Careful with the De Bruijn indices!

Sourceval forall_fvars : t HVar.t list -> t -> t

forall_fvars vars body makes the De Bruijn conversion before quantifying on vars

Sourceval bvar : int -> t

bound variable

Sourceval (==>) : 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.

Sourceval of_term_unsafe : InnerTerm.t -> t

NOTE: this can break the invariants and make view fail. Only use with caution.

Sourceval of_terms_unsafe : InnerTerm.t list -> t list
Sourceval cast_var_unsafe : InnerTerm.t HVar.t -> t HVar.t

Definition

Sourcetype def =
  1. | Def_unin of int
  2. | Def_data of int * ty list
Sourceval def : ID.t -> def option

Access the definition of a type

Sourceval def_exn : ID.t -> def

Unsafe version of def

Sourceval set_def : ID.t -> def -> unit

Set definition of an ID

Containers

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

Utils

Sourcemodule VarSet : CCSet.S with type elt = t HVar.t
Sourcemodule VarMap : CCMap.S with type key = t HVar.t
Sourcemodule VarTbl : CCHashtbl.S with type key = t HVar.t
Sourceval vars_set : VarSet.t -> t -> VarSet.t

Add the free variables to the given set

Sourceval vars : t -> t HVar.t list

List of free variables

Sourceval close_forall : t -> t

bind free variables

Sourcetype arity_result =
  1. | Arity of int * int
  2. | NoArity
Sourceval 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)

Sourceval 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).

Sourceval expected_ty_vars : t -> int

Number of type parameters expected. 0 for monomorphic types.

Sourceval needs_args : t -> bool

needs_args ty iff expected_ty_vars ty>0 || expected_args ty<>[]

Sourceval order : t -> int

Number of left-nested function types (1 for constant and variables). order (a->b) = 1 order ((a->b)->c) = 2 order (((a->b)->c)->d) = 2

Sourceval is_ground : t -> bool

Is the type ground? (means that no Var not BVar occurs in it)

Sourceval size : t -> int

Size of type, in number of "nodes"

Sourceval depth : t -> int

Depth of the type (length of the longest path to some leaf)

  • since 0.5.3
Sourceval 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

Sourceval 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

Sourceval returns : t -> t

returned type (going through foralls and arrows). returns a is like let _, _, ret = open_poly_fun a in ret NOTE caution, not always closed

Sourceval returns_prop : t -> bool
Sourceval returns_tType : t -> bool
Sourceexception ApplyError of string

Error raised when apply fails

Sourceval 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.

Sourceval apply1 : t -> t -> t

apply1 a b is short for apply a [b].

Sourceval apply_unsafe : t -> InnerTerm.t list -> t

Similar to apply, but assumes its arguments are well-formed types without more ado.

Sourceval is_unifiable : t -> bool

Are terms of this type syntactically unifiable? See InnerTerm.type_is_unifiable

IO

include Interfaces.PRINT_DE_BRUIJN with type term := t and type t := t
Sourcetype print_hook = int -> t CCFormat.printer -> Format.formatter -> t -> bool

User-provided hook that can be used to print terms (for composite cases) before the default printing occurs. The int argument is the De Bruijn depth in the term. A hook takes as arguments the depth and the recursive printing function that it can use to print subterms. A hook should return true if it fired, false to fall back on the default printing.

Sourceval pp_depth : ?hooks:print_hook list -> int -> t CCFormat.printer
include Interfaces.PRINT with type t := t
Sourceval to_string : t -> string
Sourceval pp_surrounded : t CCFormat.printer
Sourceval pp_typed_var : t HVar.t CCFormat.printer
Sourceval mangle : t -> string
Sourceval pp_mangle : t CCFormat.printer

TPTP

specific printer and types

Sourcemodule TPTP : sig ... end
Sourcemodule ZF : sig ... end

Conversions

Sourcemodule Conv : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct