1-- | Case trees. 2-- 3-- After coverage checking, pattern matching is translated 4-- to case trees, i.e., a tree of successive case splits 5-- on one variable at a time. 6 7module Agda.TypeChecking.CompiledClause where 8 9import Prelude hiding (null) 10 11import Control.DeepSeq 12 13import qualified Data.Map as Map 14import Data.Map (Map) 15import Data.Semigroup hiding (Arg(..)) 16 17 18 19 20import Data.Data (Data) 21 22import GHC.Generics (Generic) 23 24import Agda.Syntax.Common 25import Agda.Syntax.Internal 26import Agda.Syntax.Internal.Generic 27import Agda.Syntax.Literal 28import Agda.Syntax.Position 29 30import Agda.Utils.Null 31import Agda.Utils.Pretty 32 33import Agda.Utils.Impossible 34 35data WithArity c = WithArity { arity :: Int, content :: c } 36 deriving (Data, Functor, Foldable, Traversable, Show, Generic) 37 38-- | Branches in a case tree. 39 40data Case c = Branches 41 { projPatterns :: Bool 42 -- ^ We are constructing a record here (copatterns). 43 -- 'conBranches' lists projections. 44 , conBranches :: Map QName (WithArity c) 45 -- ^ Map from constructor (or projection) names to their arity 46 -- and the case subtree. (Projections have arity 0.) 47 , etaBranch :: Maybe (ConHead, WithArity c) 48 -- ^ Eta-expand with the given (eta record) constructor. If this is 49 -- present, there should not be any conBranches or litBranches. 50 , litBranches :: Map Literal c 51 -- ^ Map from literal to case subtree. 52 , catchAllBranch :: Maybe c 53 -- ^ (Possibly additional) catch-all clause. 54 , fallThrough :: Maybe Bool 55 -- ^ (if True) In case of non-canonical argument use catchAllBranch. 56 , lazyMatch :: Bool 57 -- ^ Lazy pattern match. Requires single (non-copattern) branch with no lit 58 -- branches and no catch-all. 59 } 60 deriving (Data, Functor, Foldable, Traversable, Show, Generic) 61 62-- | Case tree with bodies. 63 64data CompiledClauses' a 65 = Case (Arg Int) (Case (CompiledClauses' a)) 66 -- ^ @Case n bs@ stands for a match on the @n@-th argument 67 -- (counting from zero) with @bs@ as the case branches. 68 -- If the @n@-th argument is a projection, we have only 'conBranches' 69 -- with arity 0. 70 | Done [Arg ArgName] a 71 -- ^ @Done xs b@ stands for the body @b@ where the @xs@ contains hiding 72 -- and name suggestions for the free variables. This is needed to build 73 -- lambdas on the right hand side for partial applications which can 74 -- still reduce. 75 | Fail [Arg ArgName] 76 -- ^ Absurd case. Add the free variables here as well so we can build correct 77 -- number of lambdas for strict backends. (#4280) 78 deriving (Data, Functor, Traversable, Foldable, Show, Generic) 79 80type CompiledClauses = CompiledClauses' Term 81 82litCase :: Literal -> c -> Case c 83litCase l x = Branches False Map.empty Nothing (Map.singleton l x) Nothing (Just False) False 84 85conCase :: QName -> Bool -> WithArity c -> Case c 86conCase c b x = Branches False (Map.singleton c x) Nothing Map.empty Nothing (Just b) False 87 88etaCase :: ConHead -> WithArity c -> Case c 89etaCase c x = Branches False Map.empty (Just (c, x)) Map.empty Nothing (Just False) True 90 91projCase :: QName -> c -> Case c 92projCase c x = Branches True (Map.singleton c $ WithArity 0 x) Nothing Map.empty Nothing (Just False) False 93 94catchAll :: c -> Case c 95catchAll x = Branches False Map.empty Nothing Map.empty (Just x) (Just True) False 96 97-- | Check that the requirements on lazy matching (single inductive case) are 98-- met, and set lazy to False otherwise. 99checkLazyMatch :: Case c -> Case c 100checkLazyMatch b = b { lazyMatch = lazyMatch b && requirements } 101 where 102 requirements = and 103 [ null (catchAllBranch b) 104 , Map.size (conBranches b) <= 1 105 , null (litBranches b) 106 , not $ projPatterns b ] 107 108-- | Check whether a case tree has a catch-all clause. 109hasCatchAll :: CompiledClauses -> Bool 110hasCatchAll = getAny . loop 111 where 112 loop cc = case cc of 113 Fail{} -> mempty 114 Done{} -> mempty 115 Case _ br -> maybe (foldMap loop br) (const $ Any True) $ catchAllBranch br 116 117-- | Check whether a case tree has any projection patterns 118hasProjectionPatterns :: CompiledClauses -> Bool 119hasProjectionPatterns = getAny . loop 120 where 121 loop cc = case cc of 122 Fail{} -> mempty 123 Done{} -> mempty 124 Case _ br -> Any (projPatterns br) <> foldMap loop br 125 126instance Semigroup c => Semigroup (WithArity c) where 127 WithArity n1 c1 <> WithArity n2 c2 128 | n1 == n2 = WithArity n1 (c1 <> c2) 129 | otherwise = __IMPOSSIBLE__ -- arity must match! 130 131instance (Semigroup c, Monoid c) => Monoid (WithArity c) where 132 mempty = WithArity __IMPOSSIBLE__ mempty 133 mappend = (<>) 134 135instance Semigroup m => Semigroup (Case m) where 136 Branches cop cs eta ls m b lazy <> Branches cop' cs' eta' ls' m' b' lazy' = checkLazyMatch $ 137 Branches (cop || cop') -- for @projCase <> mempty@ 138 (Map.unionWith (<>) cs cs') 139 (unionEta eta eta') 140 (Map.unionWith (<>) ls ls') 141 (m <> m') 142 (combine b b') 143 (lazy && lazy') 144 where 145 combine Nothing b' = b 146 combine b Nothing = b 147 combine (Just b) (Just b') = Just $ b && b' 148 149 unionEta Nothing b = b 150 unionEta b Nothing = b 151 unionEta Just{} Just{} = __IMPOSSIBLE__ 152 153instance (Semigroup m, Monoid m) => Monoid (Case m) where 154 mempty = empty 155 mappend = (<>) 156 157instance Null (Case m) where 158 empty = Branches False Map.empty Nothing Map.empty Nothing Nothing True 159 null (Branches _cop cs eta ls mcatch _b _lazy) = null cs && null eta && null ls && null mcatch 160 161-- * Pretty instances. 162 163instance Pretty a => Pretty (WithArity a) where 164 pretty = pretty . content 165 166instance Pretty a => Pretty (Case a) where 167 prettyPrec p (Branches _cop cs eta ls m b lazy) = 168 mparens (p > 0) $ prLazy lazy <+> vcat (prettyMap_ cs ++ prEta eta ++ prettyMap_ ls ++ prC m) 169 where 170 prLazy True = "~" 171 prLazy False = empty 172 prC Nothing = [] 173 prC (Just x) = ["_ ->" <+> pretty x] 174 prEta Nothing = [] 175 prEta (Just (c, cc)) = [("eta" <+> pretty c <+> "->") <?> pretty cc] 176 177prettyMap_ :: (Pretty k, Pretty v) => Map k v -> [Doc] 178prettyMap_ = map prettyAssign . Map.toList 179 180instance Pretty CompiledClauses where 181 pretty (Done hs t) = ("done" <> pretty hs) <?> pretty t 182 pretty Fail{} = "fail" 183 pretty (Case n bs) | projPatterns bs = 184 sep [ "record" 185 , nest 2 $ pretty bs 186 ] 187 pretty (Case n bs) = 188 text ("case " ++ prettyShow n ++ " of") <?> pretty bs 189 190-- * KillRange instances. 191 192instance KillRange c => KillRange (WithArity c) where 193 killRange = fmap killRange 194 195instance KillRange c => KillRange (Case c) where 196 killRange (Branches cop con eta lit all b lazy) = Branches cop 197 (killRangeMap con) 198 (killRange eta) 199 (killRangeMap lit) 200 (killRange all) 201 b lazy 202 203instance KillRange CompiledClauses where 204 killRange (Case i br) = killRange2 Case i br 205 killRange (Done xs v) = killRange2 Done xs v 206 killRange (Fail xs) = killRange1 Fail xs 207 208-- * TermLike instances 209 210instance TermLike a => TermLike (WithArity a) where 211 traverseTermM = traverse . traverseTermM 212 foldTerm = foldMap . foldTerm 213 214instance TermLike a => TermLike (Case a) where 215 traverseTermM = traverse . traverseTermM 216 foldTerm = foldMap . foldTerm 217 218instance TermLike a => TermLike (CompiledClauses' a) where 219 traverseTermM = traverse . traverseTermM 220 foldTerm = foldMap . foldTerm 221 222-- NFData instances 223 224instance NFData c => NFData (WithArity c) 225instance NFData a => NFData (Case a) 226instance NFData a => NFData (CompiledClauses' a) 227