0 | module TTImp.ProcessRecord

  2 | import Core.Env

  3 | import Core.Metadata

  4 | import Core.UnifyState

  6 | import Idris.REPL.Opts

  7 | import Idris.Syntax

  9 | import TTImp.BindImplicits

 10 | import TTImp.Elab.Check

 11 | import TTImp.TTImp

 12 | import TTImp.TTImp.Functor

 13 | import TTImp.TTImp.Traversals

 14 | import TTImp.Unelab

 15 | import TTImp.Utils

 17 | import Libraries.Data.WithDefault

 19 | import Data.String

 21 | %default covering

 26 | killHole : RawImp -> RawImp

 27 | killHole (IHole fc str) = Implicit fc True

 28 | killHole t = t

 31 | projVis : Visibility -> Visibility

 32 | projVis Public = Public

 33 | projVis _ = Private

 35 | elabRecord : {vars : _} ->

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

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

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

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

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

 41 |              List ElabOpt -> FC -> Env Term vars ->

 42 |              NestedNames vars -> Maybe String ->

 43 |              WithDefault Visibility Private ->

 44 |              Maybe TotalReq ->

 45 |              (tyName : Name) ->

 46 |              (params : List ImpParameter) ->

 47 |              (opts : List DataOpt) ->

 48 |              (conName : Name) ->

 49 |              List IField ->

 50 |              Core ()

 51 | elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conName_in fields

 52 |     = do tn <- inCurrentNS tn_in

 53 |          conName <- inCurrentNS conName_in

 54 |          params <- preElabAsData tn

 55 |          log "declare.record.parameters" 100 $

 56 |            unlines ("New list of parameters:" :: map (("  " ++) . displayParam) params)

 57 |          elabAsData tn conName params

 58 |          defs <- get Ctxt

 59 |          Just conty <- lookupTyExact conName (gamma defs)

 60 |              | Nothing => throw (InternalError ("Adding " ++ show tn ++ "failed"))

 62 |          -- #1404

 63 |          whenJust mbtot $ \tot => do

 64 |            log "declare.record" 5 $ "setting totality flag for " ++ show tn

 65 |            setFlag fc tn (SetTotal tot)

 67 |          -- Go into new namespace, if there is one, for getters

 68 |          case newns of

 69 |               Nothing => elabGetters tn conName params 0 [] Env.empty conty

 70 |               Just ns =>

 71 |                    do let cns = currentNS defs

 72 |                       let nns = nestedNS defs

 73 |                       extendNS (mkNamespace ns)

 74 |                       newns <- getNS

 75 |                       elabGetters tn conName params 0 [] Env.empty conty

 76 |                       -- Record that the current namespace is allowed to look

 77 |                       -- at private names in the nested namespace

 78 |                       update Ctxt { currentNS := cns,

 79 |                                     nestedNS := newns :: nns }

 81 |   where

 83 |     displayParam : ImpParameter -> String

 84 |     displayParam binder

 85 |       = withPiInfo binder.val.info "\{showCount binder.rig}\{show binder.name.val} : \{show binder.val.boundType}"

 87 |     paramTelescope : List ImpParameter -> List (AddFC $ WithRig $ WithMName (PiBindData RawImp))

 88 |     paramTelescope params = map jname params

 89 |       where

 90 |         jname : ImpParameter

 91 |              -> (AddFC $ WithRig $ WithMName (PiBindData RawImp))

 92 |         -- Record type parameters are implicit in the constructor

 93 |         -- and projections

 94 |         jname binder = Mk [EmptyFC, erased, Just binder.name] $ {info := Implicit} binder.val

 96 |     fname : IField -> Name

 97 |     fname field = field.name.val

 99 |     farg : IField -> AddFC (WithRig $ WithMName (PiBindData RawImp))

100 |     farg field = Mk [virtualiseFC field.fc, field.rig, Just field.name] field.val

102 |     mkTy : List (AddFC $ WithRig $ WithMName (PiBindData RawImp)) -> RawImp -> RawImp

103 |     mkTy [] ret = ret

104 |     mkTy (bind :: args) ret

105 |         = IPi bind.fc bind.rig bind.val.info (map val bind.mName) bind.val.boundType (mkTy args ret)

107 |     recTy : (tn : Name) -> -- fully qualified name of the record type

108 |             (params : List ImpParameter) -> -- list of all the parameters

109 |             RawImp

110 |     recTy tn params = apply (IVar (virtualiseFC fc) tn) (map (\binder => (binder.name.val, IVar EmptyFC binder.name.val, binder.val.info)) params)

111 |       where

112 |         ||| Apply argument to list of explicit or implicit named arguments

113 |         apply : RawImp -> List (Name, RawImp, PiInfo RawImp) -> RawImp

114 |         apply f [] = f

115 |         apply f ((n, arg, Explicit) :: xs) = apply (IApp         (getFC f) f          arg) xs

116 |         apply f ((n, arg, _       ) :: xs) = apply (INamedApp (getFC f) f n arg) xs

118 |     paramNames : List ImpParameter -> List Name

119 |     paramNames params = map (.name.val) params

121 |     mkDataTy : FC -> List ImpParameter -> RawImp

122 |     mkDataTy fc [] = IType fc

123 |     mkDataTy fc (binder :: ps) = IPi fc binder.rig binder.val.info (Just binder.name.val) binder.val.boundType (mkDataTy fc ps)

125 |     nestDrop : Core (List (Name, Nat))

126 |     nestDrop

127 |       = do let assoc = map (\ (n, (_, ns, _)) => (n, length ns)) (names nest)

128 |            traverse (\ (n, ns) => pure (!(toFullNames n), ns)) assoc

130 |     -- Parameters may need implicit names to be bound e.g.

131 |     --   record HasLength (xs : List a) (n : Nat)

132 |     -- needs to be turned into

133 |     --   record HasLength {0 a : Type} (xs : List a) (n : Nat)

134 |     -- otherwise `a` will be bound as a field rather than a parameter!

135 |     -- We pre-elaborate the datatype, thus resolving all the missing bindings,

136 |     -- and return the new list of parameters

137 |     preElabAsData : (tn : Name) -> -- fully qualified name of the record type

138 |                     Core (List ImpParameter) -- New telescope of parameters, including missing bindings

139 |     preElabAsData tn

140 |         = do let fc = virtualiseFC fc

141 |              let dataTy = IBindHere fc (PI erased) !(bindTypeNames fc [] (toList vars) (mkDataTy fc params0))

142 |              defs <- get Ctxt

143 |              -- Create a forward declaration if none exists

144 |              when (isNothing !(lookupTyExact tn (gamma defs))) $ do

145 |                let dt = MkImpLater fc tn dataTy

146 |                log "declare.record" 10 $ "Pre-declare record data type: \{show dt}"

147 |                processDecl [] nest env (IData fc def_vis mbtot dt)

148 |              defs <- get Ctxt

149 |              Just ty <- lookupTyExact tn (gamma defs)

150 |                | Nothing => throw (InternalError "Missing data type \{show tn}, despite having just declared it!")

151 |              log "declare.record" 20 "Obtained type: \{show ty}"

152 |              (_ ** (tyenv, ty)) <- dropLeadingPis vars ty Env.empty

153 |              ty <- unelabNest (NoSugar True) !nestDrop tyenv ty

154 |              log "declare.record.parameters" 30 "Unelaborated type: \{show ty}"

155 |              params <- getParameters [<] ty

156 |              addMissingNames ([<] <>< map (\x => x.name) params0 ) params []

158 |       where

160 |         -- We have elaborated the record type in a context (e.g. variables bound on

161 |         -- a LHS, or inside a `parameters` block) and so we need to start by dropping

162 |         -- these local variables from the fully elaborated record's type

163 |         -- We'll use the `env` thus obtained to unelab the remaining scope

164 |         dropLeadingPis : {vs : _} -> (vars : Scope) -> Term vs -> Env Term vs ->

165 |                          Core (vars' : Scope ** (Env Term vars', Term vars'))

166 |         dropLeadingPis [] ty env

167 |           = do unless (null vars) $

168 |                  logC "declare.record.parameters" 60 $ pure $ unlines

169 |                    [ "We elaborated \{show tn} in a non-empty local context."

170 |                    , "  Dropped: \{show vars}"

171 |                    , "  Remaining type: \{show !(toFullNames ty)}"

172 |                    ]

173 |                pure (_ ** (env, ty))

174 |         dropLeadingPis (var :: vars) (Bind fc n b@(Pi {}) ty) env

175 |           = dropLeadingPis vars ty (b :: env)

176 |         dropLeadingPis _ ty _ = throw (InternalError "Malformed record type \{show ty}")

178 |         getParameters :

179 |           SnocList (WithRig $ WithMName $ PiBindData RawImp) -> -- accumulator

180 |           RawImp' KindedName -> -- quoted type (some names may have disappeared)

181 |           Core (SnocList (WithRig $ WithMName $ PiBindData RawImp))

182 |         getParameters acc (IPi fc rig pinfo mnm argTy retTy)

183 |           = let clean = mapTTImp killHole . map fullName in

184 |             getParameters (acc :< (Mk [rig, map NoFC mnm] (MkPiBindData (map clean pinfo) (clean argTy)))) retTy

185 |         getParameters acc (IType _) = pure acc

186 |         getParameters acc ty = throw (InternalError "Malformed record type \{show ty}")

188 |         addMissingNames :

189 |           SnocList (WithFC Name) ->

190 |           SnocList (WithRig $ WithMName $ PiBindData RawImp) ->

191 |           List ImpParameter -> -- accumulator

192 |           Core (List ImpParameter)

193 |         addMissingNames (nms :< nm) (tele :< rest) acc

194 |           = addMissingNames nms tele (Mk [rest.rig, nm] rest.val :: acc)

195 |         addMissingNames [<] tele acc

196 |           = do tele <- flip Core.traverseSnocList tele $ \ rest =>

197 |                          case rest.mName of

198 |                            Nothing => throw (InternalError "Some names have disappeared?! \{show rest.val}")

199 |                            Just nm => pure (Mk [rest.rig, nm] rest.val) -- (nm, rest)

200 |                unless (null tele) $

201 |                  log "declare.record.parameters" 50 $

202 |                    unlines ( "Decided to bind the following extra parameters:"

203 |                            :: map (("  " ++) . displayParam) (tele <>> []))

204 |                pure (tele <>> acc)

206 |         addMissingNames nms [<] acc

207 |           = throw (InternalError "Some arguments have disappeared")

210 |     elabAsData : (tn : Name) -> -- fully qualified name of the record type

211 |                  (conName : Name) -> -- fully qualified name of the record type constructor

212 |                  (params : List ImpParameter) -> -- telescope of parameters

213 |                  Core ()

214 |     elabAsData tn cname params

215 |         = do let fc = virtualiseFC fc

216 |              let conty = mkTy (paramTelescope params) $

217 |                          mkTy (map farg fields) (recTy tn params)

218 |              let boundNames = paramNames params ++ map fname fields ++ (toList vars)

219 |              let con = Mk [virtualiseFC fc, NoFC cname]

220 |                        !(bindTypeNames fc [] boundNames conty)

221 |              let dt = MkImpData fc tn Nothing opts [con]

222 |              log "declare.record" 5 $ "Record data type " ++ show dt

223 |              processDecl [] nest env (IData fc def_vis mbtot dt)

225 |     countExp : Term vs -> Nat

226 |     countExp (Bind _ _ (Pi _ _ Explicit _) sc) = S (countExp sc)

227 |     countExp (Bind _ _ (Pi {}) sc) = countExp sc

228 |     countExp _ = 0

230 |     -- Generate getters from the elaborated record constructor type

231 |     --

232 |     -- WARNING: if you alter the names of the getters,

233 |     --          you probably will have to adjust TTImp.TTImp.definedInBlock.

234 |     --

235 |     elabGetters : {vs : _} ->

236 |                   (tn : Name) -> -- fully qualified name of the record type

237 |                   (conName : Name) -> -- fully qualified name of the record type constructor

238 |                   (params : List ImpParameter) -> -- Telescope of parameters

239 |                   (done : Nat) -> -- number of explicit fields processed

240 |                   List (Name, RawImp) -> -- names to update in types

241 |                     -- (for dependent records, where a field's type may depend

242 |                     -- on an earlier projection)

243 |                   Env Term vs -> Term vs ->

244 |                   Core ()

245 |     elabGetters tn con params done upds tyenv (Bind bfc n b@(Pi _ rc imp ty_chk) sc)

246 |         = let rig = if isErased rc then erased else top

247 |               isVis = projVis (collapseDefault def_vis)

248 |               paramNames = map (\x => x.name.val) params

249 |           in if (n `elem` paramNames) || (n `elem` vars)

250 |              then elabGetters tn con params

251 |                               (if imp == Explicit && not (n `elem` vars)

252 |                                   then S done else done)

253 |                               upds (b :: tyenv) sc

254 |              else

255 |                 do let fldNameStr = nameRoot n

256 |                    let unName = UN $ Basic fldNameStr

257 |                    rfNameNS <- inCurrentNS (UN $ Field fldNameStr)

258 |                    unNameNS <- inCurrentNS unName

260 |                    ty <- unelabNest (NoSugar False) !nestDrop tyenv ty_chk

261 |                    let ty' = substNames (toList vars) upds $ map rawName ty

262 |                    log "declare.record.field" 5 $ "Field type: " ++ show ty'

263 |                    let rname = MN "rec" 0

265 |                    -- Claim the projection type

266 |                    projTy <- bindTypeNames fc []

267 |                                  (paramNames ++ map fname fields ++ toList vars) $

268 |                                       mkTy (paramTelescope params) $

269 |                                       IPi bfc top Explicit (Just rname) (recTy tn params) ty'

270 |                    let fc' = virtualiseFC fc

271 |                    let mkProjClaim = \ nm =>

272 |                           let ty = Mk [fc', MkFCVal fc' nm] projTy

273 |                           in IClaim (MkFCVal bfc (MkIClaimData rig isVis [Inline] ty))

275 |                    log "declare.record.projection.claim" 5 $

276 |                       "Projection " ++ show rfNameNS ++ ": " ++ show projTy

277 |                    processDecl [] nest env (mkProjClaim rfNameNS)

279 |                    -- Define the LHS and RHS

280 |                    let lhs_exp

281 |                           = apply (IVar bfc con)

282 |                                     (replicate done (Implicit bfc True) ++

283 |                                        (if imp == Explicit

284 |                                            then [IBindVar fc' unName]

285 |                                            else []) ++

286 |                                     (replicate (countExp sc) (Implicit bfc True)))

287 |                    let lhs = IApp bfc (IVar bfc rfNameNS)

288 |                                 (if imp == Explicit

289 |                                     then lhs_exp

290 |                                     else INamedApp bfc lhs_exp unName

291 |                                              (IBindVar bfc unName))

292 |                    let rhs = IVar fc' unName

294 |                    -- EtaExpand implicits on both sides:

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

296 |                    -- See idris-lang/Idris2#3467

297 |                    (lhs, rhs) <- etaExpandImplicits fc' ty' lhs rhs

299 |                    log "declare.record.projection.clause" 5 $ "Projection " ++ show lhs ++ " = " ++ show rhs

300 |                    processDecl [] nest env

301 |                        (IDef bfc rfNameNS [PatClause bfc lhs rhs])

303 |                    -- Make prefix projection aliases if requested

304 |                    when !isPrefixRecordProjections $ do  -- beware: `!` is NOT boolean `not`!

305 |                      -- Claim the type.

306 |                      -- we just reuse `projTy` defined above

307 |                      log "declare.record.projection.prefix" 5 $

308 |                        "Prefix projection " ++ show unNameNS ++ " : " ++ show projTy

309 |                      processDecl [] nest env (mkProjClaim unNameNS)

311 |                      -- Define the LHS and RHS

312 |                      let lhs = IVar bfc unNameNS

313 |                      let rhs = IVar bfc rfNameNS

314 |                      log "declare.record.projection.prefix" 5 $

315 |                        "Prefix projection " ++ show lhs ++ " = " ++ show rhs

316 |                      processDecl [] nest env

317 |                          (IDef bfc unNameNS [PatClause bfc lhs rhs])

319 |                    -- Move on to the next getter.

320 |                    --

321 |                    -- In upds, we use unNameNS (as opposed to rfNameNS or both)

322 |                    -- because the field types will probably mention the UN versions of the projections;

323 |                    -- but only when prefix record projections are enabled, otherwise

324 |                    -- dependent records won't typecheck!

325 |                    --

326 |                    -- With the braching on this flag, this change of using `rfNamesNS` remains backward compatible

327 |                    -- (though the only difference I'm aware is in the output of the `:doc` command)

328 |                    prefix_flag <- isPrefixRecordProjections

329 |                    let upds' = if prefix_flag

330 |                          then (n, IApp bfc (IVar bfc unNameNS) (IVar bfc rname)) :: upds

331 |                          else (n, IApp bfc (IVar bfc rfNameNS) (IVar bfc rname)) :: upds

333 |                    elabGetters tn con params

334 |                                (if imp == Explicit

335 |                                    then S done else done)

336 |                                upds' (b :: tyenv) sc

338 |     elabGetters tn con _ done upds _ _ = pure ()

341 | processRecord : {vars : _} ->

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

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

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

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

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

347 |                 List ElabOpt -> NestedNames vars ->

348 |                 Env Term vars -> Maybe String ->

349 |                 WithDefault Visibility Private -> Maybe TotalReq ->

350 |                 ImpRecord -> Core ()

351 | processRecord eopts nest env newns def_vis mbtot rec@(MkWithData _ $ MkImpRecord header body)

352 |     = elabRecord eopts rec.fc env nest newns def_vis mbtot header.name.val header.val body.opts body.name.val body.val