17d2cea · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix for expansion of types in parameters blocks

commit17d2cea22143c28bb1a2db1ce02f67c7991bca14 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 21 Nov 2012, 22:53 (14 years ago) parentb939fbd

1 file changed+6−4

unifiedsplit

src/Idris/AbsSyntax.hs+6−4

@@ -505,10 +505,12 @@ expandParams dec ps ns tm = en tm

505505expandParamsD :: Bool -> -- True = RHS only

506506 IState ->

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

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

509− = if n `elem` ns

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

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

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

509+ = if n `elem` ns && (not rhsonly)

510+ then -- trace (show (n, expandParams dec ps ns ty)) $

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

512+ else --trace (show (n, expandParams dec ps ns ty)) $

513+ PTy doc syn fc o n (expandParams dec ps ns ty)

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

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

514516 PClauses fc opts n' (map expandParamsC cs)