16eee46 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix case split bug on complex nested patterns

16eee46Edwin Brady13 years ago

src/Idris/AbsSyntaxTree.hs+1−1

compare with master

unifiedsplit

@@ -1221,7 +1221,7 @@ showImp ist impl colour tm = se 10 [] tm where

1221-- se p bnd x = "Not implemented"

1222

1223 slist' p bnd (PApp _ (PRef _ nil) _)

1224− | nsroot nil == UN "Nil" = Just []

1224+ | not impl && nsroot nil == UN "Nil" = Just []

1225 slist' p bnd (PApp _ (PRef _ cons) args)

1226 | nsroot cons == UN "::",

1227 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

src/Idris/CaseSplit.hs+9−3

@@ -60,10 +60,12 @@ split n t'

60 Nothing -> fail $ show n ++ " is not a pattern variable"

61 Just ty ->

62 do let splits = findPats ist ty

63− iLOG ("New patterns " ++ show splits)

63+ iLOG ("New patterns " ++ showSep ", "

64+ (map (showImp Nothing True False) splits))

64 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)

65 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)

65 logLvl 4 ("Working from " ++ show t)

66 logLvl 4 ("Working from " ++ show t)

66− logLvl 4 ("Trying " ++ showSep "\n" (map show newPats_in))

67+ logLvl 4 ("Trying " ++ showSep "\n"

68+ (map (showImp Nothing True False) newPats_in))

67 newPats <- mapM elabNewPat newPats_in

69 newPats <- mapM elabNewPat newPats_in

68 logLvl 3 ("Original:\n" ++ show t)

70 logLvl 3 ("Original:\n" ++ show t)

69 logLvl 3 ("Split:\n" ++

71 logLvl 3 ("Split:\n" ++

@@ -148,7 +150,9 @@ elabNewPat :: PTerm -> Idris (Maybe PTerm)

148elabNewPat t = idrisCatch (do (tm, ty) <- elabVal toplevel True t

150elabNewPat t = idrisCatch (do (tm, ty) <- elabVal toplevel True t

149 i <- getIState

151 i <- getIState

150 return (Just (delab i tm)))

152 return (Just (delab i tm)))

153+ (\e -> do i <- getIState

154+ logLvl 5 $ "Not a valid split:\n" ++ pshow i e

151− (\e -> return Nothing)

155+ return Nothing)

152

156

153findPats :: IState -> Type -> [PTerm]

157findPats :: IState -> Type -> [PTerm]

154findPats ist t | (P _ n _, _) <- unApply t

158findPats ist t | (P _ n _, _) <- unApply t

@@ -170,6 +174,8 @@ replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)

170 subst orig@(PRef _ v) | v == n = t

174 subst orig@(PRef _ v) | v == n = t

171 | isDConName v ctxt = orig

175 | isDConName v ctxt = orig

172 subst (PRef _ _) = Placeholder

176 subst (PRef _ _) = Placeholder

177+ subst (PApp fc (PRef _ t) pats)

178+ | isTConName t ctxt = Placeholder -- infer types

173 subst (PApp fc f pats) = PApp fc f (map substArg pats)

179 subst (PApp fc f pats) = PApp fc f (map substArg pats)

174 subst (PEq fc l r) = PEq fc (subst l) (subst r)

180 subst (PEq fc l r) = PEq fc (subst l) (subst r)

175 subst x = x

181 subst x = x

src/Idris/ElabDecls.hs+19−6

@@ -767,6 +767,17 @@ elabPE info fc r =

767 let sa = getSpecApps ist [] r

768 mapM_ (mkSpecialised ist) sa

769 where

770+ -- TODO: Freeze the newly defined name, make sure it never gets

771+ -- reduced when specialising (not quite the same as an 'abstract' name

772+ -- so may need a new class (public/abstract/private/specialised)

773+

774+ -- Add a PTerm level transformation rule, which is basically the

775+ -- new definition in reverse (before specialising it).

776+ -- RHS => LHS where implicit arguments are left blank in the

777+ -- transformation.

778+

779+ -- Apply that transformation after every PClauses elaboration

780+

770 mkSpecialised ist specapp = do

781 mkSpecialised ist specapp = do

771 let specTy = getSpecTy ist specapp

782 let specTy = getSpecTy ist specapp

772 let (n, newnm, [(lhs, rhs)]) = getSpecClause ist specapp

783 let (n, newnm, [(lhs, rhs)]) = getSpecClause ist specapp

@@ -822,7 +833,8 @@ elabValBind :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])

822elabValBind info aspat tm_in

833elabValBind info aspat tm_in

823 = do ctxt <- getContext

834 = do ctxt <- getContext

824 i <- getIState

835 i <- getIState

836+ let tm = if aspat then addImplPat i tm_in

825− let tm = addImpl i tm_in

837+ else addImpl i tm_in

826 logLvl 10 (showImp Nothing True False tm)

838 logLvl 10 (showImp Nothing True False tm)

827 -- try:

839 -- try:

828 -- * ordinary elaboration

840 -- * ordinary elaboration

@@ -833,18 +845,19 @@ elabValBind info aspat tm_in

833-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []

845-- tctry (elaborate ctxt (MN 0 "val") (TType (UVal 0)) []

834-- (build i info aspat (MN 0 "val") tm))

846-- (build i info aspat (MN 0 "val") tm))

835 tclift (elaborate ctxt (MN 0 "val") infP []

847 tclift (elaborate ctxt (MN 0 "val") infP []

836− (build i info aspat (MN 0 "val") (infTerm tm)))

848+ (buildTC i info aspat False (MN 0 "val") (infTerm tm)))

837 let vtm = orderPats (getInferTerm tm')

849 let vtm = orderPats (getInferTerm tm')

838− let bargs = getPBtys vtm

839

850

840 def' <- checkDef (fileFC "(input)") defer

851 def' <- checkDef (fileFC "(input)") defer

841 addDeferred def'

852 addDeferred def'

842 mapM_ (elabCaseBlock info []) is

853 mapM_ (elabCaseBlock info []) is

843

854

844− logLvl 3 ("Value: " ++ show tm')

855+ logLvl 3 ("Value: " ++ show vtm)

845− recheckC (fileFC "(input)") [] tm'

856+-- recheckC (fileFC "(input)") [] tm'

846− logLvl 2 (show vtm)

857+-- logLvl 2 (show vtm)

847 (vtm, vty) <- recheckC (fileFC "(input)") [] vtm

858 (vtm, vty) <- recheckC (fileFC "(input)") [] vtm

859+ let bargs = getPBtys vtm

860+

848 return (vtm, vty, bargs)

861 return (vtm, vty, bargs)

849

862

850elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)

863elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)