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

git.iko.soy/Idris-dev

on master help sign in

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

978479bEdwin Brady15 years ago

lib/checkall.idr+1

compare with master

unifiedsplit

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

24import network.cgi

26import 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

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

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

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

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

54 show' acc [] = acc

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

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

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

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

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

60+ show' : Vect a m -> String

61 show' [] = ""

62 show' [x] = show x

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

lib/prelude/fin.idr+5−3

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

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

9instance Eq (Fin n) where

10+ (==) = eq where

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

10− fO == fO = True

12+ eq fO fO = True

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

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

12− _ == _ = False

14+ eq _ _ = False

src/Idris/AbsSyntax.hs+8−5

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

665 show tm = showImp False tm

666

667instance Show PDecl where

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

668+ show d = showDeclImp False d

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

672

669

673instance Show PClause where

670instance Show PClause where

674 show c = showCImp True c

671 show c = showCImp True c

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

676instance Show PData where

673instance Show PData where

677 show d = showDImp False d

674 show d = showDImp False d

678

675

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+

679showCImp :: Bool -> PClause -> String

681showCImp :: Bool -> PClause -> String

680showCImp impl (PClause n l ws r w)

682showCImp impl (PClause n l ws r w)

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

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

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

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

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

728 " in " ++ se 10 sc

730 " in " ++ se 10 sc

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

731 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 $

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

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

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

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

733 ") " ++ st ++

736 ") " ++ 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

44 i <- get

45 ty' <- implicit syn n ty'

46 let ty = addImpl i ty'

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

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

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

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

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

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

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

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

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

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

113 isNonImp _ = Nothing

114 isNonImp _ = Nothing

114

115

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

117+ = getImplB k sc

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

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

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

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

117 getImplB k (PPi _ n ty sc)

120 getImplB k (PPi _ n ty sc)

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

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

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

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

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

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

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

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

638− let lhs = PRef fc iname

649+ [] -> PRef fc iname

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

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

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

640 (map (pexp . mkMethApp) mtys)

652 (map (pexp . mkMethApp) mtys)

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

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

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

659 papp fc f [] = f

671 papp fc f [] = f

660 papp fc f as = PApp fc f as

672 papp fc f as = PApp fc f as

661

673

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+

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

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

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

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

664

686

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

761

783

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

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

763 = do addIBC (IBCDef n)

785 = do addIBC (IBCDef n)

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

764 elabDecl' info d

787 elabDecl' info d

765

788

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

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

src/Idris/ElabTerm.hs+6−1

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

269 args <- get_env

270 cname <- unique_hole (mkCaseName fn)

271 elab' ina (PMetavar cname)

272+ let cname' = mkN cname

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

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

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

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

274 -- elaborate case

275 -- elaborate case

275 updateAux (newdef : )

276 updateAux (newdef : )

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

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

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

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

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

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

280 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

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

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

281

286

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

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