diff options
Diffstat (limited to 'contrib/jprover/jlogic.mli')
| -rw-r--r-- | contrib/jprover/jlogic.mli | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/contrib/jprover/jlogic.mli b/contrib/jprover/jlogic.mli new file mode 100644 index 00000000..a9079791 --- /dev/null +++ b/contrib/jprover/jlogic.mli @@ -0,0 +1,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 |