module Agda.TypeChecking.CompiledClause where
import qualified Data.Map as Map
import Data.Map (Map)
import Data.Monoid
import Data.Typeable (Typeable)
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Agda.Utils.Pretty
#include "undefined.h"
import Agda.Utils.Impossible
data WithArity c = WithArity { arity :: Int, content :: c }
deriving (Typeable, Functor, Foldable, Traversable)
data Case c = Branches
{ conBranches :: Map QName (WithArity c)
, litBranches :: Map Literal c
, catchAllBranch :: Maybe c
}
deriving (Typeable, Functor, Foldable, Traversable)
data CompiledClauses
= Case Int (Case CompiledClauses)
| Done [Arg ArgName] Term
| Fail
deriving (Typeable)
emptyBranches :: Case CompiledClauses
emptyBranches = Branches Map.empty Map.empty Nothing
litCase :: Literal -> c -> Case c
litCase l x = Branches Map.empty (Map.singleton l x) Nothing
conCase :: QName -> WithArity c -> Case c
conCase c x = Branches (Map.singleton c x) Map.empty Nothing
catchAll :: c -> Case c
catchAll x = Branches Map.empty Map.empty (Just x)
instance Monoid c => Monoid (WithArity c) where
mempty = WithArity __IMPOSSIBLE__ mempty
mappend (WithArity n1 c1) (WithArity n2 c2)
| n1 == n2 = WithArity n1 $ mappend c1 c2
| otherwise = __IMPOSSIBLE__
instance Monoid m => Monoid (Case m) where
mempty = Branches Map.empty Map.empty Nothing
mappend (Branches cs ls m)
(Branches cs' ls' m') =
Branches (Map.unionWith mappend cs cs')
(Map.unionWith mappend ls ls')
(mappend m m')
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 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) <+> text (show t)
pretty Fail = text "fail"
pretty (Case n bs) =
sep [ text ("case " ++ show n ++ " of")
, nest 2 $ pretty bs
]