Data.Metrology.Internal

This file gathers and exports user-visible type-level definitions, to make error messages less cluttered. Non-expert users should never have to use the definitions exported from this module.

LCSU lookup

type family Lookup dim lcsu :: *

Equations

Lookup dim (MkLCSU_ (`(dim, unit)` : rest)) = unit

Lookup dim (MkLCSU_ (`(other, u)` : rest)) = Lookup dim (MkLCSU_ rest)

Lookup dim DefaultLCSU = DefaultUnitOfDim dim

type family LookupList keys map :: [Factor *]

Equations

LookupList `[]` lcsu = `[]`

LookupList (F dim z : rest) lcsu = F (Lookup dim lcsu) z : LookupList rest lcsu

Validity checking

type family ConvertibleLCSUs dfactors l1 l2 :: Constraint

Are two LCSUs inter-convertible at the given dimension?

Equations

ConvertibleLCSUs dfactors l1 l2 = (LookupList dfactors l1 *~ LookupList dfactors l2, ValidDL dfactors l1, ValidDL dfactors l2, UnitFactor (LookupList dfactors l1), UnitFactor (LookupList dfactors l2))

type family ValidDLU dfactors lcsu unit

Check if a (dimension factors, LCSU, unit) triple are all valid to be used together.

Equations

ValidDLU dfactors lcsu unit = (dfactors ~ DimFactorsOf (DimOfUnit unit), UnitFactor (LookupList dfactors lcsu), Units (LookupList dfactors lcsu), Unit unit, UnitFactorsOf unit *~ LookupList dfactors lcsu)

type family ValidDL dfactors lcsu :: Constraint

Check if a (dimension factors, LCSU) pair are valid to be used together. This checks that each dimension maps to a unit of the correct dimension.

Equations

ValidDL dfactors lcsu = ValidDLU dfactors lcsu (UnitOfDimFactors dfactors lcsu)

type family units1 *~ units2 :: Constraint infix 4

Check if two [Factor *]s, representing units, should be considered to be equal

Equations

units1 *~ units2 = CanonicalUnitsOfFactors units1 `SetEqual` CanonicalUnitsOfFactors units2

type family CanonicalUnitsOfFactors fs :: [*]

Given a list of unit factors, extract out the canonical units they are based on.

Equations

CanonicalUnitsOfFactors `[]` = `[]`

CanonicalUnitsOfFactors (F u z : fs) = CanonicalUnit u : CanonicalUnitsOfFactors fs

Manipulating units

type family DimOfUnitIsConsistent unit :: Constraint

Check to make sure that a unit has the same dimension as its base unit, if any.

Equations

DimOfUnitIsConsistent unit = (Dimension (DimOfUnit unit), If (BaseUnit unit == Canonical) (() :: Constraint) (DimOfUnit unit ~ DimOfUnit (BaseUnit unit)))

type family IsCanonical unit

Is this unit a canonical unit?

Equations

IsCanonical unit = BaseUnit unit == Canonical

type CanonicalUnit unit = CanonicalUnit' (BaseUnit unit) unit

Get the canonical unit from a given unit. For example: CanonicalUnit Foot = Meter

type family CanonicalUnit' base_unit unit :: *

Helper function in CanonicalUnit

Equations

CanonicalUnit' Canonical unit = unit

CanonicalUnit' base unit = CanonicalUnit' (BaseUnit base) base

type family BaseHasConvRatio unit

Essentially, a constraint that checks if a conversion ratio can be calculated for a BaseUnit of a unit.

Equations

BaseHasConvRatio unit = HasConvRatio (IsCanonical unit) unit

class UnitFactor units

Classifies well-formed list of unit factors, and permits calculating a conversion ratio for the purposes of LCSU conversions.

Minimal complete definition

canonicalConvRatioSpec

Instances

UnitFactor ([] (Factor *))

(UnitFactor rest, Unit unit, SingI Z n) => UnitFactor ((:) (Factor *) (F * unit n) rest)

Maniuplating dimension specifications

data Factor star

This will only be used at the kind level. It holds a dimension or unit with its exponent.

Constructors

F star Z

Instances

UnitFactor ([] (Factor *))

Read n => Read (Qu ([] (Factor *)) l n)

Show n => Show (Qu ([] (Factor *)) l n)

(UnitFactor rest, Unit unit, SingI Z n) => UnitFactor ((:) (Factor *) (F * unit n) rest)

type family a $= b :: Bool infix 4

Do these Factors represent the same dimension?

Equations

(F n1 z1) $= (F n2 z2) = n1 == n2

a $= b = False

type family Extract s lst :: ([Factor *], Maybe (Factor *))

(Extract s lst) pulls the Factor that matches s out of lst, returning a diminished list and, possibly, the extracted Factor.

Extract A [A, B, C] ==> ([B, C], Just A
Extract F [A, B, C] ==> ([A, B, C], Nothing)

Equations

Extract s `[]` = `(`[]`, Nothing)`

Extract s (h : t) = If (s $= h) `(t, Just h)` `(h : Fst (Extract s t), Snd (Extract s t))`

type family Reorder a b :: [Factor *]

Reorders a to be the in the same order as b, putting entries not in b at the end

Reorder [A 1, B 2] [B 5, A 2] ==> [B 2, A 1]
Reorder [A 1, B 2, C 3] [C 2, A 8] ==> [C 3, A 1, B 2]
Reorder [A 1, B 2] [B 4, C 1, A 9] ==> [B 2, A 1]
Reorder x x ==> x
Reorder x [] ==> x
Reorder [] x ==> []

Equations

Reorder x x = x

Reorder `[]` x = `[]`

Reorder `[x]` y = `[x]`

Reorder x `[]` = x

Reorder x (h : t) = Reorder' (Extract h x) t

type family Reorder' scrut t :: [Factor *]

Helper function in Reorder

Equations

Reorder' `(lst, Nothing)` t = Reorder lst t

Reorder' `(lst, Just elt)` t = elt : Reorder lst t

type family a @~ b :: Constraint infix 4

Check if two [Factor *]s should be considered to be equal

Equations

a @~ b = Normalize (a @- b) ~ `[]`

type family Normalize d :: [Factor *]

Take a [Factor *] and remove any Factors with an exponent of 0

Equations

Normalize `[]` = `[]`

Normalize (F n Zero : t) = Normalize t

Normalize (h : t) = h : Normalize t

type family a @@+ b :: [Factor *] infixl 6

Adds corresponding exponents in two dimension, assuming the lists are ordered similarly.

Equations

`[]` @@+ b = b

a @@+ `[]` = a

(F name z1 : t1) @@+ (F name z2 : t2) = F name (z1 #+ z2) : (t1 @@+ t2)

(h : t) @@+ b = h : (t @@+ b)

type family a @+ b :: [Factor *] infixl 6

Adds corresponding exponents in two dimension, preserving order

Equations

a @+ b = a @@+ Reorder b a

type family a @@- b :: [Factor *] infixl 6

Subtract exponents in two dimensions, assuming the lists are ordered similarly.

Equations

`[]` @@- b = NegList b

a @@- `[]` = a

(F name z1 : t1) @@- (F name z2 : t2) = F name (z1 #- z2) : (t1 @@- t2)

(h : t) @@- b = h : (t @@- b)

type family a @- b :: [Factor *] infixl 6

Subtract exponents in two dimensions

Equations

a @- a = `[]`

a @- b = a @@- Reorder b a

type family NegDim a :: Factor *

negate a single Factor

Equations

NegDim (F n z) = F n (Negate z)

type family NegList a :: [Factor *]

negate a list of Factors

Equations

NegList `[]` = `[]`

NegList (h : t) = NegDim h : NegList t

type family base @* power :: [Factor *] infixl 7

Multiplication of the exponents in a dimension by a scalar

Equations

`[]` @* power = `[]`

(F name num : t) @* power = F name (num #* power) : (t @* power)

type family dims @/ z :: [Factor *] infixl 7

Division of the exponents in a dimension by a scalar

Equations

`[]` @/ z = `[]`

(F name num : t) @/ z = F name (num #/ z) : (t @/ z)

Set operations on lists

module Data.Metrology.Set

Dimensions