diff options
Diffstat (limited to 'parsing/prettyp.ml')
| -rw-r--r-- | parsing/prettyp.ml | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 06d148ec6..741f9201e 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -151,6 +151,45 @@ let print_argument_scopes prefix = function str "]")] | _ -> [] +(*****************************) +(** Printing simpl behaviour *) + +let print_simpl_behaviour ref = + match Tacred.get_simpl_behaviour ref with + | None -> [] + | Some (recargs, nargs, flags) -> + let never = List.mem `SimplNeverUnfold flags in + let nomatch = List.mem `SimplDontExposeCase flags in + let pp_nomatch = spc() ++ if nomatch then + str "avoiding to expose match constructs" else str"" in + let pp_recargs = spc() ++ str "when the " ++ + let rec aux = function + | [] -> mt() + | [x] -> str (ordinal (x+1)) + | [x;y] -> str (ordinal (x+1)) ++ str " and " ++ str (ordinal (y+1)) + | x::tl -> str (ordinal (x+1)) ++ str ", " ++ aux tl in + aux recargs ++ str (plural (List.length recargs) " argument") ++ + str (plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++ + str " to a constructor" in + let pp_nargs = + spc() ++ str "when applied to " ++ int nargs ++ + str (plural nargs " argument") in + [hov 2 (str "The simpl tactic " ++ + match recargs, nargs, never with + | _,_, true -> str "never unfolds " ++ pr_global ref + | [], 0, _ -> str "always unfolds " ++ pr_global ref + | _::_, n, _ when n < 0 -> + str "unfolds " ++ pr_global ref ++ pp_recargs ++ pp_nomatch + | _::_, n, _ when n > List.fold_left max 0 recargs -> + str "unfolds " ++ pr_global ref ++ pp_recargs ++ + str " and" ++ pp_nargs ++ pp_nomatch + | _::_, _, _ -> + str "unfolds " ++ pr_global ref ++ pp_recargs ++ pp_nomatch + | [], n, _ when n > 0 -> + str "unfolds " ++ pr_global ref ++ pp_nargs ++ pp_nomatch + | _ -> str "unfolds " ++ pr_global ref ++ pp_nomatch )] +;; + (*********************) (** Printing Opacity *) @@ -625,6 +664,7 @@ let print_about_any k = pr_infos_list ([print_ref false ref; blankline] @ print_name_infos ref @ + print_simpl_behaviour ref @ print_opacity ref @ [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) | Syntactic kn -> |