dolmen_loop 0.9 (latest) · OCaml Package

This modules defines a wrapper around the bare-bones typechecker provided by Dolmen_type. It provides convenience function to match on Dolmen untyped statements and type-check them.

include Types

type state

type ty

type ty_var

type ty_cst

type ty_def

type term

type term_var

type term_cst

type formula

type env

type input = [

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

]

type lang = [

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

]

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

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

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

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

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

val defs : 
  mode:[ `Create_id | `Use_declared_id ] ->
  state ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.defs ->
  state
  * [ `Type_alias of Dolmen.Std.Id.t * ty_cst * ty_var list * ty
    | `Term_def of
      Dolmen.Std.Id.t * term_cst * ty_var list * term_var list * term
    | `Instanceof of
      Dolmen.Std.Id.t * term_cst * ty list * ty_var list * term_var list * term ]
      list

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

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

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

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

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

package dolmen_loop