package logtk

  1. Overview
  2. Docs
On This Page
  1. Unsafe API
package logtk
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

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

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

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

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