Created
March 26, 2017 15:00
-
-
Save erutuf/fa897f6268135f5cdd604313f418f6e5 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment