{-# 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 #-}

-- | Very very rough support for reading units of measure in the
-- syntax used by "Data.UnitsOfMeasure.Show".
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

-- | Represents a quantity whose units have a syntactic representation
-- that is known statically and at runtime.
data QuantityWithUnit a u where
  QuantityWithUnit :: Quantity a (Pack u) -> SUnit u -> QuantityWithUnit a u

-- | An existential wrapper type: @'Some' p@ is essentially @exists x . p x@.
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
_ = []

-- | Parse a quantity and check that it has the expected units.
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))

-- | Parse a quantity along with its units.
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"

-- | Parse a unit.
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