Correction de quelques défauts d'affichage (notations sous "as" pour

filtrage; sauts de line intempestifs dans pretty.ml)



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10179 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 57 insertions, 34 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 32d9f107c..ec88e6fe8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -386,7 +386,7 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
   | PatVar (_,Anonymous), AHole _ -> sigma
   | a, AHole _ -> sigma
-  | PatCstr (loc,(ind,_ as r1),args1,Anonymous), _ ->
+  | PatCstr (loc,(ind,_ as r1),args1,_), _ ->
       let nparams =
 	(fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
       let l2 =
@@ -441,15 +441,15 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
   | (keyrule,pat,n as _rule)::rules ->
       try
 	(* Check the number of arguments expected by the notation *)
-	let loc = match t,n with
+	let loc,na = match t,n with
 	  | PatCstr (_,f,l,_), Some n when List.length l > n ->
 	      raise No_match
-	  | PatCstr (loc,_,_,_),_ -> loc
-	  | PatVar (loc,_),_ -> loc in
+	  | PatCstr (loc,_,_,na),_ -> loc,na
+	  | PatVar (loc,na),_ -> loc,na in
 	(* Try matching ... *)
 	let subst = match_aconstr_cases_pattern t pat in
 	(* Try availability of interpretation ... *)
-        match keyrule with
+	let p = match keyrule with
           | NotationRule (sc,ntn) ->
 	      (match availability_of_notation (sc,ntn) allscopes with
                   (* Uninterpretation is not allowed in current context *)
@@ -464,7 +464,8 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 		  insert_pat_delimiters loc (make_pat_notation loc ntn l) key)
           | SynDefRule kn ->
 	      let qid = shortest_qualid_of_syndef vars kn in
-              CPatAtom (loc,Some (Qualid (loc, qid)))
+              CPatAtom (loc,Some (Qualid (loc, qid))) in
+	insert_pat_alias loc p na
       with
 	  No_match -> extern_symbol_pattern allscopes vars t rules
 
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index bfabb533b..415a3002a 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -140,6 +140,8 @@ let strbrk s =
     else if p=n then [< >] else [< str (String.sub s p (n-p)) >]
   in aux 0 0
 
+let ismt s = try let _ = Stream.empty s in true with Stream.Failure -> false
+
 (* boxing commands *)
 let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >]
 let v n s = [< 'Ppcmd_box(Pp_vbox n,s) >]
diff --git a/lib/pp.mli b/lib/pp.mli
index 8a5aee799..41ea9ca0f 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -35,6 +35,7 @@ val fnl : unit -> std_ppcmds
 val pifb : unit -> std_ppcmds
 val ws : int -> std_ppcmds
 val mt : unit -> std_ppcmds
+val ismt : std_ppcmds -> bool
 
 val comment : int -> std_ppcmds
 val comments : ((int * int) * string) list ref
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 9acf697e3..a2341edb1 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -58,6 +58,8 @@ let print_basename sp = pr_global (ConstRef sp)
 
 let print_closed_sections = ref false
 
+let with_line_skip p = if ismt p then mt() else (fnl () ++ p)
+
 (********************************)
 (** Printing implicit arguments *)
 			  		  
@@ -140,12 +142,7 @@ let print_name_infos ref =
       str "Expanded type for implicit arguments" ++ fnl () ++ 
       print_ref true ref ++ fnl()
     else mt() in
-  (if (List.filter is_status_implicit impl<>[])
-      or not (List.for_all ((=) None) scopes) 
-  then fnl()
-  else mt())
-  ++ type_for_implicit 
-  ++ print_impl_args impl ++ print_argument_scopes scopes
+  type_for_implicit ++ print_impl_args impl ++ print_argument_scopes scopes
 
 let print_id_args_data test pr id l =
   if List.exists test l then
@@ -261,10 +258,10 @@ let print_named_def name body typ =
   (str "*** [" ++ str name ++ str " " ++
      hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++
 	      str ":" ++ brk (1,2) ++ ptyp) ++
-	   str "]" ++ fnl ())
+	   str "]")
 
 let print_named_assum name typ =
-  (str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]" ++ fnl ())
+  str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]"
 
 let gallina_print_named_decl (id,c,typ) =
   let s = string_of_id id in
@@ -358,21 +355,24 @@ let gallina_print_inductive sp =
   (if mib.mind_record & not !Options.raw_print then
     pr_record (List.hd names)
   else
-    pr_mutual_inductive mib.mind_finite names) ++ fnl () ++ fnl () ++
-  print_inductive_implicit_args sp mipv ++
-  print_inductive_argument_scopes sp mipv
+    pr_mutual_inductive mib.mind_finite names) ++ fnl () ++
+  with_line_skip 
+    (print_inductive_implicit_args sp mipv ++
+     print_inductive_argument_scopes sp mipv)
+
+let print_named_decl sp = 
+  gallina_print_named_decl (get_variable sp) ++ fnl ()
 
 let gallina_print_section_variable sp =
-  let d = get_variable sp in
-  gallina_print_named_decl d ++ 
-  print_name_infos (VarRef sp)
+  print_named_decl sp ++
+  with_line_skip (print_name_infos (VarRef sp))
 
 let print_body = function
   | Some lc  -> pr_lconstr (Declarations.force lc)
   | None -> (str"<no body>")
 
 let print_typed_body (val_0,typ) =
-  (print_body val_0 ++ fnl () ++ str "     : " ++ pr_ltype typ ++ fnl ())
+  (print_body val_0 ++ fnl () ++ str "     : " ++ pr_ltype typ)
 
 let ungeneralized_type_of_constant_type = function
   | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
@@ -387,14 +387,15 @@ let print_constant with_values sep sp =
     | None -> 
 	str"*** [ " ++ 
 	print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ 
-	str" ]" ++ fnl ()
+	str" ]"
     | _ -> 
 	print_basename sp ++ str sep ++ cut () ++
-	(if with_values then print_typed_body (val_0,typ) else pr_ltype typ) ++
-	fnl ())
+	(if with_values then print_typed_body (val_0,typ) else pr_ltype typ))
+  ++ fnl ()
 
 let gallina_print_constant_with_infos sp =
-  print_constant true " = " sp ++ print_name_infos (ConstRef sp)
+  print_constant true " = " sp ++ 
+  with_line_skip (print_name_infos (ConstRef sp))
 
 let gallina_print_syntactic_def kn =
   let sep = " := "
@@ -411,7 +412,7 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
       | (_,"VARIABLE") ->
 	  (* Outside sections, VARIABLES still exist but only with universes 
              constraints *)
-	  (try Some(gallina_print_section_variable (basename sp)) with Not_found -> None)
+	  (try Some(print_named_decl (basename sp)) with Not_found -> None)
       | (_,"CONSTANT") ->
 	  Some (print_constant with_values sep (constant_of_kn kn))
       | (_,"INDUCTIVE") ->
@@ -659,8 +660,9 @@ let print_opaque_name qid =
 let print_about ref = 
   let k = locate_any_name ref in
   begin match k with
-  | Term ref -> 
-      print_ref false ref ++ print_name_infos ref ++ print_opacity ref
+  | Term ref ->
+      print_ref false ref ++ fnl () ++ print_name_infos ref ++ 
+      print_opacity ref
   | Syntactic kn ->
       print_syntactic_def kn
   | Dir _ | ModuleType _ | Undefined _ ->
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 3c440b9d0..9d0d06580 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,7 +6,6 @@ fix F (t : t) : P t :=
   end
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
-
 proj = 
 fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
 match eq_nat_dec x y with
@@ -18,5 +17,14 @@ match eq_nat_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
-
 Argument scopes are [nat_scope nat_scope _ _ _]
+foo = 
+fix foo (A : Type) (l : list A) {struct l} : option A :=
+  match l with
+  | nil => None (A:=A)
+  | x0 :: nil => Some x0
+  | x0 :: (_ :: _) as l0 => foo A l0
+  end
+     : forall A : Type, list A -> option A
+
+Argument scopes are [type_scope list_scope]
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 56d5cfb4e..61f89d403 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -20,3 +20,16 @@ Definition proj (x y:nat) (P:nat -> Type) (def:P x) (prf:P y) : P y :=
  end.
 
 Print proj.
+
+(* Use notations even below aliases *)
+
+Require Import List.
+
+Fixpoint foo (A:Type) (l:list A) : option A :=
+  match l with
+  | nil => None
+  | x0 :: nil => Some x0
+  | x0 :: (x1 :: xs) as l0 => foo A l0
+  end.
+
+Print foo.
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 7949ef7b2..ecfe85054 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,7 +5,6 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
 d2 = fun x : nat => d1 (y:=x)
      : forall x x0 : nat, x0 = x -> x0 = x
 
-
 Arguments x, x0 are implicit
 Argument scopes are [nat_scope nat_scope _]
 map id (1 :: nil)
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index 41e8648bc..f94ed6423 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,10 +1,7 @@
 TrM.A = M.A
      : Set
-
 OpM.A = M.A
      : Set
-
 TrM.B = M.B
      : Set
-
 *** [ OpM.B : Set ]