Imported Upstream version 8.3upstream/8.3

6 files changed, 132 insertions, 89 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 1f5a6cf9..304640b2 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -9,7 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id: g_vernac.ml4 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: g_vernac.ml4 13492 2010-10-04 21:20:01Z herbelin $ *)
 
 
 open Pp
@@ -549,7 +549,7 @@ GEXTEND Gram
 
       (* Implicit *)
       | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global;
-	   pos = OPT [ "["; l = LIST0 implicit_name; "]" ->
+	   pos = LIST0 [ "["; l = LIST0 implicit_name; "]" ->
 	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
 	   VernacDeclareImplicits (use_section_locality (),qid,pos)
 
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index cc48c84f..a89594c2 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -10,7 +10,7 @@
 (* Add pr_o.cmo to circumvent a useless-warning bug when preprocessed with
  * ast-based camlp4 *)
 
-(*i $Id: lexer.ml4 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: lexer.ml4 13521 2010-10-10 21:59:00Z herbelin $ i*)
 
 open Pp
 open Util
@@ -147,7 +147,7 @@ let lookup_utf8_tail c cs =
       | _ -> error_utf8 cs
     in
     try classify_unicode unicode, n
-    with UnsupportedUtf8 -> error_unsupported_unicode_character n cs
+    with UnsupportedUtf8 -> njunk n cs; error_unsupported_unicode_character n cs
 
 let lookup_utf8 cs =
   match Stream.peek cs with
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index ff35be57..b5e0cc4a 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppvernac.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: ppvernac.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
 
 open Pp
 open Names
@@ -847,13 +847,15 @@ let rec pr_vernac = function
         (pr_locality local ++ str"Notation " ++ pr_lident id ++
 	 prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
-  | VernacDeclareImplicits (local,q,None) ->
+  | VernacDeclareImplicits (local,q,[]) ->
       hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++ 
 	pr_smart_global q)
-  | VernacDeclareImplicits (local,q,Some imps) ->
+  | VernacDeclareImplicits (local,q,impls) ->
       hov 1 (pr_section_locality local ++ str"Implicit Arguments " ++ 
 	spc() ++ pr_smart_global q ++ spc() ++
-	str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
+	prlist_with_sep spc (fun imps ->
+	  str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
+	  impls)
   | VernacReserve bl ->
       let n = List.length (List.flatten (List.map fst bl)) in
       hov 2 (str"Implicit Type" ++
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 9c39e57e..cf83c72a 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -10,7 +10,7 @@
  * on May-June 2006 for implementation of abstraction of pretty-printing of objects.
  *)
 
-(* $Id: prettyp.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: prettyp.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
 
 open Pp
 open Util
@@ -51,39 +51,25 @@ type object_pr = {
 let gallina_print_module  = print_module
 let gallina_print_modtype = print_modtype
 
-(*********************)
-(** Basic printing   *)
-
-let print_basename sp = pr_global (ConstRef sp)
+(**************)
+(** Utilities *)
 
 let print_closed_sections = ref false
 
-let with_line_skip p = if ismt p then mt() else (fnl () ++ p)
+let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l) ++ fnl()
 
-(********************************)
-(** Printing implicit arguments *)
+let with_line_skip l = if l = [] then mt() else fnl() ++ pr_infos_list l
 
-let conjugate_to_be = function [_] -> "is" | _ -> "are"
+let blankline = mt() (* add a blank sentence in the list of infos *)
 
-let pr_implicit imp = pr_id (name_of_implicit imp)
+let add_colon prefix = if ismt prefix then mt () else prefix ++ str ": "
 
-let print_impl_args_by_name max = function
-  | []  -> mt ()
-  | impls ->
-      hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++
-      prlist_with_sep pr_comma pr_implicit impls ++ spc() ++
-      str (conjugate_to_be impls) ++ str" implicit" ++
-      (if max then strbrk " and maximally inserted" else mt())) ++ fnl()
+let int_or_no n = if n=0 then str "no" else int n
 
-let print_impl_args l =
-  let imps = List.filter is_status_implicit l in
-  let maximps = List.filter Impargs.maximal_insertion_of imps in
-  let nonmaximps = list_subtract imps maximps in
-  print_impl_args_by_name false nonmaximps ++
-  print_impl_args_by_name true maximps
+(*******************)
+(** Basic printing *)
 
-(*********************)
-(** Printing Scopes  *)
+let print_basename sp = pr_global (ConstRef sp)
 
 let print_ref reduce ref =
   let typ = Global.type_of_global ref in
@@ -92,16 +78,49 @@ let print_ref reduce ref =
       let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ
       in it_mkProd_or_LetIn ccl ctx
     else typ in
-  hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ) ++ fnl ()
+  hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ)
 
-let print_argument_scopes = function
-  | [Some sc] -> str"Argument scope is [" ++ str sc ++ str"]" ++ fnl()
-  | l when not (List.for_all ((=) None) l) ->
-      hov 2 (str"Argument scopes are" ++ spc() ++
-      str "[" ++
-      prlist_with_sep spc (function Some sc -> str sc | None -> str "_") l ++
-      str "]") ++ fnl()
-  | _  -> mt()
+(********************************)
+(** Printing implicit arguments *)
+
+let conjugate_verb_to_be = function [_] -> "is" | _ -> "are"
+
+let pr_impl_name imp = pr_id (name_of_implicit imp)
+
+let print_impargs_by_name max = function
+  | []  -> []
+  | impls ->
+     [hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++
+      prlist_with_sep pr_comma pr_impl_name impls ++ spc() ++
+      str (conjugate_verb_to_be impls) ++ str" implicit" ++
+      (if max then strbrk " and maximally inserted" else mt()))]
+
+let print_one_impargs_list l =
+  let imps = List.filter is_status_implicit l in
+  let maximps = List.filter Impargs.maximal_insertion_of imps in
+  let nonmaximps = list_subtract imps maximps in
+  print_impargs_by_name false nonmaximps @
+  print_impargs_by_name true maximps
+
+let print_impargs_list prefix l =
+  let l = extract_impargs_data l in
+  List.flatten (List.map (fun (cond,imps) ->
+    match cond with
+    | None ->
+	List.map (fun pp -> add_colon prefix ++ pp)
+	  (print_one_impargs_list imps)
+    | Some (n1,n2) ->
+       [v 2 (prlist_with_sep cut (fun x -> x)
+	 [(if ismt prefix then str "When" else prefix ++ str ", when") ++
+	   str " applied to " ++
+	   (if n1 = n2 then int_or_no n2 else
+	    if n1 = 0 then str "less than " ++ int n2
+	    else int n1 ++ str " to " ++ int_or_no n2) ++
+	    str (plural n2 " argument") ++ str ":";
+          v 0 (prlist_with_sep cut (fun x -> x)
+	    (if List.exists is_status_implicit imps
+	    then print_one_impargs_list imps
+	    else [str "No implicit arguments"]))])]) l)
 
 let need_expansion impl ref =
   let typ = Global.type_of_global ref in
@@ -111,6 +130,33 @@ let need_expansion impl ref =
     let _,lastimpl = list_chop nprods impl in
       List.filter is_status_implicit lastimpl <> []
 
+let print_impargs ref =
+  let ref = Smartlocate.smart_global ref in
+  let impl = implicits_of_global ref in
+  let has_impl = impl <> [] in
+  (* Need to reduce since implicits are computed with products flattened *)
+  pr_infos_list
+    ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref;
+       blankline ] @
+    (if has_impl then print_impargs_list (mt()) impl
+     else [str "No implicit arguments"]))
+
+(*********************)
+(** Printing Scopes  *)
+
+let print_argument_scopes prefix = function
+  | [Some sc] ->
+      [add_colon prefix ++ str"Argument scope is [" ++ str sc ++ str"]"]
+  | l when not (List.for_all ((=) None) l) ->
+     [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++
+      str "[" ++
+      prlist_with_sep spc (function Some sc -> str sc | None -> str "_") l ++
+      str "]")]
+  | _  -> []
+
+(*********************)
+(** Printing Opacity *)
+
 type opacity =
   | FullyOpaque
   | TransparentMaybeOpacified of Conv_oracle.level
@@ -128,8 +174,9 @@ let opacity env = function
 
 let print_opacity ref =
   match opacity (Global.env()) ref with
-    | None -> mt ()
-    | Some s -> pr_global ref ++ str " is " ++
+    | None -> []
+    | Some s ->
+       [pr_global ref ++ str " is " ++
         str (match s with
           | FullyOpaque -> "opaque"
           | TransparentMaybeOpacified Conv_oracle.Opaque ->
@@ -139,38 +186,45 @@ let print_opacity ref =
           | TransparentMaybeOpacified (Conv_oracle.Level n) ->
               "transparent (with expansion weight "^string_of_int n^")"
           | TransparentMaybeOpacified Conv_oracle.Expand ->
-              "transparent (with minimal expansion weight)") ++ fnl()
+              "transparent (with minimal expansion weight)")]
+
+(*******************)
+(* *)
 
 let print_name_infos ref =
-  let impl = implicits_of_global ref in
+  let impls = implicits_of_global ref in
   let scopes = Notation.find_arguments_scope ref in
-  let type_for_implicit =
-    if need_expansion impl ref then
+  let type_info_for_implicit =
+    if need_expansion (select_impargs_size 0 impls) ref then
       (* Need to reduce since implicits are computed with products flattened *)
-      str "Expanded type for implicit arguments" ++ fnl () ++
-      print_ref true ref ++ fnl()
-    else mt() in
-  type_for_implicit ++ print_impl_args impl ++ print_argument_scopes scopes
+      [str "Expanded type for implicit arguments";
+       print_ref true ref; blankline]
+    else
+      [] in
+  type_info_for_implicit @
+  print_impargs_list (mt()) impls @
+  print_argument_scopes (mt()) scopes
 
 let print_id_args_data test pr id l =
   if List.exists test l then
-    str"For " ++ pr_id id ++ str": " ++ pr l
+    pr (str "For " ++ pr_id id) l
   else
-    mt()
+    []
 
 let print_args_data_of_inductive_ids get test pr sp mipv =
-  prvecti
+  List.flatten (Array.to_list (Array.mapi
     (fun i mip ->
-      print_id_args_data test pr mip.mind_typename (get (IndRef (sp,i))) ++
-      prvecti
+      print_id_args_data test pr mip.mind_typename (get (IndRef (sp,i))) @
+      List.flatten (Array.to_list (Array.mapi
 	(fun j idc ->
 	  print_id_args_data test pr idc (get (ConstructRef ((sp,i),j+1))))
-        mip.mind_consnames)
-    mipv
+        mip.mind_consnames)))
+    mipv))
 
 let print_inductive_implicit_args =
   print_args_data_of_inductive_ids
-    implicits_of_global is_status_implicit print_impl_args
+    implicits_of_global (fun l -> positions_of_implicits l <> [])
+    print_impargs_list
 
 let print_inductive_argument_scopes =
   print_args_data_of_inductive_ids
@@ -365,7 +419,7 @@ let gallina_print_inductive sp =
   else
     pr_mutual_inductive mib.mind_finite names) ++ fnl () ++
   with_line_skip
-    (print_inductive_implicit_args sp mipv ++
+    (print_inductive_implicit_args sp mipv @
      print_inductive_argument_scopes sp mipv)
 
 let print_named_decl id =
@@ -666,16 +720,19 @@ let print_opaque_name qid =
 	print_named_decl (id,c,ty)
 
 let print_about_any k =
-  begin match k with
+  match k with
   | Term ref ->
-      print_ref false ref ++ fnl () ++ print_name_infos ref ++
-      print_opacity ref
+      pr_infos_list
+       ([print_ref false ref; blankline] @
+	print_name_infos ref @
+	print_opacity ref @
+	[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
   | Syntactic kn ->
-      print_syntactic_def kn
+      v 0 (
+      print_syntactic_def kn ++
+      hov 0 (str "Expands to: " ++ pr_located_qualid k)) ++ fnl()
   | Dir _ | ModuleType _ | Undefined _ ->
-      mt () end
-  ++
-  hov 0 (str "Expands to: " ++ pr_located_qualid k)
+      hov 0 (pr_located_qualid k) ++ fnl()
 
 let print_about = function
   | Genarg.ByNotation (loc,ntn,sc) ->
@@ -685,15 +742,6 @@ let print_about = function
   | Genarg.AN ref ->
       print_about_any (locate_any_name ref)
 
-let print_impargs ref =
-  let ref = Smartlocate.smart_global ref in
-  let impl = implicits_of_global ref in
-  let has_impl = List.filter is_status_implicit impl <> [] in
-  (* Need to reduce since implicits are computed with products flattened *)
-  print_ref (need_expansion impl ref) ref ++ fnl() ++
-  (if has_impl then print_impl_args impl
-   else (str "No implicit arguments" ++ fnl ()))
-
 let unfold_head_fconst =
   let rec unfrec k = match kind_of_term k with
     | Const cst -> constant_value (Global.env ()) cst
@@ -771,7 +819,7 @@ let print_canonical_projections () =
 open Typeclasses
 
 let pr_typeclass env t =
-  print_ref false t.cl_impl
+  print_ref false t.cl_impl ++ fnl ()
 
 let print_typeclasses () =
   let env = Global.env () in
@@ -780,7 +828,7 @@ let print_typeclasses () =
 let pr_instance env i =
   (*   gallina_print_constant_with_infos i.is_impl *)
   (* lighter *)
-  print_ref false (instance_impl i)
+  print_ref false (instance_impl i) ++ fnl ()
 
 let print_all_instances () =
   let env = Global.env () in
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index d7f83b63..5704f54e 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: prettyp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: prettyp.mli 13492 2010-10-04 21:20:01Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -26,7 +26,6 @@ open Genarg
 val assumptions_for_print : name list -> Termops.names_context
 
 val print_closed_sections : bool ref
-val print_impl_args : Impargs.implicits_list -> std_ppcmds
 val print_context : bool -> int option -> Lib.library_segment -> std_ppcmds
 val print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option
 val print_full_context : unit -> std_ppcmds
@@ -46,12 +45,6 @@ val print_opaque_name : reference -> std_ppcmds
 val print_about : reference or_by_notation -> std_ppcmds
 val print_impargs : reference or_by_notation -> std_ppcmds
 
-(*i
-val print_extracted_name : identifier -> std_ppcmds
-val print_extraction : unit -> std_ppcmds
-val print_extracted_vars : unit -> std_ppcmds
-i*)
-
 (* Pretty-printing functions for classes and coercions *)
 val print_graph : unit -> std_ppcmds
 val print_classes : unit -> std_ppcmds
diff --git a/parsing/printer.ml b/parsing/printer.ml
index c9f27678..cf0050a5 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: printer.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: printer.ml 13390 2010-09-02 08:03:01Z herbelin $ *)
 
 open Pp
 open Util
@@ -263,7 +263,7 @@ let pr_predicate pr_elt (b, elts) =
     else
       if elts = [] then str"none" else pr_elts
 
-let pr_cpred p = pr_predicate pr_con (Cpred.elements p)
+let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p)
 let pr_idpred p = pr_predicate Nameops.pr_id (Idpred.elements p)
 
 let pr_transparent_state (ids, csts) =