{-# LANGUAGE FlexibleContexts
, FlexibleInstances
, GADTs
, InstanceSigs
, MultiParamTypeClasses
, OverloadedStrings
, RankNTypes
, ScopedTypeVariables
, TypeInType
, TypeOperators #-}
module Data.Expression.IfThenElse ( IfThenElseF(..)
, ite ) where
import Data.Coerce
import Data.Functor.Const
import Data.Singletons
import Data.Singletons.Decide
import Data.Expression.Parser
import Data.Expression.Sort
import Data.Expression.Utils.Indexed.Eq
import Data.Expression.Utils.Indexed.Foldable
import Data.Expression.Utils.Indexed.Functor
import Data.Expression.Utils.Indexed.Show
import Data.Expression.Utils.Indexed.Sum
import Data.Expression.Utils.Indexed.Traversable
data IfThenElseF a (s :: Sort) where
IfThenElse :: Sing s -> a 'BooleanSort -> a s -> a s -> IfThenElseF a s
instance IEq1 IfThenElseF where
IfThenElse sa ia ta ea `ieq1` IfThenElse sb ib tb eb = ia `ieq` ib && case sa %~ sb of
Proved Refl -> ta `ieq` tb && ea `ieq` eb
Disproved _ -> False
instance IFunctor IfThenElseF where
imap f (IfThenElse s i t e) = IfThenElse s (f i) (f t) (f e)
index (IfThenElse s _ _ _) = s
instance IFoldable IfThenElseF where
ifold :: forall m (s :: Sort). Monoid m => IfThenElseF (Const m) s -> Const m s
ifold (IfThenElse _ i t e) = coerce ((coerce i <> coerce t <> coerce e) :: m)
instance ITraversable IfThenElseF where
itraverse f (IfThenElse s i t e) = IfThenElse s <$> f i <*> f t <*> f e
instance IShow IfThenElseF where
ishow (IfThenElse _ i t e) = coerce $ "(ite " ++ coerce i ++ " " ++ coerce t ++ " " ++ coerce e ++ ")"
instance IfThenElseF :<: f => Parseable IfThenElseF f where
parser _ r = do
_ <- char '(' *> string "ite" *> space
i <- r
_ <- space
t <- r
_ <- space
e <- r
_ <- char ')'
ifThenElse i t e <?> "IfThenElse" where
ifThenElse :: DynamicallySortedFix f -> DynamicallySortedFix f -> DynamicallySortedFix f -> Parser (DynamicallySortedFix f)
ifThenElse (DynamicallySorted s1 i)
(DynamicallySorted s2 t)
(DynamicallySorted s3 e) = case s1 %~ SBooleanSort of
Proved Refl -> case s2 %~ s3 of
Proved Refl -> return . DynamicallySorted s2 $ inject (IfThenElse s2 i t e)
Disproved _ -> fail "inconsistent sorts of then and else branches"
Disproved _ -> fail "branching on non-boolean expression"
ite :: forall f s. ( IfThenElseF :<: f, SingI s ) => IFix f 'BooleanSort -> IFix f s -> IFix f s -> IFix f s
ite i t e = inject (IfThenElse (sing :: Sing s) i t e)