Make (dolmen_loop.Dolmen_loop.Export.Make)

Parameters

module Expr : Expr_intf.Export

module Sexpr : 
  Dolmen_intf.View.Sexpr.S
    with type t = Dolmen_std.Term.t
     and type id := Dolmen_std.Id.t

module View : 
  Dolmen_intf.View.TFF.S
    with type ty = Expr.Ty.t
     and type ty_var = Expr.Ty.Var.t
     and type ty_cst = Expr.Ty.Const.t
     and type ty_def = Expr.ty_def
     and type term = Expr.Term.t
     and type term_var = Expr.Term.Var.t
     and type term_cst = Expr.Term.Const.t

module State : State.S

module Typer_Types : 
  Typer.Types
    with type ty = Expr.ty
     and type ty_var = Expr.ty_var
     and type ty_cst = Expr.ty_cst
     and type ty_def = Expr.ty_def
     and type term = Expr.term
     and type term_var = Expr.term_var
     and type term_cst = Expr.term_cst
     and type formula = Expr.term

Signature

module type S' =
  S
    with type st := State.t
     and type ty := Expr.ty
     and type ty_var := Expr.ty_var
     and type ty_cst := Expr.ty_cst
     and type ty_def := Expr.ty_def
     and type term := Expr.term
     and type term_var := Expr.term_var
     and type term_cst := Expr.term_cst
     and type formula := Expr.term

type 'acc printer = (module S' with type acc = 'acc)

type state =

| No_export : state
| Export : {
1. acc : 'acc;
2. printer : 'acc printer;
} -> state

module Dummy : sig ... end

module Smtlib2_6 : sig ... end

module Smtlib2_7 : sig ... end

module Smtlib2_Poly : sig ... end

val pipe : string

val state : state State.key

val init : ?output_file:file -> State.t -> State.t

val export : 
  State.t ->
  Typer_Types.typechecked Typer_Types.stmt list ->
  State.t * Typer_Types.typechecked Typer_Types.stmt list