Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 35 insertions, 0 deletions

diff --git a/contrib/jprover/jtunify.mli b/contrib/jprover/jtunify.mli
new file mode 100644
index 00000000..0aabc79e
--- /dev/null
+++ b/contrib/jprover/jtunify.mli
@@ -0,0 +1,35 @@
+exception Not_unifiable
+exception Failed
+
+(* Utilities *)
+
+val is_const : string -> bool
+val is_var : string -> bool
+val r_1 : 'a list -> 'b list -> 'c list -> bool
+val r_2 : 'a list -> 'b list -> 'c list -> bool
+val r_3 : 'a list -> 'b list -> 'a list -> bool
+val r_4 : string list -> 'a list -> string list -> bool
+val r_5 : string list -> 'a -> 'b list -> bool
+val r_6 : string list -> 'a list -> string list -> bool
+val r_7 : string list -> 'a -> string list -> bool
+val r_8 : string list -> 'a list -> string list -> bool
+val r_9 : string list -> 'a list -> string list -> bool
+val r_10 : string list -> 'a -> string list -> bool
+val com_subst : 'a list -> 'a * 'a list -> 'a list
+
+(* Debugging *)
+
+val print_equations : (string list * (string list * string list)) list -> unit
+
+val print_tunify : int * (string * string list) list -> unit
+
+(* Main function *)
+
+val do_stringunify : string list ->
+                     string list ->
+                     string ->
+                     string ->
+                     (string list * (string list * string list)) list ->
+                     (int * (string * string list) list) *                 (* unifier *)
+                     (int * ((string list * (string list * string list)) list))    (* applied new eqlist *)
+