0 | module Core.Case.CaseTree.Pretty
  1 |
  2 | import Core.Case.CaseTree
  3 | import Core.Env
  4 | import Idris.Syntax
  5 | import Idris.Pretty
  6 | import Idris.Resugar
  7 |
  8 | import Data.String
  9 | import Libraries.Text.PrettyPrint.Prettyprinter
 10 |
 11 | namespace Raw
 12 |
 13 |   export
 14 |   prettyTree : {vars : _} -> CaseTree vars -> Doc IdrisSyntax
 15 |   prettyAlt : {vars : _} -> CaseAlt vars -> Doc IdrisSyntax
 16 |
 17 |   prettyTree (Case {name} idx prf ty alts)
 18 |       = let ann = case ty of
 19 |                     Erased {} => ""
 20 |                     _ => space <+> keyword ":" <++> byShow ty
 21 |         in case_ <++> annotate Bound (pretty0 name) <+> ann <++> of_
 22 |          <+> nest 2 (hardline
 23 |          <+> vsep (assert_total (map prettyAlt alts)))
 24 |   prettyTree (STerm i tm) = byShow tm
 25 |   prettyTree (Unmatched msg) = "Error:" <++> pretty0 msg
 26 |   prettyTree Impossible = "Impossible"
 27 |
 28 |   prettyAlt (ConCase n tag args sc)
 29 |       = hsep (annotate (DCon (Just n)) (pretty0 n) ::  map pretty0 args)
 30 |         <++> fatArrow
 31 |         <+> let sc = prettyTree sc in
 32 |             Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
 33 |   prettyAlt (DelayCase _ arg sc) =
 34 |         keyword "Delay" <++> pretty0 arg
 35 |         <++> fatArrow
 36 |         <+> let sc = prettyTree sc in
 37 |             Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
 38 |   prettyAlt (ConstCase c sc) =
 39 |         pretty c
 40 |         <++> fatArrow
 41 |         <+> let sc = prettyTree sc in
 42 |             Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
 43 |   prettyAlt (DefaultCase sc) =
 44 |         keyword "_"
 45 |         <++> fatArrow
 46 |         <+> let sc = prettyTree sc in
 47 |             Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
 48 |
 49 | namespace Resugared
 50 |
 51 |   prettyName : {auto c : Ref Ctxt Defs} ->
 52 |                Name -> Core (Doc IdrisSyntax)
 53 |   prettyName nm
 54 |     = pure $ ifThenElse (fullNamespace !(getPPrint))
 55 |                (pretty0 nm)
 56 |                (cast $ prettyOp True $ dropNS nm)
 57 |
 58 |   export
 59 |   prettyTree : {vars : _} ->
 60 |     {auto c : Ref Ctxt Defs} ->
 61 |     {auto s : Ref Syn SyntaxInfo} ->
 62 |     Env Term vars -> CaseTree vars -> Core (Doc IdrisSyntax)
 63 |   prettyAlt : {vars : _} ->
 64 |     {auto c : Ref Ctxt Defs} ->
 65 |     {auto s : Ref Syn SyntaxInfo} ->
 66 |     Env Term vars -> CaseAlt vars -> Core (Doc IdrisSyntax)
 67 |
 68 |   prettyTree env (Case {name} idx prf ty alts) = do
 69 |     ann <- case ty of
 70 |              Erased {} => pure ""
 71 |              _ => do ty <- resugar env ty
 72 |                      pure (space <+> keyword ":" <++> pretty ty)
 73 |     alts <- assert_total (traverse (prettyAlt env) alts)
 74 |     pure $ case_ <++> pretty0 name <+> ann <++> of_
 75 |        <+> nest 2 (hardline <+> vsep alts)
 76 |   prettyTree env (STerm i tm) = pretty <$> resugar env tm
 77 |   prettyTree env (Unmatched msg) = pure ("Error:" <++> pretty0 msg)
 78 |   prettyTree env Impossible = pure "Impossible"
 79 |
 80 |   prettyAlt env (ConCase n tag args sc) = do
 81 |     con <- prettyName n
 82 |     sc <- prettyTree (mkEnvOnto emptyFC args env) sc
 83 |     pure $ hsep (annotate (DCon (Just n)) con ::  map pretty0 args)
 84 |      <++> fatArrow
 85 |       <+> Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
 86 |   prettyAlt env (DelayCase _ arg sc) = do
 87 |     sc <- prettyTree (mkEnvOnto emptyFC [_,_] env) sc
 88 |     pure $ keyword "Delay" <++> pretty0 arg
 89 |         <++> fatArrow
 90 |         <+> Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
 91 |   prettyAlt env (ConstCase c sc) = do
 92 |     sc <- prettyTree env sc
 93 |     pure $ pretty c
 94 |         <++> fatArrow
 95 |         <+> Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
 96 |   prettyAlt env (DefaultCase sc) = do
 97 |     sc <- prettyTree env sc
 98 |     pure $ keyword "_"
 99 |         <++> fatArrow
100 |         <+> Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
101 |