abe2cd3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Tidy case blocks in hole types

abe2cd3Edwin Brady10 years ago

src/Idris/CaseSplit.hs+2−2

compare with master

unifiedsplit

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

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

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

77-- iputStrLn (show pats)

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

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

79 let ctxt = tt_ctxt ist

80 case lookup n pats of

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

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

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

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

249 i <- getIState

250− return (True, delab i tm))

250+ return (True, delabDirect i tm))

251 (\e -> do i <- getIState

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

253 ++ pshow i e

src/Idris/Delaborate.hs+34−13

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

8{-# LANGUAGE PatternGuards #-}

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

10module Idris.Delaborate (

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

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

12 , delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab

13 , pprintDelabTy, pprintErr, resugar

14 ) where

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

82-- | Delaborate a term without resugaring

83delab :: IState -> Term -> PTerm

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

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

86delabMV :: 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

89delabTy :: IState -> Name -> PTerm

95delabTy :: IState -> Name -> PTerm

90delabTy i n

96delabTy i n

91 = case lookupTy n (tt_ctxt i) of

97 = case lookupTy n (tt_ctxt i) of

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

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

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

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

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

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

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

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

102

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

103delab' :: 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

105

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

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

101 -> Term

107 -> Term

102 -> Bool -- ^ use full names

108 -> Bool -- ^ use full names

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

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

110+ -> Bool -- ^ resugar cases

104 -> PTerm

111 -> PTerm

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

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

106 where

113 where

107 un = fileFC "(val)"

114 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

108

128

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

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

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

130 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

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

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

142

162

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

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

164+ | docases

144− | isCaseApp sc

165+ , isCaseApp sc

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

166 , (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

147 | otherwise =

168 | otherwise =

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

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

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

170 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

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

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

207 isCN _ = False

228 isCN _ = False

208

229

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

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

210− delabCase env imps scvar scrutinee caseName caseArgs =

231+ delabCase env imps scrutinee caseName caseArgs =

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

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

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

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

213 _ -> Nothing

234 _ -> Nothing

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

247 = case lookupTy n (tt_ctxt i) of

268 = case lookupTy n (tt_ctxt i) of

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

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

249 case lookupCtxt n (idris_implicits i) of

270 case lookupCtxt n (idris_implicits i) of

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

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

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

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

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

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

253

274

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

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

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

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

2600 focus script

2601 ptm <- get_term

2602 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)])

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

2605 -- now that we have the script apply

2606 -- it to the reflected goal

src/Idris/REPL.hs+3−3

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

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

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

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

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

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

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

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

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

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

441

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

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