0 | module Geom.Gen2D.Types
  1 |
  2 | import public Chem
  3 | import public Data.Graph.Indexed.Subgraph
  4 | import Data.Graph.Indexed.Query.Visited
  5 | import Data.Queue
  6 | import Data.SortedMap
  7 | import Derive.Prelude
  8 |
  9 | %default total
 10 | %language ElabReflection
 11 |
 12 | --------------------------------------------------------------------------------
 13 | --      Components
 14 | --------------------------------------------------------------------------------
 15 |
 16 | public export
 17 | 0 Nodes : Nat -> Type
 18 | Nodes = List . Fin
 19 |
 20 | public export
 21 | 0 SnocNodes : Nat -> Type
 22 | SnocNodes = SnocList . Fin
 23 |
 24 | public export
 25 | data AttachPoint : (k : Nat) -> Type where
 26 |   None   : AttachPoint k
 27 |   Attach : (parent : Fin k) -> (node : Fin k) -> AttachPoint k
 28 |
 29 | %runElab deriveIndexed "AttachPoint" [Show,Eq]
 30 |
 31 | public export
 32 | 0 SubgraphType : Bool -> Nat -> Type -> Type -> Type
 33 | SubgraphType True  k e n = Subgraph k e n
 34 | SubgraphType False _ _ _ = ()
 35 |
 36 | ||| A component is a part of a molecular graph that will be placed
 37 | ||| as a single unit.
 38 | |||
 39 | ||| Every componenent `c` except the first (the "main component")
 40 | ||| comes with an attachement point: A node in another component
 41 | ||| that will be placed before `c`.
 42 | public export
 43 | record Component (k : Nat) (e,n : Type) where
 44 |   constructor C
 45 |   attach   : AttachPoint k
 46 |   nodes    : List (Fin k)
 47 |   isRing   : Bool
 48 |   subgraph : SubgraphType isRing k e n
 49 |
 50 | public export
 51 | 0 SnocComps : Nat -> Type -> Type -> Type
 52 | SnocComps k e = SnocList . Component k e
 53 |
 54 | public export
 55 | 0 Comps : Nat -> Type -> Type -> Type
 56 | Comps k e = List . Component k e
 57 |
 58 | setAttach : (a,x : Fin k) -> Component k e n -> Component k e n
 59 | setAttach a x = {attach := Attach a x}
 60 |
 61 | --------------------------------------------------------------------------------
 62 | -- Utilities
 63 | --------------------------------------------------------------------------------
 64 |
 65 | -- A mapping from a node to the ring it belongs to (if any).
 66 | 0 RingMap : Nat -> Type -> Type -> Type
 67 | RingMap k e n = IArray k (Maybe $ Component k e n)
 68 |
 69 | %inline
 70 | subnodes : Subgraph k e n -> List (Fin k)
 71 | subnodes (G _ g) = fst <$> labels g
 72 |
 73 | children : IGraph k e n -> Visited k -> Component k e n -> List (Fin k, Fin k)
 74 | children g v c =
 75 |   nodes c >>= \a => (a,) <$> filter (flip unvisited v) (neighbours g a)
 76 |
 77 | --------------------------------------------------------------------------------
 78 | -- Component Partition
 79 | --------------------------------------------------------------------------------
 80 |
 81 | pairs : Subgraph k e n -> List (Nat, Maybe $ Component k e n)
 82 | pairs g =
 83 |  let ns := subnodes g
 84 |      c  := Just (C None ns True g)
 85 |   in map (\x => (finToNat x ,c)) ns
 86 |
 87 | -- Extracts the ring systems from a graph storing them in an array and
 88 | -- returning the largest of them as the molecule's main component.
 89 | -- Returns `Nothing` in case the molecule is acyclic.
 90 | rings : {k : _} -> (g : IGraph k e n) -> Maybe (Component k e n, RingMap k e n)
 91 | rings g =
 92 |   case reverse $ sortBy (comparing order) (biconnectedComponents g) of
 93 |     []    => Nothing
 94 |     r::rs => Just (C None (subnodes r) True r, fromPairs k Nothing (rs >>= pairs))
 95 |
 96 | parameters {k : Nat}
 97 |            (g : IGraph k e n)
 98 |            (m : RingMap k e n)
 99 |
100 |   -- `True` if the given node is not in a ring and has not yet been visited
101 |   nonVisitedInChain : Visited k -> Fin k -> Bool
102 |   nonVisitedInChain v n = isNothing (m `at` n) && unvisited n v
103 |
104 |   -- runner for `chain`
105 |   lcf : SnocNodes k -> Queue (SnocNodes k, Fin k) -> Visited k -> SnocNodes k
106 |   lcf sx q vis =
107 |     case dequeue q of
108 |       Nothing          => sx
109 |       Just ((sy,y),q2) =>
110 |        let ss := sy:<y
111 |            ns := filter (nonVisitedInChain vis) (neighbours g y)
112 |            v2 := assert_smaller vis (visitAll ns vis)
113 |         in lcf ss (enqueueAll q2 $ (ss,) <$> ns) v2
114 |
115 |   -- computes the longest chain of atoms not in a ring
116 |   -- from the given starting point
117 |   chain : Visited k -> Fin k -> SnocList (Fin k)
118 |   chain vis x = lcf [<] (enqueue empty ([<], x)) (visit x vis)
119 |
120 |   nextComp : Visited k -> (a,x : Fin k) -> Component k e n
121 |   nextComp v a x =
122 |     maybe (C (Attach a x) (chain v x <>> []) False ()) (setAttach a x) (at m x)
123 |
124 |   -- Iteratively computes the longest chains from the attachment
125 |   -- points of already found components
126 |   chains : SnocComps k e n -> Queue (Fin k,Fin k) -> Visited k -> (Comps k e n)
127 |   chains sx q vis =
128 |     case dequeue q of
129 |       Nothing         => sx <>> []
130 |       Just ((a,n),q2) =>
131 |        let c    := nextComp vis a n
132 |            vis2 := assert_smaller vis $ visitAll (nodes c) vis
133 |            q3   := enqueueAll q2 (children g vis2 c)
134 |         in chains (sx:<c) q3 vis2
135 |
136 | ||| Partitions the nodes of a graph into disjoint components,
137 | ||| which will be placed individually in the given order.
138 | |||
139 | ||| The first component to be placed will be the most complex
140 | ||| cyclic system (if any) or the longest chain. All other
141 | ||| components in the list are linked via an `AttachPoint` to
142 | ||| a parent component, which will be placed first.
143 | export
144 | components : {k : _} -> IGraph k e n -> List (Component k e n)
145 | components {k = Z}   g = []
146 | components {k = S x} g =
147 |   case rings g of
148 |     Just (c,m) =>
149 |      let vis := visitAll (nodes c) ini
150 |       in chains g m [<c] (fromList $ children g vis c) vis
151 |     Nothing     =>
152 |      let m      := fill (S x) Nothing
153 |          _ :< n := chain g m ini FZ | [<] => []
154 |          ns     := reverse $ chain g m ini n <>> []
155 |          c      := C None ns False ()
156 |          vis    := visitAll ns ini
157 |       in chains g m [<c] (fromList $ children g vis c) vis
158 |