0 | module Core.CompileExpr.Pretty
  1 |
  2 | import Core.CompileExpr
  3 | import Core.TT
  4 | import Data.String
  5 | import Data.Vect
  6 | import Idris.Pretty
  7 | import Idris.Doc.Annotations
  8 |
  9 | %default covering
 10 |
 11 | %hide Vect.(::)
 12 | %hide Vect.Nil
 13 | %hide Vect.catMaybes
 14 | %hide Vect.(++)
 15 |
 16 | %hide Core.Name.prettyOp
 17 |
 18 | %hide CompileExpr.(::)
 19 | %hide CompileExpr.Nil
 20 | %hide String.(::)
 21 | %hide String.Nil
 22 | %hide Doc.Nil
 23 | %hide Subst.(::)
 24 | %hide Subst.Nil
 25 | %hide CList.(::)
 26 | %hide CList.Nil
 27 | %hide Stream.(::)
 28 | %hide Symbols.equals
 29 | %hide Fin.fromInteger
 30 | %hide String.indent
 31 | %hide List1.(++)
 32 | %hide SnocList.(++)
 33 | %hide String.(++)
 34 | %hide Pretty.Syntax
 35 | %hide List1.forget
 36 |
 37 | prettyFlag : ConInfo -> Maybe (Doc ann)
 38 | prettyFlag DATACON = Nothing
 39 | prettyFlag f = Just (byShow f)
 40 |
 41 | prettyCon : Name -> ConInfo -> Maybe Int -> Doc IdrisSyntax
 42 | prettyCon x ci mtag
 43 |   = hsep $ catMaybes
 44 |       [ Just (annotate ((if ci == TYCON then TCon else DCon) (Just x)) (pretty0 x))
 45 |       , (braces . ("tag =" <++>) . byShow) <$> mtag
 46 |       , prettyFlag ci
 47 |       ]
 48 |
 49 | prettyName : Name -> Doc IdrisSyntax
 50 | prettyName = pretty0
 51 |
 52 | mutual
 53 |
 54 |   prettyNamedCExp : NamedCExp -> Doc IdrisSyntax
 55 |   prettyNamedCExp = prettyPrecNamedCExp Open
 56 |
 57 |   prettyPrecNamedCExp : Prec -> NamedCExp -> Doc IdrisSyntax
 58 |   prettyPrecNamedCExp d (NmLocal _ x) = annotate Bound $ prettyName x
 59 |   prettyPrecNamedCExp d (NmRef _ x) = annotate (Fun x) $ prettyName x
 60 |   prettyPrecNamedCExp d (NmLam _ x y)
 61 |     = parenthesise (d > Open) $ keyword "\\" <+> prettyName x <+> fatArrow <++> prettyNamedCExp y
 62 |   prettyPrecNamedCExp d (NmLet _ x y z)
 63 |       = parenthesise (d > Open) $
 64 |           vcat [ let_ <++> prettyName x <++> equals <++> prettyNamedCExp y <++> in_, prettyNamedCExp z ]
 65 |   prettyPrecNamedCExp d (NmApp _ x xs)
 66 |       = parenthesise (d > Open) $
 67 |           sep (prettyNamedCExp x :: map (prettyPrecNamedCExp App) xs)
 68 |   prettyPrecNamedCExp d (NmCon _ x ci tag xs)
 69 |       = parenthesise (d > Open) $
 70 |           sep (prettyCon x ci tag :: map (prettyPrecNamedCExp App) xs)
 71 |   prettyPrecNamedCExp d (NmOp _ op xs)
 72 |       = parenthesise (d > Open) $ prettyOp op $ map (prettyPrecNamedCExp App) xs
 73 |   prettyPrecNamedCExp d (NmExtPrim _ p xs)
 74 |       = parenthesise (d > Open) $
 75 |           sep (annotate (Fun p) (pretty0 p) :: map (prettyPrecNamedCExp App) xs)
 76 |   prettyPrecNamedCExp d (NmForce _ lr x)
 77 |       = parenthesise (d > Open) $
 78 |           sep [keyword "Force", byShow lr, prettyPrecNamedCExp App x]
 79 |   prettyPrecNamedCExp d (NmDelay _ lr x)
 80 |       = parenthesise (d > Open) $
 81 |           sep [keyword "Delay", byShow lr, prettyPrecNamedCExp App x]
 82 |   prettyPrecNamedCExp d (NmConCase _ sc xs def)
 83 |       = parenthesise (d > Open) $
 84 |           vcat [ case_ <++> prettyNamedCExp sc <++> of_
 85 |                , indent 2 (prettyAlts prettyNamedConAlt xs def)]
 86 |   prettyPrecNamedCExp d (NmConstCase _ sc xs def)
 87 |       = parenthesise (d > Open) $
 88 |           vcat [ case_ <++> prettyNamedCExp sc <++> of_
 89 |                , indent 2 (prettyAlts prettyNamedConstAlt xs def)]
 90 |   prettyPrecNamedCExp d (NmPrimVal _ x) = pretty x
 91 |   prettyPrecNamedCExp d (NmErased _) = "___"
 92 |   prettyPrecNamedCExp d (NmCrash _ x)
 93 |       = parenthesise (d > Open) $
 94 |           sep [annotate Keyword "crash", byShow x]
 95 |
 96 |   prettyNamedConAlt : NamedConAlt -> Doc IdrisSyntax
 97 |   prettyNamedConAlt (MkNConAlt x ci tag args exp)
 98 |         = sep (prettyCon x ci tag :: map prettyName args ++ [fatArrow <+> softline <+> align (prettyNamedCExp exp) ])
 99 |
100 |   prettyNamedConstAlt : NamedConstAlt -> Doc IdrisSyntax
101 |   prettyNamedConstAlt (MkNConstAlt x exp)
102 |         = pretty x <++> fatArrow <+> softline <+> align (prettyNamedCExp exp)
103 |
104 |   prettyAlts : (alt -> Doc IdrisSyntax) -> List alt -> Maybe NamedCExp -> Doc IdrisSyntax
105 |   prettyAlts pre xs def = vcat
106 |     $ zipWith (\ s, p => s <++> pre p)
107 |               (keyword "{" :: (keyword ";" <$ xs))
108 |               xs
109 |    ++ maybe [] (\ deflt => [keyword "; _" <++> fatArrow <+> softline <+> align (prettyNamedCExp deflt)]) def
110 |    ++ [keyword "}"]
111 |
112 | prettyCExp : {args : _} -> CExp args -> Doc IdrisSyntax
113 | prettyCExp = prettyNamedCExp . forget
114 |
115 | prettyCDef : CDef -> Doc IdrisDocAnn
116 | prettyCDef (MkFun [] exp) = reAnnotate Syntax $ prettyCExp exp
117 | prettyCDef (MkFun args exp) = reAnnotate Syntax $
118 |   keyword "\\" <++> concatWith (\ x, y => x <+> keyword "," <++> y) (map prettyName $ toList args)
119 |        <++> fatArrow <++> prettyCExp exp
120 | prettyCDef (MkCon mtag arity nt)
121 |   = vcat $ header (maybe "Type" (const "Data") mtag <++> "Constructor") :: map (indent 2)
122 |          ( maybe [] (\ tag => ["tag:" <++> byShow tag]) mtag ++
123 |          [ "arity:" <++> byShow arity ] ++
124 |            maybe [] (\ n => ["newtype by:" <++> byShow n]) nt)
125 | prettyCDef (MkForeign ccs args ret)
126 |   = vcat $ header "Foreign function" :: map (indent 2)
127 |          [ "bindings:" <++> cast (prettyList ccs)
128 |          , "argument types:" <++> byShow args
129 |          , "return type:" <++> byShow ret
130 |          ]
131 | prettyCDef (MkError exp) = "Error:" <++> reAnnotate Syntax (prettyCExp exp)
132 |
133 | export
134 | Pretty IdrisDocAnn CDef where
135 |   pretty = prettyCDef
136 |