0 | module Idris.Resugar

  2 | import Core.Env

  4 | import Idris.Syntax

  5 | import Idris.Syntax.Traversals

  7 | import TTImp.TTImp

  8 | import TTImp.TTImp.Functor

  9 | import TTImp.Unelab

 10 | import TTImp.Utils

 12 | import Data.String

 13 | import Libraries.Data.ANameMap

 15 | %default covering

 22 | unbracketApp : PTerm' nm -> PTerm' nm

 23 | unbracketApp (PBracketed _ tm@(PApp {})) = tm

 24 | unbracketApp tm = tm

 27 | mkOp : {auto s : Ref Syn SyntaxInfo} ->

 28 |        IPTerm -> Core IPTerm

 29 | mkOp tm@(PApp fc (PApp _ (PRef opFC kn) x) y)

 30 |   = do syn <- get Syn

 31 |        let raw = rawName kn

 32 |        let pop = if isOpName raw then OpSymbols else Backticked

 33 |        -- to check if the name is an operator we use the root name as a basic

 34 |        -- user name. This is because if the name is qualified with the namespace

 35 |        -- looking the fixity context will fail. A qualified operator would look

 36 |        -- like this: `M1.M2.(++)` which would not match its fixity namesapce

 37 |        -- that looks like this: `M1.M2.infixl.(++)`. However, since we only want

 38 |        -- to know if the name is an operator or not, it's enough to check

 39 |        -- that the fixity context contains the name `(++)`

 40 |        let rootName = UN (Basic (nameRoot raw))

 41 |        let asOp = POp fc (MkFCVal opFC

 42 |                 $ NoBinder (unbracketApp x)) (MkFCVal opFC (pop kn)) (unbracketApp y)

 43 |        if not (null (lookupName rootName (infixes syn)))

 44 |          then pure asOp

 45 |          else case dropNS raw of

 46 |            DN str _ => pure $ ifThenElse (isOpUserName (Basic str)) asOp tm

 47 |            _ => pure tm

 48 | mkOp tm@(PApp fc (PRef opFC kn) x)

 49 |   = do syn <- get Syn

 50 |        let n = rawName kn

 51 |        let asOp = PSectionR fc (unbracketApp x) (MkFCVal opFC $ OpSymbols kn)

 52 |        if not (null $ lookupName (UN $ Basic (nameRoot n)) (infixes syn))

 53 |          then pure asOp

 54 |          else case dropNS n of

 55 |            DN str _ => pure $ ifThenElse (isOpUserName (Basic str)) asOp tm

 56 |            _ => pure tm

 57 | mkOp tm = pure tm

 59 | mkSectionL : {auto c : Ref Ctxt Defs} ->

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

 61 |              IPTerm -> Core IPTerm

 62 | mkSectionL tm@(PLam fc rig info (PRef _ bd) ty

 63 |                  (PApp _ (PApp _ (PRef opFC kn) (PRef _ (MkKindedName (Just Bound) nm _))) x))

 64 |   = do log "resugar.sectionL" 30 $ "SectionL candidate: \{show tm}"

 65 |        let True = bd.fullName == nm

 66 |          | _ => pure tm

 67 |        syn <- get Syn

 68 |        let n = rawName kn

 69 |        let asOp = PSectionL fc (MkFCVal opFC $ OpSymbols kn) (unbracketApp x)

 70 |        if not (null $ lookupName (UN $ Basic (nameRoot n)) (fixities syn))

 71 |          then pure asOp

 72 |          else case dropNS n of

 73 |            DN str _ => pure $ ifThenElse (isOpUserName (Basic str)) asOp tm

 74 |            _ => pure tm

 75 | mkSectionL tm = pure tm

 78 | addBracket : FC -> PTerm' nm -> PTerm' nm

 79 | addBracket fc tm = if needed tm then PBracketed fc tm else tm

 80 |   where

 81 |     needed : PTerm' nm -> Bool

 82 |     needed (PBracketed {}) = False

 83 |     needed (PRef {}) = False

 84 |     needed (PPair {}) = False

 85 |     needed (PDPair {}) = False

 86 |     needed (PUnit {}) = False

 87 |     needed (PComprehension {}) = False

 88 |     needed (PList {}) = False

 89 |     needed (PSnocList {}) = False

 90 |     needed (PRange {}) = False

 91 |     needed (PRangeStream {}) = False

 92 |     needed (PPrimVal {}) = False

 93 |     needed (PIdiom {}) = False

 94 |     needed (PBang {}) = False

 95 |     needed tm = True

 97 | bracket : {auto c : Ref Ctxt Defs} ->

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

 99 |           (outer : Nat) -> (inner : Nat) ->

100 |           IPTerm -> Core IPTerm

101 | bracket outer inner tm

102 |     = do tm <- mkOp tm

103 |          tm <- mkSectionL tm

104 |          if outer > inner

105 |             then pure (addBracket emptyFC tm)

106 |             else pure tm

108 | startPrec : Nat

109 | startPrec = 0

111 | tyPrec : Nat

112 | tyPrec = 1

114 | appPrec : Nat

115 | appPrec = 999

117 | argPrec : Nat

118 | argPrec = 1000

120 | showImplicits : {auto c : Ref Ctxt Defs} ->

121 |                 Core Bool

122 | showImplicits = showImplicits <$> getPPrint

124 | showFullEnv : {auto c : Ref Ctxt Defs} ->

125 |               Core Bool

126 | showFullEnv = showFullEnv <$> getPPrint

128 | unbracket : PTerm' nm -> PTerm' nm

129 | unbracket (PBracketed _ tm) = tm

130 | unbracket tm = tm

133 | extractNat : Nat -> IPTerm -> Maybe Nat

134 | extractNat acc tm = case tm of

135 |   PRef _ (MkKindedName _ (NS ns (UN (Basic n))) rn) =>

136 |     do guard (n == "Z")

137 |        guard (ns == typesNS || ns == preludeNS)

138 |        pure acc

139 |   PApp _ (PRef _ (MkKindedName _ (NS ns (UN (Basic n))) rn)) k => case n of

140 |     "S" => do guard (ns == typesNS || ns == preludeNS)

141 |               extractNat (1 + acc) k

142 |     "fromInteger" => extractNat acc k

143 |     _ => Nothing

144 |   PPrimVal _ (BI n) => do guard (0 <= n)

145 |                           pure (acc + integerToNat n)

146 |   PBracketed _ k    => extractNat acc k

147 |   _                 => Nothing

150 | extractInteger : IPTerm -> Maybe Integer

151 | extractInteger tm = case tm of

152 |   PApp _ (PRef _ (MkKindedName _ (NS ns (UN (Basic n))) rn)) k => case n of

153 |     "fromInteger" => extractInteger k

154 |     "negate"      => negate <$> extractInteger k

155 |     _ => Nothing

156 |   PPrimVal _ (BI i) => pure i

157 |   PBracketed _ t    => extractInteger t

158 |   _                 => Nothing

161 | extractDouble : IPTerm -> Maybe Double

162 | extractDouble tm = case tm of

163 |   PApp _ (PRef _ (MkKindedName _ (NS ns (UN (Basic n))) rn)) k => case n of

164 |     "fromDouble" => extractDouble k

165 |     "negate"     => negate <$> extractDouble k

166 |     _ => Nothing

167 |   PPrimVal _ (Db d) => pure d

168 |   PBracketed _ t    => extractDouble t

169 |   _                 => Nothing

173 | sugarPrimAppM : {auto c : Ref Ctxt Defs} ->

174 |                 IPTerm -> Core (Maybe IPTerm)

175 | sugarPrimAppM (PApp fc (PApp fc' (PRef opFC (MkKindedName nt (UN $ Basic n) rn)) l) r) = do

176 |   defs <- get Ctxt

177 |   case definition <$> !(lookupCtxtExact rn defs.gamma) of

178 |       Just (Builtin {arity=2} f) =>

179 |          let nm' = (UN $ Basic $ show @{Sugared} f)

180 |              l'  = (MkFCVal fc' $ NoBinder l)

181 |              op' = (MkFCVal opFC (OpSymbols $ (MkKindedName nt nm' nm')))

182 |              in  do log "resugar.var" 80

183 |                           "Resugaring primitive op \{show n} to \{show nm'}"

184 |                     pure . Just $ POp fc l' op' r

185 |       _ => pure Nothing

186 | sugarPrimAppM _ = pure Nothing

188 | sugarPrimApp : {auto c : Ref Ctxt Defs} ->

189 |                IPTerm -> Core IPTerm

190 | sugarPrimApp tm = pure $ fromMaybe tm !(sugarPrimAppM tm)

193 |   ||| Put the special names (Nil, ::, Pair, Z, S, etc) back as syntax

195 |   sugarAppM : IPTerm -> Maybe IPTerm

196 |   sugarAppM (PApp fc (PApp _ (PApp _ (PRef opFC (MkKindedName nt (NS ns nm) rn)) l) m) r) =

197 |     case nameRoot nm of

198 |       "rangeFromThenTo" => pure $ PRange fc (unbracket l) (Just $ unbracket m) (unbracket r)

199 |       _ => Nothing

200 |   sugarAppM (PApp fc (PApp _ (PRef opFC (MkKindedName nt (NS ns nm) rn)) l) r) =

201 |     if builtinNS == ns then

202 |       case nameRoot nm of

203 |         "Pair"   => pure $ PPair fc (unbracket l) (unbracket r)

204 |         "MkPair" => pure $ PPair fc (unbracket l) (unbracket r)

205 |         "Equal"  => pure $ PEq fc (unbracket l) (unbracket r)

206 |         "==="    => pure $ PEq fc (unbracket l) (unbracket r)

207 |         "~=~"    => pure $ PEq fc (unbracket l) (unbracket r)

208 |         _        => Nothing

209 |     else if dpairNS == ns then

210 |       case nameRoot nm of

211 |         "DPair"  => case unbracket r of

212 |           PLam _ _ _ n _ r' => pure $ PDPair fc opFC n (unbracket l) (unbracket r')

213 |           _                 => Nothing

214 |         "MkDPair" => pure $ PDPair fc opFC (unbracket l) (PImplicit opFC) (unbracket r)

215 |         _                 => Nothing

216 |     else

217 |       case nameRoot nm of

218 |         "::" => case sugarApp (unbracket r) of

219 |           PList fc nilFC xs => pure $ PList fc nilFC ((opFC, unbracketApp l) :: xs)

220 |           _ => Nothing

221 |         ":<" => case sugarApp (unbracket l) of

222 |           PSnocList fc nilFC xs => pure $ PSnocList fc nilFC

223 |                                             (xs :< (opFC, unbracketApp r))

224 |           _ => Nothing

225 |         "rangeFromTo" => pure $ PRange fc (unbracket l) Nothing (unbracket r)

226 |         "rangeFromThen" => pure $ PRangeStream fc (unbracket l) (Just $ unbracket r)

227 |         _    => Nothing

228 |   sugarAppM tm =

229 |   -- refolding natural numbers if the expression is a constant

230 |     let Nothing = extractNat 0 tm

231 |           | Just k => pure $ PPrimVal (getPTermLoc tm) (BI (cast k))

232 |         Nothing = extractInteger tm

233 |           | Just k => pure $ PPrimVal (getPTermLoc tm) (BI k)

234 |         Nothing = extractDouble tm

235 |           | Just d => pure $ PPrimVal (getPTermLoc tm) (Db d)

236 |     in case tm of

237 |         PRef fc (MkKindedName nt (NS ns nm) rn) =>

238 |           if builtinNS == ns

239 |              then case nameRoot nm of

240 |                "Unit"   => pure $ PUnit fc

241 |                "MkUnit" => pure $ PUnit fc

242 |                _           => Nothing

243 |              else case nameRoot nm of

244 |                "Nil" => pure $ PList fc fc []

245 |                "Lin" => pure $ PSnocList fc fc [<]

246 |                _     => Nothing

247 |         PApp fc (PRef _ (MkKindedName nt (NS ns nm) rn)) arg =>

248 |           case nameRoot nm of

249 |             "rangeFrom" => pure $ PRangeStream fc (unbracket arg) Nothing

250 |             _           => Nothing

251 |         _ => Nothing

253 |   ||| Put the special names (Nil, ::, Pair, Z, S, etc.) back as syntax

254 |   sugarApp : IPTerm -> IPTerm

255 |   sugarApp tm = fromMaybe tm (sugarAppM tm)

258 | sugarName : Name -> String

259 | sugarName (MN n _) = "(implicit) " ++ n

260 | sugarName (PV n _) = sugarName n

261 | sugarName (DN n _) = n

262 | sugarName x = show x

264 | toPRef : FC -> KindedName -> Core IPTerm

265 | toPRef fc (MkKindedName nt fn nm) = case dropNS nm of

266 |   MN n i     => pure (sugarApp (PRef fc (MkKindedName nt fn $ MN n i)))

267 |   PV n _     => pure (sugarApp (PRef fc (MkKindedName nt fn $ n)))

268 |   DN n _     => pure (sugarApp (PRef fc (MkKindedName nt fn $ UN $ Basic n)))

269 |   Nested _ n => toPRef fc (MkKindedName nt fn n)

270 |   n          => pure (sugarApp (PRef fc (MkKindedName nt fn n)))

273 |   toPTerm : {auto c : Ref Ctxt Defs} ->

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

275 |             (prec : Nat) -> IRawImp -> Core IPTerm

276 |   toPTerm p (IVar fc nm) = do

277 |     t <- if fullNamespace !(getPPrint)

278 |       then pure $ PRef fc nm

279 |       else toPRef fc nm

280 |     log "resugar.var" 70 $

281 |       unwords [ "Resugaring", show @{Raw} nm.rawName, "to", show t]

282 |     pure t

283 |   toPTerm p (IPi fc rig Implicit n arg ret)

284 |       = do imp <- showImplicits

285 |            if imp

286 |               then do arg' <- toPTerm tyPrec arg

287 |                       ret' <- toPTerm tyPrec ret

288 |                       bracket p tyPrec (PPi fc rig Implicit n arg' ret')

289 |               else if needsBind n

290 |                       then do arg' <- toPTerm tyPrec arg

291 |                               ret' <- toPTerm tyPrec ret

292 |                               bracket p tyPrec (PPi fc rig Implicit n arg' ret')

293 |                       else toPTerm p ret

294 |     where

295 |       needsBind : Maybe Name -> Bool

296 |       needsBind (Just nm@(UN (Basic _)))

297 |           = let ret = map rawName ret

298 |                 ns = findBindableNames False [] [] ret

299 |                 allNs = findAllNames [] ret in

300 |                 (nm `elem` allNs) && not (nm `elem` (map Builtin.fst ns))

301 |       needsBind _ = False

302 |   toPTerm p (IPi fc rig pt n arg ret)

303 |       = do arg' <- toPTerm appPrec arg

304 |            ret' <- toPTerm tyPrec ret

305 |            pt' <- traverse (toPTerm argPrec) pt

306 |            bracket p tyPrec (PPi fc rig pt' n arg' ret')

307 |   toPTerm p (ILam fc rig pt mn arg sc)

308 |       = do let n = case mn of

309 |                         Nothing => UN Underscore

310 |                         Just n' => n'

311 |            imp <- showImplicits

312 |            arg' <- if imp then toPTerm tyPrec arg

313 |                           else pure (PImplicit fc)

314 |            sc' <- toPTerm startPrec sc

315 |            pt' <- traverse (toPTerm argPrec) pt

316 |            let var = PRef fc (MkKindedName (Just Bound) n n)

317 |            bracket p startPrec (PLam fc rig pt' var arg' sc')

318 |   toPTerm p (ILet fc lhsFC rig n ty val sc)

319 |       = do imp <- showImplicits

320 |            ty' <- if imp then toPTerm startPrec ty

321 |                          else pure (PImplicit fc)

322 |            val' <- toPTerm startPrec val

323 |            sc' <- toPTerm startPrec sc

324 |            let var = PRef lhsFC (MkKindedName (Just Bound) n n)

325 |            bracket p startPrec (PLet fc rig var ty' val' sc' [])

326 |   toPTerm p (ICase fc _ sc scty [PatClause _ lhs rhs])

327 |       = do sc' <- toPTerm startPrec sc

328 |            lhs' <- toPTerm startPrec lhs

329 |            rhs' <- toPTerm startPrec rhs

330 |            bracket p startPrec

331 |                    (PLet fc top lhs' (PImplicit fc) sc' rhs' [])

332 |   toPTerm p (ICase fc opts sc scty alts)

333 |       = do opts' <- traverse toPFnOpt opts

334 |            sc' <- toPTerm startPrec sc

335 |            alts' <- traverse toPClause alts

336 |            bracket p startPrec (mkIf (PCase fc opts' sc' alts'))

337 |     where

338 |       mkIf : IPTerm -> IPTerm

339 |       mkIf tm@(PCase loc opts sc

340 |                  [ MkPatClause _ (PRef _ tval) t []

341 |                  , MkPatClause _ (PRef _ fval) f []])

342 |          = if dropNS (rawName tval) == UN (Basic "True")

343 |            && dropNS (rawName fval) == UN (Basic "False")

344 |               then PIfThenElse loc sc t f

345 |               else tm

346 |       mkIf tm = tm

347 |   toPTerm p (ILocal fc ds sc)

348 |       = do ds' <- traverse toPDecl ds

349 |            sc' <- toPTerm startPrec sc

350 |            bracket p startPrec (PLocal fc (catMaybes ds') sc')

351 |   toPTerm p (ICaseLocal fc _ _ _ sc) = toPTerm p sc

352 |   toPTerm p (IUpdate fc ds f)

353 |       = do ds' <- traverse toPFieldUpdate ds

354 |            f' <- toPTerm argPrec f

355 |            bracket p startPrec (PApp fc (PUpdate fc ds') f')

356 |   toPTerm p (IApp fc fn arg)

357 |       = do arg' <- toPTerm argPrec arg

358 |            app <- toPTermApp fn [(fc, Nothing, arg')]

359 |            bracket p appPrec app

360 |   toPTerm p (IAutoApp fc fn arg)

361 |       = do arg' <- toPTerm argPrec arg

362 |            app <- toPTermApp fn [(fc, Just Nothing, arg')]

363 |            bracket p appPrec app

364 |   toPTerm p (IWithApp fc fn arg)

365 |       = do arg' <- toPTerm startPrec arg

366 |            fn' <- toPTerm startPrec fn

367 |            bracket p appPrec (PWithApp fc fn' arg')

368 |   toPTerm p (INamedApp fc fn n arg)

369 |       = do arg' <- toPTerm startPrec arg

370 |            app <- toPTermApp fn [(fc, Just (Just n), arg')]

371 |            imp <- showImplicits

372 |            if imp

373 |               then bracket p startPrec app

374 |               else mkOp app

375 |   toPTerm p (ISearch fc d) = pure (PSearch fc d)

376 |   toPTerm p (IAlternative fc _ _) = pure (PImplicit fc)

377 |   toPTerm p (IRewrite fc rule tm)

378 |       = pure (PRewrite fc !(toPTerm startPrec rule)

379 |                                !(toPTerm startPrec tm))

380 |   toPTerm p (ICoerced fc tm) = toPTerm p tm

381 |   toPTerm p (IPrimVal fc c) = pure (PPrimVal fc c)

382 |   toPTerm p (IHole fc str) = pure (PHole fc False str)

383 |   toPTerm p (IType fc) = pure (PType fc)

384 |   toPTerm p (IBindVar fc nm)

385 |     = pure (PRef fc (MkKindedName (Just Bound) nm nm))

386 |   toPTerm p (IBindHere fc _ tm) = toPTerm p tm

387 |   toPTerm p (IAs fc nameFC _ n pat) = pure (PAs fc nameFC n !(toPTerm argPrec pat))

388 |   toPTerm p (IMustUnify fc r pat) = pure (PDotted fc !(toPTerm argPrec pat))

390 |   toPTerm p (IDelayed fc r ty) = pure (PDelayed fc r !(toPTerm argPrec ty))

391 |   toPTerm p (IDelay fc tm) = pure (PDelay fc !(toPTerm argPrec tm))

392 |   toPTerm p (IForce fc tm) = pure (PForce fc !(toPTerm argPrec tm))

393 |   toPTerm p (IQuote fc tm) = pure (PQuote fc !(toPTerm argPrec tm))

394 |   toPTerm p (IQuoteName fc n) = pure (PQuoteName fc n)

395 |   toPTerm p (IQuoteDecl fc ds)

396 |       = do ds' <- traverse toPDecl ds

397 |            pure $ PQuoteDecl fc (catMaybes ds')

398 |   toPTerm p (IUnquote fc tm) = pure (PUnquote fc !(toPTerm argPrec tm))

399 |   toPTerm p (IRunElab fc _ tm) = pure (PRunElab fc !(toPTerm argPrec tm))

401 |   toPTerm p (IUnifyLog fc _ tm) = toPTerm p tm

402 |   toPTerm p (Implicit fc True) = pure (PImplicit fc)

403 |   toPTerm p (Implicit fc False) = pure (PInfer fc)

405 |   toPTerm p (IWithUnambigNames fc ns rhs) =

406 |     PWithUnambigNames fc ns <$> toPTerm startPrec rhs

408 |   mkApp : {auto c : Ref Ctxt Defs} ->

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

410 |           IPTerm ->

411 |           List (FC, Maybe (Maybe Name), IPTerm) ->

412 |           Core IPTerm

413 |   mkApp fn [] = pure fn

414 |   mkApp fn ((fc, Nothing, arg) :: rest)

415 |       = do ap <- sugarPrimApp $ sugarApp (PApp fc fn arg)

416 |            mkApp ap rest

417 |   mkApp fn ((fc, Just Nothing, arg) :: rest)

418 |       = do ap <- sugarPrimApp $ sugarApp (PAutoApp fc fn arg)

419 |            mkApp ap rest

420 |   mkApp fn ((fc, Just (Just n), arg) :: rest)

421 |       = do imp <- showImplicits

422 |            if imp

423 |               then do let ap = PNamedApp fc fn n arg

424 |                       mkApp ap rest

425 |               else mkApp fn rest

427 |   toPTermApp : {auto c : Ref Ctxt Defs} ->

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

429 |                IRawImp -> List (FC, Maybe (Maybe Name), IPTerm) ->

430 |                Core IPTerm

431 |   toPTermApp (IApp fc f a) args

432 |       = do a' <- toPTerm argPrec a

433 |            toPTermApp f ((fc, Nothing, a') :: args)

434 |   toPTermApp (INamedApp fc f n a) args

435 |       = do a' <- toPTerm startPrec a

436 |            toPTermApp f ((fc, Just (Just n), a') :: args)

437 |   toPTermApp fn@(IVar fc n) args

438 |       = do defs <- get Ctxt

439 |            case !(lookupCtxtExact (rawName n) (gamma defs)) of

440 |                 Nothing => do fn' <- toPTerm appPrec fn

441 |                               mkApp fn' args

442 |                 Just def => do fn' <- toPTerm appPrec fn

443 |                                fenv <- showFullEnv

444 |                                let args'

445 |                                      = if fenv

446 |                                           then args

447 |                                           else drop (length (localVars def)) args

448 |                                mkApp fn' args'

449 |   toPTermApp fn args

450 |       = do fn' <- toPTerm appPrec fn

451 |            mkApp fn' args

453 |   toPFieldUpdate : {auto c : Ref Ctxt Defs} ->

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

455 |                    IFieldUpdate' KindedName -> Core (PFieldUpdate' KindedName)

456 |   toPFieldUpdate (ISetField p v)

457 |       = do v' <- toPTerm startPrec v

458 |            pure (PSetField p v')

459 |   toPFieldUpdate (ISetFieldApp p v)

460 |       = do v' <- toPTerm startPrec v

461 |            pure (PSetFieldApp p v')

463 |   toPClause : {auto c : Ref Ctxt Defs} ->

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

465 |               ImpClause' KindedName -> Core (PClause' KindedName)

466 |   toPClause (PatClause fc lhs rhs)

467 |       = pure (MkPatClause fc !(toPTerm startPrec lhs)

468 |                              !(toPTerm startPrec rhs)

469 |                              [])

470 |   toPClause (WithClause fc lhs rig wval prf flags cs)

471 |       = pure $ MkWithClause fc

472 |                  !(toPTerm startPrec lhs)

473 |                  (MkPWithProblem rig !(toPTerm startPrec wval) prf ::: [])

474 |                  flags

475 |                  !(traverse toPClause cs)

476 |   toPClause (ImpossibleClause fc lhs)

477 |       = pure (MkImpossible fc !(toPTerm startPrec lhs))

479 |   toPTypeDecl : {auto c : Ref Ctxt Defs} ->

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

481 |                 ImpTy' KindedName -> Core (PTypeDecl' KindedName)

482 |   toPTypeDecl impTy

483 |       = pure (MkFCVal impTy.fc $ MkPTy (pure ("", impTy.tyName)) "" !(toPTerm startPrec impTy.val))

485 |   toPData : {auto c : Ref Ctxt Defs} ->

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

487 |             ImpData' KindedName -> Core (PDataDecl' KindedName)

488 |   toPData (MkImpData fc n ty opts cs)

489 |       = pure (MkPData fc n !(traverseOpt (toPTerm startPrec) ty) opts

490 |                    !(traverse toPTypeDecl cs))

491 |   toPData (MkImpLater fc n ty)

492 |       = pure (MkPLater fc n !(toPTerm startPrec ty))

494 |   toPField : {auto c : Ref Ctxt Defs} ->

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

496 |              IField' KindedName -> Core (PField' KindedName)

497 |   toPField field

498 |       = do bind' <- traverse (toPTerm startPrec) field.val

499 |            pure (Mk [field.fc , "", field.rig, [field.name]] bind')

501 |   toPFnOpt : {auto c : Ref Ctxt Defs} ->

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

503 |              FnOpt' KindedName -> Core (PFnOpt' KindedName)

504 |   toPFnOpt (ForeignFn cs)

505 |       = do cs' <- traverse (toPTerm startPrec) cs

506 |            pure (PForeign cs')

507 |   toPFnOpt o = pure $ IFnOpt o

509 |   toPDecl : {auto c : Ref Ctxt Defs} ->

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

511 |             ImpDecl' KindedName -> Core (Maybe (PDecl' KindedName))

512 |   toPDecl (IClaim (MkWithData fc $ MkIClaimData rig vis opts ty))

513 |       = do opts' <- traverse toPFnOpt opts

514 |            pure (Just (MkWithData fc $ PClaim (MkPClaim rig vis opts' !(toPTypeDecl ty))))

515 |   toPDecl (IData fc vis mbtot d)

516 |       = pure (Just (MkFCVal fc $ PData "" vis mbtot !(toPData d)))

517 |   toPDecl (IDef fc n cs)

518 |       = pure (Just (MkFCVal fc $ PDef !(traverse toPClause cs)))

519 |   toPDecl (IParameters fc ps ds)

520 |       = do ds' <- traverse toPDecl ds

521 |            args <-

522 |              traverseList1 (\binder =>

523 |                  do info' <- traverse (toPTerm startPrec) binder.val.info

524 |                     type' <- toPTerm startPrec binder.val.boundType

525 |                     pure (MkFullBinder info' binder.rig binder.name type')) ps

526 |            pure (Just (MkFCVal fc (PParameters (Right args) (catMaybes ds'))))

527 |   toPDecl (IRecord fc _ vis mbtot (MkWithData _ $ MkImpRecord header body))

528 |       = do ps' <- traverse (traverse (traverse (toPTerm startPrec))) header.val

529 |            fs' <- traverse toPField body.val

530 |            pure (Just (MkFCVal fc $ PRecord "" vis mbtot

531 |                           (MkPRecord header.name.val (map toBinder ps') body.opts (Just (AddDef body.name)) fs')))

532 |            where

533 |              toBinder : ImpParameter' (PTerm' KindedName) -> PBinder' KindedName

534 |              toBinder binder

535 |                = MkFullBinder binder.val.info binder.rig binder.name binder.val.boundType

537 |   toPDecl (IFail fc msg ds)

538 |       = do ds' <- traverse toPDecl ds

539 |            pure (Just (MkFCVal fc $ PFail msg (catMaybes ds')))

540 |   toPDecl (INamespace fc ns ds)

541 |       = do ds' <- traverse toPDecl ds

542 |            pure (Just (MkFCVal fc $ PNamespace ns (catMaybes ds')))

543 |   toPDecl (ITransform fc n lhs rhs)

544 |       = pure (Just (MkFCVal fc $ PTransform (show n)

545 |                                   !(toPTerm startPrec lhs)

546 |                                   !(toPTerm startPrec rhs)))

547 |   toPDecl (IRunElabDecl fc tm)

548 |       = pure (Just (MkFCVal fc $ PRunElabDecl !(toPTerm startPrec tm)))

549 |   toPDecl (IPragma {}) = pure Nothing

550 |   toPDecl (ILog _) = pure Nothing

551 |   toPDecl (IBuiltin fc type name) = pure $ Just $ MkFCVal fc $ PBuiltin type name

554 | cleanPTerm : {auto c : Ref Ctxt Defs} ->

555 |              IPTerm -> Core IPTerm

556 | cleanPTerm ptm

557 |    = do pp <- getPPrint

558 |         if showMachineNames pp then pure ptm else mapPTermM cleanNode ptm

560 |   where

562 |     cleanName : Name -> Core Name

563 |     cleanName nm = case nm of

564 |       PV n _     => pure n

565 |       -- Some of these may be "_" so we use `mkUserName`

566 |       MN n _     => pure (UN $ mkUserName n)

567 |       DN n _     => pure (UN $ mkUserName n)

568 |       -- namespaces have already been stripped in toPTerm if necessary

569 |       NS ns n    => NS ns <$> cleanName n

570 |       Nested _ n => cleanName n

571 |       UN n       => pure (UN n)

572 |       _          => UN . mkUserName <$> prettyName nm

574 |     cleanKindedName : KindedName -> Core KindedName

575 |     cleanKindedName (MkKindedName nt fn nm) = MkKindedName nt fn <$> cleanName nm

577 |     cleanBinderName : PiInfo IPTerm -> Name -> Core (Maybe Name)

578 |     cleanBinderName AutoImplicit (UN (Basic "__con")) = pure Nothing

579 |     cleanBinderName _ nm = Just <$> cleanName nm

581 |     cleanNode : IPTerm -> Core IPTerm

582 |     cleanNode (PRef fc nm)    =

583 |       PRef fc <$> cleanKindedName nm

584 |     cleanNode (POp fc abi op y) =

585 |       (\ op => POp fc abi op y) <$> traverse (traverseOp @{Functor.CORE} cleanKindedName) op

586 |     cleanNode (PPrefixOp fc op x) =

587 |       (\ op => PPrefixOp fc op x) <$> traverse (traverseOp @{Functor.CORE} cleanKindedName) op

588 |     cleanNode (PSectionL fc op x) =

589 |       (\ op => PSectionL fc op x) <$> traverse (traverseOp @{Functor.CORE} cleanKindedName) op

590 |     cleanNode (PSectionR fc x op) =

591 |       PSectionR fc x <$> traverse (traverseOp @{Functor.CORE} cleanKindedName) op

592 |     cleanNode (PPi fc rig vis (Just n) arg ret) =

593 |       (\ n => PPi fc rig vis n arg ret) <$> (cleanBinderName vis n)

594 |     cleanNode tm = pure tm

596 | toCleanPTerm : {auto c : Ref Ctxt Defs} ->

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

598 |                (prec : Nat) -> IRawImp -> Core IPTerm

599 | toCleanPTerm prec tti = do

600 |   ptm <- toPTerm prec tti

601 |   cleanPTerm ptm

604 | resugar : {vars : _} ->

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

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

607 |           Env Term vars -> Term vars -> Core IPTerm

608 | resugar env tm

609 |     = do tti <- unelab env tm

610 |          toCleanPTerm startPrec tti

613 | resugarNoPatvars : {vars : _} ->

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

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

616 |                    Env Term vars -> Term vars -> Core IPTerm

617 | resugarNoPatvars env tm

618 |     = do tti <- unelabNoPatvars env tm

619 |          toCleanPTerm startPrec tti

622 | pterm : {auto c : Ref Ctxt Defs} ->

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

624 |         IRawImp -> Core IPTerm

625 | pterm raw = toCleanPTerm startPrec raw