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

git.iko.soy/Idris-dev

on master help sign in

Added 'parameters' blocks

72c0156Edwin Brady14 years ago

CHANGELOG+6

compare with master

unifiedsplit

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

1New in 0.9.5:

2-------------

4+User visible changes:

6+* Added 'parameters' blocks

7+* Allow local data definitions in where blocks

4Internal changes:

9Internal changes:

6* Several improvements and fixes to unification

11* Several improvements and fixes to unification

12+* Added collapsing optimisation and more aggressive erasure

8New in 0.9.4:

14New in 0.9.4:

9-------------

15-------------

src/Idris/AbsSyntax.hs+42−6

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

407existsCon = UN "Ex_intro"

408

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

410−piBind [] t = t

410+piBind = piBindp expl

411+

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

413+piBindp p [] t = t

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

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

412

415

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

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

414tcname (NS n _) = tcname n

417tcname (NS n _) = tcname n

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

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

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

456

459

457 en (PQuote (Var n))

460 en (PQuote (Var n))

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

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

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

462 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))

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

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

462 en (PRef fc n)

465 en (PRef fc n)

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

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

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

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

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

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

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

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

467 en t = t

470 en t = t

468

471

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+

469expandParamsD :: IState ->

478expandParamsD :: IState ->

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

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

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

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

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

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

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

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

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

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

507 | 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)

500expandParamsD ist dec ps ns d = d

534expandParamsD ist dec ps ns d = d

501

535

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

537+

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

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

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

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

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

540-- * 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

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

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

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

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

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

622+

620

623

621showCImp :: Bool -> PClause -> String

624showCImp :: Bool -> PClause -> String

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

625showCImp 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

907 [fs] -> fs

908 [] -> []

909 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

911 where

915 where

912 pinfo = let ds = concatMap declared ps

916 pinfo = let ds = concatMap declared ps

913 newps = params info ++ ns

917 newps = params info ++ ns

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

915 newb = addAlist dsParams (inblock info) in

919 newb = addAlist dsParams (inblock info) in

916 info { params = newps,

920 info { params = newps,

917 inblock = newb }

921 inblock = newb }

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

923+

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

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

919 where

925 where

920 ninfo = case namespace info of

926 ninfo = case namespace info of

src/Idris/Parser.hs+4−4

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

430

431pParams :: SyntaxInfo -> IParser [PDecl]

432pParams syn =

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

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

434− lchar '{'

434+ openBlock

435 let pvars = syn_params syn

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

437− lchar '}'

437+ closeBlock

438 fc <- pfc

439 return [PParams fc ns (concat ds)]

440

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

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

1338pWhereblock n syn

1339 = do reserved "where"; openBlock

1340− ds <- many1 $ pFunDecl syn

1340+ ds <- many1 $ pDecl syn

1341 let dns = concatMap (concatMap declared) ds

1342 closeBlock

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