0 | module TTImp.Elab.Binders

  2 | import Core.Env

  3 | import Core.Metadata

  4 | import Core.Unify

  5 | import Core.Value

  7 | import Idris.REPL.Opts

  8 | import Idris.Syntax

 10 | import TTImp.Elab.Check

 11 | import TTImp.Elab.Delayed

 12 | import TTImp.TTImp

 14 | import Libraries.Data.IntMap

 16 | %default covering

 22 | dropName : Name -> NestedNames vars -> NestedNames vars

 23 | dropName n nest = { names $= drop } nest

 24 |   where

 25 |     drop : List (Name, a) -> List (Name, a)

 26 |     drop [] = []

 27 |     drop ((x, y) :: xs)

 28 |         = if x == n then drop xs

 29 |              else (x, y) :: drop xs

 31 | checkPiInfo : {vars : _} ->

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

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

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

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

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

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

 38 |               RigCount -> ElabInfo -> NestedNames vars -> Env Term vars ->

 39 |               PiInfo RawImp -> (expTy : Maybe (Glued vars)) ->

 40 |               Core (PiInfo (Term vars))

 41 | checkPiInfo rig elabinfo nest env Explicit exp = pure Explicit

 42 | checkPiInfo rig elabinfo nest env Implicit exp = pure Implicit

 43 | checkPiInfo rig elabinfo nest env AutoImplicit exp = pure AutoImplicit

 44 | checkPiInfo rig elabinfo nest env (DefImplicit t) exp

 45 |     = do (tv, _) <- check rig elabinfo nest env t exp

 46 |          pure (DefImplicit tv)

 49 | checkPi : {vars : _} ->

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

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

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

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

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

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

 56 |           RigCount -> ElabInfo ->

 57 |           NestedNames vars -> Env Term vars ->

 58 |           FC ->

 59 |           RigCount -> PiInfo RawImp -> (n : Name) ->

 60 |           (argTy : RawImp) -> (retTy : RawImp) ->

 61 |           (expTy : Maybe (Glued vars)) ->

 62 |           Core (Term vars, Glued vars)

 63 | checkPi rig elabinfo nest env fc rigf info n argTy retTy expTy

 64 |     = do let pirig = getRig (elabMode elabinfo)

 65 |          tyu <- uniVar fc

 66 |          (tyv, tyt) <- check pirig elabinfo nest env argTy

 67 |                              (Just (gType fc tyu))

 68 |          info' <- checkPiInfo rigf elabinfo nest env info (Just (gnf env tyv))

 69 |          let env' : Env Term (n :: _) = Pi fc rigf info' tyv :: env

 70 |          let nest' = weaken (dropName n nest)

 71 |          scu <- uniVar fc

 72 |          (scopev, scopet) <-

 73 |             inScope fc env' (\e' =>

 74 |               check {e=e'} pirig elabinfo nest' env' retTy (Just (gType fc scu)))

 75 |          -- TODO Cumulativity: tyu <= max, scu <= max

 76 |          piu <- uniVar fc

 77 |          checkExp rig elabinfo env fc (Bind fc n (Pi (getFC argTy) rigf info' tyv) scopev) (gType fc piu) expTy

 78 |   where

 79 |     -- Might want to match on the LHS, so use the context rig, otherwise

 80 |     -- it's always erased

 81 |     getRig : ElabMode -> RigCount

 82 |     getRig (InLHS _) = rig

 83 |     getRig _ = erased

 85 | findLamRig : {auto c : Ref Ctxt Defs} ->

 86 |              Maybe (Glued vars) -> Core RigCount

 87 | findLamRig Nothing = pure top

 88 | findLamRig (Just expty)

 89 |     = do tynf <- getNF expty

 90 |          case tynf of

 91 |               NBind _ _ (Pi _ c _ _) sc => pure c

 92 |               _ => pure top

 94 | inferLambda : {vars : _} ->

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

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

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

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

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

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

101 |               RigCount -> ElabInfo ->

102 |               NestedNames vars -> Env Term vars ->

103 |               FC ->

104 |               RigCount -> PiInfo RawImp -> (n : Name) ->

105 |               (argTy : RawImp) -> (scope : RawImp) ->

106 |               (expTy : Maybe (Glued vars)) ->

107 |               Core (Term vars, Glued vars)

108 | inferLambda rig elabinfo nest env fc rigl info n argTy scope expTy

109 |     = do rigb_in <- findLamRig expTy

110 |          let rigb = rigb_in `glb` rigl

111 |          u <- uniVar fc

112 |          (tyv, tyt) <- check erased elabinfo nest env argTy (Just (gType fc u))

113 |          info' <- checkPiInfo rigl elabinfo nest env info (Just (gnf env tyv))

114 |          let env' : Env Term (n :: _) = Lam fc rigb info' tyv :: env

115 |          let nest' = weaken (dropName n nest)

116 |          (scopev, scopet) <- inScope fc env' (\e' =>

117 |                                 check {e=e'} rig elabinfo

118 |                                       nest' env' scope Nothing)

119 |          let lamty = gnf env (Bind fc n (Pi fc rigb info' tyv) !(getTerm scopet))

120 |          logGlue "elab.binder" 5 "Inferred lambda type" lamty

121 |          maybe (pure ())

122 |                (logGlueNF "elab.binder" 5 "Expected lambda type" env) expTy

123 |          checkExp rig elabinfo env fc

124 |                   (Bind fc n (Lam fc rigb info' tyv) scopev)

125 |                   lamty expTy

127 | getTyNF : {vars : _} ->

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

129 |           Env Term vars -> Term vars -> Core (Term vars)

130 | getTyNF env x@(Bind {}) = pure x

131 | getTyNF env x

132 |     = do defs <- get Ctxt

133 |          xnf <- nf defs env x

134 |          empty <- clearDefs defs

135 |          quote empty env xnf

141 | isResolved : IntMap Constraint -> (constraintId : Int) ->  Bool

142 | isResolved constraints key

143 |   = case lookup key constraints of

144 |          Just Resolved => True

145 |          _ => False

148 | checkLambda : {vars : _} ->

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

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

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

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

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

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

155 |               RigCount -> ElabInfo ->

156 |               NestedNames vars -> Env Term vars ->

157 |               FC ->

158 |               RigCount -> PiInfo RawImp -> (n : Name) ->

159 |               (argTy : RawImp) -> (scope : RawImp) ->

160 |               (expTy : Maybe (Glued vars)) ->

161 |               Core (Term vars, Glued vars)

162 | checkLambda rig_in elabinfo nest env fc rigl info n argTy scope Nothing

163 |     = let rig = if isErased rig_in then erased else linear in

164 |           inferLambda rig elabinfo nest env fc rigl info n argTy scope Nothing

165 | checkLambda rig_in elabinfo nest env fc rigl info n argTy scope (Just expty_in)

166 |     = do let rig = if isErased rig_in then erased else linear

167 |          let solvemode = case elabMode elabinfo of

168 |                               InLHS _ => inLHS

169 |                               _ => inTerm

170 |          solveConstraints solvemode Normal

171 |          expty <- getTerm expty_in

172 |          exptynf <- getTyNF env expty

173 |          defs <- get Ctxt

174 |          case exptynf of

175 |               Bind bfc bn (Pi fc' c _ pty) psc =>

176 |                  do u <- uniVar fc'

177 |                     (tyv, tyt) <- check erased elabinfo nest env

178 |                                         argTy (Just (gType fc u))

179 |                     info' <- checkPiInfo rigl elabinfo nest env info (Just (gnf env tyv))

180 |                     let originalPiType = Bind fc bn (Pi fc' c info' pty) psc

181 |                     let rigb = rigl `glb` c

182 |                     let env' : Env Term (n :: _) = Lam fc rigb info' tyv :: env

183 |                     lambdaUnifyResult <- convert fc elabinfo env (gnf env tyv) (gnf env pty)

184 |                     let nest' = weaken (dropName n nest)

185 |                     pscnf <- normaliseHoles defs env' $ compat psc

186 |                     (scopev, scopet) <-

187 |                        inScope fc env' (\e' =>

188 |                           check {e=e'} rig elabinfo nest' env' scope

189 |                                 (Just $ gnf env' pscnf))

190 |                     let elaboratedPiType = Bind fc n (Pi fc' rigb info' tyv) !(getTerm scopet)

191 |                     logTermNF "elab.binder" 10 "Lambda type" env exptynf

192 |                     logGlueNF "elab.binder" 10 "Got scope type" env' scopet

194 |                     -- Currently, the fc a PLam holds (and that ILam gets as a consequence)

195 |                     -- is the file context of the argument to the lambda. This fits nicely

196 |                     -- in this exact use, but is likely a bug.

197 |                     log "metadata.names" 7 "checkLambda is adding ↓"

198 |                     addNameType fc n env pty -- Add the type of the argument to the metadata

200 |                     -- We've already checked the argument and scope types,

201 |                     -- so we just need to check multiplicities

202 |                     when (rigb /= c) $

203 |                         throw (CantConvert fc (gamma defs) env

204 |                                   elaboratedPiType

205 |                                   originalPiType)

206 |                     let lamTerm = Bind fc n (Lam fc' rigb info' tyv) scopev

207 |                     let lamType = gnf env elaboratedPiType

208 |                     let lambdaConstraints = constraints lambdaUnifyResult

209 |                     -- check if elaborating the body solved the constraints we collected earlied

210 |                     allCs <- constraints <$> get UST

211 |                     let prunedConstraints = filter (not . isResolved allCs) lambdaConstraints

212 |                     if null prunedConstraints

213 |                        then pure (lamTerm, lamType)

214 |                        else do ctm <- newConstant fc rig env lamTerm lamTerm prunedConstraints

215 |                                pure (ctm, lamType)

216 |               _ => inferLambda rig elabinfo nest env fc rigl info n argTy scope (Just expty_in)

218 | weakenExp : {x, vars : _} ->

219 |             Env Term (x :: vars) ->

220 |             Maybe (Glued vars) -> Core (Maybe (Glued (x :: vars)))

221 | weakenExp env Nothing = pure Nothing

222 | weakenExp env (Just gtm)

223 |     = do tm <- getTerm gtm

224 |          pure (Just (gnf env (weaken tm)))

227 | checkLet : {vars : _} ->

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

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

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

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

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

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

234 |            RigCount -> ElabInfo ->

235 |            NestedNames vars -> Env Term vars ->

236 |            FC -> (lhsFC : FC) -> RigCount -> (n : Name) ->

237 |            (nTy : RawImp) -> (nVal : RawImp) -> (scope : RawImp) ->

238 |            (expTy : Maybe (Glued vars)) ->

239 |            Core (Term vars, Glued vars)

240 | checkLet rigc_in elabinfo nest env fc lhsFC rigl n nTy nVal scope expty {vars}

241 |     = do let rigc = if isErased rigc_in then erased else linear

242 |          u <- uniVar fc

243 |          (tyv, tyt) <- check erased elabinfo nest env nTy (Just (gType fc u))

244 |          -- Try checking at the given multiplicity; if that doesn't work,

245 |          -- try checking at Rig1 (meaning that we're using a linear variable

246 |          -- so the resulting binding should be linear)

247 |          -- Also elaborate any case blocks in the value via runDelays

248 |          (valv, valt, rigb) <- handle

249 |               (do c <- runDelays (==CaseBlock) $ check (rigl |*| rigc)

250 |                              ({ preciseInf := True } elabinfo)

251 |                              nest env nVal (Just (gnf env tyv))

252 |                   pure (fst c, snd c, rigl |*| rigc))

253 |               (\err => case linearErr err of

254 |                             Just r

255 |                               => do branchOne

256 |                                      (do c <- runDelays (==CaseBlock) $ check linear elabinfo

257 |                                                   nest env nVal (Just (gnf env tyv))

258 |                                          pure (fst c, snd c, linear))

259 |                                      (do c <- check (rigl |*| rigc)

260 |                                                   elabinfo -- without preciseInf

261 |                                                   nest env nVal (Just (gnf env tyv))

262 |                                          pure (fst c, snd c, rigMult rigl rigc))

263 |                                      r

264 |                             _ => do c <- check (rigl |*| rigc)

265 |                                                elabinfo -- without preciseInf

266 |                                                nest env nVal (Just (gnf env tyv))

267 |                                     pure (fst c, snd c, rigl |*| rigc))

268 |          let env' : Env Term (n :: _) = Lam fc rigb Explicit tyv :: env

269 |          let nest' = weaken (dropName n nest)

270 |          expScope <- weakenExp env' expty

271 |          (scopev, gscopet) <-

272 |             inScope fc env' (\e' =>

273 |               check {e=e'} rigc elabinfo nest' env' scope expScope)

274 |          scopet <- getTerm gscopet

276 |          -- No need to 'checkExp' here - we've already checked scopet

277 |          -- against the expected type when checking the scope, so just

278 |          -- build the term directly

280 |          -- Add the lhs of the let to metadata

281 |          log "metadata.names" 7 $ "checkLet is adding ↓"

282 |          addNameType lhsFC n env tyv

284 |          pure (Bind fc n (Let fc rigb valv tyv) scopev,

285 |                gnf env (Bind fc n (Let fc rigb valv tyv) scopet))

286 |   where

287 |     linearErr : Error -> Maybe RigCount

288 |     linearErr (LinearMisuse _ _ r _) = Just r

289 |     linearErr (InType _ _ e) = linearErr e

290 |     linearErr (InCon _ e) = linearErr e

291 |     linearErr (InLHS _ _ e) = linearErr e

292 |     linearErr (InRHS _ _ e) = linearErr e

293 |     linearErr _ = Nothing