f2c3b8d · Idris-dev · git.iko.soy

175elabRecordFunctions info rsyn fc tyn params fields dconName target

176 = do logElab 1 $ "Elaborating helper functions for record " ++ show tyn

177

178− logElab 1 $ "Fields: " ++ show fieldNames

178+ logElab 3 $ "Fields: " ++ show fieldNames

179− logElab 1 $ "Params: " ++ show paramNames

179+ logElab 3 $ "Params: " ++ show paramNames

180 -- The elaborated constructor type for the data declaration

181 i <- getIState

182 ttConsTy <-

186

187 -- The arguments to the constructor

188 let constructorArgs = getArgTys ttConsTy

189− logElab 1 $ "Cons args: " ++ show constructorArgs

189+ logElab 3 $ "Cons args: " ++ show constructorArgs

190− logElab 1 $ "Free fields: " ++ show (filter (not . isFieldOrParam') constructorArgs)

190+ logElab 3 $ "Free fields: " ++ show (filter (not . isFieldOrParam') constructorArgs)

191 -- If elaborating the constructor has resulted in some new implicit fields we make projection functions for them.

192 let freeFieldsForElab = map (freeField i) (filter (not . isFieldOrParam') constructorArgs)

193

201 -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.

202 let projectors = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]

203 -- Build and elaborate projection functions

204− elabProj dconName projectors

204+ elabProj dconName paramNames projectors

205

206− logElab 1 $ "Dependencies: " ++ show fieldDependencies

206+ logElab 3 $ "Dependencies: " ++ show fieldDependencies

207

208− logElab 1 $ "Depended on: " ++ show dependedOn

208+ logElab 3 $ "Depended on: " ++ show dependedOn

209

210 -- All things we need to elaborate update functions for, together with a number denoting their position in the constructor.

211 let updaters = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (paramsForElab ++ userFieldsForElab) [0..]]

212 -- Build and elaborate update functions

213− elabUp dconName updaters

213+ elabUp dconName paramNames updaters

214 where

215 -- | Creates a PArg from a plicity and a name where the term is a Placeholder.

216 placeholderArg :: Plicity -> Name -> PArg

270 paramName n = n

271

272 -- | Elaborate the projection functions.

273− elabProj :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

273+ elabProj :: Name -> [Name] -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

274+ elabProj cn paramnames fs

274− elabProj cn fs = let phArgs = map (uncurry placeholderArg) [(p, n) | (n, _, p, _, _, _) <- fs]

275+ = let phArgs = map (uncurry placeholderArg) [(p, n) | (n, _, p, _, _, _) <- fs]

275 elab = \(n, n', p, t, doc, i) ->

276 elab = \(n, n', p, t, doc, i) ->

276 -- Use projections in types

277 -- Use projections in types

277 do let t' = projectInType [(m, m') | (m, m', _, _, _, _) <- fs

278 do let t' = projectInType [(m, m') | (m, m', _, _, _, _) <- fs

278 -- Parameters are already in scope, so just use them

279 -- Parameters are already in scope, so just use them

279 , not (m `elem` paramNames)] t

280 , not (m `elem` paramNames)] t

280− elabProjection info n n' p t' doc rsyn fc target cn phArgs fieldNames i

281+ elabProjection info n paramnames n' p t' doc rsyn fc target cn phArgs fieldNames i

281 in mapM_ elab fs

282 in mapM_ elab fs

282

283

283 -- | Elaborate the update functions.

284 -- | Elaborate the update functions.

284− elabUp :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

285+ elabUp :: Name -> [Name] -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

286+ elabUp cn paramnames fs

285− elabUp cn fs = let args = map (uncurry asPRefArg) [(p, n) | (n, _, p, _, _, _) <- fs]

287+ = let args = map (uncurry asPRefArg) [(p, n) | (n, _, p, _, _, _) <- fs]

286− elab = \(n, n', p, t, doc, i) -> elabUpdate info n n' p t doc rsyn fc target cn args fieldNames i (optionalSetter n)

288+ elab = \(n, n', p, t, doc, i) -> elabUpdate info n paramnames n' p t doc rsyn fc target cn args fieldNames i (optionalSetter n)

287 in mapM_ elab fs

289 in mapM_ elab fs

288

290

289 -- | Decides whether a setter should be generated for a field or not.

291 -- | Decides whether a setter should be generated for a field or not.

313-- | Creates and elaborates a projection function.

315-- | Creates and elaborates a projection function.

314elabProjection :: ElabInfo

316elabProjection :: ElabInfo

315 -> Name -- ^ Name of the argument in the constructor

317 -> Name -- ^ Name of the argument in the constructor

318+ -> [Name] -- ^ Parameter names

316 -> Name -- ^ Projection Name

319 -> Name -- ^ Projection Name

317 -> Plicity -- ^ Projection Plicity

320 -> Plicity -- ^ Projection Plicity

318 -> PTerm -- ^ Projection Type

321 -> PTerm -- ^ Projection Type

324 -> [Name] -- ^ All Field Names

327 -> [Name] -- ^ All Field Names

325 -> Int -- ^ Argument Index

328 -> Int -- ^ Argument Index

326 -> Idris ()

329 -> Idris ()

327−elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs fnames index

330+elabProjection info cname paramnames pname plicity projTy pdoc psyn fc targetTy cn phArgs fnames index

328 = do logElab 1 $ "Generating Projection for " ++ show pname

331 = do logElab 1 $ "Generating Projection for " ++ show pname

329

332

330 let ty = generateTy

333 let ty = generateTy

343 -- | The type of the projection function.

346 -- | The type of the projection function.

344 generateTy :: PDecl

347 generateTy :: PDecl

345 generateTy = PTy pdoc [] psyn fc [] pname NoFC $

348 generateTy = PTy pdoc [] psyn fc [] pname NoFC $

349+ bindParams paramnames $

346− PPi expl recName NoFC targetTy projTy

350+ PPi expl recName NoFC targetTy projTy

351+

352+ bindParams [] t = t

353+ bindParams (n : ns) ty = PPi impl n NoFC Placeholder (bindParams ns ty)

347

354

348 -- | The left hand side of the projection function.

355 -- | The left hand side of the projection function.

349 generateLhs :: PTerm

356 generateLhs :: PTerm

370-- If 'optional' is true, we will not fail if we can't elaborate the update function.

377-- If 'optional' is true, we will not fail if we can't elaborate the update function.

371elabUpdate :: ElabInfo

378elabUpdate :: ElabInfo

372 -> Name -- ^ Name of the argument in the constructor

379 -> Name -- ^ Name of the argument in the constructor

380+ -> [Name] -- ^ Parameter names

373 -> Name -- ^ Field Name

381 -> Name -- ^ Field Name

374 -> Plicity -- ^ Field Plicity

382 -> Plicity -- ^ Field Plicity

375 -> PTerm -- ^ Field Type

383 -> PTerm -- ^ Field Type

382 -> Int -- ^ Argument Index

390 -> Int -- ^ Argument Index

383 -> Bool -- ^ Optional

391 -> Bool -- ^ Optional

384 -> Idris ()

392 -> Idris ()

385−elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i optional

393+elabUpdate info cname paramnames pname plicity pty pdoc psyn fc sty cn args fnames i optional

386 = do logElab 1 $ "Generating Update for " ++ show pname

394 = do logElab 1 $ "Generating Update for " ++ show pname

387

395

388 let ty = generateTy

396 let ty = generateTy

406 -- | The type of the update function.

414 -- | The type of the update function.

407 generateTy :: PDecl

415 generateTy :: PDecl

408 generateTy = PTy pdoc [] psyn fc [] set_pname NoFC $

416 generateTy = PTy pdoc [] psyn fc [] set_pname NoFC $

417+ bindParams paramnames $

409− PPi expl (nsroot pname) NoFC pty $

418+ PPi expl (nsroot pname) NoFC pty $

410− PPi expl recName NoFC sty (substInput sty)

419+ PPi expl recName NoFC sty (substInput sty)

411 where substInput = substMatches [(cname, PRef fc [] (nsroot pname))]

420 where substInput = substMatches [(cname, PRef fc [] (nsroot pname))]

412

421

422+ bindParams [] t = t

423+ bindParams (n : ns) ty = PPi impl n NoFC Placeholder (bindParams ns ty)

424+

413 -- | The "_set" name.

425 -- | The "_set" name.

414 set_pname :: Name

426 set_pname :: Name

415 set_pname = set_name pname

427 set_pname = set_name pname