1b6cc6a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix parameter block expansion

1b6cc6aEdwin Brady14 years ago

src/Idris/AbsSyntax.hs+21−17

compare with master

unifiedsplit

@@ -502,37 +502,40 @@ expandParams dec ps ns tm = en tm

502

503 nseq x y = nsroot x == nsroot y

504

505−expandParamsD :: IState ->

505+expandParamsD :: Bool -> -- True = RHS only

506+ IState ->

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

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

507−expandParamsD ist dec ps ns (PTy doc syn fc o n ty)

508+expandParamsD False ist dec ps ns (PTy doc syn fc o n ty)

508 = if n `elem` ns

509 = if n `elem` ns

509 then PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))

510 then PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))

510 else PTy doc syn fc o n (expandParams dec ps ns ty)

511 else PTy doc syn fc o n (expandParams dec ps ns ty)

511−expandParamsD ist dec ps ns (PClauses fc opts n cs)

512+expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

512 = let n' = if n `elem` ns then dec n else n in

513 = let n' = if n `elem` ns then dec n else n in

513 PClauses fc opts n' (map expandParamsC cs)

514 PClauses fc opts n' (map expandParamsC cs)

514 where

515 where

515 expandParamsC (PClause fc n lhs ws rhs ds)

516 expandParamsC (PClause fc n lhs ws rhs ds)

516 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])

517 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])

517 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])

518 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])

519+ lhs' = if rhsonly then lhs else (expandParams dec ps'' ns lhs)

518 n' = if n `elem` ns then dec n else n in

520 n' = if n `elem` ns then dec n else n in

519− PClause fc n' (expandParams dec ps'' ns lhs)

521+ PClause fc n' lhs'

520 (map (expandParams dec ps'' ns) ws)

522 (map (expandParams dec ps'' ns) ws)

521 (expandParams dec ps'' ns rhs)

523 (expandParams dec ps'' ns rhs)

522− (map (expandParamsD ist dec ps'' ns) ds)

524+ (map (expandParamsD True ist dec ps'' ns) ds)

523 expandParamsC (PWith fc n lhs ws wval ds)

525 expandParamsC (PWith fc n lhs ws wval ds)

524 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])

526 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])

525 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])

527 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])

528+ lhs' = if rhsonly then lhs else (expandParams dec ps'' ns lhs)

526 n' = if n `elem` ns then dec n else n in

529 n' = if n `elem` ns then dec n else n in

527− PWith fc n' (expandParams dec ps'' ns lhs)

530+ PWith fc n' lhs'

528 (map (expandParams dec ps'' ns) ws)

531 (map (expandParams dec ps'' ns) ws)

529 (expandParams dec ps'' ns wval)

532 (expandParams dec ps'' ns wval)

530− (map (expandParamsD ist dec ps'' ns) ds)

533+ (map (expandParamsD rhsonly ist dec ps'' ns) ds)

531 updateps yn nm [] = []

534 updateps yn nm [] = []

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

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

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

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

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

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

535−expandParamsD ist dec ps ns (PData doc syn fc co pd)

538+expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)

536 = PData doc syn fc co (expandPData pd)

539 = PData doc syn fc co (expandPData pd)

537 where

540 where

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

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

@@ -543,26 +546,27 @@ expandParamsD ist dec ps ns (PData doc syn fc co pd)

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

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

544 econ (doc, n, t, fc)

547 econ (doc, n, t, fc)

545 = (doc, dec n, piBindp expl ps (expandParams dec ps ns t), fc)

548 = (doc, dec n, piBindp expl ps (expandParams dec ps ns t), fc)

546−expandParamsD ist dec ps ns (PParams f params pds)

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

547− = PParams f (ps ++ map (mapsnd (expandParams dec ps ns)) params) pds

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

551+ (map (expandParamsD True ist dec ps ns) pds)

548-- (map (expandParamsD ist dec ps ns) pds)

552-- (map (expandParamsD ist dec ps ns) pds)

549−expandParamsD ist dec ps ns (PMutual f pds)

553+expandParamsD rhs ist dec ps ns (PMutual f pds)

550− = PMutual f (map (expandParamsD ist dec ps ns) pds)

554+ = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)

551−expandParamsD ist dec ps ns (PClass doc info f cs n params decls)

555+expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)

552 = PClass doc info f

556 = PClass doc info f

553 (map (expandParams dec ps ns) cs)

557 (map (expandParams dec ps ns) cs)

554 n

558 n

555 (map (mapsnd (expandParams dec ps ns)) params)

559 (map (mapsnd (expandParams dec ps ns)) params)

556− (map (expandParamsD ist dec ps ns) decls)

560+ (map (expandParamsD rhs ist dec ps ns) decls)

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

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

558 = PInstance info f

562 = PInstance info f

559 (map (expandParams dec ps ns) cs)

563 (map (expandParams dec ps ns) cs)

560 n

564 n

561 (map (expandParams dec ps ns) params)

565 (map (expandParams dec ps ns) params)

562 (expandParams dec ps ns ty)

566 (expandParams dec ps ns ty)

563 cn

567 cn

564− (map (expandParamsD ist dec ps ns) decls)

568+ (map (expandParamsD rhs ist dec ps ns) decls)

565−expandParamsD ist dec ps ns d = d

569+expandParamsD rhs ist dec ps ns d = d

566

570

567mapsnd f (x, t) = (x, f t)

571mapsnd f (x, t) = (x, f t)

568

572

src/Idris/ElabDecls.hs+7−5

@@ -45,9 +45,9 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

45 do checkUndefined fc n

46 ctxt <- getContext

47 i <- get

48+ logLvl 3 $ show n ++ " pre-type " ++ showImp True ty'

48 ty' <- implicit syn n ty'

49 ty' <- implicit syn n ty'

49 let ty = addImpl i ty'

50 let ty = addImpl i ty'

50− logLvl 3 $ show n ++ " pre-type " ++ showImp True ty'

51 logLvl 2 $ show n ++ " type " ++ showImp True ty

52 ((tyT, defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []

53 (erun fc (build i info False n ty))

@@ -470,7 +470,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

470 let winfo = pinfo (pvars ist lhs_tm) whereblock windex

471 let decls = concatMap declared whereblock

472 let newargs = pvars ist lhs_tm

473− let wb = map (expandParamsD ist decorate newargs decls) whereblock

473+ let wb = map (expandParamsD False ist decorate newargs decls) whereblock

474 logLvl 5 $ "Where block: " ++ show wb

475 mapM_ (elabDecl' EAll info) wb

476 -- Now build the RHS, using the type of the LHS as the goal.

@@ -898,7 +898,7 @@ elabInstance info syn fc cs n ps t expn ds

898

899 insertDef i meth def clauses ns iname decls

900 | null $ filter (clauseFor meth iname ns) decls

901− = let newd = expandParamsD i (\n -> meth) [] [def] clauses in

901+ = let newd = expandParamsD False i (\n -> meth) [] [def] clauses in

902 -- trace (show newd) $

903 decls ++ [newd]

904 | otherwise = decls

@@ -987,7 +987,8 @@ elabDecl' what info (PMutual f ps)

987 mapM_ (elabDecl EDefns info) ps

988elabDecl' what info (PParams f ns ps)

989 = do i <- get

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

990+ iLOG $ "Expanding params block with " ++ show ns ++ " decls " ++

991+ show (concatMap declared ps)

991 let nblock = pblock i

992 let nblock = pblock i

992 mapM_ (elabDecl' what info) nblock

993 mapM_ (elabDecl' what info) nblock

993 where

994 where

@@ -997,7 +998,8 @@ elabDecl' what info (PParams f ns ps)

997 newb = addAlist dsParams (inblock info) in

998 newb = addAlist dsParams (inblock info) in

998 info { params = newps,

999 info { params = newps,

999 inblock = newb }

1000 inblock = newb }

1000− pblock i = map (expandParamsD i id ns (concatMap declared ps)) ps

1001+ pblock i = map (expandParamsD False i id ns

1002+ (concatMap declared ps)) ps

1001

1003

1002elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps

1004elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps

1003 where

1005 where