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

git.iko.soy/Idris-dev

Fix case split bug on complex nested patterns

Leave 'type' implicit arguments to be inferred, rather than have built.

commit16eee46bae47dd2b3952bd3a40b56fbe02060782 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 10 Nov 2013, 20:36 (13 years ago) parent8531634

3 files changed+29−10

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/CaseSplit.hs+9−3 src/Idris/ElabDecls.hs+19−6

src/Idris/AbsSyntaxTree.hs+1−1

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

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

12221222

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

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

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

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

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

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

src/Idris/CaseSplit.hs+9−3

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

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

6161 Just ty ->

6262 do let splits = findPats ist ty

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

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

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

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

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

6769 newPats <- mapM elabNewPat newPats_in

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

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

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

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

149151 i <- getIState

150152 return (Just (delab i tm)))

151− (\e -> return Nothing)

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

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

155+ return Nothing)

152156

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

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

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

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

171175 | isDConName v ctxt = orig

172176 subst (PRef _ _) = Placeholder

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

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

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

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

175181 subst x = x

src/Idris/ElabDecls.hs+19−6

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

767767 let sa = getSpecApps ist [] r

768768 mapM_ (mkSpecialised ist) sa

769769 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+

770781 mkSpecialised ist specapp = do

771782 let specTy = getSpecTy ist specapp

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

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

822833elabValBind info aspat tm_in

823834 = do ctxt <- getContext

824835 i <- getIState

825− let tm = addImpl i tm_in

836+ let tm = if aspat then addImplPat i tm_in

837+ else addImpl i tm_in

826838 logLvl 10 (showImp Nothing True False tm)

827839 -- try:

828840 -- * ordinary elaboration

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

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

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

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

837849 let vtm = orderPats (getInferTerm tm')

838− let bargs = getPBtys vtm

839850

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

841852 addDeferred def'

842853 mapM_ (elabCaseBlock info []) is

843854

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

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

846− logLvl 2 (show vtm)

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

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

857+-- logLvl 2 (show vtm)

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

859+ let bargs = getPBtys vtm

860+

848861 return (vtm, vty, bargs)

849862

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