Theory Comparison

subsection ‹Structural Graph Comparison›

theory
  Comparison
imports
  IRGraph
begin

text ‹
We introduce a form of structural graph comparison that is able to assert structural
equivalence of graphs which differ in zero or more reference node chains for any given nodes.
›

fun find_ref_nodes :: "IRGraph ⇒ (ID ⇀ ID)" where
"find_ref_nodes g = map_of
  (map (λn. (n, ir_ref (kind g n))) (filter (λid. is_RefNode (kind g id)) (sorted_list_of_set (ids g))))"

fun replace_ref_nodes :: "IRGraph ⇒ (ID ⇀ ID) ⇒ ID list ⇒ ID list" where
"replace_ref_nodes g m xs = map (λid. (case (m id) of Some other ⇒ other | None ⇒ id)) xs"

fun find_next :: "ID list ⇒ ID set ⇒ ID option" where
  "find_next to_see seen = (let l = (filter (λnid. nid ∉ seen) to_see)
    in (case l of [] ⇒ None | xs ⇒ Some (hd xs)))"

inductive reachables :: "IRGraph ⇒ ID list ⇒ ID set ⇒ ID set ⇒ bool" where
"reachables g [] {} {}" |
"⟦None = find_next to_see seen⟧ ⟹ reachables g to_see seen seen" |
"⟦Some n = find_next to_see seen;
  node = kind g n;
  new = (inputs_of node) @ (successors_of node);
  reachables g (to_see @ new) ({n} ∪ seen) seen' ⟧ ⟹ reachables g to_see seen seen' "

code_pred (modes: i ⇒ i ⇒ i ⇒ o ⇒ bool) [show_steps,show_mode_inference,show_intermediate_results] 
reachables .

inductive nodeEq :: "(ID ⇀ ID) ⇒ IRGraph ⇒ ID ⇒ IRGraph ⇒ ID ⇒ bool" where 
"⟦ kind g1 n1 = RefNode ref; nodeEq m g1 ref g2 n2 ⟧ ⟹ nodeEq m g1 n1 g2 n2" | 
"⟦ x = kind g1 n1; 
  y = kind g2 n2; 
  is_same_ir_node_type x y;
  replace_ref_nodes g1 m (successors_of x) = successors_of y; 
  replace_ref_nodes g1 m (inputs_of x) = inputs_of y ⟧ 
  ⟹ nodeEq m g1 n1 g2 n2"

code_pred [show_modes] nodeEq .

fun diffNodesGraph :: "IRGraph ⇒ IRGraph ⇒ ID set" where
"diffNodesGraph g1 g2 = (let refNodes = find_ref_nodes g1 in
    { n . n ∈ Predicate.the (reachables_i_i_i_o g1 [0] {}) ∧ (case refNodes n of Some _ ⇒ False | _ ⇒ True) ∧ ¬(nodeEq refNodes g1 n g2 n)})"

fun diffNodesInfo :: "IRGraph ⇒ IRGraph ⇒ (ID × IRNode × IRNode) set" (infix "∩⇩s" 20)
  where
"diffNodesInfo g1 g2 = {(nid, kind g1 nid, kind g2 nid) | nid . nid ∈ diffNodesGraph g1 g2}"

fun eqGraph :: "IRGraph ⇒ IRGraph ⇒ bool" (infix "≈⇩s" 20)
  where
"eqGraph isabelle_graph graal_graph = ((diffNodesGraph isabelle_graph graal_graph) = {})"


end