Module `Tff.Make`Source

Parameters

module Tag : Dolmen.Intf.Tag.S

module Ty : 
  Dolmen.Intf.Ty.Tff
    with type 'a tag := 'a Tag.t
     and type path := Dolmen.Std.Path.t

module T : 
  Dolmen.Intf.Term.Tff
    with type ty := Ty.t
     and type ty_var := Ty.Var.t
     and type ty_const := Ty.Const.t
     and type ty_def := Ty.def
     and type 'a tag := 'a Tag.t
     and type path := Dolmen.Std.Path.t

Signature

Sourcemodule Tag = Tag

Sourcemodule Ty = Ty

Sourcemodule T = T

include Intf.Formulas
  with type ty := Ty.t
   and type ty_var := Ty.Var.t
   and type ty_cst := Ty.Const.t
   and type ty_def := Ty.def
   and type term := T.t
   and type term_var := T.Var.t
   and type term_cst := T.Const.t
   and type term_cstr := T.Cstr.t
   and type term_field := T.Field.t
   and type 'a ast_tag := 'a Tag.t

Type definitions

Sourcetype order =

| First_order
(*
First-oreder typechecking
*)
| Higher_order
(*
Higher-order typechecking
*)

Control whether the typechecker should type

Sourcetype poly =

| Explicit
(*
Type arguments must be explicitly given in funciton applications
*)
| Implicit
(*
Type arguments are not given in funciton applications, and instead type annotations/coercions are used to disambiguate applications of polymorphic symbols.
*)
| Flexible
(*
Mix between explicit and implicit: depending on the arity of a symbol and the number of arguments provided, either the provided type arguments are used, or wildcards are generated for all of them, and later instantiated when needed.
*)

The various polymorphism mode for the typechecker

Sourcetype sym_inference_source = {

symbol : Dolmen.Std.Id.t;
symbol_loc : Dolmen.Std.Loc.t;
mutable inferred_ty : Ty.t;

}

Sourcetype var_inference_source = {

variable : Dolmen.Std.Id.t;
variable_loc : Dolmen.Std.Loc.t;
mutable inferred_ty : Ty.t;

}

Sourcetype wildcard_source =

| Arg_of of wildcard_source
| Ret_of of wildcard_source
| From_source of Dolmen.Std.Term.t
| Added_type_argument of Dolmen.Std.Term.t
| Symbol_inference of sym_inference_source
| Variable_inference of var_inference_source

Sourcetype wildcard_shape =

| Forbidden
| Any_in_scope
| Any_base of {
1. allowed : Ty.t list;
2. preferred : Ty.t;
}
| Arrow of {
1. arg_shape : wildcard_shape;
2. ret_shape : wildcard_shape;
}

Sourcetype infer_unbound_var_scheme =

| No_inference
| Unification_type_variable

Sourcetype infer_term_scheme =

| No_inference
| Wildcard of wildcard_shape

Sourcetype var_infer = {

infer_unbound_vars : infer_unbound_var_scheme;
infer_type_vars_in_binding_pos : bool;
infer_term_vars_in_binding_pos : infer_term_scheme;
var_hook : [ `Ty_var of Ty.Var.t | `Term_var of T.Var.t ] -> unit;

}

Specification of how to infer variables.

Sourcetype sym_infer = {

infer_type_csts : bool;
infer_term_csts : infer_term_scheme;
sym_hook : [ `Ty_cst of Ty.Const.t | `Term_cst of T.Const.t ] -> unit;

}

Specification of how to infer symbols.

Sourcetype free_wildcards =

| Forbidden
| Implicitly_universally_quantified

Sourcetype expect =

| Type
| Term
| Anything

Sourcetype tag =

| Set : 'a Tag.t * 'a -> tag
| Add : 'a list Tag.t * 'a -> tag
| Hook : (Dolmen.Std.Term.t -> res -> res) -> tag
(*
Existencial wrapper around tags
*)

Sourceand res =

| Ttype
| Ty of Ty.t
| Term of T.t
| Tags of tag list

The results of parsing an untyped term.

Sourcetype reservation =

| Strict
(*
Strict reservation: the language dictates that the corresponding id is reserved for another use, and therefore cannot appear in its position.
*)
| Model_completion
(*
Soft reservation: the id is not technically reserved by the language, but it happens that it is used in models to complete the interpretation of a partial symbol (for isntance division by zero).
*)

Types of reservation of symbols: some symbols/id are reserved for some uses, and therefore cannot/should not occur at some positions. This type tries and explain the reason for such restrictions.

Sourcetype reason =

| Builtin
| Reserved of reservation * string
| Bound of Dolmen.Std.Loc.file * Dolmen.Std.Term.t
| Inferred of Dolmen.Std.Loc.file * Dolmen.Std.Term.t
| Defined of Dolmen.Std.Loc.file * Dolmen.Std.Statement.def
| Declared of Dolmen.Std.Loc.file * Dolmen.Std.Statement.decl
| Implicit_in_def of Dolmen.Std.Loc.file * Dolmen.Std.Statement.def
| Implicit_in_decl of Dolmen.Std.Loc.file * Dolmen.Std.Statement.decl
| Implicit_in_term of Dolmen.Std.Loc.file * Dolmen.Std.Term.t
(*
The type of reasons for constant typing
*)

Sourcetype binding = [

| `Not_found
| `Reserved of [ `Model of string | `Solver of string ]
| `Builtin of [ `Ttype | `Ty | `Term | `Tag ]
| `Variable of [ `Ty of Ty.Var.t * reason option | `Term of T.Var.t * reason option ]
| `Constant of [ `Ty of Ty.Const.t * reason option | `Cstr of T.Cstr.t * reason option | `Dstr of T.Const.t * reason option | `Term of T.Const.t * reason option | `Field of T.Field.t * reason option ]

]

Sourcetype builtin_meta_ttype = unit

The bindings that can occur.

Sourcetype builtin_meta_ty = unit

Sourcetype builtin_meta_tags = unit

Some type aliases

Sourcetype partial_semantics = [

| `Partial of Ty.Var.t list -> T.Var.t list -> Ty.t -> T.Const.t

]

Sourcetype term_semantics = [

| partial_semantics
| `Total

]

Semantics of term constants. Some term constants have only partially defined semantics (for instance division by zero), and these constants can have their semantics/interpretation extended/completed by later definitions.

Sourcetype builtin_meta_term = term_semantics

Meta data for term builtins.

Source

type ('res, 'meta) builtin_common_res =
  'meta * (Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> 'res)

Small record to hold the results of builtin parsing by theories.

Sourcetype builtin_res = [

| `Ttype of (unit, builtin_meta_ttype) builtin_common_res
| `Ty of (Ty.t, builtin_meta_ty) builtin_common_res
| `Term of (T.t, builtin_meta_term) builtin_common_res
| `Tags of (tag list, builtin_meta_tags) builtin_common_res
| `Reserved of [ `Solver of string | `Model of string * partial_semantics ]
| `Infer of binding * var_infer * sym_infer

]

The result of parsing a symbol by the theory

Sourcetype not_found = [

| `Not_found

]

Not bound bindings

Sourcetype var_kind = [

| `Let_bound
| `Quantified
| `Function_param
| `Type_alias_param

]

The type of kinds of variables

Sourcetype nonrec symbol = Intf.symbol =

| Id of Dolmen.Std.Id.t
| Builtin of Dolmen.Std.Term.builtin

Wrapper around potential function symbols from the Dolmen AST.

Sourcetype decl = [

| `Type_decl of Ty.Const.t * Ty.def option
| `Term_decl of T.Const.t

]

Sourcetype def = [

| `Type_alias of Dolmen.Std.Loc.t * Dolmen.Std.Id.t * Ty.Const.t * Ty.Var.t list * Ty.t
| `Term_def of Dolmen.Std.Loc.t * Dolmen.Std.Id.t * T.Const.t * Ty.Var.t list * T.Var.t list * T.t
| `Instanceof of Dolmen.Std.Loc.t * Dolmen.Std.Id.t * T.Const.t * Ty.t list * Ty.Var.t list * T.Var.t list * T.t

]

Sourcetype implicit = [

| decl
| def

]

Errors and warnings

Sourcetype _ fragment =

| Ast : Dolmen.Std.Term.t -> Dolmen.Std.Term.t fragment
| Def : Dolmen.Std.Statement.def -> Dolmen.Std.Statement.def fragment
| Defs : Dolmen.Std.Statement.defs -> Dolmen.Std.Statement.defs fragment
| Decl : Dolmen.Std.Statement.decl -> Dolmen.Std.Statement.decl fragment
| Decls : Dolmen.Std.Statement.decls -> Dolmen.Std.Statement.decls fragment
| Located : Dolmen.Std.Loc.t -> Dolmen.Std.Loc.t fragment

Fragments of input that represent the sources of warnings/errors

Sourcetype _ warn = ..

The type of warnings, parameterized by the type of fragment they can trigger on

Sourcetype warn +=

| Unused_type_variable : var_kind * Ty.Var.t -> Dolmen.Std.Term.t warn
(*
Unused quantified type variable
*)
| Unused_term_variable : var_kind * T.Var.t -> Dolmen.Std.Term.t warn
(*
Unused quantified term variable
*)
| Superfluous_destructor : Dolmen.Std.Id.t * Dolmen.Std.Id.t * T.Const.t -> Dolmen.Std.Term.t warn
(*
The user implementation of typed terms returned a destructor where was asked for. This warning can very safely be ignored.
*)
| Redundant_pattern : T.t -> Dolmen.Std.Term.t warn
(*
Redundant cases in pattern matching
*)

Warnings that cna trigger on regular parsed terms.

Sourcetype warn +=

| Shadowing : Dolmen.Std.Id.t * binding * binding -> _ warn
(*
Shadowing of the given identifier, together with the old and current binding.
*)

Special case of warnings for shadowing, as it can happen both from a term but also a declaration, hence why the type variable of warn is left wild.

Sourcetype _ err = ..

The type of errors, parameterized by the type of fragment they can trigger on

Sourcetype err +=

| Not_well_founded_datatypes : Dolmen.Std.Statement.decl list -> Dolmen.Std.Statement.decls err
(*
Not well-dounded datatypes definitions.
*)

Errors that occur on declaration(s)

Sourcetype err +=

| Expected : string * res option -> Dolmen.Std.Term.t err
(*
The parsed term didn't match the expected shape
*)
| Bad_index_arity : string * int * int -> Dolmen.Std.Term.t err
(*
Bad_index_arity (name, expected, actual) denotes an error where an indexed family of operators (based on name) expect to be indexed by expected arguments but got actual instead.
*)
| Bad_ty_arity : Ty.Const.t * int -> Dolmen.Std.Term.t err
(*
Bad_ty_arity (cst, actual) denotes a type constant that was applied to actual arguments, but which has a different arity (which should be accessible by getting its type/sort/arity).
*)
| Bad_op_arity : symbol * int list * int -> Dolmen.Std.Term.t err
(*
Bad_op_arity (symbol, expected, actual) denotes a named operator (which may be a builtin operator, a top-level defined constant which is being substituted, etc...) expecting a number of arguments among the expected list, but instead got actual number of arguments.
*)
| Bad_cstr_arity : T.Cstr.t * int list * int -> Dolmen.Std.Term.t err
(*
Bad_cstr_arity (cstr, expected, actual) denotes an ADT constructor, which was expecting one of expected arguments, but which was applied to actual arguments.
*)
| Bad_term_arity : T.Const.t * int list * int -> Dolmen.Std.Term.t err
(*
Bad_term_arity (func, expected, actual) denotes a function symbol, which was expecting one of expected arguments, but which was applied to actual arguments.
*)
| Bad_poly_arity : Ty.Var.t list * Ty.t list -> Dolmen.Std.Term.t err
(*
Bad_poly_arity (ty_vars, ty_args) denotes a polymorphic term application, where the function term being applied was provided with the type arguments [ty_args], but the function type expected a number of arguments that is the length of [ty_vars], and the two lengths differ. Under application is allowed, so in the cases where there are less provided arguments than expected type arguments, the presence of term arguments after the type arguments forced the raising of this exception.
*)
| Over_application : T.t list -> Dolmen.Std.Term.t err
(*
Over_application over_args denotes an application where after applying the provided arguments, the application resulted in a term with a non-function type, but that term was still provided with over_args.
*)
| Repeated_record_field : T.Field.t -> Dolmen.Std.Term.t err
(*
Repeated_record_field f denotes an error within an expression that builds a record by giving values to all fields, but where the field f appears more than once.
*)
| Missing_record_field : T.Field.t -> Dolmen.Std.Term.t err
(*
Missing_record_field f denotes an error within an expression that builds a record by giving values to all fields, but where the field f does not appear.
*)
| Mismatch_record_type : T.Field.t * Ty.Const.t -> Dolmen.Std.Term.t err
(*
Mismatch_record_type (f, r) denotes an error where while building a record expression for a record of type c, a field f belonging to another record type was used.
*)
| Mismatch_sum_type : T.Cstr.t * Ty.t -> Dolmen.Std.Term.t err
| Partial_pattern_match : T.t list -> Dolmen.Std.Term.t err
(*
Partial_pattern_match missing denotes an error within a pattern matching in which the list of patterns do not cover all of the values of the type being matched. A list of non-matched terms is given to help users complete the pattern matching.
*)
| Var_application : T.Var.t -> Dolmen.Std.Term.t err
(*
Var_application v denotes a variable which was applied to other terms, which is forbidden in first-order formulas.
*)
| Ty_var_application : Ty.Var.t -> Dolmen.Std.Term.t err
(*
Ty_var_application v denotes a type variable which was applied to other terms, which is forbidden in first-order formulas.
*)
| Type_mismatch : T.t * Ty.t -> Dolmen.Std.Term.t err
(*
Type_mismatch (term, expected) denotes a context where term was expected to have type expected, but it is not the case.
*)
| Var_in_binding_pos_underspecified : Dolmen.Std.Term.t err
(*
Variable in a binding pos (e.g. quantifier) without a type, and no configured way to infer its type.
*)
| Unhandled_builtin : Dolmen.Std.Term.builtin -> Dolmen.Std.Term.t err
| Cannot_tag_tag : Dolmen.Std.Term.t err
| Cannot_tag_ttype : Dolmen.Std.Term.t err
| Cannot_find : Dolmen.Std.Id.t * string -> Dolmen.Std.Term.t err
| Forbidden_quantifier : Dolmen.Std.Term.t err
| Missing_destructor : Dolmen.Std.Id.t -> Dolmen.Std.Term.t err
| Type_def_rec : Dolmen.Std.Statement.def -> Dolmen.Std.Statement.defs err
| Id_definition_conflict : Dolmen.Std.Id.t * binding -> Dolmen.Std.Loc.t err
| Higher_order_application : Dolmen.Std.Term.t err
| Higher_order_type : Dolmen.Std.Term.t err
| Higher_order_env_in_tff_typechecker : Dolmen.Std.Loc.t err
(*
Programmer error
*)
| Polymorphic_function_argument : Dolmen.Std.Term.t err
| Non_prenex_polymorphism : Ty.t -> Dolmen.Std.Term.t err
| Inference_forbidden : Ty.Var.t * wildcard_source * Ty.t -> Dolmen.Std.Term.t err
| Inference_conflict : Ty.Var.t * wildcard_source * Ty.t * Ty.t list -> Dolmen.Std.Term.t err
| Inference_scope_escape : Ty.Var.t * wildcard_source * Ty.Var.t * reason option -> Dolmen.Std.Term.t err
(*
Inference_scope_escape (w, w_src, v, reason) denotes a situation where the wildcard variable w (which comes from w_src), was instantiated with a type that would lead to the variable v from escaping its scope; reason is the reason of the binding for v.
*)
| Unbound_type_wildcards : (Ty.Var.t * wildcard_source list) list -> Dolmen.Std.Term.t err
| Incoherent_type_redefinition : Dolmen.Std.Id.t * Ty.Const.t * reason * int -> Dolmen.Std.Statement.def err
| Incoherent_term_redefinition : Dolmen.Std.Id.t * T.Const.t * reason * Ty.t -> Dolmen.Std.Statement.def err
| Inferred_builtin : Dolmen.Std.Term.builtin -> Dolmen.Std.Term.t err
| Forbidden_hook : Dolmen.Std.Term.t err
| Uncaught_exn : exn * Printexc.raw_backtrace -> Dolmen.Std.Term.t err
| Unhandled_ast : Dolmen.Std.Term.t err

Errors that occur on regular parsed terms.

Global State

Sourcetype state

The type of mutable state for typechecking.

Sourceval new_state : unit -> state

Create a new state.

Sourceval copy_state : state -> state

Make a copy of the global state included in the env

Typing Environment

Sourcetype env

The type of environments for typechecking.

Sourcetype 'a typer = env -> Dolmen.Std.Term.t -> 'a

A general type for typers. Takes a local environment and the current untyped term, and return a value. The typer may need additional information for parsing, in which case the return value will be a function.

raises Typing_error

Sourcetype builtin_symbols = env -> symbol -> [ builtin_res | not_found ]

The type of a typer for builtin symbols. Given the environment and a symbol, the theory should return a typing function if the symbol belongs to the theory. This typing function takes first the ast term of the whole application that is beign typechecked, and the list of arguments to the symbol.

Sourcetype warning =

| Warning : env * 'a fragment * 'a warn -> warning

Existential wrapper around warnings

Sourcetype error =

| Error : env * 'a fragment * 'a err -> error

Existential wrapper around errors

Sourceexception Typing_error of error

Exception for typing errors

Source

val empty_env : 
  ?st:state ->
  ?expect:expect ->
  ?var_infer:var_infer ->
  ?sym_infer:sym_infer ->
  ?order:order ->
  ?poly:poly ->
  ?quants:bool ->
  ?free_wildcards:free_wildcards ->
  warnings:(warning -> unit) ->
  file:Dolmen.Std.Loc.file ->
  builtin_symbols ->
  env

Create a new environment.

Sourceval state : env -> state

Get the mutable state for an env.

Inference for vars and syms

Sourceval var_infer : env -> var_infer

Getter for an env's var infer.

Sourceval with_var_infer : env -> var_infer -> env

Set the variable inference configuation

Sourceval sym_infer : env -> sym_infer

Getter for an env's sym infer.

Sourceval with_sym_infer : env -> sym_infer -> env

Set the symbol inference configuration

Errors & Warnings

Sourceval _warn : env -> 'a fragment -> 'a warn -> unit

Emit a warning

Sourceval _error : env -> 'a fragment -> 'a err -> _

Raise an error

Sourceval file : env -> Dolmen.Std.Loc.file

Return the current file for th eenv.

Sourceval suggest : limit:int -> env -> Dolmen.Std.Id.t -> Dolmen.Std.Id.t list

From a dolmen identifier, return a list of existing bound identifiers in the env that are up to ~limit in terms of distance of edition.

Sourceval _wrap : env -> Dolmen.Std.Term.t -> ('a -> 'b) -> 'a -> 'b

Sourceval _wrap2 : env -> Dolmen.Std.Term.t -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'c

Source

val _wrap3 : 
  env ->
  Dolmen.Std.Term.t ->
  ('a -> 'b -> 'c -> 'd) ->
  'a ->
  'b ->
  'c ->
  'd

Location helpers

Sourceval loc : env -> Dolmen.Std.Loc.t -> Dolmen.Std.Loc.full

Completes the location with the file name form the env.

Sourceval fragment_loc : env -> _ fragment -> Dolmen.Std.Loc.full

Convenient function to get the location of a fragment.

Sourceval binding_reason : binding -> reason option

Extract the reason from a binding

raises Invalid_argument
if the binding is `Not_found

Name/Path helpers

Sourceval var_name : env -> Dolmen.Std.Name.t -> string

Extract a variable name from a standard name.

Sourceval cst_path : env -> Dolmen.Std.Name.t -> Dolmen.Std.Path.t

Build a path from a standard name.

Bindings helpers

Sourcetype var = [

| `Ty_var of Ty.Var.t
| `Term_var of T.Var.t
| `Letin of env * Dolmen.Std.Term.t * T.Var.t * T.t

]

Variable bindings

Sourcetype cst = [

| `Cstr of T.Cstr.t
| `Dstr of T.Const.t
| `Field of T.Field.t
| `Ty_cst of Ty.Const.t
| `Term_cst of T.Const.t

]

Constant bindings

Sourcetype builtin = [

| `Builtin of builtin_res

]

Builtin binding

Sourcetype bound = [

| var
| cst
| builtin

]

Sourceval find_var : env -> Dolmen.Std.Id.t -> [ var | not_found ]

Try and find the given id in the set of locally bound variables.

Sourceval find_global : env -> Dolmen.Std.Id.t -> [ cst | not_found ]

Try and find the given id in the set of globally bound constants.

Sourceval find_global_st : state -> Dolmen.Std.Id.t -> [ cst | not_found ]

Try and find the given id in the set of globally bound constants.

Sourceval find_builtin : env -> Dolmen.Std.Id.t -> [ builtin | not_found ]

Try and find the given id in the set of bound builtin symbols.

Sourceval find_bound : env -> Dolmen.Std.Id.t -> [ bound | not_found ]

Try and find a bound identifier in the env, whether it be locally bound (such as bound variables), constants bound at top-level, or builtin symbols bound by the builtin theory.

Sourceval find_reason : env -> bound -> reason option

Return the reason (if any) for the given typed symbol.

Source

val decl_ty_const : 
  env ->
  _ fragment ->
  Dolmen.Std.Id.t ->
  Ty.Const.t ->
  reason ->
  unit

Declare a new type constant in the global environment used by the given environment

Source

val decl_term_const : 
  env ->
  _ fragment ->
  Dolmen.Std.Id.t ->
  T.Const.t ->
  reason ->
  unit

Declare a new term constant in the global environment used by the given environment

Sourceval register_implicit : env -> implicit -> unit

Custom global state

Sourceval get_global_custom : env -> 'a Dolmen.Std.Tag.t -> 'a option

Sourceval get_global_custom_state : state -> 'a Dolmen.Std.Tag.t -> 'a option

Get a custom value from the global environment or state.

Sourceval set_global_custom : env -> 'a Dolmen.Std.Tag.t -> 'a -> unit

Sourceval set_global_custom_state : state -> 'a Dolmen.Std.Tag.t -> 'a -> unit

Set a custom value in the global environment or state.

Builtin helpers

Source

val builtin_ttype : 
  ?meta:builtin_meta_ttype ->
  (Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> unit) ->
  [> builtin_res ]

Source

val builtin_ty : 
  ?meta:builtin_meta_ty ->
  (Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> Ty.t) ->
  [> builtin_res ]

Source

val builtin_term : 
  ?meta:builtin_meta_term ->
  (Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> T.t) ->
  [> builtin_res ]

Source

val builtin_tags : 
  ?meta:builtin_meta_tags ->
  (Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> tag list) ->
  [> builtin_res ]

Parsing functions

Sourceval wildcard : env -> wildcard_source -> wildcard_shape -> Ty.t

Create a wildcard type.

Sourceval monomorphize : env -> Dolmen.Std.Term.t -> T.t -> T.t

Monomorphize a term.

Sourceval parse_expr : res typer

Main parsing function.

Sourceval parse_ty : Ty.t typer

Sourceval parse_term : T.t typer

Sourceval parse_prop : T.t typer

Wrappers around parse_expr to set the expect field of the env, and unwrap an expected return value.

Sourceval parse_app_ty_cst : (Ty.Const.t -> Dolmen.Std.Term.t list -> res) typer

Sourceval parse_app_term_cst : (T.Const.t -> Dolmen.Std.Term.t list -> res) typer

Function used for parsing applications. The first dolmen term given is the application term being parsed (used for reporting errors).

Sourceval parse_app_ho_term : (T.t -> Dolmen.Std.Term.t list -> res) typer

Function used for parsing an higher-order application.

Sourceval unwrap_ty : env -> Dolmen.Std.Term.t -> res -> Ty.t

Sourceval unwrap_term : env -> Dolmen.Std.Term.t -> res -> T.t

Unwrap a result, raising the adequate typing error if the result if not as expected.

High-level functions

Sourcetype 'a ret = {

implicit_decls : decl list;
implicit_defs : def list;
result : 'a;

}

Source

val decls : 
  env ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.decls ->
  decl list ret

Parse a list of potentially mutually recursive declarations.

Source

val defs : 
  ?mode:[ `Create_id | `Use_declared_id ] ->
  env ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.defs ->
  def list ret

Parse a definition

Sourceval term : env -> Dolmen.Std.Term.t -> T.t ret

Sourceval formula : env -> Dolmen.Std.Term.t -> T.t ret

Top-level functions to typecheck terms and formulas.

package dolmen_type

Module Tff.MakeSource

Parameters

Signature

Type definitions

Errors and warnings

Global State

Typing Environment

Inference for vars and syms

Errors & Warnings

Location helpers

Name/Path helpers

Bindings helpers

Custom global state

Builtin helpers

Parsing functions

High-level functions

Module `Tff.Make`Source