dolmen_type 0.7 · OCaml Package

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 'a tag := 'a Tag.t
     and type path := Dolmen.Std.Path.t

Signature required by terms for typing first-order polymorphic terms.

include Intf.Formulas
  with type ty := Ty.t
   and type ty_var := Ty.Var.t
   and type ty_cst := Ty.Const.t
   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

type order =

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

Control whether the typechecker should type

type 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

type sym_inference_source = {

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

}

type var_inference_source = {

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

}

type 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

type 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;
}

type infer_unbound_var_scheme =

| No_inference
| Unification_type_variable

type infer_term_scheme =

| No_inference
| Wildcard of wildcard_shape

type 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;

}

Specification of how to infer variables.

type sym_infer = {

infer_type_csts : bool;
infer_term_csts : infer_term_scheme;

}

Specification of how to infer symbols.

type free_wildcards =

| Forbidden
| Implicitly_universally_quantified

type expect =

| Type
| Term
| Anything

type tag =

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

type res =

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

The results of parsing an untyped term.

type builtin_res = [

| `Ttype of Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> unit
| `Ty of Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> Ty.t
| `Term of Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> T.t
| `Tags of Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> tag list

]

The result of parsing a symbol by the theory

type not_found = [

| `Not_found

]

Not bound bindings

type inferred =

| Ty_fun of Ty.Const.t
| Term_fun of T.Const.t

The type for inferred symbols.

type reason =

| Builtin
| 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
(*
The type of reasons for constant typing
*)

type binding = [

| `Not_found
| `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 ]

]

The bindings that can occur.

type 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.

Errors and warnings

type _ 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

type _ warn = ..

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

type warn +=

| Unused_type_variable : [ `Quantified | `Letbound ] * Ty.Var.t -> Dolmen.Std.Term.t warn
(*
Unused quantified type variable
*)
| Unused_term_variable : [ `Quantified | `Letbound ] * T.Var.t -> Dolmen.Std.Term.t warn
(*
Unused quantified term variable
*)
| Error_in_attribute : exn -> Dolmen.Std.Term.t warn
(*
An error occurred wile parsing an attribute
*)
| 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.

type 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.

type _ err = ..

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

type 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)

type 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
| 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
| Uncaught_exn : exn * Stdlib.Printexc.raw_backtrace -> Dolmen.Std.Term.t err
| Unhandled_ast : Dolmen.Std.Term.t err

Errors that occur on regular parsed terms.

Global State

type state

The type of mutable state for typechecking.

val new_state : unit -> state

Create a new state.

val copy_state : state -> state

Make a copy of the global state included in the env

Typing Environment

type env

The type of environments for typechecking.

type '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

type 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.

type warning =

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

Existential wrapper around warnings

type error =

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

Existential wrapper around errors

exception Typing_error of error

Exception for typing errors

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.

Location helpers

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

Completes the location with the file name form the env.

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

Convenient function to get the location of a fragment.

val binding_reason : binding -> reason option

Extract the reason from a binding

raises Invalid_argument
if the binding is `Not_found

Name/Path helpers

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

Extract a variable name from a standard name.

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

Build a path from a standard name.

Bindings helpers

type 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

type 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

type builtin = [

| `Builtin of builtin_res

]

Builtin binding

type bound = [

| var
| cst
| builtin

]

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

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

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

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

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

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

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

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

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

Get a custom value from the global environment.

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

Set a custom value in the global environment.

Errors & Warnings

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

Emit a warning

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

Raise an error

val 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.

Parsing functions

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

Monomorphize a term.

val parse_expr : res typer

Main parsing function.

val parse_ty : Ty.t typer

val parse_term : T.t typer

val parse_prop : T.t typer

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

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

val 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).

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

Function used for parsing an higher-order application.

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

val 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

val decls : 
  env ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.decls ->
  [ `Type_decl of Ty.Const.t | `Term_decl of T.Const.t ] list

Parse a list of potentially mutually recursive declarations.

val defs : 
  env ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.defs ->
  [ `Type_def of Dolmen.Std.Id.t * Ty.Const.t * Ty.Var.t list * Ty.t
  | `Term_def of
    Dolmen.Std.Id.t * T.Const.t * Ty.Var.t list * T.Var.t list * T.t ]
    list

Parse a definition

val parse : T.t typer

Parse a formula

package dolmen_type