This module is used for two things that overlap:
- inferring the types of symbols that have not been declared (e.g. in "fof" or "cnf" TPTP statements) so as to enrich a
- converting untyped terms or formulas into typed formulas, by inferring the exact type of each subterm (and possibly inferring type parameters).
In this context, generalizing type variables means that if some ID.t whose type was unknown and its type still contains variables after the type inference, those variables are quantified instead of being bound to a default type (typically
For instance: say
f is not declared and occurs in the term
f(f(nil)) with the declared constructor
nil : list(A). The inferred type for
f should be something like
list(B) -> list(B).
- If we generalize, we declare that
f : list(A) -> list(A)(for all
- If we don't, we declare that
f : list($i) -> list($i).
Here we use a single scope when we unify and substitute type variables, the scope 0.
Many functions will use an Error monad to make errors explicit. The error type is
or_error. The module
CCError in containers can be used to deal with errors (including monadic operators).
type 'a or_error = ( 'a, string ) CCResult.t
type type_ = TypedSTerm.t
type untyped = STerm.t
type typed = TypedSTerm.t
type loc = ParseLocation.t
val section : Util.Section.t
module TyBuiltin : sig ... end
This module provides a typing context, with an applicative interface. The context is used to map terms to types locally during type inference. It also keeps and updates a signature when symbols' types are inferred.
This module is quite low-level, and shouldn't be used in simple cases (see the following modules)
module Ctx : sig ... end
This module, abstract in the exact kind of term it types, takes as input a signature and an untyped term, and updates the typing context so that the untyped term can be converted into a typed term.
Infer the type of this term under the given signature. This updates the context's typing environment!
Convert a clause. Free variables in each of the list's elements are shared
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
Force the term's type and the given type to be the same.
Safe version of
Safe version of
val infer_statement_exn : ?file:string -> Ctx.t -> UntypedAST.statement -> typed_statement * typed_statement list
infer_statement ctx ~f st checks and convert
st into a typed statements, and a list of auxiliary type declarations for symbols that were inferred implicitly.
val infer_statements_exn : ?def_as_rewrite:bool -> ?on_var:[ `Infer | `Default ] -> ?on_undef:[ `Warn | `Fail | `Guess ] -> ?on_shadow:[ `Warn | `Ignore ] -> ?ctx:Ctx.t -> ?file:string -> implicit_ty_args:bool -> UntypedAST.statement Iter.t -> typed_statement CCVector.ro_vector
Infer all statements