# mutated_ocaml / testsuite / tests / misc-kb / orderings.ml

 ``` 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 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98``` ```(***********************************************************************) (* *) (* OCaml *) (* *) (* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) (* *) (* Copyright 1996 Institut National de Recherche en Informatique et *) (* en Automatique. All rights reserved. This file is distributed *) (* under the terms of the Q Public License version 1.0. *) (* *) (***********************************************************************) (* \$Id: orderings.ml 12800 2012-07-30 18:59:07Z doligez \$ *) (*********************** 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 rec rem_eq equiv x = function [] -> failwith "rem_eq" | y::l -> if equiv (x,y) then l else y :: rem_eq equiv x l 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 diffrec(y,x) 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 -> gt_ord order (m,n)) 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 vm -> NotGE | Term(op1,sons1) -> match n with Var vn -> if occurs vn 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 ```