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 |                Meta {} => pure Nothing -- might be solved

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

 72 |                _ => pure $ Just tm

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

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

 76 |         = pure tm

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

 78 |         = pure tm

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

 80 |         = do defs <- get Ctxt

 81 |              n' <- genVarName (nameRoot n)

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

 83 |              sc' <- bindLamNF tm sctm

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

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

 86 |         = do defs <- get Ctxt

 87 |              n' <- genVarName (nameRoot n)

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

 89 |              sc' <- bindLamNF tm sctm

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

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

 92 |         = do defs <- get Ctxt

 93 |              n' <- genVarName (nameRoot n)

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

 95 |              sc' <- bindLamNF tm sctm

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

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

 98 |     bindLamNF tm sc = pure tm

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

101 |     bindLam tm gty

102 |         = do ty <- getTerm gty

103 |              Just tm' <- bindLamTm tm ty

104 |                 | Nothing =>

105 |                     do nf <- getNF gty

106 |                        bindLamNF tm nf

107 |              pure tm'

108 | insertImpLam env tm _ = pure tm

112 | checkTerm : {vars : _} ->

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

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

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

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

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

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

119 |             RigCount -> ElabInfo ->

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

121 |             Core (Term vars, Glued vars)

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

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

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

125 |       -- application with no arguments

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

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

128 |     = do n <- case p of

129 |                    Explicit => genVarName "arg"

130 |                    Implicit => genVarName "impArg"

131 |                    AutoImplicit => genVarName "conArg"

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

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

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

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

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

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

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

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

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

141 |     = do n <- genVarName "_"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

162 |     = do est <- get EST

163 |          nm <- genName "search"

164 |          expty <- getTerm gexpty

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

166 |          pure (sval, gexpty)

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

168 |     = do est <- get EST

169 |          nmty <- genName "searchTy"

170 |          u <- uniVar fc

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

172 |          nm <- genName "search"

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

174 |          pure (sval, gnf env ty)

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

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

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

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

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

180 |     = checkTerm rig elabinfo nest env tm exp

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

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

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

184 |     = checkBindVar rig elabinfo nest env fc n exp

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

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

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

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

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

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

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

192 |     = checkDelay rig elabinfo nest env fc tm exp

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

194 |     = checkForce rig elabinfo nest env fc tm exp

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

196 |     = checkQuote rig elabinfo nest env fc tm exp

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

198 |     = checkQuoteName rig elabinfo nest env fc n exp

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

200 |     = checkQuoteDecl rig elabinfo nest env fc ds exp

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

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

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

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

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

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

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

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

209 |     = do u <- uniVar fc

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

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

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

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

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

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

216 |     = do nm <- genName "_"

217 |          expty <- getTerm gexpty

218 |          metaval <- metaVar fc rig env nm expty

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

220 |          when (b && bindingVars elabinfo) $

221 |             do expty <- getTerm gexpty

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

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

224 |          pure (metaval, gexpty)

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

226 |     = do nmty <- genName "implicit_type"

227 |          u <- uniVar fc

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

229 |          nm <- genName "_"

230 |          metaval <- metaVar fc rig env nm ty

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

232 |          when (b && bindingVars elabinfo) $

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

234 |          pure (metaval, gnf env ty)

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

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

237 |          est <- get EST

238 |          rns <- resolveNames fc ns

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

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

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

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

245 |          newEST <- get EST

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

248 |          pure result

249 |   where

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

251 |     resolveNames fc [] = pure empty

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

253 |       case userNameRoot n of

254 |         -- should never happen

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

256 |         Just nRoot => do

257 |           -- this will always be a global name

258 |           -- so we lookup only among the globals

259 |           ctxt <- get Ctxt

260 |           rns <- lookupCtxtName n (gamma ctxt)

261 |           case rns of

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

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

264 |                      let nt = getDefNameType def

265 |                      let decor = nameDecoration def.fullname nt

266 |                      log "ide-mode.highlight" 7

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

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

269 |                    insert nRoot rn <$> resolveNames fc ns

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

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

287 |     = checkImp rigc elabinfo nest env tm exp

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

290 |     = checkImp rigc elabinfo nest env tm exp

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

292 |     = checkImp rigc elabinfo nest env tm exp

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

294 |     = checkImp rigc elabinfo nest env tm exp

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

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

297 |          case elabMode elabinfo of

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

299 |                  checkImp rigc elabinfo nest env tm exp

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

301 |                       checkImp rigc elabinfo nest env tm' exp

303 | onLHS : ElabMode -> Bool

304 | onLHS (InLHS {}) = True

305 | onLHS _ = False

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

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

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

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

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

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

324 |             do let (argv, argt) = res

325 |                let Just expty = exp

326 |                         | Nothing => pure ()

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

328 |          pure res