blob: a9079791100009ddb11c5d0e9316c2e97d51e21c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
(* The interface to manipulate [jterms], which is
extracted and modified from Meta-Prl. *)
type rule =
Ax | Andr | Andl | Orr | Orr1 | Orr2 | Orl | Impr | Impl | Negr | Negl
| Allr | Alll| Exr | Exl | Fail | Falsel | Truer
module type JLogicSig =
sig
val is_all_term : Jterm.term -> bool
val dest_all : Jterm.term -> string * Jterm.term * Jterm.term
val is_exists_term : Jterm.term -> bool
val dest_exists : Jterm.term -> string * Jterm.term * Jterm.term
val is_and_term : Jterm.term -> bool
val dest_and : Jterm.term -> Jterm.term * Jterm.term
val is_or_term : Jterm.term -> bool
val dest_or : Jterm.term -> Jterm.term * Jterm.term
val is_implies_term : Jterm.term -> bool
val dest_implies : Jterm.term -> Jterm.term * Jterm.term
val is_not_term : Jterm.term -> bool
val dest_not : Jterm.term -> Jterm.term
type inf_step = rule * (string * Jterm.term) * (string * Jterm.term)
type inference = inf_step list
val empty_inf : inference
val append_inf :
inference -> (string * Jterm.term) -> (string * Jterm.term) -> rule -> inference
val print_inf : inference -> unit
end
module JLogic : JLogicSig
val show_loading : string -> unit
type my_Debug = {
mutable debug_name : string;
mutable debug_description : string;
debug_value : bool;
}
val create_debug : 'a -> bool ref
val ruletable : rule -> string
|
