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