0 | module Idris.Syntax.Traversals

  2 | import Idris.Syntax

  4 | import TTImp.TTImp

  6 | %default covering

  9 | mapPTermM : (PTerm' nm -> Core (PTerm' nm)) -> PTerm' nm -> Core (PTerm' nm)

 10 | mapPTermM f = goPTerm where

 12 |   mutual

 14 |     goPTerm : PTerm' nm -> Core (PTerm' nm)

 15 |     goPTerm t@(PRef {}) = f t

 16 |     goPTerm (NewPi x) =

 17 |       NewPi <$> traverse goPBinderScope x

 18 |     goPTerm (Forall x) =

 19 |       Forall <$> traverse (\(a, b) => MkPair a <$> goPTerm b) x

 20 |     goPTerm (PPi fc x info z argTy retTy) =

 21 |       PPi fc x <$> goPiInfo info

 22 |                <*> pure z

 23 |                <*> goPTerm argTy

 24 |                <*> goPTerm retTy

 25 |       >>= f

 26 |     goPTerm (PLam fc x info pat argTy scope) =

 27 |       PLam fc x <$> goPiInfo info

 28 |                 <*> goPTerm pat

 29 |                 <*> goPTerm argTy

 30 |                 <*> goPTerm scope

 31 |       >>= f

 32 |     goPTerm (PLet fc x pat nTy nVal scope alts) =

 33 |       PLet fc x <$> goPTerm pat

 34 |                 <*> goPTerm nTy

 35 |                 <*> goPTerm nVal

 36 |                 <*> goPTerm scope

 37 |                 <*> goPClauses alts

 38 |       >>= f

 39 |     goPTerm (PCase fc opts x xs) =

 40 |       PCase fc <$> goPFnOpts opts

 41 |                <*> goPTerm x

 42 |                <*> goPClauses xs

 43 |       >>= f

 44 |     goPTerm (PLocal fc xs scope) =

 45 |       PLocal fc <$> traverse (traverse goPDecl) xs

 46 |                 <*> goPTerm scope

 47 |       >>= f

 48 |     goPTerm (PUpdate fc xs) =

 49 |       PUpdate fc <$> goPFieldUpdates xs

 50 |       >>= f

 51 |     goPTerm (PApp fc x y) =

 52 |       PApp fc <$> goPTerm x

 53 |               <*> goPTerm y

 54 |       >>= f

 55 |     goPTerm (PWithApp fc x y) =

 56 |       PWithApp fc <$> goPTerm x

 57 |                   <*> goPTerm y

 58 |       >>= f

 59 |     goPTerm (PAutoApp fc x y) =

 60 |       PAutoApp fc <$> goPTerm x

 61 |                          <*> goPTerm y

 62 |       >>= f

 63 |     goPTerm (PNamedApp fc x n y) =

 64 |       PNamedApp fc <$> goPTerm x

 65 |                    <*> pure n

 66 |                    <*> goPTerm y

 67 |       >>= f

 68 |     goPTerm (PDelayed fc x y) =

 69 |       PDelayed fc x <$> goPTerm y

 70 |       >>= f

 71 |     goPTerm (PDelay fc x) =

 72 |       PDelay fc <$> goPTerm x

 73 |       >>= f

 74 |     goPTerm (PForce fc x) =

 75 |       PForce fc <$> goPTerm x

 76 |       >>= f

 77 |     goPTerm t@(PSearch {}) = f t

 78 |     goPTerm t@(PPrimVal {}) = f t

 79 |     goPTerm (PQuote fc x) =

 80 |       PQuote fc <$> goPTerm x

 81 |       >>= f

 82 |     goPTerm t@(PQuoteName {}) = f t

 83 |     goPTerm (PQuoteDecl fc x) =

 84 |       PQuoteDecl fc <$> goPDecls x

 85 |       >>= f

 86 |     goPTerm (PUnquote fc x) =

 87 |       PUnquote fc <$> goPTerm x

 88 |       >>= f

 89 |     goPTerm (PRunElab fc x) =

 90 |       PRunElab fc <$> goPTerm x

 91 |       >>= f

 92 |     goPTerm t@(PHole {}) = f t

 93 |     goPTerm t@(PType {}) = f t

 94 |     goPTerm (PAs fc nameFC x pat) =

 95 |       PAs fc nameFC x <$> goPTerm pat

 96 |       >>= f

 97 |     goPTerm (PDotted fc x) =

 98 |       PDotted fc <$> goPTerm x

 99 |       >>= f

100 |     goPTerm t@(PImplicit {}) = f t

101 |     goPTerm t@(PInfer {}) = f t

102 |     goPTerm (POp fc bind op right) =

103 |       POp fc

104 |           <$> traverse goOpBinder bind

105 |           <*> pure op

106 |           <*> goPTerm right

107 |       >>= f

108 |     goPTerm (PPrefixOp fc x y) =

109 |       PPrefixOp fc x <$> goPTerm y

110 |       >>= f

111 |     goPTerm (PSectionL fc x y) =

112 |       PSectionL fc x <$> goPTerm y

113 |       >>= f

114 |     goPTerm (PSectionR fc x y) =

115 |       PSectionR fc <$> goPTerm x

116 |                    <*> pure y

117 |       >>= f

118 |     goPTerm (PEq fc x y) =

119 |       PEq fc <$> goPTerm x

120 |              <*> goPTerm y

121 |       >>= f

122 |     goPTerm (PBracketed fc x) =

123 |       PBracketed fc <$> goPTerm x

124 |       >>= f

125 |     goPTerm (PString fc x ys) =

126 |       PString fc x <$> goPStrings ys

127 |       >>= f

128 |     goPTerm (PMultiline fc x y zs) =

129 |       PMultiline fc x y <$> goPStringLines zs

130 |       >>= f

131 |     goPTerm (PDoBlock fc ns xs) =

132 |       PDoBlock fc ns <$> goPDos xs

133 |       >>= f

134 |     goPTerm (PBang fc x) =

135 |       PBang fc <$> goPTerm x

136 |       >>= f

137 |     goPTerm (PIdiom fc ns x) =

138 |       PIdiom fc ns <$> goPTerm x

139 |       >>= f

140 |     goPTerm (PList fc nilFC xs) =

141 |       PList fc nilFC <$> goPairedPTerms xs

142 |       >>= f

143 |     goPTerm (PSnocList fc nilFC xs) =

144 |       PSnocList fc nilFC <$> goPairedSnocPTerms xs

145 |       >>= f

146 |     goPTerm (PPair fc x y) =

147 |       PPair fc <$> goPTerm x

148 |                <*> goPTerm y

149 |       >>= f

150 |     goPTerm (PDPair fc opFC x y z) =

151 |       PDPair fc opFC

152 |                 <$> goPTerm x

153 |                 <*> goPTerm y

154 |                 <*> goPTerm z

155 |       >>= f

156 |     goPTerm t@(PUnit {}) = f t

157 |     goPTerm (PIfThenElse fc x y z) =

158 |       PIfThenElse fc <$> goPTerm x

159 |                      <*> goPTerm y

160 |                      <*> goPTerm z

161 |       >>= f

162 |     goPTerm (PComprehension fc x xs) =

163 |       PComprehension fc <$> goPTerm x

164 |                         <*> goPDos xs

165 |       >>= f

166 |     goPTerm (PRewrite fc x y) =

167 |       PRewrite fc <$> goPTerm x

168 |                   <*> goPTerm y

169 |       >>= f

170 |     goPTerm (PRange fc x y z) =

171 |       PRange fc <$> goPTerm x

172 |                 <*> goMPTerm y

173 |                 <*> goPTerm z

174 |       >>= f

175 |     goPTerm (PRangeStream fc x y) =

176 |       PRangeStream fc <$> goPTerm x

177 |                       <*> goMPTerm y

178 |       >>= f

179 |     goPTerm (PUnifyLog fc k x) =

180 |       PUnifyLog fc k <$> goPTerm x

181 |       >>= f

182 |     goPTerm (PPostfixApp fc rec fields) =

183 |       PPostfixApp fc <$> goPTerm rec <*> pure fields

184 |       >>= f

185 |     goPTerm (PPostfixAppPartial fc fields) =

186 |       f (PPostfixAppPartial fc fields)

187 |     goPTerm (PWithUnambigNames fc ns rhs) =

188 |       PWithUnambigNames fc ns <$> goPTerm rhs

189 |       >>= f

191 |     goOpBinder : OperatorLHSInfo (PTerm' nm) -> Core (OperatorLHSInfo (PTerm' nm))

192 |     goOpBinder (NoBinder lhs) = NoBinder <$> goPTerm lhs

193 |     goOpBinder (BindType name ty) = BindType <$> goPTerm name <*> goPTerm ty

194 |     goOpBinder (BindExpr name expr) = BindExpr <$> goPTerm name <*> goPTerm expr

195 |     goOpBinder (BindExplicitType name type expr)

196 |       = BindExplicitType <$> goPTerm name <*> goPTerm type <*> goPTerm expr

198 |     goPFieldUpdate : PFieldUpdate' nm -> Core (PFieldUpdate' nm)

199 |     goPFieldUpdate (PSetField p t)    = PSetField p <$> goPTerm t

200 |     goPFieldUpdate (PSetFieldApp p t) = PSetFieldApp p <$> goPTerm t

202 |     goPStr : PStr' nm -> Core (PStr' nm)

203 |     goPStr (StrInterp fc t) = StrInterp fc <$> goPTerm t

204 |     goPStr x                = pure x

206 |     goPDo : PDo' nm -> Core (PDo' nm)

207 |     goPDo (DoExp fc t) = DoExp fc <$> goPTerm t

208 |     goPDo (DoBind fc nameFC n c ty t) = DoBind fc nameFC n c <$> goMPTerm ty <*> goPTerm t

209 |     goPDo (DoBindPat fc t ty u cls) =

210 |       DoBindPat fc <$> goPTerm t

211 |                    <*> goMPTerm ty

212 |                    <*> goPTerm u

213 |                    <*> goPClauses cls

214 |     goPDo (DoLet fc lhsFC n c t scope) =

215 |        DoLet fc lhsFC n c <$> goPTerm t

216 |                           <*> goPTerm scope

217 |     goPDo (DoLetPat fc pat t scope cls) =

218 |        DoLetPat fc <$> goPTerm pat

219 |                    <*> goPTerm t

220 |                    <*> goPTerm scope

221 |                    <*> goPClauses cls

222 |     goPDo (DoLetLocal fc decls) = DoLetLocal fc <$> goPDecls decls

223 |     goPDo (DoRewrite fc t) = DoRewrite fc <$> goPTerm t

225 |     goPRecordDeclLet : PRecordDeclLet' nm -> Core (PRecordDeclLet' nm)

226 |     goPRecordDeclLet (RecordClaim x) = RecordClaim <$> traverse goPClaim x

227 |     goPRecordDeclLet (RecordClause x) = RecordClause <$> traverse goPClause x

229 |     goPClause : PClause' nm -> Core (PClause' nm)

230 |     goPClause (MkPatClause fc lhs rhs wh) =

231 |       MkPatClause fc <$> goPTerm lhs

232 |                      <*> goPTerm rhs

233 |                      <*> goPDecls wh

234 |     goPClause (MkWithClause fc lhs wps flags cls) =

235 |       MkWithClause fc <$> goPTerm lhs

236 |                       <*> traverseList1 goPWithProblem wps

237 |                       <*> pure flags

238 |                       <*> goPClauses cls

239 |     goPClause (MkImpossible fc lhs) = MkImpossible fc <$> goPTerm lhs

241 |     goPWithProblem : PWithProblem' nm -> Core (PWithProblem' nm)

242 |     goPWithProblem (MkPWithProblem rig wval mnm)

243 |       = MkPWithProblem rig <$> goPTerm wval <*> pure mnm

245 |     goPClaim : PClaimData' nm -> Core (PClaimData' nm)

246 |     goPClaim (MkPClaim c v opts tdecl) =

247 |       MkPClaim c v <$> goPFnOpts opts

248 |                    <*> traverse goPTypeDecl tdecl

250 |     goBasicMultiBinder : BasicMultiBinder' nm -> Core (BasicMultiBinder' nm)

251 |     goBasicMultiBinder (MkBasicMultiBinder rig names type)

252 |       = MkBasicMultiBinder rig names <$> goPTerm type

254 |     goPBinder : PBinder' nm -> Core (PBinder' nm)

255 |     goPBinder (MkPBinder info bind)

256 |       = MkPBinder <$> goPiInfo info <*> goBasicMultiBinder bind

258 |     goPBinderScope : PBinderScope' nm -> Core (PBinderScope' nm)

259 |     goPBinderScope (MkPBinderScope binder scope)

260 |       = MkPBinderScope <$> goPBinder binder <*> goPTerm scope

262 |     goPDecl : PDeclNoFC' nm -> Core (PDeclNoFC' nm)

263 |     goPDecl (PClaim claim) =

264 |       PClaim <$> goPClaim claim

265 |     goPDecl (PDef cls) = PDef <$> goPClauses cls

266 |     goPDecl (PData doc v mbt d) = PData doc v mbt <$> goPDataDecl d

267 |     goPDecl (PParameters nts ps) =

268 |       PParameters <$> either (\x => Left <$> traverseList1 (traverse goPTerm) x)

269 |                              (\x => Right <$> traverseList1 goPBinder x) nts

270 |                   <*> goPDecls ps

271 |     goPDecl (PUsing mnts ps) =

272 |       PUsing <$> goPairedPTerms mnts

273 |              <*> goPDecls ps

274 |     goPDecl (PInterface v mnts n doc nrts ns mn ps) =

275 |       PInterface v <$> goPairedPTerms mnts

276 |                    <*> pure n

277 |                    <*> pure doc

278 |                    <*> traverse goBasicMultiBinder nrts

279 |                    <*> pure ns

280 |                    <*> pure mn

281 |                    <*> goPDecls ps

282 |     goPDecl (PImplementation v opts p is cs n ts mn ns mps) =

283 |       PImplementation v opts p <$> traverse (traverse (traverse goPTerm)) is

284 |                                <*> goPairedPTerms cs

285 |                                <*> pure n

286 |                                <*> goPTerms ts

287 |                                <*> pure mn

288 |                                <*> pure ns

289 |                                <*> goMPDecls mps

290 |     goPDecl (PRecord doc v tot (MkPRecord n nts opts mn fs)) =

291 |       pure $ PRecord doc v tot !(MkPRecord n <$> traverse goPBinder nts

292 |                                              <*> pure opts

293 |                                              <*> pure mn

294 |                                              <*> goPFields fs)

295 |     goPDecl (PRecord doc v tot (MkPRecordLater n nts)) =

296 |       pure $ PRecord doc v tot (MkPRecordLater n !(traverse goPBinder nts))

297 |     goPDecl (PFail msg ps) = PFail msg <$> goPDecls ps

298 |     goPDecl (PMutual ps) = PMutual <$> goPDecls ps

299 |     goPDecl (PFixity p) = pure (PFixity p)

300 |     goPDecl (PNamespace strs ps) = PNamespace strs <$> goPDecls ps

301 |     goPDecl (PTransform n a b) = PTransform n <$> goPTerm a <*> goPTerm b

302 |     goPDecl (PRunElabDecl a) = PRunElabDecl <$> goPTerm a

303 |     goPDecl (PDirective d) = pure (PDirective d)

304 |     goPDecl p@(PBuiltin {}) = pure p

306 |     goPTypeDecl : PTypeDeclData' nm -> Core (PTypeDeclData' nm)

307 |     goPTypeDecl (MkPTy n d t) = MkPTy n d <$> goPTerm t

309 |     goPDataDecl : PDataDecl' nm -> Core (PDataDecl' nm)

310 |     goPDataDecl (MkPData fc n t opts tdecls) =

311 |       MkPData fc n <$> goMPTerm t

312 |                    <*> pure opts

313 |                    <*> goPTypeDecls tdecls

314 |     goPDataDecl (MkPLater fc n t) = MkPLater fc n <$> goPTerm t

316 |     goPiInfo : PiInfo (PTerm' nm) -> Core (PiInfo (PTerm' nm))

317 |     goPiInfo (DefImplicit t) = DefImplicit <$> goPTerm t

318 |     goPiInfo t = pure t

320 |     goPFnOpt : PFnOpt' nm -> Core (PFnOpt' nm)

321 |     goPFnOpt o@(IFnOpt {}) = pure o

322 |     goPFnOpt (PForeign ts) = PForeign <$> goPTerms ts

323 |     goPFnOpt (PForeignExport ts) = PForeignExport <$> goPTerms ts

325 |     -- Traversable stuff. Inlined for termination checking.

327 |     goMPTerm : Maybe (PTerm' nm) -> Core (Maybe $ PTerm' nm)

328 |     goMPTerm Nothing  = pure Nothing

329 |     goMPTerm (Just t) = Just <$> goPTerm t

331 |     goPTerms : List (PTerm' nm) -> Core (List $ PTerm' nm)

332 |     goPTerms []        = pure []

333 |     goPTerms (t :: ts) = (::) <$> goPTerm t <*> goPTerms ts

335 |     goPairedPTerms : List (x, PTerm' nm) -> Core (List (x, PTerm' nm))

336 |     goPairedPTerms []             = pure []

337 |     goPairedPTerms ((a, t) :: ts) =

338 |        (::) . MkPair a <$> goPTerm t

339 |                        <*> goPairedPTerms ts

341 |     goPairedSnocPTerms : SnocList (x, PTerm' nm) -> Core (SnocList (x, PTerm' nm))

342 |     goPairedSnocPTerms [<]            = pure [<]

343 |     goPairedSnocPTerms (ts :< (a, t)) =

344 |        (:<) <$> goPairedSnocPTerms ts

345 |             <*> MkPair a <$> goPTerm t

347 |     go3TupledPTerms : List (x, y, PTerm' nm) -> Core (List (x, y, PTerm' nm))

348 |     go3TupledPTerms [] = pure []

349 |     go3TupledPTerms ((a, b, t) :: ts) =

350 |       (::) . (\ c => (a, b, c)) <$> goPTerm t

351 |                                 <*> go3TupledPTerms ts

353 |     go4TupledPTerms : List (x, y, PiInfo (PTerm' nm), PTerm' nm) ->

354 |                       Core (List (x, y, PiInfo (PTerm' nm), PTerm' nm))

355 |     go4TupledPTerms [] = pure []

356 |     go4TupledPTerms ((a, b, p, t) :: ts) =

357 |       (\ p, d, ts => (a, b, p, d) :: ts) <$> goPiInfo p

358 |                                          <*> goPTerm t

359 |                                          <*> go4TupledPTerms ts

361 |     goPStringLines : List (List (PStr' nm)) -> Core (List (List (PStr' nm)))

362 |     goPStringLines []        = pure []

363 |     goPStringLines (line :: lines) = (::) <$> goPStrings line <*> goPStringLines lines

365 |     goPStrings : List (PStr' nm) -> Core (List (PStr' nm))

366 |     goPStrings []        = pure []

367 |     goPStrings (str :: strs) = (::) <$> goPStr str <*> goPStrings strs

369 |     goPDos : List (PDo' nm) -> Core (List (PDo' nm))

370 |     goPDos []        = pure []

371 |     goPDos (d :: ds) = (::) <$> goPDo d <*> goPDos ds

373 |     goPClauses : List (PClause' nm) -> Core (List (PClause' nm))

374 |     goPClauses []          = pure []

375 |     goPClauses (cl :: cls) = (::) <$> goPClause cl <*> goPClauses cls

377 |     goMPDecls : Maybe (List (PDecl' nm)) -> Core (Maybe (List (PDecl' nm)))

378 |     goMPDecls Nothing   = pure Nothing

379 |     goMPDecls (Just ps) = Just <$> goPDecls ps

381 |     goPDecls : List (PDecl' nm) -> Core (List (PDecl' nm))

382 |     goPDecls []          = pure []

383 |     goPDecls (d :: ds) = (::) <$> traverse goPDecl d <*> goPDecls ds

385 |     goPFieldUpdates : List (PFieldUpdate' nm) -> Core (List (PFieldUpdate' nm))

386 |     goPFieldUpdates []          = pure []

387 |     goPFieldUpdates (fu :: fus) = (::) <$> goPFieldUpdate fu <*> goPFieldUpdates fus

389 |     goPFields : List (PField' nm) -> Core (List (PField' nm))

390 |     goPFields []        = pure []

391 |     goPFields (f :: fs) = (::) <$> traverse (traverse goPTerm) f <*> goPFields fs

393 |     goPFnOpts : List (PFnOpt' nm) -> Core (List (PFnOpt' nm))

394 |     goPFnOpts []        = pure []

395 |     goPFnOpts (o :: os) = (::) <$> goPFnOpt o <*> goPFnOpts os

397 |     goPTypeDecls : List (PTypeDecl' nm) -> Core (List (PTypeDecl' nm))

398 |     goPTypeDecls []        = pure []

399 |     goPTypeDecls (t :: ts) = (::) <$> traverse goPTypeDecl t <*> goPTypeDecls ts

402 | mapPTerm : (PTerm' nm -> PTerm' nm) -> PTerm' nm -> PTerm' nm

403 | mapPTerm f = goPTerm where

405 |   mutual

407 |     goPTerm : PTerm' nm -> PTerm' nm

408 |     goPTerm t@(PRef {}) = f t

409 |     goPTerm (Forall binderScope)

410 |       = Forall (map (mapSnd f) binderScope)

411 |     goPTerm (NewPi binderScope)

412 |       = NewPi (map goPBinderScope binderScope)

413 |     goPTerm (PPi fc x info z argTy retTy)

414 |       = f $ PPi fc x (goPiInfo info) z (goPTerm argTy) (goPTerm retTy)

415 |     goPTerm (PLam fc x info z argTy scope)

416 |       = f $ PLam fc x (goPiInfo info) z (goPTerm argTy) (goPTerm scope)

417 |     goPTerm (PLet fc x pat nTy nVal scope alts)

418 |       = f $ PLet fc x (goPTerm pat) (goPTerm nTy) (goPTerm nVal) (goPTerm scope) (goPClause <$> alts)

419 |     goPTerm (PCase fc opts x xs)

420 |       = f $ PCase fc (goPFnOpt <$>  opts) (goPTerm x) (goPClause <$> xs)

421 |     goPTerm (PLocal fc xs scope)

422 |       = f $ PLocal fc (map goPDecl <$> xs) (goPTerm scope)

423 |     goPTerm (PUpdate fc xs)

424 |       = f $ PUpdate fc (goPFieldUpdate <$> xs)

425 |     goPTerm (PApp fc x y)

426 |       = f $ PApp fc (goPTerm x) (goPTerm y)

427 |     goPTerm (PWithApp fc x y)

428 |       = f $ PWithApp fc (goPTerm x) (goPTerm y)

429 |     goPTerm (PAutoApp fc x y)

430 |       = f $ PAutoApp fc (goPTerm x) (goPTerm y)

431 |     goPTerm (PNamedApp fc x n y)

432 |       = f $ PNamedApp fc (goPTerm x) n (goPTerm y)

433 |     goPTerm (PDelayed fc x y)

434 |       = f $ PDelayed fc x (goPTerm y)

435 |     goPTerm (PDelay fc x)

436 |       = f $ PDelay fc $ goPTerm x

437 |     goPTerm (PForce fc x)

438 |       = f $ PForce fc $ goPTerm x

439 |     goPTerm t@(PSearch {}) = f t

440 |     goPTerm t@(PPrimVal {}) = f t

441 |     goPTerm (PQuote fc x)

442 |       = f $ PQuote fc $ goPTerm x

443 |     goPTerm t@(PQuoteName {}) = f t

444 |     goPTerm (PQuoteDecl fc x)

445 |       = f $ PQuoteDecl fc (map goPDecl <$> x)

446 |     goPTerm (PUnquote fc x)

447 |       = f $ PUnquote fc $ goPTerm x

448 |     goPTerm (PRunElab fc x)

449 |       = f $ PRunElab fc $ goPTerm x

450 |     goPTerm t@(PHole {}) = f t

451 |     goPTerm t@(PType {}) = f t

452 |     goPTerm (PAs fc nameFC x pat)

453 |       = f $ PAs fc nameFC x $ goPTerm pat

454 |     goPTerm (PDotted fc x)

455 |       = f $ PDotted fc $ goPTerm x

456 |     goPTerm t@(PImplicit {}) = f t

457 |     goPTerm t@(PInfer {}) = f t

458 |     goPTerm (POp fc autoBindInfo opName z)

459 |       = f $ POp fc (map (map f) autoBindInfo) opName (goPTerm z)

460 |     goPTerm (PPrefixOp fc x y)

461 |       = f $ PPrefixOp fc x $ goPTerm y

462 |     goPTerm (PSectionL fc x y)

463 |       = f $ PSectionL fc x $ goPTerm y

464 |     goPTerm (PSectionR fc x y)

465 |       = f $ PSectionR fc (goPTerm x) y

466 |     goPTerm (PEq fc x y)

467 |       = f $ PEq fc (goPTerm x) (goPTerm y)

468 |     goPTerm (PBracketed fc x)

469 |       = f $ PBracketed fc $ goPTerm x

470 |     goPTerm (PString fc x ys)

471 |       = f $ PString fc x $ goPStr <$> ys

472 |     goPTerm (PMultiline fc x y zs)

473 |       = f $  PMultiline fc x y $ map (map goPStr) zs

474 |     goPTerm (PDoBlock fc ns xs)

475 |       = f $ PDoBlock fc ns $ goPDo <$> xs

476 |     goPTerm (PBang fc x)

477 |       = f $ PBang fc $ goPTerm x

478 |     goPTerm (PIdiom fc ns x)

479 |       = f $ PIdiom fc ns $ goPTerm x

480 |     goPTerm (PList fc nilFC xs)

481 |       = f $ PList fc nilFC $ goPairedPTerms xs

482 |     goPTerm (PSnocList fc nilFC xs)

483 |       = f $ PSnocList fc nilFC $ goPairedSnocPTerms xs

484 |     goPTerm (PPair fc x y)

485 |       = f $ PPair fc (goPTerm x) (goPTerm y)

486 |     goPTerm (PDPair fc opFC x y z)

487 |       = f $ PDPair fc opFC (goPTerm x) (goPTerm y) (goPTerm z)

488 |     goPTerm t@(PUnit {}) = f t

489 |     goPTerm (PIfThenElse fc x y z)

490 |       = f $ PIfThenElse fc (goPTerm x) (goPTerm y) (goPTerm z)

491 |     goPTerm (PComprehension fc x xs)

492 |       = f $ PComprehension fc (goPTerm x) (goPDo <$> xs)

493 |     goPTerm (PRewrite fc x y)

494 |       = f $ PRewrite fc (goPTerm x) (goPTerm y)

495 |     goPTerm (PRange fc x y z)

496 |       = f $ PRange fc (goPTerm x) (map goPTerm y) (goPTerm z)

497 |     goPTerm (PRangeStream fc x y)

498 |       = f $ PRangeStream fc (goPTerm x) (map goPTerm y)

499 |     goPTerm (PUnifyLog fc k x)

500 |       = f $ PUnifyLog fc k (goPTerm x)

501 |     goPTerm (PPostfixApp fc rec fields)

502 |       = f $ PPostfixApp fc (goPTerm rec) fields

503 |     goPTerm t@(PPostfixAppPartial fc fields) = f t

504 |     goPTerm (PWithUnambigNames fc ns rhs)

505 |       = f $ PWithUnambigNames fc ns (goPTerm rhs)

507 |     goPFieldUpdate : PFieldUpdate' nm -> PFieldUpdate' nm

508 |     goPFieldUpdate (PSetField p t)    = PSetField p $ goPTerm t

509 |     goPFieldUpdate (PSetFieldApp p t) = PSetFieldApp p $ goPTerm t

511 |     goPStr : PStr' nm -> PStr' nm

512 |     goPStr (StrInterp fc t) = StrInterp fc $ goPTerm t

513 |     goPStr x                = x

515 |     goPDo : PDo' nm -> PDo' nm

516 |     goPDo (DoExp fc t) = DoExp fc $ goPTerm t

517 |     goPDo (DoBind fc nameFC n c ty t) = DoBind fc nameFC n c (goPTerm <$> ty) (goPTerm t)

518 |     goPDo (DoBindPat fc t ty u cls)

519 |       = DoBindPat fc (goPTerm t) (goPTerm <$> ty) (goPTerm u) (goPClause <$> cls)

520 |     goPDo (DoLet fc lhsFC n c t scope)

521 |       = DoLet fc lhsFC n c (goPTerm t) (goPTerm scope)

522 |     goPDo (DoLetPat fc pat t scope cls)

523 |       = DoLetPat fc (goPTerm pat) (goPTerm t) (goPTerm scope) (goPClause <$> cls)

524 |     goPDo (DoLetLocal fc decls) = DoLetLocal fc $ map goPDecl <$> decls

525 |     goPDo (DoRewrite fc t) = DoRewrite fc $ goPTerm t

527 |     goPWithProblem : PWithProblem' nm -> PWithProblem' nm

528 |     goPWithProblem (MkPWithProblem rig wval mnm)= MkPWithProblem rig (goPTerm wval) mnm

530 |     goPClause : PClause' nm -> PClause' nm

531 |     goPClause (MkPatClause fc lhs rhs wh)

532 |       = MkPatClause fc (goPTerm lhs) (goPTerm rhs) (map goPDecl <$> wh)

533 |     goPClause (MkWithClause fc lhs wps flags cls)

534 |       = MkWithClause fc (goPTerm lhs) (goPWithProblem <$> wps) flags (goPClause <$> cls)

535 |     goPClause (MkImpossible fc lhs) = MkImpossible fc $ goPTerm lhs

537 |     goPClaim : PClaimData' nm -> PClaimData' nm

538 |     goPClaim (MkPClaim c v opts tdecl) = MkPClaim c v (goPFnOpt <$> opts) (map goPTypeDecl tdecl)

540 |     goPBinderScope : PBinderScope' nm -> PBinderScope' nm

541 |     goPBinderScope (MkPBinderScope binder scope)

542 |       = MkPBinderScope (goPBinder binder) (goPTerm scope)

544 |     goPDecl : PDeclNoFC' nm -> PDeclNoFC' nm

545 |     goPDecl (PClaim claim)

546 |       = PClaim $ goPClaim claim

547 |     goPDecl (PDef cls) = PDef $ (map goPClause) cls

548 |     goPDecl (PData doc v mbt d) = PData doc v mbt $ goPDataDecl d

549 |     goPDecl (PParameters nts ps)

550 |       = PParameters (bimap (map (map goPTerm)) (map goPBinder) nts) (map goPDecl <$> ps)

551 |     goPDecl (PUsing mnts ps)

552 |       = PUsing (goPairedPTerms mnts) (map goPDecl <$> ps)

553 |     goPDecl (PInterface v mnts n doc nrts ns mn ps)

554 |       = PInterface v (goPairedPTerms mnts) n doc (goBasicMultiBinder <$> nrts) ns mn (map goPDecl <$> ps)

555 |     goPDecl (PImplementation v opts p is cs n ts mn ns mps)

556 |       = PImplementation v opts p (map (map (map goPTerm)) is) (goPairedPTerms cs)

557 |            n (goPTerm <$> ts) mn ns (map (map goPDecl <$>) mps)

558 |     goPDecl (PRecord doc v tot (MkPRecord n nts opts mn fs))

559 |       = PRecord doc v tot

560 |           (MkPRecord n (map goPBinder nts) opts mn (map (map (map goPTerm)) fs))

561 |     goPDecl (PRecord doc v tot (MkPRecordLater n nts))

562 |       = PRecord doc v tot (MkPRecordLater n (goPBinder <$> nts ))

563 |     goPDecl (PFail msg ps) = PFail msg $ map goPDecl <$> ps

564 |     goPDecl (PMutual ps) = PMutual $ map (map goPDecl) ps

565 |     goPDecl (PFixity p) = PFixity p

566 |     goPDecl (PNamespace strs ps) = PNamespace strs $ map goPDecl <$> ps

567 |     goPDecl (PTransform n a b) = PTransform n (goPTerm a) (goPTerm b)

568 |     goPDecl (PRunElabDecl a) = PRunElabDecl $ goPTerm a

569 |     goPDecl (PDirective d) = PDirective d

570 |     goPDecl p@(PBuiltin {}) = p

572 |     goPBinder : PBinder' nm -> PBinder' nm

573 |     goPBinder (MkPBinder info bind) = MkPBinder (goPiInfo info) (goBasicMultiBinder bind)

575 |     goBasicMultiBinder : BasicMultiBinder' nm -> BasicMultiBinder' nm

576 |     goBasicMultiBinder (MkBasicMultiBinder rig names type)

577 |       = MkBasicMultiBinder rig names (goPTerm type)

579 |     goPTypeDecl : PTypeDeclData' nm -> PTypeDeclData' nm

580 |     goPTypeDecl (MkPTy n d t) = MkPTy n d $ goPTerm t

582 |     goPDataDecl : PDataDecl' nm -> PDataDecl' nm

583 |     goPDataDecl (MkPData fc n t opts tdecls)

584 |       = MkPData fc n (map goPTerm t) opts (map goPTypeDecl <$> tdecls)

585 |     goPDataDecl (MkPLater fc n t) = MkPLater fc n $ goPTerm t

587 |     goPRecordDeclLet : PRecordDeclLet' nm -> PRecordDeclLet' nm

588 |     goPRecordDeclLet (RecordClaim claim) = RecordClaim $ map goPClaim claim

589 |     goPRecordDeclLet (RecordClause clause) = RecordClause $ map goPClause clause

591 |     goPiInfo : PiInfo (PTerm' nm) -> PiInfo (PTerm' nm)

592 |     goPiInfo (DefImplicit t) = DefImplicit $ goPTerm t

593 |     goPiInfo t = t

595 |     goPFnOpt : PFnOpt' nm -> PFnOpt' nm

596 |     goPFnOpt o@(IFnOpt {}) = o

597 |     goPFnOpt (PForeign ts) = PForeign $ goPTerm <$> ts

598 |     goPFnOpt (PForeignExport ts) = PForeignExport $ goPTerm <$> ts

600 |     goPairedPTerms : List (x, PTerm' nm) -> List (x, PTerm' nm)

601 |     goPairedPTerms [] = []

602 |     goPairedPTerms ((a, t) :: ts) = (a, goPTerm t) :: goPairedPTerms ts

604 |     goPairedSnocPTerms : SnocList (x, PTerm' nm) -> SnocList (x, PTerm' nm)

605 |     goPairedSnocPTerms [<] = [<]

606 |     goPairedSnocPTerms (ts :< (a, t)) = goPairedSnocPTerms ts :< (a, goPTerm t)

608 |     goImplicits : List (x, ImpParameter' (PTerm' nm)) -> List (x, ImpParameter' (PTerm' nm))

609 |     goImplicits [] = []

610 |     goImplicits ((a, t) :: ts) = (a,map (map f) t) :: goImplicits ts

617 | substFC : FC -> PTerm' nm -> PTerm' nm

618 | substFC fc = mapPTerm $ \case

619 |   PRef _ x => PRef fc x

620 |   NewPi x => NewPi (setFC fc x)

621 |   Forall x => Forall (setFC fc x)

622 |   PPi _ x y z argTy retTy => PPi fc x y z argTy retTy

623 |   PLam _ x y pat argTy scope => PLam fc x y pat argTy scope

624 |   PLet _ x pat nTy nVal scope alts => PLet fc x pat nTy nVal scope alts

625 |   PCase _ opts x xs => PCase fc opts x xs

626 |   PLocal _ xs scope => PLocal fc xs scope

627 |   PUpdate _ xs => PUpdate fc xs

628 |   PApp _ x y => PApp fc x y

629 |   PWithApp _ x y => PWithApp fc x y

630 |   PNamedApp _ x n y => PNamedApp fc x n y

631 |   PAutoApp _ x y => PAutoApp fc x y

632 |   PDelayed _ x y => PDelayed fc x y

633 |   PDelay _ x => PDelay fc x

634 |   PForce _ x => PForce fc x

635 |   PSearch _ depth => PSearch fc depth

636 |   PPrimVal _ x => PPrimVal fc x

637 |   PQuote _ x => PQuote fc x

638 |   PQuoteName _ n => PQuoteName fc n

639 |   PQuoteDecl _ xs => PQuoteDecl fc xs

640 |   PUnquote _ x => PUnquote fc x

641 |   PRunElab _ x => PRunElab fc x

642 |   PHole _ bracket holename => PHole fc bracket holename

643 |   PType _ => PType fc

644 |   PAs _ _ n pattern => PAs fc fc n pattern

645 |   PDotted _ x => PDotted fc x

646 |   PImplicit _ => PImplicit fc

647 |   PInfer _ => PInfer fc

648 |   POp _ ab nm r => POp fc (setFC fc ab) nm r

649 |   PPrefixOp _ x y => PPrefixOp fc (setFC fc x) y

650 |   PSectionL _ x y => PSectionL fc (setFC fc x) y

651 |   PSectionR _ x y => PSectionR fc x (setFC fc y)

652 |   PEq _ x y => PEq fc x y

653 |   PBracketed _ x => PBracketed fc x

654 |   PString _ x ys => PString fc x ys

655 |   PMultiline _ x y zs => PMultiline fc x y zs

656 |   PDoBlock _ x xs => PDoBlock fc x xs

657 |   PBang _ x => PBang fc x

658 |   PIdiom _ x y => PIdiom fc x y

659 |   PList _ _ xs => PList fc fc xs

660 |   PSnocList _ _ sx => PSnocList fc fc sx

661 |   PPair _ x y => PPair fc x y

662 |   PDPair _ _ x y z => PDPair fc fc x y z

663 |   PUnit _ => PUnit fc

664 |   PIfThenElse _ x y z => PIfThenElse fc x y z

665 |   PComprehension _ x xs => PComprehension fc x xs

666 |   PRewrite _ x y => PRewrite fc x y

667 |   PRange _ x y z => PRange fc x y z

668 |   PRangeStream _ x y => PRangeStream fc x y

669 |   PPostfixApp _ x xs => PPostfixApp fc x xs

670 |   PPostfixAppPartial _ xs => PPostfixAppPartial fc xs

671 |   PUnifyLog _ x y => PUnifyLog fc x y

672 |   PWithUnambigNames _ xs x => PWithUnambigNames fc xs x