dolmen_loop 0.10 · 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

]

type decl = [

| `Type_decl of Expr.ty_cst * Expr.ty_def option
| `Term_decl of Expr.term_cst

]

type def = [

| `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

]

type 'a ret = {

implicit_decls : decl list;
implicit_defs : def list;
ret : 'a;

}

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 decls : 
  State.t ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.decls ->
  State.t * decl list ret

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 * def list ret

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 ret

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 ret

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 ret

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