@@ -69,49 +69,62 @@ showDoc ist d
6969 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d
7070
7171pprintFD :: IState -> Bool -> Bool -> FunDoc -> Doc OutputAnnotation
72−pprintFD ist totalityFlag nsFlag (FD n doc args ty f)
73− = nest 4 (prettyName True nsFlag [] n <+> colon <+>
74− pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
75− , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
76− -- show doc
77− renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>
78− -- show fixity
79− maybe empty (\f -> text (show f) <> line) f <>
80− -- show arguments doc
81− let argshow = showArgs args [] in
82− (if not (null argshow)
83− then nest 4 $ text "Arguments:" <$> vsep argshow
84− else empty) <>
85− -- show totality status
86− let totality = getTotality in
87− (if totalityFlag && not (null totality) then
88− line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
89− else
90− empty))
91−
92− where ppo = ppOptionIst ist
93− infixes = idris_infixes ist
94− showArgs ((n, ty, Exp {}, Just d):args) bnd
95− = bindingOf n False <+> colon <+>
96− pprintPTerm ppo bnd [] infixes ty <>
97− showDoc ist d <> line
98− :
99− showArgs args ((n, False):bnd)
100− showArgs ((n, ty, Constraint {}, Just d):args) bnd
101− = text "Class constraint" <+>
102− pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line
103− :
104− showArgs args ((n, True):bnd)
105− showArgs ((n, ty, Imp {}, Just d):args) bnd
106− = text "(implicit)" <+>
107− bindingOf n True <+> colon <+>
108− pprintPTerm ppo bnd [] infixes ty <>
109− showDoc ist d <> line
110− :
111− showArgs args ((n, True):bnd)
112− showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
113− showArgs [] _ = []
114− getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
72+pprintFD ist totalityFlag nsFlag (FD n doc args ty f) =
73+ nest 4 (prettyName True nsFlag [] n
74+ <+> colon
75+ <+> pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
76+ , not (T.isPrefixOf (T.pack "__") n') ] infixes ty
77+ -- show doc
78+ <$> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc
79+ -- show fixity
80+ <$> maybe empty (\f -> text (show f) <> line) f
81+ -- show arguments doc
82+ <> let argshow = showArgs args [] in
83+ (if not (null argshow)
84+ then nest 4 $ text "Arguments:" <$> vsep argshow
85+ else empty)
86+ -- show totality status
87+ <> let totality = getTotality in
88+ (if totalityFlag && not (null totality)
89+ then line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
90+ else empty))
91+
92+ where
93+ ppo = ppOptionIst ist
94+
95+ infixes = idris_infixes ist
96+
97+ -- Recurse over and show the Function's Documented arguments
98+ showArgs ((n, ty, Exp {}, Just d):args) bnd = -- Explicitly bound.
99+ bindingOf n False
100+ <+> colon
101+ <+> pprintPTerm ppo bnd [] infixes ty
102+ <> showDoc ist d
103+ <> line : showArgs args ((n, False):bnd)
104+ showArgs ((n, ty, Constraint {}, Just d):args) bnd = -- Class constraints.
105+ text "Class constraint"
106+ <+> pprintPTerm ppo bnd [] infixes ty
107+ <> showDoc ist d
108+ <> line : showArgs args ((n, True):bnd)
109+ showArgs ((n, ty, Imp {}, Just d):args) bnd = -- Implicit arguments.
110+ text "(implicit)"
111+ <+> bindingOf n True
112+ <+> colon
113+ <+> pprintPTerm ppo bnd [] infixes ty
114+ <> showDoc ist d
115+ <> line : showArgs args ((n, True):bnd)
116+ showArgs ((n, ty, TacImp{}, Just d):args) bnd = -- Tacit implicits
117+ text "(auto implicit)"
118+ <+> bindingOf n True
119+ <+> colon
120+ <+> pprintPTerm ppo bnd [] infixes ty
121+ <> showDoc ist d
122+ <> line : showArgs args ((n, True):bnd)
123+ showArgs ((n, _, _, _):args) bnd = -- Anything else
124+ showArgs args ((n, True):bnd)
125+ showArgs [] _ = [] -- end of arguments
126+
127+ getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
115128
116129pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
117130pprintFDWithTotality ist = pprintFD ist True