1e36589 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #801 from david-christiansen/semantic-pprint

1e36589Edwin Brady13 years ago

idris.cabal+2

compare with master

unifiedsplit

@@ -434,6 +434,7 @@ Library

434

435 Build-depends: base >=4 && <5

436 , Cabal

437+ , annotated-wl-pprint >= 0.5.3

437 , ansi-terminal

438 , ansi-terminal

438 , ansi-wl-pprint

439 , ansi-wl-pprint

439 , binary

440 , binary

@@ -463,6 +464,7 @@ Library

463 , zlib

464 , zlib

464 Extensions: MultiParamTypeClasses

465 Extensions: MultiParamTypeClasses

465 , FunctionalDependencies

466 , FunctionalDependencies

467+ , FlexibleContexts

466 , FlexibleInstances

468 , FlexibleInstances

467 , TemplateHaskell

469 , TemplateHaskell

468

470

src/Idris/AbsSyntax.hs+56−89

@@ -397,6 +397,55 @@ ihPrintResult h s = do i <- getIState

397 let good = SexpList [SymbolAtom "ok", toSExp s] in

398 runIO $ hPutStrLn h $ convSExp "return" good n

399

400+-- | Write a pretty-printed term to the console with semantic coloring

401+consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

402+consoleDisplayAnnotated h output = do ist <- getIState

403+ runIO . hPutStrLn h .

404+ displayDecorated (consoleDecorate ist) .

405+ renderCompact $ output

406+

407+-- | Write pretty-printed output to IDESlave with semantic annotations

408+ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

409+ideSlaveReturnAnnotated n h out = do ist <- getIState

410+ let (str, spans) = displaySpans .

411+ renderCompact .

412+ fmap (fancifyAnnots ist) $

413+ out

414+ good = [SymbolAtom "ok", toSExp str, toSExp spans]

415+ runIO . hPutStrLn h $ convSExp "return" good n

416+

417+ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

418+ihPrintTermWithType h tm ty = do ist <- getIState

419+ let output = tm <+> colon <+> ty

420+ case idris_outputmode ist of

421+ RawOutput -> consoleDisplayAnnotated h output

422+ IdeSlave n -> ideSlaveReturnAnnotated n h output

423+

424+-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

425+ihPrintFunTypes :: Handle -> Name -> [(Name, PTerm)] -> Idris ()

426+ihPrintFunTypes h n [] = ihPrintError h $ "No such variable " ++ show n

427+ihPrintFunTypes h n overloads = do imp <- impShow

428+ ist <- getIState

429+ let output = vsep (map (uncurry (ppOverload imp)) overloads)

430+ case idris_outputmode ist of

431+ RawOutput -> consoleDisplayAnnotated h output

432+ IdeSlave n -> ideSlaveReturnAnnotated n h output

433+ where fullName n = annotate (AnnName n Nothing Nothing) $ text (show n)

434+ ppOverload imp n tm = fullName n <+> colon <+> prettyImp imp tm

435+

436+fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

437+fancifyAnnots ist annot@(AnnName n _ _) =

438+ do let ctxt = tt_ctxt ist

439+ case () of

440+ _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing

441+ _ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing

442+ _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing

443+ _ | otherwise -> annot

444+fancifyAnnots _ annot = annot

445+

446+type1Doc :: Doc OutputAnnotation

447+type1Doc = (annotate AnnConstType $ text "Type 1")

448+

400ihPrintError :: Handle -> String -> Idris ()

449ihPrintError :: Handle -> String -> Idris ()

401ihPrintError h s = do i <- getIState

450ihPrintError h s = do i <- getIState

402 case idris_outputmode i of

451 case idris_outputmode i of

@@ -425,11 +474,12 @@ ideslavePutSExp cmd info = do i <- getIState

425 _ -> return ()

474 _ -> return ()

426

475

427-- this needs some typing magic and more structured output towards emacs

476-- this needs some typing magic and more structured output towards emacs

428−iputGoal :: String -> Idris ()

477+iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

429−iputGoal s = do i <- getIState

478+iputGoal g = do i <- getIState

430 case idris_outputmode i of

479 case idris_outputmode i of

431− RawOutput -> runIO $ putStrLn s

480+ RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)

432− IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n

481+ IdeSlave n -> runIO . putStrLn $

482+ convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n

433

483

434isetPrompt :: String -> Idris ()

484isetPrompt :: String -> Idris ()

435isetPrompt p = do i <- getIState

485isetPrompt p = do i <- getIState

@@ -692,90 +742,6 @@ setTypeCase t = do i <- getIState

692 putIState $ i { idris_options = opt' }

742 putIState $ i { idris_options = opt' }

693

743

694

744

695−-- For inferring types of things

696−

697−bi = fileFC "builtin"

698−

699−inferTy = sMN 0 "__Infer"

700−inferCon = sMN 0 "__infer"

701−inferDecl = PDatadecl inferTy

702− PType

703− [("", inferCon, PPi impl (sMN 0 "iType") PType (

704− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

705− (PRef bi inferTy)), bi, [])]

706−inferOpts = []

707−

708−infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

709−infP = P (TCon 6 0) inferTy (TType (UVal 0))

710−

711−getInferTerm, getInferType :: Term -> Term

712−getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

713−getInferTerm (App (App _ _) tm) = tm

714−getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

715−

716−getInferType (Bind n b sc) = Bind n b $ getInferType sc

717−getInferType (App (App _ ty) _) = ty

718−

719−-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class

720−

721−primNames = [unitTy, unitCon,

722− falseTy, pairTy, pairCon,

723− eqTy, eqCon, inferTy, inferCon]

724−

725−unitTy = sMN 0 "__Unit"

726−unitCon = sMN 0 "__II"

727−unitDecl = PDatadecl unitTy PType

728− [("", unitCon, PRef bi unitTy, bi, [])]

729−unitOpts = [DefaultEliminator]

730−

731−falseTy = sMN 0 "__False"

732−falseDecl = PDatadecl falseTy PType []

733−falseOpts = []

734−

735−pairTy = sMN 0 "__Pair"

736−pairCon = sMN 0 "__MkPair"

737−pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

738− [("", pairCon, PPi impl (n "A") PType (

739− PPi impl (n "B") PType (

740− PPi expl (n "a") (PRef bi (n "A")) (

741− PPi expl (n "b") (PRef bi (n "B"))

742− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

743− pexp (PRef bi (n "B"))])))), bi, [])]

744− where n a = sMN 0 a

745−pairOpts = []

746−

747−eqTy = sUN "="

748−eqCon = sUN "refl"

749−eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

750− (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

751− PType)

752− [("", eqCon, PPi impl (n "A") PType (

753− PPi impl (n "x") (PRef bi (n "A"))

754− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

755− pimp (n "B") Placeholder False,

756− pexp (PRef bi (n "x")),

757− pexp (PRef bi (n "x"))])), bi, [])]

758− where n a = sMN 0 a

759−eqOpts = []

760−

761−elimName = sUN "__Elim"

762−elimMethElimTy = sUN "__elimTy"

763−elimMethElim = sUN "elim"

764−elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

765− [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,

766− PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

767−

768−-- Defined in builtins.idr

769−sigmaTy = sUN "Exists"

770−existsCon = sUN "Ex_intro"

771−

772−piBind :: [(Name, PTerm)] -> PTerm -> PTerm

773−piBind = piBindp expl

774−

775−piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm

776−piBindp p [] t = t

777−piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)

778−

779-- Dealing with parameters

745-- Dealing with parameters

780

746

781expandParams :: (Name -> Name) -> [(Name, PTerm)] ->

747expandParams :: (Name -> Name) -> [(Name, PTerm)] ->

@@ -1442,7 +1408,7 @@ mkPApp fc a f as = let rest = drop a as in

1442-- FIXME: It's possible that this really has to happen after elaboration

1408-- FIXME: It's possible that this really has to happen after elaboration

1443

1409

1444findStatics :: IState -> PTerm -> (PTerm, [Bool])

1410findStatics :: IState -> PTerm -> (PTerm, [Bool])

1445−findStatics ist tm = trace (showImp Nothing True False tm) $

1411+findStatics ist tm = trace (show tm) $

1446 let (ns, ss) = fs tm in

1412 let (ns, ss) = fs tm in

1447 runState (pos ns ss tm) []

1413 runState (pos ns ss tm) []

1448 where fs (PPi p n t sc)

1414 where fs (PPi p n t sc)

@@ -1726,3 +1692,4 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

1726 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

1692 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

1727 mkUniq t = return t

1693 mkUniq t = return t

1728

1694

1695+

src/Idris/AbsSyntaxTree.hs+361−351

@@ -30,6 +30,8 @@ import Data.Word (Word)

31import Debug.Trace

33+import Text.PrettyPrint.Annotated.Leijen

34+

33data IOption = IOption { opt_logLevel :: Int,

35data IOption = IOption { opt_logLevel :: Int,

34 opt_typecase :: Bool,

36 opt_typecase :: Bool,

35 opt_typeintype :: Bool,

37 opt_typeintype :: Bool,

@@ -908,275 +910,440 @@ expandNS syn n = case syn_namespace syn of

908 xs -> sNS n xs

910 xs -> sNS n xs

909

911

910

912

911−--- Pretty printing declarations and terms

913+-- For inferring types of things

912

914

913−instance Show PTerm where

915+bi = fileFC "builtin"

914− show tm = showImp Nothing False False tm

915

916

916−instance Pretty PTerm where

917+inferTy = sMN 0 "__Infer"

917− pretty = prettyImp False

918+inferCon = sMN 0 "__infer"

919+inferDecl = PDatadecl inferTy

920+ PType

921+ [("", inferCon, PPi impl (sMN 0 "iType") PType (

922+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

923+ (PRef bi inferTy)), bi, [])]

924+inferOpts = []

918

925

919−instance Show PDecl where

926+infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

920− show d = showDeclImp False d

927+infP = P (TCon 6 0) inferTy (TType (UVal 0))

921

928

922−instance Show PClause where

929+getInferTerm, getInferType :: Term -> Term

923− show c = showCImp True c

930+getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

931+getInferTerm (App (App _ _) tm) = tm

932+getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

924

933

925−instance Show PData where

934+getInferType (Bind n b sc) = Bind n b $ getInferType sc

926− show d = showDImp False d

935+getInferType (App (App _ ty) _) = ty

927

936

928−showDecls :: Bool -> [PDecl] -> String

929−showDecls _ [] = ""

930−showDecls i (d:ds) = showDeclImp i d ++ "\n" ++ showDecls i ds

931

937

932−showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

933−showDeclImp i (PTy _ _ _ _ n t) = "tydecl " ++ showCG n ++ " : " ++ showImp Nothing i False t

934−showDeclImp i (PClauses _ _ n cs) = "pat " ++ showCG n ++ "\t" ++ showSep "\n\t" (map (showCImp i) cs)

935−showDeclImp _ (PData _ _ _ _ d) = showDImp True d

936−showDeclImp i (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ showDecls i ps ++ "}\n"

937−showDeclImp i (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ showDecls i ps ++ "}\n"

938−showDeclImp _ (PSyntax _ syn) = "syntax " ++ show syn

939−showDeclImp i (PClass _ _ _ cs n ps ds)

940− = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ showDecls i ds

941−showDeclImp i (PInstance _ _ cs n _ t _ ds)

942− = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ showDecls i ds

943−showDeclImp _ _ = "..."

944−-- showDeclImp (PImport i) = "import " ++ i

945

938

939+-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class

946

940

947−showCImp :: Bool -> PClause -> String

941+primNames = [unitTy, unitCon,

948−showCImp impl (PClause _ n l ws r w)

942+ falseTy, pairTy, pairCon,

949− = showImp Nothing impl False l ++ showWs ws ++ " = " ++ showImp Nothing impl False r

943+ eqTy, eqCon, inferTy, inferCon]

950− ++ " where " ++ show w

951− where

952− showWs [] = ""

953− showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs

954−showCImp impl (PWith _ n l ws r w)

955− = showImp Nothing impl False l ++ showWs ws ++ " with " ++ showImp Nothing impl False r

956− ++ " { " ++ show w ++ " } "

957− where

958− showWs [] = ""

959− showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs

960

944

945+unitTy = sMN 0 "__Unit"

946+unitCon = sMN 0 "__II"

947+unitDecl = PDatadecl unitTy PType

948+ [("", unitCon, PRef bi unitTy, bi, [])]

949+unitOpts = [DefaultEliminator]

961

950

962−showDImp :: Bool -> PData -> String

951+falseTy = sMN 0 "__False"

963−showDImp impl (PDatadecl n ty cons)

952+falseDecl = PDatadecl falseTy PType []

964− = "data " ++ show n ++ " : " ++ showImp Nothing impl False ty ++ " where\n\t"

953+falseOpts = []

965− ++ showSep "\n\t| "

966− (map (\ (_, n, t, _, _) -> show n ++ " : " ++ showImp Nothing impl False t) cons)

967

954

968−getImps :: [PArg] -> [(Name, PTerm)]

955+pairTy = sMN 0 "__Pair"

969−getImps [] = []

956+pairCon = sMN 0 "__MkPair"

970−getImps (PImp _ _ _ n tm _ : xs) = (n, tm) : getImps xs

957+pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

971−getImps (_ : xs) = getImps xs

958+ [("", pairCon, PPi impl (n "A") PType (

959+ PPi impl (n "B") PType (

960+ PPi expl (n "a") (PRef bi (n "A")) (

961+ PPi expl (n "b") (PRef bi (n "B"))

962+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

963+ pexp (PRef bi (n "B"))])))), bi, [])]

964+ where n a = sMN 0 a

965+pairOpts = []

972

966

973−getExps :: [PArg] -> [PTerm]

967+eqTy = sUN "="

974−getExps [] = []

968+eqCon = sUN "refl"

975−getExps (PExp _ _ tm _ : xs) = tm : getExps xs

969+eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

976−getExps (_ : xs) = getExps xs

970+ (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

971+ PType)

972+ [("", eqCon, PPi impl (n "A") PType (

973+ PPi impl (n "x") (PRef bi (n "A"))

974+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

975+ pimp (n "B") Placeholder False,

976+ pexp (PRef bi (n "x")),

977+ pexp (PRef bi (n "x"))])), bi, [])]

978+ where n a = sMN 0 a

979+eqOpts = []

977

980

978−getConsts :: [PArg] -> [PTerm]

981+elimName = sUN "__Elim"

979−getConsts [] = []

982+elimMethElimTy = sUN "__elimTy"

980−getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs

983+elimMethElim = sUN "elim"

981−getConsts (_ : xs) = getConsts xs

984+elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

985+ [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,

986+ PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

987+

988+-- Defined in builtins.idr

989+sigmaTy = sUN "Exists"

990+existsCon = sUN "Ex_intro"

991+

992+piBind :: [(Name, PTerm)] -> PTerm -> PTerm

993+piBind = piBindp expl

994+

995+piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm

996+piBindp p [] t = t

997+piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)

982

998

983−getAll :: [PArg] -> [PTerm]

984−getAll = map getTm

985

999

1000+-- Pretty-printing declarations and terms

1001+

1002+instance Show PTerm where

1003+ showsPrec _ tm = (displayS . renderCompact . prettyImp False) tm

1004+

1005+instance Show PDecl where

1006+ showsPrec _ d = (displayS . renderCompact . showDeclImp False) d

1007+

1008+instance Show PClause where

1009+ showsPrec _ c = (displayS . renderCompact . showCImp True) c

1010+

1011+instance Show PData where

1012+ showsPrec _ d = (displayS . renderCompact . showDImp False) d

1013+

1014+instance Pretty PTerm OutputAnnotation where

1015+ pretty = prettyImp False

1016+

1017+-- | Colourise annotations according to an Idris state. It ignores the names

1018+-- in the annotation, as there's no good way to show extended information on a

1019+-- terminal.

1020+consoleDecorate :: IState -> OutputAnnotation -> String -> String

1021+consoleDecorate ist _ | not (idris_colourRepl ist) = id

1022+consoleDecorate ist AnnConstData = let theme = idris_colourTheme ist

1023+ in colouriseData theme

1024+consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist

1025+ in colouriseType theme

1026+consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)

1027+consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)

1028+consoleDecorate ist (AnnName n _ _) = let ctxt = tt_ctxt ist

1029+ theme = idris_colourTheme ist

1030+ in case () of

1031+ _ | isDConName n ctxt -> colouriseData theme

1032+ _ | isFnName n ctxt -> colouriseFun theme

1033+ _ | isTConName n ctxt -> colouriseType theme

1034+ _ | otherwise -> id -- don't colourise unknown names

1035+consoleDecorate ist (AnnFC _) = id

1036+

986−-- | Pretty-print a high-level Idris term

1037+-- | Pretty-print a high-level closed Idris term

987prettyImp :: Bool -- ^^ whether to show implicits

1038prettyImp :: Bool -- ^^ whether to show implicits

988 -> PTerm -- ^^ the term to pretty-print

1039 -> PTerm -- ^^ the term to pretty-print

989− -> Doc

1040+ -> Doc OutputAnnotation

990−prettyImp impl = prettySe 10

1041+prettyImp impl = pprintPTerm impl []

1042+

1043+-- | Pretty-print a high-level Idris term in some bindings context

1044+pprintPTerm :: Bool -- ^^ whether to show implicits

1045+ -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

1046+ -> PTerm -- ^^ the term to pretty-print

1047+ -> Doc OutputAnnotation

1048+pprintPTerm impl bnd = prettySe 10 bnd

991 where

1049 where

1050+ prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

992− prettySe p (PQuote r) =

1051+ prettySe p bnd (PQuote r) =

993 if size r > breakingSize then

1052 if size r > breakingSize then

994− text "![" $$ pretty r <> text "]"

1053+ text "![" <> line <> pretty r <> text "]"

995 else

1054 else

996 text "![" <> pretty r <> text "]"

1055 text "![" <> pretty r <> text "]"

997− prettySe p (PPatvar fc n) = pretty n

1056+ prettySe p bnd (PPatvar fc n) = pretty n

998− prettySe p (PRef fc n) =

1057+ prettySe p bnd e

999− if impl then

1058+ | Just str <- slist p bnd e = str

1000− pretty n

1059+ | Just n <- snat p e = annotate AnnConstData (text (show n))

1001− else

1060+ prettySe p bnd (PRef fc n) = prettyName impl bnd n

1002− prettyBasic n

1003− where

1004− prettyBasic n@(UN _) = pretty n

1005− prettyBasic (MN _ s) = text (str s)

1006− prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map (text.str) $ reverse s))) <> prettyBasic n

1007− prettyBasic (SN sn) = text (show sn)

1008− prettySe p (PLam n ty sc) =

1061+ prettySe p bnd (PLam n ty sc) =

1009 bracket p 2 $

1062 bracket p 2 $

1010 if size sc > breakingSize then

1063 if size sc > breakingSize then

1011− text "λ" <> pretty n <+> text "=>" $+$ pretty sc

1064+ text "\\" <> bindingOf n False <+> text "=>" <> line <> prettySe 10 ((n, False):bnd) sc

1012 else

1065 else

1013− text "λ" <> pretty n <+> text "=>" <+> pretty sc

1066+ text "\\" <> bindingOf n False <+> text "=>" <+> prettySe 10 ((n, False):bnd) sc

1014− prettySe p (PLet n ty v sc) =

1067+ prettySe p bnd (PLet n ty v sc) =

1015 bracket p 2 $

1068 bracket p 2 $

1016 if size sc > breakingSize then

1069 if size sc > breakingSize then

1017− text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$

1070+ text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <>

1018− nest nestingSize (prettySe 10 sc)

1071+ nest nestingSize (prettySe 10 ((n, False):bnd) sc)

1019 else

1072 else

1020− text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>

1073+ text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <+>

1021− prettySe 10 sc

1074+ prettySe 10 ((n, False):bnd) sc

1022− prettySe p (PPi (Exp l s _ _) n ty sc)

1075+ prettySe p bnd (PPi (Exp l s _ _) n ty sc)

1023 | n `elem` allNamesIn sc || impl =

1076 | n `elem` allNamesIn sc || impl =

1024 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1077 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1025 bracket p 2 $

1078 bracket p 2 $

1026 if size sc > breakingSize then

1079 if size sc > breakingSize then

1027− open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>

1080+ enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1028− st <+> text "->" $+$ prettySe 10 sc

1081+ st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc

1029 else

1082 else

1030− open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>

1083+ enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1031− st <+> text "->" <+> prettySe 10 sc

1084+ st <> text "->" <+> prettySe 10 ((n, False):bnd) sc

1032 | otherwise =

1085 | otherwise =

1033 bracket p 2 $

1086 bracket p 2 $

1034 if size sc > breakingSize then

1087 if size sc > breakingSize then

1035− prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc

1088+ prettySe 0 bnd ty <+> st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc

1036 else

1089 else

1037− prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc

1090+ prettySe 0 bnd ty <+> st <> text "->" <+> prettySe 10 ((n, False):bnd) sc

1038 where

1091 where

1039 st =

1092 st =

1040 case s of

1093 case s of

1041− Static -> text "[static]"

1094+ Static -> text "[static]" <> space

1042 _ -> empty

1095 _ -> empty

1043− prettySe p (PPi (Imp l s _ _) n ty sc)

1096+ prettySe p bnd (PPi (Imp l s _ _) n ty sc)

1044 | impl =

1097 | impl =

1045 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

1098 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

1046 bracket p 2 $

1099 bracket p 2 $

1047 if size sc > breakingSize then

1100 if size sc > breakingSize then

1048− open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>

1101+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1049− st <+> text "->" <+> prettySe 10 sc

1102+ st <> text "->" <+> prettySe 10 ((n, True):bnd) sc

1050 else

1103 else

1051− open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>

1104+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1052− st <+> text "->" <+> prettySe 10 sc

1105+ st <> text "->" <+> prettySe 10 ((n, True):bnd) sc

1053− | otherwise = prettySe 10 sc

1106+ | otherwise = prettySe 10 ((n, True):bnd) sc

1054 where

1107 where

1055 st =

1108 st =

1056 case s of

1109 case s of

1057− Static -> text $ "[static]"

1110+ Static -> text "[static]" <> space

1058 _ -> empty

1111 _ -> empty

1059− prettySe p (PPi (Constraint _ _ _) n ty sc) =

1112+ prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =

1060 bracket p 2 $

1113 bracket p 2 $

1061 if size sc > breakingSize then

1114 if size sc > breakingSize then

1062− prettySe 10 ty <+> text "=>" <+> prettySe 10 sc

1115+ prettySe 10 bnd ty <+> text "=>" <+> prettySe 10 ((n, True):bnd) sc

1063 else

1116 else

1064− prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc

1117+ prettySe 10 bnd ty <+> text "=>" <> line <> prettySe 10 ((n, True):bnd) sc

1065− prettySe p (PPi (TacImp _ _ s _) n ty sc) =

1118+ prettySe p bnd (PPi (TacImp _ _ s _) n ty sc) =

1066 bracket p 2 $

1119 bracket p 2 $

1067 if size sc > breakingSize then

1120 if size sc > breakingSize then

1068− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>

1121+ lbrace <> text "tacimp" <+> bindingOf n True <+> colon <+> prettySe 10 bnd ty <>

1069− rbrace <+> text "->" $+$ prettySe 10 sc

1122+ rbrace <+> text "->" <> line <> prettySe 10 ((n, True):bnd) sc

1070 else

1123 else

1071− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>

1124+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

1072− rbrace <+> text "->" <+> prettySe 10 sc

1125+ rbrace <+> text "->" <+> prettySe 10 ((n, True):bnd) sc

1073− prettySe p (PApp _ (PRef _ f) [])

1126+ prettySe p bnd (PApp _ (PRef _ f) [])

1074− | not impl = pretty f

1127+ | not impl = prettyName impl bnd f

1075− prettySe p (PAppBind _ (PRef _ f) [])

1128+ prettySe p bnd (PAppBind _ (PRef _ f) [])

1076− | not impl = text "!" <+> pretty f

1129+ | not impl = text "!" <> prettyName impl bnd f

1077− prettySe p (PApp _ (PRef _ op@(UN nm)) args)

1130+ prettySe p bnd (PApp _ (PRef _ op) args)

1131+ | UN nm <- basename op

1078− | not (tnull nm) &&

1132+ , not (tnull nm) &&

1079 length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =

1133 length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =

1080 let [l, r] = getExps args in

1134 let [l, r] = getExps args in

1081 bracket p 1 $

1135 bracket p 1 $

1082 if size r > breakingSize then

1136 if size r > breakingSize then

1083− prettySe 1 l <+> pretty op $+$ prettySe 0 r

1137+ prettySe 1 bnd l <+> prettyName impl bnd op <> line <> prettySe 0 bnd r

1084 else

1138 else

1085− prettySe 1 l <+> pretty op <+> prettySe 0 r

1139+ prettySe 1 bnd l <+> prettyName impl bnd op <+> prettySe 0 bnd r

1140+ prettySe p bnd (PApp _ hd@(PRef fc f) [tm])

1141+ | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1142+ f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

1086− prettySe p (PApp _ f as) =

1143+ prettySe p bnd (PApp _ f as) =

1087− let args = getExps as in

1144+ let args = getExps as

1145+ fp = prettySe 1 bnd f

1146+ in

1088 bracket p 1 $

1147 bracket p 1 $

1089− prettySe 1 f <+>

1090− if impl then

1148+ hsep (if impl

1091− foldl' fS empty as

1092− -- foldr (<+>) empty $ map prettyArgS as

1149+ then fp : map (prettyArgS bnd) as

1093− else

1094− foldl' fSe empty args

1095− -- foldr (<+>) empty $ map prettyArgSe args

1150+ else fp : map (prettyArgSe bnd) args)

1151+ prettySe p bnd (PCase _ scr opts) =

1152+ text "case" <+> prettySe 10 bnd scr <+> text "of" <> prettyBody

1096 where

1153 where

1097− fS l r =

1098− if size r > breakingSize then

1099− l $+$ nest nestingSize (prettyArgS r)

1100− else

1101− l <+> prettyArgS r

1102−

1103− fSe l r =

1104− if size r > breakingSize then

1105− l $+$ nest nestingSize (prettyArgSe r)

1106− else

1107− l <+> prettyArgSe r

1108− prettySe p (PCase _ scr opts) =

1109− text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody

1110− where

1111− prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts

1154+ prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts

1112−

1155+

1113− sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r

1156+ sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r

1114− prettySe p (PHidden tm) = text "." <> prettySe 0 tm

1157+ prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm

1115− prettySe p (PRefl _ _) = text "refl"

1158+ prettySe p bnd (PRefl _ _) = annotate (AnnName eqCon Nothing Nothing) $ text "refl"

1116− prettySe p (PResolveTC _) = text "resolvetc"

1159+ prettySe p bnd (PResolveTC _) = text "resolvetc"

1117− prettySe p (PTrue _) = text "()"

1160+ prettySe p bnd (PTrue _) = annotate (AnnName unitTy Nothing Nothing) $ text "()"

1118− prettySe p (PFalse _) = text "_|_"

1161+ prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"

1119− prettySe p (PEq _ l r) =

1162+ prettySe p bnd (PEq _ l r) =

1120 bracket p 2 $

1163 bracket p 2 $

1121 if size r > breakingSize then

1164 if size r > breakingSize then

1122− prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)

1165+ prettySe 10 bnd l <+> eq <$> nest nestingSize (prettySe 10 bnd r)

1123 else

1166 else

1124− prettySe 10 l <+> text "=" <+> prettySe 10 r

1167+ prettySe 10 bnd l <+> eq <+> prettySe 10 bnd r

1168+ where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")

1125− prettySe p (PRewrite _ l r _) =

1169+ prettySe p bnd (PRewrite _ l r _) =

1126 bracket p 2 $

1170 bracket p 2 $

1127 if size r > breakingSize then

1171 if size r > breakingSize then

1128− text "rewrite" <+> prettySe 10 l <+> text "in" $$ nest nestingSize (prettySe 10 r)

1172+ text "rewrite" <+> prettySe 10 bnd l <+> text "in" <> nest nestingSize (prettySe 10 bnd r)

1129 else

1173 else

1130− text "rewrite" <+> prettySe 10 l <+> text "in" <+> prettySe 10 r

1174+ text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r

1131− prettySe p (PTyped l r) =

1175+ prettySe p bnd (PTyped l r) =

1132− lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen

1176+ lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen

1133− prettySe p (PPair _ l r) =

1177+ prettySe p bnd (PPair _ l r) =

1134 if size r > breakingSize then

1178 if size r > breakingSize then

1135− lparen <> prettySe 10 l <> text "," $+$

1179+ lparen <> prettySe 10 bnd l <> text "," <>

1136− prettySe 10 r <> rparen

1180+ line <> prettySe 10 bnd r <> rparen

1137 else

1181 else

1138− lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen

1182+ lparen <> prettySe 10 bnd l <> text "," <+> prettySe 10 bnd r <> rparen

1139− prettySe p (PDPair _ l t r) =

1183+ prettySe p bnd (PDPair _ l t r) =

1140 if size r > breakingSize then

1184 if size r > breakingSize then

1141− lparen <> prettySe 10 l <+> text "**" $+$

1185+ lparen <> prettySe 10 bnd l <+> text "**" <>

1142− prettySe 10 r <> rparen

1186+ line <> prettySe 10 bnd r <> rparen

1143 else

1187 else

1144− lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen

1188+ lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen

1145− prettySe p (PAlternative a as) =

1189+ prettySe p bnd (PAlternative a as) =

1146 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1190 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1147 where

1191 where

1148 prettyAs =

1192 prettyAs =

1149− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as

1193+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as

1150− prettySe p PType = text "Type"

1194+ prettySe p bnd PType = annotate AnnConstType $ text "Type"

1151− prettySe p (PConstant c) = pretty c

1195+ prettySe p bnd (PConstant c) = annotate (annot c) (text (show c))

1196+ where annot (AType _) = AnnConstType

1197+ annot StrType = AnnConstType

1198+ annot PtrType = AnnConstType

1199+ annot VoidType = AnnConstType

1200+ annot _ = AnnConstData

1152 -- XXX: add pretty for tactics

1201 -- XXX: add pretty for tactics

1153− prettySe p (PProof ts) =

1202+ prettySe p bnd (PProof ts) =

1154− text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace

1203+ text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace

1155− prettySe p (PTactics ts) =

1204+ prettySe p bnd (PTactics ts) =

1156− text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace

1205+ text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace

1157− prettySe p (PMetavar n) = text "?" <> pretty n

1206+ prettySe p bnd (PMetavar n) = text "?" <> pretty n

1158− prettySe p (PReturn f) = text "return"

1207+ prettySe p bnd (PReturn f) = text "return"

1159− prettySe p PImpossible = text "impossible"

1208+ prettySe p bnd PImpossible = text "impossible"

1160− prettySe p Placeholder = text "_"

1209+ prettySe p bnd Placeholder = text "_"

1161− prettySe p (PDoBlock _) = text "do block pretty not implemented"

1210+ prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"

1162− prettySe p (PElabError s) = pretty s

1211+ prettySe p bnd (PElabError s) = pretty s

1163−

1212+

1164− prettySe p _ = text "test"

1213+ prettySe p bnd _ = text "test"

1165−

1214+

1166− prettyArgS (PImp _ _ _ n tm _) = prettyArgSi (n, tm)

1215+ prettyArgS bnd (PImp _ _ _ n tm _) = prettyArgSi bnd (n, tm)

1167− prettyArgS (PExp _ _ tm _) = prettyArgSe tm

1216+ prettyArgS bnd (PExp _ _ tm _) = prettyArgSe bnd tm

1168− prettyArgS (PConstraint _ _ tm _) = prettyArgSc tm

1217+ prettyArgS bnd (PConstraint _ _ tm _) = prettyArgSc bnd tm

1169− prettyArgS (PTacImplicit _ _ n _ tm _) = prettyArgSti (n, tm)

1218+ prettyArgS bnd (PTacImplicit _ _ n _ tm _) = prettyArgSti bnd (n, tm)

1170−

1219+

1171− prettyArgSe arg = prettySe 0 arg

1220+ prettyArgSe bnd arg = prettySe 0 bnd arg

1172− prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace

1221+ prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1173− prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace

1222+ prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace

1174− prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace

1223+ prettyArgSti bnd (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1224+

1225+ basename :: Name -> Name

1226+ basename (NS n _) = basename n

1227+ basename n = n

1228+

1229+ slist' p bnd (PApp _ (PRef _ nil) _)

1230+ | not impl && nsroot nil == sUN "Nil" = Just []

1231+ slist' p bnd (PApp _ (PRef _ cons) args)

1232+ | nsroot cons == sUN "::",

1233+ (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

1234+ all isImp imps,

1235+ Just tl' <- slist' p bnd tl

1236+ = Just (hd:tl')

1237+ where

1238+ isImp (PImp {}) = True

1239+ isImp _ = False

1240+ slist' _ _ _ = Nothing

1241+

1242+ slist p bnd e | Just es <- slist' p bnd e = Just $

1243+ case es of [] -> annotate AnnConstData $ text "[]"

1244+ [x] -> enclose left

1245+ right

1246+ (prettySe p bnd x)

1247+ xs -> (enclose left right . hsep . punctuate comma . map (prettySe p bnd)) xs

1248+ where left = (annotate AnnConstData (text "["))

1249+ right = (annotate AnnConstData (text "]"))

1250+ comma = (annotate AnnConstData (text ","))

1251+ slist _ _ _ = Nothing

1252+

1253+ natns = "Prelude.Nat."

1254+

1255+ snat p (PRef _ z)

1256+ | show z == (natns++"Z") || show z == "Z" = Just 0

1257+ snat p (PApp _ s [PExp {getTm=n}])

1258+ | show s == (natns++"S") || show s == "S",

1259+ Just n' <- snat p n

1260+ = Just $ 1 + n'

1261+ snat _ _ = Nothing

1175

1262

1176 bracket outer inner doc

1263 bracket outer inner doc

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

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

1178 | otherwise = doc

1265 | otherwise = doc

1179

1266

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

1268+bindingOf :: Name -- ^^ the bound name

1269+ -> Bool -- ^^ whether the name is implicit

1270+ -> Doc OutputAnnotation

1271+bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))

1272+

1273+-- | Pretty-printer helper for names that attaches the correct annotations

1274+prettyName :: Bool -- ^^ whether to show namespaces

1275+ -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit

1276+ -> Name -- ^^ the name to pprint

1277+ -> Doc OutputAnnotation

1278+prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) (text (strName n))

1279+ | otherwise = annotate (AnnName n Nothing Nothing) (text (strName n))

1280+ where strName (UN n) = T.unpack n

1281+ strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

1282+ | otherwise = strName n

1283+ strName (MN i s) = T.unpack s

1284+ strName other = show other

1285+

1286+

1287+showCImp :: Bool -> PClause -> Doc OutputAnnotation

1288+showCImp impl (PClause _ n l ws r w)

1289+ = prettyImp impl l <+> showWs ws <+> text "=" <+> prettyImp impl r

1290+ <+> text "where" <+> text (show w)

1291+ where

1292+ showWs [] = empty

1293+ showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs

1294+showCImp impl (PWith _ n l ws r w)

1295+ = prettyImp impl l <+> showWs ws <+> text "with" <+> prettyImp impl r

1296+ <+> braces (text (show w))

1297+ where

1298+ showWs [] = empty

1299+ showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs

1300+

1301+

1302+showDImp :: Bool -> PData -> Doc OutputAnnotation

1303+showDImp impl (PDatadecl n ty cons)

1304+ = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>

1305+ (indent 2 $ vsep (map (\ (_, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))

1306+

1307+showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation

1308+showDecls i ds = vsep (map (showDeclImp i) ds)

1309+

1310+showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))

1311+showDeclImp i (PTy _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t

1312+showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1313+ indent 2 (vsep (map (showCImp i) cs))

1314+showDeclImp _ (PData _ _ _ _ d) = showDImp True d

1315+showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)

1316+showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)

1317+showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1318+showDeclImp i (PClass _ _ _ cs n ps ds)

1319+ = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls i ds

1320+showDeclImp i (PInstance _ _ cs n _ t _ ds)

1321+ = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp i t <> line <> showDecls i ds

1322+showDeclImp _ _ = text "..."

1323+-- showDeclImp (PImport i) = "import " ++ i

1324+

1325+instance Show (Doc OutputAnnotation) where

1326+ show = flip (displayS . renderCompact) ""

1327+

1328+getImps :: [PArg] -> [(Name, PTerm)]

1329+getImps [] = []

1330+getImps (PImp _ _ _ n tm _ : xs) = (n, tm) : getImps xs

1331+getImps (_ : xs) = getImps xs

1332+

1333+getExps :: [PArg] -> [PTerm]

1334+getExps [] = []

1335+getExps (PExp _ _ tm _ : xs) = tm : getExps xs

1336+getExps (_ : xs) = getExps xs

1337+

1338+getConsts :: [PArg] -> [PTerm]

1339+getConsts [] = []

1340+getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs

1341+getConsts (_ : xs) = getConsts xs

1342+

1343+getAll :: [PArg] -> [PTerm]

1344+getAll = map getTm

1345+

1346+

1180-- | Show Idris name

1347-- | Show Idris name

1181showName :: Maybe IState -- ^^ the Idris state, for information about names and colours

1348showName :: Maybe IState -- ^^ the Idris state, for information about names and colours

1182 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit

1349 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit

@@ -1206,171 +1373,14 @@ showName ist bnd impl colour n = case ist of

1206 -- (like error messages). Thus, unknown vars are colourised as implicits.

1373 -- (like error messages). Thus, unknown vars are colourised as implicits.

1207 | otherwise -> colouriseImplicit t name

1374 | otherwise -> colouriseImplicit t name

1208

1375

1209−-- | Show Idris term

1210−showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers and colours

1376+showTm :: IState -- ^^ the Idris state, for information about identifiers and colours

1211− -> Bool -- ^^ whether to show implicits

1212− -> Bool -- ^^ whether to colourise

1213− -> PTerm -- ^^ the term to show

1377+ -> PTerm -- ^^ the term to show

1214− -> String

1378+ -> String

1215−showImp ist impl colour tm = se 10 [] tm where

1379+showTm ist = displayDecorated (consoleDecorate ist) . renderCompact . prettyImp (opt_showimp (idris_options ist))

1216− perhapsColourise :: (ColourTheme -> String -> String) -> String -> String

1217− perhapsColourise col str = case ist of

1218− Just i -> if colour then col (idris_colourTheme i) str else str

1219− Nothing -> str

1220−

1221− se :: Int -> [(Name, Bool)] -> PTerm -> String

1222− se p bnd (PQuote r) = "![" ++ show r ++ "]"

1223− se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n

1224− se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"

1225− se p bnd e

1226− | Just str <- slist p bnd e = str

1227− | Just num <- snat p e = perhapsColourise colouriseData (show num)

1228− se p bnd (PRef fc n) = showName ist bnd impl colour n

1229− se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++

1230− (if impl then " : " ++ se 10 bnd ty else "") ++ " => "

1231− ++ se 10 ((n, False):bnd) sc

1232− se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++

1233− " = " ++ se 10 bnd v ++

1234− " in " ++ se 10 ((n, False):bnd) sc

1235− se p bnd (PPi (Exp l s _ param) n ty sc)

1236− | n `elem` allNamesIn sc || impl

1237− = bracket p 2 $

1238− (if Lazy `elem` l then "|(" else "(") ++

1239− perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1240− ") " ++

1241− (if (impl && param) then "P" else "") ++

1242− st ++

1243− "-> " ++ se 10 ((n, False):bnd) sc

1244− | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc

1245− where st = case s of

1246− Static -> "[static] "

1247− _ -> ""

1248− se p bnd (PPi (Imp l s _ _) n ty sc)

1249− | impl = bracket p 2 $ (if Lazy `elem` l then "|{" else "{") ++

1250− perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1251− "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc

1252− | otherwise = se 10 ((n, True):bnd) sc

1253− where st = case s of

1254− Static -> "[static] "

1255− _ -> ""

1256− se p bnd (PPi (Constraint _ _ _) n ty sc)

1257− = bracket p 2 $ se 10 bnd ty ++ " => " ++ se 10 bnd sc

1258− se p bnd (PPi (TacImp _ _ s _) n ty sc)

1259− = bracket p 2 $

1260− "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++

1261− se 10 ((n, False):bnd) sc

1262− se p bnd (PMatchApp _ f) = "match " ++ show f

1263− se p bnd (PApp _ hd@(PRef fc f) [tm])

1264− | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1265− f == sUN "Symbol_" = "'" ++ se 10 bnd (PRef fc (sUN str))

1266− se p bnd (PApp _ hd@(PRef _ f) [])

1267− | not impl = se p bnd hd

1268− se p bnd (PAppBind _ hd@(PRef _ f) [])

1269− | not impl = "!" ++ se p bnd hd

1270− se p bnd (PApp _ op@(PRef _ (UN nm)) args)

1271− | not (tnull nm) &&

1272− length (getExps args) == 2 && not impl && not (isAlpha (thead nm))

1273− = let [l, r] = getExps args in

1274− bracket p 1 $ se 1 bnd l ++ " " ++ se p bnd op ++ " " ++ se 0 bnd r

1275− se p bnd (PApp _ f as)

1276− = -- let args = getExps as in

1277− bracket p 1 $ se 1 bnd f ++

1278− if impl then concatMap (sArg bnd) as

1279− else concatMap (suiArg impl bnd) as

1280− se p bnd (PAppBind _ f as)

1281− = let args = getExps as in

1282− "!" ++ (bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as

1283− else concatMap (seArg bnd) args)

1284− se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)

1285− where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r

1286− se p bnd (PHidden tm) = "." ++ se 0 bnd tm

1287− se p bnd (PRefl _ t)

1288− | not impl = perhapsColourise colouriseData "refl"

1289− | otherwise = perhapsColourise colouriseData $ "refl {" ++ se 10 bnd t ++ "}"

1290− se p bnd (PResolveTC _) = "resolvetc"

1291− se p bnd (PTrue _) = perhapsColourise colouriseType "()"

1292− se p bnd (PFalse _) = perhapsColourise colouriseType "_|_"

1293− se p bnd (PEq _ l r) = bracket p 2 $ se 10 bnd l ++ perhapsColourise colouriseType " = " ++ se 10 bnd r

1294− se p bnd (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 bnd l ++ " in " ++ se 10 bnd r

1295− se p bnd (PTyped l r) = "(" ++ se 10 bnd l ++ " : " ++ se 10 bnd r ++ ")"

1296− se p bnd (PPair _ l r) = "(" ++ se 10 bnd l ++ ", " ++ se 10 bnd r ++ ")"

1297− se p bnd (PDPair _ l t r) = "(" ++ se 10 bnd l ++ " ** " ++ se 10 bnd r ++ ")"

1298− se p bnd (PAlternative a as) = "(|" ++ showSep " , " (map (se 10 bnd) as) ++ "|)"

1299− se p bnd PType = perhapsColourise colouriseType "Type"

1300− se p bnd (PConstant c) = perhapsColourise (cfun c) (show c)

1301− where cfun (AType _) = colouriseType

1302− cfun StrType = colouriseType

1303− cfun PtrType = colouriseType

1304− cfun VoidType = colouriseType

1305− cfun _ = colouriseData

1306− se p bnd (PProof ts) = "proof { " ++ show ts ++ "}"

1307− se p bnd (PTactics ts) = "tactics { " ++ show ts ++ "}"

1308− se p bnd (PMetavar n) = "?" ++ show n

1309− se p bnd (PReturn f) = "return"

1310− se p bnd PImpossible = "impossible"

1311− se p bnd Placeholder = "_"

1312− se p bnd (PDoBlock _) = "do block show not implemented"

1313− se p bnd (PElabError s) = show s

1314− se p bnd (PCoerced t) = se p bnd t

1315− se p bnd (PUnifyLog t) = "%unifyLog " ++ se p bnd t

1316− se p bnd (PDisamb ns t) = "%disamb " ++ show ns ++ se p bnd t

1317− se p bnd (PNoImplicits t) = "%noimplicit " ++ se p bnd t

1318−-- se p bnd x = "Not implemented"

1319−

1320− slist' p bnd (PApp _ (PRef _ nil) _)

1321− | not impl && nsroot nil == sUN "Nil" = Just []

1322− slist' p bnd (PApp _ (PRef _ cons) args)

1323− | nsroot cons == sUN "::",

1324− (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

1325− all isImp imps,

1326− Just tl' <- slist' p bnd tl

1327− = Just (hd:tl')

1328− where

1329− isImp (PImp {}) = True

1330− isImp _ = False

1331− slist' _ _ _ = Nothing

1332−

1333− slist p bnd e | Just es <- slist' p bnd e = Just $

1334− case es of [] -> "[]"

1335− [x] -> "[" ++ se p bnd x ++ "]"

1336− xs -> "[" ++ intercalate "," (map (se p bnd ) xs) ++ "]"

1337− slist _ _ _ = Nothing

1338−

1339− -- since Prelude is always imported, S & Z are unqualified iff they're the

1340− -- Nat ones.

1341− snat p (PRef _ o)

1342− | show o == (natns++"Z") || show o == "Z" = Just 0

1343− snat p (PApp _ s [PExp {getTm=n}])

1344− | show s == (natns++"S") || show s == "S",

1345− Just n' <- snat p n

1346− = Just $ 1 + n'

1347− snat _ _ = Nothing

1348−

1349− natns = "Prelude.Nat."

1350

1380

1351− sArg bnd (PImp _ _ _ n tm _) = siArg bnd (n, tm)

1381+-- | Show a term with implicits, no colours

1352− sArg bnd (PExp _ _ tm _) = seArg bnd tm

1382+showTmImpls :: PTerm -> String

1353− sArg bnd (PConstraint _ _ tm _) = scArg bnd tm

1383+showTmImpls = flip (displayS . renderCompact . prettyImp True) ""

1354− sArg bnd (PTacImplicit _ _ n _ tm _) = stiArg bnd (n, tm)

1355−

1356− -- show argument, implicits given by the user also shown

1357− suiArg impl bnd (PImp _ mi _ n tm _)

1358− | impl || not mi = siArg bnd (n, tm)

1359− suiArg impl bnd (PExp _ _ tm _) = seArg bnd tm

1360− suiArg impl bnd _ = ""

1361−

1362− seArg bnd arg = " " ++ se 0 bnd arg

1363− siArg bnd (n, val) =

1364− let n' = show n

1365− val' = se 10 bnd val in

1366− if (n' == val')

1367− then " {" ++ n' ++ "}"

1368− else " {" ++ n' ++ " = " ++ val' ++ "}"

1369− scArg bnd val = " {{" ++ se 10 bnd val ++ "}}"

1370− stiArg bnd (n, val) = " {auto " ++ show n ++ " = " ++ se 10 bnd val ++ "}"

1371−

1372− bracket outer inner str | inner > outer = "(" ++ str ++ ")"

1373− | otherwise = str

1374

1384

1375

1385

1376instance Sized PTerm where

1386instance Sized PTerm where

src/Idris/CaseSplit.hs+3−3

@@ -62,11 +62,11 @@ split n t'

62 Just ty ->

63 do let splits = findPats ist ty

64 iLOG ("New patterns " ++ showSep ", "

65− (map (showImp Nothing True False) splits))

65+ (map showTmImpls splits))

66 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)

67 logLvl 4 ("Working from " ++ show t)

68 logLvl 4 ("Trying " ++ showSep "\n"

69− (map (showImp Nothing True False) newPats_in))

69+ (map (showTmImpls) newPats_in))

70 newPats <- mapM elabNewPat newPats_in

71 logLvl 3 ("Original:\n" ++ show t)

72 logLvl 3 ("Split:\n" ++

@@ -237,7 +237,7 @@ splitOnLine l n fn = do

237-- let (before, later) = splitAt (l-1) (lines inp)

238-- i <- getIState

239 cl <- getInternalApp fn l

240− logLvl 3 ("Working with " ++ showImp Nothing True False cl)

240+ logLvl 3 ("Working with " ++ showTmImpls cl)

241 tms <- split n cl

242-- iputStrLn (showSep "\n" (map show tms))

243 return tms -- "" -- not yet done...

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

@@ -24,7 +24,7 @@ import Data.Char

24import Data.List

25import Debug.Trace

27−import Util.Pretty

27+import Util.Pretty hiding (fill)

29-- I don't really want this here, but it's useful for the test shell

30data Command = Theorem Name Raw

src/Idris/Core/ProofState.hs+12−12

@@ -18,7 +18,7 @@ import Control.Applicative hiding (empty)

18import Data.List

19import Debug.Trace

21−import Util.Pretty

21+import Util.Pretty hiding (fill)

23data ProofState = PS { thname :: Name,

24 holes :: [Name], -- holes still to be solved

@@ -113,23 +113,23 @@ instance Show ProofState where

113 " =?= " ++ showEnv ps v

114 showG ps b = showEnv ps (binderTy b)

115

116−instance Pretty ProofState where

116+instance Pretty ProofState OutputAnnotation where

117 pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

118 if size nm > breakingSize then

119− pretty nm <> colon $$ nest nestingSize (text " no more goals.")

119+ pretty nm <+> colon <+> nest nestingSize (text " no more goals.")

120 else

121− pretty nm <> colon <+> text " no more goals."

121+ pretty nm <+> colon <+> text " no more goals."

122 pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _) =

123 let OK g = goal (Just h) tm in

124 let wkEnv = premises g in

125− text "Other goals" <+> colon <+> pretty hs $$

125+ text "Other goals" <+> colon <+> pretty hs <+>

126− prettyPs wkEnv (reverse wkEnv) $$

126+ prettyPs wkEnv (reverse wkEnv) <+>

127− text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$

127+ text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" <+>

128 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)

129 where

130 prettyGoal ps (Guess t v) =

131 if size v > breakingSize then

132− prettyEnv ps t <+> text "=?=" $$

132+ prettyEnv ps t <+> text "=?=" <+>

133 nest nestingSize (prettyEnv ps v)

134 else

135 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v

@@ -139,17 +139,17 @@ instance Pretty ProofState where

139 prettyPs env ((n, Let t v):bs) =

140 nest nestingSize (pretty n <+> colon <+>

141 if size v > breakingSize then

142− prettyEnv env t <+> text "=" $$

142+ prettyEnv env t <+> text "=" <+>

143− nest nestingSize (prettyEnv env v) $$

143+ nest nestingSize (prettyEnv env v) <+>

144 nest nestingSize (prettyPs env bs)

145 else

146− prettyEnv env t <+> text "=" <+> prettyEnv env v $$

146+ prettyEnv env t <+> text "=" <+> prettyEnv env v <+>

147 nest nestingSize (prettyPs env bs))

148 prettyPs env ((n, b):bs) =

149 if size (binderTy b) > breakingSize then

150 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)

151 else

152− nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$

152+ nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>

153 nest nestingSize (prettyPs env bs))

154

155same Nothing n = True

src/Idris/Core/TT.hs+33−19

@@ -77,6 +77,16 @@ instance Sized FC where

77instance Show FC where

78 show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c

80+-- | Output annotation for pretty-printed name - decides colour

81+data NameOutput = TypeOutput | FunOutput | DataOutput

82+

83+-- | Output annotations for pretty-printing

84+data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe Type)

85+ | AnnBoundName Name Bool

86+ | AnnConstData

87+ | AnnConstType

88+ | AnnFC FC

89+

80-- | Used for error reflection

90-- | Used for error reflection

81data ErrorReportPart = TextPart String

91data ErrorReportPart = TextPart String

82 | NamePart Name

92 | NamePart Name

@@ -177,15 +187,15 @@ instance Show Err where

177 show (At f e) = show f ++ ":" ++ show e

187 show (At f e) = show f ++ ":" ++ show e

178 show _ = "Error"

188 show _ = "Error"

179

189

180−instance Pretty Err where

190+instance Pretty Err OutputAnnotation where

181 pretty (Msg m) = text m

191 pretty (Msg m) = text m

182 pretty (CantUnify _ l r e _ i) =

192 pretty (CantUnify _ l r e _ i) =

183 if size l + size r > breakingSize then

193 if size l + size r > breakingSize then

184− text "Cannot unify" <+> colon $$

194+ text "Cannot unify" <+> colon <+>

185− nest nestingSize (pretty l <+> text "and" <+> pretty r) $$

195+ nest nestingSize (pretty l <+> text "and" <+> pretty r) <+>

186 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

196 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

187 else

197 else

188− text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$

198+ text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>

189 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

199 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

190 pretty (ProviderError msg) = text msg

200 pretty (ProviderError msg) = text msg

191 pretty err@(LoadingFailed _ _) = text (show err)

201 pretty err@(LoadingFailed _ _) = text (show err)

@@ -196,11 +206,11 @@ instance Error Err where

196

206

197type TC = TC' Err

207type TC = TC' Err

198

208

199−instance (Pretty a) => Pretty (TC a) where

209+instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where

200 pretty (OK ok) = pretty ok

210 pretty (OK ok) = pretty ok

201 pretty (Error err) =

211 pretty (Error err) =

202 if size err > breakingSize then

212 if size err > breakingSize then

203− text "Error" <+> colon $$ (nest nestingSize $ pretty err)

213+ text "Error" <+> colon <+> (nest nestingSize $ pretty err)

204 else

214 else

205 text "Error" <+> colon <+> pretty err

215 text "Error" <+> colon <+> pretty err

206

216

@@ -294,11 +304,15 @@ instance Sized Name where

294 size (MN i n) = 1

304 size (MN i n) = 1

295 size _ = 1

305 size _ = 1

296

306

297−instance Pretty Name where

307+instance Pretty Name OutputAnnotation where

298− pretty (UN n) = text (T.unpack n)

308+ pretty n@(UN n') = annotate (AnnName n Nothing Nothing) $ text (T.unpack n')

299− pretty (NS n s) = pretty n

309+ pretty n@(NS un s) = annotate (AnnName n Nothing Nothing) . noAnnotate $ pretty un

310+ pretty n@(MN i s) = annotate (AnnName n Nothing Nothing) $

300− pretty (MN i s) = lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace

311+ lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace

301− pretty (SN s) = text (show s)

312+ pretty n@(SN s) = annotate (AnnName n Nothing Nothing) $ text (show s)

313+

314+instance Pretty [Name] OutputAnnotation where

315+ pretty = encloseSep empty empty comma . map pretty

302

316

303instance Show Name where

317instance Show Name where

304 show (UN n) = str n

318 show (UN n) = str n

@@ -417,7 +431,7 @@ addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

417data NativeTy = IT8 | IT16 | IT32 | IT64

431data NativeTy = IT8 | IT16 | IT32 | IT64

418 deriving (Show, Eq, Ord, Enum)

432 deriving (Show, Eq, Ord, Enum)

419

433

420−instance Pretty NativeTy where

434+instance Pretty NativeTy OutputAnnotation where

421 pretty IT8 = text "Bits8"

435 pretty IT8 = text "Bits8"

422 pretty IT16 = text "Bits16"

436 pretty IT16 = text "Bits16"

423 pretty IT32 = text "Bits32"

437 pretty IT32 = text "Bits32"

@@ -435,7 +449,7 @@ deriving instance NFData NativeTy

435deriving instance NFData ArithTy

449deriving instance NFData ArithTy

436!-}

450!-}

437

451

438−instance Pretty ArithTy where

452+instance Pretty ArithTy OutputAnnotation where

439 pretty (ATInt ITNative) = text "Int"

453 pretty (ATInt ITNative) = text "Int"

440 pretty (ATInt ITBig) = text "BigInt"

454 pretty (ATInt ITBig) = text "BigInt"

441 pretty (ATInt ITChar) = text "Char"

455 pretty (ATInt ITChar) = text "Char"

@@ -471,7 +485,7 @@ deriving instance NFData Const

471instance Sized Const where

485instance Sized Const where

472 size _ = 1

486 size _ = 1

473

487

474−instance Pretty Const where

488+instance Pretty Const OutputAnnotation where

475 pretty (I i) = text . show $ i

489 pretty (I i) = text . show $ i

476 pretty (BI i) = text . show $ i

490 pretty (BI i) = text . show $ i

477 pretty (Fl f) = text . show $ f

491 pretty (Fl f) = text . show $ f

@@ -503,7 +517,7 @@ instance Sized Raw where

503 size (RForce raw) = 1 + size raw

517 size (RForce raw) = 1 + size raw

504 size (RConstant const) = size const

518 size (RConstant const) = size const

505

519

506−instance Pretty Raw where

520+instance Pretty Raw OutputAnnotation where

507 pretty = text . show

521 pretty = text . show

508

522

509{-!

523{-!

@@ -621,7 +635,7 @@ deriving instance NFData NameType

621instance Sized NameType where

635instance Sized NameType where

622 size _ = 1

636 size _ = 1

623

637

624−instance Pretty NameType where

638+instance Pretty NameType OutputAnnotation where

625 pretty = text . show

639 pretty = text . show

626

640

627instance Eq NameType where

641instance Eq NameType where

@@ -687,7 +701,7 @@ instance Sized a => Sized (TT a) where

687 size Erased = 1

701 size Erased = 1

688 size (TType u) = 1 + size u

702 size (TType u) = 1 + size u

689

703

690−instance Pretty a => Pretty (TT a) where

704+instance Pretty a o => Pretty (TT a) o where

691 pretty _ = text "test"

705 pretty _ = text "test"

692

706

693type EnvTT n = [(n, Binder (TT n))]

707type EnvTT n = [(n, Binder (TT n))]

@@ -1042,7 +1056,7 @@ prettyEnv env t = prettyEnv' env t False

1042 prettySe p env (P nt n t) debug =

1056 prettySe p env (P nt n t) debug =

1043 pretty n <+>

1057 pretty n <+>

1044 if debug then

1058 if debug then

1045− lbrack <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbrack

1059+ lbracket <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbracket

1046 else

1060 else

1047 empty

1061 empty

1048 prettySe p env (V i) debug

1062 prettySe p env (V i) debug

@@ -1050,7 +1064,7 @@ prettyEnv env t = prettyEnv' env t False

1050 if debug then

1064 if debug then

1051 text . show . fst $ env!!i

1065 text . show . fst $ env!!i

1052 else

1066 else

1053− lbrack <+> text (show i) <+> rbrack

1067+ lbracket <+> text (show i) <+> rbracket

1054 | otherwise = text "unbound" <+> text (show i) <+> text "!"

1068 | otherwise = text "unbound" <+> text (show i) <+> text "!"

1055 prettySe p env (Bind n b@(Pi t) sc) debug

1069 prettySe p env (Bind n b@(Pi t) sc) debug

1056 | noOccurrence n sc && not debug =

1070 | noOccurrence n sc && not debug =

src/Idris/Coverage.hs+3−3

@@ -50,7 +50,7 @@ genClauses fc n xs given

50 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)

51 logLvl 10 $ show argss ++ "\n" ++ show all_args

52 logLvl 10 $ "Original: \n" ++

53− showSep "\n" (map (\t -> showImp Nothing True False (delab' i t True True)) xs)

53+ showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)

54 -- add an infinite supply of explicit arguments to update the possible

55 -- cases for (the return type may be variadic, or function type, sp

56 -- there may be more case splitting that the idris_implicits record

@@ -60,10 +60,10 @@ genClauses fc n xs given

60 _ -> repeat (pexp Placeholder)

61 let tryclauses = mkClauses parg all_args

62 logLvl 2 $ show (length tryclauses) ++ " initially to check"

63− logLvl 5 $ showSep "\n" (map (showImp Nothing True False) tryclauses)

63+ logLvl 5 $ showSep "\n" (map (showTm i) tryclauses)

64 let new = filter (noMatch i) (nub tryclauses)

65 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"

66− logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showImp Nothing True False) new)

66+ logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)

67-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

68 return new

69-- return (map (\t -> PClause n t [] PImpossible []) new)

src/Idris/Delaborate.hs+109−103

@@ -1,10 +1,12 @@

1{-# LANGUAGE PatternGuards #-}

3−module Idris.Delaborate where

3+module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pshow, pprintErr) where

5-- Convert core TT back into high level syntax, primarily for display

6-- purposes.

8+import Util.Pretty

8import Idris.AbsSyntax

10import Idris.AbsSyntax

9import Idris.Core.TT

11import Idris.Core.TT

10import Idris.Core.Evaluate

12import Idris.Core.Evaluate

@@ -33,7 +35,7 @@ delab' :: IState -> Term -> Bool -> Bool -> PTerm

33delab' i t f mvs = delabTy' i [] t f mvs

35delab' i t f mvs = delabTy' i [] t f mvs

35delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any

37delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any

36− -> Term

38+ -> Term

37 -> Bool -- ^ use full names

39 -> Bool -- ^ use full names

38 -> Bool -- ^ Don't treat metavariables specially

40 -> Bool -- ^ Don't treat metavariables specially

39 -> PTerm

41 -> PTerm

@@ -50,8 +52,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

50 | Just n' <- lookup n env = PRef un n'

52 | Just n' <- lookup n env = PRef un n'

51 | otherwise

53 | otherwise

52 = case lookup n (idris_metavars ist) of

54 = case lookup n (idris_metavars ist) of

53− Just (Just _, mi, _) -> mkMVApp (dens n) []

55+ Just (Just _, mi, _) -> mkMVApp n []

54− _ -> PRef un (dens n)

56+ _ -> PRef un n

55 de env _ (Bind n (Lam ty) sc)

57 de env _ (Bind n (Lam ty) sc)

56 = PLam n (de env [] ty) (de ((n,n):env) [] sc)

58 = PLam n (de env [] ty) (de ((n,n):env) [] sc)

57 de env (PImp _ _ _ _ _ _:is) (Bind n (Pi ty) sc)

59 de env (PImp _ _ _ _ _ _:is) (Bind n (Pi ty) sc)

@@ -96,9 +98,9 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

96 deFn env (P _ n _) args | not mvs

98 deFn env (P _ n _) args | not mvs

97 = case lookup n (idris_metavars ist) of

99 = case lookup n (idris_metavars ist) of

98 Just (Just _, mi, _) ->

100 Just (Just _, mi, _) ->

99− mkMVApp (dens n) (drop mi (map (de env []) args))

101+ mkMVApp n (drop mi (map (de env []) args))

100− _ -> mkPApp (dens n) (map (de env []) args)

102+ _ -> mkPApp n (map (de env []) args)

101− | otherwise = mkPApp (dens n) (map (de env []) args)

103+ | otherwise = mkPApp n (map (de env []) args)

102 deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))

104 deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))

103

105

104 mkMVApp n []

106 mkMVApp n []

@@ -115,105 +117,109 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

115 imp (PConstraint p l _ d) arg = PConstraint p l arg d

117 imp (PConstraint p l _ d) arg = PConstraint p l arg d

116 imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d

118 imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d

117

119

120+-- | How far to indent sub-errors

121+errorIndent :: Int

122+errorIndent = 8

118

123

119−indented text = boxIt '\n' $ unlines $ map ('\t':) $ lines text where

124+-- | Actually indent a sub-error - no line at end because a newline can end

120− boxIt c text = (c:text) ++ if last text == c

125+-- multiple layers of indent

121− then ""

126+indented :: Doc a -> Doc a

122− else [c]

127+indented = nest errorIndent . (line <>)

123

128

124−pshow :: IState -> Err -> String

129+pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

125−pshow i err = pshow' i (fmap (errReverse i) err)

126−

127−pshow' i (Msg s) = s

128−pshow' i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

129− "\nThis is probably a bug, or a missing error message.\n" ++

130− "Please consider reporting at " ++ bugaddr

131−pshow' i (CantUnify _ x y e sc s)

132− = let imps = opt_showimp (idris_options i) in

130+pprintTerm ist = prettyImp (opt_showimp (idris_options ist))

133− let colour = idris_colourRepl i in

134− "Can't unify" ++ indented (showImp (Just i) imps colour (delab i x))

135− ++ "with" ++ indented (showImp (Just i) imps colour (delab i y)) ++

136−-- " (" ++ show x ++ " and " ++ show y ++ ") " ++

137− case e of

138− Msg "" -> ""

139− _ -> "\nSpecifically:" ++

140− indented (pshow' i e) ++

141− if (opt_errContext (idris_options i)) then showSc i sc else ""

142−pshow' i (CantConvert x y env)

143− = let imps = opt_showimp (idris_options i) in

144− let colour = idris_colourRepl i in

145− "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"

146− ++ indented (showImp (Just i) imps colour (delab i y)) ++

147− if (opt_errContext (idris_options i)) then showSc i env else ""

148−pshow' i (CantSolveGoal x env)

149− = let imps = opt_showimp (idris_options i) in

150− let colour = idris_colourRepl i in

151− "Can't solve goal " ++ indented (showImp (Just i) imps colour (delab i x)) ++

152− if (opt_errContext (idris_options i)) then showSc i env else ""

153−pshow' i (UnifyScope n out tm env)

154− = let imps = opt_showimp (idris_options i) in

155− let colour = idris_colourRepl i in

156− "Can't unify" ++ indented (show n) ++ "with"

157− ++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++

158− indented (show out) ++ "is not in scope" ++

159− if (opt_errContext (idris_options i)) then showSc i env else ""

160−pshow' i (CantInferType t)

161− = "Can't infer type for " ++ t

162−pshow' i (NonFunctionType f ty)

163− = let imps = opt_showimp (idris_options i) in

164− let colour = idris_colourRepl i in

165− showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("

166− ++ showImp (Just i) imps colour (delab i ty) ++ ")"

167−pshow' i (NotEquality tm ty)

168− = let imps = opt_showimp (idris_options i) in

169− let colour = idris_colourRepl i in

170− showImp (Just i) imps colour (delab i tm) ++ " does not have an equality type ("

171− ++ showImp (Just i) imps colour (delab i ty) ++ ")"

172−pshow' i (TooManyArguments f)

173− = "Too many arguments for " ++ show f

174−pshow' i (CantIntroduce ty)

175− = let imps = opt_showimp (idris_options i) in

176− let colour = idris_colourRepl i in

177− "Can't use lambda here: type is " ++ showImp (Just i) imps colour (delab i ty)

178−pshow' i (InfiniteUnify x tm env)

179− = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

180− " would lead to infinite value" ++

181− if (opt_errContext (idris_options i)) then showSc i env else ""

182−pshow' i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++

183− " when unifying " ++ show (delab i x) ++ " and " ++

184− show (delab i y)

185−pshow' i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

186−pshow' i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as

187−pshow' i (NoTypeDecl n) = "No type declaration for " ++ show n

188−pshow' i (NoSuchVariable n) = "No such variable " ++ show n

189−pshow' i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing True False (delab i t)

190−pshow' i UniverseError = "Universe inconsistency"

191−pshow' i ProgramLineComment = "Program line next to comment"

192−pshow' i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

193−pshow' i (NonCollapsiblePostulate n)

194− = "The return type of postulate " ++ show n ++ " is not collapsible"

195−pshow' i (AlreadyDefined n) = show n ++ " is already defined"

196−pshow' i (ProofSearchFail e) = pshow' i e

197−pshow' i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)

198−pshow' i (At f e) = show f ++ ":" ++ pshow' i e

199−pshow' i (Elaborating s n e) = "When elaborating " ++ s ++

200− showqual i n ++ ":\n" ++ pshow' i e

201−pshow' i (ProviderError msg) = "Type provider error: " ++ msg

202−pshow' i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow' i e

203−pshow' i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in

204− concat (intersperse "\n" parts') ++

205− "\nOriginal error:\n" ++ indented (pshow' i orig)

206− where showPart :: ErrorReportPart -> String

207− showPart (TextPart str) = str

208− showPart (NamePart n) = let colour = idris_colourRepl i in

209− showName (Just i) [] False colour n

210− showPart (TermPart tm) = let colour = idris_colourRepl i

211− in showImp (Just i) False colour (delab i tm)

212− showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs

213−pshow' i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++

214− indented (pshow' i err) ++

215− "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr

216

131

132+pshow :: IState -> Err -> String

133+pshow ist err = displayDecorated (consoleDecorate ist) .

134+ renderPretty 1.0 80 .

135+ fmap (fancifyAnnots ist) $ pprintErr ist err

136+

137+pprintErr :: IState -> Err -> Doc OutputAnnotation

138+pprintErr i err = pprintErr' i (fmap (errReverse i) err)

139+

140+pprintErr' i (Msg s) = text s

141+pprintErr' i (InternalMsg s) =

142+ vsep [ text "INTERNAL ERROR:" <+> text s,

143+ text "This is probably a bug, or a missing error message.",

144+ text ("Please consider reporting at " ++ bugaddr)

145+ ]

146+pprintErr' i (CantUnify _ x y e sc s) =

147+ text "Can't unify" <> indented (pprintTerm i (delab i x)) <$>

148+ text "with" <> indented (pprintTerm i (delab i y)) <>

149+ case e of

150+ Msg "" -> empty

151+ _ -> line <> line <> text "Specifically:" <>

152+ indented (pprintErr' i e) <>

153+ if (opt_errContext (idris_options i)) then text $ showSc i sc else empty

154+pprintErr' i (CantConvert x y env) =

155+ text "Can't convert" <> indented (pprintTerm i (delab i x)) <>

156+ text "with" <> indented (pprintTerm i (delab i y)) <>

157+ if (opt_errContext (idris_options i)) then text (showSc i env) else empty

158+pprintErr' i (UnifyScope n out tm env) =

159+ text "Can't unify" <> indented (annName n) <+>

160+ text "with" <> indented (pprintTerm i (delab i tm)) <+>

161+ text "as" <> indented (annName out) <> text "is not in scope" <>

162+ if (opt_errContext (idris_options i)) then text (showSc i env) else empty

163+pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t

164+pprintErr' i (NonFunctionType f ty) =

165+ pprintTerm i (delab i f) <+>

166+ text "does not have a function type" <+>

167+ parens (pprintTerm i (delab i ty))

168+pprintErr' i (NotEquality tm ty) =

169+ pprintTerm i (delab i tm) <+>

170+ text "does not have an equality type" <+>

171+ parens (pprintTerm i (delab i ty))

172+pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f

173+pprintErr' i (CantIntroduce ty) =

174+ text "Can't use lambda here: type is" <+> pprintTerm i (delab i ty)

175+pprintErr' i (InfiniteUnify x tm env) =

176+ text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+> pprintTerm i (delab i tm) <+>

177+ text "would lead to infinite value" <>

178+ if (opt_errContext (idris_options i)) then text (showSc i env) else empty

179+pprintErr' i (NotInjective p x y) =

180+ text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>

181+ text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>

182+ pprintTerm i (delab i y)

183+pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

184+pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

185+ cat (punctuate comma (map text as))

186+pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

187+pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

188+pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)

189+pprintErr' i UniverseError = text "Universe inconsistency"

190+pprintErr' i ProgramLineComment = text "Program line next to comment"

191+pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"

192+pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>

193+ annName n <+> text "is not collapsible"

194+pprintErr' i (AlreadyDefined n) = annName n<+>

195+ text "is already defined"

196+pprintErr' i (ProofSearchFail e) = pprintErr' i e

197+pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> pprintTerm i (delab i tm)

198+pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e

199+pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>

200+ annName' n (showqual i n) <> colon <$>

201+ pprintErr' i e

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

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

204+pprintErr' i (ReflectionError parts orig) =

205+ let parts' = map (hsep . map showPart) parts in

206+ vsep parts' <> line <> line <>

207+ text "Original error:" <$> indented (pprintErr' i orig)

208+ where showPart :: ErrorReportPart -> Doc OutputAnnotation

209+ showPart (TextPart str) = text str

210+ showPart (NamePart n) = annName n

211+ showPart (TermPart tm) = pprintTerm i (delab i tm)

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

213+pprintErr' i (ReflectionFailed msg err) =

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

215+ indented (pprintErr' i err) <>

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

217+

218+annName :: Name -> Doc OutputAnnotation

219+annName n = annName' n (show n)

220+

221+annName' :: Name -> String -> Doc OutputAnnotation

222+annName' n str = annotate (AnnName n Nothing Nothing) (text str)

217

223

218showSc i [] = ""

224showSc i [] = ""

219showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

225showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

src/Idris/ElabDecls.hs+32−32

@@ -67,12 +67,12 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

67 ctxt <- getContext

68 i <- getIState

70− logLvl 3 $ show n ++ " pre-type " ++ showImp Nothing True False ty'

70+ logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

71 ty' <- addUsingConstraints syn fc ty'

72 ty' <- implicit syn n ty'

74 let ty = addImpl i ty'

75− logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty

75+ logLvl 2 $ show n ++ " type " ++ showTmImpls ty

76 ((tyT, defer, is), log) <-

77 tclift $ elaborate ctxt n (TType (UVal 0)) []

78 (errAt "type of " n (erun fc (build i info False [] n ty)))

@@ -326,10 +326,10 @@ elabEliminator paramPos n ty cons info = do

326 let clauseConsElimArgs = map getPiName consTerms

327 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

328 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

329− let elimSig = "-- eliminator signature: " ++ showImp Nothing True True eliminatorTy

329+ let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy

330 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

331 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

332− elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef

332+ elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef

333 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())

334 -- Do not elaborate clauses if there aren't any

335 case eliminatorClauses of

@@ -814,7 +814,7 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

814 i <- getIState

815 t_in <- implicit syn n (if codata then mkLazy t_in else t_in)

816 let t = addImpl i t_in

817− logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp Nothing True False t

817+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

818 ((t', defer, is), log) <-

819 tclift $ elaborate ctxt n (TType (UVal 0)) []

820 (errAt "constructor " n (erun fc (build i info False [] n t)))

@@ -959,9 +959,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

959 missing' <- filterM (checkPossible info fc True n) missing

960 let clhs = map getLHS pdef

961 logLvl 2 $ "Must be unreachable:\n" ++

962− showSep "\n" (map (showImp Nothing True False) missing') ++

962+ showSep "\n" (map showTmImpls missing') ++

963 "\nAgainst: " ++

964− showSep "\n" (map (\t -> showImp Nothing True False (delab ist t)) (map getLHS pdef))

964+ showSep "\n" (map (\t -> showTmImpls (delab ist t)) (map getLHS pdef))

965 -- filter out anything in missing' which is

966 -- matched by any of clhs. This might happen since

967 -- unification may force a variable to take a

@@ -1125,8 +1125,8 @@ elabPE info fc caller r =

1125 logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++

1126 showSep "\n"

1127 (map (\ (lhs, rhs) ->

1128− (showImp Nothing True False lhs ++ " = " ++

1128+ (showTmImpls lhs ++ " = " ++

1129− showImp Nothing True False rhs)) pats)

1129+ showTmImpls rhs)) pats)

1130 elabType info defaultSyntax "" fc opts newnm specTy

1131 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

1132 elabClauses info fc opts newnm def

@@ -1180,7 +1180,7 @@ elabValBind info aspat tm_in

1180 = do ctxt <- getContext

1181 i <- getIState

1182 let tm = addImpl i tm_in

1183− logLvl 10 (showImp Nothing True False tm)

1183+ logLvl 10 (showTmImpls tm)

1184 -- try:

1185 -- * ordinary elaboration

1186 -- * elaboration as a Type

@@ -1271,7 +1271,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1271 let params = getParamsInType i [] fn_is fn_ty

1272 let lhs = stripUnmatchable i $

1273 addImplPat i (propagateParams params (stripLinear i lhs_in))

1274− logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)

1274+ logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

1275 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

1276

1277 ((lhs', dlhs, []), _) <-

@@ -1286,7 +1286,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1286 (clhs_c, clhsty) <- recheckC fc [] lhs_tm

1287 let clhs = normalise ctxt [] clhs_c

1288

1289− logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))

1289+ logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))

1290

1291 rep <- useREPL

1292 when rep $ do

@@ -1312,10 +1312,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1312 mapM_ (elabDecl' EAll info) wbefore

1313 -- Now build the RHS, using the type of the LHS as the goal.

1314 i <- getIState -- new implicits from where block

1315− logLvl 5 (showImp Nothing True False (expandParams decorate newargs defs (defs \\ decls) rhs_in))

1315+ logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))

1316 let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)

1317 (expandParams decorate newargs defs (defs \\ decls) rhs_in)

1318− logLvl 2 $ "RHS: " ++ showImp Nothing True False rhs

1318+ logLvl 2 $ "RHS: " ++ showTmImpls rhs

1319 ctxt <- getContext -- new context with where block added

1320 logLvl 5 "STARTING CHECK"

1321 ((rhs', defer, is), _) <-

@@ -1468,7 +1468,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1468 -- pattern bindings

1469 i <- getIState

1470 let lhs = addImplPat i (stripLinear i lhs_in)

1471− logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)

1471+ logLvl 5 ("LHS: " ++ showTmImpls lhs)

1472 ((lhs', dlhs, []), _) <-

1473 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1474 (errAt "left hand side of with in " fname

@@ -1481,7 +1481,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1481 logLvl 5 ("Checked " ++ show clhs)

1482 let bargs = getPBtys lhs_tm

1483 let wval = addImplBound i (map fst bargs) wval_in

1484− logLvl 5 ("Checking " ++ showImp Nothing True False wval)

1484+ logLvl 5 ("Checking " ++ showTmImpls wval)

1485 -- Elaborate wval in this context

1486 ((wval', defer, is), _) <-

1487 tclift $ elaborate ctxt (sMN 0 "withRHS")

@@ -1545,7 +1545,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1545 (map (pexp . (PRef fc) . fst) bargs_pre ++

1546 pexp wval :

1547 (map (pexp . (PRef fc) . fst) bargs_post))

1548− logLvl 5 ("New RHS " ++ showImp Nothing True False rhs)

1548+ logLvl 5 ("New RHS " ++ showTmImpls rhs)

1549 ctxt <- getContext -- New context with block added

1550 i <- getIState

1551 ((rhs', defer, is), _) <-

@@ -1576,8 +1576,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1576 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)

1577 = do i <- getIState

1578 let tm = addImplPat i tm_in

1579− logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++

1579+ logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++

1580− showImp Nothing True False toplhs)

1580+ showTmImpls toplhs)

1581 case matchClause i toplhs tm of

1582 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ ":with clause does not match top level")

1583 Right mvars ->

@@ -1587,8 +1587,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1587 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)

1588 = do i <- getIState

1589 let tm = addImplPat i tm_in

1590− logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++

1590+ logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++

1591− showImp Nothing True False toplhs)

1591+ showTmImpls toplhs)

1592 withs' <- mapM (mkAuxC wname toplhs ns ns') withs

1593 case matchClause i toplhs tm of

1594 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")

@@ -1655,7 +1655,7 @@ elabClass info syn doc fc constraints tn ps ds

1655 constraint

1656 let cons = [("", cn, cty, fc, [])]

1657 let ddecl = PDatadecl tn tty cons

1658− logLvl 5 $ "Class data " ++ showDImp True ddecl

1658+ logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1659 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl

1660 -- for each constraint, build a top level function to chase it

1661 logLvl 5 $ "Building functions"

@@ -1697,7 +1697,7 @@ elabClass info syn doc fc constraints tn ps ds

1697 getMName (PTy _ _ _ _ n _) = nsroot n

1698 tdecl allmeths (PTy doc syn _ o n t)

1699 = do t' <- implicit' syn allmeths n t

1700− logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp Nothing True False t'

1700+ logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

1701 return ( (n, (toExp (map fst ps) Exp t')),

1702 (n, (doc, o, (toExp (map fst ps) Imp t'))),

1703 (n, (syn, o, t) ) )

@@ -1734,8 +1734,8 @@ elabClass info syn doc fc constraints tn ps ds

1734 let lhs = PApp fc (PRef fc cfn) [pconst capp]

1735 let rhs = PResolveTC (fileFC "HACK")

1736 let ty = PPi constraint (sMN 0 "pc") c con

1737− iLOG (showImp Nothing True False ty)

1737+ iLOG (showTmImpls ty)

1738− iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)

1738+ iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

1739 i <- getIState

1740 let conn = case con of

1741 PRef _ n -> n

@@ -1759,9 +1759,9 @@ elabClass info syn doc fc constraints tn ps ds

1759 let anames = map (\x -> sMN x "arg") [0..]

1760 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

1761 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

1762− iLOG (showImp Nothing True False ty)

1762+ iLOG (showTmImpls ty)

1763 iLOG (show (m, ty', capp, margs))

1764− iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)

1764+ iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

1765 return [PTy doc syn fc o m ty',

1766 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

1767

@@ -1849,7 +1849,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

1849 let wbTys = map mkTyDecl mtys

1850 let wbVals = map (decorateid (decorate ns iname)) ds'

1851 let wb = wbTys ++ wbVals

1852− logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys)

1852+ logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp True . mkTyDecl) mtys)

1853 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

1854 show (concat (nub wparams))

1855 let lhs = PRef fc iname

@@ -2156,8 +2156,8 @@ elabCaseBlock info opts d@(PClauses f o n ps)

2156

2157checkInferred :: FC -> PTerm -> PTerm -> Idris ()

2158checkInferred fc inf user =

2159− do logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n\nFROM\n\n" ++

2159+ do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++

2160− showImp Nothing True False user

2160+ showTmImpls user

2161 logLvl 10 $ "Checking match"

2162 i <- getIState

2163 tclift $ case matchClause' True i user inf of

@@ -2174,8 +2174,8 @@ checkInferred fc inf user =

2174inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

2175inferredDiff fc inf user =

2176 do i <- getIState

2177− logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n" ++

2177+ logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n" ++

2178− showImp Nothing True False user

2178+ showTmImpls user

2179 tclift $ case matchClause' True i user inf of

2180 Right vs -> return False

2181 Left (x, y) -> return True

src/Idris/IdeSlave.hs+17

@@ -69,6 +69,23 @@ instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where

69instance (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) where

70 toSExp (l, m, n, o) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o]

72+instance SExpable NameOutput where

73+ toSExp TypeOutput = SymbolAtom "type"

74+ toSExp FunOutput = SymbolAtom "function"

75+ toSExp DataOutput = SymbolAtom "data"

76+

77+instance SExpable OutputAnnotation where

78+ toSExp (AnnName n Nothing _) = toSExp [(SymbolAtom "name", StringAtom (show n)),

79+ (SymbolAtom "implicit", BoolAtom False)]

80+ toSExp (AnnName n (Just ty) _) = toSExp [(SymbolAtom "name", StringAtom (show n)),

81+ (SymbolAtom "decor", toSExp ty),

82+ (SymbolAtom "implicit", BoolAtom False)]

83+ toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),

84+ (SymbolAtom "decor", SymbolAtom "bound"),

85+ (SymbolAtom "implicit", BoolAtom imp)]

86+ toSExp AnnConstData = toSExp [(SymbolAtom "decor", SymbolAtom "data")]

87+ toSExp AnnConstType = toSExp [(SymbolAtom "decor", SymbolAtom "type")]

88+

72escape :: String -> String

89escape :: String -> String

73escape = concatMap escapeChar

90escape = concatMap escapeChar

74 where

91 where

src/Idris/Parser.hs+1−1

@@ -1062,7 +1062,7 @@ loadSource h lidr f

1062 f file pos

1063 unless (null ds') $ do

1064 let ds = namespaces mname ds'

1065− logLvl 3 (showDecls True ds)

1065+ logLvl 3 (show $ showDecls True ds)

1066 i <- getIState

1067 logLvl 10 (show (toAlist (idris_implicits i)))

1068 logLvl 3 (show (idris_infixes i))

src/Idris/Prover.hs+28−23

@@ -89,47 +89,52 @@ elabStep st e = do case runStateT e st of

90dumpState :: IState -> ProofState -> Idris ()

91dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

92+ iputGoal . renderPretty 0.7 breakingSize $

92− iputGoal . render $ pretty nm <> colon <+> text "No more goals."

93+ prettyName False [] nm <> colon <+> text "No more goals."

93dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do

94dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do

94 let OK ty = goalAtFocus ps

95 let OK ty = goalAtFocus ps

95 let OK env = envAtFocus ps

96 let OK env = envAtFocus ps

96− iputGoal . render $

97+ iputGoal . renderPretty 0.7 breakingSize $

97− prettyOtherGoals hs $$

98+ prettyOtherGoals hs <> line <>

98− prettyAssumptions env $$

99+ prettyAssumptions env <> line <>

99− prettyGoal ty

100+ prettyGoal (zip (assumptionNames env) (repeat False)) ty

100 where

101 where

101 -- XXX

102 -- XXX

102− tPretty t = pretty $ delab ist t

103+ tPretty bnd t = pprintPTerm True bnd $ delab ist t

103

104

104− prettyPs [] = empty

105+ assumptionNames :: Env -> [Name]

105− prettyPs ((MN _ r, _) : bs)

106+ assumptionNames = map fst

106− | r == txt "rewrite_rule" = prettyPs bs

107− prettyPs ((n, Let t v) : bs) =

108− nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>

109− tPretty t $$ prettyPs bs)

110− prettyPs ((n, b) : bs) =

111− pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs

112

107

113− prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v

108+ prettyPs :: [(Name, Bool)] -> Env -> Doc OutputAnnotation

114− prettyG b = tPretty $ binderTy b

109+ prettyPs bnd [] = empty

110+ prettyPs bnd ((n@(MN _ r), _) : bs)

111+ | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs

112+ prettyPs bnd ((n, Let t v) : bs) =

113+ nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>

114+ tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)

115+ prettyPs bnd ((n, b) : bs) =

116+ line <> bindingOf n False <+> colon <+> tPretty bnd (binderTy b) <> prettyPs ((n, False):bnd) bs

115

117

118+ prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v

119+ prettyG bnd b = tPretty bnd $ binderTy b

120+

116− prettyGoal ty =

121+ prettyGoal bnd ty =

117− text "---------- Goal: ----------" $$

122+ text "---------- Goal: ----------" <$$>

118− pretty h <> colon $$ nest nestingSize (prettyG ty)

123+ bindingOf h False <+> colon <+> nest nestingSize (prettyG bnd ty)

119

124

120 prettyAssumptions env =

125 prettyAssumptions env =

121 if length env == 0 then

126 if length env == 0 then

122 empty

127 empty

123 else

128 else

124− text "---------- Assumptions: ----------" $$

129+ text "---------- Assumptions: ----------" <>

125− nest nestingSize (prettyPs $ reverse env)

130+ nest nestingSize (prettyPs [] $ reverse env)

126

131

127 prettyOtherGoals hs =

132 prettyOtherGoals hs =

128 if length hs == 0 then

133 if length hs == 0 then

129 empty

134 empty

130 else

135 else

131− text "---------- Other goals: ----------" $$

136+ text "---------- Other goals: ----------" <$$>

132− pretty hs

137+ nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)

133

138

134lifte :: ElabState [PDecl] -> ElabD a -> Idris a

139lifte :: ElabState [PDecl] -> ElabD a -> Idris a

135lifte st e = do (v, _) <- elabStep st e

140lifte st e = do (v, _) <- elabStep st e

src/Idris/REPL.hs+23−27

@@ -448,10 +448,11 @@ process h fn (Eval t)

448 ist <- getIState

449 logLvl 3 $ "Raw: " ++ show (tm', ty')

450 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

451− imp <- impShow

451+ let imp = opt_showimp (idris_options ist)

452− c <- colourise

452+ tmDoc = prettyImp imp (delab ist tm')

453− ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++

454− showImp (Just ist) imp c (delab ist ty'))

453+ tyDoc = prettyImp imp (delab ist ty')

454+ ihPrintTermWithType h tmDoc tyDoc

455+

455process h fn (ExecVal t)

456process h fn (ExecVal t)

456 = do ctxt <- getContext

457 = do ctxt <- getContext

457 ist <- getIState

458 ist <- getIState

@@ -459,10 +460,8 @@ process h fn (ExecVal t)

459-- let tm' = normaliseAll ctxt [] tm

460-- let tm' = normaliseAll ctxt [] tm

460 let ty' = normaliseAll ctxt [] ty

461 let ty' = normaliseAll ctxt [] ty

461 res <- execute tm

462 res <- execute tm

462− imp <- impShow

463− c <- colourise

464− ihPrintResult h (showImp (Just ist) imp c (delab ist res) ++ " : " ++

463+ ihPrintResult h (showTm ist (delab ist res) ++ " : " ++

465− showImp (Just ist) imp c (delab ist ty'))

464+ showTm ist (delab ist ty'))

466process h fn (Check (PRef _ n))

465process h fn (Check (PRef _ n))

467 = do ctxt <- getContext

466 = do ctxt <- getContext

468 ist <- getIState

467 ist <- getIState

@@ -472,9 +471,7 @@ process h fn (Check (PRef _ n))

472 ts@(t:_) ->

471 ts@(t:_) ->

473 case lookup t (idris_metavars ist) of

472 case lookup t (idris_metavars ist) of

474 Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)

473 Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)

475− Nothing -> ihPrintResult h $

474+ Nothing -> ihPrintFunTypes h n (map (\n -> (n, delabTy ist n)) ts)

476− concat . intersperse "\n" . map (\n -> showName (Just ist) [] False c n ++ " : " ++

477− showImp (Just ist) imp c (delabTy ist n)) $ ts

478 [] -> ihPrintError h $ "No such variable " ++ show n

475 [] -> ihPrintError h $ "No such variable " ++ show n

479 where

476 where

480 showMetavarInfo c imp ist n i

477 showMetavarInfo c imp ist n i

@@ -487,27 +484,27 @@ process h fn (Check (PRef _ n))

487 MN _ _ -> "_"

484 MN _ _ -> "_"

488 UN nm | ('_':'_':_) <- str nm -> "_"

485 UN nm | ('_':'_':_) <- str nm -> "_"

489 _ -> showName (Just ist) [] False c n) ++

486 _ -> showName (Just ist) [] False c n) ++

490− " : " ++ showImp (Just ist) imp c t ++ "\n"

487+ " : " ++ showTm ist t ++ "\n"

491 in

488 in

492 current ++ putTy c imp ist (i-1) sc

489 current ++ putTy c imp ist (i-1) sc

493 putTy c imp ist _ sc = putGoal c imp ist sc

490 putTy c imp ist _ sc = putGoal c imp ist sc

494 putGoal c imp ist g

491 putGoal c imp ist g

495 = "--------------------------------------\n" ++

492 = "--------------------------------------\n" ++

496 showName (Just ist) [] False c n ++ " : " ++

493 showName (Just ist) [] False c n ++ " : " ++

497− showImp (Just ist) imp c g

494+ showTm ist g

498

495

499

496

500process h fn (Check t)

497process h fn (Check t)

501 = do (tm, ty) <- elabVal toplevel False t

498 = do (tm, ty) <- elabVal toplevel False t

502 ctxt <- getContext

499 ctxt <- getContext

503 ist <- getIState

500 ist <- getIState

504− imp <- impShow

501+ let imp = opt_showimp (idris_options ist)

505− c <- colourise

506− let ty' = normaliseC ctxt [] ty

502+ ty' = normaliseC ctxt [] ty

507 case tm of

503 case tm of

508− TType _ -> ihPrintResult h ("Type : Type 1")

504+ TType _ ->

509− _ -> ihPrintResult h (showImp (Just ist) imp c (delab ist tm) ++ " : " ++

505+ ihPrintTermWithType h (prettyImp imp PType) type1Doc

506+ _ -> ihPrintTermWithType h (prettyImp imp (delab ist tm))

510− showImp (Just ist) imp c (delab ist ty))

507+ (prettyImp imp (delab ist ty))

511

508

512process h fn (DocStr n)

509process h fn (DocStr n)

513 = do i <- getIState

510 = do i <- getIState

@@ -540,9 +537,9 @@ process h fn (Defn n)

540 [t] -> iputStrLn (showTotal t i)

537 [t] -> iputStrLn (showTotal t i)

541 _ -> return ()

538 _ -> return ()

542 where printCase i (_, lhs, rhs)

539 where printCase i (_, lhs, rhs)

543− = do c <- colourise

540+ = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

544− iputStrLn (showImp (Just i) True c (delab i lhs) ++ " = " ++

541+ in iputStrLn (showTm i' (delab i lhs) ++ " = " ++

545− showImp (Just i) True c (delab i rhs))

542+ showTm i' (delab i rhs))

546process h fn (TotCheck n)

543process h fn (TotCheck n)

547 = do i <- getIState

544 = do i <- getIState

548 case lookupNameTotal n (tt_ctxt i) of

545 case lookupNameTotal n (tt_ctxt i) of

@@ -848,7 +845,7 @@ process h fn (TestInline t)

848 let tm' = inlineTerm ist tm

845 let tm' = inlineTerm ist tm

849 imp <- impShow

846 imp <- impShow

850 c <- colourise

847 c <- colourise

851− iPrintResult (showImp (Just ist) imp c (delab ist tm'))

848+ iPrintResult (showTm ist (delab ist tm'))

852process h fn Execute

849process h fn Execute

853 = do (m, _) <- elabVal toplevel False

850 = do (m, _) <- elabVal toplevel False

854 (PApp fc

851 (PApp fc

@@ -876,11 +873,11 @@ process h fn (Pattelab t)

876

873

877process h fn (Missing n)

874process h fn (Missing n)

878 = do i <- getIState

875 = do i <- getIState

879− c <- colourise

876+ let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

880 case lookupCtxt n (idris_patdefs i) of

877 case lookupCtxt n (idris_patdefs i) of

881 [] -> return ()

878 [] -> return ()

882 [(_, tms)] ->

879 [(_, tms)] ->

883− iPrintResult (showSep "\n" (map (showImp (Just i) True c) tms))

880+ iPrintResult (showSep "\n" (map (showTm i') tms))

884 _ -> iPrintError $ "Ambiguous name"

881 _ -> iPrintError $ "Ambiguous name"

885process h fn (DynamicLink l)

882process h fn (DynamicLink l)

886 = do i <- getIState

883 = do i <- getIState

@@ -949,9 +946,8 @@ dumpDefaultInstance (PInstance _ _ _ _ _ t _ _) = iputStrLn $ show t

949dumpInstance :: Name -> Idris ()

946dumpInstance :: Name -> Idris ()

950dumpInstance n = do i <- getIState

947dumpInstance n = do i <- getIState

951 ctxt <- getContext

948 ctxt <- getContext

952− imp <- impShow

953 case lookupTy n ctxt of

949 case lookupTy n ctxt of

954− ts -> mapM_ (\t -> iputStrLn $ showImp Nothing imp False (delab i t)) ts

950+ ts -> mapM_ (\t -> iputStrLn $ showTm i (delab i t)) ts

955

951

956showTotal :: Totality -> IState -> String

952showTotal :: Totality -> IState -> String

957showTotal t@(Partial (Other ns)) i

953showTotal t@(Partial (Other ns)) i

src/Util/Pretty.hs+5−8

@@ -1,10 +1,11 @@

1module Util.Pretty (

2− module Text.PrettyPrint.HughesPJ,

2+ module Text.PrettyPrint.Annotated.Leijen,

3 Sized(..), breakingSize, nestingSize,

4 Pretty(..)

5) where

7−import Text.PrettyPrint.HughesPJ

7+--import Text.PrettyPrint.HughesPJ

8+import Text.PrettyPrint.Annotated.Leijen

9-- A rough notion of size for pretty printing various types.

10-- A rough notion of size for pretty printing various types.

10class Sized a where

11class Sized a where

@@ -23,11 +24,7 @@ breakingSize = 15

23nestingSize :: Int

24nestingSize :: Int

24nestingSize = 1

25nestingSize = 1

26−class Pretty a where

27+class Pretty a ty where

27− pretty :: a -> Doc

28+ pretty :: a -> Doc ty

29−instance Pretty () where

30− pretty () = text "()"

32−instance Pretty a => Pretty [a] where

33− pretty l = foldr ($$) empty $ map pretty l

test/reg007/expected+6−7

@@ -1,13 +1,12 @@

1reg007.lidr:8:1:A.n is already defined

2reg007.lidr:12:9:When elaborating right hand side of hurrah:

3Can't unify

4− [92mn[0m[94m = [0m[92mlala[0m

4+ n = lala

5with

6− [91m0[0m[94m = [0m[91m1[0m

6+ 0 = 1

8Specifically:

9− Can't unify

9+ Can't unify

10− [91m1[0m

10+ 1

11− with

11+ with

12− [91m0[0m

12+ 0

13−

test/reg007/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris --check $@ reg007.lidr

2+idris --nocolour --check $@ reg007.lidr

3rm -f *.ibc

test/reg010/expected+6−7

@@ -1,12 +1,11 @@

1reg010.idr:5:15:When elaborating right hand side of usubst.unsafeSubst:

2Can't unify

3− P x

3+ P x

4with

5− P y

5+ P y

7Specifically:

8− Can't unify

8+ Can't unify

9− P x

9+ P x

10− with

10+ with

11− P y

11+ P y

12−

test/reg023/expected+6−7

@@ -1,12 +1,11 @@

1reg023.idr:7:5:When elaborating right hand side of bad:

2Can't unify

3− [94mNat[0m

3+ [94mNat[0m

4with

5− [92mf[0m [94mNat[0m

5+ [92mf[0m [94mNat[0m

7Specifically:

8− Can't unify

8+ Can't unify

9− [94mNat[0m

9+ [94mNat[0m

10− with

10+ with

11− [92mf[0m [94mNat[0m

11+ [92mf[0m [94mNat[0m

12−

test/test020/expected+6−7

@@ -1,14 +1,13 @@

1When elaborating right hand side of foo:

2test020a.idr:14:18:Can't unify

3− Vect n a

3+ Vect n a

4with

5− List a

5+ List a

7Specifically:

8− Can't unify

8+ Can't unify

9− Vect n a

9+ Vect n a

10− with

10+ with

11− List a

11+ List a

12−

13[3, 2, 1]

12[3, 2, 1]

14"Number 42"

13"Number 42"

test/test030/expected+6−7

@@ -1,12 +1,11 @@

1test030a.idr:12:14:When elaborating right hand side of testReflect1:

2Can't unify

3− IsJust (Just x)

3+ IsJust (Just x)

4with

5− IsJust (prove (getProof x))

5+ IsJust (prove (getProof x))

7Specifically:

8− Can't unify

8+ Can't unify

9− Just x

9+ Just x

10− with

10+ with

11− Nothing

11+ Nothing

12−

test/test037/expected+13−14

@@ -1,18 +1,17 @@

1In file ErrorReflection.idr line 78 column 5

2− When elaborating right hand side of Main.bad :

2+ When elaborating right hand side of Main.bad :

3− DSL type error: (t'(504) => t'(504)) doesn't match ()

3+ DSL type error: (t'(504) => t'(504)) doesn't match ()

5Original error:

7− ErrorReflection.idr:78:5:When elaborating right hand side of bad:

7+ ErrorReflection.idr:78:5:When elaborating right hand side of bad:

8− Can't unify

8+ Can't unify

9− Tm [] (Main.TFun t' t')

9+ Tm [] (TFun t' t')

10− with

10+ with

11− Tm [] Main.TUnit

11+ Tm [] TUnit

12−

12+

13− Specifically:

13+ Specifically:

14− Can't unify

14+ Can't unify

15− Main.TFun t' t'

15+ TFun t' t'

16− with

16+ with

17− Main.TUnit

17+ TUnit

18−