2b7db6a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix 'where' lifting bug

Make sure functions have unique names when lifted

commit2b7db6af4cd62680504c26d5882dc38582846641 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 5 Nov 2012, 15:02 (14 years ago) parent379c0f9

5 files changed+32−6

compare with master

unifiedsplit

src/Idris/Docs.hs+2 src/Idris/ElabDecls.hs+8−6 test/reg004/expected+2 test/reg004/reg004.idr+16 test/reg004/run+4

src/Idris/Docs.hs+2

@@ -7,6 +7,8 @@ import Core.Evaluate

88import Data.Maybe

10+-- TODO: Only include names with public/abstract accessibility

11+

1012data FunDoc = Doc Name String

1113 [(Name, PArg)] -- args

1214 PTerm -- function type

src/Idris/ElabDecls.hs+8−6

@@ -277,7 +277,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

277277 -- question: CAFs in where blocks?

278278 tclift $ tfail $ (At fc (NoTypeDecl n))

279279 [ty] -> return ty

280− pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs

280+ pats_in <- mapM (elabClause info (TCGen `elem` opts))

281+ (zip [0..] cs)

281282 -- if the return type of 'ty' is collapsible, the optimised version should

282283 -- just do nothing

283284 ist <- get

@@ -439,14 +440,15 @@ checkPossible info fc tcgen fname lhs_in

439440-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)

440441 Error _ -> return False

441442

442−elabClause :: ElabInfo -> Bool -> PClause -> Idris (Either Term (Term, Term))

443−elabClause info tcgen (PClause fc fname lhs_in [] PImpossible [])

443+elabClause :: ElabInfo -> Bool -> (Int, PClause) ->

444+ Idris (Either Term (Term, Term))

445+elabClause info tcgen (_, PClause fc fname lhs_in [] PImpossible [])

444446 = do b <- checkPossible info fc tcgen fname lhs_in

445447 case b of

446448 True -> fail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"

447449 False -> do ptm <- mkPatTm lhs_in

448450 return (Left ptm)

449−elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)

451+elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

450452 = do ctxt <- getContext

451453 -- Build the LHS as an "Infer", and pull out its type and

452454 -- pattern bindings

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

503505 checkInferred fc (delab' i crhs True) rhs

504506 return $ Right (clhs, crhs)

505507 where

506− decorate x = UN (show x ++ "#" ++ show fname)

508+ decorate x = UN (show x ++ "#" ++ show cnum ++ "#" ++ show fname)

507509 pinfo ns ps i

508510 = let ds = concatMap declared ps

509511 newps = params info ++ ns

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

517519 -- _ -> MN i (show n)) . l

518520 }

519521

520−elabClause info tcgen (PWith fc fname lhs_in withs wval_in withblock)

522+elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

521523 = do ctxt <- getContext

522524 -- Build the LHS as an "Infer", and pull out its type and

523525 -- pattern bindings

test/reg004/expectednew file+2

@@ -0,0 +1,2 @@

1+O

2+sO

test/reg004/reg004.idrnew file+16

@@ -0,0 +1,16 @@

1+module Main

3+h : Bool -> Nat

4+h False = r1 where

5+ r : Nat

6+ r = S O

7+ r1 : Nat

8+ r1 = r

9+h True = r2 where

10+ r : Nat

11+ r = O

12+ r2 : Nat

13+ r2 = r

14+

15+main : IO ()

16+main = do print (h True); print (h False)

test/reg004/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris reg004.idr -o reg004

3+./reg004

4+rm -f reg004 *.ibc