4ede52d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow the pretty-printing of Raw terms

Also, this extends Elab reflection and error reflection to be able to display Raw terms in an accessible, debuggable meta-presentation. This makes it much easier to debug user elaborator scripts.

commit4ede52d3f94d71855222f91ff448595230ed1267 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 1 Jun 2015, 16:07 (11 years ago) parentfa38cb5

11 files changed+96−34

compare with master

unifiedsplit

libs/prelude/Language/Reflection.idr+10−8 libs/prelude/Language/Reflection/Elab.idr+4−4 src/Idris/Core/Binary.hs+2 src/Idris/Core/DeepSeq.hs+8−1 src/Idris/Core/Elaborate.hs+1−1 src/Idris/Core/TT.hs+50−1 src/Idris/DeepSeq.hs−6 src/Idris/Delaborate.hs+9−7 src/Idris/Elab/Term.hs+3−5 src/Idris/IBC.hs+1−1 src/Idris/Reflection.hs+8

libs/prelude/Language/Reflection.idr+10−8

@@ -215,6 +215,8 @@ data ErrorReportPart =

215215 NamePart TTName |

216216 ||| An Idris term, to be pretty printed

217217 TermPart TT |

218+ ||| A Raw term to be displayed by the compiler

219+ RawPart Raw |

218220 ||| An indented sub-report, to provide more details

219221 SubReport (List ErrorReportPart)

220222%name ErrorReportPart part, p

@@ -576,14 +578,6 @@ mutual

576578 quote (PVar x) = `(PVar {a=TT} ~(assert_total (quote x)))

577579 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))

578580

579−

580−instance Quotable ErrorReportPart TT where

581− quotedTy = `(ErrorReportPart)

582− quote (TextPart x) = `(TextPart ~(quote x))

583− quote (NamePart n) = `(NamePart ~(quote n))

584− quote (TermPart tm) = `(TermPart ~(quote tm))

585− quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs))

586−

587581mutual

588582 quoteRaw : Raw -> TT

589583 quoteRaw (Var n) = `(Var ~(quote n))

@@ -613,6 +607,14 @@ instance Quotable (Binder Raw) TT where

613607 quotedTy = `(Binder Raw)

614608 quote = quoteRawBinder

615609

610+instance Quotable ErrorReportPart TT where

611+ quotedTy = `(ErrorReportPart)

612+ quote (TextPart x) = `(TextPart ~(quote x))

613+ quote (NamePart n) = `(NamePart ~(quote n))

614+ quote (TermPart tm) = `(TermPart ~(quote tm))

615+ quote (RawPart tm) = `(RawPart ~(quote tm))

616+ quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs))

617+

616618instance Quotable Tactic TT where

617619 quotedTy = `(Tactic)

618620 quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))

libs/prelude/Language/Reflection/Elab.idr+4−4

@@ -118,7 +118,7 @@ data Elab : Type -> Type where

118118 prim__Search : Int -> List TTName -> Elab ()

119119 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)

120120

121− prim__Debug : {a : Type} -> Maybe String -> Elab a

121+ prim__Debug : {a : Type} -> List ErrorReportPart -> Elab a

122122

123123

124124-------------

@@ -329,7 +329,7 @@ namespace Tactics

329329 ||| This is intended for elaboration script developers, not for

330330 ||| end-users. Use `fail` for final scripts.

331331 debug : Elab a

332− debug = prim__Debug Nothing

332+ debug = prim__Debug []

333333

334334 ||| Halt elaboration, dumping the internal state and displaying a

335335 ||| message.

@@ -338,8 +338,8 @@ namespace Tactics

338338 ||| end-users. Use `fail` for final scripts.

339339 |||

340340 ||| @ msg the message to display

341− debugMessage : (msg : String) -> Elab a

342− debugMessage msg = prim__Debug (Just msg)

341+ debugMessage : (msg : List ErrorReportPart) -> Elab a

342+ debugMessage msg = prim__Debug msg

343343

344344 ||| Recursively invoke the reflected elaborator with some goal.

345345 |||

src/Idris/Core/Binary.hs+2

@@ -18,6 +18,7 @@ instance Binary ErrorReportPart where

1818 put (NamePart n) = do putWord8 1 ; put n

1919 put (TermPart t) = do putWord8 2 ; put t

2020 put (SubReport ps) = do putWord8 3 ; put ps

21+ put (RawPart r) = do putWord8 4 ; put r

2122

2223 get = do i <- getWord8

2324 case i of

@@ -25,6 +26,7 @@ instance Binary ErrorReportPart where

2526 1 -> fmap NamePart get

2627 2 -> fmap TermPart get

2728 3 -> fmap SubReport get

29+ 4 -> fmap RawPart get

2830 _ -> error "Corrupted binary data for ErrorReportPart"

2931

3032instance Binary Provenance where

src/Idris/Core/DeepSeq.hs+8−1

@@ -76,7 +76,7 @@ instance NFData Err where

7676 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

7777 rnf (CantInferType x1) = rnf x1 `seq` ()

7878 rnf (CantMatch x1) = rnf x1 `seq` ()

79− rnf (ReflectionError x1 x2) = x1 `seq` rnf x2 `seq` ()

79+ rnf (ReflectionError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

8080 rnf (ReflectionFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

8181 rnf (CantSolveGoal x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

8282 rnf (UniqueError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

@@ -111,6 +111,13 @@ instance NFData Err where

111111 rnf (ElabScriptDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

112112 rnf (ElabScriptStuck x1) = rnf x1 `seq` ()

113113

114+instance NFData ErrorReportPart where

115+ rnf (TextPart x1) = rnf x1 `seq` ()

116+ rnf (TermPart x1) = rnf x1 `seq` ()

117+ rnf (RawPart x1) = rnf x1 `seq` ()

118+ rnf (NamePart x1) = rnf x1 `seq` ()

119+ rnf (SubReport x1) = rnf x1 `seq` ()

120+

114121instance NFData ImplicitInfo where

115122 rnf (Impl x1) = rnf x1 `seq` ()

116123

src/Idris/Core/Elaborate.hs+1−1

@@ -877,7 +877,7 @@ prunStateT pmax zok ps x s

877877 else OK ((v, newpmax, problems p), s')

878878 Error e -> Error e

879879

880−debugElaborator :: Maybe String -> Elab' aux a

880+debugElaborator :: [ErrorReportPart] -> Elab' aux a

881881debugElaborator msg = do ps <- fmap proof get

882882 saveState -- so we don't need to remember the hole order

883883 hs <- get_holes

src/Idris/Core/TT.hs+50−1

@@ -176,6 +176,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St

176176data ErrorReportPart = TextPart String

177177 | NamePart Name

178178 | TermPart Term

179+ | RawPart Raw

179180 | SubReport [ErrorReportPart]

180181 deriving (Show, Eq, Data, Typeable)

181182

@@ -244,7 +245,7 @@ data Err' t

244245 | LoadingFailed String (Err' t)

245246 | ReflectionError [[ErrorReportPart]] (Err' t)

246247 | ReflectionFailed String (Err' t)

247− | ElabScriptDebug (Maybe String) t [(Name, t, [(Name, Binder t)])]

248+ | ElabScriptDebug [ErrorReportPart] t [(Name, t, [(Name, Binder t)])]

248249 -- ^ User-specified message, proof term, goals with context (first goal is focused)

249250 | ElabScriptStuck t

250251 deriving (Eq, Functor, Data, Typeable)

@@ -288,6 +289,7 @@ deriving instance NFData Err

288289instance Sized ErrorReportPart where

289290 size (TextPart msg) = 1 + length msg

290291 size (TermPart t) = 1 + size t

292+ size (RawPart r) = 1 + size r

291293 size (NamePart n) = 1 + size n

292294 size (SubReport rs) = 1 + size rs

293295

@@ -1715,6 +1717,53 @@ pprintTT bound tm = pp startPrec bound tm

17151717 | outer > inner = lparen <> doc <> rparen

17161718 | otherwise = doc

17171719

1720+-- | Pretty-print a raw term.

1721+pprintRaw :: [Name] -- ^ Bound names, for highlighting

1722+ -> Raw -- ^ The term to pretty-print

1723+ -> Doc OutputAnnotation

1724+pprintRaw bound (Var n) =

1725+ enclose lparen rparen . group . align . hang 2 $

1726+ (text "Var") <$> annotate (if n `elem` bound

1727+ then AnnBoundName n False

1728+ else AnnName n Nothing Nothing Nothing)

1729+ (text $ show n)

1730+pprintRaw bound (RBind n b body) =

1731+ enclose lparen rparen . group . align . hang 2 $

1732+ vsep [ text "RBind"

1733+ , annotate (AnnBoundName n False) (text $ show n)

1734+ , ppb b

1735+ , pprintRaw (n:bound) body]

1736+ where

1737+ ppb (Lam ty) = enclose lparen rparen . group . align . hang 2 $

1738+ text "Lam" <$> pprintRaw bound ty

1739+ ppb (Pi _ ty k) = enclose lparen rparen . group . align . hang 2 $

1740+ vsep [text "Pi", pprintRaw bound ty, pprintRaw bound k]

1741+ ppb (Let ty v) = enclose lparen rparen . group . align . hang 2 $

1742+ vsep [text "Let", pprintRaw bound ty, pprintRaw bound v]

1743+ ppb (NLet ty v) = enclose lparen rparen . group . align . hang 2 $

1744+ vsep [text "NLet", pprintRaw bound ty, pprintRaw bound v]

1745+ ppb (Hole ty) = enclose lparen rparen . group . align . hang 2 $

1746+ text "Hole" <$> pprintRaw bound ty

1747+ ppb (GHole _ ty) = enclose lparen rparen . group . align . hang 2 $

1748+ text "GHole" <$> pprintRaw bound ty

1749+ ppb (Guess ty v) = enclose lparen rparen . group . align . hang 2 $

1750+ vsep [text "Guess", pprintRaw bound ty, pprintRaw bound v]

1751+ ppb (PVar ty) = enclose lparen rparen . group . align . hang 2 $

1752+ text "PVar" <$> pprintRaw bound ty

1753+ ppb (PVTy ty) = enclose lparen rparen . group . align . hang 2 $

1754+ text "PVTy" <$> pprintRaw bound ty

1755+pprintRaw bound (RApp f x) =

1756+ enclose lparen rparen . group . align . hang 2 . vsep $

1757+ [text "RApp", pprintRaw bound f, pprintRaw bound x]

1758+pprintRaw bound RType = text "RType"

1759+pprintRaw bound (RUType u) = enclose lparen rparen . group . align . hang 2 $

1760+ text "RUType" <$> text (show u)

1761+pprintRaw bound (RForce r) =

1762+ enclose lparen rparen . group . align . hang 2 $

1763+ vsep [text "RForce", pprintRaw bound r]

1764+pprintRaw bound (RConstant c) =

1765+ enclose lparen rparen . group . align . hang 2 $

1766+ vsep [text "RConstant", annotate (AnnConst c) (text (show c))]

17181767

17191768-- | Pretty-printer helper for the binding site of a name

17201769bindingOf :: Name -- ^^ the bound name

src/Idris/DeepSeq.hs−6

@@ -310,12 +310,6 @@ instance (NFData t) => NFData (PTactic' t) where

310310 rnf SourceFC = ()

311311 rnf Unfocus = ()

312312

313−instance NFData ErrorReportPart where

314− rnf (TermPart x1) = rnf x1 `seq` ()

315− rnf (TextPart x1) = rnf x1 `seq` ()

316− rnf (NamePart x1) = rnf x1 `seq` ()

317− rnf (SubReport x1) = rnf x1 `seq` ()

318−

319313instance (NFData t) => NFData (PDo' t) where

320314 rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

321315 rnf (DoBind x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

src/Idris/Delaborate.hs+9−7

@@ -376,23 +376,18 @@ pprintErr' i (ElaboratingArg f x _ e)

376376pprintErr' i (ProviderError msg) = text ("Type provider error: " ++ msg)

377377pprintErr' i (LoadingFailed fn e) = text "Loading" <+> text fn <+> text "failed:" <+> pprintErr' i e

378378pprintErr' i (ReflectionError parts orig) =

379− let parts' = map (fillSep . map showPart) parts in

379+ let parts' = map (fillSep . map (showPart i)) parts in

380380 align (fillSep parts') <>

381381 if (opt_origerr (idris_options i))

382382 then line <> line <> text "Original error:" <$> indented (pprintErr' i orig)

383383 else empty

384− where showPart :: ErrorReportPart -> Doc OutputAnnotation

385− showPart (TextPart str) = fillSep . map text . words $ str

386− showPart (NamePart n) = annName n

387− showPart (TermPart tm) = pprintTerm i (delab i tm)

388− showPart (SubReport rs) = indented . hsep . map showPart $ rs

389384pprintErr' i (ReflectionFailed msg err) =

390385 text "When attempting to perform error reflection, the following internal error occurred:" <>

391386 indented (pprintErr' i err) <>

392387 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

393388pprintErr' i (ElabScriptDebug msg tm holes) =

394389 text "Elaboration halted." <>

395− maybe empty (indented . text) msg <>

390+ indented (align . hsep $ map (showPart i) msg) <>

396391 line <> line <>

397392 text "Holes:" <>

398393 indented (vsep (map ppHole holes)) <> line <> line <>

@@ -416,6 +411,13 @@ pprintErr' i (ElabScriptStuck tm) =

416411 text "Can't run" <+> pprintTT [] tm <+> text "as an elaborator script." <$>

417412 text "Is it a stuck term?"

418413

414+showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation

415+showPart ist (TextPart str) = fillSep . map text . words $ str

416+showPart ist (NamePart n) = annName n

417+showPart ist (TermPart tm) = pprintTerm ist (delab ist tm)

418+showPart ist (RawPart tm) = pprintRaw [] tm

419+showPart ist (SubReport rs) = indented . hsep . map (showPart ist) $ rs

420+

419421-- | Make sure the machine invented names are shown helpfully to the user, so

420422-- that any names which differ internally also differ visibly

421423renameMNs :: Term -> Term -> (Term, Term, [Name])

src/Idris/Elab/Term.hs+3−5

@@ -1970,11 +1970,9 @@ runTactical ist fc env tm = do tm' <- eval tm

19701970 rawPair (Var $ reflm "TT", Var $ reflm "TT")

19711971 (tm', ty')

19721972 | n == tacN "prim__Debug", [ty, msg] <- args

1973− = do let msg' = fromTTMaybe msg

1974− case msg' of

1975− Nothing -> debugElaborator Nothing

1976− Just (Constant (Str m)) -> debugElaborator (Just m)

1977− Just x -> lift . tfail . InternalMsg $ "Can't reify message for debugging: " ++ show x

1973+ = do msg' <- eval msg

1974+ parts <- reifyReportParts msg

1975+ debugElaborator parts

19781976 runTacTm x = lift . tfail $ ElabScriptStuck x

19791977

19801978-- Running tactics directly

src/Idris/IBC.hs+1−1

@@ -41,7 +41,7 @@ import Codec.Archive.Zip

4141import Util.Zlib (decompressEither)

4242

4343ibcVersion :: Word16

44−ibcVersion = 110

44+ibcVersion = 111

4545

4646data IBCFile = IBCFile { ver :: Word16,

4747 sourcefile :: FilePath,

src/Idris/Reflection.hs+8

@@ -913,6 +913,14 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

913913 show tm ++

914914 " when reflecting an error:" ++ show e

915915 OK (tm', _) -> Right $ TermPart tm'

916+reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

917+ | n == reflm "RawPart" =

918+ case runElab initEState (reifyRaw tm) (initElaborator NErased initContext emptyContext Erased) of

919+ Error e -> Left . InternalMsg $

920+ "could not reify reflected raw term " ++

921+ show tm ++

922+ " when reflecting an error: " ++ show e

923+ OK (tm', _) -> Right $ RawPart tm'

916924reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

917925 | n == reflm "SubReport" =

918926 case unList tm of