git.iko.soy/Idris-dev
on master help sign in
Add :core to the REPL

:core TM shows the elaborated value and type of TM

commit75f6c2dc1413425356487b4ab25beebeb2efbf73 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 16 Mar 2015, 20:03 (12 years ago) parentbb013f0
5 files changed+16−7
compare with master
unifiedsplit
CHANGELOG+2 src/Idris/AbsSyntaxTree.hs+1 src/Idris/Core/TT.hs+7−7 src/Idris/REPL.hs+5 src/Idris/REPLParser.hs+1
CHANGELOG+2
@@ -29,6 +29,8 @@ New in 0.9.17:
2929* Type providers can have documentation strings.
3030* Unification errors now (where possible) contain information about provenance
3131 of a type
32+* New REPL command ":core TM" that shows the elaborated form of TM along with
33+ its elaborated type using the syntax of TT
3234
3335New in 0.9.16:
3436--------------
src/Idris/AbsSyntaxTree.hs+1
@@ -347,6 +347,7 @@ data Command = Quit
347347 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
348348 | Undefine [Name]
349349 | Check PTerm
350+ | Core PTerm
350351 | DocStr (Either Name Const) HowMuchDocs
351352 | TotCheck Name
352353 | Reload
src/Idris/Core/TT.hs+7−7
@@ -1545,12 +1545,12 @@ pprintTT bound tm = pp startPrec bound tm
15451545
15461546 ppb p bound n (Lam ty) sc =
15471547 bracket p startPrec . group . align . hang 2 $
1548− text "λ" <> bindingOf n False <+> text "." <> line <> sc
1548+ text "λ" <+> bindingOf n False <+> text "." <> line <> sc
15491549 ppb p bound n (Pi _ ty k) sc =
15501550 bracket p startPrec . group . align $
15511551 lparen <> (bindingOf n False) <+> colon <+>
15521552 (group . align) (pp startPrec bound ty) <>
1553− rparen <> mkArrow k <> line <> sc
1553+ rparen <+> mkArrow k <> line <> sc
15541554 where mkArrow (UType UniqueType) = text "⇴"
15551555 mkArrow (UType NullType) = text "⥛"
15561556 mkArrow _ = text "→"
@@ -1572,25 +1572,25 @@ pprintTT bound tm = pp startPrec bound tm
15721572 (group . hang 2) (annotate AnnKeyword (text "in") <+> sc)
15731573 ppb p bound n (Hole ty) sc =
15741574 bracket p startPrec . group . align . hang 2 $
1575− text "?" <> bindingOf n False <+> text "." <> line <> sc
1575+ text "?" <+> bindingOf n False <+> text "." <> line <> sc
15761576 ppb p bound n (GHole _ ty) sc =
15771577 bracket p startPrec . group . align . hang 2 $
1578− text "¿" <> bindingOf n False <+> text "." <> line <> sc
1578+ text "¿" <+> bindingOf n False <+> text "." <> line <> sc
15791579 ppb p bound n (Guess ty val) sc =
15801580 bracket p startPrec . group . align . hang 2 $
15811581 text "?" <> bindingOf n False <+>
1582− text "≈" <+> pp startPrec bound val <>
1582+ text "≈" <+> pp startPrec bound val <+>
15831583 text "." <> line <> sc
15841584 ppb p bound n (PVar ty) sc =
15851585 bracket p startPrec . group . align . hang 2 $
15861586 annotate AnnKeyword (text "pat") <+>
1587− bindingOf n False <+> colon <+> pp startPrec bound ty <>
1587+ bindingOf n False <+> colon <+> pp startPrec bound ty <+>
15881588 text "." <> line <>
15891589 sc
15901590 ppb p bound n (PVTy ty) sc =
15911591 bracket p startPrec . group . align . hang 2 $
15921592 annotate AnnKeyword (text "patTy") <+>
1593− bindingOf n False <+> colon <+> pp startPrec bound ty <>
1593+ bindingOf n False <+> colon <+> pp startPrec bound ty <+>
15941594 text "." <> line <>
15951595 sc
15961596
src/Idris/REPL.hs+5
@@ -556,6 +556,7 @@ idemodeProcess fn (Undefine n) = process fn (Undefine n)
556556idemodeProcess fn (ExecVal t) = process fn (ExecVal t)
557557idemodeProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))
558558idemodeProcess fn (Check t) = process fn (Check t)
559+idemodeProcess fn (Core t) = process fn (Core t)
559560idemodeProcess fn (DocStr n w) = process fn (DocStr n w)
560561idemodeProcess fn Universes = process fn Universes
561562idemodeProcess fn (Defn n) = do process fn (Defn n)
@@ -908,6 +909,10 @@ process fn (Check t)
908909 _ -> iPrintTermWithType (pprintDelab ist tm)
909910 (pprintDelab ist ty)
910911
912+process fn (Core t)
913+ = do (tm, ty) <- elabVal recinfo ERHS t
914+ iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)
915+
911916process fn (DocStr (Left n) w)
912917 = do ist <- getIState
913918 let docs = lookupCtxtName n (idris_docstrings ist) ++
src/Idris/REPLParser.hs+1
@@ -41,6 +41,7 @@ allHelp = [ (map (':' :) names, args, text)
4141parserCommandsForHelp :: CommandTable
4242parserCommandsForHelp =
4343 [ exprArgCmd ["t", "type"] Check "Check the type of an expression"
44+ , exprArgCmd ["core"] Core "View the core language representation of a term"
4445 , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"
4546 , (["doc"], NameArg, "Show internal documentation", cmd_doc)
4647 , (["mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"