summaryrefslogtreecommitdiff
path: root/contrib/jprover/jlogic.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /contrib/jprover/jlogic.mli
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'contrib/jprover/jlogic.mli')
-rw-r--r--contrib/jprover/jlogic.mli40
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