From f350cd8cb53e675a5793336b9b17c4749fa474b8 Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 30 May 2008 12:41:39 +0000 Subject: 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 --- interp/constrintern.ml | 143 +++++++++++++++++++++++++++++++++++++------------ 1 file changed, 110 insertions(+), 33 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 65efc1f67..283dc269d 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) = -- cgit v1.2.3