{- Data/Metrology.Factor.hs The units Package Copyright (c) 2013 Richard Eisenberg rae@cs.brynmawr.edu This file defines the Factor kind and operations over lists of Factors. Factors represents dimensions and units raised to a power of integers, and the lists of Factors represents monomials of dimensions and units. -} {-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances, CPP #-} -- allow compilation even without Cabal #ifndef MIN_VERSION_singletons #define MIN_VERSION_singletons(a,b,c) 1 #endif #if __GLASGOW_HASKELL__ >= 900 {-# OPTIONS_GHC -Wno-star-is-type #-} #endif module Data.Metrology.Factor where import GHC.Exts (Constraint) import Data.Metrology.Z as Z import Data.Type.Equality as DTE import Data.Type.Bool #if MIN_VERSION_singletons(3,0,0) import Prelude.Singletons #else import Data.Singletons.Prelude #endif -- | This will only be used at the kind level. It holds a dimension or unit -- with its exponent. data Factor star = F star Z ---------------------------------------------------------- --- Set-like operations ---------------------------------- ---------------------------------------------------------- {- These functions are templates for type-level functions. remove :: String -> [String] -> [String] remove _ [] = [] remove s (h:t) = if s == h then t else h : remove s t member :: String -> [String] -> Bool member _ [] = False member s (h:t) = s == h || member s t extract :: String -> [String] -> ([String], Maybe String) extract _ [] = ([], Nothing) extract s (h:t) = if s == h then (t, Just s) else let (resList, resVal) = extract s t in (h : resList, resVal) reorder :: [String] -> [String] -> [String] reorder x [] = x reorder x (h:t) = case extract h x of (lst, Nothing) -> reorder lst t (lst, Just elt) -> elt : (reorder lst t) -} infix 4 $= -- | Do these Factors represent the same dimension? type family (a :: Factor *) $= (b :: Factor *) :: Bool where (F n1 z1) $= (F n2 z2) = n1 DTE.== n2 a $= b = False -- | @(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) -- @ type family Extract (s :: Factor *) (lst :: [Factor *]) :: ([Factor *], Maybe (Factor *)) where Extract s '[] = '( '[], Nothing ) Extract s (h ': t) = If (s $= h) '(t, Just h) '(h ': Fst (Extract s t), Snd (Extract s t)) -- kind DimAnnotation = [Factor *] -- a list of Factors forms a full annotation of a quantity's dimension -- | 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 ==> [] -- @ type family Reorder (a :: [Factor *]) (b :: [Factor *]) :: [Factor *] where Reorder x x = x Reorder '[] x = '[] Reorder '[x] y = '[x] Reorder x '[] = x Reorder x (h ': t) = Reorder' (Extract h x) t -- | Helper function in 'Reorder' type family Reorder' (scrut :: ([Factor *], Maybe (Factor *))) (t :: [Factor *]) :: [Factor *] where Reorder' '(lst, Nothing) t = Reorder lst t Reorder' '(lst, Just elt) t = elt ': (Reorder lst t) infix 4 @~ -- | Check if two @[Factor *]@s should be considered to be equal type family (a :: [Factor *]) @~ (b :: [Factor *]) :: Constraint where a @~ b = (Normalize (a @- b) ~ '[]) ---------------------------------------------------------- --- Normalization ---------------------------------------- ---------------------------------------------------------- -- | Take a @[Factor *]@ and remove any @Factor@s with an exponent of 0 type family Normalize (d :: [Factor *]) :: [Factor *] where Normalize '[] = '[] Normalize ((F n Zero) ': t) = Normalize t Normalize (h ': t) = h ': Normalize t ---------------------------------------------------------- --- Arithmetic ------------------------------------------- ---------------------------------------------------------- infixl 6 @@+ -- | Adds corresponding exponents in two dimension, assuming the lists are -- ordered similarly. type family (a :: [Factor *]) @@+ (b :: [Factor *]) :: [Factor *] where '[] @@+ b = b a @@+ '[] = a ((F name z1) ': t1) @@+ ((F name z2) ': t2) = (F name (z1 #+ z2)) ': (t1 @@+ t2) (h ': t) @@+ b = h ': (t @@+ b) infixl 6 @+ -- | Adds corresponding exponents in two dimension, preserving order type family (a :: [Factor *]) @+ (b :: [Factor *]) :: [Factor *] where a @+ b = a @@+ (Reorder b a) infixl 6 @@- -- | Subtract exponents in two dimensions, assuming the lists are ordered -- similarly. type family (a :: [Factor *]) @@- (b :: [Factor *]) :: [Factor *] where '[] @@- 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) infixl 6 @- -- | Subtract exponents in two dimensions type family (a :: [Factor *]) @- (b :: [Factor *]) :: [Factor *] where a @- a = '[] a @- b = a @@- (Reorder b a) -- | negate a single @Factor@ type family NegDim (a :: Factor *) :: Factor * where NegDim (F n z) = F n (Z.Negate z) -- | negate a list of @Factor@s type family NegList (a :: [Factor *]) :: [Factor *] where NegList '[] = '[] NegList (h ': t) = (NegDim h ': (NegList t)) infixl 7 @* -- | Multiplication of the exponents in a dimension by a scalar type family (base :: [Factor *]) @* (power :: Z) :: [Factor *] where '[] @* power = '[] ((F name num) ': t) @* power = (F name (num #* power)) ': (t @* power) infixl 7 @/ -- | Division of the exponents in a dimension by a scalar type family (dims :: [Factor *]) @/ (z :: Z) :: [Factor *] where '[] @/ z = '[] ((F name num) ': t) @/ z = (F name (num #/ z)) ': (t @/ z)