0 | module Idris.Elab.Interface

  2 | import Core.Env

  3 | import Core.Metadata

  4 | import Core.Unify

  6 | import Idris.Doc.String

  7 | import Idris.REPL.Opts

  8 | import Idris.Syntax

 10 | import TTImp.BindImplicits

 11 | import TTImp.ProcessDecls

 12 | import TTImp.Elab.Check

 13 | import TTImp.TTImp

 14 | import TTImp.Utils

 16 | import Libraries.Data.ANameMap

 17 | import Libraries.Data.List.Extra

 18 | import Libraries.Data.WithDefault

 20 | %default covering

 25 | record Signature where

 26 |   constructor MkSignature

 27 |   count    : RigCount

 28 |   flags    : List FnOpt

 29 |   name     : WithFC Name

 30 |   isData   : Bool

 31 |   type     : RawImp

 33 | constructorBindName : Name

 34 | constructorBindName = UN (Basic "__con")

 38 | namePis : Int -> RawImp -> RawImp

 39 | namePis i (IPi fc r info n ty sc)

 40 |     = let (n', i') = if isImplicit info && isUnnamed n

 41 |                         then (Just (MN "i_con" i), i + 1)

 42 |                         else (n, i)

 43 |        in IPi fc r info n' ty (namePis i' sc)

 44 |   where

 45 |     isUnnamed : Maybe Name -> Bool

 46 |     isUnnamed = maybe True isUnderscoreName

 47 | namePis i (IBindHere fc m ty) = IBindHere fc m (namePis i ty)

 48 | namePis i ty = ty

 50 | getSig : ImpDecl -> Maybe Signature

 51 | getSig (IClaim (MkWithData _ $ MkIClaimData c _ opts ty))

 52 |     = Just $ MkSignature { count    = c

 53 |                          , flags    = opts

 54 |                          , name     = ty.tyName

 55 |                          , isData   = False

 56 |                          , type     = namePis 0 ty.val

 57 |                          }

 58 | getSig (IData _ _ _ (MkImpLater fc n ty))

 59 |     = Just $ MkSignature { count    = erased

 60 |                          , flags    = [Invertible]

 61 |                          , name     = NoFC n

 62 |                          , isData   = True

 63 |                          , type     = namePis 0 ty

 64 |                          }

 65 | getSig _ = Nothing

 73 | mkDataTy : FC -> List (Name, (RigCount, RawImp)) -> RawImp

 74 | mkDataTy fc [] = IType fc

 75 | mkDataTy fc ((n, (_, ty)) :: ps)

 76 |     = IPi fc top Explicit (Just n) ty (mkDataTy fc ps)

 78 | jname : (Name, (RigCount, RawImp)) -> (Maybe Name, RigCount, RawImp)

 79 | jname (n, rig, t) = (Just n, rig, t)

 81 | mkTy : FC -> PiInfo RawImp ->

 82 |        List (Maybe Name, RigCount, RawImp) -> RawImp -> RawImp

 83 | mkTy fc imp [] ret = ret

 84 | mkTy fc imp ((n, c, argty) :: args) ret

 85 |     = IPi fc c imp n argty (mkTy fc imp args ret)

 87 | mkIfaceData : {vars : _} ->

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

 89 |               FC -> WithDefault Visibility Private -> Env Term vars ->

 90 |               List (Maybe Name, RigCount, RawImp) ->

 91 |               Name -> Name -> List (Name, (RigCount, RawImp)) ->

 92 |               Maybe (List1 Name) -> List (Name, RigCount, RawImp) -> Core ImpDecl

 93 | mkIfaceData {vars} ifc def_vis env constraints n conName ps dets meths

 94 |     = let opts = [NoHints, UniqueSearch] ++

 95 |                  maybe [] (singleton . SearchBy) dets

 96 |           pNames = map fst ps

 97 |           retty = apply (IVar vfc n) (map (IVar EmptyFC) pNames)

 98 |           conty = mkTy vfc Implicit (map jname ps) $

 99 |                   mkTy vfc AutoImplicit (map bhere constraints) $

100 |                   mkTy vfc Explicit (map bname meths) retty

101 |           con = Mk [vfc, NoFC conName] !(bindTypeNames ifc [] (pNames ++ map fst meths ++ toList vars) conty)

102 |           bound = pNames ++ map fst meths ++ toList vars in

104 |           pure $ IData vfc def_vis Nothing {- ?? -}

105 |                $ MkImpData vfc n

106 |                    (Just !(bindTypeNames ifc [] bound (mkDataTy vfc ps)))

107 |                    opts [con]

108 |   where

109 |     vfc : FC

110 |     vfc = virtualiseFC ifc

112 |     bname : (Name, RigCount, RawImp) -> (Maybe Name, RigCount, RawImp)

113 |     bname (n, c, t) = (Just n, c, IBindHere (getFC t) (PI erased) t)

115 |     bhere : (Maybe Name, RigCount, RawImp) -> (Maybe Name, RigCount, RawImp)

116 |     bhere (n, c, t) = (n, c, IBindHere (getFC t) (PI erased) t)

120 | getMethDecl : {vars : _} ->

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

122 |               Env Term vars -> NestedNames vars ->

123 |               (params : List (Name, (RigCount, RawImp))) ->

124 |               (mnames : List Name) ->

125 |               (RigCount, nm, RawImp) ->

126 |               Core (nm, RigCount, RawImp)

127 | getMethDecl {vars} env nest params mnames (c, nm, ty)

128 |     = do let paramNames = map fst params

129 |          ty_imp <- bindTypeNames EmptyFC [] (paramNames ++ mnames ++ toList vars) ty

130 |          pure (nm, c, stripParams paramNames ty_imp)

131 |   where

132 |     -- We don't want the parameters to explicitly appear in the method

133 |     -- type in the record for the interface (they are parameters of the

134 |     -- interface type), so remove it here

135 |     stripParams : List Name -> RawImp -> RawImp

136 |     stripParams ps (IPi fc r p mn arg ret)

137 |         = if (maybe False (\n => n `elem` ps) mn)

138 |              then stripParams ps ret

139 |              else IPi fc r p mn arg (stripParams ps ret)

140 |     stripParams ps ty = ty

144 | bindIFace : FC -> RawImp -> RawImp -> RawImp

145 | bindIFace fc ity sc = IPi fc top AutoImplicit (Just constructorBindName) ity sc

148 | getMethToplevel : {vars : _} ->

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

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

151 |                   Env Term vars -> Visibility ->

152 |                   Name -> Name ->

153 |                   (allmeths : List Name) ->

154 |                   (bindNames : List Name) ->

155 |                   (params : List (Name, (RigCount, RawImp))) ->

156 |                   (Name, Signature) ->

157 |                   Core (List ImpDecl)

158 | getMethToplevel {vars} env vis iname cname allmeths bindNames params (mname, sig)

159 |     = do let paramNames = map fst params

160 |          let ity = apply (IVar vfc iname) (map (IVar EmptyFC) paramNames)

161 |          -- Make the constraint application explicit for any method names

162 |          -- which appear in other method types

163 |          let ty_constr =

164 |              substNames (toList vars) (map applyCon allmeths) sig.type

165 |          ty_imp <- bindTypeNames EmptyFC [] (toList vars) (bindPs params $ bindIFace vfc ity ty_constr)

166 |          cn <- traverse inCurrentNS sig.name

167 |          let tydecl = IClaim (MkFCVal vfc $ MkIClaimData sig.count vis (if sig.isData then [Inline, Invertible]

168 |                                             else [Inline])

169 |                                       (Mk [vfc, cn] ty_imp))

170 |          let conapp = apply (IVar vfc cname) (map (IBindVar EmptyFC) bindNames)

172 |          let lhs = INamedApp vfc

173 |                              (IVar cn.fc cn.val) -- See #3409

174 |                              constructorBindName

175 |                              conapp

176 |          let rhs = IVar EmptyFC mname

178 |          -- EtaExpand implicits on both sides:

179 |          -- First, obtain all the implicit names in the prefix of

180 |          -- See idris-lang/Idris2#3474

181 |          (lhs, rhs) <- etaExpandImplicits vfc sig.type lhs rhs

183 |          let fnclause = PatClause vfc lhs rhs

184 |          let fndef = IDef vfc cn.val [fnclause]

185 |          pure [tydecl, fndef]

186 |   where

187 |     vfc : FC

188 |     vfc = virtualiseFC sig.name.fc

190 |     -- Bind the type parameters given explicitly - there might be information

191 |     -- in there that we can't infer after all

192 |     bindPs : List (Name, (RigCount, RawImp)) -> RawImp -> RawImp

193 |     bindPs [] ty = ty

194 |     bindPs ((n, rig, pty) :: ps) ty

195 |         = IPi (getFC pty) rig Implicit (Just n) pty (bindPs ps ty)

197 |     applyCon : Name -> (Name, RawImp)

198 |     applyCon n

199 |       = (n, INamedApp vfc (IVar vfc n) constructorBindName (IVar vfc constructorBindName))

203 | getConstraintHint : {vars : _} ->

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

205 |                     FC -> Env Term vars -> Visibility ->

206 |                     Name -> Name ->

207 |                     (constraints : List Name) ->

208 |                     (allmeths : List Name) ->

209 |                     (params : List (Name, RigCount, RawImp)) ->

210 |                     (Name, RawImp) -> Core (Name, List ImpDecl)

211 | getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, con)

212 |     = do let pNames = map fst params

213 |          let ity = apply (IVar fc iname) (map (IVar fc) pNames)

214 |          let fty = mkTy fc Implicit (map jname params) $

215 |                    mkTy fc Explicit [(Nothing, top, ity)] con

216 |          ty_imp <- bindTypeNames fc [] (pNames ++ meths ++ toList vars) fty

217 |          let hintname = DN ("Constraint " ++ show con)

218 |                            (UN (Basic $ "__" ++ show iname ++ "_" ++ show con))

220 |          let tydecl = IClaim (MkFCVal fc $ MkIClaimData top vis [Inline, Hint False]

221 |                              (Mk [EmptyFC, NoFC hintname] ty_imp))

223 |          let conapp = apply (impsBind (IVar fc cname) constraints)

224 |                             (map (const (Implicit fc True)) meths)

226 |          let fnclause = PatClause fc (IApp fc (IVar fc hintname) conapp)

227 |                                      (IVar fc cn)

228 |          let fndef = IDef fc hintname [fnclause]

229 |          pure (hintname, [tydecl, fndef])

230 |   where

232 |     impsBind : RawImp -> List Name -> RawImp

233 |     impsBind fn [] = fn

234 |     impsBind fn (n :: ns)

235 |         = impsBind (IAutoApp fc fn (IBindVar fc n)) ns

238 | getDefault : ImpDecl -> Maybe (FC, List FnOpt, Name, List ImpClause)

239 | getDefault (IDef fc n cs) = Just (fc, [], n, cs)

240 | getDefault _ = Nothing

242 | mkCon : FC -> Name -> Name

243 | mkCon loc (NS ns (UN n))

244 |    = let str = displayUserName n in

245 |      NS ns (DN (str ++ " at " ++ show loc) (UN $ Basic ("__mk" ++ str)))

246 | mkCon loc n

247 |    = let str = show n in

248 |      DN (str ++ " at " ++ show loc) (UN $ Basic ("__mk" ++  str))

250 | updateIfaceSyn : {auto c : Ref Ctxt Defs} ->

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

252 |                  Name -> Name -> List Name -> List Name -> List RawImp ->

253 |                  List Signature -> List (Name, List ImpClause) ->

254 |                  Core ()

255 | updateIfaceSyn iname cn impps ps cs ms ds

256 |     = do ms' <- traverse totMeth ms

257 |          let info = MkIFaceInfo cn impps ps cs ms' ds

258 |          update Syn { ifaces     $= addName iname info,

259 |                       saveIFaces $= (iname :: ) }

260 |  where

261 |     totMeth : Signature -> Core Method

262 |     totMeth decl

263 |         = do let treq = findTotality decl.flags

264 |              pure $ Mk [decl.name, decl.count, treq] decl.type

268 | getImplParams : Term vars -> List Name

269 | getImplParams (Bind _ n (Pi _ _ Implicit _) sc)

270 |     = n :: getImplParams sc

271 | getImplParams _ = []

274 | elabInterface : {vars : _} ->

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

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

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

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

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

280 |                 FC -> WithDefault Visibility Private ->

281 |                 Env Term vars -> NestedNames vars ->

282 |                 (constraints : List (Maybe Name, RawImp)) ->

283 |                 Name ->

284 |                 (params : List (Name, (RigCount, RawImp))) ->

285 |                 (dets : Maybe (List1 Name)) ->

286 |                 (conName : Maybe (WithDoc $ AddFC Name)) ->

287 |                 List ImpDecl ->

288 |                 Core ()

289 | elabInterface {vars} ifc def_vis env nest constraints iname params dets mcon body

290 |     = do fullIName <- getFullName iname

291 |          ns_iname <- inCurrentNS fullIName

292 |          let conName_in = maybe (mkCon vfc fullIName) val mcon

293 |          -- Machine generated names need to be qualified when looking them up

294 |          conName <- inCurrentNS conName_in

295 |          whenJust (get "doc" <$> mcon) (addDocString conName)

296 |          let meth_sigs = mapMaybe getSig body

297 |          let meth_decls = meth_sigs

298 |          let meth_names = map (val . name) meth_decls

299 |          let defaults = mapMaybe getDefault body

301 |          elabAsData conName meth_names meth_sigs

302 |          elabConstraintHints conName meth_names

303 |          elabMethods conName meth_names meth_sigs

304 |          ds <- traverse (elabDefault meth_decls) defaults

306 |          ns_meths <- traverse (\mt => do n <- traverse inCurrentNS mt.name

307 |                                          pure ({ name := n } mt)) meth_decls

308 |          defs <- get Ctxt

309 |          Just ty <- lookupTyExact ns_iname (gamma defs)

310 |               | Nothing => undefinedName ifc iname

311 |          let implParams = getImplParams ty

313 |          updateIfaceSyn ns_iname conName

314 |                         implParams paramNames (map snd constraints)

315 |                         ns_meths ds

316 |   where

317 |     vfc : FC

318 |     vfc = virtualiseFC ifc

320 |     paramNames : List Name

321 |     paramNames = map fst params

323 |     nameConstraints : List (Maybe Name, RawImp) -> Core (List (Name, RawImp))

324 |     nameConstraints [] = pure []

325 |     nameConstraints ((_, ty) :: rest)

326 |         = pure $ (!(genVarName "constraint"), ty) :: !(nameConstraints rest)

328 |     -- Elaborate the data declaration part of the interface

329 |     elabAsData : (conName : Name) -> List Name ->

330 |                  List Signature ->

331 |                  Core ()

332 |     elabAsData conName meth_names meth_sigs

333 |         = do -- set up the implicit arguments correctly in the method

334 |              -- signatures and constraint hints

335 |              meths <- traverse (\ meth => getMethDecl env nest params meth_names

336 |                                           (meth.count, meth.name.val, meth.type))

337 |                                 meth_sigs

338 |              log "elab.interface" 5 $ "Method declarations: " ++ show meths

340 |              consts <- traverse (getMethDecl env nest params meth_names . (top,)) constraints

341 |              log "elab.interface" 5 $ "Constraints: " ++ show consts

343 |              dt <- mkIfaceData vfc def_vis env consts iname conName params

344 |                                   dets meths

345 |              log "elab.interface" 10 $ "Methods: " ++ show meths

346 |              log "elab.interface" 5 $ "Making interface data type " ++ show dt

347 |              ignore $ processDecls nest env [dt]

349 |     elabMethods : (conName : Name) -> List Name -> List Signature -> Core ()

350 |     elabMethods conName methNames methSigs

351 |         = do bindNames <- for methNames $ genVarName . nameRoot

352 |              -- Methods have same visibility as data declaration

353 |              fnsm <- traverse (getMethToplevel env (collapseDefault def_vis)

354 |                                                iname conName

355 |                                                methNames

356 |                                                bindNames

357 |                                                params)

358 |                               (zip bindNames methSigs)

359 |              let fns = concat fnsm

360 |              log "elab.interface" 5 $ "Top level methods: " ++ show fns

361 |              traverse_ (processDecl [] nest env) fns

362 |              traverse_ (\n => do mn <- inCurrentNS n

363 |                                  setFlag vfc mn Inline

364 |                                  setFlag vfc mn TCInline

365 |                                  setFlag vfc mn Overloadable) methNames

367 |     -- Check that a default definition is correct. We just discard it here once

368 |     -- we know it's okay, since we'll need to re-elaborate it for each

369 |     -- instance, to specialise it

370 |     elabDefault : List Signature ->

371 |                   (FC, List FnOpt, Name, List ImpClause) ->

372 |                   Core (Name, List ImpClause)

373 |     elabDefault tydecls (dfc, opts, n, cs)

374 |         = do -- orig <- branch

376 |              let dn_in = MN ("Default implementation of " ++ show n) 0

377 |              dn <- inCurrentNS dn_in

379 |              (rig, dty) <-

380 |                        case findBy (\ d => d <$ guard (n == d.name.val)) tydecls of

381 |                           Just d => pure (d.count, d.type)

382 |                           Nothing => throw (GenericMsg dfc ("No method named " ++ show n ++ " in interface " ++ show iname))

384 |              let ity = apply (IVar vdfc iname) (map (IVar vdfc) paramNames)

386 |              -- Substitute the method names with their top level function

387 |              -- name, so they don't get implicitly bound in the name

388 |              methNameMap <- traverse (\d =>

389 |                                 do let n = d.name.val

390 |                                    cn <- inCurrentNS n

391 |                                    pure (n, applyParams (IVar vdfc cn) paramNames))

392 |                                tydecls

393 |              let dty = bindPs params      -- bind parameters

394 |                      $ bindIFace vdfc ity -- bind interface (?!)

395 |                      $ substNames (toList vars) methNameMap dty

397 |              dty_imp <- bindTypeNames dfc [] (map (val . name) tydecls ++ toList vars) dty

398 |              log "elab.interface.default" 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp

400 |              let dtydecl = IClaim $ MkFCVal vdfc

401 |                                   $ MkIClaimData rig (collapseDefault def_vis) []

402 |                                   $ Mk [EmptyFC, NoFC dn] dty_imp

404 |              processDecl [] nest env dtydecl

406 |              cs' <- traverse (changeName dn) cs

407 |              log "elab.interface.default" 5 $ "Default method body " ++ show cs'

409 |              processDecl [] nest env (IDef vdfc dn cs')

410 |              -- Reset the original context, we don't need to keep the definition

411 |              -- Actually we do for the metadata and name map!

413 |              pure (n, cs)

414 |       where

415 |         vdfc : FC

416 |         vdfc = virtualiseFC dfc

418 |         -- Bind the type parameters given explicitly - there might be information

419 |         -- in there that we can't infer after all

420 |         bindPs : List (Name, (RigCount, RawImp)) -> RawImp -> RawImp

421 |         bindPs [] ty = ty

422 |         bindPs ((n, (rig, pty)) :: ps) ty

423 |           = IPi (getFC pty) rig Implicit (Just n) pty (bindPs ps ty)

425 |         applyParams : RawImp -> List Name -> RawImp

426 |         applyParams tm [] = tm

427 |         applyParams tm (n@(UN (Basic _)) :: ns)

428 |             = applyParams (INamedApp vdfc tm n (IBindVar vdfc n)) ns

429 |         applyParams tm (_ :: ns) = applyParams tm ns

431 |         changeNameTerm : Name -> RawImp -> Core RawImp

432 |         changeNameTerm dn (IVar fc n')

433 |             = do if n /= n' then pure (IVar fc n') else do

434 |                  log "ide-mode.highlight" 7 $

435 |                    "elabDefault is trying to add Function: " ++ show n ++ " (" ++ show fc ++")"

436 |                  whenJust (isConcreteFC fc) $ \nfc => do

437 |                    log "ide-mode.highlight" 7 $ "elabDefault is adding Function: " ++ show n

438 |                    addSemanticDecorations [(nfc, Function, Just n)]

439 |                  pure (IVar fc dn)

440 |         changeNameTerm dn (IApp fc f arg)

441 |             = IApp fc <$> changeNameTerm dn f <*> pure arg

442 |         changeNameTerm dn (IAutoApp fc f arg)

443 |             = IAutoApp fc <$> changeNameTerm dn f <*> pure arg

444 |         changeNameTerm dn (INamedApp fc f x arg)

445 |             = INamedApp fc <$> changeNameTerm dn f <*> pure x <*> pure arg

446 |         changeNameTerm dn tm = pure tm

448 |         changeName : Name -> ImpClause -> Core ImpClause

449 |         changeName dn (PatClause fc lhs rhs)

450 |             = PatClause fc <$> changeNameTerm dn lhs <*> pure rhs

451 |         changeName dn (WithClause fc lhs rig wval prf flags cs)

452 |             = WithClause fc

453 |                  <$> changeNameTerm dn lhs

454 |                  <*> pure rig

455 |                  <*> pure wval

456 |                  <*> pure prf

457 |                  <*> pure flags

458 |                  <*> traverse (changeName dn) cs

459 |         changeName dn (ImpossibleClause fc lhs)

460 |             = ImpossibleClause fc <$> changeNameTerm dn lhs

462 |     elabConstraintHints : (conName : Name) -> List Name ->

463 |                           Core ()

464 |     elabConstraintHints conName meth_names

465 |         = do nconstraints <- nameConstraints constraints

466 |              chints <- traverse (getConstraintHint vfc env (collapseDefault def_vis)

467 |                                                  iname conName

468 |                                                  (map fst nconstraints)

469 |                                                  meth_names

470 |                                                  params) nconstraints

471 |              log "elab.interface" 5 $ "Constraint hints from " ++ show constraints ++ ": " ++ show chints

472 |              List.traverse_ (processDecl [] nest env) (concatMap snd chints)

473 |              traverse_ (\n => do mn <- inCurrentNS n

474 |                                  setFlag vfc mn TCInline) (map fst chints)