1 files changed, 106 insertions, 0 deletions
diff --git a/contrib/jprover/jlogic.ml b/contrib/jprover/jlogic.ml
new file mode 100644
index 00000000..c074e93e
--- /dev/null
+++ b/contrib/jprover/jlogic.ml
@@ -0,0 +1,106 @@
+open Opname
+open Jterm
+
+type rule =
+ | Ax | Andr | Andl | Orr | Orr1 | Orr2 | Orl | Impr | Impl | Negr | Negl
+ | Allr | Alll| Exr | Exl | Fail | Falsel | Truer
+
+let ruletable = function
+ | Fail -> "Fail"
+ | Ax ->     "Ax"
+ | Negl ->  "Negl"
+ | Negr ->  "Negr"
+ | Andl ->  "Andl"
+ | Andr ->  "Andr"
+ | Orl ->   "Orl"
+ | Orr ->   "Orr"
+ | Orr1 ->   "Orr1"
+ | Orr2 ->   "Orr2"
+ | Impl ->   "Impl"
+ | Impr ->   "Impr"
+ | Exl ->   "Exl"
+ | Exr ->   "Exr"
+ | Alll ->   "Alll"
+ | Allr ->   "Allr"
+ | Falsel -> "Falsel"
+ | Truer -> "Truer"
+
+module type JLogicSig =
+sig
+   (* understanding the input *)
+	val is_all_term	: term -> bool
+	val dest_all : term -> string * term * term
+	val is_exists_term : term -> bool
+	val dest_exists : term -> string * term * term
+	val is_and_term : term -> bool
+	val dest_and : term -> term * term
+	val is_or_term : term -> bool
+	val dest_or : term -> term * term
+	val is_implies_term : term -> bool
+	val dest_implies : term -> term * term
+	val is_not_term : term -> bool
+	val dest_not : term -> term 
+
+   (* processing the output *)
+   type inf_step = rule * (string * term) * (string * term)
+   type inference = inf_step list
+(* type inference *)
+   val empty_inf : inference
+   val append_inf : inference -> (string * term) -> (string * term) -> rule -> inference
+   val print_inf : inference -> unit
+end;;
+
+(* Copy from [term_op_std.ml]: *)
+
+   let rec print_address int_list =
+      match int_list with
+       | [] ->
+            Format.print_string ""
+       | hd::rest ->
+            begin
+               Format.print_int hd;
+               print_address rest
+            end
+
+module JLogic: JLogicSig =
+struct
+  let is_all_term = Jterm.is_all_term
+  let dest_all = Jterm.dest_all
+  let is_exists_term = Jterm.is_exists_term
+  let dest_exists = Jterm.dest_exists
+  let is_and_term = Jterm.is_and_term
+  let dest_and = Jterm.dest_and
+  let is_or_term = Jterm.is_or_term
+  let dest_or = Jterm.dest_or
+  let is_implies_term = Jterm.is_implies_term
+  let dest_implies = Jterm.dest_implies
+  let is_not_term = Jterm.is_not_term
+  let dest_not = Jterm.dest_not
+
+  type inf_step = rule * (string * term) * (string * term)
+  type inference = inf_step list
+
+  let empty_inf = []
+  let append_inf inf t1 t2 rule =
+    (rule, t1, t2)::inf
+
+  let rec print_inf inf =
+   match inf with
+  |  [] -> print_string "."; Format.print_flush ()
+  |  (rule, (n1,t1), (n2,t2))::d ->
+      print_string (ruletable rule);
+      print_string (":("^n1^":");
+      print_term stdout t1;
+      print_string (","^n2^":");
+      print_term stdout t2;
+      print_string ")\n";
+      print_inf d
+end;;
+
+let show_loading s = print_string s
+type my_Debug = { mutable debug_name: string;
+                  mutable debug_description: string;
+                  debug_value: bool
+                }
+
+let create_debug x = ref false