Improvements on coqdoc by adding more information into .glob

files, about definitions and type of references.
- Add missing location information on fixpoints/cofixpoint in topconstr and
syntactic definitions in vernacentries for correct dumping.
- Dump definition information in vernacentries: defs, constructors,
projections etc...
- Modify coqdoc/index.mll to use this information instead of trying to
scan the file.
- Use the type information in latex output, update coqdoc.sty accordingly.
- Use the hyperref package to do crossrefs between definition and 
  references to coq objects in latex.  

Next step is to test and debug it on bigger developments.

On the side:
- Fix Program Let which was adding a Global definition. 
- Correct implicits for well-founded Program Fixpoints.
- Add new [Method] declaration kind.


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

5 files changed, 121 insertions, 42 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index dedaf6af4a..c922503aab 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -726,7 +726,7 @@ let rec extern inctx scopes vars r =
 		     | Some x -> Some (dummy_loc, out_name (List.nth ids x))
 		 in 
 		 let ro = extern_recursion_order scopes vars (snd nv.(i)) in
-		 (fi, (n, ro), bl, extern_typ scopes vars0 ty,
+		 ((dummy_loc, fi), (n, ro), bl, extern_typ scopes vars0 ty,
                   extern false scopes vars1 def)) idv
 	     in 
 	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
@@ -736,7 +736,7 @@ let rec extern inctx scopes vars r =
                  let (ids,bl) = extern_local_binder scopes vars blv.(i) in
                  let vars0 = List.fold_right (name_fold Idset.add) ids vars in
                  let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
-		 (fi,bl,extern_typ scopes vars0 tyv.(i),
+		 ((dummy_loc, fi),bl,extern_typ scopes vars0 tyv.(i),
                   sub_extern false scopes vars1 bv.(i))) idv
 	     in
 	     CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 65efc1f67b..283dc269d5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -44,8 +44,6 @@ let for_grammar f x =
     interning_grammar := false;
     a
 
-let variables_bind = ref false
-
 (**********************************************************************)
 (* Internalisation errors                                             *)
 
@@ -144,6 +142,56 @@ let coqdoc_unfreeze (lt,tn,lp) =
   token_number := tn;
   last_pos := lp
 
+open Decl_kinds
+
+let type_of_logical_kind = function
+  | IsDefinition def -> 
+      (match def with
+      | Definition -> "def"
+      | Coercion -> "coe"
+      | SubClass -> "subclass"
+      | CanonicalStructure -> "canonstruc"
+      | Example -> "ex"
+      | Fixpoint -> "def"
+      | CoFixpoint -> "def"
+      | Scheme -> "scheme"
+      | StructureComponent -> "proj"
+      | IdentityCoercion -> "coe"
+      | Instance -> "inst"
+      | Method -> "meth")
+  | IsAssumption a ->
+      (match a with
+      | Definitional -> "def"
+      | Logical -> "prf"
+      | Conjectural -> "prf")
+  | IsProof th ->
+      (match th with
+      | Theorem
+      | Lemma
+      | Fact
+      | Remark
+      | Property
+      | Proposition
+      | Corollary -> "thm")
+
+let type_of_global_ref gr =
+  if Typeclasses.is_class gr then
+    "class"
+  else
+    match gr with
+    | ConstRef cst -> 
+	type_of_logical_kind (Decls.constant_kind cst)
+    | VarRef v ->
+	"var" ^ type_of_logical_kind (Decls.variable_kind v)
+    | IndRef ind ->
+	let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
+	  if mib.Declarations.mind_record then
+	    if mib.Declarations.mind_finite then "rec"
+	    else "corec"
+	  else if mib.Declarations.mind_finite then "ind"
+	  else "coind"
+    | ConstructRef _ -> "constr"
+	
 let add_glob loc ref = 
   let sp = Nametab.sp_of_global ref in
   let lib_dp = Lib.library_part ref in
@@ -151,8 +199,25 @@ let add_glob loc ref =
   let mod_dp_trunc =  drop_dirpath_prefix lib_dp mod_dp in
   let filepath = string_of_dirpath lib_dp in
   let fullname = string_of_qualid (make_qualid mod_dp_trunc id) in
-    dump_string (Printf.sprintf "R%d %s %s\n" (fst (unloc loc)) filepath fullname)
+  let ty = type_of_global_ref ref in
+    dump_string (Printf.sprintf "R%d %s %s %s\n" 
+		    (fst (unloc loc)) filepath fullname ty)
+
+let add_glob loc ref =
+  if !Flags.dump && loc <> dummy_loc then add_glob loc ref
 
+let add_glob_kn loc kn =
+  let sp = Nametab.sp_of_syntactic_definition kn in
+  let dp, id = repr_path sp in
+  let fullname = string_of_id id in
+  let filepath = string_of_dirpath dp in
+    dump_string (Printf.sprintf "R%d %s %s syndef\n" (fst (unloc loc)) filepath fullname)
+
+let add_glob_kn loc ref =
+  if !Flags.dump && loc <> dummy_loc then add_glob_kn loc ref
+
+let dump_binding loc id = ()
+      
 let loc_of_notation f loc args ntn =
   if args=[] or ntn.[0] <> '_' then fst (unloc loc)
   else snd (unloc (f (List.hd args)))
@@ -171,8 +236,8 @@ let dump_notation_location pos ((path,df),sc) =
   let loc = next (pos >= !last_pos) in
     last_pos := pos;
     let path = string_of_dirpath path in
-    let sc = match sc with Some sc -> " "^sc | None -> "" in
-      dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc)
+    let _sc = match sc with Some sc -> " "^sc | None -> "" in
+      dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (unloc loc)) path df)
 
 (**********************************************************************)
 (* Contracting "{ _ }" in notations *)
@@ -383,9 +448,10 @@ let check_no_explicitation l =
 let intern_qualid loc qid intern env args =
   try match Nametab.extended_locate qid with
   | TrueGlobal ref ->
-      if !dump then add_glob loc ref;
+      add_glob loc ref;
       RRef (loc, ref), args
   | SyntacticDef sp ->
+      add_glob_kn loc sp;
       let (ids,c) = Syntax_def.search_syntactic_definition loc sp in
       let nids = List.length ids in
       if List.length args < nids then error_not_enough_arguments loc;
@@ -615,7 +681,7 @@ let find_constructor ref f aliases pats scopes =
 	    let v = Environ.constant_value (Global.env()) cst in
 	    unf (global_of_constr v)
         | ConstructRef cstr -> 
-	    if !dump then add_glob loc r; 
+	    add_glob loc r; 
 	    cstr, [], pats
         | _ -> raise Not_found
       in unf r
@@ -731,20 +797,28 @@ let push_name_env lvar (ids,tmpsc,scopes as env) = function
       check_hidden_implicit_parameters id lvar;
       (Idset.add id ids,tmpsc,scopes)
 
-let intern_typeclass_binders intern_type env bl =
+let push_loc_name_env lvar (ids,tmpsc,scopes as env) loc = function
+  | Anonymous -> env 
+  | Name id -> 
+      check_hidden_implicit_parameters id lvar;
+      dump_binding loc id;
+      (Idset.add id ids,tmpsc,scopes)
+
+let intern_typeclass_binders intern_type lvar env bl =
   List.fold_left 
     (fun ((ids,ts,sc) as env,bl) ((loc, na), bk, ty) ->
+      let env = push_loc_name_env lvar env loc na in
       let ty = locate_if_isevar loc na (intern_type env ty) in
-	((name_fold Idset.add na ids,ts,sc), (na,bk,None,ty)::bl))
+	(env, (na,bk,None,ty)::bl))
     env bl
 
-let intern_typeclass_binder intern_type (env,bl) na b ty =
+let intern_typeclass_binder intern_type lvar (env,bl) na b ty =
   let ctx = (na, b, ty) in
   let (fvs, bind) = Implicit_quantifiers.generalize_class_binders_raw (pi1 env) [ctx] in
-  let env, ifvs = intern_typeclass_binders intern_type (env,bl) fvs in
-    intern_typeclass_binders intern_type (env,ifvs) bind
+  let env, ifvs = intern_typeclass_binders intern_type lvar (env,bl) fvs in
+    intern_typeclass_binders intern_type lvar (env,ifvs) bind
     
-let intern_local_binder_aux intern intern_type ((ids,ts,sc as env),bl) = function
+let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = function
   | LocalRawAssum(nal,bk,ty) ->
       (match bk with
 	| Default k ->
@@ -756,7 +830,7 @@ let intern_local_binder_aux intern intern_type ((ids,ts,sc as env),bl) = functio
 		  ((name_fold Idset.add na ids,ts,sc), (na,k,None,ty)::bl))
 		(env,bl) nal
 	| TypeClass b ->
-	    intern_typeclass_binder intern_type (env,bl) (List.hd nal) b ty)
+	    intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal) b ty)
   | LocalRawDef((loc,na),def) ->
       ((name_fold Idset.add na ids,ts,sc),
       (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
@@ -840,7 +914,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
           | [] -> c
           | l -> RApp (constr_loc x, c, l))
     | CFix (loc, (locid,iddef), dl) ->
-        let lf = List.map (fun (id,_,_,_,_) -> id) dl in
+        let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
 	  try list_index0 iddef lf
@@ -886,7 +960,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
               Array.map (fun (_,_,ty,_) -> ty) idl,
               Array.map (fun (_,_,_,bd) -> bd) idl)
     | CCoFix (loc, (locid,iddef), dl) ->
-        let lf = List.map (fun (id,_,_,_) -> id) dl in
+        let lf = List.map (fun ((_, id),_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
           try list_index0 iddef lf
@@ -916,9 +990,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
         intern env c2
     | CLambdaN (loc,(nal,bk,ty)::bll,c2) ->
 	iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal
-    | CLetIn (loc,(_,na),c1,c2) ->
+    | CLetIn (loc,(loc1,na),c1,c2) ->
 	RLetIn (loc, na, intern (reset_tmp_scope env) c1,
-          intern (push_name_env lvar env na) c2)
+          intern (push_loc_name_env lvar env loc1 na) c2)
     | CNotation (loc,"- _",[CPrim (_,Numeral p)])
 	when Bigint.is_strictly_pos p -> 
 	intern env (CPrim (loc,Numeral (Bigint.neg p)))
@@ -999,7 +1073,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
   and intern_type env = intern (set_type_scope env)
 
   and intern_local_binder env bind = 
-    intern_local_binder_aux intern intern_type env bind
+    intern_local_binder_aux intern intern_type lvar env bind
 
   (* Expands a multiple pattern into a disjunction of multiple patterns *)
   and intern_multiple_pattern scopes n (loc,pl) =
@@ -1064,7 +1138,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
     let rec default env bk = function
     | (loc1,na)::nal ->
 	if nal <> [] then check_capture loc1 ty na;
-	let body = default (push_name_env lvar env na) bk nal in
+	let body = default (push_loc_name_env lvar env loc1 na) bk nal in
 	let ty = locate_if_isevar loc1 na (intern_type env ty) in
 	  RProd (join_loc loc1 loc2, na, bk, ty, body)
     | [] -> intern_type env body
@@ -1072,7 +1146,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
       match bk with
 	| Default b -> default env b nal
 	| TypeClass b -> 
-	    let env, ibind = intern_typeclass_binder intern_type (env, []) (List.hd nal) b ty in
+	    let env, ibind = intern_typeclass_binder intern_type lvar
+	      (env, []) (List.hd nal) b ty in
 	    let body = intern_type env body in
 	      it_mkRProd ibind body
 					   
@@ -1080,14 +1155,15 @@ let internalise sigma globalenv env allow_patvar lvar c =
     let rec default env bk = function 
       | (loc1,na)::nal ->
 	  if nal <> [] then check_capture loc1 ty na;
-	  let body = default (push_name_env lvar env na) bk nal in
+	  let body = default (push_loc_name_env lvar env loc1 na) bk nal in
 	  let ty = locate_if_isevar loc1 na (intern_type env ty) in
 	    RLambda (join_loc loc1 loc2, na, bk, ty, body)
       | [] -> intern env body
     in match bk with
       | Default b -> default env b nal
-      | TypeClass b ->
-	  let env, ibind = intern_typeclass_binder intern_type (env, []) (List.hd nal) b ty in
+      | TypeClass b ->	  
+	  let env, ibind = intern_typeclass_binder intern_type lvar
+	    (env, []) (List.hd nal) b ty in
 	  let body = intern env body in
 	    it_mkRLambda ibind body
 	      
@@ -1151,9 +1227,9 @@ let intern_gen isarity sigma env
                c =
   let tmp_scope = 
     if isarity then Some Notation.type_scope else None in
-  internalise sigma env (extract_ids env, tmp_scope,[])
-    allow_patvar (ltacvars,Environ.named_context env, [], impls) c
-
+    internalise sigma env (extract_ids env, tmp_scope,[])
+      allow_patvar (ltacvars,Environ.named_context env, [], impls) c
+      
 let intern_constr sigma env c = intern_gen false sigma env c 
 
 let intern_type sigma env c = intern_gen true sigma env c 
@@ -1282,15 +1358,16 @@ let interp_binder_evars evdref env na t =
 open Environ
 open Term
 
-let my_intern_constr sigma env acc c =
-  internalise sigma env acc false (([],[]),Environ.named_context env, [], ([], [])) c
+let my_intern_constr sigma env lvar acc c =
+  internalise sigma env acc false lvar c
 
-let my_intern_type sigma env acc c = my_intern_constr sigma env (set_type_scope acc) c
+let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c
 
 let intern_context sigma env params =
-  snd (List.fold_left
-	  (intern_local_binder_aux (my_intern_constr sigma env) (my_intern_type sigma env))
-	  ((extract_ids env,None,[]), []) params)
+  let lvar = (([],[]),Environ.named_context env, [], ([], [])) in
+    snd (List.fold_left
+	    (intern_local_binder_aux (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
+	    ((extract_ids env,None,[]), []) params)
 
 let interp_context_gen understand_type understand_judgment env bl = 
   let (env, par, _, impls) =
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index fb69460c4a..d3b8da8f9e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -149,3 +149,5 @@ val for_grammar : ('a -> 'b) -> 'a -> 'b
 type coqdoc_state
 val coqdoc_freeze : unit -> coqdoc_state
 val coqdoc_unfreeze : coqdoc_state -> unit
+
+val add_glob : Util.loc -> global_reference -> unit
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 35b8f075a3..cef1b93915 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -634,7 +634,7 @@ type constr_expr =
   | CDynamic of loc * Dyn.t
 
 and fixpoint_expr =
-    identifier * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+    identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and local_binder =
   | LocalRawDef of name located * constr_expr
@@ -645,7 +645,7 @@ and typeclass_constraint = name located * binding_kind * constr_expr
 and typeclass_context = typeclass_constraint list
 
 and cofixpoint_expr =
-    identifier * local_binder list * constr_expr * constr_expr
+    identifier located * local_binder list * constr_expr * constr_expr
 
 and recursion_order_expr = 
   | CStructRec
@@ -794,7 +794,7 @@ let fold_constr_expr_with_binders g f n acc = function
       let acc = f n (f n (f n acc b1) b2) c in
       Option.fold_left (f (Option.fold_right (name_fold g) ona n)) acc po
   | CFix (loc,_,l) ->
-      let n' = List.fold_right (fun (id,_,_,_,_) -> g id) l n in
+      let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
       List.fold_right (fun (_,(_,o),lb,t,c) acc ->
 	fold_local_binders g f n' 
 	  (fold_local_binders g f n acc t lb) c lb) l acc
@@ -909,14 +909,14 @@ let map_constr_expr_with_binders g f e = function
         let (e',bl') = map_local_binders f g e bl in
         let t' = f e' t in
         (* Note: fix names should be inserted before the arguments... *)
-        let e'' = List.fold_left (fun e (id,_,_,_,_) -> g id e) e' dl in
+        let e'' = List.fold_left (fun e ((_,id),_,_,_,_) -> g id e) e' dl in
         let d' = f e'' d in
         (id,n,bl',t',d')) dl)
   | CCoFix (loc,id,dl) ->
       CCoFix (loc,id,List.map (fun (id,bl,t,d) ->
         let (e',bl') = map_local_binders f g e bl in
         let t' = f e' t in
-        let e'' = List.fold_left (fun e (id,_,_,_) -> g id e) e' dl in
+        let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in
         let d' = f e'' d in
         (id,bl',t',d')) dl)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 155ac9ca8f..6790e400ff 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -139,10 +139,10 @@ type constr_expr =
   | CDynamic of loc * Dyn.t
 
 and fixpoint_expr =
-    identifier * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+    identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and cofixpoint_expr =
-    identifier * local_binder list * constr_expr * constr_expr
+    identifier located * local_binder list * constr_expr * constr_expr
 
 and recursion_order_expr = 
   | CStructRec