0 | module TTImp.Elab

  2 | import Core.Env

  3 | import Core.LinearCheck

  4 | import Core.Metadata

  5 | import Core.Unify

  7 | import Idris.REPL.Opts

  8 | import Idris.Syntax

 10 | import TTImp.Elab.Check

 11 | import TTImp.Elab.Delayed

 12 | import TTImp.Elab.Term

 13 | import TTImp.TTImp

 15 | import Libraries.Data.IntMap

 16 | import Libraries.Data.NameMap

 18 | %default covering

 20 | findPLetRenames : {vars : _} ->

 21 |                   Term vars -> List (Name, (RigCount, Name))

 22 | findPLetRenames (Bind fc n (PLet _ c (Local _ _ idx p) ty) sc)

 23 |     = case nameAt p of

 24 |            x@(MN {}) => (x, (c, n)) :: findPLetRenames sc

 25 |            _ => findPLetRenames sc

 26 | findPLetRenames (Bind fc n _ sc) = findPLetRenames sc

 27 | findPLetRenames tm = []

 29 | doPLetRenames : {vars : _} ->

 30 |                 List (Name, (RigCount, Name)) ->

 31 |                 List Name -> Term vars -> Term vars

 32 | doPLetRenames ns drops (Bind fc n b@(PLet {}) sc)

 33 |     = if n `elem` drops

 34 |          then subst (Erased fc Placeholder) (doPLetRenames ns drops sc)

 35 |          else Bind fc n b (doPLetRenames ns drops sc)

 36 | doPLetRenames ns drops (Bind fc n b sc)

 37 |     = case lookup n ns of

 38 |            Just (c, n') =>

 39 |              Bind fc n' (setMultiplicity b (c `lub` (multiplicity b)))

 40 |                      (doPLetRenames ns (n' :: drops) (compat sc))

 41 |            Nothing => Bind fc n b (doPLetRenames ns drops sc)

 42 | doPLetRenames ns drops sc = sc

 44 | getRigNeeded : ElabMode -> RigCount

 45 | getRigNeeded InType = erased -- unrestricted usage in types

 46 | getRigNeeded (InLHS r) = if isErased r then erased

 47 |                                      else linear

 48 | getRigNeeded _ = linear

 53 | normaliseHoleTypes : {auto c : Ref Ctxt Defs} ->

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

 55 |                      Core ()

 57 |     = do ust <- get UST

 58 |          let hs = keys (holes ust)

 59 |          defs <- get Ctxt

 60 |          traverse_ (normaliseH defs) hs

 61 |   where

 62 |     updateType : Defs -> Int -> GlobalDef -> Core ()

 63 |     updateType defs i def

 64 |         = do ty' <- catch (tryNormaliseSizeLimit defs 10 Env.empty (type def))

 65 |                           (\err => normaliseHoles defs Env.empty (type def))

 66 |              ignore $ addDef (Resolved i) ({ type := ty' } def)

 68 |     normaliseH : Defs -> Int -> Core ()

 69 |     normaliseH defs i

 70 |         = whenJust !(lookupCtxtExact (Resolved i) (gamma defs)) $ \ gdef =>

 71 |             case definition gdef of

 72 |               Hole {} => updateType defs i gdef

 73 |               _ => pure ()

 76 | addHoleToSave : {auto c : Ref Ctxt Defs} ->

 77 |                 Name -> Core ()

 78 | addHoleToSave n

 79 |     = do defs <- get Ctxt

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

 81 |               | Nothing => pure ()

 82 |          let ms = keys (getMetas ty)

 83 |          addToSave n

 84 |          traverse_ addToSave ms

 87 | elabTermSub : {inner, vars : _} ->

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

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

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

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

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

 93 |               Int -> ElabMode -> List ElabOpt ->

 94 |               NestedNames vars -> Env Term vars ->

 95 |               Env Term inner -> Thin inner vars ->

 96 |               RawImp -> Maybe (Glued vars) ->

 97 |               Core (Term vars, Glued vars)

 98 | elabTermSub {vars} defining mode opts nest env env' sub tm ty

 99 |     = do let incase = elem InCase opts

100 |          let inPE = elem InPartialEval opts

101 |          let inTrans = elem InTrans opts

103 |          -- Record the current hole state; we only check the list of current

104 |          -- holes is completely solved so this needs to be accurate.

105 |          oldhs <- if not incase

106 |                      then saveHoles

107 |                      else pure empty

108 |          ust <- get UST

109 |          let olddelayed = delayedElab ust

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

111 |          constart <- getNextEntry

113 |          defs <- get Ctxt

114 |          e <- newRef EST (initEStateSub defining env' sub)

115 |          let rigc = getRigNeeded mode

117 |          (chktm, chkty) <- check {e} rigc (initElabInfo mode) nest env tm ty

118 |          -- Final retry of constraints and delayed elaborations

119 |          -- - Solve any constraints, then retry any delayed elaborations

120 |          -- - Finally, last attempts at solving constraints, but this

121 |          --   is most likely just to be able to display helpful errors

122 |          let solvemode = case mode of

123 |                               InLHS _ => inLHS

124 |                               _ => inTerm

125 |          solveConstraints solvemode Normal

126 |          logTerm "elab" 5 "Looking for delayed in " chktm

127 |          ust <- get UST

128 |          catch (retryDelayed solvemode

129 |                              (sortBy (\x, y => compare (fst x) (fst y))

130 |                                        (delayedElab ust)))

131 |                  (\err =>

132 |                     do update UST { delayedElab := olddelayed }

133 |                        throw err)

134 |          update UST { delayedElab := olddelayed }

135 |          solveConstraintsAfter constart solvemode MatchArgs

137 |          -- As long as we're not in the RHS of a case block,

138 |          -- finish off constraint solving

139 |          -- On the LHS the constraint solving is used to handle overloading

140 |          when (not incase || isJust (isLHS mode)) $

141 |            -- resolve any default hints

142 |            do log "elab" 5 "Resolving default hints"

143 |               solveConstraintsAfter constart solvemode Defaults

144 |               -- perhaps resolving defaults helps...

145 |               -- otherwise, this last go is most likely just to give us more

146 |               -- helpful errors.

147 |               solveConstraintsAfter constart solvemode LastChance

149 |          dumpConstraints "elab" 4 False

150 |          defs <- get Ctxt

151 |          chktm <- if inPE -- Need to fully normalise holes in partial evaluation

152 |                           -- because the holes don't have types saved to ttc

153 |                      then normaliseHoles defs env chktm

154 |                      else normaliseArgHoles defs env chktm

156 |          -- Linearity and hole checking.

157 |          -- on the LHS, all holes need to have been solved

158 |          chktm <- case mode of

159 |               InLHS _ => do when (not incase) $ checkUserHolesAfter constart True

160 |                             pure chktm

161 |               InTransform => do when (not incase) $ checkUserHolesAfter constart True

162 |                                 pure chktm

163 |               -- elsewhere, all unification problems must be

164 |               -- solved, though we defer that if it's a case block since we

165 |               -- might learn a bit more later.

166 |               _ => if (not incase)

167 |                       then do checkUserHolesAfter constart (inTrans || inPE)

168 |                               linearCheck (getFC tm) rigc False env chktm

169 |                           -- Linearity checking looks in case blocks, so no

170 |                           -- need to check here.

171 |                       else pure chktm

172 |          normaliseHoleTypes

173 |          -- Put the current hole state back to what it was (minus anything

174 |          -- which has been solved in the meantime)

175 |          when (not incase) $

176 |            do hs <- getHoles

177 |               restoreHoles (addHoles empty hs (toList oldhs))

179 |          -- Make a note to save all the user holes and the things they

180 |          -- reference

181 |          est <- get EST

182 |          traverse_ addHoleToSave (keys (saveHoles est))

184 |          -- On the LHS, finish by tidying up the plets (changing things that

185 |          -- were of the form x@_, where the _ is inferred to be a variable,

186 |          -- to just x)

187 |          case mode of

188 |               InLHS _ =>

189 |                  do let vs = findPLetRenames chktm

190 |                     let ret = doPLetRenames vs [] chktm

191 |                     pure (ret, gnf env (doPLetRenames vs [] !(getTerm chkty)))

192 |               _ => do dumpConstraints "elab" 2 False

193 |                       pure (chktm, chkty)

194 |   where

195 |     addHoles : (acc : IntMap (FC, Name)) ->

196 |                (allHoles : IntMap (FC, Name)) ->

197 |                List (Int, (FC, Name)) ->

198 |                IntMap (FC, Name)

199 |     addHoles acc allhs [] = acc

200 |     addHoles acc allhs ((n, x) :: hs)

201 |         = case lookup n allhs of

202 |                Nothing => addHoles acc allhs hs

203 |                Just _ => addHoles (insert n x acc) allhs hs

206 | elabTerm : {vars : _} ->

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

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

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

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

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

212 |            Int -> ElabMode -> List ElabOpt ->

213 |            NestedNames vars -> Env Term vars ->

214 |            RawImp -> Maybe (Glued vars) ->

215 |            Core (Term vars, Glued vars)

216 | elabTerm defining mode opts nest env tm ty

217 |     = elabTermSub defining mode opts nest env env Refl tm ty

220 | checkTermSub : {inner, vars : _} ->

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

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

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

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

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

226 |                Int -> ElabMode -> List ElabOpt ->

227 |                NestedNames vars -> Env Term vars ->

228 |                Env Term inner -> Thin inner vars ->

229 |                RawImp -> Glued vars ->

230 |                Core (Term vars)

231 | checkTermSub defining mode opts nest env env' sub tm ty

232 |     = do defs <- case mode of

233 |                       InType => branch -- might need to backtrack if there's

234 |                                        -- a case in the type

235 |                       _ => get Ctxt

236 |          ust <- get UST

237 |          mv <- get MD

238 |          res <-

239 |             catch {t = Error}

240 |                   (elabTermSub defining mode opts nest

241 |                                env env' sub tm (Just ty))

242 |                   $ \case

243 |                     TryWithImplicits loc benv ns

244 |                       => do put Ctxt defs

245 |                             put UST ust

246 |                             put MD mv

247 |                             tm' <- bindImps loc benv ns tm

248 |                             elabTermSub defining mode opts nest

249 |                                         env env' sub

250 |                                         tm' (Just ty)

251 |                     err => throw err

252 |          case mode of

253 |               InType => commit -- bracket the 'branch' above

254 |               _ => pure ()

256 |          pure (fst res)

257 |   where

258 |     bindImps' : FC -> Env Term vs -> List (Name, Term vs) -> RawImp ->

259 |                 Core RawImp

260 |     bindImps' loc env [] ty = pure ty

261 |     bindImps' loc env ((n, ty) :: ntys) sc

262 |         = pure $ IPi loc erased Implicit (Just n)

263 |                      (Implicit loc True) !(bindImps' loc env ntys sc)

265 |     bindImps : FC -> Env Term vs -> List (Name, Term vs) -> RawImp ->

266 |                Core RawImp

267 |     bindImps loc env ns (IBindHere fc m ty)

268 |         = pure $ IBindHere fc m !(bindImps' loc env ns ty)

269 |     bindImps loc env ns ty = bindImps' loc env ns ty

272 | checkTerm : {vars : _} ->

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

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

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

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

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

278 |             Int -> ElabMode -> List ElabOpt ->

279 |             NestedNames vars -> Env Term vars ->

280 |             RawImp -> Glued vars ->

281 |             Core (Term vars)

282 | checkTerm defining mode opts nest env tm ty

283 |     = checkTermSub defining mode opts nest env env Refl tm ty