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.Foldable (Foldable, foldMap)
import Data.Traversable (Traversable, traverse)
import Data.Data (Data)
import Data.Typeable (Typeable)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic
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, Data, Functor, Foldable, Traversable, Show)
data Case c = Branches
{ projPatterns :: Bool
, conBranches :: Map QName (WithArity c)
, litBranches :: Map Literal c
, catchAllBranch :: Maybe c
}
deriving (Typeable, Data, Functor, Foldable, Traversable, Show)
data CompiledClauses' a
= Case (Arg Int) (Case (CompiledClauses' a))
| Done [Arg ArgName] a
| Fail
deriving (Typeable, Data, Functor, Traversable, Foldable, Show)
type CompiledClauses = CompiledClauses' Term
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 Semigroup c => Semigroup (WithArity c) where
WithArity n1 c1 <> WithArity n2 c2
| n1 == n2 = WithArity n1 (c1 <> c2)
| otherwise = __IMPOSSIBLE__
instance (Semigroup c, Monoid c) => Monoid (WithArity c) where
mempty = WithArity __IMPOSSIBLE__ mempty
mappend = (<>)
instance Semigroup m => Semigroup (Case m) where
Branches cop cs ls m <> Branches cop' cs' ls' m' =
Branches (cop || cop')
(Map.unionWith (<>) cs cs')
(Map.unionWith (<>) ls ls')
(m <> m')
instance (Semigroup m, 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 => 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 :: (Pretty k, Pretty v) => Map k v -> [Doc]
prettyMap m = [ sep [ pretty k <+> text "->"
, nest 2 $ pretty v ]
| (k, 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 " ++ prettyShow 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
instance TermLike a => TermLike (WithArity a) where
traverseTermM = traverse . traverseTermM
foldTerm = foldMap . foldTerm
instance TermLike a => TermLike (Case a) where
traverseTermM = traverse . traverseTermM
foldTerm = foldMap . foldTerm
instance TermLike a => TermLike (CompiledClauses' a) where
traverseTermM = traverse . traverseTermM
foldTerm = foldMap . foldTerm