git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2712 from david-christiansen/no-more-ugly-script

Show source location of case block names

commitbe03634759e28fb19616675e148e7450b41d788e authorDavid Christiansen <david@davidchristiansen.dk> dateFri 9 Oct 2015, 11:52 (11 years ago) parent32269f8d5b66a9
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