0 | module TTImp.Elab.Term

  2 | import Libraries.Data.UserNameMap

  4 | import Core.Env

  5 | import Core.Metadata

  6 | import Core.UnifyState

  7 | import Core.Value

  9 | import Idris.REPL.Opts

 10 | import Idris.Syntax

 12 | import TTImp.Elab.Ambiguity

 13 | import TTImp.Elab.App

 14 | import TTImp.Elab.As

 15 | import TTImp.Elab.Binders

 16 | import TTImp.Elab.Case

 17 | import TTImp.Elab.Check

 18 | import TTImp.Elab.Dot

 19 | import TTImp.Elab.Hole

 20 | import TTImp.Elab.ImplicitBind

 21 | import TTImp.Elab.Lazy

 22 | import TTImp.Elab.Local

 23 | import TTImp.Elab.Prim

 24 | import TTImp.Elab.Quote

 25 | import TTImp.Elab.Record

 26 | import TTImp.Elab.Rewrite

 27 | import TTImp.Elab.RunElab

 28 | import TTImp.TTImp

 30 | %default covering

 34 | insertImpLam : {auto c : Ref Ctxt Defs} ->

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

 36 |                Env Term vars ->

 37 |                (term : RawImp) -> (expected : Maybe (Glued vars)) ->

 38 |                Core RawImp

 39 | insertImpLam {vars} env tm (Just ty) = bindLam tm ty

 40 |   where

 41 |     -- If we can decide whether we need implicit lambdas without looking

 42 |     -- at the normal form, do so

 43 |     bindLamTm : RawImp -> Term vs -> Core (Maybe RawImp)

 44 |     bindLamTm tm@(ILam _ _ Implicit _ _ _) (Bind fc n (Pi _ _ Implicit _) sc)

 45 |         = pure (Just tm)

 46 |     bindLamTm tm@(ILam _ _ AutoImplicit _ _ _) (Bind fc n (Pi _ _ AutoImplicit _) sc)

 47 |         = pure (Just tm)

 48 |     bindLamTm tm@(ILam _ _ (DefImplicit _) _ _ _) (Bind fc n (Pi _ _ (DefImplicit _) _) sc)

 49 |         = pure (Just tm)

 50 |     bindLamTm tm (Bind fc n (Pi _ c Implicit ty) sc)

 51 |         = do n' <- genVarName (nameRoot n)

 52 |              Just sc' <- bindLamTm tm sc

 53 |                  | Nothing => pure Nothing

 54 |              pure $ Just (ILam fc c Implicit (Just n') (Implicit fc False) sc')

 55 |     bindLamTm tm (Bind fc n (Pi _ c AutoImplicit ty) sc)

 56 |         = do n' <- genVarName (nameRoot n)

 57 |              Just sc' <- bindLamTm tm sc

 58 |                  | Nothing => pure Nothing

 59 |              pure $ Just (ILam fc c AutoImplicit (Just n') (Implicit fc False) sc')

 60 |     bindLamTm tm (Bind fc n (Pi _ c (DefImplicit _) ty) sc)

 61 |         = do n' <- genVarName (nameRoot n)

 62 |              Just sc' <- bindLamTm tm sc

 63 |                  | Nothing => pure Nothing

 64 |              pure $ Just (ILam fc c (DefImplicit (Implicit fc False))

 65 |                                     (Just n') (Implicit fc False) sc')

 66 |     bindLamTm tm exp

 67 |         = case getFn exp of

 68 |                Ref _ Func _ => pure Nothing -- might still be implicit

 69 |                TForce {} => pure Nothing

 70 |                Bind _ _ (Lam {}) _ => pure Nothing

 71 |                _ => pure $ Just tm

 73 |     bindLamNF : RawImp -> NF vars -> Core RawImp

 74 |     bindLamNF tm@(ILam _ _ Implicit _ _ _) (NBind fc n (Pi _ _ Implicit _) sc)

 75 |         = pure tm

 76 |     bindLamNF tm@(ILam _ _ AutoImplicit _ _ _) (NBind fc n (Pi _ _ AutoImplicit _) sc)

 77 |         = pure tm

 78 |     bindLamNF tm (NBind fc n (Pi fc' c Implicit ty) sc)

 79 |         = do defs <- get Ctxt

 80 |              n' <- genVarName (nameRoot n)

 81 |              sctm <- sc defs (toClosure defaultOpts env (Ref fc Bound n'))

 82 |              sc' <- bindLamNF tm sctm

 83 |              pure $ ILam fc c Implicit (Just n') (Implicit fc False) sc'

 84 |     bindLamNF tm (NBind fc n (Pi fc' c AutoImplicit ty) sc)

 85 |         = do defs <- get Ctxt

 86 |              n' <- genVarName (nameRoot n)

 87 |              sctm <- sc defs (toClosure defaultOpts env (Ref fc Bound n'))

 88 |              sc' <- bindLamNF tm sctm

 89 |              pure $ ILam fc c AutoImplicit (Just n') (Implicit fc False) sc'

 90 |     bindLamNF tm (NBind fc n (Pi _ c (DefImplicit _) ty) sc)

 91 |         = do defs <- get Ctxt

 92 |              n' <- genVarName (nameRoot n)

 93 |              sctm <- sc defs (toClosure defaultOpts env (Ref fc Bound n'))

 94 |              sc' <- bindLamNF tm sctm

 95 |              pure $ ILam fc c (DefImplicit (Implicit fc False))

 96 |                               (Just n') (Implicit fc False) sc'

 97 |     bindLamNF tm sc = pure tm

 99 |     bindLam : RawImp -> Glued vars -> Core RawImp

100 |     bindLam tm gty

101 |         = do ty <- getTerm gty

102 |              Just tm' <- bindLamTm tm ty

103 |                 | Nothing =>

104 |                     do nf <- getNF gty

105 |                        bindLamNF tm nf

106 |              pure tm'

107 | insertImpLam env tm _ = pure tm

111 | checkTerm : {vars : _} ->

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

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

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

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

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

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

118 |             RigCount -> ElabInfo ->

119 |             NestedNames vars -> Env Term vars -> RawImp -> Maybe (Glued vars) ->

120 |             Core (Term vars, Glued vars)

121 | checkTerm rig elabinfo nest env (IVar fc n) exp

122 |     = -- It may actually turn out to be an application, if the expected

123 |       -- type is expecting an implicit argument, so check it as an

124 |       -- application with no arguments

125 |       checkApp rig elabinfo nest env fc (IVar fc n) [] [] [] exp

126 | checkTerm rig elabinfo nest env (IPi fc r p Nothing argTy retTy) exp

127 |     = do n <- case p of

128 |                    Explicit => genVarName "arg"

129 |                    Implicit => genVarName "impArg"

130 |                    AutoImplicit => genVarName "conArg"

131 |                    (DefImplicit _) => genVarName "defArg"

132 |          checkPi rig elabinfo nest env fc r p n argTy retTy exp

133 | checkTerm rig elabinfo nest env (IPi fc r p (Just (UN Underscore)) argTy retTy) exp

134 |     = checkTerm rig elabinfo nest env (IPi fc r p Nothing argTy retTy) exp

135 | checkTerm rig elabinfo nest env (IPi fc r p (Just n) argTy retTy) exp

136 |     = checkPi rig elabinfo nest env fc r p n argTy retTy exp

137 | checkTerm rig elabinfo nest env (ILam fc r p (Just n) argTy scope) exp

138 |     = checkLambda rig elabinfo nest env fc r p n argTy scope exp

139 | checkTerm rig elabinfo nest env (ILam fc r p Nothing argTy scope) exp

140 |     = do n <- genVarName "_"

141 |          checkLambda rig elabinfo nest env fc r p n argTy scope exp

142 | checkTerm rig elabinfo nest env (ILet fc lhsFC r n nTy nVal scope) exp

143 |     = checkLet rig elabinfo nest env fc lhsFC r n nTy nVal scope exp

144 | checkTerm rig elabinfo nest env (ICase fc opts scr scrty alts) exp

145 |     = checkCase rig elabinfo nest env fc opts scr scrty alts exp

146 | checkTerm rig elabinfo nest env (ILocal fc nested scope) exp

147 |     = checkLocal rig elabinfo nest env fc nested scope exp

148 | checkTerm rig elabinfo nest env (ICaseLocal fc uname iname args scope) exp

149 |     = checkCaseLocal rig elabinfo nest env fc uname iname args scope exp

150 | checkTerm rig elabinfo nest env (IUpdate fc upds rec) exp

151 |     = checkUpdate rig elabinfo nest env fc upds rec exp

152 | checkTerm rig elabinfo nest env (IApp fc fn arg) exp

153 |     = checkApp rig elabinfo nest env fc fn [arg] [] []  exp

154 | checkTerm rig elabinfo nest env (IAutoApp fc fn arg) exp

155 |     = checkApp rig elabinfo nest env fc fn [] [arg] []  exp

156 | checkTerm rig elabinfo nest env (IWithApp fc fn arg) exp

157 |     = throw (GenericMsg fc "with application not implemented yet")

158 | checkTerm rig elabinfo nest env (INamedApp fc fn nm arg) exp

159 |     = checkApp rig elabinfo nest env fc fn [] [] [(nm, arg)] exp

160 | checkTerm rig elabinfo nest env (ISearch fc depth) (Just gexpty)

161 |     = do est <- get EST

162 |          nm <- genName "search"

163 |          expty <- getTerm gexpty

164 |          sval <- searchVar fc rig depth (Resolved (defining est)) env nest nm expty

165 |          pure (sval, gexpty)

166 | checkTerm rig elabinfo nest env (ISearch fc depth) Nothing

167 |     = do est <- get EST

168 |          nmty <- genName "searchTy"

169 |          u <- uniVar fc

170 |          ty <- metaVar fc erased env nmty (TType fc u)

171 |          nm <- genName "search"

172 |          sval <- searchVar fc rig depth (Resolved (defining est)) env nest nm ty

173 |          pure (sval, gnf env ty)

174 | checkTerm rig elabinfo nest env (IAlternative fc uniq alts) exp

175 |     = checkAlternative rig elabinfo nest env fc uniq alts exp

176 | checkTerm rig elabinfo nest env (IRewrite fc rule tm) exp

177 |     = checkRewrite rig elabinfo nest env fc rule tm exp

178 | checkTerm rig elabinfo nest env (ICoerced fc tm) exp

179 |     = checkTerm rig elabinfo nest env tm exp

180 | checkTerm rig elabinfo nest env (IBindHere fc binder sc) exp

181 |     = checkBindHere rig elabinfo nest env fc binder sc exp

182 | checkTerm rig elabinfo nest env (IBindVar fc n) exp

183 |     = checkBindVar rig elabinfo nest env fc n exp

184 | checkTerm rig elabinfo nest env (IAs fc nameFC side n_in tm) exp

185 |     = checkAs rig elabinfo nest env fc nameFC side n_in tm exp

186 | checkTerm rig elabinfo nest env (IMustUnify fc reason tm) exp

187 |     = checkDot rig elabinfo nest env fc reason tm exp

188 | checkTerm rig elabinfo nest env (IDelayed fc r tm) exp

189 |     = checkDelayed rig elabinfo nest env fc r tm exp

190 | checkTerm rig elabinfo nest env (IDelay fc tm) exp

191 |     = checkDelay rig elabinfo nest env fc tm exp

192 | checkTerm rig elabinfo nest env (IForce fc tm) exp

193 |     = checkForce rig elabinfo nest env fc tm exp

194 | checkTerm rig elabinfo nest env (IQuote fc tm) exp

195 |     = checkQuote rig elabinfo nest env fc tm exp

196 | checkTerm rig elabinfo nest env (IQuoteName fc n) exp

197 |     = checkQuoteName rig elabinfo nest env fc n exp

198 | checkTerm rig elabinfo nest env (IQuoteDecl fc ds) exp

199 |     = checkQuoteDecl rig elabinfo nest env fc ds exp

200 | checkTerm rig elabinfo nest env (IUnquote fc tm) exp

201 |     = throw (GenericMsg fc "Can't escape outside a quoted term")

202 | checkTerm rig elabinfo nest env (IRunElab fc re tm) exp

203 |     = checkRunElab rig elabinfo nest env fc re tm exp

204 | checkTerm {vars} rig elabinfo nest env (IPrimVal fc c) exp

205 |     = do let (cval, cty) = checkPrim {vars} fc c

206 |          checkExp rig elabinfo env fc cval (gnf env cty) exp

207 | checkTerm rig elabinfo nest env (IType fc) exp

208 |     = do u <- uniVar fc

209 |          checkExp rig elabinfo env fc (TType fc u) (gType fc u) exp

210 | checkTerm rig elabinfo nest env (IHole fc str) exp

211 |     = checkHole rig elabinfo nest env fc (Basic str) exp

212 | checkTerm rig elabinfo nest env (IUnifyLog fc lvl tm) exp

213 |     = withLogLevel lvl $ check rig elabinfo nest env tm exp

214 | checkTerm rig elabinfo nest env (Implicit fc b) (Just gexpty)

215 |     = do nm <- genName "_"

216 |          expty <- getTerm gexpty

217 |          metaval <- metaVar fc rig env nm expty

218 |          -- Add to 'bindIfUnsolved' if 'b' set

219 |          when (b && bindingVars elabinfo) $

220 |             do expty <- getTerm gexpty

221 |                -- Explicit because it's an explicitly given thing!

222 |                update EST $ addBindIfUnsolved nm fc rig Explicit env metaval expty

223 |          pure (metaval, gexpty)

224 | checkTerm rig elabinfo nest env (Implicit fc b) Nothing

225 |     = do nmty <- genName "implicit_type"

226 |          u <- uniVar fc

227 |          ty <- metaVar fc erased env nmty (TType fc u)

228 |          nm <- genName "_"

229 |          metaval <- metaVar fc rig env nm ty

230 |          -- Add to 'bindIfUnsolved' if 'b' set

231 |          when (b && bindingVars elabinfo) $

232 |             update EST $ addBindIfUnsolved nm fc rig Explicit env metaval ty

233 |          pure (metaval, gnf env ty)

234 | checkTerm rig elabinfo nest env (IWithUnambigNames fc ns rhs) exp

235 |     = do -- enter the scope -> add unambiguous names

236 |          est <- get EST

237 |          rns <- resolveNames fc ns

238 |          put EST $ { unambiguousNames := mergeLeft rns (unambiguousNames est) } est

240 |          -- inside the scope -> check the RHS

241 |          result <- check rig elabinfo nest env rhs exp

243 |          -- exit the scope -> restore unambiguous names

244 |          newEST <- get EST

245 |          put EST $ { unambiguousNames := unambiguousNames est } newEST

247 |          pure result

248 |   where

249 |     resolveNames : FC -> List (FC, Name) -> Core (UserNameMap (Name, Int, GlobalDef))

250 |     resolveNames fc [] = pure empty

251 |     resolveNames fc ((nfc, n) :: ns) =

252 |       case userNameRoot n of

253 |         -- should never happen

254 |         Nothing => throw $ InternalError $ "non-UN in \"with\" LHS: " ++ show n

255 |         Just nRoot => do

256 |           -- this will always be a global name

257 |           -- so we lookup only among the globals

258 |           ctxt <- get Ctxt

259 |           rns <- lookupCtxtName n (gamma ctxt)

260 |           case rns of

261 |             [rn@(_, _, def)] =>

262 |                 do whenJust (isConcreteFC nfc) $ \nfc => do

263 |                      let nt = getDefNameType def

264 |                      let decor = nameDecoration def.fullname nt

265 |                      log "ide-mode.highlight" 7

266 |                        $ "`with' unambiguous name is adding " ++ show decor ++ ": " ++ show def.fullname

267 |                      addSemanticDecorations [(nfc, decor, Just def.fullname)]

268 |                    insert nRoot rn <$> resolveNames fc ns

269 |             rns  => ambiguousName fc n (map fst rns)

285 | TTImp.Elab.Check.check rigc elabinfo nest env (ICoerced fc tm) exp

286 |     = checkImp rigc elabinfo nest env tm exp

288 | TTImp.Elab.Check.check rigc elabinfo nest env tm@(ILet {}) exp

289 |     = checkImp rigc elabinfo nest env tm exp

290 | TTImp.Elab.Check.check rigc elabinfo nest env tm@(ILocal {}) exp

291 |     = checkImp rigc elabinfo nest env tm exp

292 | TTImp.Elab.Check.check rigc elabinfo nest env tm@(IUpdate {}) exp

293 |     = checkImp rigc elabinfo nest env tm exp

294 | TTImp.Elab.Check.check rigc elabinfo nest env tm_in exp

295 |     = do tm <- expandAmbigName (elabMode elabinfo) nest env tm_in [] tm_in exp

296 |          case elabMode elabinfo of

297 |               InLHS _ => -- Don't expand implicit lambda on lhs

298 |                  checkImp rigc elabinfo nest env tm exp

299 |               _ => do tm' <- insertImpLam env tm exp

300 |                       checkImp rigc elabinfo nest env tm' exp

302 | onLHS : ElabMode -> Bool

303 | onLHS (InLHS {}) = True

304 | onLHS _ = False

317 | TTImp.Elab.Check.checkImp rigc elabinfo nest env tm exp

318 |     = do res <- checkTerm rigc elabinfo nest env tm exp

319 |          -- LHS arguments can't infer their own type - they need to be inferred

320 |          -- from some other argument. This is to prevent arguments being not

321 |          -- polymorphic enough. So, here, add the constraint to be checked later.

322 |          when (onLHS (elabMode elabinfo) && not (topLevel elabinfo)) $

323 |             do let (argv, argt) = res

324 |                let Just expty = exp

325 |                         | Nothing => pure ()

326 |                addPolyConstraint (getFC tm) env argv !(getNF expty) !(getNF argt)

327 |          pure res