cc.ml

let rec find quot node =
  if quot.(node) = node
  then node
  else
    let repr = find quot quot.(node) in
    quot.(node) <- repr;
    repr

let union quot node1 node2 =
  let repr1 = find quot node1
  and repr2 = find quot node2 in
  quot.(repr2) <- repr1

let equiv quot node1 node2 =
  find quot node1 = find quot node2

type termgraph =
  {
    id : int;
    label : int;
    children : termgraph list;
  }

let congruent quot p q =
  p.label = q.label && List.for_all2 (fun pi qi -> equiv quot pi.id qi.id ) p.children q.children

let rec preds quot i t =
  if List.exists (fun ti -> equiv quot i ti.id) t.children
  then t :: List.concat (List.map (preds quot i) t.children)
  else List.concat (List.map (preds quot i) t.children)

let rec merge quot t i j =
  if equiv quot i j
  then ()
  else
    let u = preds quot i t
    and v = preds quot j t in
    union quot i j;
    List.iter (fun ui -> 
      List.iter (fun vi ->
        if equiv quot ui.id vi.id || not (congruent quot ui vi)
        then ()
        else merge quot t ui.id vi.id) v) u

type term = Term of int * term list

let rec from_term' m (Term (n, ts)) =
  let children, m' = from_term'' (m+1) ts in
  { id = m; label = n; children = children; }, m'
and from_term'' m = function
  | [] -> [], m
  | t::ts ->
      let graph, m' = from_term' m t in
      let ts', m'' = from_term'' m' ts in
      (graph :: ts', m'')

let from_term t = from_term' 0 t

let tinit ts = List.fold_right (fun (t1, t2) xs -> t1 :: t2 :: xs) ts []

let rec drop n = function
  | [] -> []
  | x :: xs -> if n = 0 then x :: xs else drop (n-1) xs

let rec cc' quot t rules =
  List.iter (fun (p, q) -> merge quot t p q) rules;
  quot, t

let rec subterm t (Term (n, ts)) =
  if t = Term (n, ts)
  then true
  else List.exists (subterm t) ts

let rec leaves graph =
  match graph.children with
  | [] -> [graph]
  | _ -> List.concat (List.map leaves graph.children)

let rec somes f = function
  | [] -> []
  | x :: xs ->
      match f x with
      | Some y -> y :: somes f xs
      | None -> somes f xs

let rec leaves_congr' base = function
  | [] -> []
  | c :: cs ->
      if List.mem c.label base
      then leaves_congr' base cs
      else
        let cs' = somes (fun c' -> if c.label = c'.label then Some c' else None) cs in
        List.map (fun c' -> (c.id, c'.id)) cs' @ leaves_congr' (c.label :: base) cs
     
let leaves_congr graph = leaves_congr' [] (leaves graph)

let rec tuples = function
  | [] -> []
  | _ :: [] -> []
  | x :: y :: xs -> (x, y) :: tuples xs

let cc symb l r rules =
  let t, m = from_term (Term (symb, tinit ((l, r) :: rules))) in
  let quot = Array.init m (fun x -> x) in
  let rules_id = leaves_congr t @ tuples (drop 2 (List.map (fun x -> x.id) t.children)) in
  cc' quot t rules_id