abe2cd3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tidy case blocks in hole types

The 'let' binding of the scrutinee at the top gets normalised away so we can't assume it's there.

commitabe2cd31d27c5574bbdbe07a8ed5b18c4b4e92a5 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 25 Jul 2016, 13:05 (10 years ago) parent1db4b80

4 files changed+40−19

compare with master

unifiedsplit

src/Idris/CaseSplit.hs+2−2 src/Idris/Delaborate.hs+34−13 src/Idris/Elab/Term.hs+1−1 src/Idris/REPL.hs+3−3

src/Idris/CaseSplit.hs+2−2

@@ -75,7 +75,7 @@ split n t'

7575 logElab 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)

7676-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))

7777-- iputStrLn (show pats)

78− let t = mergeUserImpl (addImplPat ist t') (delab ist tm)

78+ let t = mergeUserImpl (addImplPat ist t') (delabDirect ist tm)

7979 let ctxt = tt_ctxt ist

8080 case lookup n pats of

8181 Nothing -> ifail $ show n ++ " is not a pattern variable"

@@ -247,7 +247,7 @@ tidy ist tm ty = return tm

247247elabNewPat :: PTerm -> Idris (Bool, PTerm)

248248elabNewPat t = idrisCatch (do (tm, ty) <- elabVal (recinfo (fileFC "casesplit")) ELHS t

249249 i <- getIState

250− return (True, delab i tm))

250+ return (True, delabDirect i tm))

251251 (\e -> do i <- getIState

252252 logElab 5 $ "Not a valid split:\n" ++ showTmImpls t ++ "\n"

253253 ++ pshow i e

src/Idris/Delaborate.hs+34−13

@@ -8,7 +8,7 @@ Maintainer : The Idris Community.

88{-# LANGUAGE PatternGuards #-}

99{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

1010module Idris.Delaborate (

11− annName, bugaddr, delab, delab', delabMV, delabSugared

11+ annName, bugaddr, delab, delabDirect, delab', delabMV, delabSugared

1212 , delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab

1313 , pprintDelabTy, pprintErr, resugar

1414 ) where

@@ -81,30 +81,50 @@ delabSugared ist tm = resugar ist $ delab ist tm

8181

8282-- | Delaborate a term without resugaring

8383delab :: IState -> Term -> PTerm

84−delab i tm = delab' i tm False False

84+delab i tm = delab' i tm False False

8585

8686delabMV :: IState -> Term -> PTerm

87−delabMV i tm = delab' i tm False True

87+delabMV i tm = delab' i tm False True

88+

89+-- | Delaborate a term directly, leaving case applications as they are.

90+-- We need this for interactive case splitting, where we need access to the

91+-- underlying function in a delaborated form, to generate the right patterns

92+delabDirect :: IState -> Term -> PTerm

93+delabDirect i tm = delabTy' i [] tm False False False

8894

8995delabTy :: IState -> Name -> PTerm

9096delabTy i n

9197 = case lookupTy n (tt_ctxt i) of

9298 (ty:_) -> case lookupCtxt n (idris_implicits i) of

93− (imps:_) -> delabTy' i imps ty False False

94− _ -> delabTy' i [] ty False False

99+ (imps:_) -> delabTy' i imps ty False False True

100+ _ -> delabTy' i [] ty False False True

95101 [] -> error "delabTy: got non-existing name"

96102

97103delab' :: IState -> Term -> Bool -> Bool -> PTerm

98−delab' i t f mvs = delabTy' i [] t f mvs

104+delab' i t f mvs = delabTy' i [] t f mvs True

99105

100106delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any

101107 -> Term

102108 -> Bool -- ^ use full names

103109 -> Bool -- ^ Don't treat metavariables specially

110+ -> Bool -- ^ resugar cases

104111 -> PTerm

105−delabTy' ist imps tm fullname mvs = de [] imps tm

112+delabTy' ist imps tm fullname mvs docases = de [] imps tm

106113 where

107114 un = fileFC "(val)"

115+

116+ -- Special case for spotting applications of case functions

117+ -- (Normally the scrutinee is let-bound, but hole types get normalised,

118+ -- so they could appear in this form. The scrutinee is always added as

119+ -- the last argument,

120+ -- although that's not always the thing that gets pattern matched

121+ -- in the elaborated block)

122+ de env imps sc

123+ | docases

124+ , isCaseApp sc

125+ , (P _ cOp _, args@(_:_)) <- unApply sc

126+ , Just caseblock <- delabCase env imps (last args) cOp args

127+ = caseblock

108128

109129 de env _ (App _ f a) = deFn env f [a]

110130 de env _ (V i) | i < length env = PRef un [] (snd (env!!i))

@@ -141,9 +161,10 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

141161 = PPi expl n NoFC (de env [] ty) (de ((n,n):env) [] sc)

142162

143163 de env imps (Bind n (Let ty val) sc)

144− | isCaseApp sc

164+ | docases

165+ , isCaseApp sc

145166 , (P _ cOp _, args) <- unApply sc

146− , Just caseblock <- delabCase env imps n val cOp args = caseblock

167+ , Just caseblock <- delabCase env imps val cOp args = caseblock

147168 | otherwise =

148169 PLet un n NoFC (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

149170 de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc

@@ -206,8 +227,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

206227 isCN (SN (CaseN _ _)) = True

207228 isCN _ = False

208229

209− delabCase :: [(Name, Name)] -> [PArg] -> Name -> Term -> Name -> [Term] -> Maybe PTerm

210− delabCase env imps scvar scrutinee caseName caseArgs =

230+ delabCase :: [(Name, Name)] -> [PArg] -> Term -> Name -> [Term] -> Maybe PTerm

231+ delabCase env imps scrutinee caseName caseArgs =

211232 do cases <- case lookupCtxt caseName (idris_patdefs ist) of

212233 [(cases, _)] -> return cases

213234 _ -> Nothing

@@ -247,8 +268,8 @@ pprintDelabTy i n

247268 = case lookupTy n (tt_ctxt i) of

248269 (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $

249270 case lookupCtxt n (idris_implicits i) of

250− (imps:_) -> resugar i $ delabTy' i imps ty False False

251− _ -> resugar i $ delabTy' i [] ty False False

271+ (imps:_) -> resugar i $ delabTy' i imps ty False False True

272+ _ -> resugar i $ delabTy' i [] ty False False True

252273 [] -> error "pprintDelabTy got a name that doesn't exist"

253274

254275pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

src/Idris/Elab/Term.hs+1−1

@@ -2600,7 +2600,7 @@ runTac autoSolve ist perhapsFC fn tac

26002600 focus script

26012601 ptm <- get_term

26022602 elab ist toplevel ERHS [] (sMN 0 "tac")

2603− (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])

2603+ (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True True)])

26042604 (script', _) <- get_type_val (Var scriptvar)

26052605 -- now that we have the script apply

26062606 -- it to the reflected goal

src/Idris/REPL.hs+3−3

@@ -435,9 +435,9 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

435435 splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

436436 splitPi ist (Bind n (Pi _ t _) rest) =

437437 let (hs, c, pc) = splitPi ist rest in

438− ((n, t, delabTy' ist [] t False False):hs,

439− c, delabTy' ist [] c False False)

440− splitPi ist tm = ([], tm, delabTy' ist [] tm False False)

438+ ((n, t, delabTy' ist [] t False False True):hs,

439+ c, delabTy' ist [] c False False True)

440+ splitPi ist tm = ([], tm, delabTy' ist [] tm False False True)

441441

442442 -- | Get the types of a list of metavariable names

443443 mvTys :: IState -> [Name] -> [(Name, Type)]