2 | module Data.Graph.Indexed.Query.Subgraph

  4 | import Data.Array.Mutable

  5 | import Data.AssocList.Indexed

  6 | import Data.Graph.Indexed

  7 | import Data.Linear.List

  8 | import Data.Vect

 10 | %default total

 16 | data Tag = Q | T

 18 | parameters (mq : MArray s q (Maybe $ Fin t))

 19 |            (mt : MArray s t (Maybe $ Fin q))

 21 |   -- Link a query node to a target node.

 22 |   assign : Fin q -> Fin t -> F1' s

 23 |   assign x y t =

 24 |     let _ # t := set mt y (Just x) t

 25 |      in set mq x (Just y) t

 27 |   -- Undo an assignment. We use this when backtracking

 28 |   -- from an assignment that didn't work.

 29 |   unassign : Fin q -> Fin t -> F1' s

 30 |   unassign x y t =

 31 |     let _ # t := set mt y Nothing t

 32 |      in set mq x Nothing t

 38 | parameters {k : _}

 39 |            (r : MArray s k (Maybe a))

 41 |   -- Test if the value at the given position in a mutable array is still unset.

 42 |   %inline unset : Fin k -> F1 s Bool

 43 |   unset x t = let m # t := get r x t in isNothing m # t

 45 |   -- Either extracts the target nodes from a successful query, or finds the

 46 |   -- first unassigned query node.

 47 |   findUnassigned : F1 s (Either (Fin k) (Vect k a))

 48 |   findUnassigned t =

 49 |     let vs # t = toVectWith r (\x => maybe (Left x) Right) t

 50 |      in sequence vs # t

 59 | 0 Matrix : (q,t : Nat) -> Type

 60 | Matrix q t = AssocList q (List $ Fin t)

 64 | %inline remove : Fin t -> Matrix q t -> Matrix q t

 65 | remove = map . filter . (/=)

 68 | intersect : List (Fin t) -> List (Fin t) -> List (Fin t)

 69 | intersect l@(x::xs) r@(y::ys) =

 70 |   case compare x y of

 71 |     LT => intersect xs r

 72 |     EQ => x :: intersect xs ys

 73 |     GT => intersect l ys

 74 | intersect _ _ = []

 80 | parameters {0 eq,et,nq,nt : Type}

 81 |            {q,t : Nat}

 82 |            (mq      : MArray s q (Maybe $ Fin t))

 83 |            (mt      : MArray s t (Maybe $ Fin q))

 84 |            (me      : eq -> et -> Bool) -- edge label matcher

 85 |            (mn      : nq -> nt -> Bool) -- node label matcher

 86 |            (query   : IGraph q eq nq)   -- query node

 87 |            (target  : IGraph t et nt)   -- target node

 89 |   -- Computes a list of candidate mappings from lists of query nodes

 90 |   -- and target nodes (both the neighbours - plus edge labels - of the

 91 |   -- most recently assigned query and target node).

 92 |   --

 93 |   -- We have already veryfied, that both lists consist only of so far

 94 |   -- unassigned nodes.

 95 |   candidates : AssocList q eq -> AssocList t et -> Matrix q t

 96 |   candidates ps qs = mapKV cand ps

 97 |     where

 98 |       match : eq -> nq -> (Fin t, et) -> Maybe (Fin t)

 99 |       match veq vnq (y, vet) =

100 |         if me veq vet && mn vnq (lab target y) then Just y else Nothing

102 |       cand : Fin q -> eq -> List (Fin t)

103 |       cand x lq = mapMaybe (match lq $ lab query x) (pairs qs)

105 |   align : Fin q -> Fin t -> Matrix q t -> F1 s (Matrix q t)

106 |   align x y m t =

107 |     let nsX # t := filterLin (unset mq) (neighbours $ adj query x) t

108 |         nsY # t := filterLin (unset mt) (neighbours $ adj target y) t

109 |      in unionWith intersect (remove y m) (candidates nsX nsY) # t

111 |   covering

112 |   tryAll : Matrix q t -> F1 s Bool

114 |   covering

115 |   try : Fin q -> List (Fin t) -> Matrix q t -> F1 s Bool

117 |   -- There are no valid mappings left for query node `x`, so we abort

118 |   -- with `False`.

119 |   try x []      cs t = False # t

121 |   try x (v::vs) cs t =

122 |     let _ # t := assign mq mt x v t -- map query node `x` to target node `v`

124 |         -- Align the neighbours of x and v and update the candidate matrix.

125 |         cs2 # t   := align x v cs t --

127 |         -- Iterate over the matrix of candidates to assign the

128 |         -- remaining query nodes to target nodes. If this fails,

129 |         -- undo the the mapping from `x` to `v` and try another

130 |         -- one from `vs`.

131 |         False # t := tryAll cs2 t | res => res

132 |         _ # t := unassign mq mt x v t

133 |      in try x vs cs t

135 |   -- This extracts the query node with the lowest number of

136 |   -- candidate nodes from the target. If there is no node left,

137 |   -- we are done with the current connected component.

138 |   tryAll m t =

139 |     case minBy length m of

140 |       Nothing     => True # t

141 |       Just (x,vs) => try x vs (delete x m) t

143 |   -- Tries to align all connected components of the query graph

144 |   -- with nodes of the target graph.

145 |   covering

146 |   run : F1 s (Maybe $ Vect q (Fin t))

147 |   run t = -- (S m1 a1) =

148 |     let Left x # t := findUnassigned mq t | Right arr # t => Just arr # t

149 |         ns     # t := filter1 (unset mt) (nodes target) t

150 |         ns'        := filter (\y => mn (lab query x) (lab target y)) ns

151 |         True   # t := try x ns' empty t | False # t => Nothing # t

152 |      in run t

157 | export covering

158 | query :

159 |      {0 eq,et,nq,nt : Type}

160 |   -> {q,t : Nat}

161 |   -> (me      : eq -> et -> Bool) -- edge label matcher

162 |   -> (mn      : nq -> nt -> Bool) -- node label matcher

163 |   -> (query   : IGraph q eq nq)   -- query node

164 |   -> (target  : IGraph t et nt)   -- target node

165 |   -> Maybe (Vect q (Fin t))

166 | query me mn que tgt =

167 |   run1 $ \tk =>

168 |     let mt # tk := marray1 t Nothing tk

169 |         mq # tk := marray1 q Nothing tk

170 |      in run mq mt me mn que tgt tk