home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 2 / Apprentice-Release2.iso / Tools / Languages / Caml Light 0.61 / Binaries / examples / kb / order.ml < prev    next >
Encoding:
Text File  |  1993-09-24  |  2.6 KB  |  81 lines  |  [TEXT/ttxt]
  1. (*********************** Recursive Path Ordering ****************************)
  2.  
  3. #open "prelude";;
  4. #open "terms";;
  5.  
  6. type ordering = Greater | Equal | NotGE;;
  7.  
  8. let ge_ord order pair = match order pair with NotGE -> false | _ -> true
  9. and gt_ord order pair = match order pair with Greater -> true | _ -> false
  10. and eq_ord order pair = match order pair with Equal -> true | _ -> false
  11. ;;
  12.  
  13. let rem_eq equiv = remrec where rec remrec x = function
  14.      []  -> failwith "rem_eq"
  15.   | y::l -> if equiv (x,y) then l else y :: remrec x l
  16. ;;
  17.  
  18. let diff_eq equiv (x,y) =
  19.   let rec diffrec = function
  20.       ([],_) as p -> p
  21.     | (h::t, y)   -> try diffrec (t,rem_eq equiv h y)
  22.                      with Failure _ ->
  23.                        let (x',y') = diffrec (t,y) in (h::x',y') in
  24.   if list_length x > list_length y then
  25.     let (y',x') = diffrec(y,x) in (x', y')
  26.   else
  27.     diffrec(x,y)
  28. ;;
  29.  
  30. (* multiset extension of order *)
  31. let mult_ext order = function
  32.     Term(_,sons1), Term(_,sons2) ->
  33.       begin match diff_eq (eq_ord order) (sons1,sons2) with
  34.            ([],[]) -> Equal
  35.          | (l1,l2) ->
  36.               if for_all (fun N -> exists (fun M -> order(M,N)=Greater) l1) l2
  37.               then Greater else NotGE
  38.       end
  39.   | _ -> failwith "mult_ext"
  40. ;;
  41.  
  42. (* lexicographic extension of order *)
  43. let lex_ext order = function
  44.     (Term(_,sons1) as M), (Term(_,sons2) as N) ->
  45.       let rec lexrec = function
  46.         ([] , []) -> Equal
  47.       | ([] , _ ) -> NotGE
  48.       | ( _ , []) -> Greater
  49.       | (x1::l1, x2::l2) ->
  50.           match order (x1,x2) with
  51.             Greater -> if for_all (fun N' -> gt_ord order (M,N')) l2 
  52.                        then Greater else NotGE
  53.           | Equal -> lexrec (l1,l2)
  54.           | NotGE -> if exists (fun M' -> ge_ord order (M',N)) l1 
  55.                      then Greater else NotGE in
  56.       lexrec (sons1, sons2)
  57.   | _ -> failwith "lex_ext"
  58. ;;
  59.  
  60. (* recursive path ordering *)
  61. let rpo op_order ext = rporec
  62.   where rec rporec (M,N) =
  63.     if M=N then Equal else 
  64.       match M with
  65.           Var m -> NotGE
  66.         | Term(op1,sons1) ->
  67.             match N with
  68.                 Var n ->
  69.                   if occurs n M then Greater else NotGE
  70.               | Term(op2,sons2) ->
  71.                   match (op_order op1 op2) with
  72.                       Greater ->
  73.                         if for_all (fun N' -> gt_ord rporec (M,N')) sons2
  74.                         then Greater else NotGE
  75.                     | Equal ->
  76.                         ext rporec (M,N)
  77.                     | NotGE ->
  78.                         if exists (fun M' -> ge_ord rporec (M',N)) sons1
  79.                         then Greater else NotGE
  80. ;;
  81.