0 | module Core.Case.CaseBuilder
   1 |
   2 | import Core.Case.CaseTree
   3 | import Core.Case.Util
   4 | import Core.Context.Log
   5 | import Core.Env
   6 | import Core.Normalise
   7 | import Core.Options
   8 | import Core.Value
   9 |
  10 | import Idris.Pretty.Annotations
  11 |
  12 | import Data.DPair
  13 | import Data.List.Quantifiers
  14 | import Data.SortedSet
  15 | import Data.String
  16 | import Data.Vect
  17 | import Libraries.Data.IMaybe
  18 | import Libraries.Data.List.SizeOf
  19 | import Libraries.Data.List.LengthMatch
  20 | import Libraries.Data.List01
  21 | import Libraries.Data.List01.Quantifiers
  22 |
  23 | import Decidable.Equality
  24 |
  25 | import Libraries.Text.PrettyPrint.Prettyprinter
  26 |
  27 | %default covering
  28 |
  29 | %hide Symbols.equals
  30 |
  31 | public export
  32 | data Phase = CompileTime RigCount | RunTime
  33 |
  34 | Eq Phase where
  35 |   CompileTime r == CompileTime r' = r == r'
  36 |   RunTime == RunTime = True
  37 |   _ == _ = False
  38 |
  39 | data ArgType : Scoped where
  40 |      Known : RigCount -> (ty : Term vars) -> ArgType vars -- arg has type 'ty'
  41 |      Stuck : (fty : Term vars) -> ArgType vars
  42 |          -- ^ arg will have argument type of 'fty' when we know enough to
  43 |          -- calculate it
  44 |      Unknown : ArgType vars
  45 |          -- arg's type is not yet known due to a previously stuck argument
  46 |
  47 | HasNames (ArgType vars) where
  48 |   full gam (Known c ty) = Known c <$> full gam ty
  49 |   full gam (Stuck ty) = Stuck <$> full gam ty
  50 |   full gam Unknown = pure Unknown
  51 |
  52 |   resolved gam (Known c ty) = Known c <$> resolved gam ty
  53 |   resolved gam (Stuck ty) = Stuck <$> resolved gam ty
  54 |   resolved gam Unknown = pure Unknown
  55 |
  56 | covering
  57 | {ns : _} -> Show (ArgType ns) where
  58 |   show (Known c t) = "Known " ++ show c ++ " " ++ show t
  59 |   show (Stuck t) = "Stuck " ++ show t
  60 |   show Unknown = "Unknown"
  61 |
  62 | record PatInfo (pvar : Name) (vars : Scope) where
  63 |   constructor MkInfo
  64 |   {idx : Nat}
  65 |   {name : Name}
  66 |   pat : Pat
  67 |   0 loc : IsVar name idx vars
  68 |   argType : ArgType vars -- Type of the argument being inspected (i.e.
  69 |                          -- *not* refined by this particular pattern)
  70 |
  71 | covering
  72 | {vars : _} -> Show (PatInfo n vars) where
  73 |   show pi = show (pat pi) ++ " : " ++ show (argType pi)
  74 |
  75 | HasNames (PatInfo n vars) where
  76 |   full gam (MkInfo pat loc argType)
  77 |      = do pat <- full gam pat
  78 |           argType <- full gam argType
  79 |           pure $ MkInfo pat loc argType
  80 |
  81 |   resolved gam (MkInfo pat loc argType)
  82 |      = do pat <- resolved gam pat
  83 |           argType <- resolved gam argType
  84 |           pure $ MkInfo pat loc argType
  85 |
  86 | {-
  87 | NamedPats is a list of patterns on the LHS of a clause. Each entry in
  88 | the list gives a pattern, and a proof that there is a variable we can
  89 | inspect to see if it matches the pattern.
  90 |
  91 | A definition consists of a list of clauses, which are a 'NamedPats' and
  92 | a term on the RHS. There is an assumption that corresponding positions in
  93 | NamedPats always have the same 'Elem' proof, though this isn't expressed in
  94 | a type anywhere.
  95 | -}
  96 |
  97 | data NamedPats : List Name -> -- the pattern variables still to process, in order
  98 |                  Scoped where
  99 |      Nil : NamedPats [] vars
 100 |      (::) : PatInfo pvar vars ->
 101 |             -- ^ a pattern, where its variable appears in the vars list,
 102 |             -- and its type. The type has no variable names; any names it
 103 |             -- refers to are explicit
 104 |             NamedPats ns vars -> NamedPats (pvar :: ns) vars
 105 |
 106 | getPatInfo : NamedPats todo vars -> List Pat
 107 | getPatInfo [] = []
 108 | getPatInfo (x :: xs) = pat x :: getPatInfo xs
 109 |
 110 | updatePats : {vars, todo : _} ->
 111 |              {auto c : Ref Ctxt Defs} ->
 112 |              Env Term vars ->
 113 |              NF vars -> NamedPats todo vars -> Core (NamedPats todo vars)
 114 | updatePats env nf [] = pure []
 115 | updatePats {todo = pvar :: ns} env (NBind fc _ (Pi _ c _ farg) fsc) (p :: ps)
 116 |   = case argType p of
 117 |          Unknown =>
 118 |             do defs <- get Ctxt
 119 |                empty <- clearDefs defs
 120 |                pure ({ argType := Known c !(quote empty env farg) } p
 121 |                           :: !(updatePats env !(fsc defs (toClosure defaultOpts env (Ref fc Bound pvar))) ps))
 122 |          _ => pure (p :: ps)
 123 | updatePats env nf (p :: ps)
 124 |   = case argType p of
 125 |          Unknown =>
 126 |             do defs <- get Ctxt
 127 |                empty <- clearDefs defs
 128 |                pure ({ argType := Stuck !(quote empty env nf) } p :: ps)
 129 |          _ => pure (p :: ps)
 130 |
 131 | substInPatInfo : {pvar, vars, todo : _} ->
 132 |                  {auto c : Ref Ctxt Defs} ->
 133 |                  FC -> Name -> Term vars -> PatInfo pvar vars ->
 134 |                  NamedPats todo vars ->
 135 |                  Core (PatInfo pvar vars, NamedPats todo vars)
 136 | substInPatInfo fc n tm p ps
 137 |     = case argType p of
 138 |            Known c ty =>
 139 |                 do defs <- get Ctxt
 140 |                    tynf <- nf defs (mkEnv fc vars) ty
 141 |                    case tynf of
 142 |                         NApp {} =>
 143 |                            pure ({ argType := Known c (substName n tm ty) } p, ps)
 144 |                         -- Got a concrete type, and that's all we need, so stop
 145 |                         _ => pure (p, ps)
 146 |            Stuck fty =>
 147 |              do defs <- get Ctxt
 148 |                 empty <- clearDefs defs
 149 |                 let env = mkEnv fc vars
 150 |                 case !(nf defs env (substName n tm fty)) of
 151 |                      NBind pfc _ (Pi _ c _ farg) fsc =>
 152 |                        pure ({ argType := Known c !(quote empty env farg) } p,
 153 |                                  !(updatePats env
 154 |                                        !(fsc defs (toClosure defaultOpts env
 155 |                                              (Ref pfc Bound pvar))) ps))
 156 |                      _ => pure (p, ps)
 157 |            Unknown => pure (p, ps)
 158 |
 159 | -- Substitute the name with a term in the pattern types, and reduce further
 160 | -- (this aims to resolve any 'Stuck' pattern types)
 161 | substInPats : {vars, todo : _} ->
 162 |               {auto c : Ref Ctxt Defs} ->
 163 |               FC -> Name -> Term vars -> NamedPats todo vars ->
 164 |               Core (NamedPats todo vars)
 165 | substInPats fc n tm [] = pure []
 166 | substInPats fc n tm (p :: ps)
 167 |     = do (p', ps') <- substInPatInfo fc n tm p ps
 168 |          pure (p' :: !(substInPats fc n tm ps'))
 169 |
 170 | getPat : {idx : Nat} ->
 171 |          (0 el : IsVar nm idx ps) -> NamedPats ps ns -> PatInfo nm ns
 172 | getPat First (x :: xs) = x
 173 | getPat (Later p) (x :: xs) = getPat p xs
 174 |
 175 | dropPat : {idx : Nat} ->
 176 |           (0 el : IsVar nm idx ps) ->
 177 |           NamedPats ps ns -> NamedPats (dropIsVar ps el) ns
 178 | dropPat First (x :: xs) = xs
 179 | dropPat (Later p) (x :: xs) = x :: dropPat p xs
 180 |
 181 | HasNames (NamedPats todo vars) where
 182 |   full gam [] = pure []
 183 |   full gam (x::xs) = [| (::) (full gam x) (full gam xs) |]
 184 |
 185 |   resolved gam [] = pure []
 186 |   resolved gam (x::xs) = [| (::) (resolved gam x) (resolved gam xs) |]
 187 |
 188 | covering
 189 | {vars : _} -> {todo : _} -> Show (NamedPats todo vars) where
 190 |   show xs = "[" ++ showAll xs ++ "]"
 191 |     where
 192 |       showAll : {vs, ts : _} -> NamedPats ts vs -> String
 193 |       showAll [] = ""
 194 |       showAll {ts = t :: _} [x]
 195 |           = show t ++ " " ++ show (pat x) ++ " [" ++ show (argType x) ++ "]"
 196 |       showAll {ts = t :: _} (x :: xs)
 197 |           = show t ++ " " ++ show (pat x) ++ " [" ++ show (argType x) ++ "]"
 198 |                      ++ ", " ++ showAll xs
 199 |
 200 | {vars : _} -> {todo : _} -> Pretty IdrisSyntax (NamedPats todo vars) where
 201 |   pretty xs = hsep $ prettyAll xs
 202 |     where
 203 |       prettyAll : {vs, ts : _} -> NamedPats ts vs -> List (Doc IdrisSyntax)
 204 |       prettyAll [] = []
 205 |       prettyAll {ts = t :: _} (x :: xs)
 206 |           = parens (pretty0 t <++> equals <++> pretty (pat x))
 207 |           :: prettyAll xs
 208 |
 209 | Weaken ArgType where
 210 |   weaken (Known c ty) = Known c (weaken ty)
 211 |   weaken (Stuck fty) = Stuck (weaken fty)
 212 |   weaken Unknown = Unknown
 213 |
 214 |   weakenNs s (Known c ty) = Known c (weakenNs s ty)
 215 |   weakenNs s (Stuck fty) = Stuck (weakenNs s fty)
 216 |   weakenNs s Unknown = Unknown
 217 |
 218 | Weaken (PatInfo p) where
 219 |   weakenNs s (MkInfo p el fty) = MkInfo p (weakenIsVar s el) (weakenNs s fty)
 220 |
 221 | Weaken (NamedPats todo) where
 222 |   weaken [] = []
 223 |   weaken (p :: ps) = weaken p :: weaken ps
 224 |
 225 |   weakenNs ns [] = []
 226 |   weakenNs ns (p :: ps) = weakenNs ns p :: weakenNs ns ps
 227 |
 228 | (++) : NamedPats ms vars -> NamedPats ns vars -> NamedPats (ms ++ ns) vars
 229 | (++) [] ys = ys
 230 | (++) (x :: xs) ys = x :: xs ++ ys
 231 |
 232 | tail : NamedPats (p :: ps) vars -> NamedPats ps vars
 233 | tail (x :: xs) = xs
 234 |
 235 | data PatClause : (todo : List Name) -> Scoped where
 236 |      MkPatClause : List Name -> -- names matched so far (from original lhs)
 237 |                    NamedPats todo vars ->
 238 |                    Int -> (rhs : Term vars) -> PatClause todo vars
 239 |
 240 | getNPs : PatClause todo vars -> NamedPats todo vars
 241 | getNPs (MkPatClause _ lhs pid rhs) = lhs
 242 |
 243 | covering
 244 | {vars : _} -> {todo : _} -> Show (PatClause todo vars) where
 245 |   show (MkPatClause _ ps pid rhs)
 246 |      = show ps ++ " => " ++ show rhs
 247 |
 248 | {vars : _} -> {todo : _} -> Pretty IdrisSyntax (PatClause todo vars) where
 249 |   pretty (MkPatClause _ ps _ rhs)
 250 |      = pretty ps <++> fatArrow <++> byShow rhs
 251 |
 252 | HasNames (PatClause todo vars) where
 253 |   full gam (MkPatClause ns nps i rhs)
 254 |      = [| MkPatClause (traverse (full gam) ns) (full gam nps) (pure i) (full gam rhs) |]
 255 |
 256 |   resolved gam (MkPatClause ns nps i rhs)
 257 |      = [| MkPatClause (traverse (resolved gam) ns) (resolved gam nps) (pure i) (resolved gam rhs) |]
 258 |
 259 | 0 IsConClause : PatClause (a :: todo) vars -> Type
 260 | IsConClause (MkPatClause _ (MkInfo pat _ _ :: _) _ _) = IsConPat pat
 261 |
 262 | substInClause : {a, vars, todo : _} ->
 263 |                 {auto c : Ref Ctxt Defs} ->
 264 |                 FC -> Subset (PatClause (a :: todo) vars) IsConClause ->
 265 |                 Core (Subset (PatClause (a :: todo) vars) IsConClause)
 266 | substInClause fc (Element (MkPatClause pvars (MkInfo pat pprf fty :: pats) pid rhs) isCons)
 267 |     = do pats' <- substInPats fc a (mkTerm vars pat) pats
 268 |          pure $ Element (MkPatClause pvars (MkInfo pat pprf fty :: pats') pid rhs) isCons
 269 |
 270 | data Partitions : List01 ne (PatClause (a :: todo) vars) -> Type where
 271 |      ConClauses : {a, todo, vars : _} ->
 272 |                   {ps : List01 ne   (PatClause (a :: todo) vars)} ->
 273 |                   (cs : List01 True (PatClause (a :: todo) vars )) ->
 274 |                   (0 isCons : All IsConClause cs) =>
 275 |                   Partitions ps -> Partitions (cs ++ ps)
 276 |      VarClauses : {a, todo, vars : _} ->
 277 |                   {ps : List01 ne   (PatClause (a :: todo) vars)} ->
 278 |                   (vs : List01 True (PatClause (a :: todo) vars)) ->
 279 |                   Partitions ps -> Partitions (vs ++ ps)
 280 |      NoClauses : Partitions []
 281 |
 282 | covering
 283 | {ps : _} -> Show (Partitions ps) where
 284 |   show (ConClauses cs rest)
 285 |     = unlines ("CON" :: map (("  " ++) . show) (forget cs))
 286 |     ++ "\n, " ++ show rest
 287 |   show (VarClauses vs rest)
 288 |     = unlines ("VAR" :: map (("  " ++) . show) (forget vs))
 289 |     ++ "\n, " ++ show rest
 290 |   show NoClauses = "NONE"
 291 |
 292 | data ClauseType : PatClause (a :: todo) vars -> Type where
 293 |      ConClause : (0 isCon : IsConClause p) => ClauseType p
 294 |      VarClause : ClauseType p
 295 |
 296 | namesIn : List Name -> Pat -> Bool
 297 | namesIn pvars (PAs _ n p) = (n `elem` pvars) && namesIn pvars p
 298 | namesIn pvars (PCon _ _ _ _ ps) = all (namesIn pvars) ps
 299 | namesIn pvars (PTyCon _ _ _ ps) = all (namesIn pvars) ps
 300 | namesIn pvars (PArrow _ _ s t) = namesIn pvars s && namesIn pvars t
 301 | namesIn pvars (PDelay _ _ t p) = namesIn pvars t && namesIn pvars p
 302 | namesIn pvars (PLoc _ n) = n `elem` pvars
 303 | namesIn pvars _ = True
 304 |
 305 | namesFrom : Pat -> List Name
 306 | namesFrom (PAs _ n p) = n :: namesFrom p
 307 | namesFrom (PCon _ _ _ _ ps) = concatMap namesFrom ps
 308 | namesFrom (PTyCon _ _ _ ps) = concatMap namesFrom ps
 309 | namesFrom (PArrow _ _ s t) = namesFrom s ++ namesFrom t
 310 | namesFrom (PDelay _ _ t p) = namesFrom t ++ namesFrom p
 311 | namesFrom (PLoc _ n) = [n]
 312 | namesFrom _ = []
 313 |
 314 | clauseType : Phase -> (p : PatClause (a :: as) vars) -> ClauseType p
 315 | -- If it's irrelevant, a constructor, and there's no names we haven't seen yet
 316 | -- and don't see later, treat it as a variable
 317 | -- Or, if we're compiling for runtime we won't be able to split on it, so
 318 | -- also treat it as a variable
 319 | -- Or, if it's an under-applied constructor then do NOT attempt to split on it!
 320 | clauseType phase (MkPatClause pvars (MkInfo arg _ ty :: rest) pid rhs)
 321 |     = maybe VarClause (\isCon => ConClause @{isCon}) $ getClauseType phase arg ty
 322 |   where
 323 |     -- used when we are tempted to split on a constructor: is
 324 |     -- this actually a fully applied one?
 325 |     splitCon : Nat -> List Pat -> Maybe (So True)
 326 |     splitCon arity xs = toMaybe (arity == length xs) Oh
 327 |
 328 |     -- used to get the remaining clause types
 329 |     clauseType' : (p : Pat) -> Maybe (IsConPat p)
 330 |     clauseType' (PCon _ _ _ a xs) = splitCon a xs
 331 |     clauseType' (PTyCon _ _ a xs) = splitCon a xs
 332 |     clauseType' (PConst _ x)      = Just Oh
 333 |     clauseType' (PArrow _ _ s t)  = Just Oh
 334 |     clauseType' (PDelay {})       = Just Oh
 335 |     clauseType' _                 = Nothing
 336 |
 337 |     getClauseType : Phase -> (p : Pat) -> ArgType vars -> Maybe (IsConPat p)
 338 |     getClauseType (CompileTime cr) (PCon _ _ _ a xs) (Known r t)
 339 |         = if (isErased r && not (isErased cr) &&
 340 |              all (namesIn (pvars ++ concatMap namesFrom (getPatInfo rest))) xs)
 341 |              then Nothing
 342 |              else splitCon a xs
 343 |     getClauseType phase (PAs _ _ p) t = getClauseType phase p t
 344 |     getClauseType phase l (Known r t) = if isErased r
 345 |       then Nothing
 346 |       else clauseType' l
 347 |     getClauseType phase l _ = clauseType' l
 348 |
 349 | partition : {a, as, vars : _} ->
 350 |             Phase -> (ps : List01 ne (PatClause (a :: as) vars)) -> Partitions ps
 351 | partition phase [] = NoClauses
 352 | partition phase (x :: xs) with (partition phase xs)
 353 |   partition phase (x :: .(cs ++ ps)) | (ConClauses cs rest)
 354 |         = case clauseType phase x of
 355 |                ConClause => ConClauses (x :: cs) rest
 356 |                VarClause => VarClauses [x] (ConClauses cs rest)
 357 |   partition phase (x :: .(vs ++ ps)) | (VarClauses vs rest)
 358 |         = case clauseType phase x of
 359 |                ConClause => ConClauses [x] (VarClauses vs rest)
 360 |                VarClause => VarClauses (x :: vs) rest
 361 |   partition phase [x] | NoClauses
 362 |         = case clauseType phase x of
 363 |                ConClause => ConClauses [x] NoClauses
 364 |                VarClause => VarClauses [x] NoClauses
 365 |
 366 | data ConType : Type where
 367 |      CName : Name -> (tag : Int) -> ConType
 368 |      CDelay : ConType
 369 |      CConst : Constant -> ConType
 370 |
 371 | data Group : List Name -> -- pattern variables still to process
 372 |              Scoped where
 373 |      ConGroup : {newargs : _} ->
 374 |                 Name -> (tag : Int) ->
 375 |                 List01 True (PatClause (newargs ++ todo) (newargs ++ vars)) ->
 376 |                 Group todo vars
 377 |      DelayGroup : {tyarg, valarg : _} ->
 378 |                   List01 True (PatClause (tyarg :: valarg :: todo)
 379 |                                          (tyarg :: valarg :: vars)) ->
 380 |                   Group todo vars
 381 |      ConstGroup : Constant -> List01 True (PatClause todo vars) ->
 382 |                   Group todo vars
 383 |
 384 | covering
 385 | {vars : _} -> {todo : _} -> Show (Group todo vars) where
 386 |   show (ConGroup c t cs) = "Con " ++ show c ++ ": " ++ show cs
 387 |   show (DelayGroup cs) = "Delay: " ++ show cs
 388 |   show (ConstGroup c cs) = "Const " ++ show c ++ ": " ++ show cs
 389 |
 390 | data GroupMatch : ConType -> List Pat -> Group todo vars -> Type where
 391 |      ConMatch : {tag : Int} -> LengthMatch ps newargs ->
 392 |                 GroupMatch (CName n tag) ps
 393 |                   (ConGroup {newargs} n tag (MkPatClause pvs pats pid rhs :: rest))
 394 |      DelayMatch : GroupMatch CDelay []
 395 |                     (DelayGroup {tyarg} {valarg} (MkPatClause pvs pats pid rhs :: rest))
 396 |      ConstMatch : GroupMatch (CConst c) []
 397 |                     (ConstGroup c (MkPatClause pvs pats pid rhs :: rest))
 398 |      NoMatch : GroupMatch ct ps g
 399 |
 400 | checkGroupMatch : (c : ConType) -> (ps : List Pat) -> (g : Group todo vars) ->
 401 |                   GroupMatch c ps g
 402 | checkGroupMatch (CName x tag) ps (ConGroup {newargs} x' tag' (MkPatClause pvs pats pid rhs :: rest))
 403 |     = case checkLengthMatch ps newargs of
 404 |            Nothing => NoMatch
 405 |            Just prf => case (nameEq x x', decEq tag tag') of
 406 |                             (Just Refl, Yes Refl) => ConMatch prf
 407 |                             _ => NoMatch
 408 | checkGroupMatch (CName x tag) ps _ = NoMatch
 409 | checkGroupMatch CDelay [] (DelayGroup (MkPatClause pvs pats pid rhs :: rest))
 410 |     = DelayMatch
 411 | checkGroupMatch (CConst c) [] (ConstGroup c' (MkPatClause pvs pats pid rhs :: rest))
 412 |     = case constantEq c c' of
 413 |            Nothing => NoMatch
 414 |            Just Refl => ConstMatch
 415 | checkGroupMatch _ _ _ = NoMatch
 416 |
 417 | data PName : Type where
 418 |
 419 | nextName : {auto i : Ref PName Int} ->
 420 |            String -> Core Name
 421 | nextName root
 422 |     = do x <- get PName
 423 |          put PName (x + 1)
 424 |          pure (MN root x)
 425 |
 426 | nextNames : {vars : _} ->
 427 |             {auto i : Ref PName Int} ->
 428 |             {auto c : Ref Ctxt Defs} ->
 429 |             FC -> String -> List Pat -> Maybe (NF vars) ->
 430 |             Core (args ** (SizeOf args, NamedPats args (args ++ vars)))
 431 | nextNames fc root [] fty = pure ([] ** (zero, []))
 432 | nextNames fc root (p :: pats) fty
 433 |      = do defs <- get Ctxt
 434 |           empty <- clearDefs defs
 435 |           n <- nextName root
 436 |           let env = mkEnv fc vars
 437 |           fa_tys <- the (Core (Maybe (NF vars), ArgType vars)) $
 438 |               case fty of
 439 |                    Nothing => pure (Nothing, Unknown)
 440 |                    Just (NBind pfc _ (Pi _ c _ fargc) fsc) =>
 441 |                       do farg <- evalClosure defs fargc
 442 |                          case farg of
 443 |                               NErased {} =>
 444 |                                 pure (Just !(fsc defs (toClosure defaultOpts env (Ref pfc Bound n))),
 445 |                                       Unknown)
 446 |                               _ => pure (Just !(fsc defs (toClosure defaultOpts env (Ref pfc Bound n))),
 447 |                                          Known c !(quote empty env farg))
 448 |                    Just t =>
 449 |                       pure (Nothing, Stuck !(quote empty env t))
 450 |           (args ** (l, ps)) <- nextNames fc root pats (fst fa_tys)
 451 |           let argTy = case snd fa_tys of
 452 |                            Unknown => Unknown
 453 |                            Known rig t => Known rig (weakenNs (suc l) t)
 454 |                            Stuck t => Stuck (weakenNs (suc l) t)
 455 |           pure (n :: args ** (suc l, MkInfo p First argTy :: weaken ps))
 456 |
 457 | -- replace the prefix of patterns with 'pargs'
 458 | newPats : (pargs : List Pat) -> LengthMatch pargs ns ->
 459 |           NamedPats (ns ++ todo) vars ->
 460 |           NamedPats ns vars
 461 | newPats [] NilMatch rest = []
 462 | newPats (newpat :: xs) (ConsMatch w) (pi :: rest)
 463 |   = { pat := newpat } pi :: newPats xs w rest
 464 |
 465 | updateNames : List (Name, Pat) -> List (Name, Name)
 466 | updateNames = mapMaybe update
 467 |   where
 468 |     update : (Name, Pat) -> Maybe (Name, Name)
 469 |     update (n, PLoc fc p) = Just (p, n)
 470 |     update _ = Nothing
 471 |
 472 | updatePatNames : List (Name, Name) -> NamedPats todo vars -> NamedPats todo vars
 473 | updatePatNames _ [] = []
 474 | updatePatNames ns (pi :: ps)
 475 |     = { pat $= update } pi :: updatePatNames ns ps
 476 |   where
 477 |     update : Pat -> Pat
 478 |     update (PAs fc n p)
 479 |         = case lookup n ns of
 480 |                Nothing => PAs fc n (update p)
 481 |                Just n' => PAs fc n' (update p)
 482 |     update (PCon fc n i a ps) = PCon fc n i a (map update ps)
 483 |     update (PTyCon fc n a ps) = PTyCon fc n a (map update ps)
 484 |     update (PArrow fc x s t) = PArrow fc x (update s) (update t)
 485 |     update (PDelay fc r t p) = PDelay fc r (update t) (update p)
 486 |     update (PLoc fc n)
 487 |         = case lookup n ns of
 488 |                Nothing => PLoc fc n
 489 |                Just n' => PLoc fc n'
 490 |     update p = p
 491 |
 492 | groupCons : {a, vars, todo : _} ->
 493 |             {auto i : Ref PName Int} ->
 494 |             {auto ct : Ref Ctxt Defs} ->
 495 |             FC -> Name ->
 496 |             List Name ->
 497 |             (cs : List01 True (PatClause (a :: todo) vars)) ->
 498 |             (0 isCons : All IsConClause cs) =>
 499 |             Core (List01 True (Group todo vars))
 500 | groupCons fc fn pvars (x :: xs) {isCons = p :: ps}
 501 |     = foldlC (uncurry . gc) !(gc [] x p) $ pushIn xs ps
 502 |   where
 503 |     addConG : {vars', todo' : _} ->
 504 |               Name -> (tag : Int) ->
 505 |               List Pat -> NamedPats todo' vars' ->
 506 |               Int -> (rhs : Term vars') ->
 507 |               (acc : List01 ne (Group todo' vars')) ->
 508 |               Core (List01 True (Group todo' vars'))
 509 |     -- Group all the clauses that begin with the same constructor, and
 510 |     -- add new pattern arguments for each of that constructor's arguments.
 511 |     -- The type of 'ConGroup' ensures that we refer to the arguments by
 512 |     -- the same name in each of the clauses
 513 |     addConG n tag pargs pats pid rhs []
 514 |         = do cty <- if n == UN (Basic "->")
 515 |                       then pure $ NBind fc (MN "_" 0) (Pi fc top Explicit (MkNFClosure defaultOpts (mkEnv fc vars') (NType fc (MN "top" 0)))) $
 516 |                               (\d, a => pure $ NBind fc (MN "_" 1) (Pi fc top Explicit (MkNFClosure defaultOpts (mkEnv fc vars') (NErased fc Placeholder)))
 517 |                                 (\d, a => pure $ NType fc (MN "top" 0)))
 518 |                       else do defs <- get Ctxt
 519 |                               Just t <- lookupTyExact n (gamma defs)
 520 |                                    | Nothing => pure (NErased fc Placeholder)
 521 |                               nf defs (mkEnv fc vars') (embed t)
 522 |              (patnames ** (l, newargs)) <- nextNames fc "e" pargs (Just cty)
 523 |              -- Update non-linear names in remaining patterns (to keep
 524 |              -- explicit dependencies in types accurate)
 525 |              let pats' = updatePatNames (updateNames (zip patnames pargs))
 526 |                                         (weakenNs l pats)
 527 |              let clause = MkPatClause pvars (newargs ++ pats') pid (weakenNs l rhs)
 528 |              pure [ConGroup n tag [clause]]
 529 |     addConG n tag pargs pats pid rhs (g :: gs) with (checkGroupMatch (CName n tag) pargs g)
 530 |       addConG n tag pargs pats pid rhs
 531 |               (ConGroup n tag (MkPatClause pvars ps tid tm :: rest) :: gs) | ConMatch {newargs} lprf
 532 |         = do let newps = newPats pargs lprf ps
 533 |              let l = mkSizeOf newargs
 534 |              let pats' = updatePatNames (updateNames (zip newargs pargs))
 535 |                                         (weakenNs l pats)
 536 |              let newclause = MkPatClause pvars (newps ++ pats') pid (weakenNs l rhs)
 537 |              -- put the new clause at the end of the group, since we
 538 |              -- match the clauses top to bottom.
 539 |              pure $ ConGroup n tag (MkPatClause pvars ps tid tm :: rest ++ [newclause]) :: gs
 540 |       addConG n tag pargs pats pid rhs (g :: gs) | NoMatch
 541 |         = (g ::) <$> addConG n tag pargs pats pid rhs gs
 542 |
 543 |     -- This rather ugly special case is to deal with laziness, where Delay
 544 |     -- is like a constructor, but with a special meaning that it forces
 545 |     -- evaluation when case analysis reaches it (dealt with in the evaluator
 546 |     -- and compiler)
 547 |     addDelayG : {vars', todo' : _} ->
 548 |                 Pat -> Pat -> NamedPats todo' vars' ->
 549 |                 Int -> (rhs : Term vars') ->
 550 |                 (acc : List01 ne (Group todo' vars')) ->
 551 |                 Core (List01 True (Group todo' vars'))
 552 |     addDelayG pty parg pats pid rhs []
 553 |         = do let dty = NBind fc (MN "a" 0) (Pi fc erased Explicit (MkNFClosure defaultOpts (mkEnv fc vars') (NType fc (MN "top" 0)))) $
 554 |                         (\d, a =>
 555 |                             do a' <- evalClosure d a
 556 |                                pure (NBind fc (MN "x" 0) (Pi fc top Explicit a)
 557 |                                        (\dv, av => pure (NDelayed fc LUnknown a'))))
 558 |              ([tyname, argname] ** (l, newargs)) <- nextNames fc "e" [pty, parg]
 559 |                                                   (Just dty)
 560 |                 | _ => throw (InternalError "Error compiling Delay pattern match")
 561 |              let pats' = updatePatNames (updateNames [(tyname, pty),
 562 |                                                       (argname, parg)])
 563 |                                         (weakenNs l pats)
 564 |              let clause = MkPatClause pvars (newargs ++ pats') pid (weakenNs l rhs)
 565 |              pure [DelayGroup [clause]]
 566 |     addDelayG pty parg pats pid rhs (g :: gs) with (checkGroupMatch CDelay [] g)
 567 |       addDelayG pty parg pats pid rhs
 568 |           (DelayGroup (MkPatClause pvars ps tid tm :: rest) :: gs) | DelayMatch {tyarg} {valarg}
 569 |         = do let l = mkSizeOf [tyarg, valarg]
 570 |              let newps = newPats [pty, parg] (ConsMatch (ConsMatch NilMatch)) ps
 571 |              let pats' = updatePatNames (updateNames [(tyarg, pty),
 572 |                                                       (valarg, parg)])
 573 |                                         (weakenNs l pats)
 574 |              let newclause = MkPatClause pvars (newps ++ pats') pid (weakenNs l rhs)
 575 |              pure $ DelayGroup (MkPatClause pvars ps tid tm :: rest ++ [newclause]) :: gs
 576 |       addDelayG pty parg pats pid rhs (g :: gs) | NoMatch
 577 |         = (g ::) <$> addDelayG pty parg pats pid rhs gs
 578 |
 579 |     addConstG : {vars', todo' : _} ->
 580 |                 Constant -> NamedPats todo' vars' ->
 581 |                 Int -> (rhs : Term vars') ->
 582 |                 (acc : List01 ne (Group todo' vars')) ->
 583 |                 Core (List01 True (Group todo' vars'))
 584 |     addConstG c pats pid rhs []
 585 |           = pure [ConstGroup c [MkPatClause pvars pats pid rhs]]
 586 |     addConstG c pats pid rhs (g :: gs) with (checkGroupMatch (CConst c) [] g)
 587 |       addConstG c pats pid rhs
 588 |               (ConstGroup c (MkPatClause pvars ps tid tm :: rest) :: gs) | ConstMatch
 589 |         = do let newclause = MkPatClause pvars pats pid rhs
 590 |              pure $ ConstGroup c (MkPatClause pvars ps tid tm :: rest ++ [newclause]) :: gs
 591 |       addConstG c pats pid rhs (g :: gs) | NoMatch
 592 |         = (g ::) <$> addConstG c pats pid rhs gs
 593 |
 594 |     addGroup : {vars, todo, idx : _} ->
 595 |                (pat : Pat) -> (0 _ : IsConPat pat) =>
 596 |                (0 p : IsVar nm idx vars) ->
 597 |                NamedPats todo vars -> Int -> Term vars ->
 598 |                List01 ne (Group todo vars) ->
 599 |                Core (List01 True (Group todo vars))
 600 |     -- In 'As' replace the name on the RHS with a reference to the
 601 |     -- variable we're doing the case split on
 602 |     addGroup (PAs fc n p) pprf pats pid rhs acc
 603 |          = addGroup p pprf pats pid (substName n (Local fc (Just True) idx pprf) rhs) acc
 604 |     addGroup (PCon cfc n t a pargs) pprf pats pid rhs acc
 605 |          = if a == length pargs
 606 |               then addConG n t pargs pats pid rhs acc
 607 |               else throw (CaseCompile cfc fn (NotFullyApplied n))
 608 |     addGroup (PTyCon cfc n a pargs) pprf pats pid rhs acc
 609 |          = if a == length pargs
 610 |            then addConG n 0 pargs pats pid rhs acc
 611 |            else throw (CaseCompile cfc fn (NotFullyApplied n))
 612 |     addGroup (PArrow _ _ s t) pprf pats pid rhs acc
 613 |          = addConG (UN $ Basic "->") 0 [s, t] pats pid rhs acc
 614 |     -- Go inside the delay; we'll flag the case as needing to force its
 615 |     -- scrutinee (need to check in 'caseGroups below)
 616 |     addGroup (PDelay _ _ pty parg) pprf pats pid rhs acc
 617 |          = addDelayG pty parg pats pid rhs acc
 618 |     addGroup (PConst _ c) pprf pats pid rhs acc
 619 |          = addConstG c pats pid rhs acc
 620 |
 621 |     gc : {a, vars, todo : _} ->
 622 |          List01 ne (Group todo vars) ->
 623 |          (p : PatClause (a :: todo) vars) ->
 624 |          (0 _ : IsConClause p) ->
 625 |          Core (List01 True (Group todo vars))
 626 |     gc acc (MkPatClause _ (MkInfo pat pprf _ :: pats) pid rhs) isCon
 627 |         = addGroup pat pprf pats pid rhs acc
 628 |
 629 | getFirstPat : NamedPats (p :: ps) ns -> Pat
 630 | getFirstPat (p :: _) = pat p
 631 |
 632 | getFirstArgType : NamedPats (p :: ps) ns -> ArgType ns
 633 | getFirstArgType (p :: _) = argType p
 634 |
 635 | ||| Store scores alongside rows of named patterns. These scores are used to determine
 636 | ||| which column of patterns to switch on first. One score per column.
 637 | data ScoredPats : List Name -> Scoped where
 638 |      Scored : List01 True (NamedPats (p :: ps) ns) -> Vect (length (p :: ps)) Int -> ScoredPats (p :: ps) ns
 639 |
 640 | {ps : _} -> Show (ScoredPats ps ns) where
 641 |   show (Scored xs ys) = (show ps) ++ "//" ++ (show ys)
 642 |
 643 | zeroedScore : {ps : _} -> List01 True (NamedPats (p :: ps) ns) -> ScoredPats (p :: ps) ns
 644 | zeroedScore nps = Scored nps (replicate (S $ length ps) 0)
 645 |
 646 | ||| Helper to find a single highest scoring name (or none at all) while
 647 | ||| retaining the context of all names processed.
 648 | highScore : {prev : List Name} ->
 649 |             (names : Scope) ->
 650 |             (scores : Vect (length names) Int) ->
 651 |             (highVal : Int) ->
 652 |             (highIdx : (n ** NVar n (prev ++ names))) -> -- TODO should be `names <>< prev`
 653 |             (duped : Bool) ->
 654 |             Maybe (n ** NVar n (prev ++ names))
 655 | highScore [] [] high idx True = Nothing
 656 | highScore [] [] high idx False = Just idx
 657 | highScore (x :: xs) (y :: ys) high idx duped =
 658 |   let next = highScore {prev = prev `snoc` x} xs ys
 659 |       prf = appendAssociative prev [x] xs
 660 |   in  rewrite prf in
 661 |         case compare y high of
 662 |              LT => next high (rewrite sym $ prf in idx) duped
 663 |              EQ => next high (rewrite sym $ prf in idx) True
 664 |              GT => next y (x ** rewrite sym $ prf in weakenNVar (mkSizeOf prev) (MkNVar First)) False
 665 |
 666 | ||| Get the index of the highest scoring column if there is one.
 667 | ||| If no column has a higher score than all other columns then
 668 | ||| the result is Nothing indicating we need to apply more scoring
 669 | ||| to break the tie.
 670 | ||| Suggested heuristic application order: f, b, a.
 671 | highScoreIdx : {p : _} -> {ps : _} -> ScoredPats (p :: ps) ns -> Maybe (n ** NVar n (p :: ps))
 672 | highScoreIdx (Scored xs (y :: ys)) = highScore {prev = []} (p :: ps) (y :: ys) (y - 1) (p ** MkNVar First) False
 673 |
 674 | ||| Apply the penalty function to the head constructor's
 675 | ||| arity. Produces 0 for all non-head-constructors.
 676 | headConsPenalty : (penality : Nat -> Int) -> Pat -> Int
 677 | headConsPenalty p (PAs _ _ w)             = headConsPenalty p w
 678 | headConsPenalty p (PCon _ n _ arity pats) = p arity
 679 | headConsPenalty p (PTyCon _ _ arity _)    = p arity
 680 | headConsPenalty _ (PConst {})             = 0
 681 | headConsPenalty _ (PArrow {})             = 0
 682 | headConsPenalty p (PDelay _ _ _ w)        = headConsPenalty p w
 683 | headConsPenalty _ (PLoc {})               = 0
 684 | headConsPenalty _ (PUnmatchable {})       = 0
 685 |
 686 | splitColumn : (nps : List01 True (NamedPats (p :: ps) ns)) -> (Vect (length nps) (PatInfo p ns), List01 True (NamedPats ps ns))
 687 | splitColumn [(w :: ws)] = ([w], [ws])
 688 | splitColumn ((w :: ws) :: nps@(_ :: _)) = bimap (w ::) (ws ::) $ splitColumn nps
 689 |
 690 | ||| Apply the given function that scores a pattern to all patterns and then
 691 | ||| sum up the column scores and add to the ScoredPats passed in.
 692 | consScoreHeuristic : {ps : _} -> (scorePat : Pat -> Int) -> ScoredPats ps ns -> ScoredPats ps ns
 693 | consScoreHeuristic scorePat (Scored xs ys) =
 694 |   let columnScores = scoreColumns xs
 695 |       ys' = zipWith (+) ys columnScores
 696 |   in  Scored xs ys'
 697 |   where
 698 |     scoreColumns : {ps' : _} -> (nps : List01 True (NamedPats ps' ns)) -> Vect (length ps') Int
 699 |     scoreColumns {ps' = []} nps = []
 700 |     scoreColumns {ps' = w :: ws} nps =
 701 |       let (col, nps') = splitColumn nps
 702 |        in sum (scorePat . pat <$> col) :: scoreColumns nps'
 703 |
 704 | ||| Add 1 to each non-default pat in the first row.
 705 | ||| This favors constructive matching first and reduces tree depth on average.
 706 | heuristicF : {ps : _} -> ScoredPats (p :: ps) ns -> ScoredPats (p :: ps) ns
 707 | heuristicF (Scored (x :: xs) ys) =
 708 |   let columnScores = scores x
 709 |       ys' = zipWith (+) ys columnScores
 710 |   in  Scored (x :: xs) ys'
 711 |   where
 712 |     isBlank : Pat -> Bool
 713 |     isBlank (PLoc {}) = True
 714 |     isBlank _ = False
 715 |
 716 |     scores : NamedPats ps' ns' -> Vect (length ps') Int
 717 |     scores [] = []
 718 |     scores (y :: ys) = let score : Int = if isBlank (pat y) then 0 else 1
 719 |                        in  score :: scores ys
 720 |
 721 | ||| Subtract 1 from each column for each pat that represents a head constructor.
 722 | ||| This favors pats that produce less branching.
 723 | heuristicB : {ps : _} -> ScoredPats ps ns -> ScoredPats ps ns
 724 | heuristicB = consScoreHeuristic (headConsPenalty (\arity => if arity == 0 then 0 else -1))
 725 |
 726 | ||| Subtract the sum of the arities of constructors in each column.
 727 | heuristicA : {ps : _} -> ScoredPats ps ns -> ScoredPats ps ns
 728 | heuristicA = consScoreHeuristic (headConsPenalty (negate . cast))
 729 |
 730 | applyHeuristics : {p : _} ->
 731 |                   {ps : _} ->
 732 |                   ScoredPats (p :: ps) ns ->
 733 |                   List (ScoredPats (p :: ps) ns -> ScoredPats (p :: ps) ns) ->
 734 |                   Maybe (n ** NVar n (p :: ps))
 735 | applyHeuristics x [] = highScoreIdx x
 736 | applyHeuristics x (f :: fs) = highScoreIdx x <|> applyHeuristics (f x) fs
 737 |
 738 | ||| Based only on the heuristic-score of columns, get the index of
 739 | ||| the column that should be processed next.
 740 | |||
 741 | ||| The scoring is inspired by results from the paper:
 742 | ||| http://moscova.inria.fr/~maranget/papers/ml05e-maranget.pdf
 743 | nextIdxByScore : {p : _} ->
 744 |                  {ps : _} ->
 745 |                  (useHeuristics : Bool) ->
 746 |                  Phase ->
 747 |                  List01 True (NamedPats (p :: ps) ns) ->
 748 |                  (n ** NVar n (p :: ps))
 749 | nextIdxByScore False _ _            = (_ ** (MkNVar First))
 750 | nextIdxByScore _ (CompileTime _) _  = (_ ** (MkNVar First))
 751 | nextIdxByScore True RunTime xs      =
 752 |   fromMaybe (_ ** (MkNVar First)) $
 753 |     applyHeuristics (zeroedScore xs) [heuristicF, heuristicB, heuristicA]
 754 |
 755 | -- Check whether all the initial patterns have the same concrete, known
 756 | -- and matchable type, which is multiplicity > 0.
 757 | -- If so, it's okay to match on it
 758 | sameType : {ns : _} ->
 759 |            {auto c : Ref Ctxt Defs} ->
 760 |            FC -> Phase -> Name ->
 761 |            Env Term ns -> List01 ne (NamedPats (p :: ps) ns) ->
 762 |            Core ()
 763 | sameType fc phase fn env [] = pure ()
 764 | sameType {ns} fc phase fn env (p :: xs)
 765 |     = do defs <- get Ctxt
 766 |          case getFirstArgType p of
 767 |               Known _ t => sameTypeAs phase
 768 |                                       !(nf defs env t)
 769 |                                       (map getFirstArgType xs)
 770 |               ty => throw (CaseCompile fc fn DifferingTypes)
 771 |   where
 772 |     firstPat : NamedPats (np :: nps) ns -> Pat
 773 |     firstPat (pinf :: _) = pat pinf
 774 |
 775 |     headEq : NF ns -> NF ns -> Phase -> Bool
 776 |     headEq (NBind _ _ (Pi {}) _) (NBind _ _ (Pi {}) _) _ = True
 777 |     headEq (NTCon _ n _ _) (NTCon _ n' _ _) _ = n == n'
 778 |     headEq (NPrimVal _ c) (NPrimVal _ c') _ = c == c'
 779 |     headEq (NType {}) (NType {}) _ = True
 780 |     headEq (NApp _ (NRef _ n) _) (NApp _ (NRef _ n') _) RunTime = n == n'
 781 |     headEq (NErased _ (Dotted x)) y ph = headEq x y ph
 782 |     headEq x (NErased _ (Dotted y)) ph = headEq x y ph
 783 |     headEq (NErased {}) _ RunTime = True
 784 |     headEq _ (NErased {}) RunTime = True
 785 |     headEq _ _ _ = False
 786 |
 787 |     sameTypeAs : forall ne. Phase -> NF ns -> List01 ne (ArgType ns) -> Core ()
 788 |     sameTypeAs _ ty [] = pure ()
 789 |     sameTypeAs ph ty (Known r t :: xs) =
 790 |          do defs <- get Ctxt
 791 |             if headEq ty !(nf defs env t) phase
 792 |                then sameTypeAs ph ty xs
 793 |                else throw (CaseCompile fc fn DifferingTypes)
 794 |     sameTypeAs p ty _ = throw (CaseCompile fc fn DifferingTypes)
 795 |
 796 | -- Check whether all the initial patterns are the same, or are all a variable.
 797 | -- If so, we'll match it to refine later types and move on
 798 | samePat : List01 True (NamedPats (p :: ps) ns) -> Bool
 799 | samePat (pi :: xs)
 800 |     = samePatAs (dropAs (getFirstPat pi))
 801 |                 (map (dropAs . getFirstPat) xs)
 802 |   where
 803 |     dropAs : Pat -> Pat
 804 |     dropAs (PAs _ _ p) = p
 805 |     dropAs p = p
 806 |
 807 |     samePatAs : Pat -> List01 ne Pat -> Bool
 808 |     samePatAs p [] = True
 809 |     samePatAs (PTyCon fc n a args) (PTyCon _ n' _ _ :: ps)
 810 |         = n == n' && samePatAs (PTyCon fc n a args) ps
 811 |     samePatAs (PCon fc n t a args) (PCon _ n' t' _ _ :: ps)
 812 |         = n == n' && t == t' && samePatAs (PCon fc n t a args) ps
 813 |     samePatAs (PConst fc c) (PConst _ c' :: ps)
 814 |         = c == c' && samePatAs (PConst fc c) ps
 815 |     samePatAs (PArrow fc x s t) (PArrow _ _ s' t' :: ps)
 816 |         = samePatAs (PArrow fc x s t) ps
 817 |     samePatAs (PDelay fc r t p) (PDelay _ _ _ _ :: ps)
 818 |         = samePatAs (PDelay fc r t p) ps
 819 |     samePatAs (PLoc fc n) (PLoc _ _ :: ps) = samePatAs (PLoc fc n) ps
 820 |     samePatAs x y = False
 821 |
 822 | getScore : {ns : _} ->
 823 |            {auto c : Ref Ctxt Defs} ->
 824 |            FC -> Phase -> Name ->
 825 |            List01 True (NamedPats (p :: ps) ns) ->
 826 |            Core (Either CaseError ())
 827 | getScore fc phase name npss
 828 |     = catch (Right () <$ sameType fc phase name (mkEnv fc ns) npss)
 829 |             $ \case
 830 |               CaseCompile _ _ err => pure $ Left err
 831 |               err => throw err
 832 |
 833 | ||| Pick the leftmost matchable thing with all constructors in the
 834 | ||| same family, or all variables, or all the same type constructor.
 835 | pickNextViable : {p, ns, ps : _} ->
 836 |                  {auto c : Ref Ctxt Defs} ->
 837 |                  FC -> Phase -> Name -> List01 True (NamedPats (p :: ps) ns) ->
 838 |                  Core (n ** NVar n (p :: ps))
 839 | -- last possible variable
 840 | pickNextViable {ps = []} fc phase fn npss
 841 |     = if samePat npss
 842 |          then pure (_ ** MkNVar First)
 843 |          else do Right () <- getScore fc phase fn npss
 844 |                        | Left err => throw (CaseCompile fc fn err)
 845 |                  pure (_ ** MkNVar First)
 846 | pickNextViable {ps = q :: qs} fc phase fn npss
 847 |     = if samePat npss
 848 |          then pure (_ ** MkNVar First)
 849 |          else case !(getScore fc phase fn npss) of
 850 |                    Right () => pure (_ ** MkNVar First)
 851 |                    _ => do (_ ** MkNVar var) <- pickNextViable fc phase fn (map tail npss)
 852 |                            pure (_ ** MkNVar (Later var))
 853 |
 854 | moveFirst : {idx : Nat} -> (0 el : IsVar nm idx ps) -> NamedPats ps ns ->
 855 |             NamedPats (nm :: dropIsVar ps el) ns
 856 | moveFirst el nps = getPat el nps :: dropPat el nps
 857 |
 858 | shuffleVars : {idx : Nat} -> (0 el : IsVar nm idx todo) -> PatClause todo vars ->
 859 |               PatClause (nm :: dropIsVar todo el) vars
 860 | shuffleVars First orig@(MkPatClause pvars lhs pid rhs) = orig -- no-op
 861 | shuffleVars el (MkPatClause pvars lhs pid rhs)
 862 |     = MkPatClause pvars (moveFirst el lhs) pid rhs
 863 |
 864 | mutual
 865 |   {- 'PatClause' contains a list of patterns still to process (that's the
 866 |      "todo") and a right hand side with the variables we know about "vars".
 867 |      So "match" builds the remainder of the case tree for
 868 |      the unprocessed patterns. "err" is the tree for when the patterns don't
 869 |      cover the input (i.e. the "fallthrough" pattern, which at the top
 870 |      level will be an error). -}
 871 |   match : {vars, todo : _} ->
 872 |           {auto i : Ref PName Int} ->
 873 |           {auto c : Ref Ctxt Defs} ->
 874 |           FC -> Name -> Phase ->
 875 |           List01 True (PatClause todo vars) ->
 876 |           IMaybe ne (CaseTree vars) ->
 877 |           Core (CaseTree vars)
 878 |   -- Before 'partition', reorder the arguments so that the one we
 879 |   -- inspect next has a concrete type that is the same in all cases, and
 880 |   -- has the most distinct constructors (via pickNextViable)
 881 |   match {todo = _ :: _} fc fn phase clauses err
 882 |       = do let nps = getNPs <$> clauses
 883 |            let (_ ** (MkNVar next)) = nextIdxByScore (caseTreeHeuristics !getSession) phase nps
 884 |            let prioritizedClauses = shuffleVars next <$> clauses
 885 |            (n ** MkNVar next') <- pickNextViable fc phase fn (getNPs <$> prioritizedClauses)
 886 |            log "compile.casetree.pick" 25 $ "Picked " ++ show n ++ " as the next split"
 887 |            let clauses' = shuffleVars next' <$> prioritizedClauses
 888 |            log "compile.casetree.clauses" 25 $
 889 |              unlines ("Using clauses:" :: map (("  " ++) . show) (forget clauses'))
 890 |            let ps = partition phase clauses'
 891 |            log "compile.casetree.partition" 25 $ "Got Partition:\n" ++ show ps
 892 |            Just mix <- mixture fc fn phase ps err
 893 |            log "compile.casetree.intermediate" 25 $ "match: new case tree " ++ show mix
 894 |            pure mix
 895 |   match {todo = []} fc fn phase (MkPatClause pvars [] pid (Erased _ Impossible) :: _) err
 896 |        = pure Impossible
 897 |   match {todo = []} fc fn phase (MkPatClause pvars [] pid rhs :: _) err
 898 |        = pure $ STerm pid rhs
 899 |
 900 |   caseGroups : {pvar, vars, todo : _} ->
 901 |                {auto i : Ref PName Int} ->
 902 |                {auto c : Ref Ctxt Defs} ->
 903 |                FC -> Name -> Phase ->
 904 |                {idx : Nat} -> (0 p : IsVar pvar idx vars) -> Term vars ->
 905 |                List01 True (Group todo vars) -> IMaybe ne (CaseTree vars) ->
 906 |                Core (CaseTree vars)
 907 |   caseGroups fc fn phase el ty gs errorCase
 908 |       = Case idx el (resolveNames vars ty) <$> altGroups gs
 909 |     where
 910 |       altGroups : forall ne. List01 ne (Group todo vars) -> Core (List (CaseAlt vars))
 911 |       altGroups [] = pure $ toList $ DefaultCase <$> errorCase
 912 |       altGroups (ConGroup {newargs} cn tag rest :: cs)
 913 |           = do crest <- match fc fn phase rest (map (weakenNs (mkSizeOf newargs)) errorCase)
 914 |                cs' <- altGroups cs
 915 |                pure (ConCase cn tag newargs crest :: cs')
 916 |       altGroups (DelayGroup {tyarg} {valarg} rest :: cs)
 917 |           = do crest <- match fc fn phase rest (map (weakenNs (mkSizeOf [tyarg, valarg])) errorCase)
 918 |                cs' <- altGroups cs
 919 |                pure (DelayCase tyarg valarg crest :: cs')
 920 |       altGroups (ConstGroup c rest :: cs)
 921 |           = do crest <- match fc fn phase rest errorCase
 922 |                cs' <- altGroups cs
 923 |                pure (ConstCase c crest :: cs')
 924 |
 925 |   conRule : {a, vars, todo : _} ->
 926 |             {auto i : Ref PName Int} ->
 927 |             {auto c : Ref Ctxt Defs} ->
 928 |             FC -> Name -> Phase ->
 929 |             (cs : List01 True (PatClause (a :: todo) vars)) ->
 930 |             (0 isCons : All IsConClause cs) =>
 931 |             IMaybe ne (CaseTree vars) ->
 932 |             Core (CaseTree vars)
 933 |   -- ASSUMPTION, not expressed in the type, that the patterns all have
 934 |   -- the same variable (pprf) for the first argument. If not, the result
 935 |   -- will be a broken case tree... so we should find a way to express this
 936 |   -- in the type if we can.
 937 |   conRule {a} fc fn phase cs@(MkPatClause pvars (MkInfo pat pprf fty :: pats) pid rhs :: rest) err
 938 |       = do Element refinedcs _ <- pullOut <$> traverseList01 (substInClause fc) (pushIn cs isCons)
 939 |            groups <- groupCons fc fn pvars refinedcs
 940 |            ty <- case fty of
 941 |                       Known _ t => pure t
 942 |                       _ => throw (CaseCompile fc fn UnknownType)
 943 |            caseGroups fc fn phase pprf ty groups err
 944 |
 945 |   varRule : {a, vars, todo : _} ->
 946 |             {auto i : Ref PName Int} ->
 947 |             {auto c : Ref Ctxt Defs} ->
 948 |             FC -> Name -> Phase ->
 949 |             List01 True (PatClause (a :: todo) vars) ->
 950 |             IMaybe ne (CaseTree vars) ->
 951 |             Core (CaseTree vars)
 952 |   varRule fc fn phase cs err
 953 |       = do alts' <- traverseList01 updateVar cs
 954 |            match fc fn phase alts' err
 955 |     where
 956 |       updateVar : PatClause (a :: todo) vars -> Core (PatClause todo vars)
 957 |       -- replace the name with the relevant variable on the rhs
 958 |       updateVar (MkPatClause pvars (MkInfo (PLoc pfc n) prf fty :: pats) pid rhs)
 959 |           = pure $ MkPatClause (n :: pvars)
 960 |                         !(substInPats fc a (Local pfc (Just False) _ prf) pats)
 961 |                         pid (substName n (Local pfc (Just False) _ prf) rhs)
 962 |       -- If it's an as pattern, replace the name with the relevant variable on
 963 |       -- the rhs then continue with the inner pattern
 964 |       updateVar (MkPatClause pvars (MkInfo (PAs pfc n pat) prf fty :: pats) pid rhs)
 965 |           = do pats' <- substInPats fc a (mkTerm _ pat) pats
 966 |                let rhs' = substName n (Local pfc (Just True) _ prf) rhs
 967 |                updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats') pid rhs')
 968 |       -- match anything, name won't appear in rhs but need to update
 969 |       -- LHS pattern types based on what we've learned
 970 |       updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats) pid rhs)
 971 |           = pure $ MkPatClause pvars
 972 |                         !(substInPats fc a (mkTerm vars pat) pats) pid rhs
 973 |
 974 |   mixture : {a, vars, todo : _} ->
 975 |             {auto i : Ref PName Int} ->
 976 |             {auto c : Ref Ctxt Defs} ->
 977 |             {ps : List01 ne (PatClause (a :: todo) vars)} ->
 978 |             FC -> Name -> Phase ->
 979 |             Partitions ps ->
 980 |             IMaybe neErr (CaseTree vars) ->
 981 |             Core (IMaybe (ne || neErr) (CaseTree vars))
 982 |   mixture fc fn phase (ConClauses cs rest) err
 983 |       = do fallthrough <- mixture fc fn phase rest err
 984 |            Just <$> conRule fc fn phase cs fallthrough
 985 |   mixture fc fn phase (VarClauses vs rest) err
 986 |       = do fallthrough <- mixture fc fn phase rest err
 987 |            Just <$> varRule fc fn phase vs fallthrough
 988 |   mixture fc fn phase NoClauses err
 989 |       = pure err
 990 |
 991 | export
 992 | mkPat : {auto c : Ref Ctxt Defs} ->
 993 |         (matchable : Bool) -> List Pat -> ClosedTerm -> ClosedTerm -> Core Pat
 994 | mkPat _ [] orig (Ref fc Bound n) = pure $ PLoc fc n
 995 | mkPat True args orig (Ref fc (DataCon t a) n) = pure $ PCon fc n t a args
 996 | mkPat True args orig (Ref fc (TyCon a) n) = pure $ PTyCon fc n a args
 997 | mkPat True args orig (Ref fc Func n)
 998 |   = do prims <- getPrimitiveNames
 999 |        mtm <- normalisePrims (const True) isPConst True prims n args orig Env.empty
1000 |        case mtm of
1001 |          Just tm => if tm /= orig -- check we made progress; if there's an
1002 |                                   -- unresolved interface, we might be stuck
1003 |                                   -- and we'd loop forever
1004 |                        then mkPat True [] tm tm
1005 |                        else -- Possibly this should be an error instead?
1006 |                             pure $ PUnmatchable (getLoc orig) orig
1007 |          Nothing =>
1008 |            do log "compile.casetree" 10 $
1009 |                 "Unmatchable function: " ++ show n
1010 |               pure $ PUnmatchable (getLoc orig) orig
1011 | mkPat True args orig (Bind fc x (Pi _ _ _ s) t)
1012 |     -- For (b:Nat) -> b, the codomain looks like b [__], but we want `b` as the pattern
1013 |     = case subst (Erased fc Placeholder) t of
1014 |         App _ t'@(Ref fc Bound n) (Erased {}) => pure $ PArrow fc x !(mkPat True [] s s) !(mkPat False [] t' t')
1015 |         t' => pure $ PArrow fc x !(mkPat True [] s s) !(mkPat False [] t' t')
1016 | mkPat True args orig (App fc fn arg)
1017 |     = do parg <- mkPat True [] arg arg
1018 |          mkPat True (parg :: args) orig fn
1019 | mkPat True args orig (As fc _ (Ref _ Bound n) ptm)
1020 |     = pure $ PAs fc n !(mkPat True [] ptm ptm)
1021 | mkPat True args orig (As fc _ _ ptm)
1022 |     = mkPat True [] orig ptm
1023 | mkPat True args orig (TDelay fc r ty p)
1024 |     = pure $ PDelay fc r !(mkPat True [] orig ty) !(mkPat True [] orig p)
1025 | mkPat True args orig (PrimVal fc $ PrT c) -- Primitive type constant
1026 |     = pure $ PTyCon fc (UN (Basic $ show c)) 0 []
1027 | mkPat True args orig (PrimVal fc c) = pure $ PConst fc c -- Non-type constant
1028 | mkPat True args orig (TType fc _) = pure $ PTyCon fc (UN $ Basic "Type") 0 []
1029 | mkPat _ args orig tm
1030 |    = do log "compile.casetree" 10 $
1031 |           "Catchall: marking " ++ show tm ++ " as unmatchable"
1032 |         pure $ PUnmatchable (getLoc orig) orig
1033 |
1034 | export
1035 | argToPat : {auto c : Ref Ctxt Defs} -> ClosedTerm -> Core Pat
1036 | argToPat tm = mkPat True [] tm tm
1037 |
1038 | mkPatClause : {auto c : Ref Ctxt Defs} ->
1039 |               FC -> Name ->
1040 |               (args : Scope) -> ClosedTerm ->
1041 |               Int -> (List Pat, ClosedTerm) ->
1042 |               Core (PatClause args args)
1043 | mkPatClause fc fn args ty pid (ps, rhs)
1044 |     = maybe (throw (CaseCompile fc fn DifferingArgNumbers))
1045 |             (\eq =>
1046 |                do defs <- get Ctxt
1047 |                   nty <- nf defs Env.empty ty
1048 |                   ns <- mkNames args ps eq (Just nty)
1049 |                   log "compile.casetree" 20 $
1050 |                     "Make pat clause for names " ++ show ns
1051 |                      ++ " in LHS " ++ show ps
1052 |                   pure (MkPatClause [] ns pid
1053 |                           (rewrite sym (appendNilRightNeutral args) in
1054 |                                    (weakenNs (mkSizeOf args) rhs))))
1055 |             (checkLengthMatch args ps)
1056 |   where
1057 |     mkNames : (vars : Scope) -> (ps : List Pat) ->
1058 |               LengthMatch vars ps -> Maybe (NF []) ->
1059 |               Core (NamedPats vars vars)
1060 |     mkNames [] [] NilMatch fty = pure []
1061 |     mkNames (arg :: args) (p :: ps) (ConsMatch eq) fty
1062 |         = do defs <- get Ctxt
1063 |              empty <- clearDefs defs
1064 |              fa_tys <- the (Core (Maybe _, ArgType _)) $
1065 |                 case fty of
1066 |                      Nothing => pure (Nothing, CaseBuilder.Unknown)
1067 |                      Just (NBind pfc _ (Pi _ c _ farg) fsc) =>
1068 |                         pure (Just !(fsc defs (toClosure defaultOpts [] (Ref pfc Bound arg))),
1069 |                               Known c (embed !(quote empty [] farg)))
1070 |                      Just t =>
1071 |                         pure (Nothing, Stuck (embed !(quote empty [] t)))
1072 |              pure (MkInfo p First (Builtin.snd fa_tys)
1073 |                       :: weaken !(mkNames args ps eq (Builtin.fst fa_tys)))
1074 |
1075 | export
1076 | patCompile : {auto c : Ref Ctxt Defs} ->
1077 |              FC -> Name -> Phase ->
1078 |              ClosedTerm -> List01 True (List Pat, ClosedTerm) ->
1079 |              Core (args ** CaseTree args)
1080 | patCompile fc fn phase ty (p :: ps)
1081 |     = do let (ns ** n) = getNames 0 (fst p)
1082 |          pats <- mkPatClausesFrom 0 ns (p :: ps)
1083 |          -- low verbosity level: pretty print fully resolved names
1084 |          logC "compile.casetree" 5 $ do
1085 |            pats <- traverse toFullNames $ forget pats
1086 |            pure $ "Pattern clauses:\n"
1087 |                 ++ show (indent 2 $ vcat $ pretty <$> pats)
1088 |          -- higher verbosity: dump the raw data structure
1089 |          log "compile.casetree" 10 $ show pats
1090 |          i <- newRef PName (the Int 0)
1091 |          cases <- match fc fn phase pats Nothing
1092 |          pure (_ ** cases)
1093 |   where
1094 |     mkPatClausesFrom : Int -> (args : Scope) ->
1095 |                        List01 ne (List Pat, ClosedTerm) ->
1096 |                        Core (List01 ne (PatClause args args))
1097 |     mkPatClausesFrom i ns [] = pure []
1098 |     mkPatClausesFrom i ns (p :: ps)
1099 |         = do p' <- mkPatClause fc fn ns ty i p
1100 |              ps' <- mkPatClausesFrom (i + 1) ns ps
1101 |              pure (p' :: ps')
1102 |
1103 |     getNames : Int -> List Pat -> (ns : Scope ** SizeOf ns)
1104 |     getNames i [] = ([] ** zero)
1105 |     getNames i (x :: xs) =
1106 |       let (ns ** n) = getNames (i + 1) xs
1107 |       in (MN "arg" i :: ns ** suc n)
1108 |
1109 | toPatClause : {auto c : Ref Ctxt Defs} ->
1110 |               FC -> Name -> (ClosedTerm, ClosedTerm) ->
1111 |               Core (List Pat, ClosedTerm)
1112 | toPatClause fc n (lhs, rhs)
1113 |     = case getFnArgs lhs of
1114 |            (Ref ffc Func fn, args)
1115 |               => do defs <- get Ctxt
1116 |                     (np, _) <- getPosition n (gamma defs)
1117 |                     (fnp, _) <- getPosition fn (gamma defs)
1118 |                     if np == fnp
1119 |                        then pure (!(traverse argToPat args), rhs)
1120 |                        else throw (GenericMsg ffc ("Wrong function name in pattern LHS " ++ show (n, fn)))
1121 |            (f, args) => throw (GenericMsg fc "Not a function name in pattern LHS")
1122 |
1123 | -- Assumption (given 'ClosedTerm') is that the pattern variables are
1124 | -- explicitly named. We'll assign de Bruijn indices when we're done, and
1125 | -- the names of the top level variables we created are returned in 'args'
1126 | export
1127 | simpleCase : {auto c : Ref Ctxt Defs} ->
1128 |              FC -> Phase -> Name -> ClosedTerm ->
1129 |              (clauses : List01 True (ClosedTerm, ClosedTerm)) ->
1130 |              Core (args ** CaseTree args)
1131 | simpleCase fc phase fn ty clauses
1132 |     = do logC "compile.casetree" 5 $
1133 |                 do cs <- traverse (\ (c,d) => [| MkPair (toFullNames c) (toFullNames d) |]) (forget clauses)
1134 |                    pure $ "simpleCase: Clauses:\n" ++ show (
1135 |                      indent 2 $ vcat $ flip map cs $ \ lrhs =>
1136 |                        byShow (fst lrhs) <++> pretty "=" <++> byShow (snd lrhs))
1137 |          ps <- traverseList01 (toPatClause fc fn) clauses
1138 |          defs <- get Ctxt
1139 |          patCompile fc fn phase ty ps
1140 |
1141 | mutual
1142 |   findReachedAlts : CaseAlt ns' -> List Int
1143 |   findReachedAlts (ConCase _ _ _ t) = findReached t
1144 |   findReachedAlts (DelayCase _ _ t) = findReached t
1145 |   findReachedAlts (ConstCase _ t) = findReached t
1146 |   findReachedAlts (DefaultCase t) = findReached t
1147 |
1148 |   findReached : CaseTree ns -> List Int
1149 |   findReached (Case _ _ _ alts) = concatMap findReachedAlts alts
1150 |   findReached (STerm i _) = [i]
1151 |   findReached _ = []
1152 |
1153 | -- Replace a default case with explicit branches for the constructors.
1154 | -- This is easier than checking whether a default is needed when traversing
1155 | -- the tree (just one constructor lookup up front).
1156 | -- Unreachable defaults are those that when replaced by all possible constructors
1157 | -- followed by a removal of duplicate cases there is one _fewer_ total case alts.
1158 | identifyUnreachableDefaults : {auto c : Ref Ctxt Defs} ->
1159 |                               {vars : _} ->
1160 |                               FC -> Defs -> NF vars -> List (CaseAlt vars) ->
1161 |                               Core (SortedSet Int)
1162 | -- Leave it alone if it's a primitive type though, since we need the catch
1163 | -- all case there
1164 | identifyUnreachableDefaults fc defs (NPrimVal {}) cs = pure empty
1165 | identifyUnreachableDefaults fc defs (NType {}) cs = pure empty
1166 | identifyUnreachableDefaults fc defs nfty cs
1167 |     = do cs' <- traverse rep cs
1168 |          let (cs'', extraClauseIdxs) = dropRep (concat cs') empty
1169 |          let extraClauseIdxs' =
1170 |            if (length cs == (length cs'' + 1))
1171 |               then extraClauseIdxs
1172 |               else empty
1173 |          -- if a clause is unreachable under all the branches it can be found under
1174 |          -- then it is entirely unreachable.
1175 |          when (not $ null extraClauseIdxs') $
1176 |            log "compile.casetree.clauses" 25 $
1177 |              "Marking the following clause indices as unreachable under the current branch of the tree: " ++ (show extraClauseIdxs')
1178 |          pure extraClauseIdxs'
1179 |   where
1180 |     rep : CaseAlt vars -> Core (List (CaseAlt vars))
1181 |     rep (DefaultCase sc)
1182 |         = do allCons <- getCons defs nfty
1183 |              pure (map (mkAlt fc sc) allCons)
1184 |     rep c = pure [c]
1185 |
1186 |     dropRep : List (CaseAlt vars) -> SortedSet Int -> (List (CaseAlt vars), SortedSet Int)
1187 |     dropRep [] extra = ([], extra)
1188 |     dropRep (c@(ConCase n t args sc) :: rest) extra
1189 |           -- assumption is that there's no defaultcase in 'rest' because
1190 |           -- we've just removed it
1191 |         = let (filteredClauses, extraCases) = partition (not . tagIs t) rest
1192 |               extraClauses = extraCases >>= findReachedAlts
1193 |               (rest', extra') = dropRep filteredClauses $ fromList extraClauses
1194 |           in  (c :: rest', extra `union` extra')
1195 |     dropRep (c :: rest) extra
1196 |         = let (rest', extra') = dropRep rest extra
1197 |           in  (c :: rest', extra')
1198 |
1199 | ||| Find unreachable default paths through the tree for each clause.
1200 | ||| This is accomplished by expanding default clases into all concrete constructions
1201 | ||| and then listing the clauses reached.
1202 | ||| This list of clauses can be substracted from the list of "reachable" clauses
1203 | ||| and if it turns out that the number of unreachable ways to use a clause is equal
1204 | ||| to the number of ways to reach a RHS for that clause then the clause is totally
1205 | ||| superfluous (it will never be reached).
1206 | findExtraDefaults : {auto c : Ref Ctxt Defs} ->
1207 |                     {vars : _} ->
1208 |                     FC -> Defs -> CaseTree vars ->
1209 |                     Core (List Int)
1210 | findExtraDefaults fc defs (Case idx el ty altsIn)
1211 |   = do let fenv = mkEnv fc vars
1212 |        nfty <- nf defs fenv ty
1213 |        extraCases <- identifyUnreachableDefaults fc defs nfty altsIn
1214 |        extraCases' <- concat <$> traverse findExtraAlts altsIn
1215 |        pure (Prelude.toList extraCases ++ extraCases')
1216 |   where
1217 |     findExtraAlts : CaseAlt vars -> Core (List Int)
1218 |     findExtraAlts (ConCase x tag args ctree) = findExtraDefaults fc defs ctree
1219 |     findExtraAlts (DelayCase x arg ctree) = findExtraDefaults fc defs ctree
1220 |     findExtraAlts (ConstCase x ctree) = findExtraDefaults fc defs ctree
1221 |     -- already handled defaults by elaborating them to all possible cons
1222 |     findExtraAlts (DefaultCase ctree) = pure []
1223 |
1224 | findExtraDefaults fc defs ctree = pure []
1225 |
1226 | -- Returns the case tree, and a list of the clauses that aren't reachable
1227 | export
1228 | getPMDef : {auto c : Ref Ctxt Defs} ->
1229 |            FC -> Phase -> Name -> ClosedTerm -> List Clause ->
1230 |            Core (args ** (CaseTree args, List Clause))
1231 | -- If there's no clauses, make a definition with the right number of arguments
1232 | -- for the type, which we can use in coverage checking to ensure that one of
1233 | -- the arguments has an empty type
1234 | getPMDef fc phase fn ty []
1235 |     = do log "compile.casetree.getpmdef" 20 "getPMDef: No clauses!"
1236 |          defs <- get Ctxt
1237 |          pure (!(getArgs 0 !(nf defs Env.empty ty)) ** (Unmatched "No clauses in \{show fn}", []))
1238 |   where
1239 |     getArgs : Int -> ClosedNF -> Core (List Name)
1240 |     getArgs i (NBind fc x (Pi {}) sc)
1241 |         = do defs <- get Ctxt
1242 |              sc' <- sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder))
1243 |              pure (MN "arg" i :: !(getArgs i sc'))
1244 |     getArgs i _ = pure []
1245 | getPMDef fc phase fn ty clauses@(_ :: _)
1246 |     = do defs <- get Ctxt
1247 |          let cs = map (toClosed defs) (labelPat 0 $ fromList clauses)
1248 |          (_ ** t) <- simpleCase fc phase fn ty cs
1249 |          logC "compile.casetree.getpmdef" 20 $
1250 |            pure $ "Compiled to: " ++ show !(toFullNames t)
1251 |          let reached = findReached t
1252 |          log "compile.casetree.clauses" 25 $
1253 |            "Reached clauses: " ++ (show reached)
1254 |          extraDefaults <- findExtraDefaults fc defs t
1255 |          let unreachable = getUnreachable 0 (reached \\ extraDefaults) clauses
1256 |          pure (_ ** (t, unreachable))
1257 |   where
1258 |     getUnreachable : Int -> List Int -> List Clause -> List Clause
1259 |     getUnreachable i is [] = []
1260 |     getUnreachable i is (c :: cs)
1261 |         = if i `elem` is
1262 |              then getUnreachable (i + 1) is cs
1263 |              else c :: getUnreachable (i + 1) is cs
1264 |
1265 |     labelPat : Int -> List01 ne a -> List01 ne (String, a)
1266 |     labelPat i [] = []
1267 |     labelPat i (x :: xs) = ("pat" ++ show i ++ ":", x) :: labelPat (i + 1) xs
1268 |
1269 |     toClosed : Defs -> (String, Clause) -> (ClosedTerm, ClosedTerm)
1270 |     toClosed defs (pname, MkClause env lhs rhs)
1271 |           = (close fc pname env lhs, close fc pname env rhs)
1272 |