package logtk

  1. Overview
  2. Docs
On This Page
  1. Unsafe API
Legend:
Library
Module
Module type
Parameter
Class
Class type
include S with type untyped = LogtkPrologTerm.t and type typed = LogtkFOTerm.t
type untyped = LogtkPrologTerm.t

untyped term

type typed = LogtkFOTerm.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

type typed_form = LogtkFormula.FO.t
val constrain_form : Ctx.t -> untyped -> unit or_error

Force the untyped term to be typable as a formula.

val infer_form : Ctx.t -> untyped -> typed_form Closure.t or_error

Inferring the type of a formula is trivial, it's always LogtkType.o. However, here we can still return a closure that produces a type formula

Infer signature for this sequence of formulas, starting with an initial signature

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

Convert a term into a typed term.

  • parameter generalize

    if true, constructor types are generalized, which means any type variable still not bound after type inference will become a type parameter. If false then those variables are bound to the default type (for instance LogtkType.TPTP.i). Default is false

val convert_form : ?generalize:bool -> ctx:Ctx.t -> untyped -> LogtkFormula.FO.t or_error

Convert a formula into a typed formula.

  • parameter ctx

    the typing context to use. Updated in place.

val convert_clause : ?generalize:bool -> ctx:Ctx.t -> untyped list -> LogtkFormula.FO.t list or_error

Convert a "clause" (i.e. just a list of atomic formulas) into its type version.

val convert_seq : ?generalize:bool -> [ `sign of LogtkSignature.t | `ctx of Ctx.t ] -> untyped Sequence.t -> LogtkFormula.FO.t list or_error

Given the signature for those formulas, infer their type and convert untyped formulas into typed formulas. Also updates the context if provided.

Unsafe API

All those functions can raise LogtkType.Error in case of type mismatch, rather than use or_error.

val infer_form_exn : Ctx.t -> untyped -> typed_form Closure.t
val constrain_form_exn : Ctx.t -> untyped -> unit
val signature_forms_exn : LogtkSignature.t -> untyped Sequence.t -> LogtkSignature.t
val convert_exn : ?generalize:bool -> ctx:Ctx.t -> untyped -> typed
val convert_form_exn : ?generalize:bool -> ctx:Ctx.t -> untyped -> LogtkFormula.FO.t
val convert_clause_exn : ?generalize:bool -> ctx:Ctx.t -> untyped list -> LogtkFormula.FO.t list
val convert_seq_exn : ?generalize:bool -> [ `sign of LogtkSignature.t | `ctx of Ctx.t ] -> untyped Sequence.t -> LogtkFormula.FO.t list
OCaml

Innovation. Community. Security.