package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module TypeInference.CtxSource

Sourcetype t
Sourceval create : ?def_as_rewrite:bool -> ?default:type_ -> ?on_var:[ `Default | `Infer ] -> ?on_undef:[ `Warn | `Fail | `Guess ] -> ?on_shadow:[ `Warn | `Ignore ] -> implicit_ty_args:bool -> unit -> t

New context with a signature and default types.

  • parameter default

    which types are inferred by default (if not provided then type_erm will be used)

  • parameter def_as_rewrite

    if true, definitions will be treated like rewrite rules

  • parameter on_undef

    behavior when an undefined identifier is met

  • parameter on_var

    behavior when a variable without type annotation is met

Sourceval copy : t -> t

Copy of the context

Sourceval exit_scope : t -> unit

Exit the current scope (formula, clause), meaning that all free variables' types are forgotten. Some free variables are bound to the default type provided at creation of the context. Some ree variables will be generalized, i.e., kept as (free) variables

Sourceval declare : ?loc:loc -> t -> ID.t -> type_ -> unit

Declare the type of a symbol, possibly shadowing a previous version

Sourceval with_var : t -> type_ Var.t -> f:(unit -> 'a) -> 'a

Execute a function f with an additional declared variable

Sourceval with_vars : t -> type_ Var.t list -> f:(unit -> 'a) -> 'a

Execute a function f with additional declared variables

Sourceval pop_new_types : t -> (ID.t * type_) list

Obtain the list of symbols whose type has been inferred recently, and reset it.