0 | module TTImp.Unelab

  2 | import Core.Case.CaseTree

  3 | import Core.Context.Log

  4 | import Core.Env

  5 | import Core.Normalise

  6 | import Core.Value

  8 | import TTImp.TTImp

 10 | import Data.String

 12 | import Libraries.Data.VarSet

 14 | import Libraries.Data.List.SizeOf

 16 | %default covering

 18 | used : (idx : Nat) -> Term vars -> Bool

 19 | used idx (Local _ _ var _) = idx == var

 20 | used {vars} idx (Bind _ x b sc) = usedBinder b || used (1 + idx) sc

 21 |   where

 22 |     usedBinder : Binder (Term vars) -> Bool

 23 |     usedBinder (Let _ _ val ty) = used idx val || used idx ty

 24 |     usedBinder b = used idx (binderType b)

 25 | used idx (Meta _ _ _ args) = any (used idx) args

 26 | used idx (App _ f a) = used idx f || used idx a

 27 | used idx (As _ _ _ pat) = used idx pat

 28 | used idx (TDelayed _ _ tm) = used idx tm

 29 | used idx (TDelay _ _ _ tm) = used idx tm

 30 | used idx (TForce _ _ tm) = used idx tm

 31 | used idx _ = False

 33 | public export

 34 | data UnelabMode

 35 |      = Full

 36 |      | NoSugar Bool -- uniqify names

 37 |      | ImplicitHoles

 39 | Eq UnelabMode where

 40 |    Full == Full = True

 41 |    NoSugar t == NoSugar u = t == u

 42 |    ImplicitHoles == ImplicitHoles = True

 43 |    _ == _ = False

 47 |   ||| Unelaborate a call to a case expression as an inline case.

 67 |   unelabCase : {vars : _} ->

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

 69 |                List (Name, Nat) ->

 70 |                Env Term vars ->

 71 |                Name ->

 72 |                List (Term vars) ->

 73 |                Core (Maybe IRawImp)

 74 |   unelabCase nest env n args

 75 |       = do defs <- get Ctxt

 76 |            Just glob <- lookupCtxtExact n (gamma defs)

 77 |                 | Nothing => pure Nothing

 78 |            let PMDef _ pargs treect _ pats = definition glob

 79 |                 | _ => pure Nothing

 80 |            let Just argpos = findArgPos treect

 81 |                 | _ => pure Nothing

 82 |            if length args == length pargs

 83 |               then mkCase pats argpos args

 84 |               else pure Nothing

 85 |     where

 86 |       -- Need to find the position of the scrutinee to rebuild original

 87 |       -- case correctly

 88 |       findArgPos : CaseTree as -> Maybe Nat

 89 |       findArgPos (Case idx p _ _) = Just idx

 90 |       findArgPos _ = Nothing

 92 |       -- TODO: some utility like this should probably be implemented in Core

 93 |       substVars : List (VarSet vs, Term vs) -> Term vs -> Term vs

 94 |       substVars xs tm@(Local fc _ idx prf)

 95 |           = case find ((MkVar prf `VarSet.elem`) . fst) xs of

 96 |                  Just (_, new) => new

 97 |                  Nothing => tm

 98 |       substVars xs (Meta fc n i args)

 99 |           = Meta fc n i (map (substVars xs) args)

100 |       substVars xs (Bind fc y b scope)

101 |           = Bind fc y (map (substVars xs) b) (substVars (map (bimap (weaken {tm = VarSet}) weaken) xs) scope)

102 |       substVars xs (App fc fn arg)

103 |           = App fc (substVars xs fn) (substVars xs arg)

104 |       substVars xs (As fc s as pat)

105 |           = As fc s as (substVars xs pat)

106 |       substVars xs (TDelayed fc y z)

107 |           = TDelayed fc y (substVars xs z)

108 |       substVars xs (TDelay fc y t z)

109 |           = TDelay fc y (substVars xs t) (substVars xs z)

110 |       substVars xs (TForce fc r y)

111 |           = TForce fc r (substVars xs y)

112 |       substVars xs tm = tm

114 |       substArgs : SizeOf vs -> List (VarSet vs, Term vars) -> Term vs -> Term (vs ++ vars)

115 |       substArgs p substs tm =

116 |         let

117 |           substs' = map (bimap (embed {tm = VarSet} {outer = vars}) (weakenNs p)) substs

118 |           tm' = embed tm

119 |         in

120 |           substVars substs' tm'

122 |       argVars : {0 vs : _} -> VarSet vs -> Term vs -> VarSet vs

123 |       argVars acc (As _ _ as pat) = argVars (argVars acc as) pat

124 |       argVars acc (Local _ _ _ p) = VarSet.insert (MkVar p) acc

125 |       argVars acc _ = acc

127 |       mkClause : FC -> Nat ->

128 |                  List (Term vars) ->

129 |                  (vs ** (Env Term vs, Term vs, Term vs)) ->

130 |                  Core (Maybe IImpClause)

131 |       mkClause fc argpos args (vs ** (clauseEnv, lhs, rhs))

132 |           = do logTerm "unelab.case.clause" 20 "Unelaborating clause" lhs

133 |                let patArgs = snd (getFnArgs lhs)

134 |                    Just pat = getAt argpos patArgs

135 |                      | _ => pure Nothing

136 |                    rhs = substArgs (mkSizeOf vs) (zip (map (argVars (VarSet.empty {vs})) patArgs) args) rhs

137 |                logTerm "unelab.case.clause" 20 "Unelaborating LHS" pat

138 |                lhs' <- unelabTy Full nest clauseEnv pat

139 |                logTerm "unelab.case.clause" 20 "Unelaborating RHS" rhs

140 |                logEnv "unelab.case.clause" 20 "In Env" clauseEnv

141 |                rhs' <- unelabTy Full nest (clauseEnv ++ env) rhs

142 |                pure $ Just $ (PatClause fc (fst lhs') (fst rhs'))

144 |       ||| mkCase looks up the value passed as the scrutinee of the case-block.

150 |       mkCase : List (vs ** (Env Term vs, Term vs, Term vs)) ->

151 |                (argpos : Nat) -> List (Term vars) -> Core (Maybe IRawImp)

152 |       mkCase pats argpos args

153 |           = do unless (null args) $ log "unelab.case.clause" 20 $

154 |                  unwords $ "Ignoring" :: map show args

155 |                let Just scrutinee = getAt argpos args

156 |                      | _ => pure Nothing

157 |                    fc = getLoc scrutinee

158 |                (tm, _) <- unelabTy Full nest env scrutinee

159 |                Just pats' <- map sequence $ traverse (mkClause fc argpos args) pats

160 |                  | _ => pure Nothing

161 |                -- TODO: actually grab the fnopts?

162 |                pure $ Just $ ICase fc [] tm (Implicit fc False) pats'

164 |   dropParams : List (Name, Nat) -> (IRawImp, Glued vars) ->

165 |                Core (IRawImp, Glued vars)

166 |   dropParams nest (tm, ty)

167 |      = case getFnArgs tm [] of

168 |             (IVar fc n, args) =>

169 |                 case lookup (rawName n) nest of

170 |                      Nothing => pure (tm, ty)

171 |                      Just i => pure $ (apply (IVar fc n) (drop i args), ty)

172 |             _ => pure (tm, ty)

173 |     where

174 |       apply : IRawImp -> List IArg -> IRawImp

175 |       apply tm [] = tm

176 |       apply tm (Explicit fc a :: args) = apply (IApp fc tm a) args

177 |       apply tm (Auto fc a :: args) = apply (IAutoApp fc tm a) args

178 |       apply tm (Named fc n a :: args) = apply (INamedApp fc tm n a) args

180 |   -- Turn a term back into an unannotated TTImp. Returns the type of the

181 |   -- unelaborated term so that we can work out where to put the implicit

182 |   -- applications

183 |   -- NOTE: There is *no guarantee* that this will elaborate back successfully!

184 |   -- It's only intended for display

185 |   unelabTy : {vars : _} ->

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

187 |              (umode : UnelabMode) ->

188 |              (nest : List (Name, Nat)) ->

189 |              Env Term vars -> Term vars ->

190 |              Core (IRawImp, Glued vars)

191 |   unelabTy umode nest env tm

192 |       = dropParams nest !(unelabTy' umode nest env tm)

194 |   unelabTy' : {vars : _} ->

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

196 |               (umode : UnelabMode) ->

197 |               (nest : List (Name, Nat)) ->

198 |               Env Term vars -> Term vars ->

199 |               Core (IRawImp, Glued vars)

200 |   unelabTy' umode nest env (Local fc _ idx p)

201 |       = do let nm = nameAt p

202 |            log "unelab.case" 20 $ "Found local name: " ++ show nm

203 |            let ty = gnf env (binderType (getBinder p env))

204 |            pure (IVar fc (MkKindedName (Just Bound) nm nm), ty)

205 |   unelabTy' umode nest env (Ref fc nt n)

206 |       = do defs <- get Ctxt

207 |            Just ty <- lookupTyExact n (gamma defs)

208 |                | Nothing => case umode of

209 |                                  ImplicitHoles => pure (Implicit fc True, gErased fc)

210 |                                  _ => pure (IVar fc (MkKindedName (Just nt) n n), gErased fc)

211 |            fn <- getFullName n

212 |            n' <- case umode of

213 |                       NoSugar _ => pure fn

214 |                       _ => aliasName fn

215 |            log "unelab.var" 50 $

216 |              unwords [ "Found name:", show n

217 |                      , " (aka " ++ show fn ++ ")"

218 |                      , "sugared to", show n'

219 |                      ]

221 |            pure (IVar fc (MkKindedName (Just nt) fn n'), gnf env (embed ty))

222 |   unelabTy' umode nest env (Meta fc n i args)

223 |       = do defs <- get Ctxt

224 |            let mkn = nameRoot n

225 |            def <- lookupDefExact (Resolved i) (gamma defs)

226 |            let term = case def of

227 |                               (Just (BySearch _ d _)) => ISearch fc d

228 |                               _ => IHole fc mkn

229 |            Just ty <- lookupTyExact (Resolved i) (gamma defs)

230 |                | Nothing => case umode of

231 |                                  ImplicitHoles => pure (Implicit fc True, gErased fc)

232 |                                  _ => pure (term, gErased fc)

233 |            pure (term, gnf env (embed ty))

234 |   unelabTy' umode nest env (Bind fc x b sc)

235 |       = case umode of

236 |           NoSugar True => do

237 |             let x' = uniqueLocal vars x

238 |             let sc : Term (x' :: vars) = compat sc

239 |             (sc', scty) <- unelabTy umode nest (b :: env) sc

240 |             unelabBinder umode nest fc env x' b

241 |                          (compat sc) sc'

242 |                          (compat !(getTerm scty))

243 |           _ => do

244 |             (sc', scty) <- unelabTy umode nest (b :: env) sc

245 |             unelabBinder umode nest fc env x b sc sc' !(getTerm scty)

246 |     where

247 |       next : Name -> Name

248 |       next (MN n i) = MN n (i + 1)

249 |       next (UN n) = MN (show n) 0

250 |       next (NS ns n) = NS ns (next n)

251 |       next n = MN (show n) 0

253 |       uniqueLocal : Scope -> Name -> Name

254 |       uniqueLocal vs n

255 |          = if n `elem` vs

256 |               then uniqueLocal vs (next n)

257 |               else n

258 |   unelabTy' umode nest env tm@(App fc fn arg)

259 |       = do (fn', gfnty) <- unelabTy umode nest env fn

260 |            (arg', gargty) <- unelabTy umode nest env arg

261 |            fnty <- getNF gfnty

262 |            defs <- get Ctxt

263 |            Nothing <-

264 |               case umode of

265 |                 (NoSugar _) => pure Nothing

266 |                 ImplicitHoles => pure Nothing

267 |                 _ => case getFnArgs tm of

268 |                      (Ref _ _ fnName, args) => do

269 |                        fullName <- getFullName fnName

270 |                        let (NS ns (CaseBlock n i)) = fullName

271 |                          | _ => pure Nothing

272 |                        unelabCase nest env fullName args

273 |                      _ => pure Nothing

274 |              | Just tm => pure (tm, gErased fc)

275 |            case fnty of

276 |                 NBind _ x (Pi _ rig Explicit ty) sc

277 |                   => do sc' <- sc defs (toClosure defaultOpts env arg)

278 |                         pure (IApp fc fn' arg',

279 |                                 glueBack defs env sc')

280 |                 NBind _ x (Pi _ rig p ty) sc

281 |                   => do sc' <- sc defs (toClosure defaultOpts env arg)

282 |                         pure (INamedApp fc fn' x arg',

283 |                                 glueBack defs env sc')

284 |                 _ => pure (IApp fc fn' arg', gErased fc)

285 |   unelabTy' umode nest env (As fc s p tm)

286 |       = do (p', _) <- unelabTy' umode nest env p

287 |            (tm', ty) <- unelabTy' umode nest env tm

288 |            case p' of

289 |                 IVar _ n =>

290 |                     case umode of

291 |                          NoSugar _ => pure (IAs fc (getLoc p) s n.rawName tm', ty)

292 |                          _ => pure (tm', ty)

293 |                 _ => pure (tm', ty) -- Should never happen!

294 |   unelabTy' umode nest env (TDelayed fc r tm)

295 |       = do (tm', ty) <- unelabTy' umode nest env tm

296 |            defs <- get Ctxt

297 |            pure (IDelayed fc r tm', gErased fc)

298 |   unelabTy' umode nest env (TDelay fc r _ tm)

299 |       = do (tm', ty) <- unelabTy' umode nest env tm

300 |            defs <- get Ctxt

301 |            pure (IDelay fc tm', gErased fc)

302 |   unelabTy' umode nest env (TForce fc r tm)

303 |       = do (tm', ty) <- unelabTy' umode nest env tm

304 |            defs <- get Ctxt

305 |            pure (IForce fc tm', gErased fc)

306 |   unelabTy' umode nest env (PrimVal fc c) = pure (IPrimVal fc c, gErased fc)

307 |   unelabTy' umode nest env (Erased fc (Dotted t))

308 |     = unelabTy' umode nest env t

309 |   unelabTy' umode nest env (Erased fc _) = pure (Implicit fc True, gErased fc)

310 |   unelabTy' umode nest env (TType fc _) = pure (IType fc, gType fc (MN "top" 0))

312 |   unelabPi : {vars : _} ->

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

314 |              (umode : UnelabMode) ->

315 |              (nest : List (Name, Nat)) ->

316 |              Env Term vars -> PiInfo (Term vars) ->

317 |              Core (PiInfo IRawImp)

318 |   unelabPi umode nest env Explicit = pure Explicit

319 |   unelabPi umode nest env Implicit = pure Implicit

320 |   unelabPi umode nest env AutoImplicit = pure AutoImplicit

321 |   unelabPi umode nest env (DefImplicit t)

322 |       = do (t', _) <- unelabTy umode nest env t

323 |            pure (DefImplicit t')

325 |   unelabBinder : {vars : _} ->

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

327 |                  (umode : UnelabMode) ->

328 |                  (nest : List (Name, Nat)) ->

329 |                  FC -> Env Term vars -> (x : Name) ->

330 |                  Binder (Term vars) -> Term (x :: vars) ->

331 |                  IRawImp -> Term (x :: vars) ->

332 |                  Core (IRawImp, Glued vars)

333 |   unelabBinder umode nest fc env x (Lam fc' rig p ty) sctm sc scty

334 |       = do (ty', _) <- unelabTy umode nest env ty

335 |            p' <- unelabPi umode nest env p

336 |            pure (ILam fc rig p' (Just x) ty' sc,

337 |                     gnf env (Bind fc x (Pi fc' rig p ty) scty))

338 |   unelabBinder umode nest fc env x (Let fc' rig val ty) sctm sc scty

339 |       = do (val', vty) <- unelabTy umode nest env val

340 |            (ty', _) <- unelabTy umode nest env ty

341 |            pure (ILet fc EmptyFC rig x ty' val' sc,

342 |                     gnf env (Bind fc x (Let fc' rig val ty) scty))

343 |   unelabBinder umode nest fc env x (Pi _ rig p ty) sctm sc scty

344 |       = do (ty', _) <- unelabTy umode nest env ty

345 |            p' <- unelabPi umode nest env p

346 |            let nm = if used 0 sctm || isNoSugar umode

347 |                        then Just x

348 |                        else if rig /= top || isDefImp p

349 |                                then Just (UN Underscore)

350 |                                else Nothing

351 |            pure (IPi fc rig p' nm ty' sc, gType fc (MN "top" 0))

352 |     where

353 |       isNoSugar : UnelabMode -> Bool

354 |       isNoSugar (NoSugar _) = True

355 |       isNoSugar _ = False

356 |       isDefImp : PiInfo t -> Bool

357 |       isDefImp (DefImplicit _) = True

358 |       isDefImp _ = False

359 |   unelabBinder umode nest fc env x (PVar fc' rig _ ty) sctm sc scty

360 |       = do (ty', _) <- unelabTy umode nest env ty

361 |            pure (sc, gnf env (Bind fc x (PVTy fc' rig ty) scty))

362 |   unelabBinder umode nest fc env x (PLet fc' rig val ty) sctm sc scty

363 |       = do (val', vty) <- unelabTy umode nest env val

364 |            (ty', _) <- unelabTy umode nest env ty

365 |            pure (ILet fc EmptyFC rig x ty' val' sc,

366 |                     gnf env (Bind fc x (PLet fc' rig val ty) scty))

367 |   unelabBinder umode nest fc env x (PVTy _ rig ty) sctm sc scty

368 |       = do (ty', _) <- unelabTy umode nest env ty

369 |            pure (sc, gType fc (MN "top" 0))

372 | unelabNoSugar : {vars : _} ->

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

374 |                 Env Term vars -> Term vars -> Core IRawImp

375 | unelabNoSugar env tm

376 |     = do tm' <- unelabTy (NoSugar False) [] env tm

377 |          pure $ fst tm'

380 | unelabUniqueBinders : {vars : _} ->

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

382 |                 Env Term vars -> Term vars -> Core IRawImp

383 | unelabUniqueBinders env tm

384 |     = do tm' <- unelabTy (NoSugar True) [] env tm

385 |          pure $ fst tm'

388 | unelabNoPatvars : {vars : _} ->

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

390 |                   Env Term vars -> Term vars -> Core IRawImp

391 | unelabNoPatvars env tm

392 |     = do tm' <- unelabTy ImplicitHoles [] env tm

393 |          pure $ fst tm'

396 | unelabNest : {vars : _} ->

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

398 |              UnelabMode ->

399 |              List (Name, Nat) ->

400 |              Env Term vars ->

401 |              Term vars -> Core IRawImp

402 | unelabNest mode nest env (Meta fc n i args)

403 |     = do let mkn = nameRoot n ++ showScope args

404 |          pure (IHole fc mkn)

405 |   where

406 |     toName : Term vars -> Maybe Name

407 |     toName (Local _ _ idx p) = Just (nameAt p)

408 |     toName _ = Nothing

410 |     showNScope : List Name -> String

411 |     showNScope [] = "[no locals in scope]"

412 |     showNScope ns = "[locals in scope: " ++ showSep ", " (map show (nub ns)) ++ "]"

414 |     showScope : List (Term vars) -> String

415 |     showScope ts = " " ++ showNScope (mapMaybe toName ts)

417 | unelabNest mode nest env tm

418 |     = do tm' <- unelabTy mode nest env tm

419 |          pure $ fst tm'

422 | unelab : {vars : _} ->

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

424 |          Env Term vars ->

425 |          Term vars -> Core IRawImp

426 | unelab = unelabNest Full []