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 :
('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