git.iko.soy/Idris-dev
on master help sign in
Print core definitions

Now, :core NAME will show the TT definition of NAME, if NAME is a pattern-matching definition.

commit29046cca62d07a319c240ac39da0823f7008d098 authorDavid Christiansen <david@davidchristiansen.dk> dateMon 29 Aug 2016, 17:59 (10 years ago) parent7da4cf2
2 files changed+48−14
compare with master
unifiedsplit
src/Idris/Core/TT.hs+21−4 src/Idris/REPL.hs+27−10
src/Idris/Core/TT.hs+21−4
@@ -42,8 +42,8 @@ module Idris.Core.TT(
4242 , intTyName, isInjective, isTypeConst, lookupCtxt
4343 , lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth
4444 , nextName, noOccurrence, nsroot, occurrences
45− , pEraseType, pmap, pprintRaw, pprintTT, prettyEnv, psubst, pToV
46− , pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget
45+ , pEraseType, pmap, pprintRaw, pprintTT, pprintTTClause, prettyEnv, psubst
46+ , pToV, pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget
4747 , safeForgetEnv, showCG, showEnv, showEnvDbg, showSep
4848 , sInstanceN, sMN, sNS, spanFC, str, subst, substNames, substTerm
4949 , substV, sUN, tcname, termSmallerThan, tfail, thead, tnull
@@ -54,8 +54,8 @@ module Idris.Core.TT(
5454-- Work around AMP without CPP
5555import Prelude (Eq(..), Show(..), Ord(..), Functor(..), Monad(..), String, Int,
5656 Integer, Ordering(..), Maybe(..), Num(..), Bool(..), Enum(..),
57− Read(..), FilePath, Double, (&&), (||), ($), (.), div, error, fst,
58− snd, not, mod, read, otherwise)
57+ Read(..), FilePath, Double, (&&), (||), ($), (.), div, error, flip,
58+ fst, snd, not, mod, read, otherwise)
5959
6060import Control.Applicative (Applicative (..), Alternative)
6161import qualified Control.Applicative as A (Alternative (..))
@@ -1811,6 +1811,23 @@ pprintTT bound tm = pp startPrec bound tm
18111811 | outer > inner = lparen <> doc <> rparen
18121812 | otherwise = doc
18131813
1814+pprintTTClause :: [(Name, Type)] -> Term -> Term -> Doc OutputAnnotation
1815+pprintTTClause pvars lhs rhs =
1816+ vars pvars . group . align $
1817+ pprintTT (map fst pvars) lhs <$>
1818+ text "↦" <$>
1819+ (pprintTT (map fst pvars) rhs)
1820+ where vars [] terms = terms
1821+ vars (v:vs) terms =
1822+ annotate AnnKeyword (text "var") <+>
1823+ group (align (sep (punctuate comma (reverse (bindVars [] (v:vs)))))) <+>
1824+ annotate AnnKeyword (text ".") <$>
1825+ indent 2 terms
1826+ bindVars _ [] = []
1827+ bindVars ns ((n, ty):vs) =
1828+ bindingOf n False <+> colon <+> pprintTT ns ty : bindVars (n:ns) vs
1829+
1830+
18141831-- | Pretty-print a raw term.
18151832pprintRaw :: [Name] -- ^ Bound names, for highlighting
18161833 -> Raw -- ^ The term to pretty-print
src/Idris/REPL.hs+27−10
@@ -1021,8 +1021,16 @@ process fn (Check t)
10211021 (pprintDelab ist ty')
10221022
10231023process fn (Core t)
1024− = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t
1025− iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)
1024+ = case t of
1025+ PRef _ _ n ->
1026+ do ist <- getIState
1027+ case lookupDef n (tt_ctxt ist) of
1028+ [CaseOp _ _ _ _ _ _] -> pprintDef True n >>= iRenderResult . vsep
1029+ _ -> coreTerm t
1030+ t -> coreTerm t
1031+ where coreTerm t =
1032+ do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t
1033+ iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)
10261034
10271035process fn (DocStr (Left n) w)
10281036 | UN ty <- n, ty == T.pack "Type" = getIState >>= iRenderResult . pprintTypeDoc
@@ -1415,7 +1423,7 @@ process fn (MakeDoc s) =
14151423 case result of Right _ -> iputStrLn "IdrisDoc generated"
14161424 Left err -> iPrintError err
14171425process fn (PrintDef n) =
1418− do result <- pprintDef n
1426+ do result <- pprintDef False n
14191427 case result of
14201428 [] -> iPrintError "Not found"
14211429 outs -> iRenderResult . vsep $ outs
@@ -1442,7 +1450,7 @@ process fn (TransformInfo n)
14421450-- showTrans i ts
14431451
14441452process fn (PPrint fmt width (PRef _ _ n))
1445− = do outs <- pprintDef n
1453+ = do outs <- pprintDef False n
14461454 iPrintResult =<< renderExternal fmt width (vsep outs)
14471455
14481456
@@ -1486,17 +1494,26 @@ displayHelp = let vstr = showVersion getIdrisVersionNoGit in
14861494 l ++ take (c1 - length l) (repeat ' ') ++
14871495 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
14881496
1489−pprintDef :: Name -> Idris [Doc OutputAnnotation]
1490−pprintDef n =
1497+pprintDef :: Bool -> Name -> Idris [Doc OutputAnnotation]
1498+pprintDef asCore n =
14911499 do ist <- getIState
14921500 ctxt <- getContext
14931501 let ambiguous = length (lookupNames n ctxt) > 1
14941502 patdefs = idris_patdefs ist
14951503 tyinfo = idris_datatypes ist
1496− return $ map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++
1497− map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++
1498− map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))
1499− where ppDef :: Bool -> IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1504+ if asCore
1505+ then return $ map (ppCoreDef ist) (lookupCtxtName n patdefs)
1506+ else return $ map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++
1507+ map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++
1508+ map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))
1509+ where ppCoreDef :: IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1510+ ppCoreDef ist (n, (clauses, missing)) =
1511+ case lookupTy n (tt_ctxt ist) of
1512+ [] -> error "Attempted pprintDef of TT of thing that doesn't exist"
1513+ (ty:_) -> prettyName True True [] n <+> colon <+>
1514+ align (annotate (AnnTerm [] ty) (pprintTT [] ty)) <$>
1515+ vsep (map (\(vars, lhs, rhs) -> pprintTTClause vars lhs rhs) clauses)
1516+ ppDef :: Bool -> IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation
15001517 ppDef amb ist (n, (clauses, missing)) =
15011518 prettyName True amb [] n <+> colon <+>
15021519 align (pprintDelabTy ist n) <$>