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 | %default covering

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

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

 22 |   where

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

 24 |     drop [] = []

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

 26 |         = if x == n then drop xs

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

 29 | checkPiInfo : {vars : _} ->

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

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

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

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

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

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

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

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

 38 |               Core (PiInfo (Term vars))

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

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

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

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

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

 44 |          pure (DefImplicit tv)

 47 | checkPi : {vars : _} ->

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

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

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

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

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

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

 54 |           RigCount -> ElabInfo ->

 55 |           NestedNames vars -> Env Term vars ->

 56 |           FC ->

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

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

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

 60 |           Core (Term vars, Glued vars)

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

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

 63 |          tyu <- uniVar fc

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

 65 |                              (Just (gType fc tyu))

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

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

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

 69 |          scu <- uniVar fc

 70 |          (scopev, scopet) <-

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

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

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

 74 |          piu <- uniVar fc

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

 76 |   where

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

 78 |     -- it's always erased

 79 |     getRig : ElabMode -> RigCount

 80 |     getRig (InLHS _) = rig

 81 |     getRig _ = erased

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

 84 |              Maybe (Glued vars) -> Core RigCount

 85 | findLamRig Nothing = pure top

 86 | findLamRig (Just expty)

 87 |     = do tynf <- getNF expty

 88 |          case tynf of

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

 90 |               _ => pure top

 92 | inferLambda : {vars : _} ->

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

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

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

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

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

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

 99 |               RigCount -> ElabInfo ->

100 |               NestedNames vars -> Env Term vars ->

101 |               FC ->

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

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

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

105 |               Core (Term vars, Glued vars)

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

107 |     = do rigb_in <- findLamRig expTy

108 |          let rigb = rigb_in `glb` rigl

109 |          u <- uniVar fc

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

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

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

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

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

115 |                                 check {e=e'} rig elabinfo

116 |                                       nest' env' scope Nothing)

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

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

119 |          maybe (pure ())

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

121 |          checkExp rig elabinfo env fc

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

123 |                   lamty expTy

125 | getTyNF : {vars : _} ->

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

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

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

129 | getTyNF env x

130 |     = do defs <- get Ctxt

131 |          xnf <- nf defs env x

132 |          empty <- clearDefs defs

133 |          quote empty env xnf

136 | checkLambda : {vars : _} ->

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

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

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

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

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

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

143 |               RigCount -> ElabInfo ->

144 |               NestedNames vars -> Env Term vars ->

145 |               FC ->

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

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

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

149 |               Core (Term vars, Glued vars)

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

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

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

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

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

155 |          let solvemode = case elabMode elabinfo of

156 |                               InLHS _ => inLHS

157 |                               _ => inTerm

158 |          solveConstraints solvemode Normal

159 |          expty <- getTerm expty_in

160 |          exptynf <- getTyNF env expty

161 |          defs <- get Ctxt

162 |          case exptynf of

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

164 |                  do u <- uniVar fc'

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

166 |                                         argTy (Just (gType fc u))

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

168 |                     let rigb = rigl `glb` c

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

170 |                     ignore $ convert fc elabinfo env (gnf env tyv) (gnf env pty)

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

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

173 |                     (scopev, scopet) <-

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

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

176 |                                 (Just $ gnf env' pscnf))

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

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

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

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

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

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

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

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

187 |                     -- so we just need to check multiplicities

188 |                     when (rigb /= c) $

189 |                         throw (CantConvert fc (gamma defs) env

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

191 |                                   (Bind fc bn (Pi fc' c info' pty) psc))

192 |                     pure (Bind fc n (Lam fc' rigb info' tyv) scopev,

193 |                           gnf env (Bind fc n (Pi fc' rigb info' tyv) !(getTerm scopet)))

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

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

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

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

199 | weakenExp env Nothing = pure Nothing

200 | weakenExp env (Just gtm)

201 |     = do tm <- getTerm gtm

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

205 | checkLet : {vars : _} ->

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

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

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

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

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

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

212 |            RigCount -> ElabInfo ->

213 |            NestedNames vars -> Env Term vars ->

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

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

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

217 |            Core (Term vars, Glued vars)

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

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

220 |          u <- uniVar fc

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

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

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

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

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

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

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

228 |                              ({ preciseInf := True } elabinfo)

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

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

231 |               (\err => case linearErr err of

232 |                             Just r

233 |                               => do branchOne

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

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

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

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

238 |                                                   elabinfo -- without preciseInf

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

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

241 |                                      r

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

243 |                                                elabinfo -- without preciseInf

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

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

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

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

248 |          expScope <- weakenExp env' expty

249 |          (scopev, gscopet) <-

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

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

252 |          scopet <- getTerm gscopet

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

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

256 |          -- build the term directly

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

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

260 |          addNameType lhsFC n env tyv

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

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

264 |   where

265 |     linearErr : Error -> Maybe RigCount

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

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

268 |     linearErr (InCon _ e) = linearErr e

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

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

271 |     linearErr _ = Nothing