978479b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

(Try again...) Fixed some case statement bugs

commit978479ba3a0fb996b4308b30edc9070e45f49a49 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 31 Jan 2012, 00:09 (15 years ago) parent6f96ffa

6 files changed+46−12

compare with master

unifiedsplit

lib/checkall.idr+1 lib/prelude.idr+2−2 lib/prelude/fin.idr+5−3 src/Idris/AbsSyntax.hs+8−5 src/Idris/ElabDecls.hs+24−1 src/Idris/ElabTerm.hs+6−1

lib/checkall.idr+1

@@ -24,3 +24,4 @@ import prelude.char

2424import network.cgi

2525

2626import control.monad.identity

27+import control.monad.state

lib/prelude.idr+2−2

@@ -50,14 +50,14 @@ instance (Show a, Show b) => Show (a, b) where

5050

5151instance Show a => Show (List a) where

5252 show xs = "[" ++ show' "" xs ++ "]" where

53− show' : Show a => String -> List a -> String

53+ show' : String -> List a -> String

5454 show' acc [] = acc

5555 show' acc [x] = acc ++ show x

5656 show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs

5757

5858instance Show a => Show (Vect a n) where

5959 show xs = "[" ++ show' xs ++ "]" where

60− show' : Show a => Vect a n -> String

60+ show' : Vect a m -> String

6161 show' [] = ""

6262 show' [x] = show x

6363 show' (x :: xs) = show x ++ ", " ++ show' xs

lib/prelude/fin.idr+5−3

@@ -7,7 +7,9 @@ data Fin : Nat -> Set where

77 fS : Fin k -> Fin (S k)

99instance Eq (Fin n) where

10− fO == fO = True

11− (fS k) == (fS k') = k == k'

12− _ == _ = False

10+ (==) = eq where

11+ eq : Fin m -> Fin m -> Bool

12+ eq fO fO = True

13+ eq (fS k) (fS k') = eq k k'

14+ eq _ _ = False

1315

src/Idris/AbsSyntax.hs+8−5

@@ -665,10 +665,7 @@ instance Show PTerm where

665665 show tm = showImp False tm

666666

667667instance Show PDecl where

668− show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

669− show (PTy _ _ _ n ty) = show n ++ " : " ++ show ty

670− show (PClauses _ _ n c) = showSep "\n" (map show c)

671− show (PData _ _ d) = show d

668+ show d = showDeclImp False d

672669

673670instance Show PClause where

674671 show c = showCImp True c

@@ -676,6 +673,11 @@ instance Show PClause where

676673instance Show PData where

677674 show d = showDImp False d

678675

676+showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

677+showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty

678+showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)

679+showDeclImp _ (PData _ _ d) = show d

680+

679681showCImp :: Bool -> PClause -> String

680682showCImp impl (PClause n l ws r w)

681683 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r

@@ -727,7 +729,8 @@ showImp impl tm = se 10 tm where

727729 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++

728730 " in " ++ se 10 sc

729731 se p (PPi (Exp l s) n ty sc)

730− | n `elem` allNamesIn sc = bracket p 2 $

732+ | n `elem` allNamesIn sc || impl

733+ = bracket p 2 $

731734 if l then "|(" else "(" ++

732735 show n ++ " : " ++ se 10 ty ++

733736 ") " ++ st ++

src/Idris/ElabDecls.hs+24−1

@@ -44,6 +44,7 @@ elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in

4444 i <- get

4545 ty' <- implicit syn n ty'

4646 let ty = addImpl i ty'

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

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

4849 ((ty', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []

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

@@ -112,6 +113,8 @@ elabRecord info syn fc tyn ty cn cty

112113 isNonImp (PExp _ _ _, a) = Just a

113114 isNonImp _ = Nothing

114115

116+ getImplB k (PPi (Imp l s) n Placeholder sc)

117+ = getImplB k sc

115118 getImplB k (PPi (Imp l s) n ty sc)

116119 = getImplB (\x -> k (PPi (Imp l s) n ty x)) sc

117120 getImplB k (PPi _ n ty sc)

@@ -635,7 +638,16 @@ elabInstance info syn fc cs n ps t ds

635638 iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci)

636639 mapM_ (warnMissing ds' ns) (map fst (class_methods ci))

637640 let wb = map mkTyDecl mtys ++ map (decorateid (decorate ns)) ds'

638− let lhs = PRef fc iname

641+ logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys)

642+ -- get the implicit parameters that need passing through to the where block

643+ wparams <- mapM (\p -> case p of

644+ PApp _ _ args -> getWParams args

645+ _ -> return []) ps

646+ logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

647+ show (concat (nub wparams))

648+ let lhs = case concat (nub wparams) of

649+ [] -> PRef fc iname

650+ as -> PApp fc (PRef fc iname) as

639651 let rhs = PApp fc (PRef fc (instanceName ci))

640652 (map (pexp . mkMethApp) mtys)

641653 let idecl = PClauses fc [Inlinable, TCGen] iname

@@ -659,6 +671,16 @@ elabInstance info syn fc cs n ps t ds

659671 papp fc f [] = f

660672 papp fc f as = PApp fc f as

661673

674+ getWParams [] = return []

675+ getWParams (p : ps)

676+ | PRef _ n <- getTm p

677+ = do ps' <- getWParams ps

678+ ctxt <- getContext

679+ case lookupP Nothing n ctxt of

680+ [] -> return (pimp n (PRef fc n) : ps')

681+ _ -> return ps'

682+ getWParams (_ : ps) = getWParams ps

683+

662684 decorate ns (UN n) = NS (UN ('!':n)) ns

663685 decorate ns (NS (UN n) s) = NS (UN ('!':n)) ns

664686

@@ -761,6 +783,7 @@ elabDecl' info (PDirective i) = i

761783

762784elabCaseBlock info d@(PClauses f o n ps)

763785 = do addIBC (IBCDef n)

786+-- iputStrLn $ "CASE BLOCK: " ++ show (n, d)

764787 elabDecl' info d

765788

766789-- elabDecl' info (PImport i) = loadModule i

src/Idris/ElabTerm.hs+6−1

@@ -269,7 +269,8 @@ elab ist info pattern tcgen fn tm

269269 args <- get_env

270270 cname <- unique_hole (mkCaseName fn)

271271 elab' ina (PMetavar cname)

272− let newdef = PClauses fc [] cname (caseBlock fc cname (reverse args) opts)

272+ let cname' = mkN cname

273+ let newdef = PClauses fc [] cname' (caseBlock fc cname' (reverse args) opts)

273274 -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args

274275 -- elaborate case

275276 updateAux (newdef : )

@@ -277,6 +278,10 @@ elab ist info pattern tcgen fn tm

277278 where mkCaseName (NS n ns) = NS (mkCaseName n) ns

278279 mkCaseName (UN x) = UN (x ++ "_case")

279280 mkCaseName (MN i x) = MN i (x ++ "_case")

281+ mkN n@(NS _ _) = n

282+ mkN n = case namespace info of

283+ Just xs@(_:_) -> NS n xs

284+ _ -> n

280285 elab' ina x = fail $ "Something's gone wrong. Did you miss a semi-colon somewhere?"

281286

282287 caseBlock :: FC -> Name -> [(Name, Binder Term)] -> [(PTerm, PTerm)] -> [PClause]