72c0156 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added 'parameters' blocks

Allows abstracting over parameters across a block of functions and data definitions. Effect is to add those parameters to *every* function, type and data constructor. Inside the block, no need to pass those parameters, outside they must be made explicit. Interesting side effect: local data definitions now allowed in where blocks. class and instance declarations are also allowed in where blocks, but visibility is global and no parameters are added.

commit72c01563a8c12c5b74dfbfabafa83248d715f41e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 22 Oct 2012, 00:35 (14 years ago) parentfb2b17d

5 files changed+62−11

compare with master

unifiedsplit

CHANGELOG+6 src/Idris/AbsSyntax.hs+42−6 src/Idris/AbsSyntaxTree.hs+3 src/Idris/ElabDecls.hs+7−1 src/Idris/Parser.hs+4−4

CHANGELOG+6

@@ -1,9 +1,15 @@

11New in 0.9.5:

22-------------

4+User visible changes:

6+* Added 'parameters' blocks

7+* Allow local data definitions in where blocks

49Internal changes:

510

611* Several improvements and fixes to unification

12+* Added collapsing optimisation and more aggressive erasure

713

814New in 0.9.4:

915-------------

src/Idris/AbsSyntax.hs+42−6

@@ -407,8 +407,11 @@ sigmaTy = UN "Exists"

407407existsCon = UN "Ex_intro"

408408

409409piBind :: [(Name, PTerm)] -> PTerm -> PTerm

410−piBind [] t = t

411−piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)

410+piBind = piBindp expl

411+

412+piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm

413+piBindp p [] t = t

414+piBindp p ((n, ty):ns) t = PPi p n ty (piBind ns t)

412415

413416tcname (UN ('@':_)) = True

414417tcname (NS n _) = tcname n

@@ -455,17 +458,23 @@ expandParams dec ps ns tm = en tm

455458 en (PTactics ts) = PTactics (map (fmap en) ts)

456459

457460 en (PQuote (Var n))

458− | n `elem` ns = PQuote (Var (dec n))

461+ | n `nselem` ns = PQuote (Var (dec n))

459462 en (PApp fc (PRef fc' n) as)

460− | n `elem` ns = PApp fc (PRef fc' (dec n))

463+ | n `nselem` ns = PApp fc (PRef fc' (dec n))

461464 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))

462465 en (PRef fc n)

463− | n `elem` ns = PApp fc (PRef fc (dec n))

466+ | n `nselem` ns = PApp fc (PRef fc (dec n))

464467 (map (pexp . (PRef fc)) (map fst ps))

465468 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

466469 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

467470 en t = t

468471

472+ nselem x [] = False

473+ nselem x (y : xs) | nseq x y = True

474+ | otherwise = nselem x xs

475+

476+ nseq x y = nsroot x == nsroot y

477+

469478expandParamsD :: IState ->

470479 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

471480expandParamsD ist dec ps ns (PTy syn fc o n ty)

@@ -496,9 +505,36 @@ expandParamsD ist dec ps ns (PClauses fc opts n cs)

496505 updateps yn nm (((a, t), i):as)

497506 | (a `elem` nm) == yn = (a, t) : updateps yn nm as

498507 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as

499−

508+expandParamsD ist dec ps ns (PData syn fc pd) = PData syn fc (expandPData pd)

509+ where

510+ -- just do the type decl, leave constructors alone (parameters will be

511+ -- added implicitly)

512+ expandPData (PDatadecl n ty cons)

513+ = if n `elem` ns

514+ then PDatadecl (dec n) (piBind ps (expandParams dec ps ns ty)) (map econ cons)

515+ else PDatadecl n (expandParams dec ps ns ty) (map econ cons)

516+ econ (n, t, fc) = (dec n, piBindp expl ps (expandParams dec ps ns t), fc)

517+expandParamsD ist dec ps ns (PParams f params pds)

518+ = PParams f (map (mapsnd (expandParams dec ps ns)) params)

519+ (map (expandParamsD ist dec ps ns) pds)

520+expandParamsD ist dec ps ns (PClass info f cs n params decls)

521+ = PClass info f

522+ (map (expandParams dec ps ns) cs)

523+ n

524+ (map (mapsnd (expandParams dec ps ns)) params)

525+ (map (expandParamsD ist dec ps ns) decls)

526+expandParamsD ist dec ps ns (PInstance info f cs n params ty cn decls)

527+ = PInstance info f

528+ (map (expandParams dec ps ns) cs)

529+ n

530+ (map (expandParams dec ps ns) params)

531+ (expandParams dec ps ns ty)

532+ cn

533+ (map (expandParamsD ist dec ps ns) decls)

500534expandParamsD ist dec ps ns d = d

501535

536+mapsnd f (x, t) = (x, f t)

537+

502538-- Calculate a priority for a type, for deciding elaboration order

503539-- * if it's just a type variable or concrete type, do it early (0)

504540-- * if there's only type variables and injective constructors, do it next (1)

src/Idris/AbsSyntaxTree.hs+3

@@ -617,6 +617,9 @@ showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

617617showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty

618618showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)

619619showDeclImp _ (PData _ _ d) = show d

620+showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++

621+ showSep "\n" (map show ps)

622+

620623

621624showCImp :: Bool -> PClause -> String

622625showCImp impl (PClause _ n l ws r w)

src/Idris/ElabDecls.hs+7−1

@@ -907,7 +907,11 @@ elabDecl' info d@(PClauses f o n ps) = do iLOG $ "Elaborating clause " ++ show n

907907 [fs] -> fs

908908 [] -> []

909909 elabClauses info f (o ++ o') n ps

910−elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

910+elabDecl' info (PParams f ns ps)

911+ = do i <- get

912+ iLOG $ "Expanding params block with " ++ show (concatMap declared ps)

913+ let nblock = pblock i

914+ mapM_ (elabDecl' info) nblock

911915 where

912916 pinfo = let ds = concatMap declared ps

913917 newps = params info ++ ns

@@ -915,6 +919,8 @@ elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

915919 newb = addAlist dsParams (inblock info) in

916920 info { params = newps,

917921 inblock = newb }

922+ pblock i = map (expandParamsD i id ns (concatMap declared ps)) ps

923+

918924elabDecl' info (PNamespace n ps) = mapM_ (elabDecl' ninfo) ps

919925 where

920926 ninfo = case namespace info of

src/Idris/Parser.hs+4−4

@@ -430,11 +430,11 @@ pUsing syn =

430430

431431pParams :: SyntaxInfo -> IParser [PDecl]

432432pParams syn =

433− do reserved "params"; lchar '('; ns <- tyDeclList syn; lchar ')'

434− lchar '{'

433+ do reserved "parameters"; lchar '('; ns <- tyDeclList syn; lchar ')'

434+ openBlock

435435 let pvars = syn_params syn

436436 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })

437− lchar '}'

437+ closeBlock

438438 fc <- pfc

439439 return [PParams fc ns (concat ds)]

440440

@@ -1337,7 +1337,7 @@ pWExpr syn = do lchar '|'

13371337pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])

13381338pWhereblock n syn

13391339 = do reserved "where"; openBlock

1340− ds <- many1 $ pFunDecl syn

1340+ ds <- many1 $ pDecl syn

13411341 let dns = concatMap (concatMap declared) ds

13421342 closeBlock

13431343 return (concat ds, map (\x -> (x, decoration syn x)) dns)