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