Module LogtkTypeInference.FO

module FO: sig .. end

include LogtkTypeInference.S
type typed_form = LogtkFormula.FO.t 
val constrain_form : LogtkTypeInference.Ctx.t -> untyped -> unit LogtkTypeInference.or_error
Force the untyped term to be typable as a formula.
val infer_form : LogtkTypeInference.Ctx.t ->
untyped ->
typed_form LogtkTypeInference.Closure.t
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
val signature_forms : LogtkSignature.t ->
untyped Sequence.t -> LogtkSignature.t LogtkTypeInference.or_error
Infer signature for this sequence of formulas, starting with an initial signature
val convert : ?generalize:bool ->
ctx:LogtkTypeInference.Ctx.t -> untyped -> typed LogtkTypeInference.or_error
Convert a term into a typed term.
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:LogtkTypeInference.Ctx.t ->
untyped -> LogtkFormula.FO.t LogtkTypeInference.or_error
Convert a formula into a typed formula.
Raises LogtkType.Error if types are inconsistent
generalize : see LogtkTypeInference.FO.convert
ctx : the typing context to use. Updated in place.
val convert_clause : ?generalize:bool ->
ctx:LogtkTypeInference.Ctx.t ->
untyped list -> LogtkFormula.FO.t list LogtkTypeInference.or_error
Convert a "clause" (i.e. just a list of atomic formulas) into its type version.
generalize : see LogtkTypeInference.FO.convert
val convert_seq : ?generalize:bool ->
[ `ctx of LogtkTypeInference.Ctx.t | `sign of LogtkSignature.t ] ->
untyped Sequence.t -> LogtkFormula.FO.t list LogtkTypeInference.or_error
Given the signature for those formulas, infer their type and convert untyped formulas into typed formulas. Also updates the context if provided.
generalize : see LogtkTypeInference.FO.convert

Unsafe API

All those functions can raise LogtkType.Error in case of type mismatch, rather than use LogtkTypeInference.or_error.
val infer_form_exn : LogtkTypeInference.Ctx.t ->
untyped -> typed_form LogtkTypeInference.Closure.t
val constrain_form_exn : LogtkTypeInference.Ctx.t -> untyped -> unit
val signature_forms_exn : LogtkSignature.t -> untyped Sequence.t -> LogtkSignature.t
val convert_exn : ?generalize:bool -> ctx:LogtkTypeInference.Ctx.t -> untyped -> typed
val convert_form_exn : ?generalize:bool ->
ctx:LogtkTypeInference.Ctx.t -> untyped -> LogtkFormula.FO.t
val convert_clause_exn : ?generalize:bool ->
ctx:LogtkTypeInference.Ctx.t -> untyped list -> LogtkFormula.FO.t list
val convert_seq_exn : ?generalize:bool ->
[ `ctx of LogtkTypeInference.Ctx.t | `sign of LogtkSignature.t ] ->
untyped Sequence.t -> LogtkFormula.FO.t list