functor
  (L : ParseLocation.S) (I : Id) (T : sig
                                        type t
                                        val eq_t : t
                                        val neq_t : t
                                        val not_t : t
                                        val or_t : t
                                        val and_t : t
                                        val xor_t : t
                                        val nor_t : t
                                        val nand_t : t
                                        val equiv_t : t
                                        val implies_t : t
                                        val implied_t : t
                                        val data_t : t
                                        val colon : ?loc:L.t -> t -> t -> t
                                        val var : ?loc:L.t -> I.t -> t
                                        val const : ?loc:L.t -> I.t -> t
                                        val distinct : ?loc:L.t -> I.t -> t
                                        val int : ?loc:L.t -> string -> t
                                        val rat : ?loc:L.t -> string -> t
                                        val real : ?loc:L.t -> string -> t
                                        val apply :
                                          ?loc:L.t -> t -> t list -> t
                                        val ite :
                                          ?loc:L.t -> t -> t -> t -> t
                                        val union : ?loc:L.t -> t -> t -> t
                                        val product : ?loc:L.t -> t -> t -> t
                                        val arrow : ?loc:L.t -> t -> t -> t
                                        val subtype : ?loc:L.t -> t -> t -> t
                                        val pi : ?loc:L.t -> t list -> t -> 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 lambda :
                                          ?loc:L.t -> t list -> t -> t
                                        val choice :
                                          ?loc:L.t -> t list -> t -> t
                                        val description :
                                          ?loc:L.t -> t list -> t -> t
                                        val sequent :
                                          ?loc:L.t -> t list -> t list -> t
                                      end) (S : sig
                                                  type t
                                                  val annot :
                                                    ?loc:L.t ->
                                                    T.t -> T.t list -> T.t
                                                  val include_ :
                                                    ?loc:L.t ->
                                                    string -> I.t list -> t
                                                  val tpi :
                                                    ?loc:L.t ->
                                                    ?annot:T.t ->
                                                    I.t -> string -> T.t -> t
                                                  val thf :
                                                    ?loc:L.t ->
                                                    ?annot:T.t ->
                                                    I.t -> string -> T.t -> t
                                                  val tff :
                                                    ?loc:L.t ->
                                                    ?annot:T.t ->
                                                    I.t -> string -> T.t -> t
                                                  val fof :
                                                    ?loc:L.t ->
                                                    ?annot:T.t ->
                                                    I.t -> string -> T.t -> t
                                                  val cnf :
                                                    ?loc:L.t ->
                                                    ?annot:T.t ->
                                                    I.t -> string -> T.t -> 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