git.iko.soy/Idris-dev
on master help sign in
Show source location of case block names

Names for case block functions (such as "case block in f") now show the source location from which they originated. This will make it easier to diagnose problems like totality warnings coming from case blocks, staging restriction errors from %runElab, and similar.

commitd5b66a9188ff692162b236c25c9fde8640882721 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 9 Oct 2015, 10:31 (11 years ago) parent32ce95f
13 files changed+98−66
compare with master
unifiedsplit
libs/base/Language/Reflection/Utils.idr+8−4 libs/prelude/Language/Reflection.idr+34−33 src/IRTS/Compiler.hs+2−2 src/Idris/Core/Binary.hs+6−2 src/Idris/Core/DeepSeq.hs+4−1 src/Idris/Core/ProofState.hs+1−1 src/Idris/Core/TT.hs+19−5 src/Idris/Delaborate.hs+1−1 src/Idris/Elab/Data.hs+1−1 src/Idris/Elab/Term.hs+3−3 src/Idris/Reflection.hs+10−4 test/reg006/expected+1−1 test/totality009/expected+8−8
libs/base/Language/Reflection/Utils.idr+8−4
@@ -61,6 +61,12 @@ binderTy (Guess t1 t2) = t1
6161binderTy (PVar t) = t
6262binderTy (PVTy t) = t
6363
64+instance Show SourceLocation where
65+ showPrec d (FileLoc filename line col) = showCon d "FileLoc" $ showArg filename ++ showArg line ++ showArg col
66+
67+instance Eq SourceLocation where
68+ (FileLoc fn s e) == (FileLoc fn' s' e') = fn == fn' && s == s' && e == e'
69+
6470mutual
6571 instance Show SpecialName where
6672 showPrec d (WhereN i n1 n2) = showCon d "WhereN" $ showArg i ++
@@ -69,7 +75,7 @@ mutual
6975 showPrec d (InstanceN i ss) = showCon d "InstanceN" $ showArg i ++ showArg ss
7076 showPrec d (ParentN n s) = showCon d "ParentN" $ showArg n ++ showArg s
7177 showPrec d (MethodN n) = showCon d "MethodN" $ showArg n
72− showPrec d (CaseN n) = showCon d "CaseN" $ showArg n
78+ showPrec d (CaseN fc n) = showCon d "CaseN" $ showArg fc ++ showArg n
7379 showPrec d (ElimN n) = showCon d "ElimN" $ showArg n
7480 showPrec d (InstanceCtorN n) = showCon d "InstanceCtorN" $ showArg n
7581 showPrec d (MetaN parent meta) = showCon d "MetaN" $ showArg parent ++ showArg meta
@@ -96,7 +102,7 @@ mutual
96102 (InstanceN i ss) == (InstanceN i' ss') = i == i' && ss == ss'
97103 (ParentN n s) == (ParentN n' s') = n == n' && s == s'
98104 (MethodN n) == (MethodN n') = n == n'
99− (CaseN n) == (CaseN n') = n == n'
105+ (CaseN fc n) == (CaseN fc' n') = fc == fc' && n == n'
100106 (ElimN n) == (ElimN n') = n == n'
101107 (InstanceCtorN n) == (InstanceCtorN n') = n == n'
102108 (MetaN parent meta) == (MetaN parent' meta') = parent == parent' && meta == meta'
@@ -272,8 +278,6 @@ instance Show Raw where
272278 my_show d RType = "RType"
273279 my_show d (RConstant c) = showCon d "RConstant" $ showArg c
274280
275−instance Show SourceLocation where
276− showPrec d (FileLoc filename line col) = showCon d "FileLoc" $ showArg filename ++ showArg line ++ showArg col
277281
278282instance Show Err where
279283 showPrec d (Msg x) = showCon d "Msg" $ showArg x
libs/prelude/Language/Reflection.idr+34−33
@@ -11,6 +11,22 @@ import Prelude.Traversable
1111
1212%access public
1313
14+||| A source location in an Idris file
15+record SourceLocation where
16+ ||| Either a source span or a source location. `start` and `end`
17+ ||| will be the same if it's a point location.
18+ constructor FileLoc
19+
20+ ||| The file name of the source location
21+ filename : String
22+ ||| The line and column of the beginning of the source span
23+ start : (Int, Int)
24+ ||| The line and column of the end of the source span
25+ end : (Int, Int)
26+
27+%name SourceLocation loc
28+
29+
1430mutual
1531 data TTName =
1632 ||| A user-provided name
@@ -34,7 +50,7 @@ mutual
3450 | InstanceN TTName (List String)
3551 | ParentN TTName String
3652 | MethodN TTName
37− | CaseN TTName
53+ | CaseN SourceLocation TTName
3854 | ElimN TTName
3955 | InstanceCtorN TTName
4056 | MetaN TTName TTName
@@ -237,21 +253,6 @@ data Raw =
237253 RConstant Const
238254%name Raw tm, tm'
239255
240−||| A source location in an Idris file
241−record SourceLocation where
242− ||| Either a source span or a source location. `start` and `end`
243− ||| will be the same if it's a point location.
244− constructor FileLoc
245−
246− ||| The file name of the source location
247− filename : String
248− ||| The line and column of the beginning of the source span
249− start : (Int, Int)
250− ||| The line and column of the end of the source span
251− end : (Int, Int)
252−
253−%name SourceLocation loc
254−
255256||| Error reports are a list of report parts
256257data ErrorReportPart =
257258 ||| A human-readable string
@@ -455,6 +456,21 @@ instance Quotable a Raw => Quotable (List a) Raw where
455456 quote [] = `(List.Nil {elem=~(quotedTy {a})})
456457 quote (x :: xs) = `(List.(::) {elem=~(quotedTy {a})} ~(quote x) ~(quote xs))
457458
459+instance Quotable SourceLocation TT where
460+ quotedTy = `(SourceLocation)
461+ quote (FileLoc fn (sl, sc) (el, ec)) =
462+ `(FileLoc ~(quote fn)
463+ (~(quote sl), ~(quote sc))
464+ (~(quote el), ~(quote ec)))
465+
466+instance Quotable SourceLocation Raw where
467+ quotedTy = `(SourceLocation)
468+ quote (FileLoc fn (sl, sc) (el, ec)) =
469+ `(FileLoc ~(quote {t=Raw} fn)
470+ (~(quote {t=Raw} sl), ~(quote {t=Raw} sc))
471+ (~(quote {t=Raw} el), ~(quote {t=Raw} ec)))
472+
473+
458474mutual
459475 instance Quotable TTName TT where
460476 quotedTy = `(TTName)
@@ -471,7 +487,7 @@ mutual
471487 quote (InstanceN i ss) = `(InstanceN ~(quote i) ~(quote ss))
472488 quote (ParentN n s) = `(ParentN ~(quote n) ~(quote s))
473489 quote (MethodN n) = `(MethodN ~(quote n))
474− quote (CaseN n) = `(CaseN ~(quote n))
490+ quote (CaseN fc n) = `(CaseN ~(quote fc) ~(quote n))
475491 quote (ElimN n) = `(ElimN ~(quote n))
476492 quote (InstanceCtorN n) = `(InstanceCtorN ~(quote n))
477493 quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta))
@@ -492,7 +508,7 @@ mutual
492508 quote (InstanceN i ss) = `(InstanceN ~(quote i) ~(quote ss))
493509 quote (ParentN n s) = `(ParentN ~(quote n) ~(quote s))
494510 quote (MethodN n) = `(MethodN ~(quote n))
495− quote (CaseN n) = `(CaseN ~(quote n))
511+ quote (CaseN fc n) = `(CaseN ~(quote fc) ~(quote n))
496512 quote (ElimN n) = `(ElimN ~(quote n))
497513 quote (InstanceCtorN n) = `(InstanceCtorN ~(quote n))
498514 quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta))
@@ -711,18 +727,3 @@ instance Quotable Tactic TT where
711727 quote Skip = `(Skip)
712728 quote (Fail xs) = `(Fail ~(quote xs))
713729 quote SourceFC = `(SourceFC)
714−
715−
716−instance Quotable SourceLocation TT where
717− quotedTy = `(SourceLocation)
718− quote (FileLoc fn (sl, sc) (el, ec)) =
719− `(FileLoc ~(quote fn)
720− (~(quote sl), ~(quote sc))
721− (~(quote el), ~(quote ec)))
722−
723−instance Quotable SourceLocation Raw where
724− quotedTy = `(SourceLocation)
725− quote (FileLoc fn (sl, sc) (el, ec)) =
726− `(FileLoc ~(quote {t=Raw} fn)
727− (~(quote {t=Raw} sl), ~(quote {t=Raw} sc))
728− (~(quote {t=Raw} el), ~(quote {t=Raw} ec)))
src/IRTS/Compiler.hs+2−2
@@ -167,7 +167,7 @@ showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
167167 snRank (InstanceN n args) = "2" ++ nameRank n ++ concatMap show args
168168 snRank (ParentN n s) = "3" ++ nameRank n ++ show s
169169 snRank (MethodN n) = "4" ++ nameRank n
170− snRank (CaseN n) = "5" ++ nameRank n
170+ snRank (CaseN _ n) = "5" ++ nameRank n
171171 snRank (ElimN n) = "6" ++ nameRank n
172172 snRank (InstanceCtorN n) = "7" ++ nameRank n
173173 snRank (WithN i n) = "8" ++ nameRank n ++ show i
@@ -205,7 +205,7 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)
205205 (args, sc) = cases_runtime cd
206206
207207 -- Always attempt to inline functions arising from 'case' expressions
208− caseName (SN (CaseN _)) = True
208+ caseName (SN (CaseN _ _)) = True
209209 caseName (SN (WithN _ _)) = True
210210 caseName (NS n _) = caseName n
211211 caseName _ = False
src/Idris/Core/Binary.hs+6−2
@@ -287,6 +287,9 @@ instance Binary FC where
287287 return (FileFC x1)
288288 _ -> error "Corrupted binary data for FC"
289289
290+instance Binary FC' where
291+ put (FC' fc) = put fc
292+ get = fmap FC' get
290293
291294instance Binary Name where
292295 put x
@@ -337,7 +340,7 @@ instance Binary SpecialName where
337340 put x2
338341 MethodN x1 -> do putWord8 3
339342 put x1
340− CaseN x1 -> do putWord8 4; put x1
343+ CaseN x1 x2 -> do putWord8 4; put x1; put x2
341344 ElimN x1 -> do putWord8 5; put x1
342345 InstanceCtorN x1 -> do putWord8 6; put x1
343346 WithN x1 x2 -> do putWord8 7
@@ -362,7 +365,8 @@ instance Binary SpecialName where
362365 3 -> do x1 <- get
363366 return (MethodN x1)
364367 4 -> do x1 <- get
365− return (CaseN x1)
368+ x2 <- get
369+ return (CaseN x1 x2)
366370 5 -> do x1 <- get
367371 return (ElimN x1)
368372 6 -> do x1 <- get
src/Idris/Core/DeepSeq.hs+4−1
@@ -65,7 +65,7 @@ instance NFData SpecialName where
6565 rnf (InstanceN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
6666 rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
6767 rnf (MethodN x1) = rnf x1 `seq` ()
68− rnf (CaseN x1) = rnf x1 `seq` ()
68+ rnf (CaseN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
6969 rnf (ElimN x1) = rnf x1 `seq` ()
7070 rnf (InstanceCtorN x1) = rnf x1 `seq` ()
7171 rnf (MetaN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
@@ -88,6 +88,9 @@ instance NFData FC where
8888 rnf NoFC = ()
8989 rnf (FileFC f) = rnf f `seq` ()
9090
91+instance NFData FC' where
92+ rnf (FC' fc) = rnf fc `seq` ()
93+
9194instance NFData Provenance where
9295 rnf ExpectedType = ()
9396 rnf InferredVal = ()
src/Idris/Core/ProofState.hs+1−1
@@ -722,7 +722,7 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
722722 let tmt' = normalise ctxt env tmt
723723 let (tacn, tacstr, tactt) = if induction
724724 then (ElimN, "eliminator", "Induction")
725− else (CaseN, "case analysis", "Case analysis")
725+ else (CaseN (FC' emptyFC), "case analysis", "Case analysis")
726726 case unApply tmt' of
727727 (P _ tnm _, tyargs) -> do
728728 case lookupTy (SN (tacn tnm)) ctxt of
src/Idris/Core/TT.hs+19−5
@@ -58,6 +58,7 @@ import Debug.Trace
5858import qualified Data.Map.Strict as Map
5959import Data.Char
6060import Data.Data (Data)
61+import Data.Monoid (mconcat)
6162import Numeric (showIntAtBase)
6263import qualified Data.Text as T
6364import Data.List hiding (group, insert)
@@ -148,7 +149,7 @@ instance Eq FC where
148149 _ == _ = True
149150
150151-- | FC with equality
151−newtype FC' = FC' { unwrapFC :: FC }
152+newtype FC' = FC' { unwrapFC :: FC } deriving (Data, Typeable, Ord)
152153
153154instance Eq FC' where
154155 FC' fc == FC' fc' = fcEq fc fc'
@@ -157,6 +158,9 @@ instance Eq FC' where
157158 fcEq (FileFC f) (FileFC f') = f == f'
158159 fcEq _ _ = False
159160
161+instance Show FC' where
162+ showsPrec d (FC' fc) = showsPrec d fc
163+
160164-- | Empty source location
161165emptyFC :: FC
162166emptyFC = NoFC
@@ -480,7 +484,7 @@ data SpecialName = WhereN !Int !Name !Name
480484 | InstanceN !Name [T.Text]
481485 | ParentN !Name !T.Text
482486 | MethodN !Name
483− | CaseN !Name
487+ | CaseN !FC' !Name
484488 | ElimN !Name
485489 | InstanceCtorN !Name
486490 | MetaN !Name !Name
@@ -530,7 +534,8 @@ instance Show SpecialName where
530534 show (InstanceN cl inst) = showSep ", " (map T.unpack inst) ++ " instance of " ++ show cl
531535 show (MethodN m) = "method " ++ show m
532536 show (ParentN p c) = show p ++ "#" ++ T.unpack c
533− show (CaseN n) = "case block in " ++ show n
537+ show (CaseN fc n) = "case block in " ++ show n ++
538+ if fc == FC' emptyFC then "" else " at " ++ show fc
534539 show (ElimN n) = "<<" ++ show n ++ " eliminator>>"
535540 show (InstanceCtorN n) = "constructor of " ++ show n
536541 show (MetaN parent meta) = "<<" ++ show parent ++ " " ++ show meta ++ ">>"
@@ -547,10 +552,19 @@ showCG (SN s) = showCG' s
547552 showCG' (InstanceN cl inst) = '@':showCG cl ++ '$':showSep ":" (map T.unpack inst)
548553 showCG' (MethodN m) = '!':showCG m
549554 showCG' (ParentN p c) = showCG p ++ "#" ++ show c
550− showCG' (CaseN c) = showCG c ++ "_case"
555+ showCG' (CaseN fc c) = showCG c ++ showFC' fc ++ "_case"
551556 showCG' (ElimN sn) = showCG sn ++ "_elim"
552557 showCG' (InstanceCtorN n) = showCG n ++ "_ictor"
553558 showCG' (MetaN parent meta) = showCG parent ++ "_meta_" ++ showCG meta
559+ showFC' (FC' NoFC) = ""
560+ showFC' (FC' (FileFC f)) = "_" ++ cgFN f
561+ showFC' (FC' (FC f s e))
562+ | s == e = "_" ++ cgFN f ++
563+ "_" ++ show (fst s) ++ "_" ++ show (snd s)
564+ | otherwise = "_" ++ cgFN f ++
565+ "_" ++ show (fst s) ++ "_" ++ show (snd s) ++
566+ "_" ++ show (fst e) ++ "_" ++ show (snd e)
567+ cgFN = concatMap (\c -> if not (isDigit c || isLetter c) then "__" else [c])
554568showCG (SymRef i) = error "can't do codegen for a symbol reference"
555569showCG NErased = "_"
556570
@@ -1436,7 +1450,7 @@ nextName (SN x) = SN (nextName' x)
14361450 nextName' (WithN i n) = WithN i (nextName n)
14371451 nextName' (InstanceN n ns) = InstanceN (nextName n) ns
14381452 nextName' (ParentN n ns) = ParentN (nextName n) ns
1439− nextName' (CaseN n) = CaseN (nextName n)
1453+ nextName' (CaseN fc n) = CaseN fc (nextName n)
14401454 nextName' (ElimN n) = ElimN (nextName n)
14411455 nextName' (MethodN n) = MethodN (nextName n)
14421456 nextName' (InstanceCtorN n) = InstanceCtorN (nextName n)
src/Idris/Delaborate.hs+1−1
@@ -192,7 +192,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
192192 isCaseApp tm | P _ n _ <- fst (unApply tm) = isCN n
193193 | otherwise = False
194194 where isCN (NS n _) = isCN n
195− isCN (SN (CaseN _)) = True
195+ isCN (SN (CaseN _ _)) = True
196196 isCN _ = False
197197
198198 delabCase :: [(Name, Name)] -> [PArg] -> Name -> Term -> Name -> [Term] -> Maybe PTerm
src/Idris/Elab/Data.hs+1−1
@@ -350,7 +350,7 @@ elabCaseFun ind paramPos n ty cons info = do
350350 elimFC = fileFC "(casefun)"
351351
352352 elimDeclName :: Name
353− elimDeclName = if ind then SN . ElimN $ n else SN . CaseN $ n
353+ elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' emptyFC) $ n
354354
355355 applyNS :: Name -> [String] -> Name
356356 applyNS n [] = n
src/Idris/Elab/Term.hs+3−3
@@ -1058,7 +1058,7 @@ elab ist info emode opts fn tm
10581058 let args' = filter (\(n, _) -> n `notElem` argsDropped) args
10591059
10601060 attack
1061− cname' <- defer argsDropped (mkN (mkCaseName fn))
1061+ cname' <- defer argsDropped (mkN (mkCaseName fc fn))
10621062 solve
10631063
10641064 -- if the scrutinee is one of the 'args' in env, we should
@@ -1071,8 +1071,8 @@ elab ist info emode opts fn tm
10711071 -- if we haven't got the type yet, hopefully we'll get it later!
10721072 movelast tyn
10731073 solve
1074− where mkCaseName (NS n ns) = NS (mkCaseName n) ns
1075− mkCaseName n = SN (CaseN n)
1074+ where mkCaseName fc (NS n ns) = NS (mkCaseName fc n) ns
1075+ mkCaseName fc n = SN (CaseN (FC' fc) n)
10761076-- mkCaseName (UN x) = UN (x ++ "_case")
10771077-- mkCaseName (MN i x) = MN i (x ++ "_case")
10781078 mkN n@(NS _ _) = n
src/Idris/Reflection.hs+10−4
@@ -257,9 +257,9 @@ reifyTTNameApp t [sn]
257257 reifySN t [n]
258258 | t == reflm "MethodN" =
259259 MethodN <$> reifyTTName n
260− reifySN t [n]
260+ reifySN t [fc, n]
261261 | t == reflm "CaseN" =
262− CaseN <$> reifyTTName n
262+ CaseN <$> (FC' <$> reifyFC fc) <*> reifyTTName n
263263 reifySN t [n]
264264 | t == reflm "ElimN" =
265265 ElimN <$> reifyTTName n
@@ -698,8 +698,8 @@ reflectSpecialName (ParentN n s) =
698698 reflCall "ParentN" [reflectName n, RConstant (Str (T.unpack s))]
699699reflectSpecialName (MethodN n) =
700700 reflCall "MethodN" [reflectName n]
701−reflectSpecialName (CaseN n) =
702− reflCall "CaseN" [reflectName n]
701+reflectSpecialName (CaseN fc n) =
702+ reflCall "CaseN" [reflectFC (unwrapFC fc), reflectName n]
703703reflectSpecialName (ElimN n) =
704704 reflCall "ElimN" [reflectName n]
705705reflectSpecialName (InstanceCtorN n) =
@@ -941,6 +941,12 @@ reflectFC fc = raw_apply (Var (reflm "FileLoc"))
941941 ]
942942 where intTy = RConstant (AType (ATInt ITNative))
943943
944+reifyFC :: Term -> ElabD FC
945+reifyFC tm
946+ | (P (DCon _ _ _) cn _, [Constant (Str fn), st, end]) <- unApply tm
947+ , cn == reflm "FileLoc" = FC fn <$> reifyPair reifyInt reifyInt st <*> reifyPair reifyInt reifyInt end
948+ | otherwise = fail $ "Not a source location: " ++ show tm
949+
944950fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
945951fromTTMaybe (App _ (App _ (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)
946952 | just == txt "Just" = Just tm
test/reg006/expected+1−1
@@ -1,2 +1,2 @@
11reg006.idr:17:1:
2−RBTree.lookup is possibly not total due to: RBTree.case block in lookup
2+RBTree.lookup is possibly not total due to: RBTree.case block in lookup at reg006.idr:19:8
test/totality009/expected+8−8
@@ -1,8 +1,8 @@
1−TestLambdaPossible.idr:9:25:Warning - TestLambdaPossible.case block in wrongPossible is not total as there are missing cases
2−TestLambdaPossible.idr:9:1:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible
3−TestLambdaPossible.idr:12:25:Warning - TestLambdaPossible.case block in wrongPossible' is not total as there are missing cases
4−TestLambdaPossible.idr:12:1:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible'
5−TestLambdaPossible.idr:9:15:Warning - TestLambdaPossible.case block in wrongPossible is not total as there are missing cases
6−TestLambdaPossible.idr:9:1:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible
7−TestLambdaPossible.idr:12:16:Warning - TestLambdaPossible.case block in wrongPossible' is not total as there are missing cases
8−TestLambdaPossible.idr:12:1:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible'
1+TestLambdaPossible.idr:9:25:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25 is not total as there are missing cases
2+TestLambdaPossible.idr:9:1:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25
3+TestLambdaPossible.idr:12:25:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases
4+TestLambdaPossible.idr:12:1:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25
5+TestLambdaPossible.idr:9:15:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25 is not total as there are missing cases
6+TestLambdaPossible.idr:9:1:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25
7+TestLambdaPossible.idr:12:16:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases
8+TestLambdaPossible.idr:12:1:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25