sig
  module type Id = Ast_zf.Id
  module type Term = Ast_zf.Term
  module type Statement = Ast_zf.Statement
  module Make :
    functor
      (L : ParseLocation.S) (I : Id) (T : sig
                                            type t
                                            val tType : t
                                            val wildcard : t
                                            val prop : t
                                            val true_ : t
                                            val false_ : t
                                            val const : ?loc:L.t -> I.t -> t
                                            val apply :
                                              ?loc:L.t -> t -> t list -> t
                                            val colon :
                                              ?loc:L.t -> t -> t -> t
                                            val arrow :
                                              ?loc:L.t -> t -> t -> t
                                            val eq : ?loc:L.t -> t -> t -> t
                                            val not_ : ?loc:L.t -> t -> t
                                            val or_ : ?loc:L.t -> t list -> t
                                            val and_ :
                                              ?loc:L.t -> t list -> t
                                            val imply :
                                              ?loc:L.t -> t -> t -> t
                                            val equiv :
                                              ?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
                                          end) (S : sig
                                                      type t
                                                      val data :
                                                        ?loc:L.t ->
                                                        t list -> t
                                                      val decl :
                                                        ?loc:L.t ->
                                                        I.t -> T.t -> t
                                                      val definition :
                                                        ?loc:L.t ->
                                                        I.t ->
                                                        T.t -> T.t -> t
                                                      val inductive :
                                                        ?loc:L.t ->
                                                        I.t ->
                                                        T.t list ->
                                                        (I.t * T.t list) list ->
                                                        t
                                                      val rewrite :
                                                        ?loc:L.t ->
                                                        ?attr:T.t -> T.t -> t
                                                      val goal :
                                                        ?loc:L.t ->
                                                        ?attr:T.t -> T.t -> t
                                                      val assume :
                                                        ?loc:L.t ->
                                                        ?attr:T.t -> 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 :
                  ('-> 'answer) ->
                  ('a checkpoint -> 'answer) ->
                  supplier -> 'a checkpoint -> 'answer
                val loop_handle_undo :
                  ('-> '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