1{-# LANGUAGE NondecreasingIndentation #-}
2
3{- | Various utility functions dealing with the non-linear, higher-order
4     patterns used for rewrite rules.
5-}
6
7module Agda.TypeChecking.Rewriting.NonLinPattern where
8
9import Control.Monad.Reader
10
11import Data.IntSet (IntSet)
12import qualified Data.IntSet as IntSet
13
14import Agda.Syntax.Common
15import Agda.Syntax.Internal
16import Agda.Syntax.Internal.Defs
17
18import Agda.TypeChecking.Datatypes
19import Agda.TypeChecking.Free
20import Agda.TypeChecking.Free.Lazy
21import Agda.TypeChecking.Irrelevance (workOnTypes, isPropM)
22import Agda.TypeChecking.Level
23import Agda.TypeChecking.Monad
24import Agda.TypeChecking.Pretty
25import Agda.TypeChecking.Records
26import Agda.TypeChecking.Reduce
27import Agda.TypeChecking.Substitute
28import Agda.TypeChecking.Telescope
29
30import Agda.Utils.Either
31import Agda.Utils.Functor
32import Agda.Utils.Impossible
33import Agda.Utils.List
34import Agda.Utils.Maybe
35import Agda.Utils.Monad
36import Agda.Utils.Null
37import Agda.Utils.Singleton
38import Agda.Utils.Size
39
40-- | Turn a term into a non-linear pattern, treating the
41--   free variables as pattern variables.
42--   The first argument indicates the relevance we are working under: if this
43--   is Irrelevant, then we construct a pattern that never fails to match.
44--   The second argument is the number of bound variables (from pattern lambdas).
45--   The third argument is the type of the term.
46
47class PatternFrom t a b where
48  patternFrom :: Relevance -> Int -> t -> a -> TCM b
49
50instance (PatternFrom t a b) => PatternFrom (Dom t) (Arg a) (Arg b) where
51  patternFrom r k t u = let r' = r `composeRelevance` getRelevance u
52                        in  traverse (patternFrom r' k $ unDom t) u
53
54instance PatternFrom (Type, Term) Elims [Elim' NLPat] where
55  patternFrom r k (t,hd) = \case
56    [] -> return []
57    (Apply u : es) -> do
58      ~(Pi a b) <- unEl <$> reduce t
59      p   <- patternFrom r k a u
60      t'  <- t `piApplyM` u
61      let hd' = hd `apply` [ u ]
62      ps  <- patternFrom r k (t',hd') es
63      return $ Apply p : ps
64    (IApply x y u : es) -> typeError $ GenericError $
65      "Rewrite rules with cubical are not yet supported"
66    (Proj o f : es) -> do
67      ~(Just (El _ (Pi a b))) <- getDefType f =<< reduce t
68      let t' = b `absApp` hd
69      hd' <- applyDef o f (argFromDom a $> hd)
70      ps  <- patternFrom r k (t',hd') es
71      return $ Proj o f : ps
72
73instance (PatternFrom t a b) => PatternFrom t (Dom a) (Dom b) where
74  patternFrom r k t = traverse $ patternFrom r k t
75
76instance PatternFrom () Type NLPType where
77  patternFrom r k _ a = workOnTypes $
78    NLPType <$> patternFrom r k () (getSort a)
79            <*> patternFrom r k (sort $ getSort a) (unEl a)
80
81instance PatternFrom () Sort NLPSort where
82  patternFrom r k _ s = do
83    s <- reduce s
84    case s of
85      Type l   -> PType <$> patternFrom r k () l
86      Prop l   -> PProp <$> patternFrom r k () l
87      Inf f n  -> return $ PInf f n
88      SSet l   -> __IMPOSSIBLE__
89      SizeUniv -> return PSizeUniv
90      LockUniv -> return PLockUniv
91      PiSort _ _ _ -> __IMPOSSIBLE__
92      FunSort _ _ -> __IMPOSSIBLE__
93      UnivSort _ -> __IMPOSSIBLE__
94      MetaS{}  -> __IMPOSSIBLE__
95      DefS{}   -> __IMPOSSIBLE__
96      DummyS s -> do
97        reportS "impossible" 10
98          [ "patternFrom: hit dummy sort with content:"
99          , s
100          ]
101        __IMPOSSIBLE__
102
103instance PatternFrom () Level NLPat where
104  patternFrom r k _ l = do
105    t <- levelType
106    v <- reallyUnLevelView l
107    patternFrom r k t v
108
109instance PatternFrom Type Term NLPat where
110  patternFrom r0 k t v = do
111    t <- reduce t
112    etaRecord <- isEtaRecordType t
113    prop <- fromRight __IMPOSSIBLE__ <.> runBlocked $ isPropM t
114    let r = if prop then Irrelevant else r0
115    v <- unLevel =<< reduce v
116    reportSDoc "rewriting.build" 60 $ sep
117      [ "building a pattern from term v = " <+> prettyTCM v
118      , " of type " <+> prettyTCM t
119      ]
120    let done = return $ PTerm v
121    case (unEl t , stripDontCare v) of
122      (Pi a b , _) -> do
123        let body = raise 1 v `apply` [ Arg (domInfo a) $ var 0 ]
124        p <- addContext a (patternFrom r (k+1) (absBody b) body)
125        return $ PLam (domInfo a) $ Abs (absName b) p
126      (_ , Var i es)
127       | i < k     -> do
128           t <- typeOfBV i
129           PBoundVar i <$> patternFrom r k (t , var i) es
130       -- The arguments of `var i` should be distinct bound variables
131       -- in order to build a Miller pattern
132       | Just vs <- allApplyElims es -> do
133           TelV tel _ <- telView =<< typeOfBV i
134           unless (size tel >= size vs) __IMPOSSIBLE__
135           let ts = applySubst (parallelS $ reverse $ map unArg vs) $ map unDom $ flattenTel tel
136           mbvs <- forM (zip ts vs) $ \(t , v) -> do
137             isEtaVar (unArg v) t >>= \case
138               Just j | j < k -> return $ Just $ v $> j
139               _              -> return Nothing
140           case sequence mbvs of
141             Just bvs | fastDistinct bvs -> do
142               let allBoundVars = IntSet.fromList (downFrom k)
143                   ok = not (isIrrelevant r) ||
144                        IntSet.fromList (map unArg bvs) == allBoundVars
145               if ok then return (PVar i bvs) else done
146             _ -> done
147       | otherwise -> done
148      (_ , _ ) | Just (d, pars) <- etaRecord -> do
149        def <- theDef <$> getConstInfo d
150        (tel, c, ci, vs) <- etaExpandRecord_ d pars def v
151        caseMaybeM (getFullyAppliedConType c t) __IMPOSSIBLE__ $ \ (_ , ct) -> do
152        PDef (conName c) <$> patternFrom r k (ct , Con c ci []) (map Apply vs)
153      (_ , Lam i t) -> __IMPOSSIBLE__
154      (_ , Lit{})   -> done
155      (_ , Def f es) | isIrrelevant r -> done
156      (_ , Def f es) -> do
157        Def lsuc [] <- primLevelSuc
158        Def lmax [] <- primLevelMax
159        case es of
160          [x]     | f == lsuc -> done
161          [x , y] | f == lmax -> done
162          _                   -> do
163            ft <- defType <$> getConstInfo f
164            PDef f <$> patternFrom r k (ft , Def f []) es
165      (_ , Con c ci vs) | isIrrelevant r -> done
166      (_ , Con c ci vs) ->
167        caseMaybeM (getFullyAppliedConType c t) __IMPOSSIBLE__ $ \ (_ , ct) -> do
168        PDef (conName c) <$> patternFrom r k (ct , Con c ci []) vs
169      (_ , Pi a b) | isIrrelevant r -> done
170      (_ , Pi a b) -> do
171        pa <- patternFrom r k () a
172        pb <- addContext a (patternFrom r (k+1) () $ absBody b)
173        return $ PPi pa (Abs (absName b) pb)
174      (_ , Sort s)     -> PSort <$> patternFrom r k () s
175      (_ , Level l)    -> __IMPOSSIBLE__
176      (_ , DontCare{}) -> __IMPOSSIBLE__
177      (_ , MetaV{})    -> __IMPOSSIBLE__
178      (_ , Dummy s _)  -> __IMPOSSIBLE_VERBOSE__ s
179
180-- | Convert from a non-linear pattern to a term.
181
182class NLPatToTerm p a where
183  nlPatToTerm :: PureTCM m => p -> m a
184
185  default nlPatToTerm ::
186    ( NLPatToTerm p' a', Traversable f, p ~ f p', a ~ f a'
187    , PureTCM m
188    ) => p -> m a
189  nlPatToTerm = traverse nlPatToTerm
190
191instance NLPatToTerm p a => NLPatToTerm [p] [a] where
192instance NLPatToTerm p a => NLPatToTerm (Arg p) (Arg a) where
193instance NLPatToTerm p a => NLPatToTerm (Dom p) (Dom a) where
194instance NLPatToTerm p a => NLPatToTerm (Elim' p) (Elim' a) where
195instance NLPatToTerm p a => NLPatToTerm (Abs p) (Abs a) where
196
197instance NLPatToTerm Nat Term where
198  nlPatToTerm = return . var
199
200instance NLPatToTerm NLPat Term where
201  nlPatToTerm = \case
202    PVar i xs      -> Var i . map Apply <$> nlPatToTerm xs
203    PTerm u        -> return u
204    PDef f es      -> (theDef <$> getConstInfo f) >>= \case
205      Constructor{ conSrcCon = c } -> Con c ConOSystem <$> nlPatToTerm es
206      _                            -> Def f <$> nlPatToTerm es
207    PLam i u       -> Lam i <$> nlPatToTerm u
208    PPi a b        -> Pi    <$> nlPatToTerm a <*> nlPatToTerm b
209    PSort s        -> Sort  <$> nlPatToTerm s
210    PBoundVar i es -> Var i <$> nlPatToTerm es
211
212instance NLPatToTerm NLPat Level where
213  nlPatToTerm = nlPatToTerm >=> levelView
214
215instance NLPatToTerm NLPType Type where
216  nlPatToTerm (NLPType s a) = El <$> nlPatToTerm s <*> nlPatToTerm a
217
218instance NLPatToTerm NLPSort Sort where
219  nlPatToTerm (PType l) = Type <$> nlPatToTerm l
220  nlPatToTerm (PProp l) = Prop <$> nlPatToTerm l
221  nlPatToTerm (PInf f n) = return $ Inf f n
222  nlPatToTerm PSizeUniv = return SizeUniv
223  nlPatToTerm PLockUniv = return LockUniv
224
225-- | Gather the set of pattern variables of a non-linear pattern
226class NLPatVars a where
227  nlPatVarsUnder :: Int -> a -> IntSet
228
229  nlPatVars :: a -> IntSet
230  nlPatVars = nlPatVarsUnder 0
231
232instance {-# OVERLAPPABLE #-} (Foldable f, NLPatVars a) => NLPatVars (f a) where
233  nlPatVarsUnder k = foldMap $ nlPatVarsUnder k
234
235instance NLPatVars NLPType where
236  nlPatVarsUnder k (NLPType l a) = nlPatVarsUnder k (l, a)
237
238instance NLPatVars NLPSort where
239  nlPatVarsUnder k = \case
240    PType l   -> nlPatVarsUnder k l
241    PProp l   -> nlPatVarsUnder k l
242    PInf f n  -> empty
243    PSizeUniv -> empty
244    PLockUniv -> empty
245
246instance NLPatVars NLPat where
247  nlPatVarsUnder k = \case
248      PVar i _  -> singleton $ i - k
249      PDef _ es -> nlPatVarsUnder k es
250      PLam _ p  -> nlPatVarsUnder k p
251      PPi a b   -> nlPatVarsUnder k (a, b)
252      PSort s   -> nlPatVarsUnder k s
253      PBoundVar _ es -> nlPatVarsUnder k es
254      PTerm{}   -> empty
255
256instance (NLPatVars a, NLPatVars b) => NLPatVars (a,b) where
257  nlPatVarsUnder k (a,b) = nlPatVarsUnder k a `mappend` nlPatVarsUnder k b
258
259instance NLPatVars a => NLPatVars (Abs a) where
260  nlPatVarsUnder k = \case
261    Abs   _ v -> nlPatVarsUnder (k+1) v
262    NoAbs _ v -> nlPatVarsUnder k v
263
264-- | Get all symbols that a non-linear pattern matches against
265class GetMatchables a where
266  getMatchables :: a -> [QName]
267
268  default getMatchables :: (Foldable f, GetMatchables a', a ~ f a') => a -> [QName]
269  getMatchables = foldMap getMatchables
270
271instance GetMatchables a => GetMatchables [a] where
272instance GetMatchables a => GetMatchables (Arg a) where
273instance GetMatchables a => GetMatchables (Dom a) where
274instance GetMatchables a => GetMatchables (Elim' a) where
275instance GetMatchables a => GetMatchables (Abs a) where
276
277instance (GetMatchables a, GetMatchables b) => GetMatchables (a,b) where
278  getMatchables (x,y) = getMatchables x ++ getMatchables y
279
280instance GetMatchables NLPat where
281  getMatchables p =
282    case p of
283      PVar _ _       -> empty
284      PDef f _       -> singleton f
285      PLam _ x       -> getMatchables x
286      PPi a b        -> getMatchables (a,b)
287      PSort s        -> getMatchables s
288      PBoundVar i es -> getMatchables es
289      PTerm u        -> getMatchables u
290
291instance GetMatchables NLPType where
292  getMatchables = getMatchables . nlpTypeUnEl
293
294instance GetMatchables NLPSort where
295  getMatchables = \case
296    PType l   -> getMatchables l
297    PProp l   -> getMatchables l
298    PInf f n  -> empty
299    PSizeUniv -> empty
300    PLockUniv -> empty
301
302instance GetMatchables Term where
303  getMatchables = getDefs' __IMPOSSIBLE__ singleton
304
305instance GetMatchables RewriteRule where
306  getMatchables = getMatchables . rewPats
307
308-- | Only computes free variables that are not bound (see 'nlPatVars'),
309--   i.e., those in a 'PTerm'.
310
311instance Free NLPat where
312  freeVars' = \case
313    PVar _ _       -> mempty
314    PDef _ es      -> freeVars' es
315    PLam _ u       -> freeVars' u
316    PPi a b        -> freeVars' (a,b)
317    PSort s        -> freeVars' s
318    PBoundVar _ es -> freeVars' es
319    PTerm t        -> freeVars' t
320
321instance Free NLPType where
322  freeVars' (NLPType s a) =
323    ifM (asks ((IgnoreNot ==) . feIgnoreSorts))
324      {- then -} (freeVars' (s, a))
325      {- else -} (freeVars' a)
326
327instance Free NLPSort where
328  freeVars' = \case
329    PType l   -> freeVars' l
330    PProp l   -> freeVars' l
331    PInf f n  -> mempty
332    PSizeUniv -> mempty
333    PLockUniv -> mempty
334