module LogtkTypeInference:`sig`

..`end`

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
`Logtk.LogtkSignature.t`

- converting
*untyped*terms or formulas into*typed*formulas, by inferring the exact type of each subterm (and possibly inferring type parameters).

`Logtk.LogtkType.i`

).
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`A`

). - If we don't, we declare that
`f : list($i) -> list($i)`

.

Many functions will use an Error monad to make errors explicit. The error
type is `LogtkTypeInference.or_error`

. The module `CCError`

in containers can be used
to deal with errors (including monadic operators).

type`'a`

or_error =`[ `Error of string | `Ok of 'a ]`

`type `

default_types = {

` ` |
`default_i : ` |

` ` |
`default_prop : ` |

` ` |
`default_int : ` |

` ` |
`default_rat : ` |

`val tptp_default : ``default_types`

Default TPTP types for ints, rats, etc.

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`

`'a`

value if provided with a proper
type inference context. It is useful to delay the translation
from untyped terms to typed terms, because locally we don't have applied all
the type constraints resulting from the context yet. Therefore, when inferring
the type of a subterm, we apply local constraints, and return a
For instance, if we infer the type of `nil`

in the terms
`cons(1, nil)`

and `cons("foo", nil)`

, we can't infer the most specialized
type for `nil`

unless we also take its context (cons(_,_)) into account.
The same closure will therefore be used to build `nil:$int`

and `nil:$string`

respectively.

module Closure:`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**.

module type S =`sig`

..`end`

`val map_error_seq : ``('a -> 'b or_error) ->`

'a Sequence.t -> 'b Sequence.t or_error

`map_error_seq f seq`

maps `f`

over the sequence `seq`

, and returns
the (persistent) sequence of result if all calls to `f`

succeed.
Otherwise it returns the first encountered error.module FO:`sig`

..`end`

module HO:`sig`

..`end`