sig
  module type Id = Ast_smtlib.Id
  module type Term = Ast_smtlib.Term
  module type Statement = Ast_smtlib.Statement
  module Make :
    functor
      (L : ParseLocation.S) (I : Id) (T : sig
                                            type t
                                            val const : ?loc:L.t -> I.t -> t
                                            val int : ?loc:L.t -> string -> t
                                            val real :
                                              ?loc:L.t -> string -> t
                                            val hexa :
                                              ?loc:L.t -> string -> t
                                            val binary :
                                              ?loc:L.t -> string -> t
                                            val colon :
                                              ?loc:L.t -> t -> t -> t
                                            val apply :
                                              ?loc:L.t -> t -> t list -> t
                                            val letin :
                                              ?loc:L.t -> t list -> t -> t
                                            val forall :
                                              ?loc:L.t -> t list -> t -> t
                                            val exists :
                                              ?loc:L.t -> t list -> t -> t
                                            val sexpr :
                                              ?loc:L.t -> t list -> t
                                            val annot :
                                              ?loc:L.t -> t -> t list -> t
                                          end) (S : sig
                                                      type t
                                                      val pop :
                                                        ?loc:L.t -> int -> t
                                                      val push :
                                                        ?loc:L.t -> int -> t
                                                      val assert_ :
                                                        ?loc:L.t -> T.t -> t
                                                      val check_sat :
                                                        ?loc:L.t -> unit -> t
                                                      val set_logic :
                                                        ?loc:L.t ->
                                                        string -> t
                                                      val get_info :
                                                        ?loc:L.t ->
                                                        string -> t
                                                      val set_info :
                                                        ?loc:L.t ->
                                                        string * T.t option ->
                                                        t
                                                      val get_option :
                                                        ?loc:L.t ->
                                                        string -> t
                                                      val set_option :
                                                        ?loc:L.t ->
                                                        string * T.t option ->
                                                        t
                                                      val type_decl :
                                                        ?loc:L.t ->
                                                        I.t -> int -> t
                                                      val type_def :
                                                        ?loc:L.t ->
                                                        I.t ->
                                                        I.t list -> T.t -> t
                                                      val fun_decl :
                                                        ?loc:L.t ->
                                                        I.t ->
                                                        T.t list -> T.t -> t
                                                      val fun_def :
                                                        ?loc:L.t ->
                                                        I.t ->
                                                        T.t list ->
                                                        T.t -> T.t -> t
                                                      val get_proof :
                                                        ?loc:L.t -> unit -> t
                                                      val get_unsat_core :
                                                        ?loc:L.t -> unit -> t
                                                      val get_value :
                                                        ?loc:L.t ->
                                                        T.t list -> t
                                                      val get_assignment :
                                                        ?loc:L.t -> unit -> t
                                                      val get_assertions :
                                                        ?loc:L.t -> unit -> t
                                                      val exit :
                                                        ?loc:L.t -> unit -> t
                                                    end) ->
      sig
        type token
        type statement = S.t
        module Lexer :
          sig exception Error val token : Lexing.lexbuf -> token end
        module Parser :
          sig
            exception Error
            val file :
              (Lexing.lexbuf -> token) -> Lexing.lexbuf -> statement list
            val input :
              (Lexing.lexbuf -> token) -> Lexing.lexbuf -> statement option
            module MenhirInterpreter :
              sig
                type token = token
                type env
                type production
                type 'a checkpoint = private
                    InputNeeded of env
                  | Shifting of env * env * bool
                  | AboutToReduce of env * production
                  | HandlingError of env
                  | Accepted of 'a
                  | Rejected
                val offer :
                  'a checkpoint ->
                  token * Lexing.position * Lexing.position -> 'a checkpoint
                val resume : 'a checkpoint -> 'a checkpoint
                type supplier =
                    unit -> token * Lexing.position * Lexing.position
                val lexer_lexbuf_to_supplier :
                  (Lexing.lexbuf -> token) -> Lexing.lexbuf -> supplier
                val loop : supplier -> 'a checkpoint -> 'a
                val loop_handle :
                  ('a -> 'answer) ->
                  ('a checkpoint -> 'answer) ->
                  supplier -> 'a checkpoint -> 'answer
                val loop_handle_undo :
                  ('a -> 'answer) ->
                  ('a checkpoint -> 'a checkpoint -> 'answer) ->
                  supplier -> 'a checkpoint -> 'answer
                val loop_test :
                  (env -> 'accu -> 'accu) -> 'a checkpoint -> 'accu -> 'accu
                val acceptable :
                  'a checkpoint -> token -> Lexing.position -> bool
                type 'a lr1state
                val number : 'a lr1state -> int
                type element =
                    Element : 'a lr1state * 'a * Lexing.position *
                      Lexing.position -> element
                type stack = element MenhirLib.General.stream
                val stack : env -> stack
                val positions : env -> Lexing.position * Lexing.position
                val has_default_reduction : env -> bool
              end
            module Incremental :
              sig
                val input :
                  Lexing.position ->
                  statement option MenhirInterpreter.checkpoint
              end
          end
        val find : ?dir:string -> string -> string option
        val parse_file : string -> statement list
        val parse_input :
          [ `File of string | `Stdin ] -> unit -> statement option
      end
end