{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.UnitsOfMeasure.Read
( readQuantity
, readUnit
, readWithUnit
, Some(..)
, QuantityWithUnit(..)
) where
import Control.Monad (join)
import GHC.TypeLits
import Data.List (genericReplicate)
import Data.Proxy
import Data.Type.Equality ((:~:)(..))
import Text.Parse.Units (parseUnit, universalSymbolTable, UnitExp(..))
import Data.UnitsOfMeasure.Internal
import Data.UnitsOfMeasure.Singleton
data QuantityWithUnit a u where
QuantityWithUnit :: Quantity a (Pack u) -> SUnit u -> QuantityWithUnit a u
data Some p where
Some :: p x -> Some p
instance (KnownUnit (Unpack u), u ~ Pack (Unpack u), Read a) => Read (Quantity a u) where
readsPrec :: Int -> ReadS (Quantity a u)
readsPrec Int
i (Char
' ':String
s) = Int -> ReadS (Quantity a u)
forall a. Read a => Int -> ReadS a
readsPrec Int
i String
s
readsPrec Int
_ (Char
'[':Char
'u':Char
'|':String
s)
| (String
t, Char
'|':Char
']':String
r) <- (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'|') String
s
, Right Quantity a (Pack (Unpack u))
v <- Proxy (Unpack u)
-> String -> Either String (Quantity a (Pack (Unpack u)))
forall (proxy :: UnitSyntax Symbol -> *) a
(u :: UnitSyntax Symbol).
(Read a, KnownUnit u) =>
proxy u -> String -> Either String (Quantity a (Pack u))
readWithUnit (Proxy (Unpack u)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Unpack u)) String
t = [(Quantity a u
Quantity a (Pack (Unpack u))
v, String
r)]
readsPrec Int
_ String
_ = []
readWithUnit :: forall proxy a u . (Read a, KnownUnit u)
=> proxy u -> String -> Either String (Quantity a (Pack u))
readWithUnit :: forall (proxy :: UnitSyntax Symbol -> *) a
(u :: UnitSyntax Symbol).
(Read a, KnownUnit u) =>
proxy u -> String -> Either String (Quantity a (Pack u))
readWithUnit proxy u
_ String
s = do
Some (QuantityWithUnit (Quantity a (Pack x)
q :: Quantity a _) SUnit x
v) <- String -> Either String (Some (QuantityWithUnit a))
forall a.
Read a =>
String -> Either String (Some (QuantityWithUnit a))
readQuantity String
s
case SUnit u -> SUnit x -> Maybe (Pack u :~: Pack x)
forall (u :: UnitSyntax Symbol) (v :: UnitSyntax Symbol).
SUnit u -> SUnit v -> Maybe (Pack u :~: Pack v)
testEquivalentSUnit (SUnit u
forall (u :: UnitSyntax Symbol). KnownUnit u => SUnit u
unitSing :: SUnit u) SUnit x
v of
Just Pack u :~: Pack x
Refl -> Quantity a (Pack u) -> Either String (Quantity a (Pack u))
forall a b. b -> Either a b
Right Quantity a (Pack u)
Quantity a (Pack x)
q
Maybe (Pack u :~: Pack x)
Nothing -> String -> Either String (Quantity a (Pack u))
forall a b. a -> Either a b
Left (String
"wrong units: got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ UnitSyntax String -> String
forall a. Show a => a -> String
show (SUnit x -> UnitSyntax String
forall (u :: UnitSyntax Symbol). SUnit u -> UnitSyntax String
forgetSUnit SUnit x
v))
readQuantity :: Read a => String -> Either String (Some (QuantityWithUnit a))
readQuantity :: forall a.
Read a =>
String -> Either String (Some (QuantityWithUnit a))
readQuantity String
s = case ReadS a
forall a. Read a => ReadS a
reads String
s of
[(a
n, String
s')] -> do Some SUnit x
u <- String -> Either String (Some SUnit)
readUnit String
s'
Some (QuantityWithUnit a)
-> Either String (Some (QuantityWithUnit a))
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some (QuantityWithUnit a)
-> Either String (Some (QuantityWithUnit a)))
-> Some (QuantityWithUnit a)
-> Either String (Some (QuantityWithUnit a))
forall a b. (a -> b) -> a -> b
$ QuantityWithUnit a x -> Some (QuantityWithUnit a)
forall {k} (p :: k -> *) (x :: k). p x -> Some p
Some (Quantity a (Pack x) -> SUnit x -> QuantityWithUnit a x
forall a (u :: UnitSyntax Symbol).
Quantity a (Pack u) -> SUnit u -> QuantityWithUnit a u
QuantityWithUnit (a -> Quantity a (Pack x)
forall a (u :: Unit). a -> Quantity a u
MkQuantity a
n) SUnit x
u)
[(a, String)]
_ -> String -> Either String (Some (QuantityWithUnit a))
forall a b. a -> Either a b
Left String
"reads: no parse"
readUnit :: String -> Either String (Some SUnit)
readUnit :: String -> Either String (Some SUnit)
readUnit String
s = UnitExp () String -> Some SUnit
expToSomeUnit (UnitExp () String -> Some SUnit)
-> Either String (UnitExp () String) -> Either String (Some SUnit)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolTable () String
-> String -> Either String (UnitExp () String)
forall pre u.
(Show pre, Show u) =>
SymbolTable pre u -> String -> Either String (UnitExp pre u)
parseUnit SymbolTable () String
forall a. SymbolTable a String
universalSymbolTable String
s
expToSomeUnit :: UnitExp () String -> Some SUnit
expToSomeUnit :: UnitExp () String -> Some SUnit
expToSomeUnit = UnitSyntax String -> Some SUnit
unitSyntaxToSomeUnit (UnitSyntax String -> Some SUnit)
-> (UnitExp () String -> UnitSyntax String)
-> UnitExp () String
-> Some SUnit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnitExp () String -> UnitSyntax String
expToUnitSyntax
unitSyntaxToSomeUnit :: UnitSyntax String -> Some SUnit
unitSyntaxToSomeUnit :: UnitSyntax String -> Some SUnit
unitSyntaxToSomeUnit ([String]
xs :/ [String]
ys) = case ([String] -> Some SList
someListVal [String]
xs, [String] -> Some SList
someListVal [String]
ys) of
(Some SList x
xs', Some SList x
ys') -> SUnit (x ':/ x) -> Some SUnit
forall {k} (p :: k -> *) (x :: k). p x -> Some p
Some (SList x -> SList x -> SUnit (x ':/ x)
forall (xs :: [Symbol]) (ys :: [Symbol]).
SList xs -> SList ys -> SUnit (xs ':/ ys)
SUnit SList x
xs' SList x
ys')
someListVal :: [String] -> Some SList
someListVal :: [String] -> Some SList
someListVal [] = SList '[] -> Some SList
forall {k} (p :: k -> *) (x :: k). p x -> Some p
Some SList '[]
SNil
someListVal (String
x:[String]
xs) = case (String -> SomeSymbol
someSymbolVal String
x, [String] -> Some SList
someListVal [String]
xs) of
(SomeSymbol Proxy n
x', Some SList x
xs') -> SList (n : x) -> Some SList
forall {k} (p :: k -> *) (x :: k). p x -> Some p
Some (Proxy n -> SList x -> SList (n : x)
forall (x :: Symbol) (proxy :: Symbol -> *) (xs1 :: [Symbol]).
KnownSymbol x =>
proxy x -> SList xs1 -> SList (x : xs1)
SCons Proxy n
x' SList x
xs')
expToUnitSyntax :: UnitExp () String -> UnitSyntax String
expToUnitSyntax :: UnitExp () String -> UnitSyntax String
expToUnitSyntax UnitExp () String
Unity = [] [String] -> [String] -> UnitSyntax String
forall s. [s] -> [s] -> UnitSyntax s
:/ []
expToUnitSyntax (Unit Maybe ()
_ String
s) = [String
s] [String] -> [String] -> UnitSyntax String
forall s. [s] -> [s] -> UnitSyntax s
:/ []
expToUnitSyntax (UnitExp () String
u `Mult` UnitExp () String
v) = ([String]
u_xs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
v_xs) [String] -> [String] -> UnitSyntax String
forall s. [s] -> [s] -> UnitSyntax s
:/ ([String]
u_ys [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
v_ys)
where
[String]
u_xs :/ [String]
u_ys = UnitExp () String -> UnitSyntax String
expToUnitSyntax UnitExp () String
u
[String]
v_xs :/ [String]
v_ys = UnitExp () String -> UnitSyntax String
expToUnitSyntax UnitExp () String
v
expToUnitSyntax (UnitExp () String
u `Div` UnitExp () String
v) = ([String]
u_xs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
v_ys) [String] -> [String] -> UnitSyntax String
forall s. [s] -> [s] -> UnitSyntax s
:/ ([String]
u_ys [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
v_xs)
where
[String]
u_xs :/ [String]
u_ys = UnitExp () String -> UnitSyntax String
expToUnitSyntax UnitExp () String
u
[String]
v_xs :/ [String]
v_ys = UnitExp () String -> UnitSyntax String
expToUnitSyntax UnitExp () String
v
expToUnitSyntax (UnitExp () String
u `Pow` Integer
n)
| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = [[String]] -> [String]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Integer -> [String] -> [[String]]
forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
n [String]
u_xs) [String] -> [String] -> UnitSyntax String
forall s. [s] -> [s] -> UnitSyntax s
:/ [[String]] -> [String]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Integer -> [String] -> [[String]]
forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
n [String]
u_ys)
| Bool
otherwise = [[String]] -> [String]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Integer -> [String] -> [[String]]
forall i a. Integral i => i -> a -> [a]
genericReplicate (Integer -> Integer
forall a. Num a => a -> a
negate Integer
n) [String]
u_ys) [String] -> [String] -> UnitSyntax String
forall s. [s] -> [s] -> UnitSyntax s
:/ [[String]] -> [String]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Integer -> [String] -> [[String]]
forall i a. Integral i => i -> a -> [a]
genericReplicate (Integer -> Integer
forall a. Num a => a -> a
negate Integer
n) [String]
u_xs)
where
[String]
u_xs :/ [String]
u_ys = UnitExp () String -> UnitSyntax String
expToUnitSyntax UnitExp () String
u