0 | module Idris.Elab.Implementation

  2 | import Core.Env

  3 | import Core.Metadata

  4 | import Core.Unify

  6 | import Idris.REPL.Opts

  7 | import Idris.Syntax

  9 | import TTImp.BindImplicits

 10 | import TTImp.Elab.Check

 11 | import TTImp.Elab

 12 | import TTImp.ProcessDecls

 13 | import TTImp.TTImp

 14 | import TTImp.TTImp.Functor

 15 | import TTImp.Unelab

 16 | import TTImp.Utils

 18 | import Control.Monad.State

 19 | import Libraries.Data.ANameMap

 20 | import Libraries.Data.NameMap

 22 | %default covering

 24 | constructorBindName : Name

 25 | constructorBindName = UN (Basic "__con")

 28 | replaceSep : String -> String

 29 | replaceSep = pack . map toForward . unpack

 30 |   where

 31 |     toForward : Char -> Char

 32 |     toForward '\\' = '/'

 33 |     toForward x = x

 36 | mkImplName : FC -> Name -> List RawImp -> Name

 37 | mkImplName fc n ps

 38 |     = DN (show n ++ " implementation at " ++ replaceSep (show fc))

 39 |          (UN $ Basic ("__Impl_" ++ show n ++ "_" ++

 40 |           showSep "_" (map show ps)))

 42 | bindConstraints : FC -> PiInfo RawImp ->

 43 |                   List (Maybe Name, RawImp) -> RawImp -> RawImp

 44 | bindConstraints fc p [] ty = ty

 45 | bindConstraints fc p ((n, ty) :: rest) sc

 46 |     = IPi fc top p n ty (bindConstraints fc p rest sc)

 48 | bindImpls : List (AddFC (ImpParameter' RawImp)) -> RawImp -> RawImp

 49 | bindImpls [] ty = ty

 50 | bindImpls (binder :: rest) sc

 51 |     = IPi binder.fc binder.rig binder.val.info (Just binder.nameVal) binder.val.boundType (bindImpls rest sc)

 53 | addDefaults : FC -> Name ->

 54 |               (params : List (Name, RawImp)) -> -- parameters have been specialised, use them!

 55 |               (allMethods : List Name) ->

 56 |               (defaults : List (Name, List ImpClause)) ->

 57 |               List ImpDecl ->

 58 |               (List ImpDecl, List Name) -- Updated body, list of missing methods

 59 | addDefaults fc impName params allms defs body

 60 |     = let missing = dropGot allms body in

 61 |           extendBody [] missing body

 62 |   where

 63 |     specialiseMeth : Name -> (Name, RawImp)

 64 |     specialiseMeth n = (n, INamedApp fc (IVar fc n) constructorBindName (IVar fc impName))

 65 |     -- Given the list of missing names, if any are among the default definitions,

 66 |     -- add them to the body

 67 |     extendBody : List Name -> List Name -> List ImpDecl ->

 68 |                  (List ImpDecl, List Name)

 69 |     extendBody ms [] body = (body, ms)

 70 |     extendBody ms (n :: ns) body

 71 |         = case lookup n defs of

 72 |                Nothing => extendBody (n :: ms) ns body

 73 |                Just cs =>

 74 |                     -- If any method names appear in the clauses, they should

 75 |                     -- be applied to the constraint name __con because they

 76 |                     -- are going to be referring to the present implementation.

 77 |                     -- That is, default method implementations could depend on

 78 |                     -- other methods.

 79 |                     -- (See test idris2/interface014 for an example!)

 81 |                     -- Similarly if any parameters appear in the clauses, they should

 82 |                     -- be substituted for the actual parameters because they are going

 83 |                     -- to be referring to unbound variables otherwise.

 84 |                     -- (See test idris2/interface018 for an example!)

 85 |                     let mupdates = params ++ map specialiseMeth allms

 86 |                         cs' = map (substNamesClause [] mupdates) cs in

 87 |                         extendBody ms ns

 88 |                              (IDef fc n (map (substLocClause fc) cs') :: body)

 90 |     -- Find which names are missing from the body

 91 |     dropGot : List Name -> List ImpDecl -> List Name

 92 |     dropGot ms [] = ms

 93 |     dropGot ms (IDef _ n _ :: ds)

 94 |         = dropGot (filter (/= n) ms) ds

 95 |     dropGot ms (_ :: ds) = dropGot ms ds

 97 | getMethImps : {vars : _} ->

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

 99 |               Env Term vars -> Term vars ->

100 |               Core (List (Name, RigCount, Maybe RawImp, RawImp))

101 | getMethImps env (Bind fc x (Pi fc' c Implicit ty) sc)

102 |     = do rty <- map (map rawName) $ unelabNoSugar env ty

103 |          ts <- getMethImps (Pi fc' c Implicit ty :: env) sc

104 |          pure ((x, c, Nothing, rty) :: ts)

105 | getMethImps env (Bind fc x (Pi fc' c (DefImplicit def) ty) sc)

106 |     = do rty <- map (map rawName) $ unelabNoSugar env ty

107 |          rdef <- map (map rawName) $ unelabNoSugar env def

108 |          ts <- getMethImps (Pi fc' c (DefImplicit def) ty :: env) sc

109 |          pure ((x, c, Just rdef, rty) :: ts)

110 | getMethImps env tm = pure []

113 | elabImplementation : {vars : _} ->

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

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

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

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

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

119 |                      FC -> Visibility -> List FnOpt -> Pass ->

120 |                      Env Term vars -> NestedNames vars ->

121 |                      (implicits : List (AddFC (ImpParameter' RawImp))) ->

122 |                      (constraints : List (Maybe Name, RawImp)) ->

123 |                      Name ->

124 |                      (ps : List RawImp) ->

125 |                      (namedimpl : Bool) ->

126 |                      (implName : Name) ->

127 |                      (nusing : List Name) ->

128 |                      Maybe (List ImpDecl) ->

129 |                      Core ()

131 | elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named impName_in nusing mbody

132 |     = do -- let impName_in = maybe (mkImplName fc iname ps) id impln

133 |          -- If we're in a nested block, update the name

134 |          let impName_nest = mapNestedName nest impName_in

135 |          impName <- inCurrentNS impName_nest

136 |          -- The interface name might be qualified, so check if it's an

137 |          -- alias for something

138 |          syn <- get Syn

139 |          defs <- get Ctxt

140 |          let varsList = toList vars -- TODO change list in findBindableNames?

141 |          inames <- lookupCtxtName iname (gamma defs)

142 |          let [cndata] = concatMap (\n => lookupName n (ifaces syn))

143 |                                   (map fst inames)

144 |              | ns => ambiguousName vfc iname (map fst ns)

145 |          let cn : Name = fst cndata

146 |          let cdata : IFaceInfo = snd cndata

148 |          Just ity <- lookupTyExact cn (gamma defs)

149 |               | Nothing => undefinedName vfc cn

150 |          Just conty <- lookupTyExact (iconstructor cdata) (gamma defs)

151 |               | Nothing => undefinedName vfc (iconstructor cdata)

153 |          let impsp = nub (concatMap findIBinds ps ++

154 |                           concatMap findIBinds (map snd cons))

156 |          logTerm "elab.implementation" 3 ("Found interface " ++ show cn) ity

157 |          log "elab.implementation" 3 $

158 |                  "\n  with params: " ++ show (params cdata)

159 |                  ++ "\n  specialised to: " ++ show ps

160 |                  ++ "\n  and parents: " ++ show (parents cdata)

161 |                  ++ "\n  using implicits: " ++ show impsp

162 |                  ++ "\n  and methods: " ++ show (map val (methods cdata)) ++ "\n"

163 |                  ++ "\nConstructor: " ++ show (iconstructor cdata) ++ "\n"

164 |          logTerm "elab.implementation" 3 "Constructor type: " conty

165 |          log "elab.implementation" 5 $ "Making implementation " ++ show impName

167 |          -- 1. Build the type for the implementation

168 |          -- Make the constraints auto implicit arguments, which can be explicitly

169 |          -- given when using named implementations

170 |          --    (cs : Constraints) -> Impl params

171 |          -- Don't make it a hint if it's a named implementation

172 |          let opts = if named

173 |                        then [Inline]

174 |                        else [Inline, Hint True]

176 |          let initTy = bindImpls is $ bindConstraints vfc AutoImplicit cons

177 |                          (apply (IVar vfc iname) ps)

178 |          let paramBinds = if !isUnboundImplicits

179 |                           then findBindableNames True varsList [] initTy

180 |                           else []

181 |          let impTy = doBind paramBinds initTy

183 |          let impTyDecl

184 |              = IClaim (MkFCVal vfc $ MkIClaimData top vis opts (Mk [EmptyFC, NoFC impName] impTy))

186 |          log "elab.implementation" 5 $ "Implementation type: " ++ show impTy

188 |          -- Handle the case where it was already declared with a Nothing mbody

189 |          when (typePass pass) $ do

190 |            gdefm <- lookupCtxtExactI impName (gamma defs)

191 |            case gdefm of

192 |               Nothing => processDecl [] nest env impTyDecl

193 |               -- If impName exists, check that it is a forward declaration of the same type

194 |               Just (tidx,gdef) =>

195 |                 do u <- uniVar vfc

196 |                    -- If the definition is filled in, it wasn't a forward declaration

197 |                    let None = definition gdef

198 |                      | _ => throw (AlreadyDefined vfc impName)

199 |                    (ty,_) <- elabTerm tidx InType [] nest env

200 |                                       (IBindHere vfc (PI erased) impTy)

201 |                                       (Just (gType vfc u))

202 |                    let fullty = abstractFullEnvType vfc env ty

203 |                    ok <- convert defs Env.empty fullty (type gdef)

204 |                    unless ok $ do logTermNF "elab.implementation" 1 "Previous" Env.empty (type gdef)

205 |                                   logTermNF "elab.implementation" 1 "Now" Env.empty fullty

206 |                                   throw (CantConvert (getFC impTy) (gamma defs) Env.empty fullty (type gdef))

208 |          -- If the body is empty, we're done for now (just declaring that

209 |          -- the implementation exists and define it later)

210 |          when (defPass pass) $

211 |            whenJust mbody $ \body_in => do

212 |                defs <- get Ctxt

213 |                Just impTyc <- lookupTyExact impName (gamma defs)

214 |                     | Nothing => throw (InternalError ("Can't happen, can't find type of " ++ show impName))

215 |                methImps <- getMethImps Env.empty impTyc

216 |                log "elab.implementation" 3 $ "Bind implicits to each method: " ++ show methImps

218 |                -- 1.5. Lookup default definitions and add them to the body

219 |                let (body, missing)

220 |                      = addDefaults vfc impName

221 |                                       (zip (params cdata) ps)

222 |                                       (map (dropNS . (.nameVal)) (methods cdata))

223 |                                       (defaults cdata) body_in

225 |                log "elab.implementation" 5 $ "Added defaults: body is " ++ show body

226 |                log "elab.implementation" 5 $ "Missing methods: " ++ show missing

227 |                when (not (isNil missing)) $

228 |                  throw (GenericMsg ifc ("Missing methods in " ++ show iname ++ ": "

229 |                                         ++ showSep ", " (map show missing)))

231 |                -- Add the 'using' hints

232 |                defs <- get Ctxt

233 |                let hs = openHints defs -- snapshot open hint state

234 |                log "elab.implementation" 10 $ "Open hints: " ++ (show (impName :: nusing))

235 |                traverse_ (\n => do n' <- checkUnambig vfc n

236 |                                    addOpenHint n') nusing

238 |                -- 2. Elaborate top level function types for this interface

239 |                defs <- get Ctxt

240 |                fns <- topMethTypes [] impName methImps impsp

241 |                                       (implParams cdata) (params cdata)

242 |                                       (map (.nameVal) (methods cdata))

243 |                                       (methods cdata)

244 |                traverse_ (processDecl [] nest env) (map mkTopMethDecl fns)

246 |                -- 3. Build the record for the implementation

247 |                let mtops = map (fst . snd) fns

248 |                let con = iconstructor cdata

249 |                let ilhs = impsApply (IVar EmptyFC impName)

250 |                                     (map (\(x, _) => (x, IBindVar vfc x)) methImps)

251 |                -- RHS is the constructor applied to a search for the necessary

252 |                -- parent constraints, then the method implementations

253 |                defs <- get Ctxt

254 |                let fldTys = getFieldArgs !(normaliseHoles defs Env.empty conty)

255 |                log "elab.implementation" 5 $ "Field types " ++ show fldTys

256 |                let irhs = apply (autoImpsApply (IVar vfc con) $ map (const (ISearch vfc 500)) (parents cdata))

257 |                                 (map (mkMethField methImps fldTys) fns)

258 |                let impFn = IDef vfc impName [PatClause vfc ilhs irhs]

259 |                log "elab.implementation" 5 $ "Implementation record: " ++ show impFn

261 |                -- If it's a named implementation, add it as a global hint while

262 |                -- elaborating the record and bodies

263 |                when named $ addOpenHint impName

265 |                -- Make sure we don't use this name to solve parent constraints

266 |                -- when elaborating the record, or we'll end up in a cycle!

267 |                setFlag vfc impName BlockedHint

269 |                -- Update nested names so we elaborate the body in the right

270 |                -- environment

271 |                names' <- traverse applyEnv (impName :: mtops)

272 |                let nest' = { names $= (names' ++) } nest

274 |                traverse_ (processDecl [] nest' env) [impFn]

275 |                unsetFlag vfc impName BlockedHint

277 |                setFlag vfc impName TCInline

278 |                -- it's the methods we're interested in, not the implementation

279 |                setFlag vfc impName (SetTotal PartialOK)

281 |                -- 4. (TODO: Order method bodies to be in declaration order, in

282 |                --    case of dependencies)

284 |                -- 5. Elaborate the method bodies

285 |                let upds = map methNameUpdate fns

286 |                body' <- traverse (updateBody upds) body

288 |                log "elab.implementation" 10 $ "Implementation body: " ++ show body'

289 |                traverse_ (processDecl [] nest' env) body'

291 |                -- 6. Add transformation rules for top level methods

292 |                traverse_ (addTransform impName upds) (methods cdata)

294 |                -- inline flag has done its job, and outside the interface

295 |                -- it can hurt, so unset it now

296 |                unsetFlag vfc impName TCInline

298 |                -- Reset the open hints (remove the named implementation)

299 |                setOpenHints hs

301 |     where

302 |     vfc : FC

303 |     vfc = virtualiseFC ifc

305 |     applyEnv : Name ->

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

307 |     applyEnv n

308 |         = do n' <- resolveName n

309 |              pure (Resolved n', (Nothing, reverse (allVars env),

310 |                       \fn, nt => applyToFull vfc

311 |                                      (Ref vfc nt (Resolved n')) env))

313 |     -- For the method fields in the record, get the arguments we need to abstract

314 |     -- over

315 |     getFieldArgs : Term vs -> List (Name, List (Name, RigCount, PiInfo RawImp))

316 |     getFieldArgs (Bind _ x (Pi _ _ _ ty) sc)

317 |         = (x, getArgs ty) :: getFieldArgs sc

318 |       where

319 |         getArgs : Term vs' -> List (Name, RigCount, PiInfo RawImp)

320 |         getArgs (Bind _ x (Pi _ c p _) sc)

321 |             = (x, c, forgetDef p) :: getArgs sc

322 |         getArgs _ = []

323 |     getFieldArgs _ = []

325 |     impsApply : RawImp -> List (Name, RawImp) -> RawImp

326 |     impsApply fn [] = fn

327 |     impsApply fn ((n, arg) :: ns)

328 |         = impsApply (INamedApp vfc fn n arg) ns

330 |     autoImpsApply : RawImp -> List RawImp -> RawImp

331 |     autoImpsApply f [] = f

332 |     autoImpsApply f (x :: xs) = autoImpsApply (IAutoApp (getFC f) f x) xs

334 |     mkLam : List (Name, RigCount, PiInfo RawImp) -> RawImp -> RawImp

335 |     mkLam [] tm = tm

336 |     mkLam ((x, c, p) :: xs) tm

337 |         = ILam EmptyFC c p (Just x) (Implicit vfc False) (mkLam xs tm)

339 |     applyTo : RawImp -> List (Name, RigCount, PiInfo RawImp) -> RawImp

340 |     applyTo tm [] = tm

341 |     applyTo tm ((x, c, Explicit) :: xs)

342 |         = applyTo (IApp EmptyFC tm (IVar EmptyFC x)) xs

343 |     applyTo tm ((x, c, AutoImplicit) :: xs)

344 |         = applyTo (INamedApp EmptyFC tm x (IVar EmptyFC x)) xs

345 |     applyTo tm ((x, c, Implicit) :: xs)

346 |         = applyTo (INamedApp EmptyFC tm x (IVar EmptyFC x)) xs

347 |     applyTo tm ((x, c, DefImplicit _) :: xs)

348 |         = applyTo (INamedApp EmptyFC tm x (IVar EmptyFC x)) xs

350 |     -- When applying the method in the field for the record, eta expand

351 |     -- the expected arguments based on the field type, so that implicits get

352 |     -- inserted in the right place

353 |     mkMethField : List (Name, a) ->

354 |                   List (Name, List (Name, RigCount, PiInfo RawImp)) ->

355 |                   (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> RawImp

356 |     mkMethField methImps fldTys (topn, n, upds, c, treq, ty)

357 |         = let argns = map applyUpdate (maybe [] id (lookup (dropNS topn) fldTys))

358 |               imps = map fst methImps in

359 |               -- Pass through implicit arguments to the function which are also

360 |               -- implicit arguments to the declaration

361 |               mkLam argns

362 |                     (impsApply

363 |                          (applyTo (IVar EmptyFC n) argns)

364 |                          (map (\n => (n, IVar vfc n)) imps))

365 |       where

366 |         applyUpdate : (Name, RigCount, PiInfo RawImp) ->

367 |                       (Name, RigCount, PiInfo RawImp)

368 |         applyUpdate (UN (Basic n), c, p)

369 |             = maybe (UN (Basic n), c, p) (\n' => (UN (Basic n'), c, p)) (lookup n upds)

370 |         applyUpdate t = t

372 |     methName : Name -> Name

373 |     methName (NS _ n) = methName n

374 |     methName n

375 |         = DN (show n)

376 |              (UN $ Basic (show n ++ "_" ++ show iname ++ "_" ++

377 |                      (if named then show impName_in else "") ++

378 |                      showSep "_" (map show ps)))

380 |     applyCon : Name -> Name -> Core (Name, RawImp)

381 |     applyCon impl n

382 |         = do mn <- inCurrentNS (methName n)

383 |              pure (dropNS n, IVar vfc mn)

385 |     bindImps : List (Name, RigCount, Maybe RawImp, RawImp) -> RawImp -> RawImp

386 |     bindImps [] ty = ty

387 |     bindImps ((n, c, Just def, t) :: ts) ty

388 |         = IPi vfc c (DefImplicit def) (Just n) t (bindImps ts ty)

389 |     bindImps ((n, c, Nothing, t) :: ts) ty

390 |         = IPi vfc c Implicit (Just n) t (bindImps ts ty)

392 |     -- Return method name, specialised method name, implicit name updates,

393 |     -- and method type. Also return how the method name should be updated

394 |     -- in later method types (specifically, putting implicits in)

395 |     topMethType : List (Name, RawImp) ->

396 |                   Name -> List (Name, RigCount, Maybe RawImp, RawImp) ->

397 |                   List String -> List Name -> List Name -> List Name ->

398 |                   Method ->

399 |                   Core ((Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp),

400 |                            List (Name, RawImp))

401 |     topMethType methupds impName methImps impsp imppnames pnames allmeths meth

402 |         = do -- Get the specialised type by applying the method to the

403 |              -- parameters

404 |              n <- inCurrentNS (methName meth.nameVal)

405 |              let varsList = toList vars

407 |              -- Avoid any name clashes between parameters and method types by

408 |              -- renaming IBindVars in the method types which appear in the

409 |              -- parameters

410 |              let upds' = !(traverse (applyCon impName) allmeths)

411 |              let mty_in = substNames varsList upds' meth.val

412 |              let (upds, mty_in) = runState [] (renameIBinds impsp (findImplicits mty_in) mty_in)

413 |              -- Finally update the method type so that implicits from the

414 |              -- parameters are passed through to any earlier methods which

415 |              -- appear in the type

416 |              let mty_in = substNames varsList methupds mty_in

418 |              -- Substitute _ in for the implicit parameters, then

419 |              -- substitute in the explicit parameters.

420 |              let mty_iparams

421 |                    = substBindVars varsList

422 |                                 (map (\n => (n, Implicit vfc False)) imppnames)

423 |                                 mty_in

424 |              let mty_params

425 |                    = substNames varsList (zip pnames ps) mty_iparams

426 |              log "elab.implementation" 5 $ "Substitute implicits " ++ show imppnames ++

427 |                      " parameters " ++ show (zip pnames ps) ++

428 |                      " "  ++ show mty_in ++ " is " ++

429 |                      show mty_params

431 |              let mbase = bindImps methImps $

432 |                          bindConstraints vfc AutoImplicit cons $

433 |                          mty_params

434 |              let ibound = findImplicits mbase

436 |              mty <- bindTypeNamesUsed ifc ibound varsList mbase

438 |              log "elab.implementation" 3 $

439 |                      "Method " ++ show meth.nameVal ++ " ==> " ++

440 |                      show n ++ " : " ++ show mty

441 |              log "elab.implementation" 3 $ "    (initially " ++ show mty_in ++ ")"

442 |              log "elab.implementation" 5 $ "Updates " ++ show methupds

443 |              log "elab.implementation" 5 $ "From " ++ show mbase

444 |              log "elab.implementation" 3 $ "Name updates " ++ show upds

445 |              log "elab.implementation" 3 $ "Param names: " ++ show pnames

446 |              log "elab.implementation" 10 $ "Used names " ++ show ibound

447 |              let ibinds = map fst methImps

448 |              let methupds' = if isNil ibinds then []

449 |                              else [(n, impsApply (IVar vfc n)

450 |                                      (map (\x => (x, IBindVar vfc x)) ibinds))]

452 |              pure ((meth.nameVal, n, upds, meth.rig, meth.totReq, mty), methupds')

454 |     topMethTypes : List (Name, RawImp) ->

455 |                    Name -> List (Name, RigCount, Maybe RawImp, RawImp) ->

456 |                    List String ->

457 |                    List Name -> List Name -> List Name ->

458 |                    List Method ->

459 |                    Core (List (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp))

460 |     topMethTypes upds impName methImps impsp imppnames pnames allmeths [] = pure []

461 |     topMethTypes upds impName methImps impsp imppnames pnames allmeths (m :: ms)

462 |         = do (m', newupds) <- topMethType upds impName methImps impsp imppnames pnames allmeths m

463 |              ms' <- topMethTypes (newupds ++ upds) impName methImps impsp imppnames pnames allmeths ms

464 |              pure (m' :: ms')

466 |     mkTopMethDecl : (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> ImpDecl

467 |     mkTopMethDecl (mn, n, upds, c, treq, mty)

468 |         = do let opts = if isJust $ findTotality opts_in

469 |                           then opts_in

470 |                           else maybe opts_in (\t => Totality t :: opts_in) treq

471 |              IClaim $ MkFCVal vfc $ MkIClaimData c vis opts $ Mk [EmptyFC, NoFC n] mty

473 |     -- Given the method type (result of topMethType) return the mapping from

474 |     -- top level method name to current implementation's method name

475 |     methNameUpdate : (Name, Name, t) -> (Name, Name)

476 |     methNameUpdate (UN mn, fn, _) = (UN mn, fn)

477 |     methNameUpdate (NS _ mn, fn, p) = methNameUpdate (mn, fn, p)

478 |     methNameUpdate (mn, fn, p) = (UN (Basic $ nameRoot mn), fn) -- probably impossible

481 |     findMethName : List (Name, Name) -> FC -> Name -> Core Name

482 |     findMethName ns fc n

483 |         = case lookup n ns of

484 |                Nothing => throw (GenericMsg fc

485 |                                 (show n ++ " is not a method of " ++

486 |                                  show iname))

487 |                Just n' => pure n'

489 |     updateApp : List (Name, Name) -> RawImp -> Core RawImp

490 |     updateApp ns (IVar fc n)

491 |         = do n' <- findMethName ns fc n

492 |              pure (IVar fc n')

493 |     updateApp ns (IApp fc f arg)

494 |         = do f' <- updateApp ns f

495 |              pure (IApp fc f' arg)

496 |     updateApp ns (IWithApp fc f arg)

497 |         = do f' <- updateApp ns f

498 |              pure (IWithApp fc f' arg)

499 |     updateApp ns (IAutoApp fc f arg)

500 |         = do f' <- updateApp ns f

501 |              pure (IAutoApp fc f' arg)

502 |     updateApp ns (INamedApp fc f x arg)

503 |         = do f' <- updateApp ns f

504 |              pure (INamedApp fc f' x arg)

505 |     updateApp ns tm

506 |         = throw (GenericMsg (getFC tm) "Invalid method definition")

508 |     updateClause : List (Name, Name) -> ImpClause ->

509 |                    Core ImpClause

510 |     updateClause ns (PatClause fc lhs rhs)

511 |         = do lhs' <- updateApp ns lhs

512 |              pure (PatClause fc lhs' rhs)

513 |     updateClause ns (WithClause fc lhs rig wval prf flags cs)

514 |         = do lhs' <- updateApp ns lhs

515 |              cs' <- traverse (updateClause ns) cs

516 |              pure (WithClause fc lhs' rig wval prf flags cs')

517 |     updateClause ns (ImpossibleClause fc lhs)

518 |         = do lhs' <- updateApp ns lhs

519 |              pure (ImpossibleClause fc lhs')

521 |     updateBody : List (Name, Name) -> ImpDecl -> Core ImpDecl

522 |     updateBody ns (IDef fc n cs)

523 |         = do cs' <- traverse (updateClause ns) cs

524 |              n' <- findMethName ns fc n

525 |              log "ide-mode.highlight" 1 $ show (n, n', fc)

526 |              pure (IDef fc n' cs')

527 |     updateBody ns e

528 |         = throw (GenericMsg (getFC e)

529 |                    "Implementation body can only contain definitions")

531 |     addTransform : Name -> List (Name, Name) ->

532 |                    Method ->

533 |                    Core ()

534 |     addTransform iname ns meth

535 |         = do log "elab.implementation" 3 $

536 |                      "Adding transform for " ++ show meth.nameVal ++ " : " ++ show meth.val ++

537 |                      "\n\tfor " ++ show iname ++ " in " ++ show ns

538 |              let lhs = INamedApp vfc (IVar vfc meth.name.val)

539 |                                      constructorBindName

540 |                                      (IVar vfc iname)

541 |              let Just mname = lookup (dropNS meth.nameVal) ns

542 |                  | Nothing => pure ()

543 |              let rhs = IVar vfc mname

544 |              log "elab.implementation" 5 $ show lhs ++ " ==> " ++ show rhs

545 |              handleUnify

546 |                  (processDecl [] nest env

547 |                      (ITransform vfc (UN $ Basic (show meth.nameVal ++ " " ++ show iname)) lhs rhs))

548 |                  (\err =>

549 |                      log "elab.implementation" 5 $ "Can't add transform " ++

550 |                                 show lhs ++ " ==> " ++ show rhs ++

551 |                              "\n\t" ++ show err)