Imported Upstream version 8.0pl1upstream/8.0pl1

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