{-
   Copyright 2016, Dominic Orchard, Andrew Rice, Mistral Contrastin, Matthew Danish

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
-}
{-# LANGUAGE DeriveDataTypeable, DeriveGeneric, PatternGuards #-}


{- Provides various data types and type class instances for the Units extension -}

module Camfort.Specification.Units.Environment
  (
    -- * Datatypes and Aliases
    Constraint(..)
  , Constraints
  , UnitInfo(..)
  , isMonomorphic, isUnitless
  , VV, PP
    -- * Helpers
  , conParamEq
  , unitParamEq
  , doubleToRationalSubset
  , pprintConstr
  , pprintUnitInfo
  , toUnitInfo
  , foldUnits
  , flattenUnits
  , simplifyUnits
  , colSort, SortFn
    -- * Modules (instances)
  , module Data.Data
  ) where

import qualified Camfort.Specification.Units.Parser.Types as P
import           Control.Arrow (first, second)
import           Data.Binary
import           Data.Char
import           Data.Data
import           Data.Generics.Uniplate.Operations (rewrite)
import           Data.List
import qualified Data.Map.Strict as M
import           Data.Ratio
import           GHC.Generics (Generic)
import qualified Language.Fortran.AST as F
import           Text.PrettyPrint (text)
import           Text.PrettyPrint.GenericPretty (Out, doc, docPrec)
import           Text.Printf

-- | A (unique name, source name) variable
type VV = (F.Name, F.Name)

-- | A (unique name, source name) program unit name
type PP = (F.Name, F.Name)

type UniqueId = Int

-- | Description of the unit of an expression.
data UnitInfo
  = UnitParamPosAbs (PP, Int)             -- an abstract parameter identified by PU name and argument position
  | UnitParamPosUse (PP, Int, Int)        -- identify particular instantiation of parameters
  | UnitParamVarAbs (PP, VV)              -- an abstract parameter identified by PU name and variable name
  | UnitParamVarUse (PP, VV, Int)         -- a particular instantiation of above
  | UnitParamLitAbs UniqueId              -- a literal with abstract, polymorphic units, uniquely identified
  | UnitParamLitUse (UniqueId, Int)       -- a particular instantiation of a polymorphic literal
  | UnitParamEAPAbs VV                    -- an abstract Explicitly Annotated Polymorphic unit variable
  | UnitParamEAPUse (VV, Int)             -- a particular instantiation of an Explicitly Annotated Polymorphic unit variable
  | UnitParamImpAbs String                -- implicitly inferred polymorphic units, uniquely identified
  | UnitLiteral Int                       -- literal with undetermined but uniquely identified units
  | UnitlessLit                           -- a unitless literal
  | UnitlessVar                           -- a unitless variable
  | UnitName String                       -- a basic unit
  | UnitAlias String                      -- the name of a unit alias
  | UnitVar VV                            -- variable with undetermined units: (unique name, source name)
  | UnitMul UnitInfo UnitInfo             -- two units multiplied
  | UnitPow UnitInfo Double               -- a unit raised to a constant power
  | UnitRecord [(String, UnitInfo)]       -- 'record'-type of units
  deriving (UnitInfo -> UnitInfo -> Bool
(UnitInfo -> UnitInfo -> Bool)
-> (UnitInfo -> UnitInfo -> Bool) -> Eq UnitInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UnitInfo -> UnitInfo -> Bool
$c/= :: UnitInfo -> UnitInfo -> Bool
== :: UnitInfo -> UnitInfo -> Bool
$c== :: UnitInfo -> UnitInfo -> Bool
Eq, Eq UnitInfo
Eq UnitInfo
-> (UnitInfo -> UnitInfo -> Ordering)
-> (UnitInfo -> UnitInfo -> Bool)
-> (UnitInfo -> UnitInfo -> Bool)
-> (UnitInfo -> UnitInfo -> Bool)
-> (UnitInfo -> UnitInfo -> Bool)
-> (UnitInfo -> UnitInfo -> UnitInfo)
-> (UnitInfo -> UnitInfo -> UnitInfo)
-> Ord UnitInfo
UnitInfo -> UnitInfo -> Bool
UnitInfo -> UnitInfo -> Ordering
UnitInfo -> UnitInfo -> UnitInfo
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: UnitInfo -> UnitInfo -> UnitInfo
$cmin :: UnitInfo -> UnitInfo -> UnitInfo
max :: UnitInfo -> UnitInfo -> UnitInfo
$cmax :: UnitInfo -> UnitInfo -> UnitInfo
>= :: UnitInfo -> UnitInfo -> Bool
$c>= :: UnitInfo -> UnitInfo -> Bool
> :: UnitInfo -> UnitInfo -> Bool
$c> :: UnitInfo -> UnitInfo -> Bool
<= :: UnitInfo -> UnitInfo -> Bool
$c<= :: UnitInfo -> UnitInfo -> Bool
< :: UnitInfo -> UnitInfo -> Bool
$c< :: UnitInfo -> UnitInfo -> Bool
compare :: UnitInfo -> UnitInfo -> Ordering
$ccompare :: UnitInfo -> UnitInfo -> Ordering
$cp1Ord :: Eq UnitInfo
Ord, Typeable UnitInfo
DataType
Constr
Typeable UnitInfo
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> UnitInfo -> c UnitInfo)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c UnitInfo)
-> (UnitInfo -> Constr)
-> (UnitInfo -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c UnitInfo))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnitInfo))
-> ((forall b. Data b => b -> b) -> UnitInfo -> UnitInfo)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> UnitInfo -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> UnitInfo -> r)
-> (forall u. (forall d. Data d => d -> u) -> UnitInfo -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> UnitInfo -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> UnitInfo -> m UnitInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> UnitInfo -> m UnitInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> UnitInfo -> m UnitInfo)
-> Data UnitInfo
UnitInfo -> DataType
UnitInfo -> Constr
(forall b. Data b => b -> b) -> UnitInfo -> UnitInfo
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnitInfo -> c UnitInfo
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnitInfo
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> UnitInfo -> u
forall u. (forall d. Data d => d -> u) -> UnitInfo -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnitInfo -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnitInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UnitInfo -> m UnitInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UnitInfo -> m UnitInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnitInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnitInfo -> c UnitInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnitInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnitInfo)
$cUnitRecord :: Constr
$cUnitPow :: Constr
$cUnitMul :: Constr
$cUnitVar :: Constr
$cUnitAlias :: Constr
$cUnitName :: Constr
$cUnitlessVar :: Constr
$cUnitlessLit :: Constr
$cUnitLiteral :: Constr
$cUnitParamImpAbs :: Constr
$cUnitParamEAPUse :: Constr
$cUnitParamEAPAbs :: Constr
$cUnitParamLitUse :: Constr
$cUnitParamLitAbs :: Constr
$cUnitParamVarUse :: Constr
$cUnitParamVarAbs :: Constr
$cUnitParamPosUse :: Constr
$cUnitParamPosAbs :: Constr
$tUnitInfo :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> UnitInfo -> m UnitInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UnitInfo -> m UnitInfo
gmapMp :: (forall d. Data d => d -> m d) -> UnitInfo -> m UnitInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UnitInfo -> m UnitInfo
gmapM :: (forall d. Data d => d -> m d) -> UnitInfo -> m UnitInfo
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UnitInfo -> m UnitInfo
gmapQi :: Int -> (forall d. Data d => d -> u) -> UnitInfo -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UnitInfo -> u
gmapQ :: (forall d. Data d => d -> u) -> UnitInfo -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UnitInfo -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnitInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UnitInfo -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnitInfo -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UnitInfo -> r
gmapT :: (forall b. Data b => b -> b) -> UnitInfo -> UnitInfo
$cgmapT :: (forall b. Data b => b -> b) -> UnitInfo -> UnitInfo
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnitInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnitInfo)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c UnitInfo)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UnitInfo)
dataTypeOf :: UnitInfo -> DataType
$cdataTypeOf :: UnitInfo -> DataType
toConstr :: UnitInfo -> Constr
$ctoConstr :: UnitInfo -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnitInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UnitInfo
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnitInfo -> c UnitInfo
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UnitInfo -> c UnitInfo
$cp1Data :: Typeable UnitInfo
Data, Typeable, (forall x. UnitInfo -> Rep UnitInfo x)
-> (forall x. Rep UnitInfo x -> UnitInfo) -> Generic UnitInfo
forall x. Rep UnitInfo x -> UnitInfo
forall x. UnitInfo -> Rep UnitInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep UnitInfo x -> UnitInfo
$cfrom :: forall x. UnitInfo -> Rep UnitInfo x
Generic)

-- | True iff u is monomorphic (has no parametric polymorphic pieces)
isMonomorphic :: UnitInfo -> Bool
isMonomorphic :: UnitInfo -> Bool
isMonomorphic UnitInfo
unitinfo = case UnitInfo
unitinfo of
  UnitName String
_      -> Bool
True
  UnitAlias String
_     -> Bool
True
  UnitVar VV
_       -> Bool
True
  UnitLiteral Int
_   -> Bool
True
  UnitInfo
UnitlessVar     -> Bool
True
  UnitInfo
UnitlessLit     -> Bool
True
  UnitRecord [(String, UnitInfo)]
recs -> ((String, UnitInfo) -> Bool) -> [(String, UnitInfo)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (UnitInfo -> Bool
isMonomorphic (UnitInfo -> Bool)
-> ((String, UnitInfo) -> UnitInfo) -> (String, UnitInfo) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, UnitInfo) -> UnitInfo
forall a b. (a, b) -> b
snd) [(String, UnitInfo)]
recs
  UnitMul UnitInfo
u1 UnitInfo
u2   -> UnitInfo -> Bool
isMonomorphic UnitInfo
u1 Bool -> Bool -> Bool
&& UnitInfo -> Bool
isMonomorphic UnitInfo
u2
  UnitPow UnitInfo
u Double
_     -> UnitInfo -> Bool
isMonomorphic UnitInfo
u
  UnitInfo
_               -> Bool
False

-- | True iff argument matches one of the unitless constructors
isUnitless :: UnitInfo -> Bool
isUnitless :: UnitInfo -> Bool
isUnitless UnitInfo
UnitlessVar = Bool
True
isUnitless UnitInfo
UnitlessLit = Bool
True
isUnitless UnitInfo
_           = Bool
False

type SortFn = UnitInfo -> UnitInfo -> Ordering
colSort :: UnitInfo -> UnitInfo -> Ordering
colSort :: UnitInfo -> UnitInfo -> Ordering
colSort (UnitLiteral Int
i) (UnitLiteral Int
j)         = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
i Int
j
colSort (UnitLiteral Int
_) UnitInfo
_                       = Ordering
LT
colSort UnitInfo
_ (UnitLiteral Int
_)                       = Ordering
GT
colSort (UnitParamPosAbs (VV, Int)
x) (UnitParamPosAbs (VV, Int)
y) = (VV, Int) -> (VV, Int) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (VV, Int)
x (VV, Int)
y
colSort (UnitParamPosAbs (VV, Int)
_) UnitInfo
_                   = Ordering
GT
colSort UnitInfo
_ (UnitParamPosAbs (VV, Int)
_)                   = Ordering
LT
colSort UnitInfo
x UnitInfo
y                                     = UnitInfo -> UnitInfo -> Ordering
forall a. Ord a => a -> a -> Ordering
compare UnitInfo
x UnitInfo
y

simplifyUnits :: UnitInfo -> UnitInfo
simplifyUnits :: UnitInfo -> UnitInfo
simplifyUnits = (UnitInfo -> Maybe UnitInfo) -> UnitInfo -> UnitInfo
forall on. Uniplate on => (on -> Maybe on) -> on -> on
rewrite UnitInfo -> Maybe UnitInfo
rw
  where
    rw :: UnitInfo -> Maybe UnitInfo
rw (UnitMul (UnitMul UnitInfo
u1 UnitInfo
u2) UnitInfo
u3)                          = UnitInfo -> Maybe UnitInfo
forall a. a -> Maybe a
Just (UnitInfo -> Maybe UnitInfo) -> UnitInfo -> Maybe UnitInfo
forall a b. (a -> b) -> a -> b
$ UnitInfo -> UnitInfo -> UnitInfo
UnitMul UnitInfo
u1 (UnitInfo -> UnitInfo -> UnitInfo
UnitMul UnitInfo
u2 UnitInfo
u3)
    rw (UnitMul UnitInfo
u1 UnitInfo
u2) | UnitInfo
u1 UnitInfo -> UnitInfo -> Bool
forall a. Eq a => a -> a -> Bool
== UnitInfo
u2                            = UnitInfo -> Maybe UnitInfo
forall a. a -> Maybe a
Just (UnitInfo -> Maybe UnitInfo) -> UnitInfo -> Maybe UnitInfo
forall a b. (a -> b) -> a -> b
$ UnitInfo -> Double -> UnitInfo
UnitPow UnitInfo
u1 Double
2
    rw (UnitPow (UnitPow UnitInfo
u1 Double
p1) Double
p2)                          = UnitInfo -> Maybe UnitInfo
forall a. a -> Maybe a
Just (UnitInfo -> Maybe UnitInfo) -> UnitInfo -> Maybe UnitInfo
forall a b. (a -> b) -> a -> b
$ UnitInfo -> Double -> UnitInfo
UnitPow UnitInfo
u1 (Double
p1 Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
p2)
    rw (UnitMul (UnitPow UnitInfo
u1 Double
p1) (UnitPow UnitInfo
u2 Double
p2)) | UnitInfo
u1 UnitInfo -> UnitInfo -> Bool
forall a. Eq a => a -> a -> Bool
== UnitInfo
u2  = UnitInfo -> Maybe UnitInfo
forall a. a -> Maybe a
Just (UnitInfo -> Maybe UnitInfo) -> UnitInfo -> Maybe UnitInfo
forall a b. (a -> b) -> a -> b
$ UnitInfo -> Double -> UnitInfo
UnitPow UnitInfo
u1 (Double
p1 Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
p2)
    rw (UnitPow UnitInfo
UnitlessLit Double
_)                               = UnitInfo -> Maybe UnitInfo
forall a. a -> Maybe a
Just UnitInfo
UnitlessLit
    rw (UnitPow UnitInfo
UnitlessVar Double
_)                               = UnitInfo -> Maybe UnitInfo
forall a. a -> Maybe a
Just UnitInfo
UnitlessVar
    rw (UnitPow UnitInfo
_ Double
p) | Double
p Double -> Double -> Bool
`approxEq` Double
0                        = UnitInfo -> Maybe UnitInfo
forall a. a -> Maybe a
Just UnitInfo
UnitlessLit
    rw (UnitMul UnitInfo
UnitlessLit UnitInfo
u)                               = UnitInfo -> Maybe UnitInfo
forall a. a -> Maybe a
Just UnitInfo
u
    rw (UnitMul UnitInfo
u UnitInfo
UnitlessLit)                               = UnitInfo -> Maybe UnitInfo
forall a. a -> Maybe a
Just UnitInfo
u
    rw (UnitMul UnitInfo
UnitlessVar UnitInfo
u)                               = UnitInfo -> Maybe UnitInfo
forall a. a -> Maybe a
Just UnitInfo
u
    rw (UnitMul UnitInfo
u UnitInfo
UnitlessVar)                               = UnitInfo -> Maybe UnitInfo
forall a. a -> Maybe a
Just UnitInfo
u
    rw UnitInfo
_                                                     = Maybe UnitInfo
forall a. Maybe a
Nothing

flattenUnits :: UnitInfo -> [UnitInfo]
flattenUnits :: UnitInfo -> [UnitInfo]
flattenUnits = ((UnitInfo, Double) -> UnitInfo)
-> [(UnitInfo, Double)] -> [UnitInfo]
forall a b. (a -> b) -> [a] -> [b]
map ((UnitInfo -> Double -> UnitInfo) -> (UnitInfo, Double) -> UnitInfo
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry UnitInfo -> Double -> UnitInfo
UnitPow) ([(UnitInfo, Double)] -> [UnitInfo])
-> (UnitInfo -> [(UnitInfo, Double)]) -> UnitInfo -> [UnitInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map UnitInfo Double -> [(UnitInfo, Double)]
forall k a. Map k a -> [(k, a)]
M.toList
             (Map UnitInfo Double -> [(UnitInfo, Double)])
-> (UnitInfo -> Map UnitInfo Double)
-> UnitInfo
-> [(UnitInfo, Double)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UnitInfo -> Double -> Bool)
-> Map UnitInfo Double -> Map UnitInfo Double
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey (\ UnitInfo
u Double
_ -> UnitInfo
u UnitInfo -> UnitInfo -> Bool
forall a. Eq a => a -> a -> Bool
/= UnitInfo
UnitlessLit Bool -> Bool -> Bool
&& UnitInfo
u UnitInfo -> UnitInfo -> Bool
forall a. Eq a => a -> a -> Bool
/= UnitInfo
UnitlessVar)
             (Map UnitInfo Double -> Map UnitInfo Double)
-> (UnitInfo -> Map UnitInfo Double)
-> UnitInfo
-> Map UnitInfo Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Double -> Bool) -> Map UnitInfo Double -> Map UnitInfo Double
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Bool -> Bool
not (Bool -> Bool) -> (Double -> Bool) -> Double -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Double -> Bool
approxEq Double
0)
             (Map UnitInfo Double -> Map UnitInfo Double)
-> (UnitInfo -> Map UnitInfo Double)
-> UnitInfo
-> Map UnitInfo Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Double -> Double -> Double)
-> [(UnitInfo, Double)] -> Map UnitInfo Double
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith Double -> Double -> Double
forall a. Num a => a -> a -> a
(+)
             ([(UnitInfo, Double)] -> Map UnitInfo Double)
-> (UnitInfo -> [(UnitInfo, Double)])
-> UnitInfo
-> Map UnitInfo Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((UnitInfo, Double) -> (UnitInfo, Double))
-> [(UnitInfo, Double)] -> [(UnitInfo, Double)]
forall a b. (a -> b) -> [a] -> [b]
map ((UnitInfo -> UnitInfo) -> (UnitInfo, Double) -> (UnitInfo, Double)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first UnitInfo -> UnitInfo
simplifyUnits)
             ([(UnitInfo, Double)] -> [(UnitInfo, Double)])
-> (UnitInfo -> [(UnitInfo, Double)])
-> UnitInfo
-> [(UnitInfo, Double)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnitInfo -> [(UnitInfo, Double)]
flatten
  where
    flatten :: UnitInfo -> [(UnitInfo, Double)]
flatten (UnitMul UnitInfo
u1 UnitInfo
u2) = UnitInfo -> [(UnitInfo, Double)]
flatten UnitInfo
u1 [(UnitInfo, Double)]
-> [(UnitInfo, Double)] -> [(UnitInfo, Double)]
forall a. [a] -> [a] -> [a]
++ UnitInfo -> [(UnitInfo, Double)]
flatten UnitInfo
u2
    flatten (UnitPow UnitInfo
u Double
p)   = ((UnitInfo, Double) -> (UnitInfo, Double))
-> [(UnitInfo, Double)] -> [(UnitInfo, Double)]
forall a b. (a -> b) -> [a] -> [b]
map ((Double -> Double) -> (UnitInfo, Double) -> (UnitInfo, Double)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Double
pDouble -> Double -> Double
forall a. Num a => a -> a -> a
*)) ([(UnitInfo, Double)] -> [(UnitInfo, Double)])
-> [(UnitInfo, Double)] -> [(UnitInfo, Double)]
forall a b. (a -> b) -> a -> b
$ UnitInfo -> [(UnitInfo, Double)]
flatten UnitInfo
u
    flatten UnitInfo
u               = [(UnitInfo
u, Double
1)]

foldUnits :: Foldable t => t UnitInfo -> UnitInfo
foldUnits :: t UnitInfo -> UnitInfo
foldUnits t UnitInfo
units
  | t UnitInfo -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t UnitInfo
units = UnitInfo
UnitlessVar
  | Bool
otherwise  = (UnitInfo -> UnitInfo -> UnitInfo) -> t UnitInfo -> UnitInfo
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 UnitInfo -> UnitInfo -> UnitInfo
UnitMul t UnitInfo
units

-- FIXME: we know better...
approxEq :: Double -> Double -> Bool
approxEq :: Double -> Double -> Bool
approxEq Double
a Double
b = Double -> Double
forall a. Num a => a -> a
abs (Double
b Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
a) Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
epsilon
epsilon :: Double
epsilon :: Double
epsilon = Double
0.001 -- arbitrary


instance Binary UnitInfo

instance Show UnitInfo where
  show :: UnitInfo -> String
show UnitInfo
unitinfo = case UnitInfo
unitinfo of
    UnitParamPosAbs ((String
f, String
_), Int
i)         -> String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"#<ParamPosAbs %s[%d]>" String
f Int
i
    UnitParamPosUse ((String
f, String
_), Int
i, Int
j)      -> String -> String -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
"#<ParamPosUse %s[%d] callId=%d>" String
f Int
i Int
j
    UnitParamVarAbs ((String
f, String
_), (String
v, String
_))    -> String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
"#<ParamVarAbs %s.%s>" String
f String
v
    UnitParamVarUse ((String
f, String
_), (String
v, String
_), Int
j) -> String -> String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"#<ParamVarUse %s.%s callId=%d>" String
f String
v Int
j
    UnitParamLitAbs Int
i                   -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"#<ParamLitAbs litId=%d>" Int
i
    UnitParamLitUse (Int
i, Int
j)              -> String -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
"#<ParamLitUse litId=%d callId=%d]>" Int
i Int
j
    UnitParamEAPAbs (String
v, String
_)              -> String
v
    UnitParamEAPUse ((String
v, String
_), Int
i)         -> String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"#<ParamEAPUse %s callId=%d]>" String
v Int
i
    UnitParamImpAbs String
iden                -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
"#<ParamImpAbs %s>" String
iden
    UnitLiteral Int
i                       -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"#<Literal id=%d>" Int
i
    UnitInfo
UnitlessLit                         -> String
"1"
    UnitInfo
UnitlessVar                         -> String
"1"
    UnitName String
name                       -> String
name
    UnitAlias String
name                      -> String
name -- FIXME: forbid polymorphism in aliases
    UnitVar (String
vName, String
_)                  -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
"#<Var %s>" String
vName
    UnitRecord [(String, UnitInfo)]
recs                     -> String
"record (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (((String, UnitInfo) -> String) -> [(String, UnitInfo)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (String
n, UnitInfo
u) -> String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitInfo -> String
forall a. Show a => a -> String
show UnitInfo
u) [(String, UnitInfo)]
recs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
    UnitMul UnitInfo
u1 (UnitPow UnitInfo
u2 Double
k)
      | Double
k Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
0                           -> UnitInfo -> String
forall a. Show a => a -> String
maybeParen UnitInfo
u1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" / " String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitInfo -> String
forall a. Show a => a -> String
maybeParen (UnitInfo -> Double -> UnitInfo
UnitPow UnitInfo
u2 (-Double
k))
    UnitMul UnitInfo
u1 UnitInfo
u2                       -> UnitInfo -> String
forall a. Show a => a -> String
maybeParenS UnitInfo
u1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitInfo -> String
forall a. Show a => a -> String
maybeParenS UnitInfo
u2
    UnitPow UnitInfo
u Double
1                         -> UnitInfo -> String
forall a. Show a => a -> String
show UnitInfo
u
    UnitPow UnitInfo
_ Double
0                         -> String
"1"
    UnitPow UnitInfo
u Double
k                         -> -- printf "%s**%f" (maybeParen u) k
      case Double -> Maybe Rational
doubleToRationalSubset Double
k of
          Just Rational
r
            | String
e <- Rational -> String
forall t. (Integral t, Show t, PrintfArg t) => Ratio t -> String
showRational Rational
r
            , String
e String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"1"  -> String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
"%s**%s" (UnitInfo -> String
forall a. Show a => a -> String
maybeParen UnitInfo
u) String
e
            | Bool
otherwise -> UnitInfo -> String
forall a. Show a => a -> String
show UnitInfo
u
          Maybe Rational
Nothing -> ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
                      String -> String -> Double -> String
forall r. PrintfType r => String -> r
printf String
"Irrational unit exponent: %s**%f" (UnitInfo -> String
forall a. Show a => a -> String
maybeParen UnitInfo
u) Double
k
       where showRational :: Ratio t -> String
showRational Ratio t
r
               | Ratio t
r Ratio t -> Ratio t -> Bool
forall a. Ord a => a -> a -> Bool
< Ratio t
0     = String -> ShowS
forall r. PrintfType r => String -> r
printf String
"(%s)" (Ratio t -> String
forall t. (Eq t, Num t, Show t, PrintfArg t) => Ratio t -> String
showRational' Ratio t
r)
               | Bool
otherwise = Ratio t -> String
forall t. (Eq t, Num t, Show t, PrintfArg t) => Ratio t -> String
showRational' Ratio t
r
             showRational' :: Ratio t -> String
showRational' Ratio t
r
               | Ratio t -> t
forall a. Ratio a -> a
denominator Ratio t
r t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
1 = t -> String
forall a. Show a => a -> String
show (Ratio t -> t
forall a. Ratio a -> a
numerator Ratio t
r)
               | Bool
otherwise = String -> t -> t -> String
forall r. PrintfType r => String -> r
printf String
"(%d / %d)" (Ratio t -> t
forall a. Ratio a -> a
numerator Ratio t
r) (Ratio t -> t
forall a. Ratio a -> a
denominator Ratio t
r)
    where
      maybeParen :: a -> String
maybeParen a
x | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isAlphaNum String
s = String
s
                   | Bool
otherwise        = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
        where s :: String
s = a -> String
forall a. Show a => a -> String
show a
x
      maybeParenS :: a -> String
maybeParenS a
x | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isUnitMulOk String
s = String
s
                    | Bool
otherwise         = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
        where s :: String
s = a -> String
forall a. Show a => a -> String
show a
x
      isUnitMulOk :: Char -> Bool
isUnitMulOk Char
c = Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
|| Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char
c Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
"*."

instance Out UnitInfo where
  doc :: UnitInfo -> Doc
doc = String -> Doc
text (String -> Doc) -> (UnitInfo -> String) -> UnitInfo -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnitInfo -> String
forall a. Show a => a -> String
show
  docPrec :: Int -> UnitInfo -> Doc
docPrec Int
_ = String -> Doc
text (String -> Doc) -> (UnitInfo -> String) -> UnitInfo -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnitInfo -> String
forall a. Show a => a -> String
show

-- Converts doubles to a rational that can be expressed
-- as a rational with denominator at most 10
-- otherwise Noting
doubleToRationalSubset :: Double -> Maybe Rational
doubleToRationalSubset :: Double -> Maybe Rational
doubleToRationalSubset Double
x | Double
x Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
0 =
    Rational -> Rational
forall a. Num a => a -> a
negate (Rational -> Rational) -> Maybe Rational -> Maybe Rational
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Double -> Maybe Rational
doubleToRationalSubset (Double -> Double
forall a. Num a => a -> a
abs Double
x)
doubleToRationalSubset Double
x =
    Integer -> Integer -> Integer -> Integer -> Maybe Rational
doubleToRational' Integer
0 Integer
1 (Double -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
ceiling Double
x) Integer
1
  where
    -- The maximum common denominator, controls granularity
    n :: Integer
n = Integer
16
    doubleToRational' :: Integer -> Integer -> Integer -> Integer -> Maybe Rational
doubleToRational' Integer
a Integer
b Integer
c Integer
d
         | Integer
b Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n Bool -> Bool -> Bool
&& Integer
d Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n =
           let mediant :: Double
mediant = (Integer -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
aInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
c))Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/(Integer -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
bInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
d))
           in if Double
x Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
mediant
              then if Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
d Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n
                   then Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$ (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
c) Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% (Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
d)
                   else Maybe Rational
forall a. Maybe a
Nothing
              else if Double
x Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double
mediant
                   then Integer -> Integer -> Integer -> Integer -> Maybe Rational
doubleToRational' (Integer
aInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
c) (Integer
bInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
d) Integer
c Integer
d
                   else Integer -> Integer -> Integer -> Integer -> Maybe Rational
doubleToRational' Integer
a Integer
b (Integer
aInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
c) (Integer
bInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
d)
         | Integer
b Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n     = Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$ Integer
c Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
d
         | Bool
otherwise = Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
b

-- | A relation between UnitInfos
data Constraint
  = ConEq   UnitInfo UnitInfo        -- an equality constraint
  | ConConj [Constraint]             -- conjunction of constraints
  deriving (Constraint -> Constraint -> Bool
(Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool) -> Eq Constraint
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Constraint -> Constraint -> Bool
$c/= :: Constraint -> Constraint -> Bool
== :: Constraint -> Constraint -> Bool
$c== :: Constraint -> Constraint -> Bool
Eq, Eq Constraint
Eq Constraint
-> (Constraint -> Constraint -> Ordering)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Constraint)
-> (Constraint -> Constraint -> Constraint)
-> Ord Constraint
Constraint -> Constraint -> Bool
Constraint -> Constraint -> Ordering
Constraint -> Constraint -> Constraint
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Constraint -> Constraint -> Constraint
$cmin :: Constraint -> Constraint -> Constraint
max :: Constraint -> Constraint -> Constraint
$cmax :: Constraint -> Constraint -> Constraint
>= :: Constraint -> Constraint -> Bool
$c>= :: Constraint -> Constraint -> Bool
> :: Constraint -> Constraint -> Bool
$c> :: Constraint -> Constraint -> Bool
<= :: Constraint -> Constraint -> Bool
$c<= :: Constraint -> Constraint -> Bool
< :: Constraint -> Constraint -> Bool
$c< :: Constraint -> Constraint -> Bool
compare :: Constraint -> Constraint -> Ordering
$ccompare :: Constraint -> Constraint -> Ordering
$cp1Ord :: Eq Constraint
Ord, Typeable Constraint
DataType
Constr
Typeable Constraint
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Constraint -> c Constraint)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Constraint)
-> (Constraint -> Constr)
-> (Constraint -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Constraint))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c Constraint))
-> ((forall b. Data b => b -> b) -> Constraint -> Constraint)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Constraint -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Constraint -> r)
-> (forall u. (forall d. Data d => d -> u) -> Constraint -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Constraint -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Constraint -> m Constraint)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Constraint -> m Constraint)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Constraint -> m Constraint)
-> Data Constraint
Constraint -> DataType
Constraint -> Constr
(forall b. Data b => b -> b) -> Constraint -> Constraint
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constraint -> c Constraint
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constraint
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Constraint -> u
forall u. (forall d. Data d => d -> u) -> Constraint -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constraint
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constraint -> c Constraint
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Constraint)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint)
$cConConj :: Constr
$cConEq :: Constr
$tConstraint :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Constraint -> m Constraint
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
gmapMp :: (forall d. Data d => d -> m d) -> Constraint -> m Constraint
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
gmapM :: (forall d. Data d => d -> m d) -> Constraint -> m Constraint
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
gmapQi :: Int -> (forall d. Data d => d -> u) -> Constraint -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Constraint -> u
gmapQ :: (forall d. Data d => d -> u) -> Constraint -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Constraint -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
gmapT :: (forall b. Data b => b -> b) -> Constraint -> Constraint
$cgmapT :: (forall b. Data b => b -> b) -> Constraint -> Constraint
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Constraint)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Constraint)
dataTypeOf :: Constraint -> DataType
$cdataTypeOf :: Constraint -> DataType
toConstr :: Constraint -> Constr
$ctoConstr :: Constraint -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constraint
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constraint
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constraint -> c Constraint
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constraint -> c Constraint
$cp1Data :: Typeable Constraint
Data, Typeable, (forall x. Constraint -> Rep Constraint x)
-> (forall x. Rep Constraint x -> Constraint) -> Generic Constraint
forall x. Rep Constraint x -> Constraint
forall x. Constraint -> Rep Constraint x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Constraint x -> Constraint
$cfrom :: forall x. Constraint -> Rep Constraint x
Generic)

instance Binary Constraint

type Constraints = [Constraint]

instance Show Constraint where
  show :: Constraint -> String
show (ConEq UnitInfo
u1 UnitInfo
u2) = UnitInfo -> String
forall a. Show a => a -> String
show UnitInfo
u1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" === " String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitInfo -> String
forall a. Show a => a -> String
show UnitInfo
u2
  show (ConConj [Constraint]
cs) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" && " ((Constraint -> String) -> [Constraint] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> String
forall a. Show a => a -> String
show [Constraint]
cs)

isUnresolvedUnit :: UnitInfo -> Bool
isUnresolvedUnit :: UnitInfo -> Bool
isUnresolvedUnit (UnitVar VV
_)         = Bool
True
isUnresolvedUnit (UnitLiteral Int
_)     = Bool
True
isUnresolvedUnit (UnitParamVarUse (VV, VV, Int)
_) = Bool
True
isUnresolvedUnit (UnitParamVarAbs (VV, VV)
_) = Bool
True
isUnresolvedUnit (UnitParamPosUse (VV, Int, Int)
_) = Bool
True
isUnresolvedUnit (UnitParamPosAbs (VV, Int)
_) = Bool
True
isUnresolvedUnit (UnitParamLitUse (Int, Int)
_) = Bool
True
isUnresolvedUnit (UnitParamLitAbs Int
_) = Bool
True
isUnresolvedUnit (UnitParamEAPAbs VV
_) = Bool
True
isUnresolvedUnit (UnitParamImpAbs String
_) = Bool
True
isUnresolvedUnit (UnitParamEAPUse (VV, Int)
_) = Bool
True
isUnresolvedUnit (UnitPow UnitInfo
u Double
_)       = UnitInfo -> Bool
isUnresolvedUnit UnitInfo
u
isUnresolvedUnit (UnitMul UnitInfo
u1 UnitInfo
u2)     = UnitInfo -> Bool
isUnresolvedUnit UnitInfo
u1 Bool -> Bool -> Bool
|| UnitInfo -> Bool
isUnresolvedUnit UnitInfo
u2
isUnresolvedUnit UnitInfo
_                   = Bool
False

isResolvedUnit :: UnitInfo -> Bool
isResolvedUnit :: UnitInfo -> Bool
isResolvedUnit = Bool -> Bool
not (Bool -> Bool) -> (UnitInfo -> Bool) -> UnitInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnitInfo -> Bool
isUnresolvedUnit

isConcreteUnit :: UnitInfo -> Bool
isConcreteUnit :: UnitInfo -> Bool
isConcreteUnit (UnitPow UnitInfo
u Double
_) = UnitInfo -> Bool
isConcreteUnit UnitInfo
u
isConcreteUnit (UnitMul UnitInfo
u UnitInfo
v) = UnitInfo -> Bool
isConcreteUnit UnitInfo
u Bool -> Bool -> Bool
&& UnitInfo -> Bool
isConcreteUnit UnitInfo
v
isConcreteUnit (UnitAlias String
_) = Bool
True
isConcreteUnit UnitInfo
UnitlessLit = Bool
True
isConcreteUnit (UnitName String
_) = Bool
True
isConcreteUnit UnitInfo
_ = Bool
False

pprintConstr :: Constraint -> String
pprintConstr :: Constraint -> String
pprintConstr (ConEq UnitInfo
u1 UnitInfo
u2)
  | UnitInfo -> Bool
isResolvedUnit UnitInfo
u1 Bool -> Bool -> Bool
&& UnitInfo -> Bool
isConcreteUnit UnitInfo
u1 Bool -> Bool -> Bool
&&
    UnitInfo -> Bool
isResolvedUnit UnitInfo
u2 Bool -> Bool -> Bool
&& UnitInfo -> Bool
isConcreteUnit UnitInfo
u2 =
      String
"Units '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitInfo -> String
pprintUnitInfo UnitInfo
u1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"' and '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitInfo -> String
pprintUnitInfo UnitInfo
u2 String -> ShowS
forall a. [a] -> [a] -> [a]
++
      String
"' should be equal"
  | UnitInfo -> Bool
isResolvedUnit UnitInfo
u1 = String
"'" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitInfo -> String
pprintUnitInfo UnitInfo
u2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"' should have unit '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitInfo -> String
pprintUnitInfo UnitInfo
u1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"'"
  | UnitInfo -> Bool
isResolvedUnit UnitInfo
u2 = String
"'" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitInfo -> String
pprintUnitInfo UnitInfo
u1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"' should have unit '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitInfo -> String
pprintUnitInfo UnitInfo
u2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"'"
  | Bool
otherwise = String
"'" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitInfo -> String
pprintUnitInfo UnitInfo
u1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"' should have the same units as '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitInfo -> String
pprintUnitInfo UnitInfo
u2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"'"
pprintConstr (ConConj [Constraint]
cs)  = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n\t and " ((Constraint -> String) -> [Constraint] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Constraint -> String
pprintConstr [Constraint]
cs)

pprintUnitInfo :: UnitInfo -> String
pprintUnitInfo :: UnitInfo -> String
pprintUnitInfo (UnitVar (String
_, String
sName))                 = String -> ShowS
forall r. PrintfType r => String -> r
printf String
"%s" String
sName
pprintUnitInfo (UnitParamVarUse (VV
_, (String
_, String
sName), Int
_)) = String -> ShowS
forall r. PrintfType r => String -> r
printf String
"%s" String
sName
pprintUnitInfo (UnitParamPosUse ((String
_, String
fname), Int
0, Int
_)) = String -> ShowS
forall r. PrintfType r => String -> r
printf String
"result of %s" String
fname
pprintUnitInfo (UnitParamPosUse ((String
_, String
fname), Int
i, Int
_)) = String -> Int -> ShowS
forall r. PrintfType r => String -> r
printf String
"parameter %d to %s" Int
i String
fname
pprintUnitInfo (UnitParamEAPUse ((String
v, String
_), Int
_))        = String -> ShowS
forall r. PrintfType r => String -> r
printf String
"explicitly annotated polymorphic unit %s" String
v
pprintUnitInfo (UnitLiteral Int
_)                      = String
"literal number"
pprintUnitInfo (UnitMul UnitInfo
u1 UnitInfo
u2)                      = UnitInfo -> String
pprintUnitInfo UnitInfo
u1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" * " String -> ShowS
forall a. [a] -> [a] -> [a]
++ UnitInfo -> String
pprintUnitInfo UnitInfo
u2
pprintUnitInfo (UnitPow UnitInfo
u Double
k) | Double
k Double -> Double -> Bool
`approxEq` Double
0       = String
"1"
                             | Bool
otherwise            =
    case Double -> Maybe Rational
doubleToRationalSubset Double
k of
          Just Rational
r
            | String
e <- Rational -> String
forall t. (Integral t, Show t, PrintfArg t) => Ratio t -> String
showRational Rational
r
            , String
e String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"1"  -> String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
"%s**%s" (UnitInfo -> String
maybeParen UnitInfo
u) String
e
            | Bool
otherwise -> UnitInfo -> String
pprintUnitInfo UnitInfo
u
          Maybe Rational
Nothing -> ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
                      String -> String -> Double -> String
forall r. PrintfType r => String -> r
printf String
"Irrational unit exponent: %s**%f" (UnitInfo -> String
maybeParen UnitInfo
u) Double
k
  where
    showRational :: Ratio t -> String
showRational Ratio t
r
      | Ratio t
r Ratio t -> Ratio t -> Bool
forall a. Ord a => a -> a -> Bool
< Ratio t
0     = String -> ShowS
forall r. PrintfType r => String -> r
printf String
"(%s)" (Ratio t -> String
forall t. (Eq t, Num t, Show t, PrintfArg t) => Ratio t -> String
showRational' Ratio t
r)
      | Bool
otherwise = Ratio t -> String
forall t. (Eq t, Num t, Show t, PrintfArg t) => Ratio t -> String
showRational' Ratio t
r
    showRational' :: Ratio t -> String
showRational' Ratio t
r
      | Ratio t -> t
forall a. Ratio a -> a
denominator Ratio t
r t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
1 = t -> String
forall a. Show a => a -> String
show (Ratio t -> t
forall a. Ratio a -> a
numerator Ratio t
r)
      | Bool
otherwise = String -> t -> t -> String
forall r. PrintfType r => String -> r
printf String
"(%d / %d)" (Ratio t -> t
forall a. Ratio a -> a
numerator Ratio t
r) (Ratio t -> t
forall a. Ratio a -> a
denominator Ratio t
r)

    maybeParen :: UnitInfo -> String
maybeParen UnitInfo
x
      | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isAlphaNum String
s = String
s
      | Bool
otherwise        = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
      where s :: String
s = UnitInfo -> String
pprintUnitInfo UnitInfo
x
    -- maybeParenS x
    --   | all isUnitMulOk s = s
    --   | otherwise         = "(" ++ s ++ ")"
    --   where s = pprintUnitInfo x
    -- isUnitMulOk c = isSpace c || isAlphaNum c || c `elem` "*."

pprintUnitInfo UnitInfo
ui                                   = UnitInfo -> String
forall a. Show a => a -> String
show UnitInfo
ui

--------------------------------------------------

-- | Constraint 'parametric' equality: treat all uses of a parametric
-- abstractions as equivalent to the abstraction.
conParamEq :: Constraint -> Constraint -> Bool
conParamEq :: Constraint -> Constraint -> Bool
conParamEq (ConEq UnitInfo
lhs1 UnitInfo
rhs1) (ConEq UnitInfo
lhs2 UnitInfo
rhs2) = (UnitInfo -> UnitInfo -> Bool
unitParamEq UnitInfo
lhs1 UnitInfo
lhs2 Bool -> Bool -> Bool
|| UnitInfo -> UnitInfo -> Bool
unitParamEq UnitInfo
rhs1 UnitInfo
rhs2) Bool -> Bool -> Bool
||
                                                 (UnitInfo -> UnitInfo -> Bool
unitParamEq UnitInfo
rhs1 UnitInfo
lhs2 Bool -> Bool -> Bool
|| UnitInfo -> UnitInfo -> Bool
unitParamEq UnitInfo
lhs1 UnitInfo
rhs2)
conParamEq (ConConj [Constraint]
cs1) (ConConj [Constraint]
cs2) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Constraint -> Constraint -> Bool)
-> [Constraint] -> [Constraint] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Constraint -> Constraint -> Bool
conParamEq [Constraint]
cs1 [Constraint]
cs2
conParamEq Constraint
_ Constraint
_ = Bool
False

-- | Unit 'parametric' equality: treat all uses of a parametric
-- abstractions as equivalent to the abstraction.
unitParamEq :: UnitInfo -> UnitInfo -> Bool
unitParamEq :: UnitInfo -> UnitInfo -> Bool
unitParamEq (UnitParamLitAbs Int
i)           (UnitParamLitUse (Int
i', Int
_))     = Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i'
unitParamEq (UnitParamLitUse (Int
i', Int
_))     (UnitParamLitAbs Int
i)           = Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i'
unitParamEq (UnitParamVarAbs (VV
f, VV
i))      (UnitParamVarUse (VV
f', VV
i', Int
_)) = (VV
f, VV
i) (VV, VV) -> (VV, VV) -> Bool
forall a. Eq a => a -> a -> Bool
== (VV
f', VV
i')
unitParamEq (UnitParamVarUse (VV
f', VV
i', Int
_)) (UnitParamVarAbs (VV
f, VV
i))      = (VV
f, VV
i) (VV, VV) -> (VV, VV) -> Bool
forall a. Eq a => a -> a -> Bool
== (VV
f', VV
i')
unitParamEq (UnitParamPosAbs (VV
f, Int
i))      (UnitParamPosUse (VV
f', Int
i', Int
_)) = (VV
f, Int
i) (VV, Int) -> (VV, Int) -> Bool
forall a. Eq a => a -> a -> Bool
== (VV
f', Int
i')
unitParamEq (UnitParamPosUse (VV
f', Int
i', Int
_)) (UnitParamPosAbs (VV
f, Int
i))      = (VV
f, Int
i) (VV, Int) -> (VV, Int) -> Bool
forall a. Eq a => a -> a -> Bool
== (VV
f', Int
i')
unitParamEq (UnitParamImpAbs String
v)           (UnitParamImpAbs String
v')          = String
v String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
v'
unitParamEq (UnitParamEAPAbs VV
v)           (UnitParamEAPUse (VV
v', Int
_))     = VV
v VV -> VV -> Bool
forall a. Eq a => a -> a -> Bool
== VV
v'
unitParamEq (UnitParamEAPUse (VV
v', Int
_))     (UnitParamEAPAbs VV
v)           = VV
v VV -> VV -> Bool
forall a. Eq a => a -> a -> Bool
== VV
v'
unitParamEq (UnitMul UnitInfo
u1 UnitInfo
u2)               (UnitMul UnitInfo
u1' UnitInfo
u2')             = UnitInfo -> UnitInfo -> Bool
unitParamEq UnitInfo
u1 UnitInfo
u1' Bool -> Bool -> Bool
&& UnitInfo -> UnitInfo -> Bool
unitParamEq UnitInfo
u2 UnitInfo
u2' Bool -> Bool -> Bool
||
                                                                          UnitInfo -> UnitInfo -> Bool
unitParamEq UnitInfo
u1 UnitInfo
u2' Bool -> Bool -> Bool
&& UnitInfo -> UnitInfo -> Bool
unitParamEq UnitInfo
u2 UnitInfo
u1'
unitParamEq (UnitPow UnitInfo
u Double
p)                 (UnitPow UnitInfo
u' Double
p')               = UnitInfo -> UnitInfo -> Bool
unitParamEq UnitInfo
u UnitInfo
u' Bool -> Bool -> Bool
&& Double
p Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
p'
unitParamEq UnitInfo
u1 UnitInfo
u2 = UnitInfo
u1 UnitInfo -> UnitInfo -> Bool
forall a. Eq a => a -> a -> Bool
== UnitInfo
u2

-- | Convert parser units to UnitInfo
toUnitInfo   :: P.UnitOfMeasure -> UnitInfo
toUnitInfo :: UnitOfMeasure -> UnitInfo
toUnitInfo (P.UnitProduct UnitOfMeasure
u1 UnitOfMeasure
u2)       = UnitInfo -> UnitInfo -> UnitInfo
UnitMul (UnitOfMeasure -> UnitInfo
toUnitInfo UnitOfMeasure
u1) (UnitOfMeasure -> UnitInfo
toUnitInfo UnitOfMeasure
u2)
toUnitInfo (P.UnitQuotient UnitOfMeasure
u1 UnitOfMeasure
u2)      = UnitInfo -> UnitInfo -> UnitInfo
UnitMul (UnitOfMeasure -> UnitInfo
toUnitInfo UnitOfMeasure
u1) (UnitInfo -> Double -> UnitInfo
UnitPow (UnitOfMeasure -> UnitInfo
toUnitInfo UnitOfMeasure
u2) (-Double
1))
toUnitInfo (P.UnitExponentiation UnitOfMeasure
u1 UnitPower
p) = UnitInfo -> Double -> UnitInfo
UnitPow (UnitOfMeasure -> UnitInfo
toUnitInfo UnitOfMeasure
u1) (UnitPower -> Double
toDouble UnitPower
p)
  where
    toDouble :: P.UnitPower   -> Double
    toDouble :: UnitPower -> Double
toDouble (P.UnitPowerInteger Integer
i)    = Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
i
    toDouble (P.UnitPowerRational Integer
x Integer
y) = Rational -> Double
forall a. Fractional a => Rational -> a
fromRational (Integer
x Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
y)
toUnitInfo (P.UnitBasic String
str)           = String -> UnitInfo
UnitName String
str
toUnitInfo (UnitOfMeasure
P.Unitless)                = UnitInfo
UnitlessLit
toUnitInfo (P.UnitRecord [(String, UnitOfMeasure)]
us)           = [(String, UnitInfo)] -> UnitInfo
UnitRecord (((String, UnitOfMeasure) -> (String, UnitInfo))
-> [(String, UnitOfMeasure)] -> [(String, UnitInfo)]
forall a b. (a -> b) -> [a] -> [b]
map ((UnitOfMeasure -> UnitInfo)
-> (String, UnitOfMeasure) -> (String, UnitInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UnitOfMeasure -> UnitInfo
toUnitInfo) [(String, UnitOfMeasure)]
us)