package dolmen_loop

You can search for identifiers within the package.

in-package search v0.2.0

package dolmen_loop

dolmen_loop
- Dolmen_loop
  - Code
  - Expr_intf
    
    Print
    
    S
  - Headers
    
    Field
    
    Pipe
    
    State
  - Headers_intf
    
    S
  - Logic
    
    S
    
    Lexer
    
    Parser
  - Parser
    
    Pipe
    
    Expr
    
    State
  - Pipeline
    
    Make
    
    State
  - Report
    
    Conf
    
    Error
    
    T
    
    Warning
    
    Status
  - State
  - State_intf
    
    Common
    
    Header_pipe
    
    Parser_pipe
    
    Pipeline
    
    Typer
    
    Typer_pipe
  - Typer
    
    Make
    
    S
    
    Pipe
    
    Expr
    
    Print
    
    State
    
    Typer
    
    T
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Typer_intf
    
    Pipe_arg
    
    Pipe_res
    
    Pipe_types
    
    S

Legend:
Library
Module
Module type
Parameter
Class
Class type

This modules defines the result signature of the Typer.Make functor

type state

The type of state for a whole pipeline.

type ty_state

The type for the state of the typer.

type env

The type of the typechecker environment.

type 'a fragment

The type of fragments on which error/warning can occur.

type error

The type of type-checking errors.

type warning

The type of type-checking warnings.

type builtin_symbols

The type of builin symbols for the type-checker.

This signature includes the requirements to instantiate the {Pipes.Make: functor

include Pipe_arg
  with type state := state
   and type ty := Dolmen.Std.Expr.ty
   and type ty_var := Dolmen.Std.Expr.ty_var
   and type ty_cst := Dolmen.Std.Expr.ty_cst
   and type term := Dolmen.Std.Expr.term
   and type term_var := Dolmen.Std.Expr.term_var
   and type term_cst := Dolmen.Std.Expr.term_cst
   and type formula := Dolmen.Std.Expr.formula

include Pipe_types
  with type state := state
  with type ty := Dolmen.Std.Expr.ty
  with type ty_var := Dolmen.Std.Expr.ty_var
  with type ty_cst := Dolmen.Std.Expr.ty_cst
  with type term := Dolmen.Std.Expr.term
  with type term_var := Dolmen.Std.Expr.term_var
  with type term_cst := Dolmen.Std.Expr.term_cst
  with type formula := Dolmen.Std.Expr.formula

val typecheck : state -> bool

val reset : state -> ?loc:Dolmen.Std.Loc.t -> unit -> state

val reset_assertions : state -> ?loc:Dolmen.Std.Loc.t -> unit -> state

val push : state -> ?loc:Dolmen.Std.Loc.t -> int -> state

val pop : state -> ?loc:Dolmen.Std.Loc.t -> int -> state

val set_logic : state -> ?loc:Dolmen.Std.Loc.t -> string -> state

val defs : 
  state ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.defs ->
  state
  * [ `Type_def of
        Dolmen.Std.Id.t
        * Dolmen.Std.Expr.ty_cst
        * Dolmen.Std.Expr.ty_var list
        * Dolmen.Std.Expr.ty
    | `Term_def of
      Dolmen.Std.Id.t
      * Dolmen.Std.Expr.term_cst
      * Dolmen.Std.Expr.ty_var list
      * Dolmen.Std.Expr.term_var list
      * Dolmen.Std.Expr.term ]
      list

val decls : 
  state ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.decls ->
  state
  * [ `Type_decl of Dolmen.Std.Expr.ty_cst
    | `Term_decl of Dolmen.Std.Expr.term_cst ]
      list

val terms : 
  state ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Term.t list ->
  state * Dolmen.Std.Expr.term list

val formula : 
  state ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  goal:bool ->
  Dolmen.Std.Term.t ->
  state * Dolmen.Std.Expr.formula

val formulas : 
  state ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Term.t list ->
  state * Dolmen.Std.Expr.formula list

val report_error : state -> error -> state

Report a typing error by calling the appropriate state function.

val report_warning : state -> warning -> state

Return a typing warning by calling the appropriate state function.

val additional_builtins : builtin_symbols ref

This reference can be modified to parse new builtin symbols. By default no additional builtin symbols are parsed. It is added for all the languages except Dimacs, and iCNF.