diff options
-rw-r--r-- | library/declare.mli | 19 | ||||
-rw-r--r-- | library/lib.ml | 16 | ||||
-rw-r--r-- | library/lib.mli | 3 | ||||
-rw-r--r-- | library/libnames.ml | 1 | ||||
-rwxr-xr-x | pretyping/classops.ml | 6 | ||||
-rw-r--r-- | pretyping/classops.mli | 5 | ||||
-rw-r--r-- | pretyping/indrec.ml | 80 | ||||
-rw-r--r-- | pretyping/indrec.mli | 3 | ||||
-rw-r--r-- | pretyping/termops.ml | 48 | ||||
-rw-r--r-- | pretyping/termops.mli | 9 | ||||
-rw-r--r-- | proofs/tacmach.ml | 2 |
11 files changed, 90 insertions, 102 deletions
diff --git a/library/declare.mli b/library/declare.mli index 27778884f..14540532b 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -90,27 +90,8 @@ val clear_proofs : named_context -> named_context (*s Global references *) val context_of_global_reference : global_reference -> section_context - -val global_qualified_reference : qualid -> constr -val global_absolute_reference : section_path -> constr -val global_reference_in_absolute_module : dir_path -> identifier -> constr - -val construct_qualified_reference : qualid -> constr -val construct_absolute_reference : section_path -> constr - -(* This should eventually disappear *) -(* [construct_reference] returns the object corresponding to - the name [id] in the global environment. It looks also for variables in a - given environment instead of looking in the current global environment. *) -val global_reference : identifier -> constr -val construct_reference : Sign.named_context option -> identifier -> constr - -val is_global : identifier -> bool - val strength_of_global : global_reference -> strength -val library_part : global_reference -> dir_path - (* hooks for XML output *) val set_xml_declare_variable : (object_name -> unit) -> unit val set_xml_declare_constant : (object_name -> unit) -> unit diff --git a/library/lib.ml b/library/lib.ml index f24cf4892..179e51bf8 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -525,3 +525,19 @@ let reset_initial () = end +(* Misc *) + +let library_part ref = + let sp = Nametab.sp_of_global ref in + let dir,_ = repr_path sp in + match ref with + | VarRef id -> + anomaly "TODO"; + extract_dirpath_prefix (sections_depth ()) (cwd ()) + | _ -> + if is_dirpath_prefix_of dir (cwd ()) then + (* Not yet (fully) discharged *) + extract_dirpath_prefix (sections_depth ()) (cwd ()) + else + (* Theorem/Lemma outside its outer section of definition *) + dir diff --git a/library/lib.mli b/library/lib.mli index 2f51d441d..e16f44af8 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -117,6 +117,9 @@ val end_compilation : dir_path -> object_prefix * library_segment compiling library (or [default_library]) *) val library_dp : unit -> dir_path +(* Extract the library part of a name even if in a section *) +val library_part : global_reference -> dir_path + (*s Sections *) val open_section : identifier -> object_prefix diff --git a/library/libnames.ml b/library/libnames.ml index 03d16f417..e8da68087 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -267,4 +267,3 @@ let pr_reference = function let loc_of_reference = function | Qualid (loc,qid) -> loc | Ident (loc,id) -> loc - diff --git a/pretyping/classops.ml b/pretyping/classops.ml index aa5057db8..03a0da56a 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -17,7 +17,6 @@ open Nametab open Environ open Libobject open Library -open Declare open Term open Termops open Rawterm @@ -240,11 +239,6 @@ let inductive_class_of ind = fst (class_info (CL_IND ind)) let class_args_of c = snd (decompose_app c) -let strength_of_cl = function - | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn)) - | CL_SECVAR sp -> variable_strength sp - | _ -> Global - let string_of_class = function | CL_FUN -> if !Options.v7 then "FUNCLASS" else "Funclass" | CL_SORT -> if !Options.v7 then "SORTCLASS" else "Sortclass" diff --git a/pretyping/classops.mli b/pretyping/classops.mli index aa0cca3dc..07f1623f8 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -14,7 +14,6 @@ open Decl_kinds open Term open Evd open Environ -open Declare open Nametab (*i*) @@ -26,6 +25,8 @@ type cl_typ = | CL_CONST of constant | CL_IND of inductive +val subst_cl_typ : substitution -> cl_typ -> cl_typ + (* This is the type of infos for declared classes *) type cl_info_typ = { cl_strength : strength; @@ -66,8 +67,6 @@ val inductive_class_of : inductive -> cl_index val class_args_of : constr -> constr list -val strength_of_cl : cl_typ -> strength - (*s [declare_coercion] adds a coercion in the graph of coercion paths *) val declare_coercion : coe_typ -> unsafe_judgment -> strength -> isid:bool -> diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index bf7e13158..f9bd67b36 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -25,7 +25,6 @@ open Reductionops open Typeops open Type_errors open Indtypes (* pour les erreurs *) -open Declare open Safe_typing open Nametab @@ -405,7 +404,8 @@ let instanciate_indrec_scheme sort = in drec -(* Change the sort in the type of an inductive definition, builds the corresponding eta-expanded term *) +(* Change the sort in the type of an inductive definition, builds the + corresponding eta-expanded term *) let instanciate_type_indrec_scheme sort npars term = let rec drec np elim = match kind_of_term elim with @@ -490,66 +490,12 @@ let type_rec_branches recursive env sigma indt p c = (*s Eliminations. *) -let type_suff = "_rect" - -let non_type_eliminations = [ (InProp,"_ind") ; (InSet,"_rec")] - let elimination_suffix = function | InProp -> "_ind" | InSet -> "_rec" | InType -> "_rect" let make_elimination_ident id s = add_suffix id (elimination_suffix s) - -let declare_one_elimination ind = - let (mib,mip) = Global.lookup_inductive ind in - let mindstr = string_of_id mip.mind_typename in - let declare na c t = - let kn = Declare.declare_constant (id_of_string na) - (DefinitionEntry - { const_entry_body = c; - const_entry_type = t; - const_entry_opaque = false }, - Decl_kinds.IsDefinition) in - Options.if_verbose ppnl (str na ++ str " is defined"); - kn - in - let env = Global.env () in - let sigma = Evd.empty in - let elim_scheme = build_indrec env sigma ind in - let npars = mip.mind_nparams in - let make_elim s = instanciate_indrec_scheme s npars elim_scheme in - let kelim = mip.mind_kelim in -(* in case the inductive has a type elimination, generates only one induction scheme, - the other ones share the same code with the apropriate type *) - if List.mem InType kelim then - let cte = - declare (mindstr^type_suff) (make_elim (new_sort_in_family InType)) None - in let c = mkConst (snd cte) and t = constant_type (Global.env ()) (snd cte) - in List.iter - (fun (sort,suff) -> - let (t',c') = instanciate_type_indrec_scheme (new_sort_in_family sort) npars c t - in let _ = declare (mindstr^suff) c' (Some t') - in ()) - non_type_eliminations - else (* Impredicative or logical inductive definition *) - List.iter - (fun (sort,suff) -> - if List.mem sort kelim then - let _ = declare (mindstr^suff) (make_elim (new_sort_in_family sort)) None in ()) - non_type_eliminations - -let declare_eliminations sp = - let mib = Global.lookup_mind sp in -(* - let ids = ids_of_named_context mib.mind_hyps in - if not (list_subset ids (ids_of_named_context (Global.named_context ()))) then error ("Declarations of elimination scheme outside the section "^ - "of the inductive definition is not implemented"); -*) - if mib.mind_finite then - for i = 0 to Array.length mib.mind_packets - 1 do - declare_one_elimination (sp,i) - done (* Look up function for the default elimination constant *) @@ -563,19 +509,19 @@ let lookup_eliminator ind_sp s = let ref = ConstRef (make_kn mp dp (label_of_id id)) in try let _ = sp_of_global ref in - constr_of_reference ref + constr_of_reference ref with Not_found -> (* Then try to get a user-defined eliminator in some other places *) (* using short name (e.g. for "eq_rec") *) - try construct_reference None id - with Not_found -> - errorlabstrm "default_elim" - (str "Cannot find the elimination combinator " ++ - pr_id id ++ spc () ++ - str "The elimination of the inductive definition " ++ - pr_id id ++ spc () ++ str "on sort " ++ - spc () ++ print_sort_family s ++ - str " is probably not allowed") + try constr_of_reference (Nametab.locate (make_short_qualid id)) + with Not_found -> + errorlabstrm "default_elim" + (str "Cannot find the elimination combinator " ++ + pr_id id ++ spc () ++ + str "The elimination of the inductive definition " ++ + pr_id id ++ spc () ++ str "on sort " ++ + spc () ++ print_sort_family s ++ + str " is probably not allowed") (* let env = Global.env() in @@ -588,7 +534,7 @@ let lookup_eliminator ind_sp s = with Not_found -> (* Then try to get a user-defined eliminator in some other places *) (* using short name (e.g. for "eq_rec") *) - try construct_reference None id + try constr_of_reference (Nametab.locate (make_short_qualid id)) with Not_found -> errorlabstrm "default_elim" (str "Cannot find the elimination combinator " ++ diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 38d07d1d9..1ab429dcf 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -30,6 +30,8 @@ val make_case_gen : env -> evar_map -> inductive -> sorts_family -> constr val build_indrec : env -> evar_map -> inductive -> constr val instanciate_indrec_scheme : sorts -> int -> constr -> constr +val instanciate_type_indrec_scheme : sorts -> int -> constr -> types -> + constr * types (* This builds complex [Scheme] *) @@ -49,7 +51,6 @@ val make_rec_branch_arg : constr -> constructor_summary -> wf_paths list -> constr (* *) -val declare_eliminations : mutual_inductive -> unit val lookup_eliminator : inductive -> sorts_family -> constr val elimination_suffix : sorts_family -> string val make_elimination_ident : identifier -> sorts_family -> identifier diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 080ed4374..a1d07777b 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -663,6 +663,36 @@ let ids_of_context env = let names_of_rel_context env = List.map (fun (na,_,_) -> na) (rel_context env) +(**** Globality of identifiers *) + +(* TODO temporary hack!!! *) +let rec is_imported_modpath = function + | MPfile dp -> dp <> (Lib.library_dp ()) +(* | MPdot (mp,_) -> is_imported_modpath mp *) + | _ -> false + +let is_imported_ref = function + | VarRef _ -> false + | ConstRef kn + | IndRef (kn,_) + | ConstructRef ((kn,_),_) +(* | ModTypeRef ln *) -> + let (mp,_,_) = repr_kn kn in is_imported_modpath mp +(* | ModRef mp -> + is_imported_modpath mp +*) + +let is_global id = + try + let ref = locate (make_short_qualid id) in + not (is_imported_ref ref) + with Not_found -> + false + +let is_section_variable id = + try let _ = Sign.lookup_named id (Global.named_context()) in true + with Not_found -> false + (* Nouvelle version de renommage des variables (DEC 98) *) (* This is the algorithm to display distinct bound variables @@ -701,14 +731,11 @@ let occur_id env nenv id0 c = with Occur -> true | Not_found -> false (* Case when a global is not in the env *) -let is_section_variable id = - try let _ = Declare.find_section_variable id in true with Not_found -> false - let next_name_not_occuring env name l env_names t = let rec next id = if List.mem id l or occur_id env env_names id t or (* To be consistent with intro mechanism *) - (Declare.is_global id & not (is_section_variable id)) + (is_global id & not (is_section_variable id)) then next (lift_ident id) else id in @@ -826,3 +853,16 @@ let rec rename_bound_var env l c = mkProd (Anonymous, c1, rename_bound_var env' l c2) | Cast (c,t) -> mkCast (rename_bound_var env l c, t) | x -> c + +(* References to constr *) + +let global_reference id = + constr_of_reference (Nametab.locate (make_short_qualid id)) + +let construct_reference ctx id = + try + mkVar (let _ = Sign.lookup_named id ctx in id) + with Not_found -> + global_reference id + + diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 216a090c4..9c9243c8c 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -175,3 +175,12 @@ val make_all_name_different : env -> env val global_vars : env -> constr -> identifier list val global_vars_set_of_decl : env -> named_declaration -> Idset.t + +(* References to constr *) + +val construct_reference : named_context -> identifier -> constr +val global_reference : identifier -> constr + +(* Test if an identifier is the basename of a global reference *) +val is_global : identifier -> bool + diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 51dd1e59d..3de476b17 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -78,7 +78,7 @@ let pf_interp_type gls c = let evc = project gls in Constrintern.interp_type evc (pf_env gls) c -let pf_global gls id = Declare.construct_reference (Some (pf_hyps gls)) id +let pf_global gls id = construct_reference (pf_hyps gls) id let pf_parse_const gls = compose (pf_global gls) id_of_string |