package logtk

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Unsafe API

package logtk

logtk
- Logtk
- LogtkCache
  - Dummy
    
    X
  - Dummy2
    
    X
    
    Y
  - EQ
  - HASH
  - LRU
    
    X
  - Linear
    
    X
  - Linear2
    
    X
    
    Y
  - Replacing
    
    X
  - Replacing2
    
    X
    
    Y
  - S
  - S2
- LogtkCnf
- LogtkComparison
  - PARTIAL_ORD
- LogtkCongruence
  - FO
  - HO
  - Make
    
    T
  - S
  - TERM
- LogtkDBEnv
- LogtkDtree
  - Default
  - Make
    
    E
- LogtkFOTerm
  - AC
    
    A
  - AC_SPEC
  - Classic
  - Map
  - Pos
  - Seq
  - Set
  - T2LogtkCache
  - TLogtkCache
  - TPTP
    
    Arith
  - Tbl
- LogtkFastFingerprint
  - Make
    
    Leaf
    
    X
- LogtkFeatureVector
  - Make
    
    C
    
    Feature
- LogtkFingerprint
  - Make
    
    Leaf
    
    X
- LogtkFormula
  - FO
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - Make
    
    Base
    
    Map
    
    MyT
    
    Seq
    
    Set
    
    TPTP
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - Map
    
    From
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
    
    To
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - S
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - TERM
    
    Seq
    
    Set
    
    TPTP
- LogtkFormulaShape
- LogtkHORewriting
  - Seq
- LogtkHOTerm
  - LogtkCache
  - Map
  - Pos
  - Seq
  - Set
  - TPTP
  - Tbl
  - any_visitor
  - id_visitor
- LogtkHashcons
  - HashedLogtkType
  - Make
    
    H
    
    X
  - S
    
    H
- LogtkIArray
  - Seq
- LogtkIndex
  - BasicEquation
  - CLAUSE
  - EQUATION
  - LEAF
  - MakeLeaf
    
    X
  - SUBSUMPTION_IDX
    
    C
  - TERM_IDX
    
    Leaf
  - UNIT_IDX
    
    E
- LogtkInterfaces
  - EQ
  - GROUP
  - HASH
  - ITER
  - MONOID
  - ORD
  - PRINT
  - PRINT1
  - PRINT_DE_BRUIJN
  - PRINT_OVERLOAD
- LogtkLambda
- LogtkLazyGraph
  - Dot
  - Full
  - Heap
  - Infix
  - Mutable
- LogtkLazyList
- LogtkMultiset
  - Make
    
    Seq
    
    X
  - S
    
    Seq
- LogtkNPDtree
  - Make
    
    E
  - MakeTerm
    
    Leaf
    
    X
- LogtkOptions
- LogtkOrdering
  - Default
  - Make
    
    P
    
    Constr
    
    Seq
- LogtkOrdering_intf
  - S
    
    Prec
    
    Constr
    
    Seq
- LogtkParseLocation
- LogtkPartialOrder
  - ELEMENT
  - Make
    
    E
- LogtkPartialOrder_intf
  - S
- LogtkPosition
  - Build
- LogtkPrecedence
  - Constr
  - Default
    
    Constr
    
    Seq
  - Make
    
    Constr
    
    Seq
    
    Sym
  - SYMBOL
  - Seq
- LogtkPrecedence_intf
  - S
    
    Constr
    
    Seq
- LogtkPrologTerm
  - Map
  - Seq
  - Set
  - TPTP
  - Tbl
  - id_visitor
  - visitor
- LogtkRewriting
  - FormRW
  - MakeOrdered
    
    E
  - MakeTRS
    
    I
    
    E
  - ORDERED
    
    E
  - SIG_TRS
  - TRS
- LogtkScopedTerm
  - DB
  - Kind
  - Map
  - Pos
  - Seq
  - Set
  - Tbl
- LogtkSignature
  - SMap
  - Seq
  - TPTP
    
    Arith
- LogtkSkolem
- LogtkSourced
- LogtkSubsts
  - FO
  - Form
  - HO
  - Renaming
  - SPECIALIZED
  - Ty
- LogtkSymbol
  - ArithOp
  - Base
  - Map
  - Seq
  - Set
  - TPTP
    
    Arith
  - Tbl
- LogtkTransform
  - DAG
    
    Form
  - FORM
  - FormDag
    
    Form
  - MakeDAG
    
    Form
- LogtkType
  - Conv
  - Map
  - Seq
  - Set
  - TPTP
  - Tbl
- LogtkTypeInference
  - Closure
  - Ctx
  - FO
  - HO
  - S
- LogtkTypedPrologTerm
  - Map
  - Seq
  - Set
  - Subst
  - Tbl
  - Visitor
- LogtkUnif
  - FO
  - Form
  - HO
  - NARY
  - Nary
  - Ty
  - UNARY
  - Unary
- LogtkUtil
  - Exn
  - Flag
  - Section

Legend:
Library
Module
Module type
Parameter
Class
Class type

include S with type untyped = LogtkPrologTerm.t and type typed = LogtkHOTerm.t

type untyped = LogtkPrologTerm.t

untyped term

type typed = LogtkHOTerm.t

untyped term

typed term

val infer_exn : Ctx.t -> untyped -> LogtkType.t * typed Closure.t

Infer the type of this term under the given signature. This updates the context's typing environment!

parameter ctx
the context

parameter untyped
the untyped term whose type must be inferred

returns
the inferred type of the untyped term (possibly a type var) along with a closure to produce a typed term once every constraint has been solved

raises LogtkType.Error
if the types are inconsistent

val infer : Ctx.t -> untyped -> (LogtkType.t * typed Closure.t) or_error

Safe version of infer_exn. It returns `Error s rather than raising LogtkType.Error if the typechecking fails.

Constraining types

This section is mostly useful for inferring a signature without converting untyped_terms into typed_terms.

val constrain_term_term_exn : Ctx.t -> untyped -> untyped -> unit

Force the two terms to have the same type in this context

raises LogtkType.Error
if an inconsistency is detected

val constrain_term_type_exn : Ctx.t -> untyped -> LogtkType.t -> unit

Force the term's type and the given type to be the same.

raises LogtkType.Error
if an inconsistency is detected

val constrain_term_term : Ctx.t -> untyped -> untyped -> unit or_error

Safe version of constrain_term_term_exn

val constrain_term_type : Ctx.t -> untyped -> LogtkType.t -> unit or_error

Safe version of constrain_term_type_exn

val constrain : ctx:Ctx.t -> untyped -> unit or_error

Constrain the term to be well-typed and of boolean type

val convert : 
  ?generalize:bool ->
  ?ret:LogtkType.t ->
  ctx:Ctx.t ->
  untyped ->
  typed or_error

Convert a single untyped term to a typed term. Binds free constructor variables to default.

parameter ctx
context used for type inference

parameter ret
is the type we expect for this term (default: LogtkType.o)

parameter generalize
if true, constructor types are generalized (see FO.convert more more details). Default is false

val convert_seq : 
  ?generalize:bool ->
  ctx:Ctx.t ->
  untyped Sequence.t ->
  typed list or_error

Infer the types of those terms and annotate each term and subterm with its type. Also updates the context's signature. All terms are assumed to be boolean.

Unsafe API

Functions that can raise LogtkType.Error

val constrain_exn : ctx:Ctx.t -> untyped -> unit

val convert_exn : 
  ?generalize:bool ->
  ?ret:LogtkType.t ->
  ctx:Ctx.t ->
  untyped ->
  typed

val convert_seq_exn : 
  ?generalize:bool ->
  ctx:Ctx.t ->
  untyped Sequence.t ->
  typed list