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

git.iko.soy/Idris-dev

Fix parameter block expansion

commit1b6cc6aee1c09b5038b355b8f689e2364a764542 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 14 Nov 2012, 00:49 (14 years ago) parentca684b6

2 files changed+28−22

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+21−17 src/Idris/ElabDecls.hs+7−5

src/Idris/AbsSyntax.hs+21−17

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

502502

503503 nseq x y = nsroot x == nsroot y

504504

505−expandParamsD :: IState ->

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

506+ IState ->

506507 (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)

508509 = if n `elem` ns

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

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

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

513514 PClauses fc opts n' (map expandParamsC cs)

514515 where

515516 expandParamsC (PClause fc n lhs ws rhs ds)

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

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

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

518520 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'

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

521523 (expandParams dec ps'' ns rhs)

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

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

523525 expandParamsC (PWith fc n lhs ws wval ds)

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

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

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

526529 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'

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

529532 (expandParams dec ps'' ns wval)

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

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

531534 updateps yn nm [] = []

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

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

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

536539 = PData doc syn fc co (expandPData pd)

537540 where

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

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

544547 econ (doc, n, t, fc)

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

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

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

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

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

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

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

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

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

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

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

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

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

552556 = PClass doc info f

553557 (map (expandParams dec ps ns) cs)

554558 n

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

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

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

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

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

558562 = PInstance info f

559563 (map (expandParams dec ps ns) cs)

560564 n

561565 (map (expandParams dec ps ns) params)

562566 (expandParams dec ps ns ty)

563567 cn

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

565−expandParamsD ist dec ps ns d = d

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

569+expandParamsD rhs ist dec ps ns d = d

566570

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

568572

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

4545 do checkUndefined fc n

4646 ctxt <- getContext

4747 i <- get

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

4849 ty' <- implicit syn n ty'

4950 let ty = addImpl i ty'

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

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

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

5353 (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)

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

471471 let decls = concatMap declared whereblock

472472 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

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

475475 mapM_ (elabDecl' EAll info) wb

476476 -- 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

898898

899899 insertDef i meth def clauses ns iname decls

900900 | 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

902902 -- trace (show newd) $

903903 decls ++ [newd]

904904 | otherwise = decls

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

987987 mapM_ (elabDecl EDefns info) ps

988988elabDecl' what info (PParams f ns ps)

989989 = 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)

991992 let nblock = pblock i

992993 mapM_ (elabDecl' what info) nblock

993994 where

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

997998 newb = addAlist dsParams (inblock info) in

998999 info { params = newps,

9991000 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

10011003

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

10031005 where