include S with type untyped = LogtkPrologTerm.t and type typed = LogtkFOTerm.ttype untyped = LogtkPrologTerm.tuntyped term
type typed = LogtkFOTerm.tuntyped term
typed term
val infer_exn : Ctx.t -> untyped -> LogtkType.t * typed Closure.tInfer the type of this term under the given signature. This updates the context's typing environment!
the context
the untyped term whose type must be inferred
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
LogtkType.Error if the types are inconsistent
Safe version of infer_exn. It returns `Error s rather than raising LogtkType.Error if the typechecking fails.
This section is mostly useful for inferring a signature without converting untyped_terms into typed_terms.
Force the two terms to have the same type in this context
LogtkType.Error if an inconsistency is detected
val constrain_term_type_exn : Ctx.t -> untyped -> LogtkType.t -> unitForce the term's type and the given type to be the same.
LogtkType.Error if an inconsistency is detected
Safe version of constrain_term_term_exn
val constrain_term_type : Ctx.t -> untyped -> LogtkType.t -> unit or_errorSafe version of constrain_term_type_exn
type typed_form = LogtkFormula.FO.tForce the untyped term to be typable as a formula.
val infer_form : Ctx.t -> untyped -> typed_form Closure.t or_errorInferring 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
val signature_forms :
LogtkSignature.t ->
untyped Sequence.t ->
LogtkSignature.t or_errorInfer signature for this sequence of formulas, starting with an initial signature
Convert a term into a typed term.
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_errorConvert a formula into a typed formula.
see convert
the typing context to use. Updated in place.
LogtkType.Error if types are inconsistent
val convert_clause :
?generalize:bool ->
ctx:Ctx.t ->
untyped list ->
LogtkFormula.FO.t list or_errorConvert a "clause" (i.e. just a list of atomic formulas) into its type version.
see convert
val convert_seq :
?generalize:bool ->
[ `sign of LogtkSignature.t | `ctx of Ctx.t ] ->
untyped Sequence.t ->
LogtkFormula.FO.t list or_errorGiven the signature for those formulas, infer their type and convert untyped formulas into typed formulas. Also updates the context if provided.
see convert
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.tval signature_forms_exn :
LogtkSignature.t ->
untyped Sequence.t ->
LogtkSignature.tval convert_form_exn :
?generalize:bool ->
ctx:Ctx.t ->
untyped ->
LogtkFormula.FO.tval convert_clause_exn :
?generalize:bool ->
ctx:Ctx.t ->
untyped list ->
LogtkFormula.FO.t listval convert_seq_exn :
?generalize:bool ->
[ `sign of LogtkSignature.t | `ctx of Ctx.t ] ->
untyped Sequence.t ->
LogtkFormula.FO.t list