sig
module Make :
functor
(L : ParseLocation.S) (I : Id_intf.Logic) (T : sig
type t
val eq_t : t
val neq_t : t
val wildcard : t
val tType : t
val prop : t
val true_ : t
val false_ : 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 implied_t : t
val implies_t : t
val data_t : t
val var :
?loc:L.t -> I.t -> t
val const :
?loc:L.t -> I.t -> t
val atom :
?loc:L.t -> int -> 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 hexa :
?loc:L.t ->
string -> t
val binary :
?loc:L.t ->
string -> t
val colon :
?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 apply :
?loc:L.t ->
t -> t list -> t
val ite :
?loc:L.t ->
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 arrow :
?loc:L.t ->
t -> t -> t
val product :
?loc:L.t ->
t -> t -> t
val union :
?loc:L.t ->
t -> t -> t
val subtype :
?loc:L.t ->
t -> t -> t
val sequent :
?loc:L.t ->
t list ->
t list -> t
val annot :
?loc:L.t ->
t -> t list -> t
val sexpr :
?loc:L.t ->
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 p_cnf :
?loc:
L.t ->
int ->
int -> t
val clause :
?loc:
L.t ->
T.t list ->
t
val assumption :
?loc:
L.t ->
T.t list ->
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
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
val inductive :
?loc:
L.t ->
I.t ->
T.t list ->
(I.t *
T.t list)
list ->
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 goal :
?loc:
L.t ->
?attr:
T.t ->
T.t -> t
val assume :
?loc:
L.t ->
?attr:
T.t ->
T.t -> t
val rewrite :
?loc:
L.t ->
?attr:
T.t ->
T.t -> t
end) ->
sig
exception Extension_not_found of string
type language = Dimacs | ICNF | Smtlib | Tptp | Zf
val enum : (string * Logic.Make.language) list
val string_of_language : Logic.Make.language -> string
val find :
?language:Logic.Make.language ->
?dir:string -> string -> string option
val parse_file :
?language:Logic.Make.language ->
string -> Logic.Make.language * S.t list
val parse_input :
?language:Logic.Make.language ->
[ `File of string | `Stdin of Logic.Make.language ] ->
Logic.Make.language * (unit -> S.t option)
module type S =
sig
type token
module Lexer :
sig exception Error val token : Lexing.lexbuf -> token end
module Parser :
sig
exception Error
val file :
(Lexing.lexbuf -> token) -> Lexing.lexbuf -> S.t list
val input :
(Lexing.lexbuf -> token) -> Lexing.lexbuf -> S.t 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 ->
S.t option MenhirInterpreter.checkpoint
end
end
val find : ?dir:string -> string -> string option
val parse_file : string -> S.t list
val parse_input :
[ `File of string | `Stdin ] -> unit -> S.t option
end
val of_language :
Logic.Make.language ->
Logic.Make.language * string * (module Logic.Make.S)
val of_extension :
string -> Logic.Make.language * string * (module Logic.Make.S)
end
end