0 | module CyBy.Draw.Internal.Atom
 1 |
 2 | import CyBy.Draw.Internal.Role
 3 | import Derive.Prelude
 4 | import Geom
 5 | import Text.Molfile
 6 |
 7 | %language ElabReflection
 8 | %default total
 9 |
10 | ||| Atom type used in the application state of cyby-draw.
11 | |||
12 | ||| This is a mol-file atom with perceived atom type paired with a role
13 | ||| used for drawing.
14 | public export
15 | record CDAtom where
16 |   constructor CA
17 |   role : Role
18 |   atom : MolAtomAT
19 |
20 | %runElab derive "CDAtom" [Show,Eq]
21 |
22 | export %inline
23 | group : CDAtom -> Maybe AtomGroup
24 | group = label . atom
25 |
26 | export %inline
27 | inAnyGroup : CDAtom -> Bool
28 | inAnyGroup = isJust . group
29 |
30 | ||| Sets the given `AtomGroup` (abbreviation) at an atom
31 | export
32 | setGroup : AtomGroup -> CDAtom -> CDAtom
33 | setGroup g (CA r a) = CA r $ {label := Just g} a
34 |
35 | ||| Unsets the abbreviation label of an atom if it belongs to
36 | ||| the given group.
37 | export
38 | clearGroup : (group : Nat) -> CDAtom -> CDAtom
39 | clearGroup g (CA r a) = CA r $ {label $= (>>= clear)} a
40 |   where
41 |     clear : AtomGroup -> Maybe AtomGroup
42 |     clear (G x l) = if x == g then Nothing else (Just $ G x l)
43 |
44 | ||| True, if the given atom is part of the abbreviation with the given ID.
45 | export %inline
46 | inGroup : Nat -> CDAtom -> Bool
47 | inGroup n (CA _ a) = 
48 |   case a.label of
49 |     Nothing      => False
50 |     Just (G m _) => n == m
51 |
52 | --------------------------------------------------------------------------------
53 | -- Implementations
54 | --------------------------------------------------------------------------------
55 |
56 | export %inline
57 | Cast CDAtom Role where cast = role
58 |
59 | export %inline
60 | Cast (Adj k b CDAtom) Role where cast = cast . label
61 |
62 | export %inline
63 | Cast (Context k b CDAtom) Role where cast = cast . label
64 |
65 | export %inline
66 | ModRole CDAtom where modRole f = {role $= f}
67 |
68 | public export
69 | GetPoint CDAtom where
70 |   gtrans = Mol
71 |   point  = point . position . atom
72 |
73 | export %inline
74 | Cast CDAtom Elem where cast = elem . elem . atom
75 |
76 | public export
77 | ModPoint CDAtom where
78 |   mtrans = Mol
79 |   modPoint f (CA r v) = CA r $ {position $= modPoint f} v
80 |