0 | module TTImp.ProcessDef

   2 | import Core.Case.CaseBuilder

   3 | import Core.Case.CaseTree

   4 | import Core.Case.CaseTree.Pretty

   5 | import Core.Coverage

   6 | import Core.Env

   7 | import Core.Hash

   8 | import Core.LinearCheck

   9 | import Core.Metadata

  10 | import Core.Termination

  11 | import Core.Termination.CallGraph

  12 | import Core.Transform

  13 | import Core.Value

  14 | import Core.UnifyState

  16 | import Idris.REPL.Opts

  17 | import Idris.Syntax

  18 | import Idris.Pretty.Annotations

  20 | import TTImp.BindImplicits

  21 | import TTImp.Elab

  22 | import TTImp.Elab.Binders

  23 | import TTImp.Elab.Check

  24 | import TTImp.Elab.Utils

  25 | import TTImp.Impossible

  26 | import TTImp.PartialEval

  27 | import TTImp.TTImp

  28 | import TTImp.TTImp.Functor

  29 | import TTImp.ProcessType

  30 | import TTImp.Unelab

  31 | import TTImp.WithClause

  33 | import Data.Either

  34 | import Data.List

  35 | import Data.String

  36 | import Data.Maybe

  37 | import Libraries.Data.NameMap

  38 | import Libraries.Data.WithDefault

  39 | import Libraries.Text.PrettyPrint.Prettyprinter

  40 | import Libraries.Data.List.SizeOf

  42 | %default covering

  45 |   mismatchNF : {auto c : Ref Ctxt Defs} ->

  46 |                {vars : _} ->

  47 |                Defs -> NF vars -> NF vars -> Core Bool

  48 |   mismatchNF defs (NTCon _ xn _ xargs) (NTCon _ yn _ yargs)

  49 |       = if xn /= yn

  50 |            then pure True

  51 |            else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)

  52 |   mismatchNF defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)

  53 |       = if xt /= yt

  54 |            then pure True

  55 |            else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)

  56 |   mismatchNF defs (NPrimVal _ xc) (NPrimVal _ yc) = pure (xc /= yc)

  57 |   mismatchNF defs (NDelayed _ _ x) (NDelayed _ _ y) = mismatchNF defs x y

  58 |   mismatchNF defs (NDelay _ _ _ x) (NDelay _ _ _ y)

  59 |       = mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)

  61 |   -- NPrimVal is apart from NDCon, NTCon, NBind, and NType

  62 |   mismatchNF defs (NPrimVal {}) (NDCon {}) = pure True

  63 |   mismatchNF defs (NDCon {}) (NPrimVal {}) = pure True

  64 |   mismatchNF defs (NPrimVal {}) (NBind {}) = pure True

  65 |   mismatchNF defs (NBind {}) (NPrimVal {}) = pure True

  66 |   mismatchNF defs (NPrimVal {}) (NTCon {}) = pure True

  67 |   mismatchNF defs (NTCon {}) (NPrimVal {}) = pure True

  68 |   mismatchNF defs (NPrimVal {}) (NType {}) = pure True

  69 |   mismatchNF defs (NType {}) (NPrimVal {}) = pure True

  72 |   mismatchNF defs (NTCon {}) (NBind {}) = pure True

  73 |   mismatchNF defs (NBind {}) (NTCon {}) = pure True

  74 |   mismatchNF defs (NTCon {}) (NType {}) = pure True

  75 |   mismatchNF defs (NType {}) (NTCon {}) = pure True

  78 |   mismatchNF defs (NBind {}) (NType {}) = pure True

  79 |   mismatchNF defs (NType {}) (NBind {}) = pure True

  81 |   mismatchNF _ _ _ = pure False

  83 |   mismatch : {auto c : Ref Ctxt Defs} ->

  84 |              {vars : _} ->

  85 |              Defs -> (Closure vars, Closure vars) -> Core Bool

  86 |   mismatch defs (x, y)

  87 |       = mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)

  93 | impossibleOK : {auto c : Ref Ctxt Defs} ->

  94 |                {vars : _} ->

  95 |                Defs -> NF vars -> NF vars -> Core Bool

  96 | impossibleOK defs (NTCon _ xn xa xargs) (NTCon _ yn ya yargs)

  97 |     = if xn /= yn

  98 |          then pure True

  99 |          else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)

 101 | impossibleOK defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)

 102 |     = if xt /= yt

 103 |          then pure True

 104 |          else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)

 105 | impossibleOK defs (NPrimVal _ x) (NPrimVal _ y) = pure (x /= y)

 108 | impossibleOK defs (NPrimVal {}) (NDCon {}) = pure True

 109 | impossibleOK defs (NDCon {}) (NPrimVal {}) = pure True

 110 | impossibleOK defs (NPrimVal {}) (NBind {}) = pure True

 111 | impossibleOK defs (NBind {}) (NPrimVal {}) = pure True

 112 | impossibleOK defs (NPrimVal {}) (NTCon {}) = pure True

 113 | impossibleOK defs (NTCon {}) (NPrimVal {}) = pure True

 114 | impossibleOK defs (NPrimVal {}) (NType {}) = pure True

 115 | impossibleOK defs (NType {}) (NPrimVal {}) = pure True

 118 | impossibleOK defs (NTCon {}) (NBind {}) = pure True

 119 | impossibleOK defs (NBind {}) (NTCon {}) = pure True

 120 | impossibleOK defs (NTCon {}) (NType {}) = pure True

 121 | impossibleOK defs (NType {}) (NTCon {}) = pure True

 124 | impossibleOK defs (NBind {}) (NType {}) = pure True

 125 | impossibleOK defs (NType {}) (NBind {}) = pure True

 127 | impossibleOK defs x y = pure False

 130 | impossibleErrOK : {auto c : Ref Ctxt Defs} ->

 131 |                   Defs -> Error -> Core Bool

 132 | impossibleErrOK defs (CantConvert fc gam env l r)

 133 |     = do let defs = { gamma := gam } defs

 134 |          impossibleOK defs !(nf defs env l)

 135 |                            !(nf defs env r)

 136 | impossibleErrOK defs (CantSolveEq fc gam env l r)

 137 |     = do let defs = { gamma := gam } defs

 138 |          impossibleOK defs !(nf defs env l)

 139 |                            !(nf defs env r)

 140 | impossibleErrOK defs (CyclicMeta {}) = pure True

 141 | impossibleErrOK defs (AllFailed errs)

 142 |     = allM (impossibleErrOK defs) (map snd errs)

 143 | impossibleErrOK defs (WhenUnifying _ _ _ _ _ err)

 144 |     = impossibleErrOK defs err

 145 | impossibleErrOK defs ImpossibleCase = pure True

 146 | impossibleErrOK defs _ = pure False

 154 | extendEnv : {vars : _} ->

 155 |             Env Term vars -> Thin inner vars ->

 156 |             NestedNames vars ->

 157 |             Term vars -> Term vars ->

 158 |             Core (vars' **

 159 |                     (Thin inner vars',

 160 |                      Env Term vars', NestedNames vars',

 161 |                      Term vars', Term vars'))

 162 | extendEnv env p nest (Bind _ n (PVar fc c pi tmty) sc) (Bind _ n' (PVTy {}) tysc) with (nameEq n n')

 163 |   extendEnv env p nest (Bind _ n (PVar fc c pi tmty) sc) (Bind _ n' (PVTy {}) tysc) | Nothing

 164 |       = throw (InternalError "Can't happen: names don't match in pattern type")

 165 |   extendEnv env p nest (Bind _ n (PVar fc c pi tmty) sc) (Bind _ n (PVTy {}) tysc) | (Just Refl)

 166 |       = extendEnv (PVar fc c pi tmty :: env) (Drop p) (weaken (dropName n nest)) sc tysc

 167 | extendEnv env p nest (Bind _ n (PLet fc c tmval tmty) sc) (Bind _ n' (PLet {}) tysc) with (nameEq n n')

 168 |   extendEnv env p nest (Bind _ n (PLet fc c tmval tmty) sc) (Bind _ n' (PLet {}) tysc) | Nothing

 169 |       = throw (InternalError "Can't happen: names don't match in pattern type")

 170 |   -- PLet on the left becomes Let on the right, to give it computational force

 171 |   extendEnv env p nest (Bind _ n (PLet fc c tmval tmty) sc) (Bind _ n (PLet {}) tysc) | (Just Refl)

 172 |       = extendEnv (Let fc c tmval tmty :: env) (Drop p) (weaken (dropName n nest)) sc tysc

 173 | extendEnv env p nest tm ty

 174 |       = pure (_ ** (p, env, nest, tm, ty))

 182 | findLinear : {vars : _} ->

 183 |              {auto c : Ref Ctxt Defs} ->

 184 |              Bool -> Nat -> RigCount -> Term vars ->

 185 |              Core (List (Name, RigCount))

 186 | findLinear top bound rig (Bind fc n b sc)

 187 |     = findLinear top (S bound) rig sc

 188 | findLinear top bound rig (As fc _ _ p)

 189 |     = findLinear top bound rig p

 190 | findLinear top bound rig tm

 191 |     = case getFnArgs tm of

 192 |            (Ref _ _ n, []) => pure []

 193 |            (Ref _ nt n, args)

 194 |               => do defs <- get Ctxt

 195 |                     Just nty <- lookupTyExact n (gamma defs)

 196 |                          | Nothing => pure []

 197 |                     findLinArg (accessible nt rig) !(nf defs Env.empty nty) args

 198 |            _ => pure []

 199 |     where

 200 |       accessible : NameType -> RigCount -> RigCount

 201 |       accessible Func r = if top then r else erased

 202 |       accessible _ r = r

 204 |       findLinArg : {vars : _} ->

 205 |                    RigCount -> ClosedNF -> List (Term vars) ->

 206 |                    Core (List (Name, RigCount))

 207 |       findLinArg rig ty@(NBind _ _ (Pi _ c _ _) _) (As fc u a p :: as)

 208 |           = if isLinear c

 209 |                then case u of

 210 |                          UseLeft => findLinArg rig ty (p :: as)

 211 |                          UseRight => findLinArg rig ty (a :: as)

 212 |                else pure $ !(findLinArg rig ty [a]) ++ !(findLinArg rig ty (p :: as))

 213 |       findLinArg rig (NBind _ x (Pi _ c _ _) sc) (Local {name=a} fc _ idx prf :: as)

 214 |           = do defs <- get Ctxt

 215 |                let a = nameAt prf

 216 |                if idx < bound

 217 |                  then do sc' <- sc defs (toClosure defaultOpts Env.empty (Ref fc Bound x))

 218 |                          pure $ (a, rigMult c rig) ::

 219 |                                     !(findLinArg rig sc' as)

 220 |                  else do sc' <- sc defs (toClosure defaultOpts Env.empty (Ref fc Bound x))

 221 |                          findLinArg rig sc' as

 222 |       findLinArg rig (NBind fc x (Pi _ c _ _) sc) (a :: as)

 223 |           = do defs <- get Ctxt

 224 |                pure $ !(findLinear False bound (c |*| rig) a) ++

 225 |                       !(findLinArg rig !(sc defs (toClosure defaultOpts Env.empty (Ref fc Bound x))) as)

 226 |       findLinArg rig ty (a :: as)

 227 |           = pure $ !(findLinear False bound rig a) ++ !(findLinArg rig ty as)

 228 |       findLinArg _ _ [] = pure []

 230 | setLinear : List (Name, RigCount) -> Term vars -> Term vars

 231 | setLinear vs tm@(Bind fc x b sc)

 232 |     = if isPatternBinder b

 233 |          then let b' = maybe b (setMultiplicity b) (lookup x vs)

 234 |                in Bind fc x b' (setLinear vs sc)

 235 |          else tm

 236 |   where

 237 |     isPatternBinder : Binder a -> Bool

 238 |     isPatternBinder (PVar {}) = True

 239 |     isPatternBinder (PVTy {}) = True

 240 |     isPatternBinder (PLet {}) = True

 241 |     isPatternBinder _ = False

 242 | setLinear vs tm = tm

 248 | combineLinear : FC -> List (Name, RigCount) ->

 249 |                 Core (List (Name, RigCount))

 250 | combineLinear loc [] = pure []

 251 | combineLinear loc ((n, count) :: cs)

 252 |     = case lookupAll n cs of

 253 |            [] => pure $ (n, count) :: !(combineLinear loc cs)

 254 |            counts => do count' <- combineAll count counts

 255 |                         pure $ (n, count') ::

 256 |                                !(combineLinear loc (filter notN cs))

 257 |   where

 258 |     notN : (Name, RigCount) -> Bool

 259 |     notN (n', _) = n /= n'

 261 |     lookupAll : Name -> List (Name, RigCount) -> List RigCount

 262 |     lookupAll n [] = []

 263 |     lookupAll n ((n', c) :: cs)

 264 |        = if n == n' then c :: lookupAll n cs else lookupAll n cs

 266 |     -- Those combine rules are obtuse enough that they are worth investigating

 267 |     combine : RigCount -> RigCount -> Core RigCount

 268 |     combine l r = if l |+| r == top && not (isErased $ l `glb` r) && (l `glb` r) /= top

 269 |                      then throw (LinearUsed loc 2 n)

 270 |                      -- if everything is fine, return the linearity that has the

 271 |                      -- highest bound

 272 |                      else pure (l `lub` r)

 274 |     combineAll : RigCount -> List RigCount -> Core RigCount

 275 |     combineAll c [] = pure c

 276 |     combineAll c (c' :: cs)

 277 |         = do newc <- combine c c'

 278 |              combineAll newc cs

 280 | export -- also used by Transforms

 281 | checkLHS : {vars : _} ->

 282 |            {auto c : Ref Ctxt Defs} ->

 283 |            {auto m : Ref MD Metadata} ->

 284 |            {auto u : Ref UST UState} ->

 285 |            {auto s : Ref Syn SyntaxInfo} ->

 286 |            {auto o : Ref ROpts REPLOpts} ->

 287 |            Bool -> -- in transform

 288 |            (mult : RigCount) ->

 289 |            Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->

 290 |            FC -> RawImp ->

 291 |            Core (RawImp, -- checked LHS with implicits added

 292 |                  (vars' ** (Thin vars vars',

 293 |                            Env Term vars', NestedNames vars',

 294 |                            Term vars', Term vars')))

 295 | checkLHS {vars} trans mult n opts nest env fc lhs_in

 296 |     = do defs <- get Ctxt

 297 |          logRaw "declare.def.lhs" 30 "Raw LHS: " lhs_in

 298 |          lhs_raw <- if trans

 299 |                        then pure lhs_in

 300 |                        else lhsInCurrentNS nest lhs_in

 301 |          logRaw "declare.def.lhs" 30 "Raw LHS in current NS: " lhs_raw

 303 |          autoimp <- isUnboundImplicits

 304 |          setUnboundImplicits True

 305 |          (_, lhs_bound) <- bindNames False lhs_raw

 306 |          setUnboundImplicits autoimp

 307 |          logRaw "declare.def.lhs" 30 "Raw LHS with implicits bound" lhs_bound

 309 |          lhs <- if trans

 310 |                    then pure lhs_bound

 311 |                    else implicitsAs n defs vars lhs_bound

 313 |          logC "declare.def.lhs" 5 $ do pure $ "Checking LHS of " ++ show !(getFullName (Resolved n))

 316 |          log "declare.def.lhs" 10 $ show lhs

 317 |          logEnv "declare.def.lhs" 5 "In env" env

 318 |          let lhsMode = if trans

 319 |                           then InTransform

 320 |                           else InLHS mult

 321 |          (lhstm, lhstyg) <-

 322 |              wrapErrorC opts (InLHS fc !(getFullName (Resolved n))) $

 323 |                      elabTerm n lhsMode opts nest env

 324 |                                 (IBindHere fc PATTERN lhs) Nothing

 325 |          logTerm "declare.def.lhs" 5 "Checked LHS term" lhstm

 326 |          lhsty <- getTerm lhstyg

 328 |          defs <- get Ctxt

 329 |          let lhsenv = letToLam env

 330 |          -- we used to fully normalise the LHS, to make sure fromInteger

 331 |          -- patterns were allowed, but now they're fully normalised anyway

 332 |          -- so we only need to do the holes. If there's a lot of type level

 333 |          -- computation, this is a huge saving!

 334 |          lhstm <- normaliseHoles defs lhsenv lhstm

 335 |          lhsty <- normaliseHoles defs env lhsty

 336 |          linvars_in <- findLinear True 0 linear lhstm

 337 |          logTerm "declare.def.lhs" 10 "Checked LHS term after normalise" lhstm

 338 |          log "declare.def.lhs" 5 $ "Linearity of names in " ++ show n ++ ": " ++

 339 |                  show linvars_in

 341 |          linvars <- combineLinear fc linvars_in

 342 |          let lhstm_lin = setLinear linvars lhstm

 343 |          let lhsty_lin = setLinear linvars lhsty

 345 |          logTerm "declare.def.lhs" 3 "LHS term" lhstm_lin

 346 |          logTerm "declare.def.lhs" 5 "LHS type" lhsty_lin

 347 |          setHoleLHS (bindEnv fc env lhstm_lin)

 349 |          ext <- extendEnv env Refl nest lhstm_lin lhsty_lin

 350 |          pure (lhs, ext)

 357 | hasEmptyPat : {vars : _} ->

 358 |               {auto c : Ref Ctxt Defs} ->

 359 |               Defs -> Env Term vars -> Term vars -> Core Bool

 360 | hasEmptyPat defs env (Bind fc x b sc)

 361 |    = pure $ !(isEmpty defs env !(nf defs env (binderType b)))

 362 |             || !(hasEmptyPat defs (b :: env) sc)

 363 | hasEmptyPat defs env _ = pure False

 366 | applyEnv : {vars : _} ->

 367 |            {auto c : Ref Ctxt Defs} ->

 368 |            Env Term vars -> Name ->

 369 |            Core (Name, (Maybe Name, List (Var vars), FC -> NameType -> Term vars))

 370 | applyEnv env withname

 371 |     = do n' <- resolveName withname

 372 |          pure (withname, (Just withname, reverse (allVarsNoLet env),

 373 |                   \fc, nt => applyTo fc

 374 |                          (Ref fc nt (Resolved n')) env))

 379 | checkClause : {vars : _} ->

 380 |               {auto c : Ref Ctxt Defs} ->

 381 |               {auto m : Ref MD Metadata} ->

 382 |               {auto u : Ref UST UState} ->

 383 |               {auto s : Ref Syn SyntaxInfo} ->

 384 |               {auto o : Ref ROpts REPLOpts} ->

 385 |               (mult : RigCount) -> (vis : Visibility) ->

 386 |               (totreq : TotalReq) -> (hashit : Bool) ->

 387 |               Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->

 388 |               ImpClause -> Core (Either RawImp Clause)

 389 | checkClause mult vis totreq hashit n opts nest env (ImpossibleClause fc lhs)

 390 |     = do lhs_raw <- lhsInCurrentNS nest lhs

 391 |          handleUnify

 392 |            (do autoimp <- isUnboundImplicits

 393 |                setUnboundImplicits True

 394 |                (_, lhs) <- bindNames False lhs_raw

 395 |                setUnboundImplicits autoimp

 397 |                log "declare.def.clause.impossible" 5 $ "Checking " ++ show lhs

 398 |                logEnv "declare.def.clause.impossible" 5 "In env" env

 399 |                (lhstm, lhstyg) <-

 400 |                            elabTerm n (InLHS mult) opts nest env

 401 |                                       (IBindHere fc COVERAGE lhs) Nothing

 402 |                defs <- get Ctxt

 403 |                lhs <- normaliseHoles defs env lhstm

 404 |                if !(hasEmptyPat defs env lhs)

 405 |                   then pure (Left lhs_raw)

 406 |                   else throw (ValidCase fc env (Left lhs)))

 407 |            (\err =>

 408 |               case err of

 409 |                    ValidCase {} => throw err

 410 |                    _ => do defs <- get Ctxt

 411 |                            if !(impossibleErrOK defs err)

 412 |                               then pure (Left lhs_raw)

 413 |                               else throw (ValidCase fc env (Right err)))

 414 | checkClause {vars} mult vis totreq hashit n opts nest env (PatClause fc lhs_in rhs)

 415 |     = do (_, (vars'  ** (sub', env', nest', lhstm', lhsty'))) <-

 416 |              checkLHS False mult n opts nest env fc lhs_in

 417 |          let rhsMode = if isErased mult then InType else InExpr

 418 |          log "declare.def.clause" 5 $ "Checking RHS " ++ show rhs

 419 |          logEnv "declare.def.clause" 5 "In env" env'

 421 |          rhstm <- logTime 3 ("Check RHS " ++ show fc) $

 422 |                     wrapErrorC opts (InRHS fc !(getFullName (Resolved n))) $

 423 |                        checkTermSub n rhsMode opts nest' env' env sub' rhs (gnf env' lhsty')

 424 |          clearHoleLHS

 426 |          logTerm "declare.def.clause" 3 "RHS term" rhstm

 427 |          when hashit $

 428 |            do addHashWithNames lhstm'

 429 |               addHashWithNames rhstm

 430 |               log "module.hash" 15 "Adding hash for def."

 432 |          -- If the rhs is a hole, record the lhs in the metadata because we

 433 |          -- might want to split it interactively

 434 |          case rhstm of

 435 |               Meta {} =>

 436 |                  addLHS (getFC lhs_in) (length env) env' lhstm'

 437 |               _ => pure ()

 439 |          pure (Right (MkClause env' lhstm' rhstm))

 441 | checkClause {vars} mult vis totreq hashit n opts nest env

 442 |     (WithClause ifc lhs_in rig wval_raw mprf flags cs)

 443 |     = do (lhs, (vars'  ** (sub', env', nest', lhspat, reqty))) <-

 444 |              checkLHS False mult n opts nest env ifc lhs_in

 445 |          let wmode

 446 |                = if isErased mult || isErased rig then InType else InExpr

 448 |          (wval, gwvalTy) <- wrapErrorC opts (InRHS ifc !(getFullName (Resolved n))) $

 449 |                 elabTermSub n wmode opts nest' env' env sub' wval_raw Nothing

 450 |          clearHoleLHS

 452 |          logTerm "declare.def.clause.with" 5 "With value (at quantity \{show rig})" wval

 453 |          logTerm "declare.def.clause.with" 3 "Required type" reqty

 454 |          wvalTy <- getTerm gwvalTy

 455 |          defs <- get Ctxt

 456 |          wval <- normaliseHoles defs env' wval

 457 |          wvalTy <- normaliseHoles defs env' wvalTy

 459 |          let (wevars ** withSub) = keepOldEnv sub' (snd (findSubEnv env' wval))

 460 |          logTerm "declare.def.clause.with" 5 "With value type" wvalTy

 461 |          log "declare.def.clause.with" 5 $ "Using vars " ++ show wevars

 463 |          let Just wval = shrink wval withSub

 464 |              | Nothing => throw (InternalError "Impossible happened: With abstraction failure #1")

 465 |          let Just wvalTy = shrink wvalTy withSub

 466 |              | Nothing => throw (InternalError "Impossible happened: With abstraction failure #2")

 467 |          -- Should the env be normalised too? If the following 'impossible'

 468 |          -- error is ever thrown, that might be the cause!

 469 |          let Just wvalEnv = shrinkEnv env' withSub

 470 |              | Nothing => throw (InternalError "Impossible happened: With abstraction failure #3")

 472 |          -- Abstracting over 'wval' in the scope of bNotReq in order

 473 |          -- to get the 'magic with' behaviour

 474 |          (wargs ** (scenv, var, binder)) <- bindWithArgs rig wvalTy ((,wval) <$> mprf) wvalEnv

 476 |          let bnr = bindNotReq vfc 0 env' withSub [] reqty

 477 |          let notreqns = fst bnr

 478 |          let notreqty = snd bnr

 480 |          rdefs <- if Syntactic `elem` flags

 481 |                      then clearDefs defs

 482 |                      else pure defs

 483 |          wtyScope <- replace rdefs scenv !(nf rdefs scenv (weakenNs (mkSizeOf wargs) wval))

 484 |                             var

 485 |                             !(nf rdefs scenv

 486 |                                  (weakenNs (mkSizeOf wargs) notreqty))

 487 |          let bNotReq = binder wtyScope

 489 |          -- The environment has some implicit and some explcit args, potentially,

 490 |          -- which is inconvenient since we have to know which is which when

 491 |          -- elaborating the application of the rhs function. So it's easier

 492 |          -- if we just make them all explicit - this type isn't visible to

 493 |          -- users anyway!

 494 |          let env' = mkExplicit env'

 496 |          let Just (reqns, envns, wtype) = bindReq vfc env' withSub [] bNotReq

 497 |              | Nothing => throw (InternalError "Impossible happened: With abstraction failure #4")

 499 |          -- list of argument names - 'Just' means we need to match the name

 500 |          -- in the with clauses to find out what the pattern should be.

 501 |          -- 'Nothing' means it's the with pattern (so wargn)

 502 |          let wargNames

 503 |                  = map Just reqns ++

 504 |                    Nothing :: map Just notreqns

 506 |          logTerm "declare.def.clause.with" 3 "With function type" wtype

 507 |          log "declare.def.clause.with" 5 $ "Argument names " ++ show wargNames

 509 |          wname <- genWithName !(prettyName !(toFullNames (Resolved n)))

 510 |          widx <- addDef wname ({flags $= (SetTotal totreq ::)}

 511 |                                     (newDef vfc wname (if isErased mult then erased else top)

 512 |                                       vars wtype (specified vis) None))

 514 |          let toWarg : Maybe (PiInfo RawImp, Name) -> List (Maybe Name, RawImp)

 515 |                := flip maybe (\pn => [(Nothing, IVar vfc (snd pn))]) $

 516 |                     (Nothing, wval_raw) ::

 517 |                     case mprf of

 518 |                       Nothing => []

 519 |                       Just _  =>

 520 |                        let fc = emptyFC in

 521 |                        let refl = IVar fc (NS builtinNS (UN $ Basic "Refl")) in

 522 |                        [(map snd mprf, INamedApp fc refl (UN $ Basic "x") wval_raw)]

 524 |          let rhs_in = gapply (IVar vfc wname)

 525 |                     $ map (\ nm => (Nothing, IVar vfc nm)) envns

 526 |                    ++ concatMap toWarg wargNames

 528 |          log "declare.def.clause.with" 3 $ "Applying to with argument " ++ show rhs_in

 529 |          rhs <- wrapErrorC opts (InRHS ifc !(getFullName (Resolved n))) $

 530 |              checkTermSub n wmode opts nest' env' env sub' rhs_in

 531 |                           (gnf env' reqty)

 533 |          -- Generate new clauses by rewriting the matched arguments

 534 |          cs' <- traverse (mkClauseWith 1 wname wargNames lhs) cs

 535 |          log "declare.def.clause.with" 3 $ "With clauses: " ++ show cs'

 537 |          -- Elaborate the new definition here

 538 |          nestname <- applyEnv env wname

 539 |          let nest'' = { names $= (nestname ::) } nest

 541 |          let wdef = IDef ifc wname cs'

 542 |          processDecl [] nest'' env wdef

 544 |          pure (Right (MkClause env' lhspat rhs))

 545 |   where

 546 |     vfc : FC

 547 |     vfc = virtualiseFC ifc

 549 |     bindWithArgs :

 550 |        (rig : RigCount) -> (wvalTy : Term xs) -> Maybe ((RigCount, Name), Term xs) ->

 551 |        (wvalEnv : Env Term xs) ->

 552 |        Core (ext : Scope

 553 |          ** ( Env Term (ext ++ xs)

 554 |             , Term (ext ++ xs)

 555 |             , (Term (ext ++ xs) -> Term xs)

 556 |             ))

 557 |     bindWithArgs {xs} rig wvalTy Nothing wvalEnv =

 558 |       let wargn : Name

 559 |           wargn = MN "warg" 0

 560 |           wargs : Scope

 561 |           wargs = [wargn]

 563 |           scenv : Env Term (wargs ++ xs)

 564 |                 := Pi vfc top Explicit wvalTy :: wvalEnv

 566 |           var : Term (wargs ++ xs)

 567 |               := Local vfc (Just False) Z First

 569 |           binder : Term (wargs ++ xs) -> Term xs

 570 |                  := Bind vfc wargn (Pi vfc rig Explicit wvalTy)

 572 |       in pure (wargs ** (scenv, var, binder))

 574 |     bindWithArgs {xs} rig wvalTy (Just ((rigPrf, name), wval)) wvalEnv = do

 575 |       defs <- get Ctxt

 577 |       let eqName = NS builtinNS (UN $ Basic "Equal")

 578 |       Just (TCon ar _ _ _ _ _ _) <- lookupDefExact eqName (gamma defs)

 579 |         | _ => throw (InternalError "Cannot find builtin Equal")

 580 |       let eqTyCon = Ref vfc (TyCon ar) !(toResolvedNames eqName)

 582 |       let wargn : Name

 583 |           wargn = MN "warg" 0

 584 |           wargs : Scope

 585 |           wargs = [name, wargn]

 587 |           wvalTy' := weaken wvalTy

 588 |           eqTy : Term (MN "warg" 0 :: xs)

 589 |                := apply vfc eqTyCon

 590 |                            [ wvalTy'

 591 |                            , wvalTy'

 592 |                            , weaken wval

 593 |                            , Local vfc (Just False) Z First

 594 |                            ]

 596 |           scenv : Env Term (wargs ++ xs)

 597 |                 := Pi vfc top Implicit eqTy

 598 |                 :: Pi vfc top Explicit wvalTy

 599 |                 :: wvalEnv

 601 |           var : Term (wargs ++ xs)

 602 |               := Local vfc (Just False) (S Z) (Later First)

 604 |           binder : Term (wargs ++ xs) -> Term xs

 605 |                  := \ t => Bind vfc wargn (Pi vfc rig Explicit wvalTy)

 606 |                          $ Bind vfc name  (Pi vfc rigPrf Implicit eqTy) t

 608 |       pure (wargs ** (scenv, var, binder))

 610 |     -- If it's 'Keep/Refl' in 'outprf', that means it was in the outer

 611 |     -- environment so we need to keep it in the same place in the 'with'

 612 |     -- function. Hence, turn it to Keep whatever

 613 |     keepOldEnv : {0 outer : _} -> {vs : _} ->

 614 |                  (outprf : Thin outer vs) -> Thin vs' vs ->

 615 |                  (vs'' : Scope ** Thin vs'' vs)

 616 |     keepOldEnv {vs} Refl p = (vs ** Refl)

 617 |     keepOldEnv {vs} p Refl = (vs ** Refl)

 618 |     keepOldEnv (Drop p) (Drop p')

 619 |         = let (_ ** rest) = keepOldEnv p p' in

 620 |               (_ ** Drop rest)

 621 |     keepOldEnv (Drop p) (Keep p')

 622 |         = let (_ ** rest) = keepOldEnv p p' in

 623 |               (_ ** Keep rest)

 624 |     keepOldEnv (Keep p) (Drop p')

 625 |         = let (_ ** rest) = keepOldEnv p p' in

 626 |               (_ ** Keep rest)

 627 |     keepOldEnv (Keep p) (Keep p')

 628 |         = let (_ ** rest) = keepOldEnv p p' in

 629 |               (_ ** Keep rest)

 631 |     -- Rewrite the clauses in the block to use an updated LHS.

 632 |     -- 'drop' is the number of additional with arguments we expect

 633 |     -- (i.e. the things to drop from the end before matching LHSs)

 634 |     mkClauseWith : (drop : Nat) -> Name ->

 635 |                    List (Maybe (PiInfo RawImp, Name)) ->

 636 |                    RawImp -> ImpClause ->

 637 |                    Core ImpClause

 638 |     mkClauseWith drop wname wargnames lhs (PatClause ploc patlhs rhs)

 639 |         = do log "declare.def.clause.with" 20 "PatClause"

 640 |              newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs

 641 |              newrhs <- withRHS ploc drop wname wargnames rhs lhs

 642 |              pure (PatClause ploc newlhs newrhs)

 643 |     mkClauseWith drop wname wargnames lhs (WithClause ploc patlhs rig wval prf flags ws)

 644 |         = do log "declare.def.clause.with" 20 "WithClause"

 645 |              newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs

 646 |              newwval <- withRHS ploc drop wname wargnames wval lhs

 647 |              ws' <- traverse (mkClauseWith (S drop) wname wargnames lhs) ws

 648 |              pure (WithClause ploc newlhs rig newwval prf flags ws')

 649 |     mkClauseWith drop wname wargnames lhs (ImpossibleClause ploc patlhs)

 650 |         = do log "declare.def.clause.with" 20 "ImpossibleClause"

 651 |              newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs

 652 |              pure (ImpossibleClause ploc newlhs)

 656 | calcRefs : {auto c : Ref Ctxt Defs} ->

 657 |            (runtime : Bool) -> (aTotal : Name) -> (fn : Name) -> Core ()

 658 | calcRefs rt at fn

 659 |     = do defs <- get Ctxt

 660 |          Just gdef <- lookupCtxtExact fn (gamma defs)

 661 |               | _ => pure ()

 662 |          let PMDef r cargs tree_ct tree_rt pats = definition gdef

 663 |               | _ => pure () -- not a function definition

 664 |          let refs : Maybe (NameMap Bool)

 665 |                   = if rt then refersToRuntimeM gdef else refersToM gdef

 666 |          let Nothing = refs

 667 |               | Just _ => pure () -- already done

 668 |          let tree : CaseTree cargs = if rt then tree_rt else tree_ct

 669 |          let metas = CaseTree.getMetas tree

 670 |          traverse_ addToSave (keys metas)

 671 |          let refs_all = addRefs at metas tree

 672 |          refs <- ifThenElse rt

 673 |                     (dropErased (keys refs_all) refs_all)

 674 |                     (pure refs_all)

 675 |          ignore $ ifThenElse rt

 676 |             (addDef fn ({ refersToRuntimeM := Just refs } gdef))

 677 |             (addDef fn ({ refersToM := Just refs } gdef))

 678 |          traverse_ (calcRefs rt at) (keys refs)

 679 |   where

 680 |     dropErased : List Name -> NameMap Bool -> Core (NameMap Bool)

 681 |     dropErased [] refs = pure refs

 682 |     dropErased (n :: ns) refs

 683 |         = do defs <- get Ctxt

 684 |              Just gdef <- lookupCtxtExact n (gamma defs)

 685 |                   | Nothing => dropErased ns refs

 686 |              if multiplicity gdef /= erased

 687 |                 then dropErased ns refs

 688 |                 else dropErased ns (delete n refs)

 691 | mkRunTime : {auto c : Ref Ctxt Defs} ->

 692 |             {auto m : Ref MD Metadata} ->

 693 |             {auto u : Ref UST UState} ->

 694 |             {auto s : Ref Syn SyntaxInfo} ->

 695 |             {auto o : Ref ROpts REPLOpts} ->

 696 |             FC -> Name -> Core ()

 697 | mkRunTime fc n

 698 |     = do logC "compile.casetree" 5 $ do pure $ "Making run time definition for " ++ show !(toFullNames n)

 699 |          defs <- get Ctxt

 700 |          Just gdef <- lookupCtxtExact n (gamma defs)

 701 |               | _ => pure ()

 702 |          let cov = gdef.totality.isCovering

 703 |          -- If it's erased at run time, don't build the tree

 704 |          when (not (isErased $ multiplicity gdef)) $ do

 705 |            let PMDef r cargs tree_ct _ pats = definition gdef

 706 |                 | _ => pure () -- not a function definition

 707 |            let ty = type gdef

 708 |            -- Prepare RHS of definitions, by erasing 0-multiplicities, and

 709 |            -- finding any applications to specialise (partially evaluate)

 710 |            pats' <- traverse (toErased (location gdef) (getSpec (flags gdef)))

 711 |                              pats

 713 |            let clauses_init = map (toClause (location gdef)) pats'

 714 |            clauses <- case cov of

 715 |                            MissingCases _ => do log "compile.casetree.missing" 5 $ "Adding uncovered error to \{show clauses_init}"

 716 |                                                 pure $ addErrorCase clauses_init

 717 |                            _ => pure clauses_init

 719 |            (rargs ** (tree_rt, _)) <- getPMDef (location gdef) RunTime n ty clauses

 720 |            logC "compile.casetree" 5 $ do

 721 |              tree_rt <- toFullNames tree_rt

 722 |              pure $ unlines

 723 |                [ show cov ++ ":"

 724 |                , "Runtime tree for " ++ show (fullname gdef) ++ ":"

 725 |                , show (indent 2 $ prettyTree tree_rt)

 726 |                ]

 727 |            log "compile.casetree" 10 $ show tree_rt

 728 |            log "compile.casetree.measure" 15 $ show (measure tree_rt)

 730 |            let Just Refl = scopeEq cargs rargs

 731 |                    | Nothing => throw (InternalError "WAT")

 732 |            ignore $ addDef n $

 733 |                        { definition := PMDef r rargs tree_ct tree_rt pats

 734 |                        } gdef

 735 |            -- If it's a case block, and not already set as inlinable or forced

 736 |            -- to not be inlinable, check if it's safe to inline

 737 |            when (caseName !(toFullNames n) && noInline (flags gdef)) $

 738 |              do inl <- canInlineCaseBlock n

 739 |                 when inl $ do

 740 |                   logC "compiler.inline.eval" 5 $ do pure "Marking \{show !(toFullNames n)} for inlining in runtime case tree."

 741 |                   setFlag fc n Inline

 742 |   where

 743 |     -- check if the flags contain explicit inline or noinline directives:

 744 |     noInline : List DefFlag -> Bool

 745 |     noInline (Inline :: _)   = False

 746 |     noInline (NoInline :: _) = False

 747 |     noInline (x :: xs) = noInline xs

 748 |     noInline _ = True

 750 |     caseName : Name -> Bool

 751 |     caseName (CaseBlock {}) = True

 752 |     caseName (NS _ n) = caseName n

 753 |     caseName _ = False

 755 |     mkCrash : {vars : _} -> String -> Term vars

 756 |     mkCrash msg

 757 |        = apply fc (Ref fc Func (UN $ Basic "prim__crash"))

 758 |                [Erased fc Placeholder, PrimVal fc (Str msg)]

 760 |     matchAny : Term vars -> Term vars

 761 |     matchAny (App fc f a) = App fc (matchAny f) (Erased fc Placeholder)

 762 |     matchAny tm = tm

 764 |     makeErrorClause : {vars : _} -> Env Term vars -> Term vars -> Clause

 765 |     makeErrorClause env lhs

 766 |         = MkClause env (matchAny lhs)

 767 |              (mkCrash ("Unhandled input for " ++ show n ++ " at " ++ show fc))

 769 |     addErrorCase : List Clause -> List Clause

 770 |     addErrorCase [] = []

 771 |     addErrorCase [MkClause env lhs rhs]

 772 |         = MkClause env lhs rhs :: makeErrorClause env lhs :: []

 773 |     addErrorCase (x :: xs) = x :: addErrorCase xs

 775 |     getSpec : List DefFlag -> Maybe (List (Name, Nat))

 776 |     getSpec [] = Nothing

 777 |     getSpec (PartialEval n :: _) = Just n

 778 |     getSpec (x :: xs) = getSpec xs

 780 |     toErased : FC -> Maybe (List (Name, Nat)) ->

 781 |                (vars ** (Env Term vars, Term vars, Term vars)) ->

 782 |                Core (vars ** (Env Term vars, Term vars, Term vars))

 783 |     toErased fc spec (_ ** (env, lhs, rhs))

 784 |         = do lhs_erased <- linearCheck fc linear True env lhs

 785 |              -- Partially evaluate RHS here, where appropriate

 786 |              rhs' <- applyTransforms env rhs

 787 |              rhs' <- applySpecialise env spec rhs'

 788 |              rhs_erased <- linearCheck fc linear True env rhs'

 789 |              pure (_ ** (env, lhs_erased, rhs_erased))

 791 |     toClause : FC -> (vars ** (Env Term vars, Term vars, Term vars)) -> Clause

 792 |     toClause fc (_ ** (env, lhs, rhs))

 793 |         = MkClause env lhs rhs

 795 | compileRunTime : {auto c : Ref Ctxt Defs} ->

 796 |                  {auto m : Ref MD Metadata} ->

 797 |                  {auto u : Ref UST UState} ->

 798 |                  {auto s : Ref Syn SyntaxInfo} ->

 799 |                  {auto o : Ref ROpts REPLOpts} ->

 800 |                  FC -> Name -> Core ()

 801 | compileRunTime fc atotal

 802 |     = do defs <- get Ctxt

 803 |          traverse_ (mkRunTime fc) (toCompileCase defs)

 804 |          traverse_ (calcRefs True atotal) (toCompileCase defs)

 806 |          update Ctxt { toCompileCase := [] }

 808 | toPats : Clause -> (vs ** (Env Term vs, Term vs, Term vs))

 809 | toPats (MkClause {vars} env lhs rhs)

 810 |     = (_ ** (env, lhs, rhs))

 812 | warnUnreachable : {auto c : Ref Ctxt Defs} ->

 813 |                   Clause -> Core ()

 814 | warnUnreachable (MkClause env lhs rhs)

 815 |     = recordWarning (UnreachableClause (getLoc lhs) env lhs)

 817 | isAlias : RawImp -> Maybe ((FC, Name)              -- head symbol

 818 |                           , List (FC, (FC, Name))) -- pattern variables

 819 | isAlias lhs

 820 |   = do let (hd, apps) = getFnArgs lhs []

 821 |        hd <- isIVar hd

 822 |        args <- traverse (isExplicit >=> bitraverse pure isIBindVar) apps

 823 |        pure (hd, args)

 825 | lookupOrAddAlias : {vars : _} ->

 826 |                    {auto m : Ref MD Metadata} ->

 827 |                    {auto c : Ref Ctxt Defs} ->

 828 |                    {auto u : Ref UST UState} ->

 829 |                    {auto s : Ref Syn SyntaxInfo} ->

 830 |                    {auto o : Ref ROpts REPLOpts} ->

 831 |                    List ElabOpt -> NestedNames vars -> Env Term vars -> FC ->

 832 |                    Name -> List ImpClause -> Core (Maybe GlobalDef)

 833 | lookupOrAddAlias eopts nest env fc n [cl@(PatClause _ lhs _)]

 834 |   = do defs <- get Ctxt

 835 |        log "declare.def.alias" 20 $ "Looking at \{show cl}"

 836 |        Nothing <- lookupCtxtExact n (gamma defs)

 837 |          | Just gdef => pure (Just gdef)

 838 |        -- No prior declaration:

 839 |        --   1) check whether it has the shape of an alias

 840 |        let Just (hd, args) = isAlias lhs

 841 |          | Nothing => pure Nothing

 842 |        --   2) check whether it could be a misspelling

 843 |        log "declare.def" 5 $

 844 |          "Missing type declaration for the alias "

 845 |          ++ show n

 846 |          ++ ". Checking first whether it is a misspelling."

 847 |        [] <- do -- get the candidates

 848 |                 Just (str, kept) <- getSimilarNames n

 849 |                    | Nothing => pure []

 850 |                 -- only keep the ones that haven't been defined yet

 851 |                 decls <- for kept $ \ (cand, vis, weight) => do

 852 |                     Just gdef <- lookupCtxtExact cand (gamma defs)

 853 |                       | Nothing => pure Nothing -- should be impossible

 854 |                     let None = definition gdef

 855 |                       | _ => pure Nothing

 856 |                     pure (Just (cand, vis, weight))

 857 |                 pure $ showSimilarNames (currentNS defs) n str $ catMaybes decls

 858 |           | (x :: xs) => throw (MaybeMisspelling (NoDeclaration fc n) (x ::: xs))

 859 |        --   3) declare an alias

 860 |        log "declare.def" 5 "Not a misspelling: go ahead and declare it!"

 861 |        processType eopts nest env fc top Public []

 862 |           -- See #3409

 863 |           $ Mk [fc, MkFCVal fc n] $ holeyType (map snd args)

 864 |        defs <- get Ctxt

 865 |        lookupCtxtExact n (gamma defs)

 867 |   where

 868 |     holeyType : List (FC, Name) -> RawImp

 869 |     holeyType [] = Implicit fc False

 870 |     holeyType ((xfc, x) :: xs)

 871 |       = let xfc = virtualiseFC xfc in

 872 |         IPi xfc top Explicit (Just x) (Implicit xfc False)

 873 |       $ holeyType xs

 875 | lookupOrAddAlias _ _ _ fc n _

 876 |   = do defs <- get Ctxt

 877 |        lookupCtxtExact n (gamma defs)

 880 | processDef : {vars : _} ->

 881 |              {auto c : Ref Ctxt Defs} ->

 882 |              {auto m : Ref MD Metadata} ->

 883 |              {auto u : Ref UST UState} ->

 884 |              {auto s : Ref Syn SyntaxInfo} ->

 885 |              {auto o : Ref ROpts REPLOpts} ->

 886 |              List ElabOpt -> NestedNames vars -> Env Term vars -> FC ->

 887 |              Name -> List ImpClause -> Core ()

 888 | processDef opts nest env fc n_in cs_in

 889 |   = do n <- inCurrentNS n_in

 890 |        withDefStacked n $ do

 891 |          defs <- get Ctxt

 892 |          Just gdef <- lookupOrAddAlias opts nest env fc n cs_in

 893 |            | Nothing => noDeclaration fc n

 894 |          let None = definition gdef

 895 |               | _ => throw (AlreadyDefined fc n)

 896 |          let ty = type gdef

 897 |          -- a module's interface hash (what determines when the module has changed)

 898 |          -- should include the definition (RHS) of anything that is public (available

 899 |          -- at compile time for elaboration) _or_ inlined (dropped into destination definitions

 900 |          -- during compilation).

 901 |          let hashit = (collapseDefault $ visibility gdef) == Public || (Inline `elem` gdef.flags)

 902 |          let mult = if isErased (multiplicity gdef)

 903 |                        then erased

 904 |                        else linear

 905 |          nidx <- resolveName n

 907 |          -- Dynamically rebind default totality requirement to this function's totality requirement

 908 |          -- and use this requirement when processing `with` blocks

 909 |          log "declare.def" 5 $ "Traversing clauses of " ++ show n ++ " with mult " ++ show mult

 910 |          let treq = fromMaybe !getDefaultTotalityOption (findSetTotal (flags gdef))

 911 |          cs <- withTotality treq $

 912 |                traverse (checkClause mult (collapseDefault $ visibility gdef) treq

 913 |                                      hashit nidx opts nest env) cs_in

 915 |          let pats = map toPats (rights cs)

 917 |          (cargs ** (tree_ct, unreachable)) <-

 918 |              logTime 3 ("Building compile time case tree for " ++ show n) $

 919 |                 getPMDef fc (CompileTime mult) n ty (rights cs)

 921 |          traverse_ warnUnreachable unreachable

 923 |          logC "declare.def" 2 $

 924 |                  do t <- toFullNames tree_ct

 925 |                     pure ("Case tree for " ++ show n ++ ": " ++ show t)

 927 |          -- check whether the name was declared in a different source file

 928 |          defs <- get Ctxt

 929 |          let pi = case lookup n (userHoles defs) of

 930 |                         Nothing => defaultPI

 931 |                         Just e => { externalDecl := e } defaultPI

 932 |          -- Add compile time tree as a placeholder for the runtime tree,

 933 |          -- but we'll rebuild that in a later pass once all the case

 934 |          -- blocks etc are resolved

 935 |          ignore $ addDef (Resolved nidx)

 936 |                   ({ definition := PMDef pi cargs tree_ct tree_ct pats

 937 |                    } gdef)

 939 |          when (collapseDefault (visibility gdef) == Public) $

 940 |              do let rmetas = getMetas tree_ct

 941 |                 log "declare.def" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys rmetas)

 942 |                 traverse_ addToSave (keys rmetas)

 943 |          when (isUserName n && collapseDefault (visibility gdef) /= Private) $

 944 |              do let tymetas = getMetas (type gdef)

 945 |                 traverse_ addToSave (keys tymetas)

 946 |          addToSave n

 948 |          -- Flag this name as one which needs compiling

 949 |          update Ctxt { toCompileCase $= (n ::) }

 951 |          atotal <- toResolvedNames (NS builtinNS (UN $ Basic "assert_total"))

 952 |          logTime 3 ("Building size change graphs " ++ show n) $

 953 |            when (not (InCase `elem` opts)) $

 954 |              do calcRefs False atotal (Resolved nidx)

 955 |                 sc <- calculateSizeChange fc n

 956 |                 setSizeChange fc n sc

 957 |                 checkIfGuarded fc n

 959 |          md <- get MD -- don't need the metadata collected on the coverage check

 961 |          cov <- logTime 3 ("Checking Coverage " ++ show n) $ checkCoverage nidx ty mult cs

 962 |          setCovering fc n cov