
   0 | module TTImp.Utils
   1 | 
   2 | import Core.Env
   3 | import Core.Value
   4 | import Core.UnifyState
   5 | import TTImp.TTImp
   6 | 
   7 | import Data.String
   8 | 
   9 | import Idris.Syntax
  10 | 
  11 | import Libraries.Data.NameMap
  12 | import Libraries.Utils.String
  13 | 
  14 | %default covering
  15 | 
  16 | 
  17 | -- Appends the ' character to "x" until it is unique with respect to "xs".
  18 | export
  19 | genUniqueStr : (xs : List String) -> (x : String) -> String
  20 | genUniqueStr xs x = if x `elem` xs then genUniqueStr xs (x ++ "'") else x
  21 | 
  22 | 
  23 | -- Extract the RawImp pieces from a ImpDecl so they can be searched for unquotes
  24 | -- Used in findBindableNames{,Quot}
  25 | rawImpFromDecl : ImpDecl -> List RawImp
  26 | rawImpFromDecl decl = case decl of
  27 |     IClaim (MkWithData fc1 $ MkIClaimData y z ys ty) => [ty.val]
  28 |     IData fc1 y _ (MkImpData fc2 n tycon opts datacons)
  29 |         => maybe id (::) tycon $ map val datacons
  30 |     IData fc1 y _ (MkImpLater fc2 n tycon) => [tycon]
  31 |     IDef fc1 y ys => getFromClause !ys
  32 |     IParameters fc1 ys zs => rawImpFromDecl !zs ++ map getParamTy (forget ys)
  33 |     IRecord fc1 y z _ (MkWithData _ (MkImpRecord header body)) => do
  34 |         binder <- header.val
  35 |         field <- body.val
  36 |         getFromPiInfo binder.val.info ++ [binder.val.boundType] ++ getFromIField field
  37 |     IFail fc1 msg zs => rawImpFromDecl !zs
  38 |     INamespace fc1 ys zs => rawImpFromDecl !zs
  39 |     ITransform fc1 y z w => [z, w]
  40 |     IRunElabDecl fc1 y => [] -- Not sure about this either
  41 |     IPragma _ _ f => []
  42 |     ILog k => []
  43 |     IBuiltin {} => []
  44 |   where getParamTy : ImpParameter' RawImp -> RawImp
  45 |         getParamTy binder = binder.val.boundType
  46 |         getFromClause : ImpClause -> List RawImp
  47 |         getFromClause (PatClause fc1 lhs rhs) = [lhs, rhs]
  48 |         getFromClause (WithClause fc1 lhs rig wval prf flags ys) = [wval, lhs] ++ getFromClause !ys
  49 |         getFromClause (ImpossibleClause fc1 lhs) = [lhs]
  50 |         getFromPiInfo : PiInfo RawImp -> List RawImp
  51 |         getFromPiInfo (DefImplicit x) = [x]
  52 |         getFromPiInfo _ = []
  53 |         getFromIField : IField -> List RawImp
  54 |         getFromIField field = getFromPiInfo field.val.info ++ [field.val.boundType]
  55 | 
  56 | 
  57 | -- Identify lower case names in argument position, which we can bind later.
  58 | -- Don't go under case, let, or local bindings, or IAlternative.
  59 | --
  60 | -- arg: Is the current expression in argument position? (We don't want to implicitly
  61 | --      bind funtions.)
  62 | --
  63 | -- env: Local names in scope. We only want to bind free variables, so we need this.
  64 | export
  65 | findBindableNames : (arg : Bool) -> (env : List Name) -> (used : List String) ->
  66 |                     RawImp -> List (Name, Name)
  67 | 
  68 | -- Helper to traverse the inside of a quoted expression, looking for unquotes
  69 | findBindableNamesQuot : List Name -> (used : List String) -> RawImp ->
  70 |                         List (Name, Name)
  71 | 
  72 | findBindableNames True env used (IVar fc nm@(UN (Basic n)))
  73 |       -- If the identifier is not bound locally and begins with a lowercase letter..
  74 |     = if not (nm `elem` env) && lowerFirst n
  75 |          then [(nm, UN $ Basic $ genUniqueStr used n)]
  76 |          else []
  77 | findBindableNames arg env used (IPi fc rig p mn aty retty)
  78 |     = let env' = case mn of
  79 |                       Nothing => env
  80 |                       Just n => n :: env in
  81 |           findBindableNames True env used aty ++
  82 |           findBindableNames True env' used retty
  83 | findBindableNames arg env used (ILam fc rig p mn aty sc)
  84 |     = let env' = case mn of
  85 |                       Nothing => env
  86 |                       Just n => n :: env in
  87 |       findBindableNames True env used aty ++
  88 |       findBindableNames True env' used sc
  89 | findBindableNames arg env used (IApp fc fn av)
  90 |     = findBindableNames False env used fn ++ findBindableNames True env used av
  91 | findBindableNames arg env used (INamedApp fc fn n av)
  92 |     = findBindableNames False env used fn ++ findBindableNames True env used av
  93 | findBindableNames arg env used (IAutoApp fc fn av)
  94 |     = findBindableNames False env used fn ++ findBindableNames True env used av
  95 | findBindableNames arg env used (IWithApp fc fn av)
  96 |     = findBindableNames False env used fn ++ findBindableNames True env used av
  97 | findBindableNames arg env used (IAs fc _ _ nm@(UN (Basic n)) pat)
  98 |     = (nm, UN $ Basic $ genUniqueStr used n) :: findBindableNames arg env used pat
  99 | findBindableNames arg env used (IAs fc _ _ n pat)
 100 |     = findBindableNames arg env used pat
 101 | findBindableNames arg env used (IMustUnify fc r pat)
 102 |     = findBindableNames arg env used pat
 103 | findBindableNames arg env used (IDelayed fc r t)
 104 |     = findBindableNames arg env used t
 105 | findBindableNames arg env used (IDelay fc t)
 106 |     = findBindableNames arg env used t
 107 | findBindableNames arg env used (IForce fc t)
 108 |     = findBindableNames arg env used t
 109 | findBindableNames arg env used (IQuote fc t)
 110 |     = findBindableNamesQuot env used t
 111 | findBindableNames arg env used (IQuoteDecl fc d)
 112 |     = findBindableNamesQuot env used !(rawImpFromDecl !d)
 113 | findBindableNames arg env used (IAlternative fc u alts)
 114 |     = concatMap (findBindableNames arg env used) alts
 115 | findBindableNames arg env used (IUpdate fc updates tm)
 116 |     = findBindableNames True env used tm ++
 117 |       concatMap (findBindableNames True env used . getFieldUpdateTerm) updates
 118 | -- We've skipped case, let and local - rather than guess where the
 119 | -- name should be bound, leave it to the programmer
 120 | findBindableNames arg env used tm = []
 121 | 
 122 | findBindableNamesQuot env used (IPi fc x y z argTy retTy)
 123 |     = findBindableNamesQuot env used ![argTy, retTy]
 124 | findBindableNamesQuot env used (ILam fc x y z argTy lamTy)
 125 |     = findBindableNamesQuot env used ![argTy, lamTy]
 126 | findBindableNamesQuot env used (ILet fc lhsfc x y nTy nVal scope)
 127 |     = findBindableNamesQuot env used ![nTy, nVal, scope]
 128 | findBindableNamesQuot env used (ICase fc _ x ty xs)
 129 |     = findBindableNamesQuot env used !([x, ty] ++ getRawImp !xs)
 130 |   where getRawImp : ImpClause -> List RawImp
 131 |         getRawImp (PatClause fc1 lhs rhs) = [lhs, rhs]
 132 |         getRawImp (WithClause fc1 lhs rig wval prf flags ys) = [wval, lhs] ++ getRawImp !ys
 133 |         getRawImp (ImpossibleClause fc1 lhs) = [lhs]
 134 | findBindableNamesQuot env used (ILocal fc xs x)
 135 |     = findBindableNamesQuot env used !(x :: rawImpFromDecl !xs)
 136 | findBindableNamesQuot env used (ICaseLocal fc uname internalName args x)
 137 |     = findBindableNamesQuot env used x
 138 | findBindableNamesQuot env used (IApp fc x y)
 139 |     = findBindableNamesQuot env used ![x, y]
 140 | findBindableNamesQuot env used (INamedApp fc x y z)
 141 |     = findBindableNamesQuot env used ![x, z]
 142 | findBindableNamesQuot env used (IAutoApp fc x y)
 143 |     = findBindableNamesQuot env used ![x, y]
 144 | findBindableNamesQuot env used (IWithApp fc x y)
 145 |     = findBindableNamesQuot env used ![x, y]
 146 | findBindableNamesQuot env used (IRewrite fc x y)
 147 |     = findBindableNamesQuot env used ![x, y]
 148 | findBindableNamesQuot env used (ICoerced fc x)
 149 |     = findBindableNamesQuot env used x
 150 | findBindableNamesQuot env used (IBindHere fc x y)
 151 |     = findBindableNamesQuot env used y
 152 | findBindableNamesQuot env used (IUpdate fc xs x)
 153 |     = findBindableNamesQuot env used !(x :: map getFieldUpdateTerm xs)
 154 | findBindableNamesQuot env used (IAs fc nfc x y z)
 155 |     = findBindableNamesQuot env used z
 156 | findBindableNamesQuot env used (IDelayed fc x y)
 157 |     = findBindableNamesQuot env used y
 158 | findBindableNamesQuot env used (IDelay fc x)
 159 |     = findBindableNamesQuot env used x
 160 | findBindableNamesQuot env used (IForce fc x)
 161 |     = findBindableNamesQuot env used x
 162 | findBindableNamesQuot env used (IUnquote fc x)
 163 |     = findBindableNames True env used x
 164 | findBindableNamesQuot env used (IWithUnambigNames fc xs x)
 165 |     = findBindableNamesQuot env used x
 166 | findBindableNamesQuot env used (IVar fc x) = []
 167 | findBindableNamesQuot env used (ISearch fc depth) = []
 168 | findBindableNamesQuot env used (IAlternative fc x xs) = []
 169 | findBindableNamesQuot env used (IBindVar fc x) = []
 170 | findBindableNamesQuot env used (IPrimVal fc c) = []
 171 | findBindableNamesQuot env used (IType fc) = []
 172 | findBindableNamesQuot env used (IHole fc x) = []
 173 | findBindableNamesQuot env used (Implicit fc bindIfUnsolved) = []
 174 | -- These are the ones I'm not sure about
 175 | findBindableNamesQuot env used (IMustUnify fc x y)
 176 |     = findBindableNamesQuot env used y
 177 | findBindableNamesQuot env used (IUnifyLog fc k x)
 178 |     = findBindableNamesQuot env used x
 179 | -- Should f `(g `(List ~(x))) bind "x" as a parameter to "f"?
 180 | -- Depends how (or if) recursive quoting works
 181 | findBindableNamesQuot env used (IQuote fc x) = []
 182 | findBindableNamesQuot env used (IQuoteName fc x) = []
 183 | findBindableNamesQuot env used (IQuoteDecl fc xs) = []
 184 | findBindableNamesQuot env used (IRunElab fc _ x) = []
 185 | 
 186 | export
 187 | findUniqueBindableNames :
 188 |   {auto c : Ref Ctxt Defs} ->
 189 |   FC -> (arg : Bool) -> (env : List Name) -> (used : List String) ->
 190 |   RawImp -> Core (List (Name, Name))
 191 | findUniqueBindableNames fc arg env used t
 192 |   = do let assoc = nub (findBindableNames arg env used t)
 193 |        when (showShadowingWarning !getSession) $
 194 |          do defs <- get Ctxt
 195 |             let ctxt = gamma defs
 196 |             ns <- map catMaybes $ for assoc $ \ (n, _) => do
 197 |                     ns <- lookupCtxtName n ctxt
 198 |                     let ns = flip List.mapMaybe ns $ \(n, _, d) =>
 199 |                                case definition d of
 200 |                                 -- do not warn about holes: `?a` is not actually
 201 |                                 -- getting shadowed as it will not become a
 202 |                                 -- toplevel declaration
 203 |                                  Hole {} => Nothing
 204 |                                  _ => pure n
 205 |                     pure $ MkPair n <$> fromList ns
 206 |             whenJust (fromList ns) $ recordWarning . ShadowingGlobalDefs fc
 207 |        pure assoc
 208 | 
 209 | export
 210 | findAllNames : (env : List Name) -> RawImp -> List Name
 211 | findAllNames env (IVar fc n)
 212 |     = if not (n `elem` env) then [n] else []
 213 | findAllNames env (IPi fc rig p mn aty retty)
 214 |     = let env' = case mn of
 215 |                       Nothing => env
 216 |                       Just n => n :: env in
 217 |           findAllNames env aty ++ findAllNames env' retty
 218 | findAllNames env (ILam fc rig p mn aty sc)
 219 |     = let env' = case mn of
 220 |                       Nothing => env
 221 |                       Just n => n :: env in
 222 |       findAllNames env' aty ++ findAllNames env' sc
 223 | findAllNames env (IApp fc fn av)
 224 |     = findAllNames env fn ++ findAllNames env av
 225 | findAllNames env (INamedApp fc fn n av)
 226 |     = findAllNames env fn ++ findAllNames env av
 227 | findAllNames env (IAutoApp fc fn av)
 228 |     = findAllNames env fn ++ findAllNames env av
 229 | findAllNames env (IWithApp fc fn av)
 230 |     = findAllNames env fn ++ findAllNames env av
 231 | findAllNames env (IAs fc _ _ n pat)
 232 |     = n :: findAllNames env pat
 233 | findAllNames env (IMustUnify fc r pat)
 234 |     = findAllNames env pat
 235 | findAllNames env (IDelayed fc r t)
 236 |     = findAllNames env t
 237 | findAllNames env (IDelay fc t)
 238 |     = findAllNames env t
 239 | findAllNames env (IForce fc t)
 240 |     = findAllNames env t
 241 | findAllNames env (IQuote fc t)
 242 |     = findAllNames env t
 243 | findAllNames env (IUnquote fc t)
 244 |     = findAllNames env t
 245 | findAllNames env (IAlternative fc u alts)
 246 |     = concatMap (findAllNames env) alts
 247 | findAllNames env (IUpdate fc updates tm)
 248 |     = findAllNames env tm
 249 |     ++ concatMap (findAllNames env . getFieldUpdateTerm) updates
 250 |     ++ concatMap (map (UN . Basic) . getFieldUpdatePath) updates
 251 | -- We've skipped case, let and local - rather than guess where the
 252 | -- name should be bound, leave it to the programmer
 253 | findAllNames env tm = []
 254 | 
 255 | -- Find the names in a type that affect the 'using' declarations (i.e.
 256 | -- the ones that mean the declaration will be added).
 257 | export
 258 | findIBindVars : RawImp -> List Name
 259 | findIBindVars (IPi fc rig p mn aty retty)
 260 |     = findIBindVars aty ++ findIBindVars retty
 261 | findIBindVars (ILam fc rig p mn aty sc)
 262 |     = findIBindVars aty ++ findIBindVars sc
 263 | findIBindVars (IApp fc fn av)
 264 |     = findIBindVars fn ++ findIBindVars av
 265 | findIBindVars (INamedApp fc fn n av)
 266 |     = findIBindVars fn ++ findIBindVars av
 267 | findIBindVars (IAutoApp fc fn av)
 268 |     = findIBindVars fn ++ findIBindVars av
 269 | findIBindVars (IWithApp fc fn av)
 270 |     = findIBindVars fn ++ findIBindVars av
 271 | findIBindVars (IBindVar fc v)
 272 |     = [v]
 273 | findIBindVars (IDelayed fc r t)
 274 |     = findIBindVars t
 275 | findIBindVars (IDelay fc t)
 276 |     = findIBindVars t
 277 | findIBindVars (IForce fc t)
 278 |     = findIBindVars t
 279 | findIBindVars (IAlternative fc u alts)
 280 |     = concatMap findIBindVars alts
 281 | findIBindVars (IUpdate fc updates tm)
 282 |     = findIBindVars tm ++ concatMap (findIBindVars . getFieldUpdateTerm) updates
 283 | -- We've skipped case, let and local - rather than guess where the
 284 | -- name should be bound, leave it to the programmer
 285 | findIBindVars tm = []
 286 | 
 287 | mutual
 288 |   -- Substitute for either an explicit variable name, or a bound variable name
 289 |   -- TODO association list should be map (should the `List Name` be a set as well?)
 290 |   substNames' : Bool -> List Name -> List (Name, RawImp) ->
 291 |                 RawImp -> RawImp
 292 |   substNames' False bound ps (IVar fc n)
 293 |       = if not (n `elem` bound)
 294 |            then case lookup n ps of
 295 |                      Just t => t
 296 |                      _ => IVar fc n
 297 |            else IVar fc n
 298 |   substNames' True bound ps (IBindVar fc n)
 299 |       = if not (n `elem` bound)
 300 |            then case lookup n ps of
 301 |                      Just t => t
 302 |                      _ => IBindVar fc n
 303 |            else IBindVar fc n
 304 |   substNames' bvar bound ps (IPi fc r p mn argTy retTy)
 305 |       = let bound' = maybe bound (\n => n :: bound) mn in
 306 |             IPi fc r p mn (substNames' bvar bound ps argTy)
 307 |                           (substNames' bvar bound' ps retTy)
 308 |   substNames' bvar bound ps (ILam fc r p mn argTy scope)
 309 |       = let bound' = maybe bound (\n => n :: bound) mn in
 310 |             ILam fc r p mn (substNames' bvar bound ps argTy)
 311 |                            (substNames' bvar bound' ps scope)
 312 |   substNames' bvar bound ps (ILet fc lhsFC r n nTy nVal scope)
 313 |       = let bound' = n :: bound in
 314 |             ILet fc lhsFC r n (substNames' bvar bound ps nTy)
 315 |                               (substNames' bvar bound ps nVal)
 316 |                               (substNames' bvar bound' ps scope)
 317 |   substNames' bvar bound ps (ICase fc opts y ty xs)
 318 |       = ICase fc opts
 319 |           (substNames' bvar bound ps y) (substNames' bvar bound ps ty)
 320 |           (map (substNamesClause' bvar bound ps) xs)
 321 |   substNames' bvar bound ps (ILocal fc xs y)
 322 |       = let bound' = definedInBlock emptyNS xs ++ bound in
 323 |             ILocal fc (map (substNamesDecl' bvar bound ps) xs)
 324 |                       (substNames' bvar bound' ps y)
 325 |   substNames' bvar bound ps (IApp fc fn arg)
 326 |       = IApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
 327 |   substNames' bvar bound ps (INamedApp fc fn y arg)
 328 |       = INamedApp fc (substNames' bvar bound ps fn) y (substNames' bvar bound ps arg)
 329 |   substNames' bvar bound ps (IAutoApp fc fn arg)
 330 |       = IAutoApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
 331 |   substNames' bvar bound ps (IWithApp fc fn arg)
 332 |       = IWithApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
 333 |   substNames' bvar bound ps (IAlternative fc y xs)
 334 |       = IAlternative fc y (map (substNames' bvar bound ps) xs)
 335 |   substNames' bvar bound ps (ICoerced fc y)
 336 |       = ICoerced fc (substNames' bvar bound ps y)
 337 |   substNames' bvar bound ps (IAs fc nameFC s y pattern)
 338 |       = IAs fc nameFC s y (substNames' bvar bound ps pattern)
 339 |   substNames' bvar bound ps (IMustUnify fc r pattern)
 340 |       = IMustUnify fc r (substNames' bvar bound ps pattern)
 341 |   substNames' bvar bound ps (IDelayed fc r t)
 342 |       = IDelayed fc r (substNames' bvar bound ps t)
 343 |   substNames' bvar bound ps (IDelay fc t)
 344 |       = IDelay fc (substNames' bvar bound ps t)
 345 |   substNames' bvar bound ps (IForce fc t)
 346 |       = IForce fc (substNames' bvar bound ps t)
 347 |   substNames' bvar bound ps (IUpdate fc updates tm)
 348 |       = IUpdate fc (map (mapFieldUpdateTerm $ substNames' bvar bound ps) updates)
 349 |                    (substNames' bvar bound ps tm)
 350 |   substNames' bvar bound ps tm = tm
 351 | 
 352 |   substNamesClause' : Bool -> List Name -> List (Name, RawImp) ->
 353 |                       ImpClause -> ImpClause
 354 |   substNamesClause' bvar bound ps (PatClause fc lhs rhs)
 355 |       = let bound' = map snd (findBindableNames True bound [] lhs)
 356 |                      ++ findIBindVars lhs
 357 |                      ++ bound in
 358 |             PatClause fc (substNames' bvar [] [] lhs)
 359 |                          (substNames' bvar bound' ps rhs)
 360 |   substNamesClause' bvar bound ps (WithClause fc lhs rig wval prf flags cs)
 361 |       = let bound' = map snd (findBindableNames True bound [] lhs)
 362 |                      ++ findIBindVars lhs
 363 |                      ++ bound in
 364 |             WithClause fc (substNames' bvar [] [] lhs) rig
 365 |                           (substNames' bvar bound' ps wval) prf flags cs
 366 |   substNamesClause' bvar bound ps (ImpossibleClause fc lhs)
 367 |       = ImpossibleClause fc (substNames' bvar bound [] lhs)
 368 | 
 369 |   substNamesData' : Bool -> List Name -> List (Name, RawImp) ->
 370 |                     ImpData -> ImpData
 371 |   substNamesData' bvar bound ps (MkImpData fc n con opts dcons)
 372 |       = MkImpData fc n (map (substNames' bvar bound ps) con) opts
 373 |                   (map (map (substNames' bvar bound ps)) dcons)
 374 |   substNamesData' bvar bound ps (MkImpLater fc n con)
 375 |       = MkImpLater fc n (substNames' bvar bound ps con)
 376 | 
 377 |   substNamesDecl' : Bool -> List Name -> List (Name, RawImp ) ->
 378 |                    ImpDecl -> ImpDecl
 379 |   substNamesDecl' bvar bound ps (IClaim claim)
 380 |       = IClaim $ map {type $= map (substNames' bvar bound ps)} claim
 381 |   substNamesDecl' bvar bound ps (IDef fc n cs)
 382 |       = IDef fc n (map (substNamesClause' bvar bound ps) cs)
 383 |   substNamesDecl' bvar bound ps (IData fc vis mbtot d)
 384 |       = IData fc vis mbtot (substNamesData' bvar bound ps d)
 385 |   substNamesDecl' bvar bound ps (IFail fc msg ds)
 386 |       = IFail fc msg (map (substNamesDecl' bvar bound ps) ds)
 387 |   substNamesDecl' bvar bound ps (INamespace fc ns ds)
 388 |       = INamespace fc ns (map (substNamesDecl' bvar bound ps) ds)
 389 |   substNamesDecl' bvar bound ps d = d
 390 | 
 391 | export
 392 | substNames : List Name -> List (Name, RawImp) ->
 393 |              RawImp -> RawImp
 394 | substNames = substNames' False
 395 | 
 396 | export
 397 | substBindVars : List Name -> List (Name, RawImp) ->
 398 |                 RawImp -> RawImp
 399 | substBindVars = substNames' True
 400 | 
 401 | export
 402 | substNamesClause : List Name -> List (Name, RawImp) ->
 403 |                    ImpClause -> ImpClause
 404 | substNamesClause = substNamesClause' False
 405 | 
 406 | mutual
 407 |   export
 408 |   substLoc : FC -> RawImp -> RawImp
 409 |   substLoc fc' (IVar fc n) = IVar fc' n
 410 |   substLoc fc' (IPi fc r p mn argTy retTy)
 411 |       = IPi fc' r p mn (substLoc fc' argTy)
 412 |                       (substLoc fc' retTy)
 413 |   substLoc fc' (ILam fc r p mn argTy scope)
 414 |       = ILam fc' r p mn (substLoc fc' argTy)
 415 |                         (substLoc fc' scope)
 416 |   substLoc fc' (ILet fc lhsFC r n nTy nVal scope)
 417 |       = ILet fc' fc' r n (substLoc fc' nTy)
 418 |                      (substLoc fc' nVal)
 419 |                      (substLoc fc' scope)
 420 |   substLoc fc' (ICase fc opts y ty xs)
 421 |       = ICase fc' opts (substLoc fc' y) (substLoc fc' ty)
 422 |                   (map (substLocClause fc') xs)
 423 |   substLoc fc' (ILocal fc xs y)
 424 |       = ILocal fc' (map (substLocDecl fc') xs)
 425 |                    (substLoc fc' y)
 426 |   substLoc fc' (IApp fc fn arg)
 427 |       = IApp fc' (substLoc fc' fn) (substLoc fc' arg)
 428 |   substLoc fc' (INamedApp fc fn y arg)
 429 |       = INamedApp fc' (substLoc fc' fn) y (substLoc fc' arg)
 430 |   substLoc fc' (IAutoApp fc fn arg)
 431 |       = IAutoApp fc' (substLoc fc' fn) (substLoc fc' arg)
 432 |   substLoc fc' (IWithApp fc fn arg)
 433 |       = IWithApp fc' (substLoc fc' fn) (substLoc fc' arg)
 434 |   substLoc fc' (IAlternative fc y xs)
 435 |       = IAlternative fc' y (map (substLoc fc') xs)
 436 |   substLoc fc' (ICoerced fc y)
 437 |       = ICoerced fc' (substLoc fc' y)
 438 |   substLoc fc' (IAs fc nameFC s y pattern)
 439 |       = IAs fc' fc' s y (substLoc fc' pattern)
 440 |   substLoc fc' (IMustUnify fc r pattern)
 441 |       = IMustUnify fc' r (substLoc fc' pattern)
 442 |   substLoc fc' (IDelayed fc r t)
 443 |       = IDelayed fc' r (substLoc fc' t)
 444 |   substLoc fc' (IDelay fc t)
 445 |       = IDelay fc' (substLoc fc' t)
 446 |   substLoc fc' (IForce fc t)
 447 |       = IForce fc' (substLoc fc' t)
 448 |   substLoc fc' (IUpdate fc updates tm)
 449 |       = IUpdate fc' (map (mapFieldUpdateTerm $ substLoc fc') updates)
 450 |                     (substLoc fc' tm)
 451 |   substLoc fc' tm = tm
 452 | 
 453 |   export
 454 |   substLocClause : FC -> ImpClause -> ImpClause
 455 |   substLocClause fc' (PatClause fc lhs rhs)
 456 |       = PatClause fc' (substLoc fc' lhs)
 457 |                       (substLoc fc' rhs)
 458 |   substLocClause fc' (WithClause fc lhs rig wval prf flags cs)
 459 |       = WithClause fc' (substLoc fc' lhs) rig
 460 |                        (substLoc fc' wval)
 461 |                        prf
 462 |                        flags
 463 |                        (map (substLocClause fc') cs)
 464 |   substLocClause fc' (ImpossibleClause fc lhs)
 465 |       = ImpossibleClause fc' (substLoc fc' lhs)
 466 | 
 467 |   substLocData : FC -> ImpData -> ImpData
 468 |   substLocData fc' (MkImpData fc n con opts dcons)
 469 |       = MkImpData fc' n (map (substLoc fc') con) opts
 470 |                         (map (map (substLoc fc') . set "fc" fc') dcons)
 471 |   substLocData fc' (MkImpLater fc n con)
 472 |       = MkImpLater fc' n (substLoc fc' con)
 473 | 
 474 |   substLocDecl : FC -> ImpDecl -> ImpDecl
 475 |   substLocDecl fc' (IClaim (MkWithData _ $ MkIClaimData r vis opts td))
 476 |       = IClaim (MkFCVal fc' $ MkIClaimData r vis opts (map (substLoc fc') (set "fc" fc' td)))
 477 |   substLocDecl fc' (IDef fc n cs)
 478 |       = IDef fc' n (map (substLocClause fc') cs)
 479 |   substLocDecl fc' (IData fc vis mbtot d)
 480 |       = IData fc' vis mbtot (substLocData fc' d)
 481 |   substLocDecl fc' (IFail fc msg ds)
 482 |       = IFail fc' msg (map (substLocDecl fc') ds)
 483 |   substLocDecl fc' (INamespace fc ns ds)
 484 |       = INamespace fc' ns (map (substLocDecl fc') ds)
 485 |   substLocDecl fc' d = d
 486 | 
 487 | nameNum : String -> (String, Maybe Int)
 488 | nameNum str = case span isDigit (reverse str) of
 489 |   ("", _) => (str, Nothing)
 490 |   (nums, pre) => case unpack pre of
 491 |     ('_' :: rest) => (reverse (pack rest), Just $ cast (reverse nums))
 492 |     _ => (str, Nothing)
 493 | 
 494 | nextNameNum : (String, Maybe Int) -> (String, Maybe Int)
 495 | nextNameNum (str, mn) = (str, Just $ maybe 0 (1+) mn)
 496 | 
 497 | unNameNum : (String, Maybe Int) -> String
 498 | unNameNum (str, Nothing) = str
 499 | unNameNum (str, Just n) = fastConcat [str, "_", show n]
 500 | 
 501 | 
 502 | -- TODO use a set of `String`s
 503 | export
 504 | uniqueBasicName : Defs -> List String -> String -> Core String
 505 | uniqueBasicName defs used n
 506 |     = if !usedName
 507 |          then uniqueBasicName defs used (next n)
 508 |          else pure n
 509 |   where
 510 |     usedName : Core Bool
 511 |     usedName
 512 |         = pure $ case !(lookupTyName (UN $ Basic n) (gamma defs)) of
 513 |                       [] => n `elem` used
 514 |                       _ => True
 515 | 
 516 |     next : String -> String
 517 |     next = unNameNum . nextNameNum . nameNum
 518 | 
 519 | export
 520 | uniqueHoleName : {auto s : Ref Syn SyntaxInfo} ->
 521 |                  Defs -> List String -> String -> Core String
 522 | uniqueHoleName defs used n
 523 |     = do syn <- get Syn
 524 |          uniqueBasicName defs (used ++ holeNames syn) n
 525 | 
 526 | export
 527 | uniqueHoleNames : {auto s : Ref Syn SyntaxInfo} ->
 528 |                   Defs -> Nat -> String -> Core (List String)
 529 | uniqueHoleNames defs = go [] where
 530 | 
 531 |   go : List String -> Nat -> String -> Core (List String)
 532 |   go acc Z _ = pure (reverse acc)
 533 |   go acc (S n) hole = do
 534 |     hole' <- uniqueHoleName defs acc hole
 535 |     go (hole' :: acc) n hole'
 536 | 
 537 | -- concatenation of the first two arguments must not be empty, or else we loop forever
 538 | unique : List String -> List String -> Int -> List Name -> String
 539 | unique [] supply suff usedns = unique supply supply (suff + 1) usedns
 540 | unique (str :: next) supply suff usedns
 541 |     = let var = mkVarN str suff in
 542 |           if UN (Basic var) `elem` usedns
 543 |              then unique next supply suff usedns
 544 |              else var
 545 |   where
 546 |     mkVarN : String -> Int -> String
 547 |     mkVarN x 0 = x
 548 |     mkVarN x i = x ++ show i
 549 | 
 550 | 
 551 | export
 552 | getArgName : {vars : _} ->
 553 |              {auto c : Ref Ctxt Defs} ->
 554 |              Defs -> Name ->
 555 |              List Name -> -- explicitly bound names (possibly coming later),
 556 |                           -- so we don't invent a default
 557 |                           -- name that duplicates it
 558 |              List Name -> -- names bound so far
 559 |              NF vars -> Core String
 560 | getArgName defs x bound allvars ty
 561 |     = do defnames <- findNames ty
 562 |          pure $ getName x defnames allvars
 563 |   where
 564 |     lookupName : Name -> List (Name, a) -> Core (Maybe a)
 565 |     lookupName n [] = pure Nothing
 566 |     lookupName n ((n', t) :: ts)
 567 |         = if !(getFullName n) == !(getFullName n')
 568 |              then pure (Just t)
 569 |              else lookupName n ts
 570 | 
 571 |     notBound : String -> Bool
 572 |     notBound x = not $ UN (Basic x) `elem` bound
 573 | 
 574 |     defaultNames : List String
 575 |     defaultNames = ["x", "y", "z", "w", "v", "s", "t", "u"]
 576 | 
 577 |     namesFor : Name -> Core (Maybe (List String))
 578 |     namesFor n = lookupName n (NameMap.toList (namedirectives defs))
 579 | 
 580 |     findNamesM : NF vars -> Core (Maybe (List String))
 581 |     findNamesM (NBind _ x (Pi {}) _)
 582 |         = pure (Just ["f", "g"])
 583 |     findNamesM (NTCon _ n d [(_, v)]) = do
 584 |           case dropNS !(full (gamma defs) n) of
 585 |             UN (Basic "List") =>
 586 |               do nf <- evalClosure defs v
 587 |                  case !(findNamesM nf) of
 588 |                    Nothing => namesFor n
 589 |                    Just ns => pure (Just (map (++ "s") ns))
 590 |             UN (Basic "Maybe") =>
 591 |               do nf <- evalClosure defs v
 592 |                  case !(findNamesM nf) of
 593 |                    Nothing => namesFor n
 594 |                    Just ns => pure (Just (map ("m" ++) ns))
 595 |             UN (Basic "SnocList") =>
 596 |               do nf <- evalClosure defs v
 597 |                  case !(findNamesM nf) of
 598 |                    Nothing => namesFor n
 599 |                    Just ns => pure (Just (map ("s" ++) ns))
 600 |             _ => namesFor n
 601 |     findNamesM (NTCon _ n _ _) = namesFor n
 602 |     findNamesM (NPrimVal fc $ PrT c) = do
 603 |           let defaultPos = ["m", "n", "p", "q"]
 604 |           let defaultInts = ["i", "j", "k", "l"]
 605 |           pure $ Just $ filter notBound $ case c of
 606 |             IntType => defaultInts
 607 |             Int8Type => defaultInts
 608 |             Int16Type => defaultInts
 609 |             Int32Type => defaultInts
 610 |             Int64Type => defaultInts
 611 |             IntegerType => defaultInts
 612 |             Bits8Type => defaultPos
 613 |             Bits16Type => defaultPos
 614 |             Bits32Type => defaultPos
 615 |             Bits64Type => defaultPos
 616 |             StringType => ["str"]
 617 |             CharType => ["c","d"]
 618 |             DoubleType => ["dbl"]
 619 |             WorldType => ["wrld", "w"]
 620 |     findNamesM ty = pure Nothing
 621 | 
 622 |     findNames : NF vars -> Core (List String)
 623 |     findNames nf = pure $ filter notBound $ fromMaybe defaultNames !(findNamesM nf)
 624 | 
 625 |     getName : Name -> List String -> List Name -> String
 626 |     getName (UN (Basic n)) defs used =
 627 |       -- # 1742 Uppercase names are not valid for pattern variables
 628 |       let candidate = ifThenElse (lowerFirst n) n (toLower n) in
 629 |       unique (candidate :: defs) (candidate :: defs) 0 used
 630 |     getName _ [] used = unique defaultNames defaultNames 0 $ used ++ bound
 631 |     getName _ defs used = unique defs defs 0 used
 632 | 
 633 | export
 634 | getArgNames : {vars : _} ->
 635 |               {auto c : Ref Ctxt Defs} ->
 636 |               Defs -> List Name -> List Name -> Env Term vars -> NF vars ->
 637 |               Core (List String)
 638 | getArgNames defs bound allvars env (NBind fc x (Pi _ _ p ty) sc)
 639 |     = do ns <- case p of
 640 |                     Explicit => pure [!(getArgName defs x bound allvars !(evalClosure defs ty))]
 641 |                     _ => pure []
 642 |          sc' <- sc defs (toClosure defaultOpts env (Erased fc Placeholder))
 643 |          pure $ ns ++ !(getArgNames defs bound (map (UN . Basic) ns ++ allvars) env sc')
 644 | getArgNames defs bound allvars env val = pure []
 645 | 
 646 | export
 647 | etaExpandImplicits : {auto c : Ref Ctxt Defs} ->
 648 |                      {auto u : Ref UST UState} ->
 649 |                      FC -> (ty, lhs, rhs : RawImp) ->
 650 |                      Core (RawImp, RawImp)
 651 | etaExpandImplicits fc ty lhs rhs
 652 |     = do let imps = collectImplicits ty
 653 |          namedImps <- for imps $ \nm => (nm,) <$> genVarName "arg"
 654 |          let lhsArgs = namedImps <&> makeArg True
 655 |          let rhsArgs = namedImps <&> makeArg False
 656 |          pure (apply lhs lhsArgs, apply rhs rhsArgs)
 657 |   where
 658 |     collectImplicits : RawImp -> List Name
 659 |     collectImplicits (IPi _ _ Explicit _        _ ty) = []
 660 |     collectImplicits (IPi _ _ _        (Just n) _ ty) = n :: collectImplicits ty
 661 |     collectImplicits _                                = []
 662 | 
 663 |     ivar : (bind : Bool) -> Name -> RawImp
 664 |     ivar True  = IBindVar fc
 665 |     ivar False = IVar fc
 666 | 
 667 |     makeArg : (bind : Bool) -> (Name, Name) -> Arg
 668 |     makeArg bind (n, bindName) = Named fc n $ ivar bind bindName
 669 |