module Agda.TypeChecking.CompiledClause where
import Prelude hiding (null)
import qualified Data.Map as Map
import Data.Map (Map)
import Data.Semigroup (Semigroup, Monoid, (<>), mempty, mappend, Any(..))
import Data.Typeable (Typeable)
import Data.Foldable (Foldable, foldMap)
import Data.Traversable (Traversable)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Utils.Null
import Agda.Utils.Pretty hiding ((<>))
#include "undefined.h"
import Agda.Utils.Impossible
data WithArity c = WithArity { arity :: Int, content :: c }
deriving (Typeable, Functor, Foldable, Traversable)
data Case c = Branches
{ projPatterns :: Bool
, conBranches :: Map QName (WithArity c)
, litBranches :: Map Literal c
, catchAllBranch :: Maybe c
}
deriving (Typeable, Functor, Foldable, Traversable)
data CompiledClauses
= Case (Arg Int) (Case CompiledClauses)
| Done [Arg ArgName] Term
| Fail
deriving (Typeable)
litCase :: Literal -> c -> Case c
litCase l x = Branches False Map.empty (Map.singleton l x) Nothing
conCase :: QName -> WithArity c -> Case c
conCase c x = Branches False (Map.singleton c x) Map.empty Nothing
projCase :: QName -> c -> Case c
projCase c x = Branches True (Map.singleton c $ WithArity 0 x) Map.empty Nothing
catchAll :: c -> Case c
catchAll x = Branches False Map.empty Map.empty (Just x)
hasCatchAll :: CompiledClauses -> Bool
hasCatchAll = getAny . loop
where
loop cc = case cc of
Fail{} -> mempty
Done{} -> mempty
Case _ br -> maybe (foldMap loop br) (const $ Any True) $ catchAllBranch br
instance Monoid c => Semigroup (WithArity c) where
WithArity n1 c1 <> WithArity n2 c2
| n1 == n2 = WithArity n1 $ mappend c1 c2
| otherwise = __IMPOSSIBLE__
instance Monoid c => Monoid (WithArity c) where
mempty = WithArity __IMPOSSIBLE__ mempty
mappend = (<>)
instance Monoid m => Semigroup (Case m) where
Branches cop cs ls m <> Branches cop' cs' ls' m' =
Branches (cop || cop')
(Map.unionWith mappend cs cs')
(Map.unionWith mappend ls ls')
(mappend m m')
instance Monoid m => Monoid (Case m) where
mempty = empty
mappend = (<>)
instance Null (Case m) where
empty = Branches False Map.empty Map.empty Nothing
null (Branches _cop cs ls mcatch) = null cs && null ls && null mcatch
instance Pretty a => Show (Case a) where
show = show . pretty
instance Show CompiledClauses where
show = show . pretty
instance Pretty a => Pretty (WithArity a) where
pretty = pretty . content
instance Pretty a => Pretty (Case a) where
prettyPrec p (Branches _cop cs ls m) =
mparens (p > 0) $ vcat $
prettyMap cs ++ prettyMap ls ++ prC m
where
prC Nothing = []
prC (Just x) = [text "_ ->" <+> pretty x]
prettyMap :: (Show k, Pretty v) => Map k v -> [Doc]
prettyMap m = [ sep [ text (show x ++ " ->")
, nest 2 $ pretty v ]
| (x, v) <- Map.toList m ]
instance Pretty CompiledClauses where
pretty (Done hs t) = text ("done" ++ show hs) <+> pretty t
pretty Fail = text "fail"
pretty (Case n bs) | projPatterns bs =
sep [ text "record"
, nest 2 $ pretty bs
]
pretty (Case n bs) =
sep [ text ("case " ++ show n ++ " of")
, nest 2 $ pretty bs
]
instance KillRange c => KillRange (WithArity c) where
killRange = fmap killRange
instance KillRange c => KillRange (Case c) where
killRange (Branches cop con lit all) = Branches cop
(killRangeMap con)
(killRangeMap lit)
(killRange all)
instance KillRange CompiledClauses where
killRange (Case i br) = killRange2 Case i br
killRange (Done xs v) = killRange2 Done xs v
killRange Fail = Fail