
   0 | module Chem.Formula
   1 | 
   2 | import Chem.Elem
   3 | import Data.Maybe.Upper
   4 | import Data.Nat
   5 | import Data.Prim.String
   6 | import Derive.Prelude
   7 | 
   8 | %default total
   9 | 
  10 | ||| Utility for ordering elements according to Hill notation.
  11 | public export %inline
  12 | hill : Elem -> String
  13 | hill C = ""
  14 | hill H = " "
  15 | hill e = symbol e
  16 | 
  17 | ||| Alias for `Upper (<)`: Used as a proof that the first
  18 | ||| string comes before the second or that the second
  19 | ||| value equals `Nothing`.
  20 | public export
  21 | 0 (<): Maybe String -> Maybe String -> Type
  22 | (<) = Upper (<)
  23 | 
  24 | ||| A proof that the first string is less than or equal
  25 | ||| to the second string. A `Nothing` is treated as being
  26 | ||| greater than all `Just`s.
  27 | public export
  28 | 0 (<=): Maybe String -> Maybe String -> Type
  29 | m1 <= m2 = Either (m1 < m2) (m1 === m2)
  30 | 
  31 | ||| A provably sorted, normalized representation
  32 | ||| of molecular formulae as a list of element-count
  33 | ||| pairs.
  34 | |||
  35 | ||| This is indexed by the Hill-string of the head element
  36 | ||| (if any) to help with the proof of the list being properly
  37 | ||| sorted.
  38 | public export
  39 | data Repr : (ix : Maybe String) -> Type where
  40 |   Nil : Repr Nothing
  41 |   (::) :  {0 ix : _}
  42 |        -> (p     : (Elem,Nat))
  43 |        -> (ps    : Repr ix)
  44 |        -> {auto 0 prf : Just (hill $ fst p) < ix}
  45 |        -> {auto 0 nz  : IsSucc (snd p)}
  46 |        -> Repr (Just $ hill $ fst p)
  47 | 
  48 | --------------------------------------------------------------------------------
  49 | --          Merging Formulae
  50 | --------------------------------------------------------------------------------
  51 | 
  52 | ||| Result of computing the union of two molecular formulae with
  53 | ||| elem indices `e1` and `e2`. The result's elem index is equal to either
  54 | ||| `e1` or `e2`
  55 | public export
  56 | record MergeRes (h1,h2 : Maybe String) where
  57 |   constructor MR
  58 |   {0 hx  : Maybe String}
  59 |   repr   : Repr hx
  60 |   0 prf  : Either (h1 === hx) (h2 === hx)
  61 | 
  62 | 0 trans_LT_EQ : {0 lt : _} -> Transitive a lt => lt x y -> y === z -> lt x z
  63 | trans_LT_EQ w Refl = w
  64 | 
  65 | %inline
  66 | prepLT : (p : (Elem,Nat))
  67 |        -> MergeRes h1 (Just k2)
  68 |        -> (0 prf1 : Just (hill $ fst p) < h1)
  69 |        => (0 prf2 : Just (hill $ fst p) < Just k2)
  70 |        => (0 nz   : IsSucc (snd p))
  71 |        => MergeRes (Just $ hill $ fst p) (Just k2)
  72 | prepLT p (MR ps prf) =
  73 |   let 0 lt = either (trans_LT_EQ prf1) (trans_LT_EQ prf2) prf
  74 |    in MR (p :: ps) (Left Refl)
  75 | 
  76 | %inline
  77 | prepGT : (p : (Elem,Nat))
  78 |        -> MergeRes (Just k1) e2
  79 |        -> (0 prf1 : Just (hill $ fst p) < e2)
  80 |        => (0 prf2 : Just (hill $ fst p) < Just k1)
  81 |        => (0 nz   : IsSucc (snd p))
  82 |        => MergeRes (Just k1) (Just $ hill $ fst p)
  83 | prepGT p (MR ps prf) =
  84 |   let 0 lt = either (trans_LT_EQ prf2) (trans_LT_EQ prf1) prf
  85 |    in MR (p :: ps) (Right Refl)
  86 | 
  87 | %inline
  88 | prepEQ :  {0 x : Maybe String}
  89 |        -> (p : (Elem,Nat))
  90 |        -> (0 eq  : hill (fst p) === k)
  91 |        -> MergeRes h1 h2
  92 |        -> (0 prf1 : Just (hill $ fst p) < h1)
  93 |        => (0 prf2 : Just k < h2)
  94 |        => (0 nz   : IsSucc (snd p))
  95 |        => MergeRes (Just $ hill $ fst p) x
  96 | prepEQ p eq (MR ps prf) =
  97 |   let 0 fstp_lt_m2 = rewrite eq in prf2
  98 |       0 lt = either (trans_LT_EQ prf1) (trans_LT_EQ fstp_lt_m2) prf
  99 |    in MR (p :: ps) (Left Refl)
 100 | 
 101 | 0 plusSucc : (m,n : Nat) -> (0 prf : IsSucc m) => IsSucc (m + n)
 102 | plusSucc (S k) n = ItIsSucc
 103 | plusSucc Z n impossible
 104 | 
 105 | ||| Merges to molecular formulae making sure by design that the
 106 | ||| result ist still normalized, that is, entries are ordered
 107 | ||| according to Hill notation, and all counts are positive.
 108 | export
 109 | merge : Repr h1 -> Repr h2 -> MergeRes h1 h2
 110 | merge xs@(p :: ps) ys@(q :: qs) = case comp (hill $ fst p) (hill $ fst q) of
 111 |   LT prf _   _   => prepLT p $ merge ps ys
 112 |   EQ _   prf _   =>
 113 |     let 0 nz := plusSucc (snd p) (snd q)
 114 |      in prepEQ (fst p, snd p + snd q) prf $ merge ps qs
 115 |   GT _   _   prf => prepGT q $ merge xs qs
 116 | merge y [] = MR y (Left Refl)
 117 | merge [] y = MR y (Right Refl)
 118 | 
 119 | ||| Extract the key-value pairs from a molecular formula.
 120 | export
 121 | pairs : Repr h1 -> List (Elem,Nat)
 122 | pairs (h :: t) = h :: pairs t
 123 | pairs []       = []
 124 | 
 125 | --------------------------------------------------------------------------------
 126 | --          Comparisons
 127 | --------------------------------------------------------------------------------
 128 | 
 129 | ||| Heterogeneous comparison of molecular formulae
 130 | public export
 131 | hcomp : Repr h1 -> Repr h2 -> Ordering
 132 | hcomp (p :: ps) (q :: qs) = case compare (hill $ fst p) (hill $ fst q) of
 133 |   EQ => case compare (snd p) (snd q) of
 134 |     EQ => hcomp ps qs
 135 |     o  => o
 136 |   o => o
 137 | hcomp []        []        = EQ
 138 | hcomp []        _         = LT
 139 | hcomp _         []        = GT
 140 | 
 141 | ||| Heterogeneous equality between molecular formulae
 142 | public export
 143 | heq : Repr h1 -> Repr h2 -> Bool
 144 | heq x y = hcomp x y == EQ
 145 | 
 146 | ||| True if the first formula has at least as many atoms of each element
 147 | ||| as the second formula.
 148 | public export
 149 | contains_ : Repr h1 -> Repr h2 -> Bool
 150 | contains_ (p :: ps) (q :: qs) = case compare (hill $ fst p) (hill $ fst q) of
 151 |   LT => contains_ ps (q :: qs)
 152 |   EQ => snd p >= snd q && contains_ ps qs
 153 |   GT => False
 154 | contains_ _  [] = True
 155 | contains_ [] _  = False
 156 | 
 157 | --------------------------------------------------------------------------------
 158 | --          Formula
 159 | --------------------------------------------------------------------------------
 160 | 
 161 | ||| A provably normalized molecular formula.
 162 | |||
 163 | ||| This is just a wrapper around `Repr mx`, the representation of a
 164 | ||| molecular formula as a provably sorted list of pairs.
 165 | public export
 166 | record Formula where
 167 |   constructor F
 168 |   {0 mx : Maybe String}
 169 |   pairs : Repr mx
 170 | 
 171 | public export %inline
 172 | Eq Formula where
 173 |   F x == F y = heq x y
 174 | 
 175 | public export %inline
 176 | Ord Formula where
 177 |   compare (F x) (F y) = hcomp x y
 178 | 
 179 | showPair : (Elem,Nat) -> String
 180 | showPair (e, 1) = symbol e
 181 | showPair (e, n) = symbol e ++ show n
 182 | 
 183 | export
 184 | Show Formula where
 185 |   show (F ps) = fastConcat $ map showPair (pairs ps)
 186 | 
 187 | export %inline
 188 | Interpolation Formula where
 189 |   interpolate = show
 190 | 
 191 | export %inline
 192 | Semigroup Formula where
 193 |   F x <+> F y = F (repr $ merge x y)
 194 | 
 195 | export %inline
 196 | Monoid Formula where
 197 |   neutral = F []
 198 | 
 199 | ||| Creates a molecular formula with the given element and count.
 200 | export %inline
 201 | singleton : Elem -> (n : Nat) -> Formula
 202 | singleton e 0     = F []
 203 | singleton e (S n) = F [(e,S n)]
 204 | 
 205 | ||| True, if the first `Formula` contains at least the atoms listed
 206 | ||| in the second formula, that is, all elements in the second formula
 207 | ||| apear at the same or a higher count in the first.
 208 | export %inline
 209 | contains : Formula -> Formula -> Bool
 210 | contains (F x) (F y) = contains_ x y
 211 | 
 212 | ||| Inserts an element plus count into a molecular formula.
 213 | export
 214 | insert : Elem -> Nat -> Formula -> Formula
 215 | insert el 0 f = f
 216 | insert el n f = singleton el n <+> f
 217 | 
 218 | ||| Inserts an element at count 1 into a molecular formula.
 219 | export
 220 | insertElem : Elem -> Formula -> Formula
 221 | insertElem el f = singleton el 1 <+> f
 222 | 
 223 | --------------------------------------------------------------------------------
 224 | --          Tests
 225 | --------------------------------------------------------------------------------
 226 | 
 227 | 0 containsTest1 : contains (F [(C,2),(H,6), (O,1)]) (F [(H,2),(O,1)]) === True
 228 | containsTest1 = Refl
 229 | 
 230 | 0 containsTest2 : contains (F [(H,1),(F,1)]) (F [(H,2),(O,1)]) === False
 231 | containsTest2 = Refl
 232 | 
 233 | 0 containsTest3 : contains (F []) (F [(H,2)]) === False
 234 | containsTest3 = Refl
 235 | 
 236 | 0 containsTest4 : contains (F []) (F []) === True
 237 | containsTest4 = Refl
 238 |