@@ -32,6 +32,8 @@ import Data.Word (Word)
3232
3333import Debug.Trace
3434
35+import Text.PrettyPrint.Annotated.Leijen
36+
3537data IOption = IOption { opt_logLevel :: Int,
3638 opt_typecase :: Bool,
3739 opt_typeintype :: Bool,
@@ -916,275 +918,440 @@ expandNS syn n = case syn_namespace syn of
916918 xs -> sNS n xs
917919
918920
919−--- Pretty printing declarations and terms
921+-- For inferring types of things
920922
921−instance Show PTerm where
922− show tm = showImp Nothing False False tm
923+bi = fileFC "builtin"
923924
924−instance Pretty PTerm where
925− pretty = prettyImp False
925+inferTy = sMN 0 "__Infer"
926+inferCon = sMN 0 "__infer"
927+inferDecl = PDatadecl inferTy
928+ PType
929+ [("", inferCon, PPi impl (sMN 0 "iType") PType (
930+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
931+ (PRef bi inferTy)), bi, [])]
932+inferOpts = []
926933
927−instance Show PDecl where
928− show d = showDeclImp False d
934+infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
935+infP = P (TCon 6 0) inferTy (TType (UVal 0))
929936
930−instance Show PClause where
931− show c = showCImp True c
937+getInferTerm, getInferType :: Term -> Term
938+getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
939+getInferTerm (App (App _ _) tm) = tm
940+getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
932941
933−instance Show PData where
934− show d = showDImp False d
942+getInferType (Bind n b sc) = Bind n b $ getInferType sc
943+getInferType (App (App _ ty) _) = ty
935944
936−showDecls :: Bool -> [PDecl] -> String
937−showDecls _ [] = ""
938−showDecls i (d:ds) = showDeclImp i d ++ "\n" ++ showDecls i ds
939945
940−showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
941−showDeclImp i (PTy _ _ _ _ n t) = "tydecl " ++ showCG n ++ " : " ++ showImp Nothing i False t
942−showDeclImp i (PClauses _ _ n cs) = "pat " ++ showCG n ++ "\t" ++ showSep "\n\t" (map (showCImp i) cs)
943−showDeclImp _ (PData _ _ _ _ d) = showDImp True d
944−showDeclImp i (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ showDecls i ps ++ "}\n"
945−showDeclImp i (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ showDecls i ps ++ "}\n"
946−showDeclImp _ (PSyntax _ syn) = "syntax " ++ show syn
947−showDeclImp i (PClass _ _ _ cs n ps ds)
948− = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ showDecls i ds
949−showDeclImp i (PInstance _ _ cs n _ t _ ds)
950− = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ showDecls i ds
951−showDeclImp _ _ = "..."
952−-- showDeclImp (PImport i) = "import " ++ i
953946
947+-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
954948
955−showCImp :: Bool -> PClause -> String
956−showCImp impl (PClause _ n l ws r w)
957− = showImp Nothing impl False l ++ showWs ws ++ " = " ++ showImp Nothing impl False r
958− ++ " where " ++ show w
959− where
960− showWs [] = ""
961− showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs
962−showCImp impl (PWith _ n l ws r w)
963− = showImp Nothing impl False l ++ showWs ws ++ " with " ++ showImp Nothing impl False r
964− ++ " { " ++ show w ++ " } "
965− where
966− showWs [] = ""
967− showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs
949+primNames = [unitTy, unitCon,
950+ falseTy, pairTy, pairCon,
951+ eqTy, eqCon, inferTy, inferCon]
968952
953+unitTy = sMN 0 "__Unit"
954+unitCon = sMN 0 "__II"
955+unitDecl = PDatadecl unitTy PType
956+ [("", unitCon, PRef bi unitTy, bi, [])]
957+unitOpts = [DefaultEliminator]
969958
970−showDImp :: Bool -> PData -> String
971−showDImp impl (PDatadecl n ty cons)
972− = "data " ++ show n ++ " : " ++ showImp Nothing impl False ty ++ " where\n\t"
973− ++ showSep "\n\t| "
974− (map (\ (_, n, t, _, _) -> show n ++ " : " ++ showImp Nothing impl False t) cons)
959+falseTy = sMN 0 "__False"
960+falseDecl = PDatadecl falseTy PType []
961+falseOpts = []
975962
976−getImps :: [PArg] -> [(Name, PTerm)]
977−getImps [] = []
978−getImps (PImp _ _ _ n tm _ : xs) = (n, tm) : getImps xs
979−getImps (_ : xs) = getImps xs
963+pairTy = sMN 0 "__Pair"
964+pairCon = sMN 0 "__MkPair"
965+pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
966+ [("", pairCon, PPi impl (n "A") PType (
967+ PPi impl (n "B") PType (
968+ PPi expl (n "a") (PRef bi (n "A")) (
969+ PPi expl (n "b") (PRef bi (n "B"))
970+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
971+ pexp (PRef bi (n "B"))])))), bi, [])]
972+ where n a = sMN 0 a
973+pairOpts = []
980974
981−getExps :: [PArg] -> [PTerm]
982−getExps [] = []
983−getExps (PExp _ _ tm _ : xs) = tm : getExps xs
984−getExps (_ : xs) = getExps xs
975+eqTy = sUN "="
976+eqCon = sUN "refl"
977+eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
978+ (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
979+ PType)
980+ [("", eqCon, PPi impl (n "A") PType (
981+ PPi impl (n "x") (PRef bi (n "A"))
982+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
983+ pimp (n "B") Placeholder False,
984+ pexp (PRef bi (n "x")),
985+ pexp (PRef bi (n "x"))])), bi, [])]
986+ where n a = sMN 0 a
987+eqOpts = []
985988
986−getConsts :: [PArg] -> [PTerm]
987−getConsts [] = []
988−getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs
989−getConsts (_ : xs) = getConsts xs
989+elimName = sUN "__Elim"
990+elimMethElimTy = sUN "__elimTy"
991+elimMethElim = sUN "elim"
992+elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
993+ [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,
994+ PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
995+
996+-- Defined in builtins.idr
997+sigmaTy = sUN "Exists"
998+existsCon = sUN "Ex_intro"
999+
1000+piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1001+piBind = piBindp expl
1002+
1003+piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1004+piBindp p [] t = t
1005+piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
9901006
991−getAll :: [PArg] -> [PTerm]
992−getAll = map getTm
9931007
994−-- | Pretty-print a high-level Idris term
1008+-- Pretty-printing declarations and terms
1009+
1010+instance Show PTerm where
1011+ showsPrec _ tm = (displayS . renderCompact . prettyImp False) tm
1012+
1013+instance Show PDecl where
1014+ showsPrec _ d = (displayS . renderCompact . showDeclImp False) d
1015+
1016+instance Show PClause where
1017+ showsPrec _ c = (displayS . renderCompact . showCImp True) c
1018+
1019+instance Show PData where
1020+ showsPrec _ d = (displayS . renderCompact . showDImp False) d
1021+
1022+instance Pretty PTerm OutputAnnotation where
1023+ pretty = prettyImp False
1024+
1025+-- | Colourise annotations according to an Idris state. It ignores the names
1026+-- in the annotation, as there's no good way to show extended information on a
1027+-- terminal.
1028+consoleDecorate :: IState -> OutputAnnotation -> String -> String
1029+consoleDecorate ist _ | not (idris_colourRepl ist) = id
1030+consoleDecorate ist AnnConstData = let theme = idris_colourTheme ist
1031+ in colouriseData theme
1032+consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist
1033+ in colouriseType theme
1034+consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1035+consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1036+consoleDecorate ist (AnnName n _ _) = let ctxt = tt_ctxt ist
1037+ theme = idris_colourTheme ist
1038+ in case () of
1039+ _ | isDConName n ctxt -> colouriseData theme
1040+ _ | isFnName n ctxt -> colouriseFun theme
1041+ _ | isTConName n ctxt -> colouriseType theme
1042+ _ | otherwise -> id -- don't colourise unknown names
1043+consoleDecorate ist (AnnFC _) = id
1044+
1045+-- | Pretty-print a high-level closed Idris term
9951046prettyImp :: Bool -- ^^ whether to show implicits
9961047 -> PTerm -- ^^ the term to pretty-print
997− -> Doc
998−prettyImp impl = prettySe 10
1048+ -> Doc OutputAnnotation
1049+prettyImp impl = pprintPTerm impl []
1050+
1051+-- | Pretty-print a high-level Idris term in some bindings context
1052+pprintPTerm :: Bool -- ^^ whether to show implicits
1053+ -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1054+ -> PTerm -- ^^ the term to pretty-print
1055+ -> Doc OutputAnnotation
1056+pprintPTerm impl bnd = prettySe 10 bnd
9991057 where
1000− prettySe p (PQuote r) =
1058+ prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1059+ prettySe p bnd (PQuote r) =
10011060 if size r > breakingSize then
1002− text "![" $$ pretty r <> text "]"
1061+ text "![" <> line <> pretty r <> text "]"
10031062 else
10041063 text "![" <> pretty r <> text "]"
1005− prettySe p (PPatvar fc n) = pretty n
1006− prettySe p (PRef fc n) =
1007− if impl then
1008− pretty n
1009− else
1010− prettyBasic n
1011− where
1012− prettyBasic n@(UN _) = pretty n
1013− prettyBasic (MN _ s) = text (str s)
1014− prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map (text.str) $ reverse s))) <> prettyBasic n
1015− prettyBasic (SN sn) = text (show sn)
1016− prettySe p (PLam n ty sc) =
1064+ prettySe p bnd (PPatvar fc n) = pretty n
1065+ prettySe p bnd e
1066+ | Just str <- slist p bnd e = str
1067+ | Just n <- snat p e = annotate AnnConstData (text (show n))
1068+ prettySe p bnd (PRef fc n) = prettyName impl bnd n
1069+ prettySe p bnd (PLam n ty sc) =
10171070 bracket p 2 $
10181071 if size sc > breakingSize then
1019− text "λ" <> pretty n <+> text "=>" $+$ pretty sc
1072+ text "\\" <> bindingOf n False <+> text "=>" <> line <> prettySe 10 ((n, False):bnd) sc
10201073 else
1021− text "λ" <> pretty n <+> text "=>" <+> pretty sc
1022− prettySe p (PLet n ty v sc) =
1074+ text "\\" <> bindingOf n False <+> text "=>" <+> prettySe 10 ((n, False):bnd) sc
1075+ prettySe p bnd (PLet n ty v sc) =
10231076 bracket p 2 $
10241077 if size sc > breakingSize then
1025− text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
1026− nest nestingSize (prettySe 10 sc)
1078+ text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <>
1079+ nest nestingSize (prettySe 10 ((n, False):bnd) sc)
10271080 else
1028− text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
1029− prettySe 10 sc
1030− prettySe p (PPi (Exp l s _ _) n ty sc)
1081+ text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <+>
1082+ prettySe 10 ((n, False):bnd) sc
1083+ prettySe p bnd (PPi (Exp l s _ _) n ty sc)
10311084 | n `elem` allNamesIn sc || impl =
10321085 let open = if Lazy `elem` l then text "|" <> lparen else lparen in
10331086 bracket p 2 $
10341087 if size sc > breakingSize then
1035− open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
1036− st <+> text "->" $+$ prettySe 10 sc
1088+ enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1089+ st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc
10371090 else
1038− open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
1039− st <+> text "->" <+> prettySe 10 sc
1091+ enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1092+ st <> text "->" <+> prettySe 10 ((n, False):bnd) sc
10401093 | otherwise =
10411094 bracket p 2 $
10421095 if size sc > breakingSize then
1043− prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
1096+ prettySe 0 bnd ty <+> st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc
10441097 else
1045− prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
1098+ prettySe 0 bnd ty <+> st <> text "->" <+> prettySe 10 ((n, False):bnd) sc
10461099 where
10471100 st =
10481101 case s of
1049− Static -> text "[static]"
1102+ Static -> text "[static]" <> space
10501103 _ -> empty
1051− prettySe p (PPi (Imp l s _ _) n ty sc)
1104+ prettySe p bnd (PPi (Imp l s _ _) n ty sc)
10521105 | impl =
10531106 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in
10541107 bracket p 2 $
10551108 if size sc > breakingSize then
1056− open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
1057− st <+> text "->" <+> prettySe 10 sc
1109+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1110+ st <> text "->" <+> prettySe 10 ((n, True):bnd) sc
10581111 else
1059− open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
1060− st <+> text "->" <+> prettySe 10 sc
1061− | otherwise = prettySe 10 sc
1112+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1113+ st <> text "->" <+> prettySe 10 ((n, True):bnd) sc
1114+ | otherwise = prettySe 10 ((n, True):bnd) sc
10621115 where
10631116 st =
10641117 case s of
1065− Static -> text $ "[static]"
1118+ Static -> text "[static]" <> space
10661119 _ -> empty
1067− prettySe p (PPi (Constraint _ _ _) n ty sc) =
1120+ prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =
10681121 bracket p 2 $
10691122 if size sc > breakingSize then
1070− prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
1123+ prettySe 10 bnd ty <+> text "=>" <+> prettySe 10 ((n, True):bnd) sc
10711124 else
1072− prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
1073− prettySe p (PPi (TacImp _ _ s _) n ty sc) =
1125+ prettySe 10 bnd ty <+> text "=>" <> line <> prettySe 10 ((n, True):bnd) sc
1126+ prettySe p bnd (PPi (TacImp _ _ s _) n ty sc) =
10741127 bracket p 2 $
10751128 if size sc > breakingSize then
1076− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
1077− rbrace <+> text "->" $+$ prettySe 10 sc
1129+ lbrace <> text "tacimp" <+> bindingOf n True <+> colon <+> prettySe 10 bnd ty <>
1130+ rbrace <+> text "->" <> line <> prettySe 10 ((n, True):bnd) sc
10781131 else
1079− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
1080− rbrace <+> text "->" <+> prettySe 10 sc
1081− prettySe p (PApp _ (PRef _ f) [])
1082− | not impl = pretty f
1083− prettySe p (PAppBind _ (PRef _ f) [])
1084− | not impl = text "!" <+> pretty f
1085− prettySe p (PApp _ (PRef _ op@(UN nm)) args)
1086− | not (tnull nm) &&
1132+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1133+ rbrace <+> text "->" <+> prettySe 10 ((n, True):bnd) sc
1134+ prettySe p bnd (PApp _ (PRef _ f) [])
1135+ | not impl = prettyName impl bnd f
1136+ prettySe p bnd (PAppBind _ (PRef _ f) [])
1137+ | not impl = text "!" <> prettyName impl bnd f
1138+ prettySe p bnd (PApp _ (PRef _ op) args)
1139+ | UN nm <- basename op
1140+ , not (tnull nm) &&
10871141 length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =
10881142 let [l, r] = getExps args in
10891143 bracket p 1 $
10901144 if size r > breakingSize then
1091− prettySe 1 l <+> pretty op $+$ prettySe 0 r
1145+ prettySe 1 bnd l <+> prettyName impl bnd op <> line <> prettySe 0 bnd r
10921146 else
1093− prettySe 1 l <+> pretty op <+> prettySe 0 r
1094− prettySe p (PApp _ f as) =
1095− let args = getExps as in
1147+ prettySe 1 bnd l <+> prettyName impl bnd op <+> prettySe 0 bnd r
1148+ prettySe p bnd (PApp _ hd@(PRef fc f) [tm])
1149+ | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1150+ f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1151+ prettySe p bnd (PApp _ f as) =
1152+ let args = getExps as
1153+ fp = prettySe 1 bnd f
1154+ in
10961155 bracket p 1 $
1097− prettySe 1 f <+>
1098− if impl then
1099− foldl' fS empty as
1100− -- foldr (<+>) empty $ map prettyArgS as
1101− else
1102− foldl' fSe empty args
1103− -- foldr (<+>) empty $ map prettyArgSe args
1156+ hsep (if impl
1157+ then fp : map (prettyArgS bnd) as
1158+ else fp : map (prettyArgSe bnd) args)
1159+ prettySe p bnd (PCase _ scr opts) =
1160+ text "case" <+> prettySe 10 bnd scr <+> text "of" <> prettyBody
11041161 where
1105− fS l r =
1106− if size r > breakingSize then
1107− l $+$ nest nestingSize (prettyArgS r)
1108− else
1109− l <+> prettyArgS r
1110−
1111− fSe l r =
1112− if size r > breakingSize then
1113− l $+$ nest nestingSize (prettyArgSe r)
1114− else
1115− l <+> prettyArgSe r
1116− prettySe p (PCase _ scr opts) =
1117− text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
1118− where
1119− prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
1120−
1121− sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
1122− prettySe p (PHidden tm) = text "." <> prettySe 0 tm
1123− prettySe p (PRefl _ _) = text "refl"
1124− prettySe p (PResolveTC _) = text "resolvetc"
1125− prettySe p (PTrue _) = text "()"
1126− prettySe p (PFalse _) = text "_|_"
1127− prettySe p (PEq _ l r) =
1162+ prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1163+
1164+ sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1165+ prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1166+ prettySe p bnd (PRefl _ _) = annotate (AnnName eqCon Nothing Nothing) $ text "refl"
1167+ prettySe p bnd (PResolveTC _) = text "resolvetc"
1168+ prettySe p bnd (PTrue _) = annotate (AnnName unitTy Nothing Nothing) $ text "()"
1169+ prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"
1170+ prettySe p bnd (PEq _ l r) =
11281171 bracket p 2 $
11291172 if size r > breakingSize then
1130− prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
1173+ prettySe 10 bnd l <+> eq <$> nest nestingSize (prettySe 10 bnd r)
11311174 else
1132− prettySe 10 l <+> text "=" <+> prettySe 10 r
1133− prettySe p (PRewrite _ l r _) =
1175+ prettySe 10 bnd l <+> eq <+> prettySe 10 bnd r
1176+ where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")
1177+ prettySe p bnd (PRewrite _ l r _) =
11341178 bracket p 2 $
11351179 if size r > breakingSize then
1136− text "rewrite" <+> prettySe 10 l <+> text "in" $$ nest nestingSize (prettySe 10 r)
1180+ text "rewrite" <+> prettySe 10 bnd l <+> text "in" <> nest nestingSize (prettySe 10 bnd r)
11371181 else
1138− text "rewrite" <+> prettySe 10 l <+> text "in" <+> prettySe 10 r
1139− prettySe p (PTyped l r) =
1140− lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
1141− prettySe p (PPair _ l r) =
1182+ text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1183+ prettySe p bnd (PTyped l r) =
1184+ lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1185+ prettySe p bnd (PPair _ l r) =
11421186 if size r > breakingSize then
1143− lparen <> prettySe 10 l <> text "," $+$
1144− prettySe 10 r <> rparen
1187+ lparen <> prettySe 10 bnd l <> text "," <>
1188+ line <> prettySe 10 bnd r <> rparen
11451189 else
1146− lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
1147− prettySe p (PDPair _ l t r) =
1190+ lparen <> prettySe 10 bnd l <> text "," <+> prettySe 10 bnd r <> rparen
1191+ prettySe p bnd (PDPair _ l t r) =
11481192 if size r > breakingSize then
1149− lparen <> prettySe 10 l <+> text "**" $+$
1150− prettySe 10 r <> rparen
1193+ lparen <> prettySe 10 bnd l <+> text "**" <>
1194+ line <> prettySe 10 bnd r <> rparen
11511195 else
1152− lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
1153− prettySe p (PAlternative a as) =
1196+ lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1197+ prettySe p bnd (PAlternative a as) =
11541198 lparen <> text "|" <> prettyAs <> text "|" <> rparen
11551199 where
11561200 prettyAs =
1157− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
1158− prettySe p PType = text "Type"
1159− prettySe p (PConstant c) = pretty c
1201+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1202+ prettySe p bnd PType = annotate AnnConstType $ text "Type"
1203+ prettySe p bnd (PConstant c) = annotate (annot c) (text (show c))
1204+ where annot (AType _) = AnnConstType
1205+ annot StrType = AnnConstType
1206+ annot PtrType = AnnConstType
1207+ annot VoidType = AnnConstType
1208+ annot _ = AnnConstData
11601209 -- XXX: add pretty for tactics
1161− prettySe p (PProof ts) =
1162− text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
1163− prettySe p (PTactics ts) =
1164− text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
1165− prettySe p (PMetavar n) = text "?" <> pretty n
1166− prettySe p (PReturn f) = text "return"
1167− prettySe p PImpossible = text "impossible"
1168− prettySe p Placeholder = text "_"
1169− prettySe p (PDoBlock _) = text "do block pretty not implemented"
1170− prettySe p (PElabError s) = pretty s
1171−
1172− prettySe p _ = text "test"
1173−
1174− prettyArgS (PImp _ _ _ n tm _) = prettyArgSi (n, tm)
1175− prettyArgS (PExp _ _ tm _) = prettyArgSe tm
1176− prettyArgS (PConstraint _ _ tm _) = prettyArgSc tm
1177− prettyArgS (PTacImplicit _ _ n _ tm _) = prettyArgSti (n, tm)
1178−
1179− prettyArgSe arg = prettySe 0 arg
1180− prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
1181− prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
1182− prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
1210+ prettySe p bnd (PProof ts) =
1211+ text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1212+ prettySe p bnd (PTactics ts) =
1213+ text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1214+ prettySe p bnd (PMetavar n) = text "?" <> pretty n
1215+ prettySe p bnd (PReturn f) = text "return"
1216+ prettySe p bnd PImpossible = text "impossible"
1217+ prettySe p bnd Placeholder = text "_"
1218+ prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1219+ prettySe p bnd (PElabError s) = pretty s
1220+
1221+ prettySe p bnd _ = text "test"
1222+
1223+ prettyArgS bnd (PImp _ _ _ n tm _) = prettyArgSi bnd (n, tm)
1224+ prettyArgS bnd (PExp _ _ tm _) = prettyArgSe bnd tm
1225+ prettyArgS bnd (PConstraint _ _ tm _) = prettyArgSc bnd tm
1226+ prettyArgS bnd (PTacImplicit _ _ n _ tm _) = prettyArgSti bnd (n, tm)
1227+
1228+ prettyArgSe bnd arg = prettySe 0 bnd arg
1229+ prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1230+ prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1231+ prettyArgSti bnd (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1232+
1233+ basename :: Name -> Name
1234+ basename (NS n _) = basename n
1235+ basename n = n
1236+
1237+ slist' p bnd (PApp _ (PRef _ nil) _)
1238+ | not impl && nsroot nil == sUN "Nil" = Just []
1239+ slist' p bnd (PApp _ (PRef _ cons) args)
1240+ | nsroot cons == sUN "::",
1241+ (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1242+ all isImp imps,
1243+ Just tl' <- slist' p bnd tl
1244+ = Just (hd:tl')
1245+ where
1246+ isImp (PImp {}) = True
1247+ isImp _ = False
1248+ slist' _ _ _ = Nothing
1249+
1250+ slist p bnd e | Just es <- slist' p bnd e = Just $
1251+ case es of [] -> annotate AnnConstData $ text "[]"
1252+ [x] -> enclose left
1253+ right
1254+ (prettySe p bnd x)
1255+ xs -> (enclose left right . hsep . punctuate comma . map (prettySe p bnd)) xs
1256+ where left = (annotate AnnConstData (text "["))
1257+ right = (annotate AnnConstData (text "]"))
1258+ comma = (annotate AnnConstData (text ","))
1259+ slist _ _ _ = Nothing
1260+
1261+ natns = "Prelude.Nat."
1262+
1263+ snat p (PRef _ z)
1264+ | show z == (natns++"Z") || show z == "Z" = Just 0
1265+ snat p (PApp _ s [PExp {getTm=n}])
1266+ | show s == (natns++"S") || show s == "S",
1267+ Just n' <- snat p n
1268+ = Just $ 1 + n'
1269+ snat _ _ = Nothing
11831270
11841271 bracket outer inner doc
11851272 | inner > outer = lparen <> doc <> rparen
11861273 | otherwise = doc
11871274
1275+-- | Pretty-printer helper for the binding site of a name
1276+bindingOf :: Name -- ^^ the bound name
1277+ -> Bool -- ^^ whether the name is implicit
1278+ -> Doc OutputAnnotation
1279+bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1280+
1281+-- | Pretty-printer helper for names that attaches the correct annotations
1282+prettyName :: Bool -- ^^ whether to show namespaces
1283+ -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1284+ -> Name -- ^^ the name to pprint
1285+ -> Doc OutputAnnotation
1286+prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) (text (strName n))
1287+ | otherwise = annotate (AnnName n Nothing Nothing) (text (strName n))
1288+ where strName (UN n) = T.unpack n
1289+ strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n
1290+ | otherwise = strName n
1291+ strName (MN i s) = T.unpack s
1292+ strName other = show other
1293+
1294+
1295+showCImp :: Bool -> PClause -> Doc OutputAnnotation
1296+showCImp impl (PClause _ n l ws r w)
1297+ = prettyImp impl l <+> showWs ws <+> text "=" <+> prettyImp impl r
1298+ <+> text "where" <+> text (show w)
1299+ where
1300+ showWs [] = empty
1301+ showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs
1302+showCImp impl (PWith _ n l ws r w)
1303+ = prettyImp impl l <+> showWs ws <+> text "with" <+> prettyImp impl r
1304+ <+> braces (text (show w))
1305+ where
1306+ showWs [] = empty
1307+ showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs
1308+
1309+
1310+showDImp :: Bool -> PData -> Doc OutputAnnotation
1311+showDImp impl (PDatadecl n ty cons)
1312+ = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>
1313+ (indent 2 $ vsep (map (\ (_, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))
1314+
1315+showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation
1316+showDecls i ds = vsep (map (showDeclImp i) ds)
1317+
1318+showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1319+showDeclImp i (PTy _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t
1320+showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1321+ indent 2 (vsep (map (showCImp i) cs))
1322+showDeclImp _ (PData _ _ _ _ d) = showDImp True d
1323+showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)
1324+showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)
1325+showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1326+showDeclImp i (PClass _ _ _ cs n ps ds)
1327+ = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls i ds
1328+showDeclImp i (PInstance _ _ cs n _ t _ ds)
1329+ = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp i t <> line <> showDecls i ds
1330+showDeclImp _ _ = text "..."
1331+-- showDeclImp (PImport i) = "import " ++ i
1332+
1333+instance Show (Doc OutputAnnotation) where
1334+ show = flip (displayS . renderCompact) ""
1335+
1336+getImps :: [PArg] -> [(Name, PTerm)]
1337+getImps [] = []
1338+getImps (PImp _ _ _ n tm _ : xs) = (n, tm) : getImps xs
1339+getImps (_ : xs) = getImps xs
1340+
1341+getExps :: [PArg] -> [PTerm]
1342+getExps [] = []
1343+getExps (PExp _ _ tm _ : xs) = tm : getExps xs
1344+getExps (_ : xs) = getExps xs
1345+
1346+getConsts :: [PArg] -> [PTerm]
1347+getConsts [] = []
1348+getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs
1349+getConsts (_ : xs) = getConsts xs
1350+
1351+getAll :: [PArg] -> [PTerm]
1352+getAll = map getTm
1353+
1354+
11881355-- | Show Idris name
11891356showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
11901357 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
@@ -1214,171 +1381,14 @@ showName ist bnd impl colour n = case ist of
12141381 -- (like error messages). Thus, unknown vars are colourised as implicits.
12151382 | otherwise -> colouriseImplicit t name
12161383
1217−-- | Show Idris term
1218−showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers and colours
1219− -> Bool -- ^^ whether to show implicits
1220− -> Bool -- ^^ whether to colourise
1221− -> PTerm -- ^^ the term to show
1222− -> String
1223−showImp ist impl colour tm = se 10 [] tm where
1224− perhapsColourise :: (ColourTheme -> String -> String) -> String -> String
1225− perhapsColourise col str = case ist of
1226− Just i -> if colour then col (idris_colourTheme i) str else str
1227− Nothing -> str
1228−
1229− se :: Int -> [(Name, Bool)] -> PTerm -> String
1230− se p bnd (PQuote r) = "![" ++ show r ++ "]"
1231− se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n
1232− se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
1233− se p bnd e
1234− | Just str <- slist p bnd e = str
1235− | Just num <- snat p e = perhapsColourise colouriseData (show num)
1236− se p bnd (PRef fc n) = showName ist bnd impl colour n
1237− se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++
1238− (if impl then " : " ++ se 10 bnd ty else "") ++ " => "
1239− ++ se 10 ((n, False):bnd) sc
1240− se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++
1241− " = " ++ se 10 bnd v ++
1242− " in " ++ se 10 ((n, False):bnd) sc
1243− se p bnd (PPi (Exp l s _ param) n ty sc)
1244− | n `elem` allNamesIn sc || impl
1245− = bracket p 2 $
1246− (if Lazy `elem` l then "|(" else "(") ++
1247− perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
1248− ") " ++
1249− (if (impl && param) then "P" else "") ++
1250− st ++
1251− "-> " ++ se 10 ((n, False):bnd) sc
1252− | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc
1253− where st = case s of
1254− Static -> "[static] "
1255− _ -> ""
1256− se p bnd (PPi (Imp l s _ _) n ty sc)
1257− | impl = bracket p 2 $ (if Lazy `elem` l then "|{" else "{") ++
1258− perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
1259− "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc
1260− | otherwise = se 10 ((n, True):bnd) sc
1261− where st = case s of
1262− Static -> "[static] "
1263− _ -> ""
1264− se p bnd (PPi (Constraint _ _ _) n ty sc)
1265− = bracket p 2 $ se 10 bnd ty ++ " => " ++ se 10 bnd sc
1266− se p bnd (PPi (TacImp _ _ s _) n ty sc)
1267− = bracket p 2 $
1268− "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++
1269− se 10 ((n, False):bnd) sc
1270− se p bnd (PMatchApp _ f) = "match " ++ show f
1271− se p bnd (PApp _ hd@(PRef fc f) [tm])
1272− | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1273− f == sUN "Symbol_" = "'" ++ se 10 bnd (PRef fc (sUN str))
1274− se p bnd (PApp _ hd@(PRef _ f) [])
1275− | not impl = se p bnd hd
1276− se p bnd (PAppBind _ hd@(PRef _ f) [])
1277− | not impl = "!" ++ se p bnd hd
1278− se p bnd (PApp _ op@(PRef _ (UN nm)) args)
1279− | not (tnull nm) &&
1280− length (getExps args) == 2 && not impl && not (isAlpha (thead nm))
1281− = let [l, r] = getExps args in
1282− bracket p 1 $ se 1 bnd l ++ " " ++ se p bnd op ++ " " ++ se 0 bnd r
1283− se p bnd (PApp _ f as)
1284− = -- let args = getExps as in
1285− bracket p 1 $ se 1 bnd f ++
1286− if impl then concatMap (sArg bnd) as
1287− else concatMap (suiArg impl bnd) as
1288− se p bnd (PAppBind _ f as)
1289− = let args = getExps as in
1290− "!" ++ (bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as
1291− else concatMap (seArg bnd) args)
1292− se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)
1293− where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r
1294− se p bnd (PHidden tm) = "." ++ se 0 bnd tm
1295− se p bnd (PRefl _ t)
1296− | not impl = perhapsColourise colouriseData "refl"
1297− | otherwise = perhapsColourise colouriseData $ "refl {" ++ se 10 bnd t ++ "}"
1298− se p bnd (PResolveTC _) = "resolvetc"
1299− se p bnd (PTrue _) = perhapsColourise colouriseType "()"
1300− se p bnd (PFalse _) = perhapsColourise colouriseType "_|_"
1301− se p bnd (PEq _ l r) = bracket p 2 $ se 10 bnd l ++ perhapsColourise colouriseType " = " ++ se 10 bnd r
1302− se p bnd (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 bnd l ++ " in " ++ se 10 bnd r
1303− se p bnd (PTyped l r) = "(" ++ se 10 bnd l ++ " : " ++ se 10 bnd r ++ ")"
1304− se p bnd (PPair _ l r) = "(" ++ se 10 bnd l ++ ", " ++ se 10 bnd r ++ ")"
1305− se p bnd (PDPair _ l t r) = "(" ++ se 10 bnd l ++ " ** " ++ se 10 bnd r ++ ")"
1306− se p bnd (PAlternative a as) = "(|" ++ showSep " , " (map (se 10 bnd) as) ++ "|)"
1307− se p bnd PType = perhapsColourise colouriseType "Type"
1308− se p bnd (PConstant c) = perhapsColourise (cfun c) (show c)
1309− where cfun (AType _) = colouriseType
1310− cfun StrType = colouriseType
1311− cfun PtrType = colouriseType
1312− cfun VoidType = colouriseType
1313− cfun _ = colouriseData
1314− se p bnd (PProof ts) = "proof { " ++ show ts ++ "}"
1315− se p bnd (PTactics ts) = "tactics { " ++ show ts ++ "}"
1316− se p bnd (PMetavar n) = "?" ++ show n
1317− se p bnd (PReturn f) = "return"
1318− se p bnd PImpossible = "impossible"
1319− se p bnd Placeholder = "_"
1320− se p bnd (PDoBlock _) = "do block show not implemented"
1321− se p bnd (PElabError s) = show s
1322− se p bnd (PCoerced t) = se p bnd t
1323− se p bnd (PUnifyLog t) = "%unifyLog " ++ se p bnd t
1324− se p bnd (PDisamb ns t) = "%disamb " ++ show ns ++ se p bnd t
1325− se p bnd (PNoImplicits t) = "%noimplicit " ++ se p bnd t
1326−-- se p bnd x = "Not implemented"
1327−
1328− slist' p bnd (PApp _ (PRef _ nil) _)
1329− | not impl && nsroot nil == sUN "Nil" = Just []
1330− slist' p bnd (PApp _ (PRef _ cons) args)
1331− | nsroot cons == sUN "::",
1332− (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1333− all isImp imps,
1334− Just tl' <- slist' p bnd tl
1335− = Just (hd:tl')
1336− where
1337− isImp (PImp {}) = True
1338− isImp _ = False
1339− slist' _ _ _ = Nothing
1340−
1341− slist p bnd e | Just es <- slist' p bnd e = Just $
1342− case es of [] -> "[]"
1343− [x] -> "[" ++ se p bnd x ++ "]"
1344− xs -> "[" ++ intercalate "," (map (se p bnd ) xs) ++ "]"
1345− slist _ _ _ = Nothing
1346−
1347− -- since Prelude is always imported, S & Z are unqualified iff they're the
1348− -- Nat ones.
1349− snat p (PRef _ o)
1350− | show o == (natns++"Z") || show o == "Z" = Just 0
1351− snat p (PApp _ s [PExp {getTm=n}])
1352− | show s == (natns++"S") || show s == "S",
1353− Just n' <- snat p n
1354− = Just $ 1 + n'
1355− snat _ _ = Nothing
1356−
1357− natns = "Prelude.Nat."
1384+showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1385+ -> PTerm -- ^^ the term to show
1386+ -> String
1387+showTm ist = displayDecorated (consoleDecorate ist) . renderCompact . prettyImp (opt_showimp (idris_options ist))
13581388
1359− sArg bnd (PImp _ _ _ n tm _) = siArg bnd (n, tm)
1360− sArg bnd (PExp _ _ tm _) = seArg bnd tm
1361− sArg bnd (PConstraint _ _ tm _) = scArg bnd tm
1362− sArg bnd (PTacImplicit _ _ n _ tm _) = stiArg bnd (n, tm)
1363−
1364− -- show argument, implicits given by the user also shown
1365− suiArg impl bnd (PImp _ mi _ n tm _)
1366− | impl || not mi = siArg bnd (n, tm)
1367− suiArg impl bnd (PExp _ _ tm _) = seArg bnd tm
1368− suiArg impl bnd _ = ""
1369−
1370− seArg bnd arg = " " ++ se 0 bnd arg
1371− siArg bnd (n, val) =
1372− let n' = show n
1373− val' = se 10 bnd val in
1374− if (n' == val')
1375− then " {" ++ n' ++ "}"
1376− else " {" ++ n' ++ " = " ++ val' ++ "}"
1377− scArg bnd val = " {{" ++ se 10 bnd val ++ "}}"
1378− stiArg bnd (n, val) = " {auto " ++ show n ++ " = " ++ se 10 bnd val ++ "}"
1379−
1380− bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1381− | otherwise = str
1389+-- | Show a term with implicits, no colours
1390+showTmImpls :: PTerm -> String
1391+showTmImpls = flip (displayS . renderCompact . prettyImp True) ""
13821392
13831393
13841394instance Sized PTerm where