0 | module TTImp.Elab.Delayed

  2 | import Core.Case.CaseTree

  3 | import Core.Context.Log

  4 | import Core.Env

  5 | import Core.Metadata

  6 | import Core.Normalise

  7 | import Core.Unify

  8 | import Core.Value

 10 | import TTImp.Elab.Check

 12 | import Libraries.Data.IntMap

 13 | import Libraries.Data.NameMap

 15 | %default covering

 19 | mkClosedElab : {vars : _} ->

 20 |                FC -> Env Term vars ->

 21 |                (Core (Term vars, Glued vars)) ->

 22 |                Core ClosedTerm

 23 | mkClosedElab fc [] elab

 24 |     = do (tm, _) <- elab

 25 |          pure tm

 26 | mkClosedElab {vars = x :: vars} fc (b :: env) elab

 27 |     = mkClosedElab fc env

 28 |           (do (sc', _) <- elab

 29 |               let b' = newBinder b

 30 |               pure (Bind fc x b' sc', gErased fc))

 31 |   where

 32 |     -- in 'abstractEnvType' we get a Pi binder (so we'll need a Lambda) for

 33 |     -- everything except 'Let', so make the appropriate corresponding binder

 34 |     -- here

 35 |     newBinder : Binder (Term vars) -> Binder (Term vars)

 36 |     newBinder b@(Let {}) = b

 37 |     newBinder b = Lam (binderLoc b) (multiplicity b) Explicit (binderType b)

 39 | deeper : {auto e : Ref EST (EState vars)} ->

 40 |          Core a -> Core a

 41 | deeper elab

 42 |     = do est <- get EST

 43 |          let d = delayDepth est

 44 |          put EST ({ delayDepth := 1 + d } est)

 45 |          res <- elab

 46 |          est <- get EST

 47 |          put EST ({ delayDepth := d } est)

 48 |          pure res

 54 | delayOnFailure : {vars : _} ->

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

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

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

 58 |                  {auto e : Ref EST (EState vars)} ->

 59 |                  FC -> RigCount -> Env Term vars ->

 60 |                  (expected : Maybe (Glued vars)) ->

 61 |                  (Error -> Bool) ->

 62 |                  (pri : DelayReason) ->

 63 |                  (Bool -> Core (Term vars, Glued vars)) ->

 64 |                  Core (Term vars, Glued vars)

 65 | delayOnFailure fc rig env exp pred pri elab

 66 |     = do ust <- get UST

 67 |          let nos = noSolve ust -- remember the holes we shouldn't solve

 68 |          handle (elab False)

 69 |           (\err =>

 70 |               do est <- get EST

 71 |                  expected <- mkExpected exp

 72 |                  if pred err

 73 |                     then

 74 |                       do nm <- genName "delayed"

 75 |                          (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)

 76 |                          logGlueNF "elab.delay" 5 ("Postponing elaborator " ++ show nm ++

 77 |                                       " at " ++ show fc ++

 78 |                                       " for") env expected

 79 |                          log "elab.delay" 10 ("Due to error " ++ show err)

 80 |                          defs <- get Ctxt

 81 |                          update UST { delayedElab $=

 82 |                                  ((pri, ci, localHints defs,

 83 |                                    mkClosedElab fc env

 84 |                                       (deeper

 85 |                                         (do ust <- get UST

 86 |                                             let nos' = noSolve ust

 87 |                                             put UST ({ noSolve := nos } ust)

 88 |                                             res <- elab True

 89 |                                             ust <- get UST

 90 |                                             put UST ({ noSolve := nos' } ust)

 91 |                                             pure res))) :: ) }

 92 |                          pure (dtm, expected)

 93 |                     else throw err)

 94 |   where

 95 |     mkExpected : Maybe (Glued vars) -> Core (Glued vars)

 96 |     mkExpected (Just ty) = pure ty

 97 |     mkExpected Nothing

 98 |         = do nm <- genName "delayTy"

 99 |              u <- uniVar fc

100 |              ty <- metaVar fc erased env nm (TType fc u)

101 |              pure (gnf env ty)

104 | delayElab : {vars : _} ->

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

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

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

108 |             {auto e : Ref EST (EState vars)} ->

109 |             FC -> RigCount -> Env Term vars ->

110 |             (expected : Maybe (Glued vars)) ->

111 |             (pri : DelayReason) ->

112 |             Core (Term vars, Glued vars) ->

113 |             Core (Term vars, Glued vars)

114 | delayElab {vars} fc rig env exp pri elab

115 |     = do ust <- get UST

116 |          let nos = noSolve ust -- remember the holes we shouldn't solve

117 |          nm <- genName "delayed"

118 |          expected <- mkExpected exp

119 |          (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)

120 |          logGlueNF "elab.delay" 5 ("Postponing elaborator " ++ show nm ++

121 |                       " for") env expected

122 |          defs <- get Ctxt

123 |          update UST { delayedElab $=

124 |                  ((pri, ci, localHints defs, mkClosedElab fc env

125 |                                               (do ust <- get UST

126 |                                                   let nos' = noSolve ust

127 |                                                   put UST ({ noSolve := nos } ust)

128 |                                                   res <- elab

129 |                                                   ust <- get UST

130 |                                                   put UST ({ noSolve := nos' } ust)

131 |                                                   pure res)) :: ) }

132 |          pure (dtm, expected)

133 |   where

134 |     mkExpected : Maybe (Glued vars) -> Core (Glued vars)

135 |     mkExpected (Just ty) = pure ty

136 |     mkExpected Nothing

137 |         = do nm <- genName "delayTy"

138 |              u <- uniVar fc

139 |              ty <- metaVar fc erased env nm (TType fc u)

140 |              pure (gnf env ty)

143 | ambiguous : Error -> Bool

144 | ambiguous (AmbiguousElab {}) = True

145 | ambiguous (AmbiguousName {}) = True

146 | ambiguous (AmbiguityTooDeep {}) = True

147 | ambiguous (InType _ _ err) = ambiguous err

148 | ambiguous (InCon _ err) = ambiguous err

149 | ambiguous (InLHS _ _ err) = ambiguous err

150 | ambiguous (InRHS _ _ err) = ambiguous err

151 | ambiguous (WhenUnifying _ _ _ _ _ err) = ambiguous err

152 | ambiguous _ = False

155 |   mismatchNF : {auto c : Ref Ctxt Defs} ->

156 |                {vars : _} ->

157 |                Defs -> NF vars -> NF vars -> Core Bool

158 |   mismatchNF defs (NTCon _ xn _ xargs) (NTCon _ yn _ yargs)

159 |       = if xn /= yn

160 |            then pure True

161 |            else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)

162 |   mismatchNF defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)

163 |       = if xt /= yt

164 |            then pure True

165 |            else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)

166 |   mismatchNF defs (NPrimVal _ xc) (NPrimVal _ yc) = pure (xc /= yc)

167 |   mismatchNF defs (NDelayed _ _ x) (NDelayed _ _ y) = mismatchNF defs x y

168 |   mismatchNF defs (NDelay _ _ _ x) (NDelay _ _ _ y)

169 |       = mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)

170 |   mismatchNF _ _ _ = pure False

172 |   mismatch : {auto c : Ref Ctxt Defs} ->

173 |              {vars : _} ->

174 |              Defs -> (Closure vars, Closure vars) -> Core Bool

175 |   mismatch defs (x, y)

176 |       = mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)

178 | contra : {auto c : Ref Ctxt Defs} ->

179 |          {vars : _} ->

180 |          Defs -> NF vars -> NF vars -> Core Bool

182 | contra defs (NTCon _ xn xa xargs) (NTCon _ yn ya yargs)

183 |     = if xn /= yn

184 |          then pure True

185 |          else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)

186 | contra defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)

187 |     = if xt /= yt

188 |          then pure True

189 |          else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)

190 | contra defs (NPrimVal _ x) (NPrimVal _ y) = pure (x /= y)

191 | contra defs (NDCon {}) (NPrimVal {}) = pure True

192 | contra defs (NPrimVal {}) (NDCon {}) = pure True

193 | contra defs x y = pure False

198 | recoverable : {auto c : Ref Ctxt Defs} ->

199 |               Error -> Core Bool

200 | recoverable (CantConvert _ gam env l r)

201 |    = do defs <- get Ctxt

202 |         let defs = { gamma := gam } defs

203 |         pure $ not !(contra defs !(nf defs env l) !(nf defs env r))

204 | recoverable (CantSolveEq _ gam env l r)

205 |    = do defs <- get Ctxt

206 |         let defs = { gamma := gam } defs

207 |         pure $ not !(contra defs !(nf defs env l) !(nf defs env r))

208 | recoverable (UndefinedName {}) = pure False

209 | recoverable (LinearMisuse {}) = pure False

210 | recoverable (InType _ _ err) = recoverable err

211 | recoverable (InCon _ err) = recoverable err

212 | recoverable (InLHS _ _ err) = recoverable err

213 | recoverable (InRHS _ _ err) = recoverable err

214 | recoverable (WhenUnifying _ _ _ _ _ err) = recoverable err

215 | recoverable _ = pure True

217 | data RetryError

218 |      = RecoverableErrors

219 |      | AllErrors

221 | Show RetryError where

222 |   show RecoverableErrors = "RecoverableErrors"

223 |   show AllErrors = "AllErrors"

228 | retryDelayed' : {vars : _} ->

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

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

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

232 |                 {auto e : Ref EST (EState vars)} ->

233 |                 RetryError ->

234 |                 (progress : Bool) ->

235 |                 List (DelayReason, Int, NameMap (), Core ClosedTerm) ->

236 |                 List (DelayReason, Int, NameMap (), Core ClosedTerm) ->

237 |                 Core (Bool, List (DelayReason, Int, NameMap (), Core ClosedTerm))

238 | retryDelayed' errmode p acc [] = pure (p, reverse acc)

239 | retryDelayed' errmode p acc (d@(_, i, hints, elab) :: ds)

240 |     = do defs <- get Ctxt

241 |          Just Delayed <- lookupDefExact (Resolved i) (gamma defs)

242 |               | _ => retryDelayed' errmode p acc ds

243 |          handle

244 |            (do est <- get EST

245 |                logC "elab.retry" 5 $ do pure $ show (delayDepth est) ++ ": Retrying delayed hole " ++ show !(getFullName (Resolved i))

246 |                -- elab itself might have delays internally, so keep track of them

247 |                update UST { delayedElab := [] }

248 |                update Ctxt { localHints := hints }

250 |                tm <- elab

251 |                ust <- get UST

252 |                let ds' = reverse (delayedElab ust) ++ ds

254 |                updateDef (Resolved i) (const (Just

255 |                     (PMDef (MkPMDefInfo NotHole True False)

256 |                            Scope.empty (STerm 0 tm) (STerm 0 tm) [])))

257 |                logTerm "elab.update" 5 ("Resolved delayed hole " ++ show i) tm

258 |                logTermNF "elab.update" 5 ("Resolved delayed hole NF " ++ show i) Env.empty tm

259 |                removeHole i

260 |                retryDelayed' errmode True acc ds')

261 |            (\err => do logC "elab" 5 $ do pure $ show errmode ++ ":Error in " ++ show !(getFullName (Resolved i))

262 |                                               ++ "\n" ++ show err

263 |                        case errmode of

264 |                          RecoverableErrors =>

265 |                             if not !(recoverable err)

266 |                                then throw err

267 |                                else retryDelayed' errmode p (d :: acc) ds

268 |                          AllErrors =>

269 |                             -- we've got an error, but see if we get a more

270 |                             -- helpful one with a later elaborator

271 |                             handle (do ignore $ retryDelayed' errmode p [] ds

272 |                                        throw err)

273 |                                (\err' => throw (better err err')))

274 |   where

275 |     better : Error -> Error -> Error

276 |     better e (GenericMsg {}) = e

277 |     better (GenericMsg {}) e = e

278 |     better e _ = e

281 | retryDelayed : {vars : _} ->

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

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

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

285 |                {auto e : Ref EST (EState vars)} ->

286 |                UnifyInfo -> List (DelayReason, Int, NameMap (), Core ClosedTerm) ->

287 |                Core ()

288 | retryDelayed mode ds

289 |     = do (p, ds) <- retryDelayed' RecoverableErrors False [] ds -- try everything again

290 |          solveConstraints mode Normal -- maybe we can resolve some interfaces now

291 |          if p

292 |             then retryDelayed mode ds -- progress, go around again

293 |             else ignore $ retryDelayed' AllErrors False [] ds -- fail on all errors

297 | runDelays : {vars : _} ->

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

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

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

301 |             {auto e : Ref EST (EState vars)} ->

302 |             (DelayReason -> Bool) -> Core a -> Core a

303 | runDelays pri elab

304 |     = do ust <- get UST

305 |          let olddelayed = delayedElab ust

306 |          put UST ({ delayedElab := [] } ust)

307 |          tm <- elab

308 |          ust <- get UST

309 |          log "elab.delay" 2 $ "Rerunning delayed in elaborator"

310 |          handle (do ignore $ retryDelayed' AllErrors False []

311 |                        (reverse (filter hasPri (delayedElab ust))))

312 |                 (\err => do put UST ({ delayedElab := olddelayed } ust)

313 |                             throw err)

314 |          update UST { delayedElab $= (++ olddelayed) }

315 |          pure tm

316 |   where

317 |     hasPri : (DelayReason, d) -> Bool

318 |     hasPri (n, _) = pri n