blob: 0aabc79ee70c81461cb3ad792cbdf6f8dbeb9392 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
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 *)
|
