Chem.Formula

Definitions

hill : Elem -> String

  Utility for ordering elements according to Hill notation.

Totality: total
Visibility: public export

0 (<) : Maybe String -> Maybe String -> Type

  Alias for `Upper (<)`: Used as a proof that the first
  string comes before the second or that the second
  value equals `Nothing`.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6

0 (<=) : Maybe String -> Maybe String -> Type

  A proof that the first string is less than or equal
  to the second string. A `Nothing` is treated as being
  greater than all `Just`s.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6

data Repr : Maybe String -> Type

  A provably sorted, normalized representation
  of molecular formulae as a list of element-count
  pairs.
  
  This is indexed by the Hill-string of the head element
  (if any) to help with the proof of the list being properly
  sorted.

Totality: total
Visibility: public export
Constructors:

Nil : Repr Nothing

(::) : (p : (Elem, Nat)) -> Repr ix -> {auto 0 _ : Just (hill (fst p)) < ix} -> {auto 0 _ : IsSucc (snd p)} -> Repr (Just (hill (fst p)))

record MergeRes : Maybe String -> Maybe String -> Type

  Result of computing the union of two molecular formulae with
  elem indices `e1` and `e2`. The result's elem index is equal to either
  `e1` or `e2`

Totality: total
Visibility: public export
Constructor: 

MR : Repr hx -> (0 _ : Either (h1 = hx) (h2 = hx)) -> MergeRes h1 h2

Projections:

0 .hx : MergeRes h1 h2 -> Maybe String

0 .prf : ({rec:0} : MergeRes h1 h2) -> Either (h1 = hx {rec:0}) (h2 = hx {rec:0})

.repr : ({rec:0} : MergeRes h1 h2) -> Repr (hx {rec:0})

0 .hx : MergeRes h1 h2 -> Maybe String

Totality: total
Visibility: public export

0 hx : MergeRes h1 h2 -> Maybe String

Totality: total
Visibility: public export

.repr : ({rec:0} : MergeRes h1 h2) -> Repr (hx {rec:0})

Totality: total
Visibility: public export

repr : ({rec:0} : MergeRes h1 h2) -> Repr (hx {rec:0})

Totality: total
Visibility: public export

0 .prf : ({rec:0} : MergeRes h1 h2) -> Either (h1 = hx {rec:0}) (h2 = hx {rec:0})

Totality: total
Visibility: public export

0 prf : ({rec:0} : MergeRes h1 h2) -> Either (h1 = hx {rec:0}) (h2 = hx {rec:0})

Totality: total
Visibility: public export

merge : Repr h1 -> Repr h2 -> MergeRes h1 h2

  Merges to molecular formulae making sure by design that the
  result ist still normalized, that is, entries are ordered
  according to Hill notation, and all counts are positive.

Totality: total
Visibility: export

pairs : Repr h1 -> List (Elem, Nat)

  Extract the key-value pairs from a molecular formula.

Totality: total
Visibility: export

hcomp : Repr h1 -> Repr h2 -> Ordering

  Heterogeneous comparison of molecular formulae

Totality: total
Visibility: public export

heq : Repr h1 -> Repr h2 -> Bool

  Heterogeneous equality between molecular formulae

Totality: total
Visibility: public export

contains_ : Repr h1 -> Repr h2 -> Bool

  True if the first formula has at least as many atoms of each element
  as the second formula.

Totality: total
Visibility: public export

record Formula : Type

  A provably normalized molecular formula.
  
  This is just a wrapper around `Repr mx`, the representation of a
  molecular formula as a provably sorted list of pairs.

Totality: total
Visibility: public export
Constructor: 

F : Repr mx -> Formula

Projections:

0 .mx : Formula -> Maybe String

.pairs : ({rec:0} : Formula) -> Repr (mx {rec:0})

Hints:

Cast e Elem => Cast (Atom e c p r NoH t ch l) Formula

Cast e Elem => Cast (Atom e c p r HCount t ch l) Formula

Eq Formula

Interpolation Formula

Monoid Formula

Ord Formula

Semigroup Formula

Show Formula

0 .mx : Formula -> Maybe String

Totality: total
Visibility: public export

0 mx : Formula -> Maybe String

Totality: total
Visibility: public export

.pairs : ({rec:0} : Formula) -> Repr (mx {rec:0})

Totality: total
Visibility: public export

pairs : ({rec:0} : Formula) -> Repr (mx {rec:0})

Totality: total
Visibility: public export

singleton : Elem -> Nat -> Formula

  Creates a molecular formula with the given element and count.

Totality: total
Visibility: export

contains : Formula -> Formula -> Bool

  True, if the first `Formula` contains at least the atoms listed
  in the second formula, that is, all elements in the second formula
  apear at the same or a higher count in the first.

Totality: total
Visibility: export

insert : Elem -> Nat -> Formula -> Formula

  Inserts an element plus count into a molecular formula.

Totality: total
Visibility: export

insertElem : Elem -> Formula -> Formula

  Inserts an element at count 1 into a molecular formula.

Totality: total
Visibility: export