diff options
Diffstat (limited to 'library')
-rw-r--r-- | library/declare.ml | 34 | ||||
-rw-r--r-- | library/declare.mli | 14 |
2 files changed, 46 insertions, 2 deletions
diff --git a/library/declare.ml b/library/declare.ml index 1257044d3..ffe53e505 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -281,3 +281,37 @@ let declare_mind isrecord mie = !xml_declare_inductive (isrecord,oname); oname +(* Declaration messages *) + +let pr_rank i = str (ordinal (i+1)) + +let fixpoint_message indexes l = + Flags.if_verbose msgnl (match l with + | [] -> anomaly "no recursive definition" + | [id] -> pr_id id ++ str " is recursively defined" ++ + (match indexes with + | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" + | _ -> mt ()) + | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ + spc () ++ str "are recursively defined" ++ + match indexes with + | Some a -> spc () ++ str "(decreasing respectively on " ++ + prlist_with_sep pr_coma pr_rank (Array.to_list a) ++ + str " arguments)" + | None -> mt ())) + +let cofixpoint_message l = + Flags.if_verbose msgnl (match l with + | [] -> anomaly "No corecursive definition." + | [id] -> pr_id id ++ str " is corecursively defined" + | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ + spc () ++ str "are corecursively defined")) + +let recursive_message isfix i l = + (if isfix then fixpoint_message i else cofixpoint_message) l + +let definition_message id = + Flags.if_verbose msgnl (pr_id id ++ str " is defined") + +let assumption_message id = + Flags.if_verbose msgnl (pr_id id ++ str " is assumed") diff --git a/library/declare.mli b/library/declare.mli index 1a68f8e20..09526f341 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -59,10 +59,20 @@ val declare_internal_constant : the whole block (boolean must be true iff it is a record) *) val declare_mind : bool -> mutual_inductive_entry -> object_name -(* hooks for XML output *) +(* Hooks for XML output *) val set_xml_declare_variable : (object_name -> unit) -> unit val set_xml_declare_constant : (bool * constant -> unit) -> unit val set_xml_declare_inductive : (bool * object_name -> unit) -> unit -(* hook for the cache function of constants and inductives *) +(* Hook for the cache function of constants and inductives *) val add_cache_hook : (full_path -> unit) -> unit + +(* Declaration messages *) + +val definition_message : identifier -> unit +val assumption_message : identifier -> unit +val fixpoint_message : int array option -> identifier list -> unit +val cofixpoint_message : identifier list -> unit +val recursive_message : bool (* true = fixpoint *) -> + int array option -> identifier list -> unit + |