dolmen_loop 0.9 (latest) · OCaml Package

include Typer_intf.Types
  with type state := State.t
  with type ty := Expr.ty
  with type ty_var := Expr.ty_var
  with type ty_cst := Expr.ty_cst
  with type ty_def := Expr.ty_def
  with type term := Expr.term
  with type term_var := Expr.term_var
  with type term_cst := Expr.term_cst
  with type formula := Expr.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.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 * Expr.ty_cst * Expr.ty_var list * Expr.ty
    | `Term_def of
      Dolmen.Std.Id.t
      * Expr.term_cst
      * Expr.ty_var list
      * Expr.term_var list
      * Expr.term
    | `Instanceof of
      Dolmen.Std.Id.t
      * Expr.term_cst
      * Expr.ty list
      * Expr.ty_var list
      * Expr.term_var list
      * 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 Expr.ty_cst * Expr.ty_def option
    | `Term_decl of 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 * 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 * 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 * 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

package dolmen_loop