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