let print_string _ = ()

let print_int _ = ()

let print_newline _ = ()

(***********************************************************************)
(*                                                                     *)
(*                           Objective Caml                            *)
(*                                                                     *)
               , 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 .               
(*                                                                     *)
(***********************************************************************)

  $ I d : terms.ml 2553 1999 - 11 - 17 18:59:06Z xleroy $

(****************** Term manipulations *****************)

type term =
  | Var of int
  | Term of string * term list

let rec union l1 l2 =
  match l1 with
  | [] -> l2
  | a :: r -> if List.mem a l2 then union r l2 else a :: union r l2

let rec vars = function Var n -> [n] | Term (_, l) -> vars_of_list l

and vars_of_list = function [] -> [] | t :: r -> union (vars t) (vars_of_list r)

let rec substitute subst = function
  | Term (oper, sons) -> Term (oper, List.map (substitute subst) sons)
  | Var n as t -> ( try List.assoc n subst with Not_found -> t )

  Term replacement : replace M u N is M[u<-N ] .

let rec replace m u n =
  match u, m with
  | [], _ -> n
  | i :: u, Term (oper, sons) -> Term (oper, replace_nth i sons u n)
  | _ -> failwith "replace"

and replace_nth i sons u n =
  match sons with
  | s :: r -> if i = 1 then replace s u n :: r else s :: replace_nth (i - 1) r u n
  | [] -> failwith "replace_nth"

(* Term matching. *)

let matching term1 term2 =
  let rec match_rec subst t1 t2 =
    match t1, t2 with
    | Var v, _ ->
        if List.mem_assoc v subst
        then if t2 = List.assoc v subst then subst else failwith "matching"
        else (v, t2) :: subst
    | Term (op1, sons1), Term (op2, sons2) ->
        if op1 = op2
        then List.fold_left2 match_rec subst sons1 sons2
        else failwith "matching"
    | _ -> failwith "matching"
  in
  match_rec [] term1 term2

(* A naive unification algorithm. *)

let compsubst subst1 subst2 =
  List.map (fun (v, t) -> v, substitute subst1 t) subst2 @ subst1

let rec occurs n = function
  | Var m -> m = n
  | Term (_, sons) -> List.exists (occurs n) sons

let rec unify term1 term2 =
  match term1, term2 with
  | Var n1, _ ->
      if term1 = term2
      then []
      else if occurs n1 term2
      then failwith "unify"
      else [n1, term2]
  | term1, Var n2 -> if occurs n2 term1 then failwith "unify" else [n2, term1]
  | Term (op1, sons1), Term (op2, sons2) ->
      if op1 = op2
      then
        List.fold_left2
          (fun s t1 t2 -> compsubst (unify (substitute s t1) (substitute s t2)) s)
          []
          sons1
          sons2
      else failwith "unify"

(* We need to print terms with variables independently from input terms
  obtained by parsing. We give arbitrary names v1,v2,... to their variables.
*)

let infixes = ["+"; "*"]

let pretty_term _ = ()

let pretty_close _ = ()

(***********************************************************************)
(*                                                                     *)
(*                           Objective Caml                            *)
(*                                                                     *)
               , 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: equations.ml 2553 1999-11-17 18:59:06Z xleroy $ *)

(****************** Equation manipulations *************)

type rule =
  { number : int
  ; numvars : int
  ; lhs : term
  ; rhs : term }

(* standardizes an equation so its variables are 1,2,... *)

let mk_rule num m n =
  let all_vars = union (vars m) (vars n) in
  let counter = ref 0 in
  let subst = List.map (fun v -> incr counter; v, Var !counter) (List.rev all_vars) in
  {number = num; numvars = !counter; lhs = substitute subst m; rhs = substitute subst n}

(* checks that rules are numbered in sequence and returns their number *)

let check_rules rules =
  let counter = ref 0 in
  List.iter
    (fun r ->
      incr counter;
      if r.number <> !counter then failwith "Rule numbers not in sequence" )
    rules;
  !counter

let pretty_rule rule =
  print_int rule.number;
  print_string " : ";
  pretty_term rule.lhs;
  print_string " = ";
  pretty_term rule.rhs;
  print_newline ()

let pretty_rules rules = List.iter pretty_rule rules

(****************** Rewriting **************************)

  Top - level rewriting . Let eq : L = R be an equation , M be a term such that L<=M. 
    With sigma = matching L M , we define the image of M by eq as sigma(R )
   With sigma = matching L M, we define the image of M by eq as sigma(R) *)
let reduce l m r = substitute (matching l m) r

  Test whether m can be reduced by l , i.e. m contains an instance of l.

let can_match l m =
  try
    let _ = matching l m in
    true
  with Failure _ -> false

let rec reducible l m =
  can_match l m
  || match m with Term (_, sons) -> List.exists (reducible l) sons | _ -> false

(* Top-level rewriting with multiple rules. *)

let rec mreduce rules m =
  match rules with
  | [] -> failwith "mreduce"
  | rule :: rest -> ( try reduce rule.lhs m rule.rhs with Failure _ -> mreduce rest m )

  One step of rewriting in leftmost - outermost strategy , 
    with multiple rules . Fails if no redex is found
   with multiple rules. Fails if no redex is found *)

let rec mrewrite1 rules m =
  try mreduce rules m with Failure _ -> (
    match m with
    | Var _ -> failwith "mrewrite1"
    | Term (f, sons) -> Term (f, mrewrite1_sons rules sons) )

and mrewrite1_sons rules = function
  | [] -> failwith "mrewrite1"
  | son :: rest -> (
    try mrewrite1 rules son :: rest with Failure _ -> son :: mrewrite1_sons rules rest )

(* Iterating rewrite1. Returns a normal form. May loop forever *)

let rec mrewrite_all rules m =
  try mrewrite_all rules (mrewrite1 rules m) with Failure _ -> m

(***********************************************************************)
(*                                                                     *)
(*                           Objective Caml                            *)
(*                                                                     *)
               , 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 .               
(*                                                                     *)
(***********************************************************************)

  $ I d : orderings.ml 2553 1999 - 11 - 17 18:59:06Z xleroy $

(*********************** Recursive Path Ordering ****************************)

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) -> (
    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 )
  | _ -> failwith "mult_ext"

   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 _ -> 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

(***********************************************************************)
(*                                                                     *)
(*                           Objective Caml                            *)
(*                                                                     *)
               , 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 .               
(*                                                                     *)
(***********************************************************************)

  $ I d :  2553 1999 - 11 - 17 18:59:06Z xleroy $

(****************** Critical pairs *********************)

  All ( u , subst ) such that N / u ( & var ) unifies with M , 
    with principal unifier subst
   with principal unifier subst *)

let rec super m = function
  | Term (_, sons) as n -> (
      let rec collate n = function
        | [] -> []
        | son :: rest ->
            List.map (fun (u, subst) -> n :: u, subst) (super m son)
            @ collate (n + 1) rest
      in
      let insides = collate 1 sons in
      try ([], unify m n) :: insides with Failure _ -> insides )
  | _ -> []

  Ex : 
 let ( m , _ ) = < < F(A , B ) > > 
 and ( n , _ ) = < < H(F(A , x),F(x , y ) ) > > in super m n 
 = = > [ [ 1],[2,Term ( " B " , [ ] ) ] ;                       x < - B 
      [ 2],[2,Term ( " A " , [ ] ) ; 1,Term ( " B " , [ ] ) ] ]      x < - A   y < - B 

let (m,_) = <<F(A,B)>>
and (n,_) = <<H(F(A,x),F(x,y))>> in super m n
==> [[1],[2,Term ("B",[])];                      x <- B
     [2],[2,Term ("A",[]); 1,Term ("B",[])]]     x <- A  y <- B
*)

  All ( u , subst ) , u & [ ] , such that n / u unifies with m

let super_strict m = function
  | Term (_, sons) ->
      let rec collate n = function
        | [] -> []
        | son :: rest ->
            List.map (fun (u, subst) -> n :: u, subst) (super m son)
            @ collate (n + 1) rest
      in
      collate 1 sons
  | _ -> []

(* Critical pairs of l1=r1 with l2=r2 *)
(* critical_pairs : term_pair -> term_pair -> term_pair list *)
let critical_pairs (l1, r1) (l2, r2) =
  let mk_pair (u, subst) = substitute subst (replace l2 u r1), substitute subst r2 in
  List.map mk_pair (super l1 l2)

(* Strict critical pairs of l1=r1 with l2=r2 *)
  strict_critical_pairs : term_pair - > term_pair - > term_pair list
let strict_critical_pairs (l1, r1) (l2, r2) =
  let mk_pair (u, subst) = substitute subst (replace l2 u r1), substitute subst r2 in
  List.map mk_pair (super_strict l1 l2)

  All critical pairs of eq1 with eq2
let mutual_critical_pairs eq1 eq2 =
  strict_critical_pairs eq1 eq2 @ critical_pairs eq2 eq1

(* Renaming of variables *)

let rename n (t1, t2) =
  let rec ren_rec = function
    | Var k -> Var (k + n)
    | Term (op, sons) -> Term (op, List.map ren_rec sons)
  in
  ren_rec t1, ren_rec t2

(************************ Completion ******************************)

let deletion_message rule =
  print_string "Rule "; print_int rule.number; print_string " deleted"; print_newline ()

(* Generate failure message *)
let non_orientable (m, n) =
  pretty_term m; print_string " = "; pretty_term n; print_newline ()

let rec partition p = function
  | [] -> [], []
  | x :: l ->
      let l1, l2 = partition p l in
      if p x then x :: l1, l2 else l1, x :: l2

let rec get_rule n = function
  | [] -> raise Not_found
  | r :: l -> if n = r.number then r else get_rule n l

  Improved Knuth - Bendix completion procedure

let kb_completion greater =
  let rec kbrec j rules =
    let rec process failures (k, l) eqs =
* * * 
      print_string " * * * kb_completion " ; print_int j ; print_newline ( ) ; 
      pretty_rules rules ; 
      List.iter non_orientable failures ; 
      print_int k ; print_string " " ; print_int l ; print_newline ( ) ; 
      List.iter non_orientable eqs ; 
 * *
     print_string "***kb_completion "; print_int j; print_newline();
     pretty_rules rules;
     List.iter non_orientable failures;
     print_int k; print_string " "; print_int l; print_newline();
     List.iter non_orientable eqs;
***)
      match eqs with
      | [] -> (
          if k < l
          then next_criticals failures (k + 1, l)
          else if l < j
          then next_criticals failures (1, l + 1)
          else
            match failures with
            | [] -> rules (* successful completion *)
            | _ ->
                print_string "Non-orientable equations :";
                print_newline ();
                List.iter non_orientable failures;
                failwith "kb_completion" )
      | (m, n) :: eqs ->
          let m' = mrewrite_all rules m
          and n' = mrewrite_all rules n
          and enter_rule (left, right) =
            let new_rule = mk_rule (j + 1) left right in
            pretty_rule new_rule;
            let left_reducible rule = reducible left rule.lhs in
            let redl, irredl = partition left_reducible rules in
            List.iter deletion_message redl;
            let right_reduce rule =
              mk_rule rule.number rule.lhs (mrewrite_all (new_rule :: rules) rule.rhs)
            in
            let irreds = List.map right_reduce irredl in
            let eqs' = List.map (fun rule -> rule.lhs, rule.rhs) redl in
            kbrec (j + 1) (new_rule :: irreds) [] (k, l) (eqs @ eqs' @ failures)
          in
          (***
        print_string "--- Considering "; non_orientable (m', n');
***)
          if m' = n'
          then process failures (k, l) eqs
          else if greater (m', n')
          then enter_rule (m', n')
          else if greater (n', m')
          then enter_rule (n', m')
          else process ((m', n') :: failures) (k, l) eqs
    and next_criticals failures (k, l) =
* * * 
     print_string " * * * next_criticals " ; 
     print_int k ; print_string " " ; print_int l ; print_newline ( ) ; 
 * * *
    print_string "***next_criticals ";
    print_int k; print_string " "; print_int l ; print_newline();
****)
      try
        let rl = get_rule l rules in
        let el = rl.lhs, rl.rhs in
        if k = l
        then process failures (k, l) (strict_critical_pairs el (rename rl.numvars el))
        else
          try
            let rk = get_rule k rules in
            let ek = rk.lhs, rk.rhs in
            process failures (k, l) (mutual_critical_pairs el (rename rl.numvars ek))
          with Not_found -> next_criticals failures (k + 1, l)
      with Not_found -> next_criticals failures (1, l + 1)
    in
    process
  in
  kbrec

  complete_rules is assumed locally confluent , and checked  with 
   ordering greater , rules is any list of rules
  ordering greater, rules is any list of rules *)

let kb_complete greater complete_rules rules =
  let n = check_rules complete_rules
  and eqs = List.map (fun rule -> rule.lhs, rule.rhs) rules in
  let completed_rules = kb_completion greater n complete_rules [] (n, n) eqs in
  print_string "Canonical set found :";
  print_newline ();
  pretty_rules (List.rev completed_rules)

(***********************************************************************)
(*                                                                     *)
(*                           Objective Caml                            *)
(*                                                                     *)
               , 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 .               
(*                                                                     *)
(***********************************************************************)

  $ I d : kbmain.ml 7017 2005 - 08 - 12 09:22:04Z xleroy $

* * * 
 let group_rules = [ 
   { number = 1 ; numvars = 1 ; 
     lhs = Term ( " * " , [ Term("U " , [ ] ) ; Var 1 ] ) ; rhs = Var 1 } ; 
   { number = 2 ; numvars = 1 ; 
     lhs = Term ( " * " , [ Term("I",[Var 1 ] ) ; Var 1 ] ) ; rhs = Term("U " , [ ] ) } ; 
   { number = 3 ; numvars = 3 ; 
     lhs = Term ( " * " , [ Term ( " * " , [ Var 1 ; Var 2 ] ) ; Var 3 ] ) ; 
     rhs = Term ( " * " , [ Var 1 ; Term ( " * " , [ Var 2 ; Var 3 ] ) ] ) } 
 ] 
 * * *
let group_rules = [
  { number = 1; numvars = 1;
    lhs = Term("*", [Term("U",[]); Var 1]); rhs = Var 1 };
  { number = 2; numvars = 1;
    lhs = Term("*", [Term("I",[Var 1]); Var 1]); rhs = Term("U",[]) };
  { number = 3; numvars = 3;
    lhs = Term("*", [Term("*", [Var 1; Var 2]); Var 3]);
    rhs = Term("*", [Var 1; Term("*", [Var 2; Var 3])]) }
]
****)

let geom_rules =
  [ {number = 1; numvars = 1; lhs = Term ("*", [Term ("U", []); Var 1]); rhs = Var 1}
  ; { number = 2
    ; numvars = 1
    ; lhs = Term ("*", [Term ("I", [Var 1]); Var 1])
    ; rhs = Term ("U", []) }
  ; { number = 3
    ; numvars = 3
    ; lhs = Term ("*", [Term ("*", [Var 1; Var 2]); Var 3])
    ; rhs = Term ("*", [Var 1; Term ("*", [Var 2; Var 3])]) }
  ; { number = 4
    ; numvars = 0
    ; lhs = Term ("*", [Term ("A", []); Term ("B", [])])
    ; rhs = Term ("*", [Term ("B", []); Term ("A", [])]) }
  ; { number = 5
    ; numvars = 0
    ; lhs = Term ("*", [Term ("C", []); Term ("C", [])])
    ; rhs = Term ("U", []) }
  ; { number = 6
    ; numvars = 0
    ; lhs =
        Term
          ( "*"
          , [Term ("C", []); Term ("*", [Term ("A", []); Term ("I", [Term ("C", [])])])]
          )
    ; rhs = Term ("I", [Term ("A", [])]) }
  ; { number = 7
    ; numvars = 0
    ; lhs =
        Term
          ( "*"
          , [Term ("C", []); Term ("*", [Term ("B", []); Term ("I", [Term ("C", [])])])]
          )
    ; rhs = Term ("B", []) } ]

let group_rank = function
  | "U" -> 0
  | "*" -> 1
  | "I" -> 2
  | "B" -> 3
  | "C" -> 4
  | "A" -> 5
  | _ -> assert false

let group_precedence op1 op2 =
  let r1 = group_rank op1 and r2 = group_rank op2 in
  if r1 = r2 then Equal else if r1 > r2 then Greater else NotGE

let group_order = rpo group_precedence lex_ext

let greater pair = match group_order pair with Greater -> true | _ -> false

let _ =
  for _ = 1 to 20 do
    kb_complete greater [] geom_rules
  done

*********************************************************************
                                                                     
                           Objective Caml                            
                                                                     
                                                                     
                                                                     
*********************************************************************
***************** Term manipulations ****************
 Term matching. 
 A naive unification algorithm. 
 We need to print terms with variables independently from input terms
  obtained by parsing. We give arbitrary names v1,v2,... to their variables.

*********************************************************************
                                                                     
                           Objective Caml                            
                                                                     
                                                                     
                                                                     
*********************************************************************
 $Id: equations.ml 2553 1999-11-17 18:59:06Z xleroy $ 
***************** Equation manipulations ************
 standardizes an equation so its variables are 1,2,... 
 checks that rules are numbered in sequence and returns their number 
***************** Rewriting *************************
 Top-level rewriting with multiple rules. 
 Iterating rewrite1. Returns a normal form. May loop forever 
*********************************************************************
                                                                     
                           Objective Caml                            
                                                                     
                                                                     
                                                                     
*********************************************************************
********************** Recursive Path Ordering ***************************
 Recursive path ordering 
*********************************************************************
                                                                     
                           Objective Caml                            
                                                                     
                                                                     
                                                                     
*********************************************************************
***************** Critical pairs ********************
 Critical pairs of l1=r1 with l2=r2 
 critical_pairs : term_pair -> term_pair -> term_pair list 
 Strict critical pairs of l1=r1 with l2=r2 
 Renaming of variables 
*********************** Completion *****************************
 Generate failure message 
 successful completion 
**
        print_string "--- Considering "; non_orientable (m', n');
**
*********************************************************************
                                                                     
                           Objective Caml                            
                                                                     
                                                                     
                                                                     
*********************************************************************
let print_string _ = ()

let print_int _ = ()

let print_newline _ = ()

               , 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 .               

  $ I d : terms.ml 2553 1999 - 11 - 17 18:59:06Z xleroy $


type term =
  | Var of int
  | Term of string * term list

let rec union l1 l2 =
  match l1 with
  | [] -> l2
  | a :: r -> if List.mem a l2 then union r l2 else a :: union r l2

let rec vars = function Var n -> [n] | Term (_, l) -> vars_of_list l

and vars_of_list = function [] -> [] | t :: r -> union (vars t) (vars_of_list r)

let rec substitute subst = function
  | Term (oper, sons) -> Term (oper, List.map (substitute subst) sons)
  | Var n as t -> ( try List.assoc n subst with Not_found -> t )

  Term replacement : replace M u N is M[u<-N ] .

let rec replace m u n =
  match u, m with
  | [], _ -> n
  | i :: u, Term (oper, sons) -> Term (oper, replace_nth i sons u n)
  | _ -> failwith "replace"

and replace_nth i sons u n =
  match sons with
  | s :: r -> if i = 1 then replace s u n :: r else s :: replace_nth (i - 1) r u n
  | [] -> failwith "replace_nth"


let matching term1 term2 =
  let rec match_rec subst t1 t2 =
    match t1, t2 with
    | Var v, _ ->
        if List.mem_assoc v subst
        then if t2 = List.assoc v subst then subst else failwith "matching"
        else (v, t2) :: subst
    | Term (op1, sons1), Term (op2, sons2) ->
        if op1 = op2
        then List.fold_left2 match_rec subst sons1 sons2
        else failwith "matching"
    | _ -> failwith "matching"
  in
  match_rec [] term1 term2


let compsubst subst1 subst2 =
  List.map (fun (v, t) -> v, substitute subst1 t) subst2 @ subst1

let rec occurs n = function
  | Var m -> m = n
  | Term (_, sons) -> List.exists (occurs n) sons

let rec unify term1 term2 =
  match term1, term2 with
  | Var n1, _ ->
      if term1 = term2
      then []
      else if occurs n1 term2
      then failwith "unify"
      else [n1, term2]
  | term1, Var n2 -> if occurs n2 term1 then failwith "unify" else [n2, term1]
  | Term (op1, sons1), Term (op2, sons2) ->
      if op1 = op2
      then
        List.fold_left2
          (fun s t1 t2 -> compsubst (unify (substitute s t1) (substitute s t2)) s)
          []
          sons1
          sons2
      else failwith "unify"


let infixes = ["+"; "*"]

let pretty_term _ = ()

let pretty_close _ = ()

               , 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 .               



type rule =
  { number : int
  ; numvars : int
  ; lhs : term
  ; rhs : term }


let mk_rule num m n =
  let all_vars = union (vars m) (vars n) in
  let counter = ref 0 in
  let subst = List.map (fun v -> incr counter; v, Var !counter) (List.rev all_vars) in
  {number = num; numvars = !counter; lhs = substitute subst m; rhs = substitute subst n}


let check_rules rules =
  let counter = ref 0 in
  List.iter
    (fun r ->
      incr counter;
      if r.number <> !counter then failwith "Rule numbers not in sequence" )
    rules;
  !counter

let pretty_rule rule =
  print_int rule.number;
  print_string " : ";
  pretty_term rule.lhs;
  print_string " = ";
  pretty_term rule.rhs;
  print_newline ()

let pretty_rules rules = List.iter pretty_rule rules


  Top - level rewriting . Let eq : L = R be an equation , M be a term such that L<=M. 
    With sigma = matching L M , we define the image of M by eq as sigma(R )
   With sigma = matching L M, we define the image of M by eq as sigma(R) *)
let reduce l m r = substitute (matching l m) r

  Test whether m can be reduced by l , i.e. m contains an instance of l.

let can_match l m =
  try
    let _ = matching l m in
    true
  with Failure _ -> false

let rec reducible l m =
  can_match l m
  || match m with Term (_, sons) -> List.exists (reducible l) sons | _ -> false


let rec mreduce rules m =
  match rules with
  | [] -> failwith "mreduce"
  | rule :: rest -> ( try reduce rule.lhs m rule.rhs with Failure _ -> mreduce rest m )

  One step of rewriting in leftmost - outermost strategy , 
    with multiple rules . Fails if no redex is found
   with multiple rules. Fails if no redex is found *)

let rec mrewrite1 rules m =
  try mreduce rules m with Failure _ -> (
    match m with
    | Var _ -> failwith "mrewrite1"
    | Term (f, sons) -> Term (f, mrewrite1_sons rules sons) )

and mrewrite1_sons rules = function
  | [] -> failwith "mrewrite1"
  | son :: rest -> (
    try mrewrite1 rules son :: rest with Failure _ -> son :: mrewrite1_sons rules rest )


let rec mrewrite_all rules m =
  try mrewrite_all rules (mrewrite1 rules m) with Failure _ -> m

               , 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 .               

  $ I d : orderings.ml 2553 1999 - 11 - 17 18:59:06Z xleroy $


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) -> (
    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 )
  | _ -> failwith "mult_ext"

   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"


let rpo op_order ext =
  let rec rporec (m, n) =
    if m = n
    then Equal
    else
      match m with
      | Var _ -> 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

               , 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 .               

  $ I d :  2553 1999 - 11 - 17 18:59:06Z xleroy $


  All ( u , subst ) such that N / u ( & var ) unifies with M , 
    with principal unifier subst
   with principal unifier subst *)

let rec super m = function
  | Term (_, sons) as n -> (
      let rec collate n = function
        | [] -> []
        | son :: rest ->
            List.map (fun (u, subst) -> n :: u, subst) (super m son)
            @ collate (n + 1) rest
      in
      let insides = collate 1 sons in
      try ([], unify m n) :: insides with Failure _ -> insides )
  | _ -> []

  Ex : 
 let ( m , _ ) = < < F(A , B ) > > 
 and ( n , _ ) = < < H(F(A , x),F(x , y ) ) > > in super m n 
 = = > [ [ 1],[2,Term ( " B " , [ ] ) ] ;                       x < - B 
      [ 2],[2,Term ( " A " , [ ] ) ; 1,Term ( " B " , [ ] ) ] ]      x < - A   y < - B 

let (m,_) = <<F(A,B)>>
and (n,_) = <<H(F(A,x),F(x,y))>> in super m n
==> [[1],[2,Term ("B",[])];                      x <- B
     [2],[2,Term ("A",[]); 1,Term ("B",[])]]     x <- A  y <- B
*)

  All ( u , subst ) , u & [ ] , such that n / u unifies with m

let super_strict m = function
  | Term (_, sons) ->
      let rec collate n = function
        | [] -> []
        | son :: rest ->
            List.map (fun (u, subst) -> n :: u, subst) (super m son)
            @ collate (n + 1) rest
      in
      collate 1 sons
  | _ -> []

let critical_pairs (l1, r1) (l2, r2) =
  let mk_pair (u, subst) = substitute subst (replace l2 u r1), substitute subst r2 in
  List.map mk_pair (super l1 l2)

  strict_critical_pairs : term_pair - > term_pair - > term_pair list
let strict_critical_pairs (l1, r1) (l2, r2) =
  let mk_pair (u, subst) = substitute subst (replace l2 u r1), substitute subst r2 in
  List.map mk_pair (super_strict l1 l2)

  All critical pairs of eq1 with eq2
let mutual_critical_pairs eq1 eq2 =
  strict_critical_pairs eq1 eq2 @ critical_pairs eq2 eq1


let rename n (t1, t2) =
  let rec ren_rec = function
    | Var k -> Var (k + n)
    | Term (op, sons) -> Term (op, List.map ren_rec sons)
  in
  ren_rec t1, ren_rec t2


let deletion_message rule =
  print_string "Rule "; print_int rule.number; print_string " deleted"; print_newline ()

let non_orientable (m, n) =
  pretty_term m; print_string " = "; pretty_term n; print_newline ()

let rec partition p = function
  | [] -> [], []
  | x :: l ->
      let l1, l2 = partition p l in
      if p x then x :: l1, l2 else l1, x :: l2

let rec get_rule n = function
  | [] -> raise Not_found
  | r :: l -> if n = r.number then r else get_rule n l

  Improved Knuth - Bendix completion procedure

let kb_completion greater =
  let rec kbrec j rules =
    let rec process failures (k, l) eqs =
* * * 
      print_string " * * * kb_completion " ; print_int j ; print_newline ( ) ; 
      pretty_rules rules ; 
      List.iter non_orientable failures ; 
      print_int k ; print_string " " ; print_int l ; print_newline ( ) ; 
      List.iter non_orientable eqs ; 
 * *
     print_string "***kb_completion "; print_int j; print_newline();
     pretty_rules rules;
     List.iter non_orientable failures;
     print_int k; print_string " "; print_int l; print_newline();
     List.iter non_orientable eqs;
***)
      match eqs with
      | [] -> (
          if k < l
          then next_criticals failures (k + 1, l)
          else if l < j
          then next_criticals failures (1, l + 1)
          else
            match failures with
            | _ ->
                print_string "Non-orientable equations :";
                print_newline ();
                List.iter non_orientable failures;
                failwith "kb_completion" )
      | (m, n) :: eqs ->
          let m' = mrewrite_all rules m
          and n' = mrewrite_all rules n
          and enter_rule (left, right) =
            let new_rule = mk_rule (j + 1) left right in
            pretty_rule new_rule;
            let left_reducible rule = reducible left rule.lhs in
            let redl, irredl = partition left_reducible rules in
            List.iter deletion_message redl;
            let right_reduce rule =
              mk_rule rule.number rule.lhs (mrewrite_all (new_rule :: rules) rule.rhs)
            in
            let irreds = List.map right_reduce irredl in
            let eqs' = List.map (fun rule -> rule.lhs, rule.rhs) redl in
            kbrec (j + 1) (new_rule :: irreds) [] (k, l) (eqs @ eqs' @ failures)
          in
          if m' = n'
          then process failures (k, l) eqs
          else if greater (m', n')
          then enter_rule (m', n')
          else if greater (n', m')
          then enter_rule (n', m')
          else process ((m', n') :: failures) (k, l) eqs
    and next_criticals failures (k, l) =
* * * 
     print_string " * * * next_criticals " ; 
     print_int k ; print_string " " ; print_int l ; print_newline ( ) ; 
 * * *
    print_string "***next_criticals ";
    print_int k; print_string " "; print_int l ; print_newline();
****)
      try
        let rl = get_rule l rules in
        let el = rl.lhs, rl.rhs in
        if k = l
        then process failures (k, l) (strict_critical_pairs el (rename rl.numvars el))
        else
          try
            let rk = get_rule k rules in
            let ek = rk.lhs, rk.rhs in
            process failures (k, l) (mutual_critical_pairs el (rename rl.numvars ek))
          with Not_found -> next_criticals failures (k + 1, l)
      with Not_found -> next_criticals failures (1, l + 1)
    in
    process
  in
  kbrec

  complete_rules is assumed locally confluent , and checked  with 
   ordering greater , rules is any list of rules
  ordering greater, rules is any list of rules *)

let kb_complete greater complete_rules rules =
  let n = check_rules complete_rules
  and eqs = List.map (fun rule -> rule.lhs, rule.rhs) rules in
  let completed_rules = kb_completion greater n complete_rules [] (n, n) eqs in
  print_string "Canonical set found :";
  print_newline ();
  pretty_rules (List.rev completed_rules)

               , 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 .               

  $ I d : kbmain.ml 7017 2005 - 08 - 12 09:22:04Z xleroy $

* * * 
 let group_rules = [ 
   { number = 1 ; numvars = 1 ; 
     lhs = Term ( " * " , [ Term("U " , [ ] ) ; Var 1 ] ) ; rhs = Var 1 } ; 
   { number = 2 ; numvars = 1 ; 
     lhs = Term ( " * " , [ Term("I",[Var 1 ] ) ; Var 1 ] ) ; rhs = Term("U " , [ ] ) } ; 
   { number = 3 ; numvars = 3 ; 
     lhs = Term ( " * " , [ Term ( " * " , [ Var 1 ; Var 2 ] ) ; Var 3 ] ) ; 
     rhs = Term ( " * " , [ Var 1 ; Term ( " * " , [ Var 2 ; Var 3 ] ) ] ) } 
 ] 
 * * *
let group_rules = [
  { number = 1; numvars = 1;
    lhs = Term("*", [Term("U",[]); Var 1]); rhs = Var 1 };
  { number = 2; numvars = 1;
    lhs = Term("*", [Term("I",[Var 1]); Var 1]); rhs = Term("U",[]) };
  { number = 3; numvars = 3;
    lhs = Term("*", [Term("*", [Var 1; Var 2]); Var 3]);
    rhs = Term("*", [Var 1; Term("*", [Var 2; Var 3])]) }
]
****)

let geom_rules =
  [ {number = 1; numvars = 1; lhs = Term ("*", [Term ("U", []); Var 1]); rhs = Var 1}
  ; { number = 2
    ; numvars = 1
    ; lhs = Term ("*", [Term ("I", [Var 1]); Var 1])
    ; rhs = Term ("U", []) }
  ; { number = 3
    ; numvars = 3
    ; lhs = Term ("*", [Term ("*", [Var 1; Var 2]); Var 3])
    ; rhs = Term ("*", [Var 1; Term ("*", [Var 2; Var 3])]) }
  ; { number = 4
    ; numvars = 0
    ; lhs = Term ("*", [Term ("A", []); Term ("B", [])])
    ; rhs = Term ("*", [Term ("B", []); Term ("A", [])]) }
  ; { number = 5
    ; numvars = 0
    ; lhs = Term ("*", [Term ("C", []); Term ("C", [])])
    ; rhs = Term ("U", []) }
  ; { number = 6
    ; numvars = 0
    ; lhs =
        Term
          ( "*"
          , [Term ("C", []); Term ("*", [Term ("A", []); Term ("I", [Term ("C", [])])])]
          )
    ; rhs = Term ("I", [Term ("A", [])]) }
  ; { number = 7
    ; numvars = 0
    ; lhs =
        Term
          ( "*"
          , [Term ("C", []); Term ("*", [Term ("B", []); Term ("I", [Term ("C", [])])])]
          )
    ; rhs = Term ("B", []) } ]

let group_rank = function
  | "U" -> 0
  | "*" -> 1
  | "I" -> 2
  | "B" -> 3
  | "C" -> 4
  | "A" -> 5
  | _ -> assert false

let group_precedence op1 op2 =
  let r1 = group_rank op1 and r2 = group_rank op2 in
  if r1 = r2 then Equal else if r1 > r2 then Greater else NotGE

let group_order = rpo group_precedence lex_ext

let greater pair = match group_order pair with Greater -> true | _ -> false

let _ =
  for _ = 1 to 20 do
    kb_complete greater [] geom_rules
  done
