1{-# LANGUAGE AllowAmbiguousTypes #-} 2{-# LANGUAGE TypeApplications #-} 3 4{-# OPTIONS_GHC -fno-warn-orphans #-} 5 6-- | This module contains the definition of hereditary substitution 7-- and application operating on internal syntax which is in β-normal 8-- form (β including projection reductions). 9-- 10-- Further, it contains auxiliary functions which rely on substitution 11-- but not on reduction. 12 13module Agda.TypeChecking.Substitute 14 ( module Agda.TypeChecking.Substitute 15 , module Agda.TypeChecking.Substitute.Class 16 , module Agda.TypeChecking.Substitute.DeBruijn 17 , Substitution'(..), Substitution 18 ) where 19 20import Control.Arrow (first, second) 21import Control.Monad (guard) 22import Data.Coerce 23import Data.Function 24import qualified Data.List as List 25import Data.Map (Map) 26import Data.Maybe 27import Data.HashMap.Strict (HashMap) 28 29import Debug.Trace (trace) 30import Language.Haskell.TH.Syntax (thenCmp) -- lexicographic combination of Ordering 31 32import Agda.Interaction.Options 33 34import Agda.Syntax.Common 35import Agda.Syntax.Position 36import Agda.Syntax.Internal 37import Agda.Syntax.Internal.Pattern 38import qualified Agda.Syntax.Abstract as A 39 40import Agda.TypeChecking.Monad.Base 41import Agda.TypeChecking.Monad.Options (typeInType) 42import Agda.TypeChecking.Free as Free 43import Agda.TypeChecking.CompiledClause 44import Agda.TypeChecking.Positivity.Occurrence as Occ 45 46import Agda.TypeChecking.Substitute.Class 47import Agda.TypeChecking.Substitute.DeBruijn 48 49import Agda.Utils.Empty 50import Agda.Utils.Functor 51import Agda.Utils.List 52import Agda.Utils.List1 (List1, pattern (:|)) 53import qualified Agda.Utils.List1 as List1 54import qualified Agda.Utils.Maybe.Strict as Strict 55import Agda.Utils.Monad 56import Agda.Utils.Permutation 57import Agda.Utils.Pretty 58import Agda.Utils.Size 59import Agda.Utils.Tuple 60 61import Agda.Utils.Impossible 62 63 64-- | Apply @Elims@ while using the given function to report ill-typed 65-- redexes. 66-- Recursive calls for @applyE@ and @applySubst@ happen at type @t@ to 67-- propagate the same strategy to subtrees. 68{-# SPECIALIZE applyTermE :: (Empty -> Term -> Elims -> Term) -> Term -> Elims -> Term #-} 69{-# SPECIALIZE applyTermE :: (Empty -> Term -> Elims -> Term) -> BraveTerm -> Elims -> BraveTerm #-} 70applyTermE :: forall t. (Coercible Term t, Apply t, EndoSubst t) 71 => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t 72applyTermE err' m [] = m 73applyTermE err' m es = coerce $ 74 case coerce m of 75 Var i es' -> Var i (es' ++ es) 76 Def f es' -> defApp f es' es -- remove projection redexes 77 Con c ci args -> conApp @t err' c ci args es 78 Lam _ b -> 79 case es of 80 Apply a : es0 -> lazyAbsApp (coerce b :: Abs t) (coerce $ unArg a) `app` es0 81 IApply _ _ a : es0 -> lazyAbsApp (coerce b :: Abs t) (coerce a) `app` es0 82 _ -> err __IMPOSSIBLE__ 83 MetaV x es' -> MetaV x (es' ++ es) 84 Lit{} -> err __IMPOSSIBLE__ 85 Level{} -> err __IMPOSSIBLE__ 86 Pi _ _ -> err __IMPOSSIBLE__ 87 Sort s -> Sort $ s `applyE` es 88 Dummy s es' -> Dummy s (es' ++ es) 89 DontCare mv -> dontCare $ mv `app` es -- Andreas, 2011-10-02 90 -- need to go under DontCare, since "with" might resurrect irrelevant term 91 where 92 app :: Coercible t x => x -> Elims -> Term 93 app t es = coerce $ (coerce t :: t) `applyE` es 94 err e = err' e (coerce m) es 95 96instance Apply Term where 97 applyE = applyTermE absurd 98 99instance Apply BraveTerm where 100 applyE = applyTermE (\ _ t es -> Dummy "applyE" (Apply (defaultArg t) : es)) 101 102-- | If $v$ is a record value, @canProject f v@ 103-- returns its field @f@. 104canProject :: QName -> Term -> Maybe (Arg Term) 105canProject f v = 106 case v of 107 (Con (ConHead _ IsRecord{} _ fs) _ vs) -> do 108 (fld, i) <- findWithIndex ((f==) . unArg) fs 109 -- Jesper, 2019-10-17: dont unfold irrelevant projections 110 guard $ not $ isIrrelevant fld 111 -- Andreas, 2018-06-12, issue #2170 112 -- The ArgInfo from the ConHead is more accurate (relevance subtyping!). 113 setArgInfo (getArgInfo fld) <.> isApplyElim =<< listToMaybe (drop i vs) 114 _ -> Nothing 115 116-- | Eliminate a constructed term. 117conApp :: forall t. (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term 118conApp fk ch ci args [] = Con ch ci args 119conApp fk ch ci args (a@Apply{} : es) = conApp @t fk ch ci (args ++ [a]) es 120conApp fk ch ci args (a@IApply{} : es) = conApp @t fk ch ci (args ++ [a]) es 121conApp fk ch@(ConHead c _ _ fs) ci args ees@(Proj o f : es) = 122 let failure :: forall a. a -> a 123 failure err = flip trace err $ concat 124 [ "conApp: constructor ", prettyShow c 125 , unlines $ " with fields" : map ((" " ++) . prettyShow) fs 126 , unlines $ " and args" : map ((" " ++) . prettyShow) args 127 , " projected by ", prettyShow f 128 ] 129 isApply e = fromMaybe (failure __IMPOSSIBLE__) $ isApplyElim e 130 stuck err = fk err (Con ch ci args) [Proj o f] 131 -- Recurse using the instance for 't', see @applyTermE@ 132 app :: Term -> Elims -> Term 133 app v es = coerce $ applyE (coerce v :: t) es 134 in 135 case findWithIndex ((f==) . unArg) fs of 136 Nothing -> failure $ stuck __IMPOSSIBLE__ `app` es 137 Just (fld, i) -> let 138 -- Andreas, 2018-06-12, issue #2170 139 -- We safe-guard the projected value by DontCare using the ArgInfo stored at the record constructor, 140 -- since the ArgInfo in the constructor application might be inaccurate because of subtyping. 141 v = maybe (failure $ stuck __IMPOSSIBLE__) (relToDontCare fld . argToDontCare . isApply) $ listToMaybe $ drop i args 142 in v `app` es 143 144 -- -- Andreas, 2016-07-20 futile attempt to magically fix ProjOrigin 145 -- fallback = v 146 -- in if not $ null es then applyE v es else 147 -- -- If we have no more eliminations, we can return v 148 -- if o == ProjSystem then fallback else 149 -- -- If the result is a projected term with ProjSystem, 150 -- -- we can can restore it to ProjOrigin o. 151 -- -- Otherwise, we get unpleasant printing with eta-expanded record metas. 152 -- caseMaybe (hasElims v) fallback $ \ (hd, es0) -> 153 -- caseMaybe (initLast es0) fallback $ \ (es1, e2) -> 154 -- case e2 of 155 -- -- We want to replace this ProjSystem by o. 156 -- Proj ProjSystem q -> hd (es1 ++ [Proj o q]) 157 -- -- Andreas, 2016-07-21 for the whole testsuite 158 -- -- this case was never triggered! 159 -- _ -> fallback 160 161{- 162 i = maybe failure id $ elemIndex f $ map unArg fs 163 v = maybe failure unArg $ listToMaybe $ drop i args 164 -- Andreas, 2013-10-20 see Issue543a: 165 -- protect result of irrelevant projection. 166 r = maybe __IMPOSSIBLE__ getRelevance $ listToMaybe $ drop i fs 167 u | Irrelevant <- r = DontCare v 168 | otherwise = v 169 in applyE v es 170-} 171 172-- | @defApp f us vs@ applies @Def f us@ to further arguments @vs@, 173-- eliminating top projection redexes. 174-- If @us@ is not empty, we cannot have a projection redex, since 175-- the record argument is the first one. 176defApp :: QName -> Elims -> Elims -> Term 177defApp f [] (Apply a : es) | Just v <- canProject f (unArg a) 178 = argToDontCare v `applyE` es 179defApp f es0 es = Def f $ es0 ++ es 180 181-- protect irrelevant fields (see issue 610) 182argToDontCare :: Arg Term -> Term 183argToDontCare (Arg ai v) = relToDontCare ai v 184 185relToDontCare :: LensRelevance a => a -> Term -> Term 186relToDontCare ai v 187 | Irrelevant <- getRelevance ai = dontCare v 188 | otherwise = v 189 190-- Andreas, 2016-01-19: In connection with debugging issue #1783, 191-- I consider the Apply instance for Type harmful, as piApply is not 192-- safe if the type is not sufficiently reduced. 193-- (piApply is not in the monad and hence cannot unfold type synonyms). 194-- 195-- Without apply for types, one has to at least use piApply and be 196-- aware of doing something which has a precondition 197-- (type sufficiently reduced). 198-- 199-- By grepping for piApply, one can quickly get an overview over 200-- potentially harmful uses. 201-- 202-- In general, piApplyM is preferable over piApply since it is more robust 203-- and fails earlier than piApply, which may only fail at serialization time, 204-- when all thunks are forced. 205 206-- REMOVED: 207-- instance Apply Type where 208-- apply = piApply 209-- -- Maybe an @applyE@ instance would be useful here as well. 210-- -- A record type could be applied to a projection name 211-- -- to yield the field type. 212-- -- However, this works only in the monad where we can 213-- -- look up the fields of a record type. 214 215instance Apply Sort where 216 applyE s [] = s 217 applyE s es = case s of 218 MetaS x es' -> MetaS x $ es' ++ es 219 DefS d es' -> DefS d $ es' ++ es 220 _ -> __IMPOSSIBLE__ 221 222-- @applyE@ does not make sense for telecopes, definitions, clauses etc. 223 224instance TermSubst a => Apply (Tele a) where 225 apply tel [] = tel 226 apply EmptyTel _ = __IMPOSSIBLE__ 227 apply (ExtendTel _ tel) (t : ts) = lazyAbsApp tel (unArg t) `apply` ts 228 229 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 230 231instance Apply Definition where 232 apply (Defn info x t pol occ gens gpars df m c inst copy ma nc inj copat blk d) args = 233 Defn info x (piApply t args) (apply pol args) (apply occ args) (apply gens args) (drop (length args) gpars) df m c inst copy ma nc inj copat blk (apply d args) 234 235 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 236 237instance Apply RewriteRule where 238 apply r args = 239 let newContext = apply (rewContext r) args 240 sub = liftS (size newContext) $ parallelS $ 241 reverse $ map (PTerm . unArg) args 242 in RewriteRule 243 { rewName = rewName r 244 , rewContext = newContext 245 , rewHead = rewHead r 246 , rewPats = applySubst sub (rewPats r) 247 , rewRHS = applyNLPatSubst sub (rewRHS r) 248 , rewType = applyNLPatSubst sub (rewType r) 249 , rewFromClause = rewFromClause r 250 } 251 252 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 253 254instance {-# OVERLAPPING #-} Apply [Occ.Occurrence] where 255 apply occ args = List.drop (length args) occ 256 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 257 258instance {-# OVERLAPPING #-} Apply [Polarity] where 259 apply pol args = List.drop (length args) pol 260 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 261 262instance Apply NumGeneralizableArgs where 263 apply NoGeneralizableArgs args = NoGeneralizableArgs 264 apply (SomeGeneralizableArgs n) args = SomeGeneralizableArgs (n - length args) 265 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 266 267-- | Make sure we only drop variable patterns. 268instance {-# OVERLAPPING #-} Apply [NamedArg (Pattern' a)] where 269 apply ps args = loop (length args) ps 270 where 271 loop 0 ps = ps 272 loop n [] = __IMPOSSIBLE__ 273 loop n (p : ps) = 274 let recurse = loop (n - 1) ps 275 in case namedArg p of 276 VarP{} -> recurse 277 DotP{} -> __IMPOSSIBLE__ 278 LitP{} -> __IMPOSSIBLE__ 279 ConP{} -> __IMPOSSIBLE__ 280 DefP{} -> __IMPOSSIBLE__ 281 ProjP{} -> __IMPOSSIBLE__ 282 IApplyP{} -> recurse 283 284 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 285 286instance Apply Projection where 287 apply p args = p 288 { projIndex = projIndex p - size args 289 , projLams = projLams p `apply` args 290 } 291 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 292 293instance Apply ProjLams where 294 apply (ProjLams lams) args = ProjLams $ List.drop (length args) lams 295 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 296 297instance Apply Defn where 298 apply d [] = d 299 apply d args@(arg1:args1) = case d of 300 Axiom{} -> d 301 DataOrRecSig n -> DataOrRecSig (n - length args) 302 GeneralizableVar{} -> d 303 AbstractDefn d -> AbstractDefn $ apply d args 304 Function{ funClauses = cs, funCompiled = cc, funCovering = cov, funInv = inv 305 , funExtLam = extLam 306 , funProjection = Nothing } -> 307 d { funClauses = apply cs args 308 , funCompiled = apply cc args 309 , funCovering = apply cov args 310 , funInv = apply inv args 311 , funExtLam = modifySystem (`apply` args) <$> extLam 312 } 313 314 Function{ funClauses = cs, funCompiled = cc, funCovering = cov, funInv = inv 315 , funExtLam = extLam 316 , funProjection = Just p0} -> 317 case p0 `apply` args of 318 p@Projection{ projIndex = n } 319 | n < 0 -> d { funProjection = __IMPOSSIBLE__ } -- TODO (#3123): we actually get here! 320 -- case: applied only to parameters 321 | n > 0 -> d { funProjection = Just p } 322 -- case: applied also to record value (n == 0) 323 | otherwise -> 324 d { funClauses = apply cs args' 325 , funCompiled = apply cc args' 326 , funCovering = apply cov args' 327 , funInv = apply inv args' 328 , funProjection = if isVar0 then Just p{ projIndex = 0 } else Nothing 329 , funExtLam = modifySystem (\ _ -> __IMPOSSIBLE__) <$> extLam 330 } 331 where 332 larg = last1 arg1 args1 -- the record value 333 args' = [larg] 334 isVar0 = case unArg larg of Var 0 [] -> True; _ -> False 335 336 Datatype{ dataPars = np, dataClause = cl } -> 337 d { dataPars = np - size args 338 , dataClause = apply cl args 339 } 340 Record{ recPars = np, recClause = cl, recTel = tel 341 {-, recArgOccurrences = occ-} } -> 342 d { recPars = np - size args 343 , recClause = apply cl args, recTel = apply tel args 344-- , recArgOccurrences = List.drop (length args) occ 345 } 346 Constructor{ conPars = np } -> 347 d { conPars = np - size args } 348 Primitive{ primClauses = cs } -> 349 d { primClauses = apply cs args } 350 PrimitiveSort{} -> d 351 352 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 353 354instance Apply PrimFun where 355 apply (PrimFun x ar def) args = PrimFun x (ar - size args) $ \ vs -> def (args ++ vs) 356 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 357 358instance Apply Clause where 359 -- This one is a little bit tricksy after the parameter refinement change. 360 -- It is assumed that we only apply a clause to "parameters", i.e. 361 -- arguments introduced by lambda lifting. The problem is that these aren't 362 -- necessarily the first elements of the clause telescope. 363 apply cls@(Clause rl rf tel ps b t catchall exact recursive unreachable ell) args 364 | length args > length ps = __IMPOSSIBLE__ 365 | otherwise = 366 Clause rl rf 367 tel' 368 (applySubst rhoP $ drop (length args) ps) 369 (applySubst rho b) 370 (applySubst rho t) 371 catchall 372 exact 373 recursive 374 unreachable 375 ell 376 where 377 -- We have 378 -- Γ ⊢ args, for some outer context Γ 379 -- Δ ⊢ ps, where Δ is the clause telescope (tel) 380 rargs = map unArg $ reverse args 381 rps = reverse $ take (length args) ps 382 n = size tel 383 384 -- This is the new telescope. Created by substituting the args into the 385 -- appropriate places in the old telescope. We know where those are by 386 -- looking at the deBruijn indices of the patterns. 387 tel' = newTel n tel rps rargs 388 389 -- We then have to create a substitution from the old telescope to the 390 -- new telescope that we can apply to dot patterns and the clause body. 391 rhoP :: PatternSubstitution 392 rhoP = mkSub dotP n rps rargs 393 rho = mkSub id n rps rargs 394 395 substP :: Nat -> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern] 396 substP i v = subst i (dotP v) 397 398 -- Building the substitution from the old telescope to the new. The 399 -- interesting case is when we have a variable pattern: 400 -- We need Δ′ ⊢ ρ : Δ 401 -- where Δ′ = newTel Δ (xⁱ : ps) (v : vs) 402 -- = newTel Δ[xⁱ:=v] ps[xⁱ:=v'] vs 403 -- Note that we need v' = raise (|Δ| - 1) v, to make Γ ⊢ v valid in 404 -- ΓΔ[xⁱ:=v]. 405 -- A recursive call ρ′ = mkSub (substP i v' ps) vs gets us 406 -- Δ′ ⊢ ρ′ : Δ[xⁱ:=v] 407 -- so we just need Δ[xⁱ:=v] ⊢ σ : Δ and then ρ = ρ′ ∘ σ. 408 -- That's achieved by σ = singletonS i v'. 409 mkSub :: EndoSubst a => (Term -> a) -> Nat -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a 410 mkSub _ _ [] [] = idS 411 mkSub tm n (p : ps) (v : vs) = 412 case namedArg p of 413 VarP _ (DBPatVar _ i) -> mkSub tm (n - 1) (substP i v' ps) vs `composeS` singletonS i (tm v') 414 where v' = raise (n - 1) v 415 DotP{} -> mkSub tm n ps vs 416 ConP c _ ps' -> mkSub tm n (ps' ++ ps) (projections c v ++ vs) 417 DefP{} -> __IMPOSSIBLE__ 418 LitP{} -> __IMPOSSIBLE__ 419 ProjP{} -> __IMPOSSIBLE__ 420 IApplyP _ _ _ (DBPatVar _ i) -> mkSub tm (n - 1) (substP i v' ps) vs `composeS` singletonS i (tm v') 421 where v' = raise (n - 1) v 422 mkSub _ _ _ _ = __IMPOSSIBLE__ 423 424 -- The parameter patterns 'ps' are all variables or dot patterns, or eta 425 -- expanded record patterns (issue #2550). If they are variables they 426 -- can appear anywhere in the clause telescope. This function 427 -- constructs the new telescope with 'vs' substituted for 'ps'. 428 -- Example: 429 -- tel = (x : A) (y : B) (z : C) (w : D) 430 -- ps = y@3 w@0 431 -- vs = u v 432 -- newTel tel ps vs = (x : A) (z : C[u/y]) 433 newTel :: Nat -> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope 434 newTel n tel [] [] = tel 435 newTel n tel (p : ps) (v : vs) = 436 case namedArg p of 437 VarP _ (DBPatVar _ i) -> newTel (n - 1) (subTel (size tel - 1 - i) v tel) (substP i (raise (n - 1) v) ps) vs 438 DotP{} -> newTel n tel ps vs 439 ConP c _ ps' -> newTel n tel (ps' ++ ps) (projections c v ++ vs) 440 DefP{} -> __IMPOSSIBLE__ 441 LitP{} -> __IMPOSSIBLE__ 442 ProjP{} -> __IMPOSSIBLE__ 443 IApplyP _ _ _ (DBPatVar _ i) -> newTel (n - 1) (subTel (size tel - 1 - i) v tel) (substP i (raise (n - 1) v) ps) vs 444 newTel _ tel _ _ = __IMPOSSIBLE__ 445 446 projections c v = [ relToDontCare ai $ 447 -- #4528: We might have bogus terms here when printing a clause that 448 -- cannot be taken. To mitigate the problem we use a Def instead 449 -- a Proj elim for data constructors, which at least stops conApp 450 -- from crashing. See #4989 for not printing bogus terms at all. 451 case conDataRecord c of 452 IsData -> Def f [Apply (Arg ai v)] 453 IsRecord{} -> applyE v [Proj ProjSystem f] 454 | Arg ai f <- conFields c ] 455 456 -- subTel i v (Δ₁ (xᵢ : A) Δ₂) = Δ₁ Δ₂[xᵢ = v] 457 subTel i v EmptyTel = __IMPOSSIBLE__ 458 subTel 0 v (ExtendTel _ tel) = absApp tel v 459 subTel i v (ExtendTel a tel) = ExtendTel a $ subTel (i - 1) (raise 1 v) <$> tel 460 461 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 462 463instance Apply CompiledClauses where 464 apply cc args = case cc of 465 Fail hs -> Fail (drop len hs) 466 Done hs t 467 | length hs >= len -> 468 let sub = parallelS $ map var [0..length hs - len - 1] ++ map unArg args 469 in Done (List.drop len hs) $ applySubst sub t 470 | otherwise -> __IMPOSSIBLE__ 471 Case n bs 472 | unArg n >= len -> Case (n <&> \ m -> m - len) (apply bs args) 473 | otherwise -> __IMPOSSIBLE__ 474 where 475 len = length args 476 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 477 478instance Apply ExtLamInfo where 479 apply (ExtLamInfo m b sys) args = ExtLamInfo m b (apply sys args) 480 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 481 482instance Apply System where 483 -- We assume we apply a system only to arguments introduced by 484 -- lambda lifting. 485 apply (System tel sys) args 486 = if nargs > ntel then __IMPOSSIBLE__ 487 else System newTel (map (map (f -*- id) -*- f) sys) 488 489 where 490 f = applySubst sigma 491 nargs = length args 492 ntel = size tel 493 newTel = apply tel args 494 -- newTel ⊢ σ : tel 495 sigma = liftS (ntel - nargs) (parallelS (reverse $ map unArg args)) 496 497 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 498 499instance Apply a => Apply (WithArity a) where 500 apply (WithArity n a) args = WithArity n $ apply a args 501 applyE (WithArity n a) es = WithArity n $ applyE a es 502 503instance Apply a => Apply (Case a) where 504 apply (Branches cop cs eta ls m b lz) args = 505 Branches cop (apply cs args) (second (`apply` args) <$> eta) (apply ls args) (apply m args) b lz 506 applyE (Branches cop cs eta ls m b lz) es = 507 Branches cop (applyE cs es) (second (`applyE` es) <$> eta)(applyE ls es) (applyE m es) b lz 508 509instance Apply FunctionInverse where 510 apply NotInjective args = NotInjective 511 apply (Inverse inv) args = Inverse $ apply inv args 512 513 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 514 515instance Apply DisplayTerm where 516 apply (DTerm v) args = DTerm $ apply v args 517 apply (DDot v) args = DDot $ apply v args 518 apply (DCon c ci vs) args = DCon c ci $ vs ++ map (fmap DTerm) args 519 apply (DDef c es) args = DDef c $ es ++ map (Apply . fmap DTerm) args 520 apply (DWithApp v ws es) args = DWithApp v ws $ es ++ map Apply args 521 522 applyE (DTerm v) es = DTerm $ applyE v es 523 applyE (DDot v) es = DDot $ applyE v es 524 applyE (DCon c ci vs) es = DCon c ci $ vs ++ map (fmap DTerm) ws 525 where ws = fromMaybe __IMPOSSIBLE__ $ allApplyElims es 526 applyE (DDef c es') es = DDef c $ es' ++ map (fmap DTerm) es 527 applyE (DWithApp v ws es') es = DWithApp v ws $ es' ++ es 528 529instance {-# OVERLAPPABLE #-} Apply t => Apply [t] where 530 apply ts args = map (`apply` args) ts 531 applyE ts es = map (`applyE` es) ts 532 533instance Apply t => Apply (Blocked t) where 534 apply b args = fmap (`apply` args) b 535 applyE b es = fmap (`applyE` es) b 536 537instance Apply t => Apply (Maybe t) where 538 apply x args = fmap (`apply` args) x 539 applyE x es = fmap (`applyE` es) x 540 541instance Apply t => Apply (Strict.Maybe t) where 542 apply x args = fmap (`apply` args) x 543 applyE x es = fmap (`applyE` es) x 544 545instance Apply v => Apply (Map k v) where 546 apply x args = fmap (`apply` args) x 547 applyE x es = fmap (`applyE` es) x 548 549instance Apply v => Apply (HashMap k v) where 550 apply x args = fmap (`apply` args) x 551 applyE x es = fmap (`applyE` es) x 552 553instance (Apply a, Apply b) => Apply (a,b) where 554 apply (x,y) args = (apply x args, apply y args) 555 applyE (x,y) es = (applyE x es , applyE y es ) 556 557instance (Apply a, Apply b, Apply c) => Apply (a,b,c) where 558 apply (x,y,z) args = (apply x args, apply y args, apply z args) 559 applyE (x,y,z) es = (applyE x es , applyE y es , applyE z es ) 560 561instance DoDrop a => Apply (Drop a) where 562 apply x args = dropMore (size args) x 563 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 564 565instance DoDrop a => Abstract (Drop a) where 566 abstract tel x = unDrop (size tel) x 567 568instance Apply Permutation where 569 -- The permutation must start with [0..m - 1] 570 -- NB: section (- m) not possible (unary minus), hence (flip (-) m) 571 apply (Perm n xs) args = Perm (n - m) $ map (flip (-) m) $ drop m xs 572 where 573 m = size args 574 575 applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 576 577instance Abstract Permutation where 578 abstract tel (Perm n xs) = Perm (n + m) $ [0..m - 1] ++ map (+ m) xs 579 where 580 m = size tel 581 582-- | @(x:A)->B(x) `piApply` [u] = B(u)@ 583-- 584-- Precondition: The type must contain the right number of pis without 585-- having to perform any reduction. 586-- 587-- @piApply@ is potentially unsafe, the monadic 'piApplyM' is preferable. 588piApply :: Type -> Args -> Type 589piApply t [] = t 590piApply (El _ (Pi _ b)) (a:args) = lazyAbsApp b (unArg a) `piApply` args 591piApply t args = 592 trace ("piApply t = " ++ prettyShow t ++ "\n args = " ++ prettyShow args) __IMPOSSIBLE__ 593 594--------------------------------------------------------------------------- 595-- * Abstraction 596--------------------------------------------------------------------------- 597 598instance Abstract Term where 599 abstract = teleLam 600 601instance Abstract Type where 602 abstract = telePi_ 603 604instance Abstract Sort where 605 abstract EmptyTel s = s 606 abstract _ s = __IMPOSSIBLE__ 607 608instance Abstract Telescope where 609 EmptyTel `abstract` tel = tel 610 ExtendTel arg xtel `abstract` tel = ExtendTel arg $ xtel <&> (`abstract` tel) 611 612instance Abstract Definition where 613 abstract tel (Defn info x t pol occ gens gpars df m c inst copy ma nc inj copat blk d) = 614 Defn info x (abstract tel t) (abstract tel pol) (abstract tel occ) (abstract tel gens) 615 (replicate (size tel) Nothing ++ gpars) df m c inst copy ma nc inj copat blk (abstract tel d) 616 617-- | @tel ⊢ (Γ ⊢ lhs ↦ rhs : t)@ becomes @tel, Γ ⊢ lhs ↦ rhs : t)@ 618-- we do not need to change lhs, rhs, and t since they live in Γ. 619-- See 'Abstract Clause'. 620instance Abstract RewriteRule where 621 abstract tel (RewriteRule q gamma f ps rhs t c) = 622 RewriteRule q (abstract tel gamma) f ps rhs t c 623 624instance {-# OVERLAPPING #-} Abstract [Occ.Occurrence] where 625 abstract tel [] = [] 626 abstract tel occ = replicate (size tel) Mixed ++ occ -- TODO: check occurrence 627 628instance {-# OVERLAPPING #-} Abstract [Polarity] where 629 abstract tel [] = [] 630 abstract tel pol = replicate (size tel) Invariant ++ pol -- TODO: check polarity 631 632instance Abstract NumGeneralizableArgs where 633 abstract tel NoGeneralizableArgs = NoGeneralizableArgs 634 abstract tel (SomeGeneralizableArgs n) = SomeGeneralizableArgs (size tel + n) 635 636instance Abstract Projection where 637 abstract tel p = p 638 { projIndex = size tel + projIndex p 639 , projLams = abstract tel $ projLams p 640 } 641 642instance Abstract ProjLams where 643 abstract tel (ProjLams lams) = ProjLams $ 644 map (\ !dom -> argFromDom (fst <$> dom)) (telToList tel) ++ lams 645 646instance Abstract System where 647 abstract tel (System tel1 sys) = System (abstract tel tel1) sys 648 649instance Abstract Defn where 650 abstract tel d = case d of 651 Axiom{} -> d 652 DataOrRecSig n -> DataOrRecSig (size tel + n) 653 GeneralizableVar{} -> d 654 AbstractDefn d -> AbstractDefn $ abstract tel d 655 Function{ funClauses = cs, funCompiled = cc, funCovering = cov, funInv = inv 656 , funExtLam = extLam 657 , funProjection = Nothing } -> 658 d { funClauses = abstract tel cs 659 , funCompiled = abstract tel cc 660 , funCovering = abstract tel cov 661 , funInv = abstract tel inv 662 , funExtLam = modifySystem (abstract tel) <$> extLam 663 } 664 Function{ funClauses = cs, funCompiled = cc, funCovering = cov, funInv = inv 665 , funExtLam = extLam 666 , funProjection = Just p } -> 667 -- Andreas, 2015-05-11 if projection was applied to Var 0 668 -- then abstract over last element of tel (the others are params). 669 if projIndex p > 0 then d' else 670 d' { funClauses = map (abstractClause tel1) cs 671 , funCompiled = abstract tel1 cc 672 , funCovering = abstract tel1 cov 673 , funInv = abstract tel1 inv 674 , funExtLam = modifySystem (\ _ -> __IMPOSSIBLE__) <$> extLam 675 } 676 where 677 d' = d { funProjection = Just $ abstract tel p 678 , funClauses = map (abstractClause EmptyTel) cs } 679 tel1 = telFromList $ drop (size tel - 1) $ telToList tel 680 -- #5128: clause telescopes should be abstracted over the full telescope, regardless of 681 -- projection shenanigans. 682 abstractClause tel1 c = (abstract tel1 c) { clauseTel = abstract tel $ clauseTel c } 683 684 Datatype{ dataPars = np, dataClause = cl } -> 685 d { dataPars = np + size tel 686 , dataClause = abstract tel cl 687 } 688 Record{ recPars = np, recClause = cl, recTel = tel' } -> 689 d { recPars = np + size tel 690 , recClause = abstract tel cl 691 , recTel = abstract tel tel' 692 } 693 Constructor{ conPars = np } -> 694 d { conPars = np + size tel } 695 Primitive{ primClauses = cs } -> 696 d { primClauses = abstract tel cs } 697 PrimitiveSort{} -> d 698 699instance Abstract PrimFun where 700 abstract tel (PrimFun x ar def) = PrimFun x (ar + n) $ \ts -> def $ drop n ts 701 where n = size tel 702 703instance Abstract Clause where 704 abstract tel (Clause rl rf tel' ps b t catchall exact recursive unreachable ell) = 705 Clause rl rf (abstract tel tel') 706 (namedTelVars m tel ++ ps) 707 b 708 t -- nothing to do for t, since it lives under the telescope 709 catchall 710 exact 711 recursive 712 unreachable 713 ell 714 where m = size tel + size tel' 715 716instance Abstract CompiledClauses where 717 abstract tel cc = case cc of 718 Fail xs -> Fail (hs ++ xs) 719 Done xs t -> Done (hs ++ xs) t 720 Case n bs -> Case (n <&> \ i -> i + size tel) (abstract tel bs) 721 where 722 hs = map (argFromDom . fmap fst) $ telToList tel 723 724instance Abstract a => Abstract (WithArity a) where 725 abstract tel (WithArity n a) = WithArity n $ abstract tel a 726 727instance Abstract a => Abstract (Case a) where 728 abstract tel (Branches cop cs eta ls m b lz) = 729 Branches cop (abstract tel cs) (second (abstract tel) <$> eta) 730 (abstract tel ls) (abstract tel m) b lz 731 732telVars :: Int -> Telescope -> [Arg DeBruijnPattern] 733telVars m = map (fmap namedThing) . (namedTelVars m) 734 735namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern] 736namedTelVars m EmptyTel = [] 737namedTelVars m (ExtendTel !dom tel) = 738 Arg (domInfo dom) (namedDBVarP (m-1) $ absName tel) : 739 namedTelVars (m-1) (unAbs tel) 740 741instance Abstract FunctionInverse where 742 abstract tel NotInjective = NotInjective 743 abstract tel (Inverse inv) = Inverse $ abstract tel inv 744 745instance {-# OVERLAPPABLE #-} Abstract t => Abstract [t] where 746 abstract tel = map (abstract tel) 747 748instance Abstract t => Abstract (Maybe t) where 749 abstract tel x = fmap (abstract tel) x 750 751instance Abstract v => Abstract (Map k v) where 752 abstract tel m = fmap (abstract tel) m 753 754instance Abstract v => Abstract (HashMap k v) where 755 abstract tel m = fmap (abstract tel) m 756 757abstractArgs :: Abstract a => Args -> a -> a 758abstractArgs args x = abstract tel x 759 where 760 tel = foldr (\arg@(Arg info x) -> ExtendTel (__DUMMY_TYPE__ <$ domFromArg arg) . Abs x) 761 EmptyTel 762 $ zipWith (<$) names args 763 names = cycle $ map (stringToArgName . (:[])) ['a'..'z'] 764 765--------------------------------------------------------------------------- 766-- * Substitution and shifting\/weakening\/strengthening 767--------------------------------------------------------------------------- 768 769-- | If @permute π : [a]Γ -> [a]Δ@, then @applySubst (renaming _ π) : Term Γ -> Term Δ@ 770renaming :: forall a. DeBruijn a => Impossible -> Permutation -> Substitution' a 771renaming err p = prependS err gamma $ raiseS $ size p 772 where 773 gamma :: [Maybe a] 774 gamma = inversePermute p (deBruijnVar :: Int -> a) 775 -- gamma = safePermute (invertP (-1) p) $ map deBruijnVar [0..] 776 777-- | If @permute π : [a]Γ -> [a]Δ@, then @applySubst (renamingR π) : Term Δ -> Term Γ@ 778renamingR :: DeBruijn a => Permutation -> Substitution' a 779renamingR p@(Perm n _) = permute (reverseP p) (map deBruijnVar [0..]) ++# raiseS n 780 781-- | The permutation should permute the corresponding context. (right-to-left list) 782renameP :: Subst a => Impossible -> Permutation -> a -> a 783renameP err p = applySubst (renaming err p) 784 785instance EndoSubst a => Subst (Substitution' a) where 786 type SubstArg (Substitution' a) = a 787 applySubst rho sgm = composeS rho sgm 788 789{-# SPECIALIZE applySubstTerm :: Substitution -> Term -> Term #-} 790{-# SPECIALIZE applySubstTerm :: Substitution' BraveTerm -> BraveTerm -> BraveTerm #-} 791applySubstTerm :: forall t. (Coercible t Term, EndoSubst t, Apply t) => Substitution' t -> t -> t 792applySubstTerm IdS t = t 793applySubstTerm rho t = coerce $ case coerce t of 794 Var i es -> coerce $ lookupS rho i `applyE` subE es 795 Lam h m -> Lam h $ sub @(Abs t) m 796 Def f es -> defApp f [] $ subE es 797 Con c ci vs -> Con c ci $ subE vs 798 MetaV x es -> MetaV x $ subE es 799 Lit l -> Lit l 800 Level l -> levelTm $ sub @(Level' t) l 801 Pi a b -> uncurry Pi $ subPi (a,b) 802 Sort s -> Sort $ sub @(Sort' t) s 803 DontCare mv -> dontCare $ sub @t mv 804 Dummy s es -> Dummy s $ subE es 805 where 806 sub :: forall a b. (Coercible b a, SubstWith t a) => b -> b 807 sub t = coerce $ applySubst rho (coerce t :: a) 808 subE :: Elims -> Elims 809 subE = sub @[Elim' t] 810 subPi :: (Dom Type, Abs Type) -> (Dom Type, Abs Type) 811 subPi = sub @(Dom' t (Type'' t t), Abs (Type'' t t)) 812 813instance Subst Term where 814 type SubstArg Term = Term 815 applySubst = applySubstTerm 816 817instance Subst BraveTerm where 818 type SubstArg BraveTerm = BraveTerm 819 applySubst = applySubstTerm 820 821instance (Coercible a Term, Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Type'' a b) where 822 type SubstArg (Type'' a b) = SubstArg a 823 applySubst rho (El s t) = applySubst rho s `El` applySubst rho t 824 825instance (Coercible a Term, Subst a) => Subst (Sort' a) where 826 type SubstArg (Sort' a) = SubstArg a 827 applySubst rho = \case 828 Type n -> Type $ sub n 829 Prop n -> Prop $ sub n 830 Inf f n -> Inf f n 831 SSet n -> SSet $ sub n 832 SizeUniv -> SizeUniv 833 LockUniv -> LockUniv 834 PiSort a s1 s2 -> coerce $ piSort (coerce $ sub a) (coerce $ sub s1) (coerce $ sub s2) 835 FunSort s1 s2 -> coerce $ funSort (coerce $ sub s1) (coerce $ sub s2) 836 UnivSort s -> coerce $ univSort $ coerce $ sub s 837 MetaS x es -> MetaS x $ sub es 838 DefS d es -> DefS d $ sub es 839 s@DummyS{} -> s 840 where 841 sub :: forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b 842 sub x = applySubst rho x 843 844instance Subst a => Subst (Level' a) where 845 type SubstArg (Level' a) = SubstArg a 846 applySubst rho (Max n as) = Max n $ applySubst rho as 847 848instance Subst a => Subst (PlusLevel' a) where 849 type SubstArg (PlusLevel' a) = SubstArg a 850 applySubst rho (Plus n l) = Plus n $ applySubst rho l 851 852instance Subst Name where 853 type SubstArg Name = Term 854 applySubst rho = id 855 856instance Subst ConPatternInfo where 857 type SubstArg ConPatternInfo = Term 858 applySubst rho i = i{ conPType = applySubst rho $ conPType i } 859 860instance Subst Pattern where 861 type SubstArg Pattern = Term 862 applySubst rho = \case 863 ConP c mt ps -> ConP c (applySubst rho mt) $ applySubst rho ps 864 DefP o q ps -> DefP o q $ applySubst rho ps 865 DotP o t -> DotP o $ applySubst rho t 866 p@(VarP _o _x) -> p 867 p@(LitP _o _l) -> p 868 p@(ProjP _o _x) -> p 869 IApplyP o t u x -> IApplyP o (applySubst rho t) (applySubst rho u) x 870 871instance Subst A.ProblemEq where 872 type SubstArg A.ProblemEq = Term 873 applySubst rho (A.ProblemEq p v a) = 874 uncurry (A.ProblemEq p) $ applySubst rho (v,a) 875 876instance DeBruijn BraveTerm where 877 deBruijnVar = BraveTerm . deBruijnVar 878 deBruijnView = deBruijnView . unBrave 879 880instance DeBruijn NLPat where 881 deBruijnVar i = PVar i [] 882 deBruijnView = \case 883 PVar i [] -> Just i 884 PVar{} -> Nothing 885 PDef{} -> Nothing 886 PLam{} -> Nothing 887 PPi{} -> Nothing 888 PSort{} -> Nothing 889 PBoundVar{} -> Nothing -- or... ? 890 PTerm{} -> Nothing -- or... ? 891 892applyNLPatSubst :: TermSubst a => Substitution' NLPat -> a -> a 893applyNLPatSubst = applySubst . fmap nlPatToTerm 894 where 895 nlPatToTerm :: NLPat -> Term 896 nlPatToTerm = \case 897 PVar i xs -> Var i $ map (Apply . fmap var) xs 898 PTerm u -> u 899 PDef f es -> __IMPOSSIBLE__ 900 PLam i u -> __IMPOSSIBLE__ 901 PPi a b -> __IMPOSSIBLE__ 902 PSort s -> __IMPOSSIBLE__ 903 PBoundVar i es -> __IMPOSSIBLE__ 904 905applyNLSubstToDom :: SubstWith NLPat a => Substitution' NLPat -> Dom a -> Dom a 906applyNLSubstToDom rho dom = applySubst rho <$> dom{ domTactic = applyNLPatSubst rho $ domTactic dom } 907 908instance Subst NLPat where 909 type SubstArg NLPat = NLPat 910 applySubst rho = \case 911 PVar i bvs -> lookupS rho i `applyBV` bvs 912 PDef f es -> PDef f $ applySubst rho es 913 PLam i u -> PLam i $ applySubst rho u 914 PPi a b -> PPi (applyNLSubstToDom rho a) (applySubst rho b) 915 PSort s -> PSort $ applySubst rho s 916 PBoundVar i es -> PBoundVar i $ applySubst rho es 917 PTerm u -> PTerm $ applyNLPatSubst rho u 918 919 where 920 applyBV :: NLPat -> [Arg Int] -> NLPat 921 applyBV p ys = case p of 922 PVar i xs -> PVar i (xs ++ ys) 923 PTerm u -> PTerm $ u `apply` map (fmap var) ys 924 PDef f es -> __IMPOSSIBLE__ 925 PLam i u -> __IMPOSSIBLE__ 926 PPi a b -> __IMPOSSIBLE__ 927 PSort s -> __IMPOSSIBLE__ 928 PBoundVar i es -> __IMPOSSIBLE__ 929 930instance Subst NLPType where 931 type SubstArg NLPType = NLPat 932 applySubst rho (NLPType s a) = NLPType (applySubst rho s) (applySubst rho a) 933 934instance Subst NLPSort where 935 type SubstArg NLPSort = NLPat 936 applySubst rho = \case 937 PType l -> PType $ applySubst rho l 938 PProp l -> PProp $ applySubst rho l 939 PInf f n -> PInf f n 940 PSizeUniv -> PSizeUniv 941 PLockUniv -> PLockUniv 942 943instance Subst RewriteRule where 944 type SubstArg RewriteRule = NLPat 945 applySubst rho (RewriteRule q gamma f ps rhs t c) = 946 RewriteRule q (applyNLPatSubst rho gamma) 947 f (applySubst (liftS n rho) ps) 948 (applyNLPatSubst (liftS n rho) rhs) 949 (applyNLPatSubst (liftS n rho) t) 950 c 951 where n = size gamma 952 953instance Subst a => Subst (Blocked a) where 954 type SubstArg (Blocked a) = SubstArg a 955 applySubst rho b = fmap (applySubst rho) b 956 957instance Subst DisplayForm where 958 type SubstArg DisplayForm = Term 959 applySubst rho (Display n ps v) = 960 Display n (applySubst (liftS n rho) ps) 961 (applySubst (liftS n rho) v) 962 963instance Subst DisplayTerm where 964 type SubstArg DisplayTerm = Term 965 applySubst rho (DTerm v) = DTerm $ applySubst rho v 966 applySubst rho (DDot v) = DDot $ applySubst rho v 967 applySubst rho (DCon c ci vs) = DCon c ci $ applySubst rho vs 968 applySubst rho (DDef c es) = DDef c $ applySubst rho es 969 applySubst rho (DWithApp v vs es) = uncurry3 DWithApp $ applySubst rho (v, vs, es) 970 971instance Subst a => Subst (Tele a) where 972 type SubstArg (Tele a) = SubstArg a 973 applySubst rho EmptyTel = EmptyTel 974 applySubst rho (ExtendTel t tel) = uncurry ExtendTel $ applySubst rho (t, tel) 975 976instance Subst Constraint where 977 type SubstArg Constraint = Term 978 979 applySubst rho = \case 980 ValueCmp cmp a u v -> ValueCmp cmp (rf a) (rf u) (rf v) 981 ValueCmpOnFace cmp p t u v -> ValueCmpOnFace cmp (rf p) (rf t) (rf u) (rf v) 982 ElimCmp ps fs a v e1 e2 -> ElimCmp ps fs (rf a) (rf v) (rf e1) (rf e2) 983 SortCmp cmp s1 s2 -> SortCmp cmp (rf s1) (rf s2) 984 LevelCmp cmp l1 l2 -> LevelCmp cmp (rf l1) (rf l2) 985 IsEmpty r a -> IsEmpty r (rf a) 986 CheckSizeLtSat t -> CheckSizeLtSat (rf t) 987 FindInstance m cands -> FindInstance m (rf cands) 988 c@UnBlock{} -> c 989 c@CheckFunDef{} -> c 990 HasBiggerSort s -> HasBiggerSort (rf s) 991 HasPTSRule a s -> HasPTSRule (rf a) (rf s) 992 CheckLockedVars a b c d -> CheckLockedVars (rf a) (rf b) (rf c) (rf d) 993 UnquoteTactic t h g -> UnquoteTactic (rf t) (rf h) (rf g) 994 CheckMetaInst m -> CheckMetaInst m 995 UsableAtModality mod m -> UsableAtModality mod (rf m) 996 where 997 rf :: forall a. TermSubst a => a -> a 998 rf x = applySubst rho x 999 1000instance Subst CompareAs where 1001 type SubstArg CompareAs = Term 1002 applySubst rho (AsTermsOf a) = AsTermsOf $ applySubst rho a 1003 applySubst rho AsSizes = AsSizes 1004 applySubst rho AsTypes = AsTypes 1005 1006instance Subst a => Subst (Elim' a) where 1007 type SubstArg (Elim' a) = SubstArg a 1008 applySubst rho = \case 1009 Apply v -> Apply $ applySubst rho v 1010 IApply x y r -> IApply (applySubst rho x) (applySubst rho y) (applySubst rho r) 1011 e@Proj{} -> e 1012 1013instance Subst a => Subst (Abs a) where 1014 type SubstArg (Abs a) = SubstArg a 1015 applySubst rho (Abs x a) = Abs x $ applySubst (liftS 1 rho) a 1016 applySubst rho (NoAbs x a) = NoAbs x $ applySubst rho a 1017 1018instance Subst a => Subst (Arg a) where 1019 type SubstArg (Arg a) = SubstArg a 1020 applySubst IdS arg = arg 1021 applySubst rho arg = setFreeVariables unknownFreeVariables $ fmap (applySubst rho) arg 1022 1023instance Subst a => Subst (Named name a) where 1024 type SubstArg (Named name a) = SubstArg a 1025 applySubst rho = fmap (applySubst rho) 1026 1027instance (Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Dom' a b) where 1028 type SubstArg (Dom' a b) = SubstArg a 1029 1030 applySubst IdS dom = dom 1031 applySubst rho dom = setFreeVariables unknownFreeVariables $ 1032 fmap (applySubst rho) dom{ domTactic = applySubst rho (domTactic dom) } 1033 1034instance Subst a => Subst (Maybe a) where 1035 type SubstArg (Maybe a) = SubstArg a 1036 1037instance Subst a => Subst [a] where 1038 type SubstArg [a] = SubstArg a 1039 1040instance (Ord k, Subst a) => Subst (Map k a) where 1041 type SubstArg (Map k a) = SubstArg a 1042 1043instance Subst a => Subst (WithHiding a) where 1044 type SubstArg (WithHiding a) = SubstArg a 1045 1046instance Subst () where 1047 type SubstArg () = Term 1048 applySubst _ _ = () 1049 1050instance (Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (a, b) where 1051 type SubstArg (a, b) = SubstArg a 1052 applySubst rho (x,y) = (applySubst rho x, applySubst rho y) 1053 1054instance (Subst a, Subst b, Subst c, SubstArg a ~ SubstArg b, SubstArg b ~ SubstArg c) => Subst (a, b, c) where 1055 type SubstArg (a, b, c) = SubstArg a 1056 applySubst rho (x,y,z) = (applySubst rho x, applySubst rho y, applySubst rho z) 1057 1058instance 1059 ( Subst a, Subst b, Subst c, Subst d 1060 , SubstArg a ~ SubstArg b 1061 , SubstArg b ~ SubstArg c 1062 , SubstArg c ~ SubstArg d 1063 ) => Subst (a, b, c, d) where 1064 type SubstArg (a, b, c, d) = SubstArg a 1065 applySubst rho (x,y,z,u) = (applySubst rho x, applySubst rho y, applySubst rho z, applySubst rho u) 1066 1067instance Subst Candidate where 1068 type SubstArg Candidate = Term 1069 applySubst rho (Candidate q u t ov) = Candidate q (applySubst rho u) (applySubst rho t) ov 1070 1071instance Subst EqualityView where 1072 type SubstArg EqualityView = Term 1073 applySubst rho (OtherType t) = OtherType 1074 (applySubst rho t) 1075 applySubst rho (IdiomType t) = IdiomType 1076 (applySubst rho t) 1077 applySubst rho (EqualityType s eq l t a b) = EqualityType 1078 (applySubst rho s) 1079 eq 1080 (map (applySubst rho) l) 1081 (applySubst rho t) 1082 (applySubst rho a) 1083 (applySubst rho b) 1084 1085instance DeBruijn a => DeBruijn (Pattern' a) where 1086 debruijnNamedVar n i = varP $ debruijnNamedVar n i 1087 -- deBruijnView returns Nothing, to prevent consS and the like 1088 -- from dropping the names and origins when building a substitution. 1089 deBruijnView _ = Nothing 1090 1091fromPatternSubstitution :: PatternSubstitution -> Substitution 1092fromPatternSubstitution = fmap patternToTerm 1093 1094applyPatSubst :: TermSubst a => PatternSubstitution -> a -> a 1095applyPatSubst = applySubst . fromPatternSubstitution 1096 1097 1098usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a 1099usePatOrigin o p = case patternInfo p of 1100 Nothing -> p 1101 Just i -> usePatternInfo (i { patOrigin = o }) p 1102 1103usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a 1104usePatternInfo i p = case patternOrigin p of 1105 Nothing -> p 1106 Just PatOSplit -> p 1107 Just PatOAbsurd -> p 1108 Just _ -> case p of 1109 (VarP _ x) -> VarP i x 1110 (DotP _ u) -> DotP i u 1111 (ConP c (ConPatternInfo _ r ft b l) ps) 1112 -> ConP c (ConPatternInfo i r ft b l) ps 1113 DefP _ q ps -> DefP i q ps 1114 (LitP _ l) -> LitP i l 1115 ProjP{} -> __IMPOSSIBLE__ 1116 (IApplyP _ t u x) -> IApplyP i t u x 1117 1118instance Subst DeBruijnPattern where 1119 type SubstArg DeBruijnPattern = DeBruijnPattern 1120 applySubst IdS = id 1121 applySubst rho = \case 1122 VarP i x -> 1123 usePatternInfo i $ 1124 useName (dbPatVarName x) $ 1125 lookupS rho $ dbPatVarIndex x 1126 DotP i u -> DotP i $ applyPatSubst rho u 1127 ConP c ci ps -> ConP c ci {conPType = applyPatSubst rho (conPType ci)} $ applySubst rho ps 1128 DefP i q ps -> DefP i q $ applySubst rho ps 1129 p@(LitP _ _) -> p 1130 p@ProjP{} -> p 1131 IApplyP i t u x -> 1132 case useName (dbPatVarName x) $ lookupS rho $ dbPatVarIndex x of 1133 IApplyP _ _ _ y -> IApplyP i (applyPatSubst rho t) (applyPatSubst rho u) y 1134 VarP _ y -> IApplyP i (applyPatSubst rho t) (applyPatSubst rho u) y 1135 _ -> __IMPOSSIBLE__ 1136 where 1137 useName :: PatVarName -> DeBruijnPattern -> DeBruijnPattern 1138 useName n (VarP o x) 1139 | isUnderscore (dbPatVarName x) 1140 = VarP o $ x { dbPatVarName = n } 1141 useName _ x = x 1142 1143instance Subst Range where 1144 type SubstArg Range = Term 1145 applySubst _ = id 1146 1147--------------------------------------------------------------------------- 1148-- * Projections 1149--------------------------------------------------------------------------- 1150 1151-- | @projDropParsApply proj o args = 'projDropPars' proj o `'apply'` args@ 1152-- 1153-- This function is an optimization, saving us from construction lambdas we 1154-- immediately remove through application. 1155projDropParsApply :: Projection -> ProjOrigin -> Relevance -> Args -> Term 1156projDropParsApply (Projection prop d r _ lams) o rel args = 1157 case initLast $ getProjLams lams of 1158 -- If we have no more abstractions, we must be a record field 1159 -- (projection applied already to record value). 1160 Nothing -> if proper then Def d $ map Apply args else __IMPOSSIBLE__ 1161 Just (pars, Arg i y) -> 1162 let irr = isIrrelevant rel 1163 core 1164 | proper && not irr = Lam i $ Abs y $ Var 0 [Proj o d] 1165 | otherwise = Lam i $ Abs y $ Def d [Apply $ Var 0 [] <$ r] 1166 -- Issue2226: get ArgInfo for principal argument from projFromType 1167 -- Now drop pars many args 1168 (pars', args') = dropCommon pars args 1169 -- We only have to abstract over the parameters that exceed the arguments. 1170 -- We only have to apply to the arguments that exceed the parameters. 1171 in List.foldr (\ (Arg ai x) -> Lam ai . NoAbs x) (core `apply` args') pars' 1172 where proper = isJust prop 1173 1174--------------------------------------------------------------------------- 1175-- * Telescopes 1176--------------------------------------------------------------------------- 1177 1178-- ** Telescope view of a type 1179 1180type TelView = TelV Type 1181data TelV a = TelV { theTel :: Tele (Dom a), theCore :: a } 1182 deriving (Show, Functor) 1183 1184deriving instance (TermSubst a, Eq a) => Eq (TelV a) 1185deriving instance (TermSubst a, Ord a) => Ord (TelV a) 1186 1187-- | Takes off all exposed function domains from the given type. 1188-- This means that it does not reduce to expose @Pi@-types. 1189telView' :: Type -> TelView 1190telView' = telView'UpTo (-1) 1191 1192-- | @telView'UpTo n t@ takes off the first @n@ exposed function types of @t@. 1193-- Takes off all (exposed ones) if @n < 0@. 1194telView'UpTo :: Int -> Type -> TelView 1195telView'UpTo 0 t = TelV EmptyTel t 1196telView'UpTo n t = case unEl t of 1197 Pi a b -> absV a (absName b) $ telView'UpTo (n - 1) (absBody b) 1198 _ -> TelV EmptyTel t 1199 where 1200 absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t 1201 1202 1203-- ** Creating telescopes from lists of types 1204 1205-- | Turn a typed binding @(x1 .. xn : A)@ into a telescope. 1206bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a 1207bindsToTel' f [] t = [] 1208bindsToTel' f (x:xs) t = fmap (f x,) t : bindsToTel' f xs (raise 1 t) 1209 1210bindsToTel :: [Name] -> Dom Type -> ListTel 1211bindsToTel = bindsToTel' nameToArgName 1212 1213bindsToTel'1 :: (Name -> a) -> List1 Name -> Dom Type -> ListTel' a 1214bindsToTel'1 f = bindsToTel' f . List1.toList 1215 1216bindsToTel1 :: List1 Name -> Dom Type -> ListTel 1217bindsToTel1 = bindsToTel . List1.toList 1218 1219-- | Turn a typed binding @(x1 .. xn : A)@ into a telescope. 1220namedBindsToTel :: [NamedArg Name] -> Type -> Telescope 1221namedBindsToTel [] t = EmptyTel 1222namedBindsToTel (x : xs) t = 1223 ExtendTel (t <$ domFromNamedArgName x) $ Abs (nameToArgName $ namedArg x) $ namedBindsToTel xs (raise 1 t) 1224 1225namedBindsToTel1 :: List1 (NamedArg Name) -> Type -> Telescope 1226namedBindsToTel1 = namedBindsToTel . List1.toList 1227 1228domFromNamedArgName :: NamedArg Name -> Dom () 1229domFromNamedArgName x = () <$ domFromNamedArg (fmap forceName x) 1230 where 1231 -- If no explicit name is given we use the bound name for the label. 1232 forceName (Named Nothing x) = Named (Just $ WithOrigin Inserted $ Ranged (getRange x) $ nameToArgName x) x 1233 forceName x = x 1234 1235-- ** Abstracting in terms and types 1236 1237mkPiSort :: Dom Type -> Abs Type -> Sort 1238mkPiSort a b = piSort (unEl <$> a) (getSort $ unDom a) (getSort <$> b) 1239 1240-- | @mkPi dom t = telePi (telFromList [dom]) t@ 1241mkPi :: Dom (ArgName, Type) -> Type -> Type 1242mkPi !dom b = el $ Pi a (mkAbs x b) 1243 where 1244 x = fst $ unDom dom 1245 a = snd <$> dom 1246 el = El $ mkPiSort a (Abs x b) 1247 1248mkLam :: Arg ArgName -> Term -> Term 1249mkLam a v = Lam (argInfo a) (Abs (unArg a) v) 1250 1251lamView :: Term -> ([Arg ArgName], Term) 1252lamView (Lam h (Abs x b)) = first (Arg h x :) $ lamView b 1253lamView (Lam h (NoAbs x b)) = first (Arg h x :) $ lamView (raise 1 b) 1254lamView t = ([], t) 1255 1256unlamView :: [Arg ArgName] -> Term -> Term 1257unlamView xs b = foldr mkLam b xs 1258 1259telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type 1260telePi' reAbs = telePi where 1261 telePi EmptyTel t = t 1262 telePi (ExtendTel u tel) t = el $ Pi u $ reAbs b 1263 where 1264 b = (`telePi` t) <$> tel 1265 el = El $ mkPiSort u b 1266 1267-- | Uses free variable analysis to introduce 'NoAbs' bindings. 1268telePi :: Telescope -> Type -> Type 1269telePi = telePi' reAbs 1270 1271-- | Everything will be an 'Abs'. 1272telePi_ :: Telescope -> Type -> Type 1273telePi_ = telePi' id 1274 1275-- | Only abstract the visible components of the telescope, 1276-- and all that bind variables. Everything will be an 'Abs'! 1277-- Caution: quadratic time! 1278 1279telePiVisible :: Telescope -> Type -> Type 1280telePiVisible EmptyTel t = t 1281telePiVisible (ExtendTel u tel) t 1282 -- If u is not declared visible and b can be strengthened, skip quantification of u. 1283 | notVisible u, NoAbs x t' <- b' = t' 1284 -- Otherwise, include quantification over u. 1285 | otherwise = El (mkPiSort u b) $ Pi u b 1286 where 1287 b = tel <&> (`telePiVisible` t) 1288 b' = reAbs b 1289 1290-- | Abstract over a telescope in a term, producing lambdas. 1291-- Dumb abstraction: Always produces 'Abs', never 'NoAbs'. 1292-- 1293-- The implementation is sound because 'Telescope' does not use 'NoAbs'. 1294teleLam :: Telescope -> Term -> Term 1295teleLam EmptyTel t = t 1296teleLam (ExtendTel u tel) t = Lam (domInfo u) $ flip teleLam t <$> tel 1297 1298-- | Performs void ('noAbs') abstraction over telescope. 1299class TeleNoAbs a where 1300 teleNoAbs :: a -> Term -> Term 1301 1302instance TeleNoAbs ListTel where 1303 teleNoAbs tel t = foldr (\ Dom{domInfo = ai, unDom = (x, _)} -> Lam ai . NoAbs x) t tel 1304 1305instance TeleNoAbs Telescope where 1306 teleNoAbs tel = teleNoAbs $ telToList tel 1307 1308 1309-- ** Telescope typing 1310 1311-- | Given arguments @vs : tel@ (vector typing), extract their individual types. 1312-- Returns @Nothing@ is @tel@ is not long enough. 1313 1314typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type] 1315typeArgsWithTel _ [] = return [] 1316typeArgsWithTel (ExtendTel dom tel) (v : vs) = (dom :) <$> typeArgsWithTel (absApp tel v) vs 1317typeArgsWithTel EmptyTel{} (_:_) = Nothing 1318 1319--------------------------------------------------------------------------- 1320-- * Clauses 1321--------------------------------------------------------------------------- 1322 1323-- | In compiled clauses, the variables in the clause body are relative to the 1324-- pattern variables (including dot patterns) instead of the clause telescope. 1325compiledClauseBody :: Clause -> Maybe Term 1326compiledClauseBody cl = applySubst (renamingR perm) $ clauseBody cl 1327 where perm = fromMaybe __IMPOSSIBLE__ $ clausePerm cl 1328 1329--------------------------------------------------------------------------- 1330-- * Syntactic equality and order 1331-- 1332-- Needs weakening. 1333--------------------------------------------------------------------------- 1334 1335deriving instance Eq Substitution 1336deriving instance Ord Substitution 1337 1338deriving instance Eq Sort 1339deriving instance Ord Sort 1340deriving instance Eq Level 1341deriving instance Ord Level 1342deriving instance Eq PlusLevel 1343deriving instance Eq NotBlocked 1344deriving instance Eq t => Eq (Blocked t) 1345deriving instance Eq CandidateKind 1346deriving instance Eq Candidate 1347 1348deriving instance (Subst a, Eq a) => Eq (Tele a) 1349deriving instance (Subst a, Ord a) => Ord (Tele a) 1350 1351-- Andreas, 2019-11-16, issue #4201: to avoid potential unintended 1352-- performance loss, the Eq instance for Constraint is disabled: 1353-- 1354-- -- deriving instance Eq Constraint 1355-- 1356-- I am tempted to write 1357-- 1358-- instance Eq Constraint where (==) = undefined 1359-- 1360-- but this does not give a compilation error anymore when trying 1361-- to use equality on constraints. 1362-- Therefore, I hope this comment is sufficient to prevent a resurrection 1363-- of the Eq instance for Constraint. 1364 1365deriving instance Eq Section 1366 1367instance Ord PlusLevel where 1368 -- Compare on the atom first. Makes most sense for levelMax. 1369 compare (Plus n a) (Plus m b) = compare (a,n) (b,m) 1370 1371-- | Syntactic 'Type' equality, ignores sort annotations. 1372instance Eq a => Eq (Type' a) where 1373 (==) = (==) `on` unEl 1374 1375instance Ord a => Ord (Type' a) where 1376 compare = compare `on` unEl 1377 1378-- | Syntactic 'Term' equality, ignores stuff below @DontCare@ and sharing. 1379instance Eq Term where 1380 Var x vs == Var x' vs' = x == x' && vs == vs' 1381 Lam h v == Lam h' v' = h == h' && v == v' 1382 Lit l == Lit l' = l == l' 1383 Def x vs == Def x' vs' = x == x' && vs == vs' 1384 Con x _ vs == Con x' _ vs' = x == x' && vs == vs' 1385 Pi a b == Pi a' b' = a == a' && b == b' 1386 Sort s == Sort s' = s == s' 1387 Level l == Level l' = l == l' 1388 MetaV m vs == MetaV m' vs' = m == m' && vs == vs' 1389 DontCare _ == DontCare _ = True 1390 Dummy{} == Dummy{} = True 1391 _ == _ = False 1392 1393instance Eq a => Eq (Pattern' a) where 1394 VarP _ x == VarP _ y = x == y 1395 DotP _ u == DotP _ v = u == v 1396 ConP c _ ps == ConP c' _ qs = c == c && ps == qs 1397 LitP _ l == LitP _ l' = l == l' 1398 ProjP _ f == ProjP _ g = f == g 1399 IApplyP _ u v x == IApplyP _ u' v' y = u == u' && v == v' && x == y 1400 DefP _ f ps == DefP _ g qs = f == g && ps == qs 1401 _ == _ = False 1402 1403instance Ord Term where 1404 Var a b `compare` Var x y = compare x a `thenCmp` compare b y -- sort de Bruijn indices down (#2765) 1405 Var{} `compare` _ = LT 1406 _ `compare` Var{} = GT 1407 Def a b `compare` Def x y = compare (a, b) (x, y) 1408 Def{} `compare` _ = LT 1409 _ `compare` Def{} = GT 1410 Con a _ b `compare` Con x _ y = compare (a, b) (x, y) 1411 Con{} `compare` _ = LT 1412 _ `compare` Con{} = GT 1413 Lit a `compare` Lit x = compare a x 1414 Lit{} `compare` _ = LT 1415 _ `compare` Lit{} = GT 1416 Lam a b `compare` Lam x y = compare (a, b) (x, y) 1417 Lam{} `compare` _ = LT 1418 _ `compare` Lam{} = GT 1419 Pi a b `compare` Pi x y = compare (a, b) (x, y) 1420 Pi{} `compare` _ = LT 1421 _ `compare` Pi{} = GT 1422 Sort a `compare` Sort x = compare a x 1423 Sort{} `compare` _ = LT 1424 _ `compare` Sort{} = GT 1425 Level a `compare` Level x = compare a x 1426 Level{} `compare` _ = LT 1427 _ `compare` Level{} = GT 1428 MetaV a b `compare` MetaV x y = compare (a, b) (x, y) 1429 MetaV{} `compare` _ = LT 1430 _ `compare` MetaV{} = GT 1431 DontCare{} `compare` DontCare{} = EQ 1432 DontCare{} `compare` _ = LT 1433 _ `compare` DontCare{} = GT 1434 Dummy{} `compare` Dummy{} = EQ 1435 1436-- Andreas, 2017-10-04, issue #2775, ignore irrelevant arguments during with-abstraction. 1437-- 1438-- For reasons beyond my comprehension, the following Eq instances are not employed 1439-- by with-abstraction in TypeChecking.Abstract.isPrefixOf. 1440-- Instead, I modified the general Eq instance for Arg to ignore the argument 1441-- if irrelevant. 1442 1443-- -- | Ignore irrelevant arguments in equality check. 1444-- -- Also ignore origin. 1445-- instance {-# OVERLAPPING #-} Eq (Arg Term) where 1446-- a@(Arg (ArgInfo h r _o) t) == a'@(Arg (ArgInfo h' r' _o') t') = trace ("Eq (Arg Term) on " ++ show a ++ " and " ++ show a') $ 1447-- h == h' && ((r == Irrelevant) || (r' == Irrelevant) || (t == t')) 1448-- -- Andreas, 2017-10-04: According to Syntax.Common, equality on Arg ignores Relevance and Origin. 1449 1450-- instance {-# OVERLAPPING #-} Eq Args where 1451-- us == vs = length us == length vs && and (zipWith (==) us vs) 1452 1453-- instance {-# OVERLAPPING #-} Eq Elims where 1454-- us == vs = length us == length vs && and (zipWith (==) us vs) 1455 1456-- | Equality of binders relies on weakening 1457-- which is a special case of renaming 1458-- which is a special case of substitution. 1459instance (Subst a, Eq a) => Eq (Abs a) where 1460 NoAbs _ a == NoAbs _ b = a == b -- no need to raise if both are NoAbs 1461 a == b = absBody a == absBody b 1462 1463instance (Subst a, Ord a) => Ord (Abs a) where 1464 NoAbs _ a `compare` NoAbs _ b = a `compare` b -- no need to raise if both are NoAbs 1465 a `compare` b = absBody a `compare` absBody b 1466 1467deriving instance Ord a => Ord (Dom a) 1468 1469instance (Subst a, Eq a) => Eq (Elim' a) where 1470 Apply a == Apply b = a == b 1471 Proj _ x == Proj _ y = x == y 1472 IApply x y r == IApply x' y' r' = x == x' && y == y' && r == r' 1473 _ == _ = False 1474 1475instance (Subst a, Ord a) => Ord (Elim' a) where 1476 Apply a `compare` Apply b = a `compare` b 1477 Proj _ x `compare` Proj _ y = x `compare` y 1478 IApply x y r `compare` IApply x' y' r' = compare x x' `mappend` compare y y' `mappend` compare r r' 1479 Apply{} `compare` _ = LT 1480 _ `compare` Apply{} = GT 1481 Proj{} `compare` _ = LT 1482 _ `compare` Proj{} = GT 1483 1484 1485--------------------------------------------------------------------------- 1486-- * Sort stuff 1487--------------------------------------------------------------------------- 1488 1489-- | @univSort' univInf s@ gets the next higher sort of @s@, if it is 1490-- known (i.e. it is not just @UnivSort s@). 1491-- 1492-- Precondition: @s@ is reduced 1493univSort' :: Sort -> Maybe Sort 1494univSort' (Type l) = Just $ Type $ levelSuc l 1495univSort' (Prop l) = Just $ Type $ levelSuc l 1496univSort' (Inf f n) = Just $ Inf f $ 1 + n 1497univSort' (SSet l) = Just $ SSet $ levelSuc l 1498univSort' SizeUniv = Just $ Inf IsFibrant 0 1499univSort' LockUniv = Just $ Inf IsFibrant 0 -- lock polymorphism is not actually supported 1500univSort' s = Nothing 1501 1502univSort :: Sort -> Sort 1503univSort s = fromMaybe (UnivSort s) $ univSort' s 1504 1505sort :: Sort -> Type 1506sort s = El (univSort s) $ Sort s 1507 1508ssort :: Level -> Type 1509ssort l = sort (SSet l) 1510 1511-- | Returns @Nothing@ for unknown (meta) sorts, and otherwise returns 1512-- @Just (b,f)@ where @b@ indicates smallness and @f@ fibrancy. 1513-- I.e., @b@ is @True@ for (relatively) small sorts like @Set l@ and 1514-- @Prop l@, and instead @b@ is @False@ for large sorts such as @Setω@. 1515isSmallSort :: Sort -> Maybe (Bool,IsFibrant) 1516isSmallSort Type{} = Just (True,IsFibrant) 1517isSmallSort Prop{} = Just (True,IsFibrant) 1518isSmallSort SizeUniv = Just (True,IsFibrant) 1519isSmallSort LockUniv = Just (True,IsFibrant) 1520isSmallSort (Inf f _) = Just (False,f) 1521isSmallSort SSet{} = Just (True,IsStrict) 1522isSmallSort MetaS{} = Nothing 1523isSmallSort FunSort{} = Nothing 1524isSmallSort PiSort{} = Nothing 1525isSmallSort UnivSort{} = Nothing 1526isSmallSort DefS{} = Nothing 1527isSmallSort DummyS{} = Nothing 1528 1529fibrantLub :: IsFibrant -> IsFibrant -> IsFibrant 1530fibrantLub IsStrict a = IsStrict 1531fibrantLub a IsStrict = IsStrict 1532fibrantLub a b = a 1533 1534-- | Compute the sort of a function type from the sorts of its 1535-- domain and codomain. 1536funSort' :: Sort -> Sort -> Maybe Sort 1537funSort' a b = case (a, b) of 1538 (Inf af m , Inf bf n ) -> Just $ Inf (fibrantLub af bf) $ max m n 1539 (Inf af m , b ) | Just (True,bf) <- isSmallSort b -> Just $ Inf (fibrantLub af bf) m 1540 (a , Inf bf n ) | Just (True,af) <- isSmallSort a -> Just $ Inf (fibrantLub af bf) n 1541 (Type a , Type b ) -> Just $ Type $ levelLub a b 1542 (LockUniv , b ) -> Just b 1543 -- No functions into lock types 1544 (a , LockUniv ) -> Nothing 1545 (SizeUniv , b ) -> Just b 1546 (a , SizeUniv ) | Just (True,_) <- isSmallSort a -> Just SizeUniv 1547 (Prop a , Type b ) -> Just $ Type $ levelLub a b 1548 (Type a , Prop b ) -> Just $ Prop $ levelLub a b 1549 (Prop a , Prop b ) -> Just $ Prop $ levelLub a b 1550 (SSet a , SSet b ) -> Just $ SSet $ levelLub a b 1551 (Type a , SSet b ) -> Just $ SSet $ levelLub a b 1552 (SSet a , Type b ) -> Just $ SSet $ levelLub a b 1553 (a , b ) -> Nothing 1554 1555funSort :: Sort -> Sort -> Sort 1556funSort a b = fromMaybe (FunSort a b) $ funSort' a b 1557 1558-- | Compute the sort of a pi type from the sorts of its domain 1559-- and codomain. 1560piSort' :: Dom Term -> Sort -> Abs Sort -> Maybe Sort 1561piSort' a s1 (NoAbs _ s2) = Just $ FunSort s1 s2 1562piSort' a s1 s2Abs@(Abs _ s2) = case flexRigOccurrenceIn 0 s2 of 1563 Nothing -> Just $ FunSort s1 $ noabsApp __IMPOSSIBLE__ s2Abs 1564 Just o | Just (True, f1) <- isSmallSort s1, Just (True, f2) <- isSmallSort s2 -> case o of 1565 StronglyRigid -> Just $ Inf (fibrantLub f1 f2) 0 1566 Unguarded -> Just $ Inf (fibrantLub f1 f2) 0 1567 WeaklyRigid -> Just $ Inf (fibrantLub f1 f2) 0 1568 Flexible _ -> Nothing 1569 Just o | Inf f1 n <- s1 , Just (True, f2) <- isSmallSort s2 -> Just $ Inf (fibrantLub f1 f2) n 1570 Just _ -> Nothing 1571 1572-- Andreas, 2019-06-20 1573-- KEEP the following commented out code for the sake of the discussion on irrelevance. 1574-- piSort' a bAbs@(Abs _ b) = case occurrence 0 b of 1575-- -- Andreas, Jesper, AIM XXIX, 2019-03-18, issue #3631 1576-- -- Remember the NoAbs here! 1577-- NoOccurrence -> Just $ funSort a $ noabsApp __IMPOSSIBLE__ bAbs 1578-- -- Andreas, 2017-01-18, issue #2408: 1579-- -- The sort of @.(a : A) → Set (f a)@ in context @f : .A → Level@ 1580-- -- is @dLub Set λ a → Set (lsuc (f a))@, but @DLub@s are not serialized. 1581-- -- Alternatives: 1582-- -- 1. -- Irrelevantly -> sLub s1 (absApp b $ DontCare $ Sort Prop) 1583-- -- We cheat here by simplifying the sort to @Set (lsuc (f *))@ 1584-- -- where * is a dummy value. The rationale is that @f * = f a@ (irrelevance!) 1585-- -- and that if we already have a neutral level @f a@ 1586-- -- it should not hurt to have @f *@ even if type @A@ is empty. 1587-- -- However: sorts are printed in error messages when sorts do not match. 1588-- -- Also, sorts with a dummy like Prop would be ill-typed. 1589-- -- 2. We keep the DLub, and serialize it. 1590-- -- That's clean and principled, even though DLubs make level solving harder. 1591-- -- Jesper, 2018-04-20: another alternative: 1592-- -- 3. Return @Inf@ as in the relevant case. This is conservative and might result 1593-- -- in more occurrences of @Setω@ than desired, but at least it doesn't pollute 1594-- -- the sort system with new 'exotic' sorts. 1595-- Irrelevantly -> Just Inf 1596-- StronglyRigid -> Just Inf 1597-- Unguarded -> Just Inf 1598-- WeaklyRigid -> Just Inf 1599-- Flexible _ -> Nothing 1600 1601piSort :: Dom Term -> Sort -> Abs Sort -> Sort 1602piSort a s1 s2 = case piSort' a s1 s2 of 1603 Just s -> s 1604 Nothing -> PiSort a s1 s2 1605 1606--------------------------------------------------------------------------- 1607-- * Level stuff 1608--------------------------------------------------------------------------- 1609 1610-- ^ Computes @n0 ⊔ a₁ ⊔ a₂ ⊔ ... ⊔ aₙ@ and return its canonical form. 1611levelMax :: Integer -> [PlusLevel] -> Level 1612levelMax n0 as0 = Max n as 1613 where 1614 -- step 1: flatten nested @Level@ expressions in @PlusLevel@s 1615 Max n1 as1 = expandLevel $ Max n0 as0 1616 -- step 2: remove subsumed @PlusLevel@s 1617 as2 = removeSubsumed as1 1618 -- step 3: sort remaining @PlusLevel@s 1619 as = List.sort as2 1620 -- step 4: set constant to 0 if it is subsumed by one of the @PlusLevel@s 1621 greatestB = Prelude.maximum $ 0 : [ n | Plus n _ <- as ] 1622 n | n1 > greatestB = n1 1623 | otherwise = 0 1624 1625 lmax :: Integer -> [PlusLevel] -> [Level] -> Level 1626 lmax m as [] = Max m as 1627 lmax m as (Max n bs : ls) = lmax (max m n) (bs ++ as) ls 1628 1629 expandLevel :: Level -> Level 1630 expandLevel (Max m as) = lmax m [] $ map expandPlus as 1631 1632 expandPlus :: PlusLevel -> Level 1633 expandPlus (Plus m l) = levelPlus m (expandTm l) 1634 1635 expandTm (Level l) = expandLevel l 1636 expandTm l = atomicLevel l 1637 1638 removeSubsumed [] = [] 1639 removeSubsumed (Plus n a : bs) 1640 | not $ null ns = removeSubsumed bs 1641 | otherwise = Plus n a : removeSubsumed [ b | b@(Plus _ a') <- bs, a /= a' ] 1642 where 1643 ns = [ m | Plus m a' <- bs, a == a', m > n ] 1644 1645-- | Given two levels @a@ and @b@, compute @a ⊔ b@ and return its 1646-- canonical form. 1647levelLub :: Level -> Level -> Level 1648levelLub (Max m as) (Max n bs) = levelMax (max m n) $ as ++ bs 1649 1650levelTm :: Level -> Term 1651levelTm l = 1652 case l of 1653 Max 0 [Plus 0 l] -> l 1654 _ -> Level l 1655