0 | module Geom.Gen2D.Rings

  2 | import Chem

  3 | import Geom.Gen2D.Place

  4 | import Geom.Gen2D.State

  5 | import Geom.Gen2D.Types

  6 | import Geom.Interpolate

  7 | import Data.Graph.Indexed.Ring.Relevant

  8 | import Data.SortedSet

  9 | import Derive.Prelude

 11 | %default total

 12 | %language ElabReflection

 18 | 0 Cycles : Nat -> Type

 19 | Cycles = List . Cycle

 21 | data BridgeType = Fused | Spiro | Brdg | Fresh | Partitioned

 23 | %runElab derive "BridgeType" [Show,Eq,Ord]

 25 | record Bridge (k : Nat) where

 26 |   constructor B

 27 |   cycle : Cycle k

 28 |   start : Fin k

 29 |   first : Fin k

 30 |   rem   : Nodes k

 31 |   end   : Fin k

 32 |   type  : BridgeType

 34 | natoms : Cycle k -> List (Cycle k) -> Nat

 35 | natoms c = sum . map (numSharedNodes c)

 37 | mostComplex :

 38 |      SnocList (Cycle k)

 39 |   -> List (Cycle k)

 40 |   -> (atms, len : Nat)

 41 |   -> Cycle k

 42 |   -> (Cycle k, List (Cycle k))

 43 | mostComplex sx []      atms len r = (r, sx <>> [])

 44 | mostComplex sx (x::xs) atms len r =

 45 |  let n := natoms x (sx <>> (r::xs))

 46 |   in case compare n atms of

 47 |        LT => mostComplex (sx:<x) xs atms len r

 48 |        GT => mostComplex (sx:<r) xs n    x.ncycle.size x

 49 |        EQ => case len >= x.ncycle.size of

 50 |          True  => mostComplex (sx:<x) xs atms len r

 51 |          False => mostComplex (sx:<r) xs n    x.ncycle.size x

 53 | partOf : Bridge k -> Cycle k -> Bool

 54 | partOf b c = numSharedNodes b.cycle c > 0

 57 | toBridge : PlaceST s k => Cycle k -> F1 s (Maybe $ Bridge k)

 58 | toBridge c t =

 59 |   case break1 isPlaced c.nodes t of

 60 |     (u::us,[])  # t => Just (B c u u us u Fresh) # t -- all unplaced

 61 |     (us,[]    ) # t => Nothing # t                   -- all placed

 62 |     (us,p::rem) # t =>

 63 |      let Just (b,p2,ns2) # t := nxt p  (rem++us++[p]) t | _ # t => Nothing # t

 64 |          Just _          # t := nxt p2 ns2            t | _ # t => Just b # t

 65 |       in Just ({type := Partitioned} b) # t

 66 |   where

 67 |     tpe : Fin k -> Fin k -> BridgeType

 68 |     tpe x y =

 69 |      case mkEdge x y () of

 70 |        Just e  => if contains e c.edgeset then Fused else Brdg

 71 |        Nothing => Spiro

 73 |     nxt : Fin k -> Nodes k -> F1 s (Maybe (Bridge k, Fin k, Nodes k))

 74 |     nxt p ns = T1.do

 75 |       -- first, take placed prefix, then take until placed again

 76 |       (ps,u::x)    <- span1  isPlaced ns | (_,[]) => pure Nothing

 77 |       (us,p2::rem) <- break1 isPlaced x  | (_,[]) => pure Nothing

 78 |       let p1 := List.last (p::ps)

 79 |       pure $ Just (B c p1 u us p2 $ tpe p1 p2, p2, rem)

 81 | bridge : PlaceST s k => Cycles k -> F1 s (Maybe (Bridge k, Cycles k))

 82 | bridge cs = T1.do

 83 |   bs <- mapMaybe1 toBridge cs

 84 |   case sortBy (comparing type) bs of

 85 |     []    => pure Nothing

 86 |     b::bs => pure $ Just (b,map cycle bs)

 92 | parameters {k : _}

 93 |            {0 e, n  : Type}

 94 |            {auto dg : DebugFlag}

 95 |            {auto ce : Cast n Elem}

 96 |            {auto ch : Cast n Hybridization}

 97 |            (g : IGraph k e n)

 98 |            {auto st : PlaceST s k}

100 |   ngon : Cycle k -> F1' s

101 |   ngon c =

102 |     let phi := fullSteps c.ncycle.size

103 |         r   := ngonRadius BOND_LEN c.ncycle.size @{c.ncycle.prf}

104 |      in polygonCorners g c.nodes origin zero phi (scaleTo r vone)

106 |   placeBridge : Cycles k -> Bridge k -> F1' s

107 |   placeBridge placed (B c _ _ _   _ Fresh) = ngon c

108 |   placeBridge placed (B c x f rem y Spiro) = T1.do

109 |     -- center of placed cycle(s)

110 |     cref <- centerOf (placed >>= \x => x.nodes)

111 |     -- positions of the attachment nodes

112 |     px   <- nodePosition x

113 |     let MkArc tot phi r d := ngon BOND_LEN c.ncycle.size @{c.ncycle.prf}

114 |         c                 := translate (scaleTo r $ px - cref) px

115 |     polygonCorners g (f::rem) c zero phi (px - c)

117 |   placeBridge placed (B c x f rem y tpe)   = T1.do

118 |     -- center of placed cycle(s)

119 |     cref <- centerOf (placed >>= \x => x.nodes)

120 |     -- positions of the attachment nodes

121 |     px   <- nodePosition x

122 |     py   <- nodePosition y

123 |     debugIf1 "Placing ring: \{show tpe}, nodes: \{c.nodes}, unplaced: \{f::rem}"

124 |     debugIf1 "Placed center: \{cref}; px: \{px}; py: \{py}"

125 |     let cs  := center2d (the (List _) [px,py])

126 |         rd  := distance px py

127 |         len := max BOND_LEN $ rd * 1.1 / cast (length rem + 2)

128 |         MkArc tot phi r d := arc (S $ length rem) len rd

129 |         v   := scaleTo d $ perpendicularFrom px py cref

130 |         v2  := if tot > pi then v else negate v

131 |         c   := translate v2 cs

132 |         ax  := angleOrZero (c - px)

133 |         ay  := angleOrZero (c - py)

134 |         ns  := f::rem

135 |         px' := translate (rotate tot $ px - c) c

136 |         py' := translate (rotate tot $ py - c) c

137 |     debugIf1 "xy-center: \{cs}; xy-distance: \{rd}; len: \{len}"

138 |     debugIf1 "vectors: v: \{v}; v2: \{v2}, arc center: \{c}"

139 |     debugIf1 "angles: ax: \{ax}, ay: \{ay}, arc: \{tot}, step: \{phi}"

140 |     debugIf1 "Arc: radius: \{r}, dist: \{d}"

141 |     debugIf1 "Images: px': \{px'}, py': \{py'}"

142 |     case (ax - ay < Angle.pi) == (tot > Angle.pi) of

143 |       True  => polygonCorners g ns c zero phi (px - c)

144 |       False => polygonCorners g (reverse ns) c zero phi (py - c)

146 |   layoutSystem : (placed, unplaced : Cycles k) -> F1' s

147 |   layoutSystem ps us t =

148 |    let Just (b,rs) # t := bridge us t | _ # t => () # t

149 |        _           # t := placeBridge (filter (partOf b) ps) b t

150 |     in layoutSystem (b.cycle::ps) (assert_smaller us rs) t

152 |   placeInitialRing : Subgraph k e n -> F1' s

153 |   placeInitialRing sg =

154 |    let c::cs  := mcb $ componentCycles sg | [] => pure ()

155 |        (r,rs) := mostComplex [<] cs (natoms c cs) (c.ncycle.size) c

156 |     in ngon r >> layoutSystem [r] rs

158 |   export

159 |   placeRing : AttachPoint k -> List (Fin k) -> Subgraph k e n -> F1' s

160 |   placeRing None         ns sg = T1.do

161 |     placeInitialRing sg

162 |     _ <- traverse1 (placeNeighbours g) ns

163 |     pure ()

164 |   placeRing (Attach p x) ns sg = T1.do

165 |     pp <- nodePosition p

166 |     xp <- nodePosition x

167 |     unplace p

168 |     placeInitialRing sg

169 |     us <- traverse1 (placeNeighbours g) ns

170 |     pq <- nodePosition p

171 |     xq <- nodePosition x

172 |     let f := alignBond pp xp pq xq

173 |     for1_ (ns ++ join us) $ adjPoint f