package dolmen_model

You can search for identifiers within the package.

in-package search v0.2.0

dolmen_model
- Dolmen_model
  - Adt
  - Array
  - Bitv
  - Bool
  - Coercion
  - Core
  - Env
  - Eval
  - Fp
  - Fun
  - Int
  - Loop
    
    Make
    
    Parse
    
    State
    
    Typer
    
    Typer_Pipe
  - Model
    
    Cst
    
    S
    
    Var
  - Rat
  - Real
  - Value

Legend:
Library
Module
Module type
Parameter
Class
Class type

type env = Dolmen_loop.Typer.T.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.

val ty_state : Dolmen_loop.Typer.ty_state State.key

Key to store the local typechecking state in the global pipeline state.

val check_model : bool State.key

The typechecker needs to know whether we are checking models or not.

val smtlib2_forced_logic : string option State.key

Force the typechecker to use the given logic (instead of using the one declared in the `set-logic` statement).

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

include Dolmen_loop.Typer_intf.Typer
  with type env := env
   and type state := State.t
   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 ty_def := Dolmen.Std.Expr.ty_def
   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 Dolmen_loop.Typer_intf.Types
  with type env := env
  with type state := State.t
  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 ty_def := Dolmen.Std.Expr.ty_def
  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

type input = [

| `Logic of Dolmen_loop.Logic.language Dolmen_loop.State.file
| `Response of Dolmen_loop.Response.language Dolmen_loop.State.file

]

type lang = [

| `Logic of Dolmen_loop.Logic.language
| `Response of Dolmen_loop.Response.language

]

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

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

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

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

val set_logic : 
  State.t ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  string ->
  State.t * Dolmen_type.Logic.t

val defs : 
  mode:[ `Create_id | `Use_declared_id ] ->
  State.t ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.defs ->
  State.t
  * [ `Type_alias 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
    | `Instanceof of
      Dolmen.Std.Id.t
      * Dolmen.Std.Expr.term_cst
      * Dolmen.Std.Expr.ty list
      * Dolmen.Std.Expr.ty_var list
      * Dolmen.Std.Expr.term_var list
      * Dolmen.Std.Expr.term ]
      list

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

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

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

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

val typing_wrap : 
  ?attrs:Dolmen.Std.Term.t list ->
  ?loc:Dolmen.Std.Loc.t ->
  input:input ->
  State.t ->
  f:(env -> 'a) ->
  State.t * 'a

val init : 
  ?ty_state:Dolmen_loop.Typer.ty_state ->
  ?smtlib2_forced_logic:string option ->
  ?additional_builtins:(State.t -> lang -> builtin_symbols) ->
  State.t ->
  State.t

val additional_builtins : (State.t -> lang -> builtin_symbols) State.key

Add new builtin symbols to the typechecker, depending on the current language.

Note. The additional builtins are never used for Dimacs and iCNF.

before 0.9
additional_builtins had type builtin_symbols ref.

val report_error : input:input -> State.t -> error -> State.t

Report a typing error by calling the appropriate state function.

val report_warning : input:input -> State.t -> warning -> State.t

Return a typing warning by calling the appropriate state function.

val pop_inferred_model_constants : State.t -> Dolmen.Std.Expr.term_cst list

TODO:doc