29046cc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Print core definitions

29046ccDavid Christiansen10 years ago

src/Idris/Core/TT.hs+21−4

compare with master

unifiedsplit

@@ -42,8 +42,8 @@ module Idris.Core.TT(

42 , intTyName, isInjective, isTypeConst, lookupCtxt

43 , lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth

44 , nextName, noOccurrence, nsroot, occurrences

45− , pEraseType, pmap, pprintRaw, pprintTT, prettyEnv, psubst, pToV

45+ , pEraseType, pmap, pprintRaw, pprintTT, pprintTTClause, prettyEnv, psubst

46− , pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget

46+ , pToV, pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget

47 , safeForgetEnv, showCG, showEnv, showEnvDbg, showSep

48 , sInstanceN, sMN, sNS, spanFC, str, subst, substNames, substTerm

49 , substV, sUN, tcname, termSmallerThan, tfail, thead, tnull

@@ -54,8 +54,8 @@ module Idris.Core.TT(

54-- Work around AMP without CPP

55import Prelude (Eq(..), Show(..), Ord(..), Functor(..), Monad(..), String, Int,

56 Integer, Ordering(..), Maybe(..), Num(..), Bool(..), Enum(..),

57− Read(..), FilePath, Double, (&&), (||), ($), (.), div, error, fst,

57+ Read(..), FilePath, Double, (&&), (||), ($), (.), div, error, flip,

58− snd, not, mod, read, otherwise)

58+ fst, snd, not, mod, read, otherwise)

60import Control.Applicative (Applicative (..), Alternative)

61import qualified Control.Applicative as A (Alternative (..))

@@ -1811,6 +1811,23 @@ pprintTT bound tm = pp startPrec bound tm

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

1812 | otherwise = doc

1813

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+

1814-- | Pretty-print a raw term.

1831-- | Pretty-print a raw term.

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

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

1816 -> Raw -- ^ The term to pretty-print

1833 -> Raw -- ^ The term to pretty-print

src/Idris/REPL.hs+27−10

@@ -1021,8 +1021,16 @@ process fn (Check t)

1021 (pprintDelab ist ty')

1022

1023process fn (Core t)

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 =

1024− = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t

1032+ do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t

1025− iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)

1033+ iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)

1026

1034

1027process fn (DocStr (Left n) w)

1035process fn (DocStr (Left n) w)

1028 | UN ty <- n, ty == T.pack "Type" = getIState >>= iRenderResult . pprintTypeDoc

1036 | UN ty <- n, ty == T.pack "Type" = getIState >>= iRenderResult . pprintTypeDoc

@@ -1415,7 +1423,7 @@ process fn (MakeDoc s) =

1415 case result of Right _ -> iputStrLn "IdrisDoc generated"

1423 case result of Right _ -> iputStrLn "IdrisDoc generated"

1416 Left err -> iPrintError err

1424 Left err -> iPrintError err

1417process fn (PrintDef n) =

1425process fn (PrintDef n) =

1418− do result <- pprintDef n

1426+ do result <- pprintDef False n

1419 case result of

1427 case result of

1420 [] -> iPrintError "Not found"

1428 [] -> iPrintError "Not found"

1421 outs -> iRenderResult . vsep $ outs

1429 outs -> iRenderResult . vsep $ outs

@@ -1442,7 +1450,7 @@ process fn (TransformInfo n)

1442-- showTrans i ts

1450-- showTrans i ts

1443

1451

1444process fn (PPrint fmt width (PRef _ _ n))

1452process fn (PPrint fmt width (PRef _ _ n))

1445− = do outs <- pprintDef n

1453+ = do outs <- pprintDef False n

1446 iPrintResult =<< renderExternal fmt width (vsep outs)

1454 iPrintResult =<< renderExternal fmt width (vsep outs)

1447

1455

1448

1456

@@ -1486,17 +1494,26 @@ displayHelp = let vstr = showVersion getIdrisVersionNoGit in

1486 l ++ take (c1 - length l) (repeat ' ') ++

1494 l ++ take (c1 - length l) (repeat ' ') ++

1487 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

1495 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

1488

1496

1489−pprintDef :: Name -> Idris [Doc OutputAnnotation]

1497+pprintDef :: Bool -> Name -> Idris [Doc OutputAnnotation]

1490−pprintDef n =

1498+pprintDef asCore n =

1491 do ist <- getIState

1499 do ist <- getIState

1492 ctxt <- getContext

1500 ctxt <- getContext

1493 let ambiguous = length (lookupNames n ctxt) > 1

1501 let ambiguous = length (lookupNames n ctxt) > 1

1494 patdefs = idris_patdefs ist

1502 patdefs = idris_patdefs ist

1495 tyinfo = idris_datatypes ist

1503 tyinfo = idris_datatypes ist

1504+ if asCore

1505+ then return $ map (ppCoreDef ist) (lookupCtxtName n patdefs)

1496− return $ map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++

1506+ else return $ map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++

1497− map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++

1507+ map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++

1498− map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))

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)

1499− where ppDef :: Bool -> IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation

1516+ ppDef :: Bool -> IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation

1500 ppDef amb ist (n, (clauses, missing)) =

1517 ppDef amb ist (n, (clauses, missing)) =

1501 prettyName True amb [] n <+> colon <+>

1518 prettyName True amb [] n <+> colon <+>

1502 align (pprintDelabTy ist n) <$>

1519 align (pprintDelabTy ist n) <$>