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

git.iko.soy/Idris-dev

on master help sign in

Fix 'where' lifting bug

2b7db6aEdwin Brady14 years ago

src/Idris/Docs.hs+2

compare with master

unifiedsplit

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

8import Data.Maybe

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

11+

10data FunDoc = Doc Name String

12data FunDoc = Doc Name String

11 [(Name, PArg)] -- args

13 [(Name, PArg)] -- args

12 PTerm -- function type

14 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

277 -- question: CAFs in where blocks?

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

279 [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)

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

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

282 -- just do nothing

283 -- just do nothing

283 ist <- get

284 ist <- get

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

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

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

440 Error _ -> return False

441 Error _ -> return False

441

442

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

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

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

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

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

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

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

445 case b of

447 case b of

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

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

447 False -> do ptm <- mkPatTm lhs_in

449 False -> do ptm <- mkPatTm lhs_in

448 return (Left ptm)

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

450 = do ctxt <- getContext

452 = do ctxt <- getContext

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

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

452 -- pattern bindings

454 -- pattern bindings

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

503 checkInferred fc (delab' i crhs True) rhs

505 checkInferred fc (delab' i crhs True) rhs

504 return $ Right (clhs, crhs)

506 return $ Right (clhs, crhs)

505 where

507 where

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

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

507 pinfo ns ps i

509 pinfo ns ps i

508 = let ds = concatMap declared ps

510 = let ds = concatMap declared ps

509 newps = params info ++ ns

511 newps = params info ++ ns

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

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

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

518 }

520 }

519

521

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)

521 = do ctxt <- getContext

523 = do ctxt <- getContext

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

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

523 -- pattern bindings

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