git.iko.soy/Idris-dev
on master help sign in
Add :core to the REPL
75f6c2dDavid Raymond Christiansen
CHANGELOG+2
compare with master
unifiedsplit
@@ -29,6 +29,8 @@ New in 0.9.17:
29* Type providers can have documentation strings.
29* Type providers can have documentation strings.
30* Unification errors now (where possible) contain information about provenance
30* Unification errors now (where possible) contain information about provenance
31 of a type
31 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
32
34
33New in 0.9.16:
35New in 0.9.16:
34--------------
36--------------
src/Idris/AbsSyntaxTree.hs+1
@@ -347,6 +347,7 @@ data Command = Quit
347 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
347 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
348 | Undefine [Name]
348 | Undefine [Name]
349 | Check PTerm
349 | Check PTerm
350+ | Core PTerm
350 | DocStr (Either Name Const) HowMuchDocs
351 | DocStr (Either Name Const) HowMuchDocs
351 | TotCheck Name
352 | TotCheck Name
352 | Reload
353 | Reload
src/Idris/Core/TT.hs+7−7
@@ -1545,12 +1545,12 @@ pprintTT bound tm = pp startPrec bound tm
1545
1545
1546 ppb p bound n (Lam ty) sc =
1546 ppb p bound n (Lam ty) sc =
1547 bracket p startPrec . group . align . hang 2 $
1547 bracket p startPrec . group . align . hang 2 $
1548− text "λ" <> bindingOf n False <+> text "." <> line <> sc
1548+ text "λ" <+> bindingOf n False <+> text "." <> line <> sc
1549 ppb p bound n (Pi _ ty k) sc =
1549 ppb p bound n (Pi _ ty k) sc =
1550 bracket p startPrec . group . align $
1550 bracket p startPrec . group . align $
1551 lparen <> (bindingOf n False) <+> colon <+>
1551 lparen <> (bindingOf n False) <+> colon <+>
1552 (group . align) (pp startPrec bound ty) <>
1552 (group . align) (pp startPrec bound ty) <>
1553− rparen <> mkArrow k <> line <> sc
1553+ rparen <+> mkArrow k <> line <> sc
1554 where mkArrow (UType UniqueType) = text "⇴"
1554 where mkArrow (UType UniqueType) = text "⇴"
1555 mkArrow (UType NullType) = text "⥛"
1555 mkArrow (UType NullType) = text "⥛"
1556 mkArrow _ = text "→"
1556 mkArrow _ = text "→"
@@ -1572,25 +1572,25 @@ pprintTT bound tm = pp startPrec bound tm
1572 (group . hang 2) (annotate AnnKeyword (text "in") <+> sc)
1572 (group . hang 2) (annotate AnnKeyword (text "in") <+> sc)
1573 ppb p bound n (Hole ty) sc =
1573 ppb p bound n (Hole ty) sc =
1574 bracket p startPrec . group . align . hang 2 $
1574 bracket p startPrec . group . align . hang 2 $
1575− text "?" <> bindingOf n False <+> text "." <> line <> sc
1575+ text "?" <+> bindingOf n False <+> text "." <> line <> sc
1576 ppb p bound n (GHole _ ty) sc =
1576 ppb p bound n (GHole _ ty) sc =
1577 bracket p startPrec . group . align . hang 2 $
1577 bracket p startPrec . group . align . hang 2 $
1578− text "¿" <> bindingOf n False <+> text "." <> line <> sc
1578+ text "¿" <+> bindingOf n False <+> text "." <> line <> sc
1579 ppb p bound n (Guess ty val) sc =
1579 ppb p bound n (Guess ty val) sc =
1580 bracket p startPrec . group . align . hang 2 $
1580 bracket p startPrec . group . align . hang 2 $
1581 text "?" <> bindingOf n False <+>
1581 text "?" <> bindingOf n False <+>
1582− text "≈" <+> pp startPrec bound val <>
1582+ text "≈" <+> pp startPrec bound val <+>
1583 text "." <> line <> sc
1583 text "." <> line <> sc
1584 ppb p bound n (PVar ty) sc =
1584 ppb p bound n (PVar ty) sc =
1585 bracket p startPrec . group . align . hang 2 $
1585 bracket p startPrec . group . align . hang 2 $
1586 annotate AnnKeyword (text "pat") <+>
1586 annotate AnnKeyword (text "pat") <+>
1587− bindingOf n False <+> colon <+> pp startPrec bound ty <>
1587+ bindingOf n False <+> colon <+> pp startPrec bound ty <+>
1588 text "." <> line <>
1588 text "." <> line <>
1589 sc
1589 sc
1590 ppb p bound n (PVTy ty) sc =
1590 ppb p bound n (PVTy ty) sc =
1591 bracket p startPrec . group . align . hang 2 $
1591 bracket p startPrec . group . align . hang 2 $
1592 annotate AnnKeyword (text "patTy") <+>
1592 annotate AnnKeyword (text "patTy") <+>
1593− bindingOf n False <+> colon <+> pp startPrec bound ty <>
1593+ bindingOf n False <+> colon <+> pp startPrec bound ty <+>
1594 text "." <> line <>
1594 text "." <> line <>
1595 sc
1595 sc
1596
1596
src/Idris/REPL.hs+5
@@ -556,6 +556,7 @@ idemodeProcess fn (Undefine n) = process fn (Undefine n)
556idemodeProcess fn (ExecVal t) = process fn (ExecVal t)
556idemodeProcess fn (ExecVal t) = process fn (ExecVal t)
557idemodeProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))
557idemodeProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))
558idemodeProcess fn (Check t) = process fn (Check t)
558idemodeProcess fn (Check t) = process fn (Check t)
559+idemodeProcess fn (Core t) = process fn (Core t)
559idemodeProcess fn (DocStr n w) = process fn (DocStr n w)
560idemodeProcess fn (DocStr n w) = process fn (DocStr n w)
560idemodeProcess fn Universes = process fn Universes
561idemodeProcess fn Universes = process fn Universes
561idemodeProcess fn (Defn n) = do process fn (Defn n)
562idemodeProcess fn (Defn n) = do process fn (Defn n)
@@ -908,6 +909,10 @@ process fn (Check t)
908 _ -> iPrintTermWithType (pprintDelab ist tm)
909 _ -> iPrintTermWithType (pprintDelab ist tm)
909 (pprintDelab ist ty)
910 (pprintDelab ist ty)
910
911
912+process fn (Core t)
913+ = do (tm, ty) <- elabVal recinfo ERHS t
914+ iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)
915+
911process fn (DocStr (Left n) w)
916process fn (DocStr (Left n) w)
912 = do ist <- getIState
917 = do ist <- getIState
913 let docs = lookupCtxtName n (idris_docstrings ist) ++
918 let docs = lookupCtxtName n (idris_docstrings ist) ++
src/Idris/REPLParser.hs+1
@@ -41,6 +41,7 @@ allHelp = [ (map (':' :) names, args, text)
41parserCommandsForHelp :: CommandTable
41parserCommandsForHelp :: CommandTable
42parserCommandsForHelp =
42parserCommandsForHelp =
43 [ exprArgCmd ["t", "type"] Check "Check the type of an expression"
43 [ exprArgCmd ["t", "type"] Check "Check the type of an expression"
44+ , exprArgCmd ["core"] Core "View the core language representation of a term"
44 , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"
45 , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"
45 , (["doc"], NameArg, "Show internal documentation", cmd_doc)
46 , (["doc"], NameArg, "Show internal documentation", cmd_doc)
46 , (["mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"
47 , (["mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"