{-# OPTIONS_GHC -fno-warn-unused-binds #-}
{-# LANGUAGE DataKinds
, EmptyCase
, FlexibleInstances
, GADTs
, KindSignatures
, OverloadedStrings
, QuantifiedConstraints
, RankNTypes
, ScopedTypeVariables
, TemplateHaskell
, TypeFamilies
, TypeOperators
, TypeSynonymInstances
, TypeInType
, UndecidableInstances #-}
module Data.Expression.Sort ( Sort(..)
, Sing(..)
, withSort
, DynamicSort(..)
, DynamicallySorted(..)
, DynamicallySortedFix
, parseSort
, toDynamicallySorted
, toStaticSort
, toStaticallySorted ) where
import Data.Attoparsec.Text
import Data.Functor
import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.TH
import Data.Expression.Utils.Indexed.Functor
data Sort = BooleanSort
| IntegralSort
| ArraySort { index :: Sort, element :: Sort }
deriving Eq
genSingletons [''Sort]
singDecideInstance ''Sort
withSort :: forall a (s :: Sort). Sing s -> (SingI s => a) -> a
withSort SBooleanSort a = a
withSort SIntegralSort a = a
withSort (SArraySort i e) a = withSort i $ withSort e $ a
show' :: Sort -> String
show' BooleanSort = "bool"
show' IntegralSort = "int"
show' (ArraySort i e) = "(array " ++ show' i ++ " " ++ show' e ++ ")"
instance Show Sort where
show s@BooleanSort = show' s
show s@IntegralSort = show' s
show (ArraySort i e) = "array " ++ show' i ++ " " ++ show' e
ssortToSort :: forall s. SSort s -> Sort
ssortToSort SBooleanSort = BooleanSort
ssortToSort SIntegralSort = IntegralSort
ssortToSort (SArraySort i e) = ArraySort (ssortToSort i) (ssortToSort e)
instance Show (SSort s) where
show = show . ssortToSort
data DynamicSort where
DynamicSort :: forall (s :: Sort). Sing s -> DynamicSort
instance Eq DynamicSort where
DynamicSort a == DynamicSort b = case a %~ b of
Proved Refl -> True
Disproved _ -> False
data DynamicallySorted (d :: Sort -> *) where
DynamicallySorted :: forall (s :: Sort) d. Sing s -> d s -> DynamicallySorted d
type DynamicallySortedFix f = DynamicallySorted (IFix f)
instance (forall (s :: Sort). Eq (d s)) => Eq (DynamicallySorted d) where
DynamicallySorted sa a == DynamicallySorted sb b = case sa %~ sb of
Proved Refl -> a == b
Disproved _ -> False
instance (forall (s :: Sort). Show (d s)) => Show (DynamicallySorted d) where
show (DynamicallySorted _ a) = show a
toStaticSort :: forall (s :: Sort). SingI s => DynamicSort -> Maybe (Sing s)
toStaticSort dx = case dx of
DynamicSort x -> case x %~ (sing :: Sing s) of
Proved Refl -> Just x
Disproved _ -> Nothing
toDynamicallySorted :: forall d (s :: Sort). SingI s => d s -> DynamicallySorted d
toDynamicallySorted = DynamicallySorted (sing :: Sing s)
toStaticallySorted :: forall d (s :: Sort). SingI s => DynamicallySorted d -> Maybe (d s)
toStaticallySorted dx = case dx of
DynamicallySorted s x -> case s %~ (sing :: Sing s) of
Proved Refl -> Just x
Disproved _ -> Nothing
parseSort :: Parser DynamicSort
parseSort = choice [ bool, int, array ] <?> "Sort" where
bool = string "bool" $> DynamicSort SBooleanSort
int = string "int" $> DynamicSort SIntegralSort
array = array' <$> (string "array" *> space *> sort') <*> (space *> sort')
sort' = choice [ bool, int, char '(' *> array <* char ')' ]
array' :: DynamicSort -> DynamicSort -> DynamicSort
array' (DynamicSort i) (DynamicSort e) = DynamicSort (SArraySort i e)