sig
module type Id = Ast_tptp.Id
module type Term = Ast_tptp.Term
module type Statement = Ast_tptp.Statement
module Make :
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
end