Module `Dolmen_loop.Typer`

Typechecker state

type ty_state: The type of state used by the Make functor.

val new_state : unit -> ty_state: Generate a fresh typing state. The bool argument given decides whether locations are kept (provides better error messages, but uses more memory when running).

module T : Dolmen_type.Tff.S with type 'a Tag.t = 'a Dolmen_std.Tag.t and type Ty.t = Dolmen_std.Expr.ty and type Ty.Var.t = Dolmen_std.Expr.ty_var and type Ty.Const.t = Dolmen_std.Expr.ty_const and type T.t = Dolmen_std.Expr.term and type T.Var.t = Dolmen_std.Expr.term_var and type T.Const.t = Dolmen_std.Expr.term_const and type T.Cstr.t = Dolmen_std.Expr.term_const: The raw type-checker module.

Typechecker Functor

module type S = Typer_intf.S

module Make : functor (S : State_intf.Typer with type ty_state := ty_state) -> S with type state := S.t and type ty_state := ty_state and type env := T.env and type 'a fragment := 'a T.fragment and type error := T.error and type warning := T.warning and type builtin_symbols := T.builtin_symbols

Typechecker Pipe

module type Pipe_arg = Typer_intf.Pipe_arg

module type Pipe_res = Typer_intf.Pipe_res

module Pipe : functor (Expr : Expr_intf.S) -> functor (State : State_intf.Typer_pipe) -> functor (Typer : Pipe_arg with type state := State.t and type ty := Expr.ty and type ty_var := Expr.ty_var and type ty_const := Expr.ty_const and type term := Expr.term and type term_var := Expr.term_var and type term_const := Expr.term_const and type formula := Expr.formula) -> Pipe_res with type state := State.t and type ty := Expr.ty and type ty_var := Expr.ty_var and type ty_const := Expr.ty_const and type term := Expr.term and type term_var := Expr.term_var and type term_const := Expr.term_const and type formula := Expr.formula