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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
(*********************** Recursive Path Ordering ****************************)
open Terms;;
type ordering = Greater | Equal | NotGE;;
let ge_ord order pair = match order pair with NotGE -> false | _ -> true
and gt_ord order pair = match order pair with Greater -> true | _ -> false
and eq_ord order pair = match order pair with Equal -> true | _ -> false
;;
let rem_eq equiv =
let rec remrec x = function
| [] -> failwith "rem_eq"
| y :: l -> if equiv (x, y) then l else y :: remrec x l in
remrec;;
let diff_eq equiv (x, y) =
let rec diffrec = function
| ([], _) as p -> p
| (h :: t, y) -> try diffrec (t, rem_eq equiv h y)
with Failure _ ->
let (x', y') = diffrec (t, y) in (h :: x', y') in
if List.length x > List.length y then
let (y', x') = diffrec (y, x) in (x', y')
else
diffrec (x, y)
;;
(* multiset extension of order *)
let mult_ext order = function
| Term (_, sons1), Term (_, sons2) ->
begin match diff_eq (eq_ord order) (sons1, sons2) with
| ([], []) -> Equal
| (l1, l2) ->
if List.for_all
(fun n -> List.exists (fun m -> order (m, n) = Greater) l1) l2
then Greater else NotGE
end
| _ -> failwith "mult_ext"
;;
(* lexicographic extension of order *)
let lex_ext order = function
| (Term (_, sons1) as m), (Term (_, sons2) as n) ->
let rec lexrec = function
| ([], []) -> Equal
| ([], _ ) -> NotGE
| ( _, []) -> Greater
| (x1 :: l1, x2 :: l2) ->
match order (x1, x2) with
| Greater -> if List.for_all (fun n' -> gt_ord order (m, n')) l2
then Greater else NotGE
| Equal -> lexrec (l1, l2)
| NotGE -> if List.exists (fun m' -> ge_ord order (m', n)) l1
then Greater else NotGE in
lexrec (sons1, sons2)
| _ -> failwith "lex_ext"
;;
(* recursive path ordering *)
let rpo op_order ext =
let rec rporec (m, n) =
if m = n then Equal else
match m with
| Var m -> NotGE
| Term (op1, sons1) ->
match n with
| Var n ->
if occurs n m then Greater else NotGE
| Term (op2, sons2) ->
match (op_order op1 op2) with
| Greater ->
if List.for_all (fun n' -> gt_ord rporec (m, n')) sons2
then Greater else NotGE
| Equal ->
ext rporec (m, n)
| NotGE ->
if List.exists (fun m' -> ge_ord rporec (m', n)) sons1
then Greater else NotGE in
rporec
;;
|
