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.Common
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Agda.Utils.Pretty
import Agda.Utils.Impossible
#include "../undefined.h"
type key :-> value = Map key value
data WithArity c = WithArity { arity :: Int, content :: c }
deriving (Typeable, Functor, Foldable, Traversable)
data Case c = Branches
{ conBranches :: QName :-> WithArity c
, litBranches :: Literal :-> c
, catchAllBranch :: Maybe c
}
deriving (Typeable, Functor, Foldable, Traversable)
data CompiledClauses
= Case Int (Case CompiledClauses)
| Done [Arg String] Term
| Fail
deriving (Typeable)
emptyBranches = Branches Map.empty Map.empty Nothing
litCase l x = Branches Map.empty (Map.singleton l x) Nothing
conCase c x = Branches (Map.singleton c x) Map.empty Nothing
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 $
pr cs ++ pr ls ++ prC m
where
prC Nothing = []
prC (Just x) = [text "_ ->" <+> pretty x]
pr 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
]