0 | module CyBy.Draw.Internal.Graph

   2 | import Chem.Util

   3 | import CyBy.Draw.Internal.CoreDims

   4 | import CyBy.Draw.Internal.Atom

   5 | import CyBy.Draw.Internal.Role

   6 | import Data.Graph.Indexed.Subgraph

   7 | import Data.SortedMap

   8 | import Data.SortedSet

   9 | import Derive.Prelude

  10 | import Geom

  11 | import Text.Molfile

  12 | import Text.ParseError

  14 | %language ElabReflection

  15 | %default total

  20 | public export

  21 | data NOE : (a,b : Type) -> Type where

  22 |   None  : NOE a b      -- the empty case

  23 |   N     : a -> NOE a b -- the "nodes" case

  24 |   E     : b -> NOE a b -- the "edges" case

  28 | noe : Maybe a -> Lazy (Maybe b) -> NOE a b

  29 | noe mn me = maybe (maybe None E me) N mn

  33 | eon : Lazy (Maybe a) -> Maybe b -> NOE a b

  34 | eon mn me = maybe (maybe None N mn) E me

  40 | eons : List a -> Lazy (List b) -> NOE (List a) (List b)

  41 | eons _  es@(_::_) = E es

  42 | eons ns []        = if null ns then None else N ns

  47 | public export

  48 | record CDBond where

  49 |   constructor CB

  50 |   role    : Role

  51 |   molBond : MolBond

  53 | %runElab derive "CDBond" [Show,Eq]

  55 | export %inline

  56 | Cast CDBond Role where cast = role

  58 | export %inline

  59 | ModRole CDBond where modRole f = {role $= f}

  62 | public export

  63 | 0 CDGraph : Type

  64 | CDGraph = Graph CDBond CDAtom

  67 | public export

  68 | 0 CDIGraph : Nat -> Type

  69 | CDIGraph k = IGraph k CDBond CDAtom

  71 | export %inline

  72 | toMolGraph : Graph CDBond CDAtom -> MolGraphAT

  73 | toMolGraph = bimap CDBond.molBond CDAtom.atom

  75 | export %inline

  76 | toMolfile : Graph CDBond CDAtom -> MolfileAT

  77 | toMolfile g = MkMolfile "" "created by cyby-draw 1.0" "" (toMolGraph g) []

  83 | initGraph : MolGraphAT -> CDGraph

  84 | initGraph (G o g) = G o $ bimap (CB None) (CA None) (normalizeMol g)

  88 | readMolfileE : String -> Either String CDGraph

  89 | readMolfileE mol =

  90 |   case readMol {es = [ParseError MolErr]} mol of

  91 |     Left (Here e)               => Left "\{e}"

  92 |     Right (MkMolfile _ _ _ g _) => Right $ initGraph (perceiveMolAtomTypes g)

  96 | readMolfile : String -> CDGraph

  97 | readMolfile = either (const $ G 0 empty) id . readMolfileE

 101 | adjAtomTypes : {k : _} -> CDIGraph k -> CDIGraph k 

 102 | adjAtomTypes =

 103 |   mapWithAdj (\(A (CA r a) ns) => CA r $ calcMolAtomType (map molBond ns) a)

 109 | adjStereo : BondStereo -> MolBond -> MolBond

 110 | adjStereo Up   (MkBond fs _ Up)   = MkBond (not fs) Single Up

 111 | adjStereo Down (MkBond fs _ Down) = MkBond (not fs) Single Down

 112 | adjStereo bs   b                  = MkBond True Single bs

 114 | nextType : BondOrder -> BondOrder

 115 | nextType Single = Dbl

 116 | nextType Dbl    = Triple

 117 | nextType Triple = Single

 120 | newBond : BondOrder -> BondStereo -> MolBond -> MolBond

 121 | newBond Single NoBondStereo b =

 122 |   if b.stereo == NoBondStereo then cast $ nextType b.type else cast Single

 123 | newBond Single s            b = adjStereo s b

 124 | newBond Dbl    _            _ = cast Dbl

 125 | newBond Triple _            _ = cast Triple

 131 | hlAdj : IArray o Bool -> Fin o -> Adj o CDBond CDAtom -> Adj o CDBond CDAtom

 132 | hlAdj arr x (A l ns) =

 133 |   case arr `at` x of

 134 |     False => A l ns

 135 |     True  => A (set Highlight l) (mapKV (setIf Highlight . at arr) ns)

 139 | highlight : List Nat -> CDGraph -> CDGraph

 140 | highlight ns (G o $ IG gr) =

 141 |   let arr := fromPairs o False (map (,True) ns)

 142 |    in G o $ IG (mapWithIndex (hlAdj arr) gr)

 149 | export %inline

 150 | groupNr : CDIGraph k -> Fin k -> Maybe Nat

 151 | groupNr g = map nr . label . atom . lab g

 155 | inAbbreviation : CDIGraph k -> Fin k -> Bool

 156 | inAbbreviation g = isJust . groupNr g

 159 | export %inline

 160 | maxGroupNr : {k : _} -> CDIGraph k -> Nat

 161 | maxGroupNr = foldr (\a,n => maybe n (max n . nr) a.atom.label) 0

 165 | groupNrs : {k : _} -> CDIGraph k -> SortedSet Nat

 166 | groupNrs =

 167 |   foldr (\a,ss => maybe ss ((`insert` ss) . nr) a.atom.label) SortedSet.empty

 169 | groupMap : SortedSet Nat -> SortedMap Nat Nat -> List Nat -> SortedMap Nat Nat

 170 | groupMap used m []      = m

 171 | groupMap used m (x::xs) =

 172 |  let n := next x in groupMap (insert n used) (insert x n m) xs

 173 |   where

 174 |     next : Nat -> Nat

 175 |     next k = if contains k used then next (assert_smaller k $ S k) else k

 184 | adjTemplate : {k,m : _} -> CDIGraph k -> CDIGraph m -> CDIGraph m

 185 | adjTemplate c t  =

 186 |   let mp := groupMap (groupNrs c) empty (Prelude.toList $ groupNrs t)

 187 |    in map (adj mp) t

 189 |   where

 190 |     nr  : SortedMap Nat Nat -> AtomGroup -> AtomGroup

 191 |     nr mp (G x lbl) = G (fromMaybe x $ lookup x mp) lbl

 193 |     adj : SortedMap Nat Nat -> CDAtom -> CDAtom

 194 |     adj mp (CA r a) = CA r $ {label $= map (nr mp)} a

 199 | anyNotInGroup : CDIGraph k -> Fin k -> Nat -> Bool

 200 | anyNotInGroup g x n = any (not . inGroup n) (neighbourLabels g x)

 204 | customLabel : CDIGraph k -> Fin k -> Maybe String

 205 | customLabel  g x = do

 206 |   G n lbl <- label . atom $ lab g x

 207 |   guard $ lbl /= "" && anyNotInGroup g x n

 208 |   pure lbl

 213 | visible : CDIGraph k -> Fin k -> Bool

 214 | visible g x =

 215 |   case Atom.label . atom $ lab g x of

 216 |     Nothing      => True

 217 |     Just (G n _) => anyNotInGroup g x n

 222 | labelVisible : (showC : Bool) -> CDIGraph k -> Fin k -> Bool

 223 | labelVisible showC g x =

 224 |   let A (CA _ a) ns  := adj g x

 225 |       MkI e m := a.elem

 226 |    in    showC

 227 |       || null ns

 228 |       || a.type.name == "C.allene"

 229 |       || e /= C 

 230 |       || isJust m

 231 |       || a.charge /= 0

 232 |       || isJust (customLabel g x)

 238 | visibleNodes : {k : _} -> CDIGraph k -> List (Fin k)

 239 | visibleNodes g = filter (visible g) (nodes g)

 243 | atomsIn : {k : _} -> CDIGraph k -> Bounds2D Mol ->  List (Fin k)

 244 | atomsIn g bs =

 245 |   filter (\n => visible g n && inBounds (point $ lab g n) bs) (nodes g)

 247 | nonAbbreviatedNodes : {k : _} -> CDIGraph k -> List (Fin k)

 248 | nonAbbreviatedNodes g = filter (not . inAnyGroup . lab g) (nodes g)

 254 | visibleNeighbours : CDIGraph k -> Fin k -> List (Fin k)

 255 | visibleNeighbours g x = filter (visible g) (neighbours g x)

 260 | hiddenNodes : {k : _} -> CDIGraph k -> List (Fin k)

 261 | hiddenNodes g = filter (not . visible g) (nodes g)

 267 | visibleEdges : {k : _} -> CDIGraph k -> List (Edge k CDBond)

 268 | visibleEdges g = filter (\(E x y _) => visible g x && visible g y) (edges g)

 275 | groupNodes : {k : _} -> CDIGraph k -> (ns : List (Fin k)) -> List (Fin k)

 276 | groupNodes g ns =

 277 |   let gs@(_::_) := ns >>= toList . groupNr g | Nil => Nil

 278 |    in filter (any (`elem` gs) . groupNr g) (hiddenNodes g)

 285 | plusGroupNodes : {k : _} -> CDIGraph k -> (ns : List (Fin k)) -> List (Fin k)

 286 | plusGroupNodes g ns = ns ++ groupNodes g ns

 293 | export %inline

 294 | pointAt : CDIGraph k -> Fin k -> Point Id

 295 | pointAt g = pointId . lab g

 299 | bondAngles : CDIGraph k -> Fin k -> List Angle

 300 | bondAngles g x =

 301 |   let p  := pointId (lab g x)

 302 |       ns := lab g <$> visibleNeighbours g x

 303 |    in mapMaybe (\k => angle $ pointId k - p) ns

 305 | parameters {k : Nat}

 306 |            {auto cd : CoreDims}

 308 |   ||| Returns the node closest to the given point,

 310 |   export

 311 |   closestNodeList : List (Fin k) -> Point Id -> CDIGraph k -> Maybe (Fin k)

 312 |   closestNodeList ks p g = do

 313 |     x <- minBy (distance p . pointId . lab g) ks

 314 |     let q := pointAt g x

 315 |     guard $ near p q cd.radiusAtom

 316 |     pure x

 318 |   ||| Finds the visible node closest to the given point, but only

 321 |   export

 322 |   closestNodeWhere : (Fin k -> Bool) -> Point Id -> CDIGraph k -> Maybe (Fin k)

 323 |   closestNodeWhere pred p g = closestNodeList (filter pred $ nodes g) p g

 325 |   ||| Finds the visible node closest to the given point, but only

 327 |   export %inline

 328 |   closestNode : Point Id -> CDIGraph k -> Maybe (Fin k)

 329 |   closestNode p g = closestNodeWhere (visible g) p g

 331 |   ||| Finds the visible edge closest to the given point, but only

 333 |   export

 334 |   closestEdge : Point Id -> CDIGraph k -> Maybe (Edge k CDBond)

 335 |   closestEdge p g = do 

 336 |     ed <- minBy distEdge $ visibleEdges g

 337 |     guard $ distEdge ed <= cd.radiusAtom

 338 |     pure ed

 340 |     where

 341 |       distEdge : Edge k n -> Double

 342 |       distEdge (E x y _) = distanceToLineSegment p (pointAt g x) (pointAt g y)

 344 |   ||| Returns the item (node or edge) closest to the current mouse position.

 345 |   export

 346 |   closestItem : Point Id -> CDIGraph k -> NOE (Fin k) (Edge k CDBond)

 347 |   closestItem p g = noe (closestNode p g) (closestEdge p g)

 349 |   ||| Generously approximates the bounds of an atom in the drawing.

 350 |   export

 351 |   approxBounds : CDIGraph k -> Fin k -> Bounds2D Id

 352 |   approxBounds g x =

 353 |     case visible g x of

 354 |       False => neutral

 355 |       True  => case group $ lab g x of

 356 |         Nothing      =>

 357 |           let r := 2 * cd.radiusAtom

 358 |               P x y := pointAt g x

 359 |            in BS (range (x-r) (x+r)) (range (y-r) (y+r))

 360 |         Just (G _ l) =>

 361 |           let w := cast {to = Double} (length l * cd.fontSize)

 362 |               h := cast {to = Double} cd.fontSize

 363 |               P x y := pointAt g x

 364 |            in BS (range (x-w) (x+w)) (range (y-h) (y+h))

 371 | export %inline

 372 | clear : CDGraph -> CDGraph

 373 | clear = bimap clear clear

 376 | export %inline

 377 | cleanup : CDGraph -> CDGraph

 378 | cleanup = bimap (keep Persistent) (keep Persistent)

 381 | unHover : {k : _} -> CDIGraph k -> CDIGraph k

 382 | unHover = bimap (unset Hover) (unset Hover)

 384 | hoverE : Fin k -> Fin k -> Fin k -> Adj k CDBond CDAtom -> Adj k CDBond CDAtom

 385 | hoverE x y z (A a ns) =

 386 |   if x == z || y == z

 387 |      then A a $ mapKV (\w => setIf Hover (w == x || w == y)) ns

 388 |      else A a ns

 407 | hover :

 408 |      {k : _}

 409 |   -> {auto cd : CoreDims}

 410 |   -> (hbond : CDBond -> Bool-> Bool)

 411 |   -> (hatom : CDAtom -> Bool)

 412 |   -> Point Id

 413 |   -> CDIGraph k

 414 |   -> CDIGraph k

 415 | hover hbond hatom p g0 =

 416 |   let g := unHover g0

 417 |    in case closestItem p g of

 418 |         N n         =>

 419 |           if hatom (lab g n)

 420 |              then mapWithCtxt (\x,(A a _) => setIf Hover (x == n) a) g

 421 |              else g

 422 |         E (E x y b) =>

 423 |           if hbond b (inAnyGroup (lab g x) || inAnyGroup (lab g y))

 424 |              then mapCtxt (hoverE x y) g

 425 |              else g

 426 |         None        => g

 429 | export %inline

 430 | ifHover : Role -> CDGraph -> CDGraph

 431 | ifHover r = map (\x => setIf r (is Hover x) x)

 440 | replaceWith : Cast a Role => ModRole a => Role -> Role -> a -> a

 441 | replaceWith old new a =

 442 |   if      is old a then unset old (set new a)

 443 |   else if is new a then unset new a

 444 |   else a

 448 | hoverIfNew : CDGraph -> CDGraph

 449 | hoverIfNew = map (New `replaceWith` Hover)

 452 | export %inline

 453 | hoveredItem : {k : _} -> CDIGraph k -> NOE (Fin k, CDAtom) (Edge k CDBond)

 454 | hoveredItem g =

 455 |   eon (find (is Hover . snd) (labNodes g)) (find (is Hover . label) (edges g))

 462 | export %inline

 463 | selectHovered : SelectMode -> SelectMode -> CDGraph -> CDGraph

 464 | selectHovered em nm = bimap (selectIfHovered em) (selectIfHovered nm)

 470 | public export

 471 | record SelectZones where

 472 |   constructor SZ

 473 |   dragUL : Point Id -- upper left corner for dragging

 474 |   dragLR : Point Id -- lower right corner for dragging

 475 |   rotUL  : Point Id -- upper left corner for rotating

 476 |   rotLR  : Point Id -- lower right corner for rotating

 481 | select : (start,end : Point Id) -> CDGraph -> CDGraph

 482 | select s e (G o g) = G o $ mapWithCtxt sel g

 483 |   where

 484 |     sel : Fin o -> Adj o CDBond CDAtom -> CDAtom

 485 |     sel n (A a _) =

 486 |       let p := pointId a

 487 |        in setIf Selected (is Hover a || (visible g n && inRectangle p s e)) a

 495 | isSelected : CDIGraph k -> (includeEdges : Bool) -> Fin k -> Bool

 496 | isSelected g include n =

 497 |   let A a bs := adj g n

 498 |    in is Selected a || (include && any (is Selected) bs)

 502 | selectedNodes : {k : _} -> CDIGraph k -> (includeEdges : Bool) -> List (Fin k)

 503 | selectedNodes g include = filter (isSelected g include) (nodes g)

 507 | selectedEdges : {k : _} -> CDIGraph k -> List (Fin k, Fin k)

 508 | selectedEdges =

 509 |   mapMaybe (\(E x y b) => if is Selected b then Just (x,y) else Nothing) . edges

 512 | selectedItems : {k : _} -> CDIGraph k -> NOE (List $ Fin k) (List (Fin k, Fin k))

 513 | selectedItems g = eons (selectedNodes g False) (selectedEdges g)

 515 | nodeBounds : CDIGraph k -> Fin k -> Bounds2D Mol

 516 | nodeBounds g = bounds . lab g

 518 | edgeBounds : CDIGraph k -> (Fin k,Fin k) -> Bounds2D Mol

 519 | edgeBounds g (x,y) = bounds (lab g x) <+> bounds (lab g y)

 524 | selectionCorners : CDGraph -> Maybe (Point Mol, Point Mol)

 525 | selectionCorners (G o g) =

 526 |   case selectedItems g of

 527 |     N ns@(_ :: _ :: _) => corners $ foldMap (nodeBounds g) ns

 528 |     E ps               => corners $ foldMap (edgeBounds g) ps

 529 |     _                  => Nothing

 533 | selectZones : (s : CoreDims) => (p1,p2 : Point Id) -> SelectZones

 534 | selectZones p1 p2 =

 535 |   let b  := s.selectBufferSize

 536 |       bs := bounds p1 <+> bounds p2

 538 |       -- translation vector for the two corners of the inner buffer

 539 |       -- this is zero if the bounding box formed by `p1` and `p2` is

 540 |       -- already large enough, otherwise both dimensions are expanded as

 541 |       -- needed

 542 |       vd := scale 0.5 $ V (max 0 (b - width bs)) (max 0 (b - height bs))

 543 |       vr := vid b b

 544 |       d1 := translate (negate vd) p1

 545 |       d2 := translate vd p2

 546 |    in SZ d1 d2 (translate (negate vr) d1) (translate vr d2)

 554 | isotopeAt : Isotope -> Point Id -> Role -> CDAtom

 555 | isotopeAt i p r =

 556 |   let pos := toCoords (convert p) [0,0,0]

 557 |    in CA r (MkAtom i 0 pos NoRadical 0 unknown () Nothing)

 560 | export %inline

 561 | elemAt : Elem -> Point Id -> Role -> CDAtom

 562 | elemAt = isotopeAt . cast

 566 | export %inline

 567 | insIsotopeAt :

 568 |      {k : _}

 569 |   -> CDIGraph k

 570 |   -> Isotope

 571 |   -> Point Id

 572 |   -> Role

 573 |   -> CDIGraph (S k)

 574 | insIsotopeAt g i p r = insNode g (isotopeAt i p r)

 578 | export %inline

 579 | insElemAt : {k : _} -> CDIGraph k -> Elem -> Point Id -> Role -> CDIGraph (S k)

 580 | insElemAt g = insIsotopeAt g . cast

 585 | preferredAngle : (isLinear : Bool) -> List Angle -> Angle

 586 | preferredAngle _     []  = (negate 1.0 / 6.0) * pi

 587 | preferredAngle True  [x] = x + pi

 588 | preferredAngle False [x] =

 589 |   if (x >= zero && x <= halfPi) || (x >= pi && x <= threeHalfPi)

 590 |      then x + twoThirdPi

 591 |      else x - twoThirdPi

 592 | preferredAngle _     xs  = largestBisector xs

 595 | isLinear : List BondOrder -> Bool

 596 | isLinear [Triple,_] = True

 597 | isLinear [_,Triple] = True

 598 | isLinear [Dbl,Dbl]  = True

 599 | isLinear _          = False

 604 | bestPos : CDIGraph k -> MolBond -> Fin k -> Point Id -> Point Id

 605 | bestPos g b n p =

 606 |   let orders   := b.type :: map (type . molBond) (edgeLabels g n)

 607 |       newAngle := preferredAngle (isLinear orders) (bondAngles g n)

 608 |    in translate (polar BondLengthInPixels newAngle) p

 612 | stepAngles : (s : CoreDims) => List Angle

 613 | stepAngles =

 614 |   let step = angle (TwoPi / cast s.angleSteps)

 615 |    in map (\x => cast x * step) [0.. pred s.angleSteps]

 621 | suggestedPos : CoreDims => Bool -> (atom, current : Point Id) -> Point Id

 622 | suggestedPos True pa pc = pc

 623 | suggestedPos False pa pc =

 624 |   let Just mouseAngle := angle (pc - pa) | Nothing => pc

 625 |       Just bondAngle  := closestAngle mouseAngle stepAngles | Nothing => pc

 626 |    in translate (polar BondLengthInPixels bondAngle) pa

 632 | bondTo :

 633 |      {k : _}

 634 |   -> {auto s : CoreDims}

 635 |   -> CDBond

 636 |   -> Fin k

 637 |   -> (current, suggested : Point Id)

 638 |   -> CDIGraph k

 639 |   -> Either (CDIGraph k) (CDIGraph $ S k)

 640 | bondTo b n pc ps g =

 641 |   maybe

 642 |     (Right $ insEdge (edge n b) (insElemAt g C ps New))

 643 |     (\e => Left $ insEdge e g)

 644 |     (closeEdge pc <|> closeEdge ps)

 645 |   where

 646 |     closeEdge : Point Id -> Maybe (Edge k CDBond)

 647 |     closeEdge p = closestNode p g >>= \k => mkEdge n k b

 652 | nodesToMerge :

 653 |      {k,m : _}

 654 |   -> {auto s : CoreDims}

 655 |   -> CDIGraph k

 656 |   -> CDIGraph m

 657 |   -> List (Fin k, Fin m)

 658 | nodesToMerge g t =

 659 |  let area := overlap {margin = s.radiusAtom }(bounds g) (Geom.Bounds.bounds t)

 660 |      ng   := g `atomsIn` area

 661 |      nt   := t `atomsIn` area

 662 |   in mapMaybe (\x => (x,) <$> closestNodeList nt (pointAt g x) t) ng

 665 | offset : CDIGraph k -> CDIGraph m -> List (Fin k, Fin m) -> Vector (transform Mol)

 666 | offset _  _  []             = vzero

 667 | offset g1 g2 ((n1,n2) :: _) = point (lab g1 n1) - point (lab g2 n2)

 671 | newEdges :

 672 |      {k,m : _}

 673 |   -> CDIGraph m

 674 |   -> List (Fin k, Fin m)

 675 |   -> List (Fin k, Fin m, CDBond)

 676 | newEdges t ps = do

 677 |   (a1,a2) <- ps

 678 |   (\(x,l) => (a1,x,l)) <$> neighboursAsPairs t a2

 680 | inBond : {m : _} -> (n1,n2 : Fin m) -> Edge m CDBond -> Bool

 681 | inBond n1 n2 bnd =

 682 |   (n1 == bnd.node1 && n2 == bnd.node2) || (n2 == bnd.node1 && n1 == bnd.node2)

 686 | createStableBond :

 687 |      {k,m : _}

 688 |   -> List (Fin k, Fin m)

 689 |   -> List (Edge k CDBond)

 690 |   -> Edge m CDBond

 691 |   -> Maybe $ Edge k CDBond

 692 | createStableBond nsToMerge bondsG bnd =

 693 |   case filter (\(_,nt) => nt == bnd.node1 || nt == bnd.node2) nsToMerge of

 694 |     [(nm1,_),(nm2,_)] =>

 695 |       if any (inBond nm1 nm2) bondsG

 696 |          then Nothing

 697 |          else mkEdge nm1 nm2 $ CB None ({type := Single} bnd.label.molBond)

 698 |     _                  => Nothing

 700 | incNode : {m : _} -> (k : Nat) -> Fin m -> Maybe (Fin $ k + m)

 701 | incNode k x = tryNatToFin (k + finToNat x)

 706 | mergeCloseNodes : CoreDims => {k:_} -> CDIGraph k -> CDGraph

 707 | mergeCloseNodes g =

 708 |   let ns        := filter (not . inAbbreviation g) (selectedNodes g True)

 709 |       lMergeN   := mapMaybe closestPair ns

 710 |       offset    := negate $ offset g g lMergeN

 711 |       lnewBonds := mapMaybe (\(x,y,l) => mkEdge x y l) (newEdges g lMergeN)

 712 |       mol'      := insEdges lnewBonds $ mapIf doAdjust (translate offset) g

 713 |    in delNodes (map snd lMergeN) mol'

 715 |   where

 716 |     canSelfMerge : Fin k -> Bool

 717 |     canSelfMerge x =

 718 |       let a := lab g x in not (isSelected g True x || inAnyGroup a)

 720 |     doAdjust : CDAtom -> Bool

 721 |     doAdjust a = is Selected a

 723 |     closestPair : Fin k -> Maybe (Fin k, Fin k)

 724 |     closestPair x = (x,) <$> closestNodeWhere canSelfMerge (pointAt g x) g

 730 | mergeGraphs' :

 731 |      {auto _ : CoreDims}

 732 |   -> {k,m:_}

 733 |   -> CDIGraph k

 734 |   -> CDIGraph m

 735 |   -> List (Fin k, Fin m, CDBond)

 736 |   -> CDGraph

 737 | mergeGraphs' g t bs =

 738 |   let t'        := adjTemplate g t

 739 |       lMergeN   := nodesToMerge g t'

 740 |       offset    := offset g t' lMergeN

 741 |       lnewBonds := newEdges t' lMergeN ++ bs

 742 |       mergeEsG  := lMergeN >>= edgesTo g . fst

 743 |       mergeEsT  := lMergeN >>= edgesTo t' . snd

 744 |       -- replaces bonds between merging (and therefore to be deleted) template

 745 |       -- atoms and origin atoms

 746 |       -- this is only done if there isn't already a bond from the origin

 747 |       -- molecule present at the same position

 748 |       mol'      :=

 749 |         insEdges (mapMaybe (createStableBond lMergeN mergeEsG) mergeEsT) g

 750 |       mol''     := mergeGraphsWithEdges mol' (translate offset t') lnewBonds

 751 |    in delNodes (mapMaybe (incNode k . snd) lMergeN) mol''

 757 | mergeGraphsOnAtom : CoreDims => {k,m : _} -> Fin k -> CDIGraph k -> CDIGraph m -> CDGraph

 758 | mergeGraphsOnAtom {m = 0}   _ g _ = G _ g

 759 | mergeGraphsOnAtom {m = S _} n g t =

 760 |   let as     := bondAngles g n

 761 |       an     := preferredAngle False as

 762 |       a0     := preferredAngle False (bondAngles t 0)

 763 |       tr     := rotate (an - a0 + pi) t

 764 |       offset := point (lab g n) - point (lab tr 0)

 765 |       v      := polar BondLengthInAngstrom an + offset

 766 |       bond   := CB New $ cast Single

 767 |    in mergeGraphs' g (translate v tr) [(n,0,bond)]

 779 | mergeGraphsOnBond :

 780 |      {k,m : _}

 781 |   -> {auto cd : CoreDims}

 782 |   -> Point Mol

 783 |   -> Edge k CDBond

 784 |   -> CDIGraph k

 785 |   -> CDIGraph m

 786 |   -> CDGraph

 787 | mergeGraphsOnBond p (E n1 n2 _) g t =

 788 |   case edges t of

 789 |     []      => G k g

 790 |     E n3 n4 _ :: _ =>

 791 |       let Just ag := angle (pointAt g n1 - pointAt g n2) | Nothing => G k g

 792 |           Just at := angle (pointAt t n3 - pointAt t n4) | Nothing => G k g

 793 |           tr1     := rotate (ag - at) t

 794 |           tt1     := translate (point (lab g n1) - point (lab tr1 n3)) tr1

 795 |           tr2     := rotate (ag - at + pi) t

 796 |           tt2     := translate (point (lab g n1) - point (lab tr2 n4)) tr2

 797 |        in if distance p (center tt1) <= distance p (center tt2)

 798 |              then mergeGraphs' g tt1 []

 799 |              else mergeGraphs' g tt2 []

 804 | mergeGraphs : CoreDims => Point Id -> (g, t : CDGraph) -> CDGraph

 805 | mergeGraphs c (G o1 g) (G o2 t) =

 806 |   case hoveredItem g of

 807 |     N k  => mergeGraphsOnAtom (fst k) g t

 808 |     E e  => mergeGraphsOnBond (convert c) e g t

 809 |     None => mergeGraphs' g t []

 817 | rotTemplOnAtom :

 818 |      {auto _ : CoreDims}

 819 |   -> {s,k,m : _}

 820 |   -> (cursor : Point s)

 821 |   -> (clickedAtom : Fin k)

 822 |   -> (mol : CDIGraph k)

 823 |   -> (templ : CDIGraph m)

 824 |   -> CDIGraph m

 825 | rotTemplOnAtom {m = 0}   _ _ _ t = t

 826 | rotTemplOnAtom {m = S _} p n g t =

 827 |   let pMol    := point $ lab g n

 828 |       a0      := preferredAngle False (bondAngles t 0)

 829 |       an      := preferredAngle False (bondAngles g n)

 830 |       angle   := an - a0 + pi

 831 |       tr      := rotate angle t

 832 |       offset  := pMol - point (lab tr 0)

 833 |       v       := polar BondLengthInAngstrom an + offset

 834 |       tr'     := translate v tr

 835 |       Just aT := Vector.angle (pMol - center tr') | Nothing => tr'

 836 |       Just aM := Vector.angle (pMol - convert p)  | Nothing => tr'

 837 |       aSteps  := fromMaybe (aM - aT) (closestAngle (aM - aT) stepAngles)

 838 |    in if distance (convert p) (point (lab g n)) <

 839 |          value (BondLengthInAngstrom / 4)

 840 |          then tr'

 841 |          else rotateAt pMol aSteps tr'

 850 | rotTemplAroundOverlap :

 851 |      {auto _ : CoreDims}

 852 |   -> {s,k,m : _}

 853 |   -> (initCursor,cursor : Point s)

 854 |   -> (aMol : Fin k)

 855 |   -> (aTempl : Fin m)

 856 |   -> (mol : CDIGraph k)

 857 |   -> (templ : CDIGraph m)

 858 |   -> CDGraph

 859 | rotTemplAroundOverlap ip p nm nt g t =

 860 |   let pMol    := point $ lab g nm

 861 |       pTemA   := point $ lab t nt

 862 |       offset  := pMol - pTemA

 863 |       t'      := translate offset t

 864 |       Just a0 := angle (pMol - center t') | Nothing => G _ t'

 865 |       Just aM := angle (pMol - convert p) | Nothing => G _ t'

 866 |       angle   := aM - a0

 867 |       aSteps  := fromMaybe angle (closestAngle angle stepAngles)

 868 |    in if distance ip p > value (BondLengthInAngstrom / 4)

 869 |          then G _ $ rotateAt pMol aSteps t'

 870 |          else G _ t'

 878 | addBondE :

 879 |      {k : _}

 880 |   -> {t : _}

 881 |   -> {auto cd   : CoreDims}

 882 |   -> (shiftDown : Bool)

 883 |   -> (mousePos  : Maybe $ Point t)

 884 |   -> (newBond   : MolBond)

 885 |   -> CDIGraph k

 886 |   -> Either (CDIGraph k) (CDIGraph $ S k)

 887 | addBondE @{cd} shiftDown p mb g =

 888 |   let b          := CB New mb -- new `CDBond`

 889 |       Just (n,a) := find (is Origin . snd) (labNodes g) | Nothing => Left g

 890 |       pa         := pointId a -- position of atom we attach new bond to

 891 |       pc         := maybe pa pointId p -- current mouse position

 892 |       

 893 |    in if near pa pc cd.radiusAtom

 894 |          -- if mouse is close to origin atom

 895 |          -- use largest bisector as new bond angle and draw a bond

 896 |          -- of preferred length

 897 |          then bondTo b n pc (bestPos g mb n pa) g

 898 |   

 899 |          -- else use an angle close to the one of the vector connecting

 900 |          -- the origin atom and the mouse pointer, unless "Shift" is down,

 901 |          -- in which case we use the mouse position without modification

 902 |          else bondTo b n pc (suggestedPos shiftDown pa pc) g

 910 | addBond :

 911 |      {k : _}

 912 |   -> {t : _}

 913 |   -> {auto cd   : CoreDims}

 914 |   -> (shiftDown : Bool)

 915 |   -> (mousePos  : Maybe $ Point t)

 916 |   -> (newBond   : MolBond)

 917 |   -> CDIGraph k

 918 |   -> CDGraph

 919 | addBond sd p mb g = either (G k) (G $ S k) (addBondE sd p mb g)

 926 | addAtom :

 927 |      {auto cd : CoreDims}

 928 |   -> {t : _}

 929 |   -> {k : _}

 930 |   -> CDIGraph k

 931 |   -> Isotope

 932 |   -> Point t

 933 |   -> CDGraph

 934 | addAtom g i p =

 935 |   case hoveredItem g of

 936 |     N (x,_) => 

 937 |       let g2 := setNode x (isotopeAt i (pointAt g x) New) g

 938 |        in delNodes (groupNodes g [x]) g2

 939 |     _       => case closestNode (convert p) g of

 940 |       Nothing => G _ $ insIsotopeAt g i (convert p) New

 942 |       -- in the `Just` case, we have a node close to the mouse pointer

 943 |       -- that is not set to "hovered". This means, replacing that node is

 944 |       -- a non-op. We don't want to insert another atom on top of it, so

 945 |       -- we return the graph unmodified.

 946 |       Just _  => G _ g

 949 | setAbbreviationAt :

 950 |      {auto cd : CoreDims}

 951 |   -> {k,m        : Nat}

 952 |   -> (lbl        : String)

 953 |   -> (node,neigh : Fin k)

 954 |   -> (abbr       : CDIGraph (S m))

 955 |   -> (mol        : CDIGraph k)

 956 |   -> CDGraph

 957 | setAbbreviationAt lbl n1 n2 a g =

 958 |   let nr      := S (maxGroupNr g)

 959 |       pn      := point (lab g n1) -- position of label

 960 |       pc      := point (lab g n2) -- node to which label is connected

 961 |       Just an := angle (pn - pc) | Nothing => G k g

 962 |       a0      := preferredAngle False (bondAngles a 0)

 963 |       ar      := rotate (an-a0+pi) (setGroup (G nr lbl) <$> a)

 964 |       at      := translate (pn - point (lab ar 0)) ar

 965 |       bond    := CB New $ maybe (cast Single) molBond (elab g n1 n2)

 966 |       gm      := mergeGraphsWithEdges g at [(n2,0,bond)]

 967 |    in delNodes (plusGroupNodes gm [weakenN _ n1]) gm

 972 | setAbbreviation :

 973 |      {auto cd : CoreDims}

 974 |   -> (shiftDown : Bool)

 975 |   -> (lbl       : String)

 976 |   -> (mouse     : Point Id)

 977 |   -> (abbr      : CDGraph)

 978 |   -> (mol       : CDGraph)

 979 |   -> CDGraph

 980 | setAbbreviation _  lbl mouse (G 0 _) g = g

 981 | setAbbreviation sd lbl mouse (G (S m) a) (G k g) =

 982 |   case find (is Origin . snd) (labNodes g) of

 983 |     Nothing     => G k g

 984 |     Just (n1,_) => case visibleNeighbours g n1 of

 985 |       [n2] => setAbbreviationAt lbl n1 n2 a g

 986 |       _    => case addBondE sd (Just mouse) (cast Single) g of

 987 |         Left _   => G k g

 988 |         Right g2 => setAbbreviationAt lbl last (weaken n1) a g2

 992 | expand : CDGraph -> CDGraph

 993 | expand (G o g) =

 994 |   let N (n1,CA _ a) := hoveredItem g | _ => G o g

 995 |       Just (G n _)  := label a       | _ => G o g

 996 |    in G o $ map (clearGroup n) g

 998 | %inline new : CDBond -> CDBond

 999 | new = {role := New}

1001 | %inline translateTemplateAtom : Vector (transform Mol) -> CDAtom -> CDAtom

1002 | translateTemplateAtom v (CA _ a) = CA None $ translate v a

1006 | translateTemplate :

1007 |      {auto _ : CoreDims}

1008 |   -> {s : _}

1009 |   -> Point s

1010 |   -> (t : CDGraph)

1011 |   -> CDGraph

1012 | translateTemplate p t =

1013 |   let v := convert p - center t in bimap new (translateTemplateAtom v) t

1018 | addTemplate : CoreDims => {s : _} -> Point s -> (t, mol : CDGraph) -> CDGraph

1019 | addTemplate p t mol =

1020 |   let v := convert p - center t

1021 |    in mergeGraphs (convert p) mol (bimap new (translateTemplateAtom v) t)

1030 | addTemplateRot :

1031 |      {auto _ : CoreDims}

1032 |   -> {s,k,n : _}

1033 |   -> (cursor : Point s)

1034 |   -> Either (Fin n) (Fin n, Fin k, Point s)

1035 |   -> (templ : CDIGraph k)

1036 |   -> (mol : CDIGraph n)

1037 |   -> CDGraph

1038 | addTemplateRot {n = S j,k = S i} p (Left f) t m =

1039 |   let rotTemp := rotTemplOnAtom p f m t

1040 |       bnd     := CB New $ cast Single

1041 |    in mergeGraphs' m rotTemp [(f,0,bnd)]

1042 | addTemplateRot {n = S j,k = S i} p (Right (fm,ft,ip)) t m =

1043 |   let (G _ rotTemp) := rotTemplAroundOverlap ip p fm ft m t

1044 |    in mergeGraphs' m rotTemp []

1045 | addTemplateRot _ _ _ m = G _ m

1051 | clearOrphanGroups : {k : _} -> List (Fin k) -> CDIGraph k -> CDIGraph k 

1052 | clearOrphanGroups ns g =

1053 |   let gs@(_::_) := ns >>= toList . groupNr g | Nil => g

1054 |    in map (\x => foldl (flip clearGroup) x gs) g

1070 | deleteSelected : CDGraph -> CDGraph

1071 | deleteSelected (G o g) =

1072 |   case selectedItems g of

1073 |     None => case hoveredItem g of

1074 |       None => G o g

1075 |       N x  => delNS [fst x]

1076 |       E x  => delES [(node1 x, node2 x)]

1077 |     N ns => delNS ns

1078 |     E es => delES es

1080 |   where

1081 |     delNS : List (Fin o) -> CDGraph

1082 |     delNS ns = delNodes (plusGroupNodes g ns) g

1084 |     delES : List (Fin o,Fin o) -> CDGraph

1085 |     delES es =