diff options
46 files changed, 684 insertions, 370 deletions
diff --git a/Makefile.common b/Makefile.common index edc9ad9e4..cf0f234d7 100644 --- a/Makefile.common +++ b/Makefile.common @@ -140,7 +140,8 @@ LIBRARY:=\ library/nameops.cmo library/libnames.cmo library/libobject.cmo \ library/summary.cmo library/nametab.cmo library/global.cmo library/lib.cmo \ library/declaremods.cmo library/library.cmo library/states.cmo \ - library/decl_kinds.cmo library/dischargedhypsmap.cmo library/goptions.cmo + library/decl_kinds.cmo library/dischargedhypsmap.cmo library/goptions.cmo \ + library/decls.cmo library/heads.cmo PRETYPING:=\ pretyping/termops.cmo pretyping/evd.cmo \ @@ -456,7 +457,7 @@ PRINTERSCMO:=\ kernel/term_typing.cmo kernel/mod_typing.cmo kernel/safe_typing.cmo \ library/summary.cmo library/global.cmo library/nameops.cmo \ library/libnames.cmo library/nametab.cmo library/libobject.cmo \ - library/lib.cmo library/goptions.cmo \ + library/lib.cmo library/goptions.cmo library/decls.cmo library/heads.cmo \ pretyping/termops.cmo pretyping/evd.cmo pretyping/rawterm.cmo \ pretyping/reductionops.cmo pretyping/inductiveops.cmo \ pretyping/retyping.cmo pretyping/cbv.cmo \ diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index b82526200..a4dc0eacd 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -408,7 +408,7 @@ let inspect n = oname, Lib.Leaf lobj -> (match oname, object_tag lobj with (sp,_), "VARIABLE" -> - let (_, _, v) = get_variable (basename sp) in + let (_, _, v) = Global.lookup_named (basename sp) in add_search2 (Nametab.locate (qualid_of_sp sp)) v | (sp,kn), "CONSTANT" -> let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 172c7479c..6b17e7396 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -158,7 +158,7 @@ let constant_to_ast_list kn = make_definition_ast (id_of_label (con_label kn)) (Declarations.force c1) typ l) let variable_to_ast_list sp = - let (id, c, v) = get_variable sp in + let (id, c, v) = Global.lookup_named sp in let l = implicits_of_global (VarRef sp) in (match c with None -> diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index afe7fc6d2..7d4eb72a9 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -27,6 +27,7 @@ open Typing open Tacmach open Tactics open Nametab +open Decls open Declare open Decl_kinds open Tacred diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 0f9331ff5..9eac4fbae 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -523,6 +523,9 @@ module Coercion = struct | Some (init, cur) -> (isevars, cj) + let inh_conv_coerce_rigid_to _ _ _ _ _ = + failwith "inh_conv_coerce_rigid_to: TODO" + let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) = (* (try *) (* trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++ *) diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 3551b262c..1bd5bb970 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -89,11 +89,11 @@ val string_of_hole_kind : hole_kind -> string val evars_of_term : evar_map -> evar_map -> constr -> evar_map val non_instanciated_map : env -> evar_defs ref -> evar_map -> evar_map val global_kind : logical_kind -val goal_kind : locality_flag * goal_object_kind +val goal_kind : locality * goal_object_kind val global_proof_kind : logical_kind -val goal_proof_kind : locality_flag * goal_object_kind +val goal_proof_kind : locality * goal_object_kind val global_fix_kind : logical_kind -val goal_fix_kind : locality_flag * goal_object_kind +val goal_fix_kind : locality * goal_object_kind val mkSubset : name -> constr -> constr -> constr val mkProj1 : constr -> constr -> constr -> constr diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index 5515320f0..6ea000f5b 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -55,7 +55,7 @@ let remove_module_dirpath_from_dirpath ~basedir dir = let get_uri_of_var v pvars = - let module D = Declare in + let module D = Decls in let module N = Names in let rec search_in_open_sections = function diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 649139f35..7e3a1bd41 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -73,11 +73,7 @@ let could_have_namesakes o sp = (* namesake = omonimo in italian *) let tag = Libobject.object_tag o in print_if_verbose ("Object tag: " ^ tag ^ "\n") ; match tag with - "CONSTANT" -> - (match D.constant_strength sp with - | DK.Local -> false (* a local definition *) - | DK.Global -> true (* a non-local one *) - ) + "CONSTANT" -> true (* constants/parameters are non global *) | "INDUCTIVE" -> true (* mutual inductive types are never local *) | "VARIABLE" -> false (* variables are local, so no namesakes *) | _ -> false (* uninteresting thing that won't be printed*) @@ -154,7 +150,7 @@ let search_variables () = | he::tl as modules -> let one_section_variables = let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in - let t = List.map N.string_of_id (Declare.last_section_hyps dirpath) in + let t = List.map N.string_of_id (Decls.last_section_hyps dirpath) in [he,t] in one_section_variables @ aux tl @@ -443,7 +439,7 @@ let kind_of_inductive isrecord kn = let kind_of_variable id = let module DK = Decl_kinds in - match Declare.variable_kind id with + match Decls.variable_kind id with | DK.IsAssumption DK.Definitional -> "VARIABLE","Assumption" | DK.IsAssumption DK.Logical -> "VARIABLE","Hypothesis" | DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture" @@ -454,7 +450,7 @@ let kind_of_variable id = let kind_of_constant kn = let module DK = Decl_kinds in - match Declare.constant_kind (Nametab.sp_of_global(Libnames.ConstRef kn)) with + match Decls.constant_kind kn with | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration" | DK.IsAssumption DK.Logical -> "AXIOM","Axiom" | DK.IsAssumption DK.Conjectural -> @@ -540,11 +536,10 @@ let print internal glob_ref kind xml_library_root = let tag,obj = match glob_ref with Ln.VarRef id -> - let sp = Declare.find_section_variable id in (* this kn is fake since it is not provided by Coq *) let kn = let (mod_path,dir_path) = Lib.current_prefix () in - N.make_kn mod_path dir_path (N.label_of_id (Ln.basename sp)) + N.make_kn mod_path dir_path (N.label_of_id id) in let (_,body,typ) = G.lookup_named id in Cic2acic.Variable kn,mk_variable_obj id body typ diff --git a/dev/base_include b/dev/base_include index 83e23d29f..d3301c88b 100644 --- a/dev/base_include +++ b/dev/base_include @@ -72,6 +72,7 @@ open Classops open Clenv open Rawterm open Coercion +open Coercion.Default open Recordops open Detyping open Reductionops diff --git a/dev/top_printers.ml b/dev/top_printers.ml index dfd813985..c67307d36 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -48,6 +48,7 @@ let ppcon con = pp(pr_con con) let ppkn kn = pp(pr_kn kn) let ppsp sp = pp(pr_sp sp) let ppqualid qid = pp(pr_qualid qid) +let ppclindex cl = pp(Classops.pr_cl_index cl) (* term printers *) let rawdebug = ref false diff --git a/kernel/inductive.ml b/kernel/inductive.ml index f60e2dbe0..ac4efc515 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -653,7 +653,7 @@ let check_one_fix renv recpos def = (* if [t] does not make recursive calls, it is guarded: *) if noccur_with_meta renv.rel_min nfi t then () else - let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in + let (f,l) = decompose_app (whd_betaiotazeta t) in match kind_of_term f with | Rel p -> (* Test if [p] is a fixpoint (recursive call) *) diff --git a/kernel/names.ml b/kernel/names.ml index 38eb38bea..d1c6ee8a4 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -65,7 +65,7 @@ let repr_dirpath x = x let empty_dirpath = [] let string_of_dirpath = function - | [] -> "_empty_" + | [] -> "<>" | sl -> String.concat "." (List.map string_of_id (List.rev sl)) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 7a6c560f8..ba7e8c41d 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -90,11 +90,11 @@ let pure_stack lfts stk = let nf_betaiota t = norm_val (create_clos_infos betaiota empty_env) (inject t) -let whd_betaiotazeta env x = +let whd_betaiotazeta x = match kind_of_term x with | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> x - | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) + | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x) let whd_betadeltaiota env t = match kind_of_term t with diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 663c18e2c..2e344b217 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -17,7 +17,7 @@ open Closure (************************************************************************) (*s Reduction functions *) -val whd_betaiotazeta : env -> constr -> constr +val whd_betaiotazeta : constr -> constr val whd_betadeltaiota : env -> constr -> constr val whd_betadeltaiota_nolet : env -> constr -> constr diff --git a/lib/gset.mli b/lib/gset.mli index af8764a9c..78fc61e14 100644 --- a/lib/gset.mli +++ b/lib/gset.mli @@ -26,7 +26,7 @@ val compare : 'a t -> 'a t -> int val equal : 'a t -> 'a t -> bool val subset : 'a t -> 'a t -> bool val iter : ('a -> unit) -> 'a t -> unit -val fold : ('a -> 'a -> 'a) -> 'a t -> 'a -> 'a +val fold : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b val cardinal : 'a t -> int val elements : 'a t -> 'a list val min_elt : 'a t -> 'a diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 8ea183509..20808f1e6 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -9,10 +9,11 @@ (* $Id$ *) open Util +open Libnames (* Informal mathematical status of declarations *) -type locality_flag = (*bool (* local = true; global = false *)*) +type locality = | Local | Global @@ -40,8 +41,6 @@ type definition_object_kind = | IdentityCoercion | Instance -type strength = locality_flag (* For compatibility *) - type assumption_object_kind = Definitional | Logical | Conjectural (* [assumption_kind] @@ -52,9 +51,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type assumption_kind = locality_flag * assumption_object_kind +type assumption_kind = locality * assumption_object_kind -type definition_kind = locality_flag * boxed_flag * definition_object_kind +type definition_kind = locality * boxed_flag * definition_object_kind (* Kinds used in proofs *) @@ -62,7 +61,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality_flag * goal_object_kind +type goal_kind = locality * goal_object_kind (* Kinds used in library *) @@ -100,3 +99,13 @@ let string_of_definition_kind (l,boxed,d) = anomaly "Unsupported local definition kind" | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Instance) -> anomaly "Internal definition kind" + +(* Strength *) + +let strength_of_global = function + | VarRef _ -> Local + | IndRef _ | ConstructRef _ | ConstRef _ -> Global + +let string_of_strength = function + | Local -> "Local" + | Global -> "Global" diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli new file mode 100644 index 000000000..c9485fa5b --- /dev/null +++ b/library/decl_kinds.mli @@ -0,0 +1,83 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: decl_kinds.ml 10410 2007-12-31 13:11:55Z msozeau $ *) + +open Util +open Libnames + +(* Informal mathematical status of declarations *) + +type locality = + | Local + | Global + +type boxed_flag = bool + +type theorem_kind = + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary + +type definition_object_kind = + | Definition + | Coercion + | SubClass + | CanonicalStructure + | Example + | Fixpoint + | CoFixpoint + | Scheme + | StructureComponent + | IdentityCoercion + | Instance + +type assumption_object_kind = Definitional | Logical | Conjectural + +(* [assumption_kind] + + | Local | Global + ------------------------------------ + Definitional | Variable | Parameter + Logical | Hypothesis | Axiom + +*) +type assumption_kind = locality * assumption_object_kind + +type definition_kind = locality * boxed_flag * definition_object_kind + +(* Kinds used in proofs *) + +type goal_object_kind = + | DefinitionBody of definition_object_kind + | Proof of theorem_kind + +type goal_kind = locality * goal_object_kind + +(* Kinds used in library *) + +type logical_kind = + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind + +(* Utils *) + +val logical_kind_of_goal_kind : goal_object_kind -> logical_kind +val string_of_theorem_kind : theorem_kind -> string +val string_of_definition_kind : + locality * boxed_flag * definition_object_kind -> string + +(* About locality *) + +val strength_of_global : global_reference -> locality +val string_of_strength : locality -> string diff --git a/library/declare.ml b/library/declare.ml index 278acc665..b524639ef 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -8,6 +8,8 @@ (* $Id$ *) +(** This module is about the low-level declaration of logical objects *) + open Pp open Util open Names @@ -17,32 +19,16 @@ open Term open Sign open Declarations open Entries -open Inductive -open Indtypes -open Reduction -open Type_errors -open Typeops open Libobject open Lib open Impargs -open Nametab open Safe_typing +open Cooking +open Decls open Decl_kinds -(**********************************************) - -(* Strength *) - -open Nametab +(** XML output hooks *) -let strength_min (stre1,stre2) = - if stre1 = Local or stre2 = Local then Local else Global - -let string_of_strength = function - | Local -> "(local)" - | Global -> "(global)" - -(* XML output hooks *) let xml_declare_variable = ref (fun (sp:object_name) -> ()) let xml_declare_constant = ref (fun (sp:bool * constant)-> ()) let xml_declare_inductive = ref (fun (sp:bool * object_name) -> ()) @@ -53,7 +39,7 @@ let set_xml_declare_variable f = xml_declare_variable := if_xml f let set_xml_declare_constant f = xml_declare_constant := if_xml f let set_xml_declare_inductive f = xml_declare_inductive := if_xml f -(* Section variables. *) +(** Declaration of section variables and local definitions *) type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) @@ -61,53 +47,30 @@ type section_variable_entry = type variable_declaration = dir_path * section_variable_entry * logical_kind -type checked_section_variable = - | CheckedSectionLocalDef of constr * types * Univ.constraints * bool - | CheckedSectionLocalAssum of types * Univ.constraints - -type checked_variable_declaration = - dir_path * checked_section_variable * logical_kind - -let vartab = ref (Idmap.empty : checked_variable_declaration Idmap.t) - -let _ = Summary.declare_summary "VARIABLE" - { Summary.freeze_function = (fun () -> !vartab); - Summary.unfreeze_function = (fun ft -> vartab := ft); - Summary.init_function = (fun () -> vartab := Idmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } - let cache_variable ((sp,_),o) = match o with | Inl cst -> Global.add_constraints cst | Inr (id,(p,d,mk)) -> (* Constr raisonne sur les noms courts *) - if Idmap.mem id !vartab then + if variable_exists id then errorlabstrm "cache_variable" (pr_id id ++ str " already exists"); - let vd,impl,keep = match d with (* Fails if not well-typed *) + let impl,opaq,cst,keep = match d with (* Fails if not well-typed *) | SectionLocalAssum (ty, impl, keep) -> let cst = Global.push_named_assum (id,ty) in - let (_,bd,ty) = Global.lookup_named id in - CheckedSectionLocalAssum (ty,cst), impl, if keep then Some ty else None + impl, true, cst, (if keep then Some ty else None) | SectionLocalDef (c,t,opaq) -> let cst = Global.push_named_def (id,c,t) in - let (_,bd,ty) = Global.lookup_named id in - CheckedSectionLocalDef (Option.get bd,ty,cst,opaq), false, None in + false, opaq, cst, None in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id impl keep; Dischargedhypsmap.set_discharged_hyps sp []; - vartab := Idmap.add id (p,vd,mk) !vartab - -let get_variable_constraints id = - match pi2 (Idmap.find id !vartab) with - | CheckedSectionLocalDef (c,ty,cst,opaq) -> cst - | CheckedSectionLocalAssum (ty,cst) -> cst + add_variable_data id (p,opaq,cst,mk) let discharge_variable (_,o) = match o with - | Inr (id,_) -> Some (Inl (get_variable_constraints id)) + | Inr (id,_) -> Some (Inl (variable_constraints id)) | Inl _ -> Some o -let (in_variable, out_variable) = +let (inVariable, outVariable) = declare_object { (default_object "VARIABLE") with cache_function = cache_variable; discharge_function = discharge_variable; @@ -115,25 +78,17 @@ let (in_variable, out_variable) = (* for initial declaration *) let declare_variable id obj = - let oname = add_leaf id (in_variable (Inr (id,obj))) in + let oname = add_leaf id (inVariable (Inr (id,obj))) in declare_var_implicits id; Notation.declare_ref_arguments_scope (VarRef id); + Heads.declare_head (EvalVarRef id); !xml_declare_variable oname; oname -(* Globals: constants and parameters *) +(** Declaration of constants and parameters *) type constant_declaration = constant_entry * logical_kind -let csttab = ref (Spmap.empty : logical_kind Spmap.t) - -let _ = Summary.declare_summary "CONSTANT" - { Summary.freeze_function = (fun () -> !csttab); - Summary.unfreeze_function = (fun ft -> csttab := ft); - Summary.init_function = (fun () -> csttab := Spmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } - (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) let load_constant i ((sp,kn),(_,_,kind)) = @@ -141,7 +96,7 @@ let load_constant i ((sp,kn),(_,_,kind)) = errorlabstrm "cache_constant" (pr_id (basename sp) ++ str " already exists"); Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn)); - csttab := Spmap.add sp kind !csttab + add_constant_kind (constant_of_kn kn) kind (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn),_) = @@ -150,18 +105,14 @@ let open_constant i ((sp,kn),_) = let cache_constant ((sp,kn),(cdt,dhyps,kind)) = let id = basename sp in let _,dir,_ = repr_kn kn in - if Idmap.mem id !vartab or Nametab.exists_cci sp then + if variable_exists id or Nametab.exists_cci sp then errorlabstrm "cache_constant" (pr_id id ++ str " already exists"); let kn' = Global.add_constant dir id cdt in assert (kn' = constant_of_kn kn); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); add_section_constant kn' (Global.lookup_constant kn').const_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; - csttab := Spmap.add sp kind !csttab - -(*s Registration as global tables and rollback. *) - -open Cooking + add_constant_kind (constant_of_kn kn) kind let discharged_hyps kn sechyps = let (_,dir,_) = repr_kn kn in @@ -185,7 +136,7 @@ let export_constant cst = Some (dummy_constant cst) let classify_constant (_,cst) = Substitute (dummy_constant cst) -let (in_constant, out_constant) = +let (inConstant, outConstant) = declare_object { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; @@ -206,9 +157,10 @@ let hcons_constant_declaration = function | cd -> cd let declare_constant_common id dhyps (cd,kind) = - let (sp,kn) = add_leaf id (in_constant (cd,dhyps,kind)) in + let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in let kn = constant_of_kn kn in declare_constant_implicits kn; + Heads.declare_head (EvalConstRef kn); Notation.declare_ref_arguments_scope (ConstRef kn); kn @@ -221,7 +173,7 @@ let declare_constant_gen internal id (cd,kind) = let declare_internal_constant = declare_constant_gen true let declare_constant = declare_constant_gen false -(* Inductives. *) +(** Declaration of inductive blocks *) let declare_inductive_argument_scopes kn mie = list_iter_i (fun i {mind_entry_consnames=lc} -> @@ -251,7 +203,7 @@ let inductive_names sp kn mie = in names let check_exists_inductive (sp,_) = - (if Idmap.mem (basename sp) !vartab then + (if variable_exists (basename sp) then errorlabstrm "" (pr_id (basename sp) ++ str " already exists")); if Nametab.exists_cci sp then @@ -301,7 +253,7 @@ let dummy_inductive_entry (_,m) = ([],{ let export_inductive x = Some (dummy_inductive_entry x) -let (in_inductive, out_inductive) = +let (inInductive, outInductive) = declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; @@ -316,84 +268,9 @@ let declare_mind isrecord mie = let id = match mie.mind_entry_inds with | ind::_ -> ind.mind_entry_typename | [] -> anomaly "cannot declare an empty list of inductives" in - let (sp,kn as oname) = add_leaf id (in_inductive ([],mie)) in + let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in declare_mib_implicits kn; declare_inductive_argument_scopes kn mie; !xml_declare_inductive (isrecord,oname); oname -(*s Test and access functions. *) - -let is_constant sp = - try let _ = Spmap.find sp !csttab in true with Not_found -> false - -let constant_strength sp = Global -let constant_kind sp = Spmap.find sp !csttab - -let get_variable id = - let (p,x,_) = Idmap.find id !vartab in - match x with - | CheckedSectionLocalDef (c,ty,cst,opaq) -> (id,Some c,ty) - | CheckedSectionLocalAssum (ty,cst) -> (id,None,ty) - -let variable_strength _ = Local - -let find_section_variable id = - let (p,_,_) = Idmap.find id !vartab in Libnames.make_path p id - -let variable_opacity id = - let (_,x,_) = Idmap.find id !vartab in - match x with - | CheckedSectionLocalDef (c,ty,cst,opaq) -> opaq - | CheckedSectionLocalAssum (ty,cst) -> false (* any.. *) - -let variable_kind id = - pi3 (Idmap.find id !vartab) - -let clear_proofs sign = - List.fold_right - (fun (id,c,t as d) signv -> - let d = if variable_opacity id then (id,None,t) else d in - Environ.push_named_context_val d signv) sign Environ.empty_named_context_val - -(* Global references. *) - -let first f v = - let n = Array.length v in - let rec look_for i = - if i = n then raise Not_found; - try f i v.(i) with Not_found -> look_for (succ i) - in - look_for 0 - -let mind_oper_of_id sp id mib = - first - (fun tyi mip -> - if id = mip.mind_typename then - IndRef (sp,tyi) - else - first - (fun cj cid -> - if id = cid then - ConstructRef ((sp,tyi),succ cj) - else raise Not_found) - mip.mind_consnames) - mib.mind_packets - -let last_section_hyps dir = - fold_named_context - (fun (id,_,_) sec_ids -> - try - let (p,_,_) = Idmap.find id !vartab in - if dir=p then id::sec_ids else sec_ids - with Not_found -> sec_ids) - (Environ.named_context (Global.env())) - ~init:[] - -let is_section_variable = function - | VarRef _ -> true - | _ -> false - -let strength_of_global = function - | VarRef _ -> Local - | IndRef _ | ConstructRef _ | ConstRef _ -> Global diff --git a/library/declare.mli b/library/declare.mli index 96fd5eb9b..93c8b9f91 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -59,26 +59,6 @@ val declare_internal_constant : the whole block (boolean must be true iff it is a record) *) val declare_mind : bool -> mutual_inductive_entry -> object_name -val strength_min : strength * strength -> strength -val string_of_strength : strength -> string - -(*s Corresponding test and access functions. *) - -val is_constant : section_path -> bool -val constant_strength : section_path -> strength -val constant_kind : section_path -> logical_kind - -val get_variable : variable -> named_declaration -val variable_strength : variable -> strength -val variable_kind : variable -> logical_kind -val find_section_variable : variable -> section_path -val last_section_hyps : dir_path -> identifier list -val clear_proofs : named_context -> Environ.named_context_val - -(*s Global references *) - -val strength_of_global : global_reference -> strength - (* hooks for XML output *) val set_xml_declare_variable : (object_name -> unit) -> unit val set_xml_declare_constant : (bool * constant -> unit) -> unit diff --git a/library/decls.ml b/library/decls.ml new file mode 100644 index 000000000..d84703271 --- /dev/null +++ b/library/decls.ml @@ -0,0 +1,76 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +(** This module registers tables for some non-logical informations + associated declarations *) + +open Names +open Term +open Sign +open Decl_kinds +open Libnames + +(** Datas associated to section variables and local definitions *) + +type variable_data = + dir_path * bool (* opacity *) * Univ.constraints * logical_kind + +let vartab = ref (Idmap.empty : variable_data Idmap.t) + +let _ = Summary.declare_summary "VARIABLE" + { Summary.freeze_function = (fun () -> !vartab); + Summary.unfreeze_function = (fun ft -> vartab := ft); + Summary.init_function = (fun () -> vartab := Idmap.empty); + Summary.survive_module = false; + Summary.survive_section = false } + +let add_variable_data id o = vartab := Idmap.add id o !vartab + +let variable_path id = let (p,_,_,_) = Idmap.find id !vartab in p +let variable_opacity id = let (_,opaq,_,_) = Idmap.find id !vartab in opaq +let variable_kind id = let (_,_,_,k) = Idmap.find id !vartab in k +let variable_constraints id = let (_,_,cst,_) = Idmap.find id !vartab in cst + +let variable_exists id = Idmap.mem id !vartab + +(** Datas associated to global parameters and constants *) + +let csttab = ref (Cmap.empty : logical_kind Cmap.t) + +let _ = Summary.declare_summary "CONSTANT" + { Summary.freeze_function = (fun () -> !csttab); + Summary.unfreeze_function = (fun ft -> csttab := ft); + Summary.init_function = (fun () -> csttab := Cmap.empty); + Summary.survive_module = false; + Summary.survive_section = false } + +let add_constant_kind kn k = csttab := Cmap.add kn k !csttab + +let constant_kind kn = Cmap.find kn !csttab + +(** Miscellaneous functions. *) + +let clear_proofs sign = + List.fold_right + (fun (id,c,t as d) signv -> + let d = if variable_opacity id then (id,None,t) else d in + Environ.push_named_context_val d signv) sign Environ.empty_named_context_val + +let last_section_hyps dir = + fold_named_context + (fun (id,_,_) sec_ids -> + try if dir=variable_path id then id::sec_ids else sec_ids + with Not_found -> sec_ids) + (Environ.named_context (Global.env())) + ~init:[] + +let is_section_variable = function + | VarRef _ -> true + | _ -> false diff --git a/library/decls.mli b/library/decls.mli new file mode 100644 index 000000000..96654bcbd --- /dev/null +++ b/library/decls.mli @@ -0,0 +1,47 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: declare.mli 10741 2008-04-02 15:47:07Z msozeau $ i*) + +open Names +open Sign +(* +open Libnames +open Term +open Declarations +open Entries +open Indtypes +open Safe_typing +open Nametab +*) +open Decl_kinds + +(** This module manages non-kernel informations about declarations. It + is either non-logical informations or logical informations that + have no place to be (yet) in the kernel *) + +(** Registration and access to the table of variable *) + +type variable_data = + dir_path * bool (* opacity *) * Univ.constraints * logical_kind + +val add_variable_data : variable -> variable_data -> unit +val variable_kind : variable -> logical_kind +val variable_opacity : variable -> bool +val variable_constraints : variable -> Univ.constraints +val variable_exists : variable -> bool + +(** Registration and access to the table of constants *) + +val add_constant_kind : constant -> logical_kind -> unit +val constant_kind : constant -> logical_kind + +(** Miscellaneous functions *) + +val last_section_hyps : dir_path -> identifier list +val clear_proofs : named_context -> Environ.named_context_val diff --git a/library/heads.ml b/library/heads.ml new file mode 100644 index 000000000..c341c835e --- /dev/null +++ b/library/heads.ml @@ -0,0 +1,190 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Pp +open Util +open Names +open Term +open Mod_subst +open Environ +open Libnames +open Nameops +open Libobject +open Lib + +(** Characterization of the head of a term *) + +(* We only compute an approximation to ensure the computation is not + arbitrary long (e.g. the head constant of [h] defined to be + [g (fun x -> phi(x))] where [g] is [fun f => g O] does not launch + the evaluation of [phi(0)] and the head of [h] is declared unknown). *) + +type rigid_head_kind = +| RigidParameter of constant (* a Const without body *) +| RigidVar of variable (* a Var without body *) +| RigidType (* an inductive, a product or a sort *) + +type head_approximation = +| RigidHead of rigid_head_kind +| ConstructorHead +| FlexibleHead of int * int * int * bool (* [true] if a surrounding case *) +| NotImmediatelyComputableHead + +(** Registration as global tables and rollback. *) + +module Evalreford = struct + type t = evaluable_global_reference + let compare = Pervasives.compare +end + +module Evalrefmap = Map.Make(Evalreford) + +let head_map = ref Evalrefmap.empty + +let init () = head_map := Evalrefmap.empty + +let freeze () = !head_map + +let unfreeze hm = head_map := hm + +let _ = + Summary.declare_summary "Head_decl" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = true; + Summary.survive_section = false } + +let variable_head id = Evalrefmap.find (EvalVarRef id) !head_map +let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map + +let kind_of_head env t = + let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta t) with + | Rel n when n > k -> NotImmediatelyComputableHead + | Rel n -> FlexibleHead (k,k+1-n,List.length l,b) + | Var id -> + (try on_subterm k l b (variable_head id) + with Not_found -> + (* a goal variable *) + match pi2 (lookup_named id env) with + | Some c -> aux k l c b + | None -> NotImmediatelyComputableHead) + | Const cst -> on_subterm k l b (constant_head cst) + | Construct _ | CoFix _ -> + if b then NotImmediatelyComputableHead else ConstructorHead + | Sort _ | Ind _ | Prod _ -> RigidHead RigidType + | Cast (c,_,_) -> aux k l c b + | Lambda (_,_,c) when l = [] -> assert (not b); aux (k+1) [] c b + | Lambda (_,_,c) -> aux (k+1) (List.tl l) (subst1 (List.hd l) c) b + | LetIn _ -> assert false + | Meta _ | Evar _ -> NotImmediatelyComputableHead + | App (c,al) -> aux k (Array.to_list al @ l) c b + | Case (_,_,c,_) -> aux k [] c true + | Fix ((i,j),_) -> + let n = i.(j) in + try aux k [] (List.nth l n) true + with Failure _ -> FlexibleHead (k + n + 1, k + n + 1, 0, true) + and on_subterm k l with_case = function + | FlexibleHead (n,i,q,with_subcase) -> + let m = List.length l in + let k',rest,a = + if n > m then + (* eta-expansion *) + let a = + if i <= m then + (* we pick the head in the existing arguments *) + lift (n-m) (List.nth l (i-1)) + else + (* we pick the head in the added arguments *) + mkRel (n-i+1) in + k+n-m,[],a + else + (* enough arguments to [cst] *) + k,list_skipn n l,List.nth l (i-1) in + let l' = list_tabulate (fun _ -> mkMeta 0) q @ rest in + aux k' l' a (with_subcase or with_case) + | ConstructorHead when with_case -> NotImmediatelyComputableHead + | x -> x + in aux 0 [] t false + +let compute_head = function +| EvalConstRef cst -> + (match constant_opt_value (Global.env()) cst with + | None -> RigidHead (RigidParameter cst) + | Some c -> kind_of_head (Global.env()) c) +| EvalVarRef id -> + (match pi2 (Global.lookup_named id) with + | Some c when not (Decls.variable_opacity id) -> + kind_of_head (Global.env()) c + | _ -> + RigidHead (RigidVar id)) + +let is_rigid env t = + match kind_of_head env t with + | RigidHead _ | ConstructorHead -> true + | _ -> false + +(** Registration of heads as an object *) + +let load_head _ (_,(ref,(k:head_approximation))) = + head_map := Evalrefmap.add ref k !head_map + +let cache_head o = + load_head 1 o + +let subst_head_approximation subst = function + | RigidHead (RigidParameter cst) as k -> + let cst,c = subst_con subst cst in + if c = mkConst cst then + (* A change of the prefix of the constant *) + k + else + (* A substitution of the constant by a functor argument *) + kind_of_head (Global.env()) c + | x -> x + +let subst_head (_,subst,(ref,k)) = + (subst_evaluable_reference subst ref, subst_head_approximation subst k) + +let discharge_head (_,(ref,k)) = + match ref with + | EvalConstRef cst -> Some (EvalConstRef (pop_con cst), k) + | EvalVarRef id -> None + +let rebuild_head (info,(ref,k)) = + (ref, compute_head ref) + +let export_head o = Some o + +let (inHead, _) = + declare_object {(default_object "HEAD") with + cache_function = cache_head; + load_function = load_head; + subst_function = subst_head; + classify_function = (fun (_,x) -> Substitute x); + discharge_function = discharge_head; + rebuild_function = rebuild_head; + export_function = export_head } + +let declare_head c = + let hd = compute_head c in + add_anonymous_leaf (inHead (c,hd)) + +(** Printing *) + +let pr_head = function +| RigidHead (RigidParameter cst) -> str "rigid constant " ++ pr_con cst +| RigidHead (RigidType) -> str "rigid type" +| RigidHead (RigidVar id) -> str "rigid variable " ++ pr_id id +| ConstructorHead -> str "constructor" +| FlexibleHead (k,n,p,b) -> int n ++ str "th of " ++ int k ++ str " binders applied to " ++ int p ++ str " arguments" ++ (if b then str " (with case)" else mt()) +| NotImmediatelyComputableHead -> str "unknown" + + diff --git a/library/heads.mli b/library/heads.mli new file mode 100644 index 000000000..4a086b9dc --- /dev/null +++ b/library/heads.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Names +open Term +open Environ + +(** This module is about the computation of an approximation of the + head symbol of defined constants and local definitions; it + provides the function to compute the head symbols and a table to + store the heads *) + +(* [declared_head] computes and registers the head symbol of a + possibly evaluable constant or variable *) + +val declare_head : evaluable_global_reference -> unit + +(* [is_rigid] tells if some term is known to ultimately reduce to a term + with a rigid head symbol *) + +val is_rigid : env -> constr -> bool diff --git a/library/libobject.mli b/library/libobject.mli index 15de388ea..33ad67c84 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -51,6 +51,14 @@ open Mod_subst this function should be declared for substitutive objects only (see obove) + * a discharge function, that is applied at section closing time to + collect the data necessary to rebuild the discharged form of the + non volatile objects + + * a rebuild function, that is applied after section closing to + rebuild the non volatile content of a section from the data + collected by the discharge function + * an export function, to enable optional writing of its contents to disk (.vo). This function is also the oportunity to remove redundant information in order to keep .vo size small diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 48fe40cab..6ca3a5c1a 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -360,12 +360,12 @@ let gallina_print_inductive sp = (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 print_named_decl id = + gallina_print_named_decl (Global.lookup_named id) ++ fnl () -let gallina_print_section_variable sp = - print_named_decl sp ++ - with_line_skip (print_name_infos (VarRef sp)) +let gallina_print_section_variable id = + print_named_decl id ++ + with_line_skip (print_name_infos (VarRef id)) let print_body = function | Some lc -> pr_lconstr (Declarations.force lc) diff --git a/parsing/search.ml b/parsing/search.ml index fd9eb12bb..88b51907b 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -50,11 +50,11 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = let crible_rec (sp,_) lobj = match object_tag lobj with | "VARIABLE" -> (try - let (idc,_,typ) = get_variable (basename sp) in + let (id,_,typ) = Global.lookup_named (basename sp) in if refopt = None || head_const typ = constr_of_global (Option.get refopt) then - fn (VarRef idc) env typ + fn (VarRef id) env typ with Not_found -> (* we are in a section *) ()) | "CONSTANT" -> let cst = locate_constant (qualid_of_sp sp) in diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 5b0c2eb36..0d7e3d611 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -44,7 +44,7 @@ type coe_typ = global_reference type coe_info_typ = { coe_value : constr; coe_type : types; - coe_strength : strength; + coe_strength : locality; coe_is_identity : bool; coe_param : int } @@ -290,7 +290,7 @@ let add_coercion_in_graph (ic,source,target) = if (!ambig_paths <> []) && is_verbose () then ppnl (message_ambig !ambig_paths) -type coercion = coe_typ * strength * bool * cl_typ * cl_typ * int +type coercion = coe_typ * locality * bool * cl_typ * cl_typ * int (* Calcul de l'arité d'une classe *) @@ -304,7 +304,7 @@ let class_params = function | CL_SECVAR sp -> reference_arity_length (VarRef sp) | CL_IND sp -> reference_arity_length (IndRef sp) -(* add_class : cl_typ -> strength option -> bool -> unit *) +(* add_class : cl_typ -> locality_flag option -> bool -> unit *) let add_class cl = add_new_class cl { cl_param = class_params cl } @@ -366,6 +366,8 @@ let coercion_identity v = v.coe_is_identity (* For printing purpose *) let get_coercion_value v = v.coe_value +let pr_cl_index n = int n + let classes () = Bijint.dom !class_tab let coercions () = Gmap.rng !coercion_tab let inheritance_graph () = Gmap.to_list !inheritance_graph diff --git a/pretyping/classops.mli b/pretyping/classops.mli index dd51ee970..c1a62b34f 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -66,7 +66,7 @@ val class_args_of : constr -> constr list (*s [declare_coercion] adds a coercion in the graph of coercion paths *) val declare_coercion : - coe_typ -> strength -> isid:bool -> + coe_typ -> locality -> isid:bool -> src:cl_typ -> target:cl_typ -> params:int -> unit (*s Access to coercions infos *) @@ -90,6 +90,7 @@ val install_path_printer : (*s This is for printing purpose *) val string_of_class : cl_typ -> string val pr_class : cl_typ -> std_ppcmds +val pr_cl_index : cl_index -> std_ppcmds val get_coercion_value : coe_index -> constr val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list val classes : unit -> cl_typ list diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index ed9d779ad..e7423c748 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -28,15 +28,7 @@ open Unification open Mod_subst open Coercion.Default -(* *) -let w_coerce env c ctyp target evd = - try - let j = make_judge c ctyp in - let tycon = mk_tycon_type target in - let (evd',j') = inh_conv_coerce_to dummy_loc env evd j tycon in - (evd',j'.uj_val) - with e when precatchable_exception e -> - evd,c +(* Abbreviations *) let pf_env gls = Global.env_of_context gls.it.evar_hyps let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c @@ -398,36 +390,24 @@ let error_already_defined b = anomalylabstrm "" (str "Position " ++ int n ++ str" already defined") -let rec similar_type_shapes t u = - let t,_ = decompose_app t and u,_ = decompose_app u in - match kind_of_term t, kind_of_term u with - | Prod (_,t1,t2), Prod (_,u1,u2) -> similar_type_shapes t2 u2 - | Const cst, Const cst' -> cst = cst' - | Var id, Var id' -> id = id' - | Ind ind, Ind ind' -> ind = ind' - | Rel n, Rel n' -> n = n' - | Sort s, Sort s' -> family_of_sort s = family_of_sort s' - | Case (_,_,c,_), Case (_,_,c',_) -> similar_type_shapes c c' - | _ -> false - -let clenv_unify_similar_types clenv c t u = - if occur_meta u then - if similar_type_shapes t u then - try TypeProcessed, clenv_unify true CUMUL t u clenv, c - with e when precatchable_exception e -> TypeNotProcessed, clenv, c - else - CoerceToType, clenv, c +let clenv_unify_binding_type clenv c t u = + if isMeta (fst (whd_stack u)) then + (* Not enough information to know if some subtyping is needed *) + CoerceToType, clenv, c else - let evd,c = w_coerce (cl_env clenv) c t u clenv.evd in - TypeProcessed, { clenv with evd = evd }, c + (* Enough information so as to try a coercion now *) + try + let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in + TypeProcessed, { clenv with evd = evd }, c + with e when precatchable_exception e -> + TypeNotProcessed, clenv, c let clenv_assign_binding clenv k (sigma,c) = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in let c_typ = clenv_hnf_constr clenv' c_typ in - let status,clenv'',c = clenv_unify_similar_types clenv' c c_typ k_typ in -(* let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in*) + let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd } let clenv_match_args bl clenv = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 729bd84f1..bd023721a 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -48,7 +48,9 @@ module type S = sig [j.uj_type] are convertible; it fails if no coercion is applicable *) val inh_conv_coerce_to : loc -> env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment - + + val inh_conv_coerce_rigid_to : loc -> + env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment (* [inh_conv_coerces_to loc env evd t t'] checks if an object of type [t] is coercible to an object of type [t'] adding evar constraints if needed; @@ -158,7 +160,11 @@ module Default = struct let inh_coerce_to_base loc env evd j = (evd, j) - let inh_coerce_to_fail env evd c1 v t = + let inh_coerce_to_fail env evd rigidonly v c1 t = + if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t) + then + raise NoCoercion + else let v', t' = try let t1,i1 = class_of1 env evd c1 in @@ -171,77 +177,44 @@ module Default = struct | None -> None, t with Not_found -> raise NoCoercion in - try (the_conv_x_leq env t' c1 evd, v', t') + try (the_conv_x_leq env t' c1 evd, v') with Reduction.NotConvertible -> raise NoCoercion - let rec inh_conv_coerce_to_fail loc env evd v t c1 = - try (the_conv_x_leq env t c1 evd, v, t) + let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = + try (the_conv_x_leq env t c1 evd, v) with Reduction.NotConvertible -> - try inh_coerce_to_fail env evd c1 v t + try inh_coerce_to_fail env evd rigidonly v c1 t with NoCoercion -> match kind_of_term (whd_betadeltaiota env (evars_of evd) t), kind_of_term (whd_betadeltaiota env (evars_of evd) c1) with - | Prod (_,t1,t2), Prod (name,u1,u2) -> - let v' = Option.map (whd_betadeltaiota env (evars_of evd)) v in - let (evd',b) = - match v' with - | Some v' -> - (match kind_of_term v' with - | Lambda (x,v1,v2) -> - (* sous-typage non contravariant: pas de "leq v1 u1" *) - (try the_conv_x env v1 u1 evd, Some (x, v1, v2) - with Reduction.NotConvertible -> (evd, None)) - | _ -> (evd, None)) - | None -> (evd, None) - in - (match b with - | Some (x, v1, v2) -> - let env1 = push_rel (x,None,v1) env in - let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd' - (Some v2) t2 u2 in - (evd'', Option.map (fun v2' -> mkLambda (x, v1, v2')) v2', - mkProd (x, v1, t2')) - | None -> - (* Mismatch on t1 and u1 or not a lambda: we eta-expand *) - (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *) - (* has type (name:u1)u2 (with v' recursively obtained) *) - let name = match name with - | Anonymous -> Name (id_of_string "x") - | _ -> name - in - let env1 = push_rel (name,None,u1) env in - let (evd', v1', t1') = - inh_conv_coerce_to_fail loc env1 evd - (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) - in - let (evd'', v2', t2') = - let v2 = - match v with - | Some v -> Option.map (fun x -> mkApp(lift 1 v,[|x|])) v1' - | None -> None - and evd', t2 = - match v1' with - | Some v1' -> evd', subst_term v1' t2 - | None -> - let evd', ev = - new_evar evd' env ~src:(loc, InternalHole) t1' in - evd', subst_term ev t2 - in - inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2 - in - (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2', - mkProd (name, u1, t2'))) + | Prod (name,t1,t2), Prod (_,u1,u2) -> + (* Conversion did not work, we may succeed with a coercion. *) + (* We eta-expand (hence possibly modifying the original term!) *) + (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *) + (* has type forall (x:u1), u2 (with v' recursively obtained) *) + let name = match name with + | Anonymous -> Name (id_of_string "x") + | _ -> name in + let env1 = push_rel (name,None,u1) env in + let (evd', v1) = + inh_conv_coerce_to_fail loc env1 evd rigidonly + (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in + let v1 = Option.get v1 in + let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in + let t2 = subst_term v1 t2 in + let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in + (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') | _ -> raise NoCoercion (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) - let inh_conv_coerce_to loc env evd cj (n, t) = + let inh_conv_coerce_to_gen rigidonly loc env evd cj (n, t) = match n with None -> - let (evd', val', type') = + let (evd', val') = try - inh_conv_coerce_to_fail loc env evd (Some cj.uj_val) cj.uj_type t + inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercion -> let sigma = evars_of evd in error_actual_type_loc loc env sigma cj t @@ -249,6 +222,10 @@ module Default = struct let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) | Some (init, cur) -> (evd, cj) + + let inh_conv_coerce_to = inh_conv_coerce_to_gen false + let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true + let inh_conv_coerces_to loc env (evd : evar_defs) t (abs, t') = evd (* Still problematic, as it changes unification diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 5476a4820..00735d874 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -45,6 +45,9 @@ module type S = sig [j.uj_type] are convertible; it fails if no coercion is applicable *) val inh_conv_coerce_to : loc -> env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment + + val inh_conv_coerce_rigid_to : loc -> + env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] is coercible to an object of type [t'] adding evar constraints if needed; diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 3adf749f0..ddc3654dc 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -341,7 +341,7 @@ let mk_freelisted c = let map_fl f cfl = { cfl with rebus=f cfl.rebus } -(* Status of an instance wrt to the meta it solves: +(* Status of an instance found by unification wrt to the meta it solves: - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X) - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X) - a term that can be eta-expanded n times while still being a solution @@ -351,9 +351,24 @@ let map_fl f cfl = { cfl with rebus=f cfl.rebus } type instance_constraint = IsSuperType | IsSubType | ConvUpToEta of int | UserGiven +(* Status of the unification of the type of an instance against the type of + the meta it instantiates: + - CoerceToType means that the unification of types has not been done + and that a coercion can still be inserted: the meta should not be + substituted freely (this happens for instance given via the + "with" binding clause). + - TypeProcessed means that the information obtainable from the + unification of types has been extracted. + - TypeNotProcessed means that the unification of types has not been + done but it is known that no coercion may be inserted: the meta + can be substituted freely. +*) + type instance_typing_status = CoerceToType | TypeNotProcessed | TypeProcessed +(* Status of an instance together with the status of its type unification *) + type instance_status = instance_constraint * instance_typing_status (* Clausal environments *) @@ -519,6 +534,13 @@ let metas_of evd = | (n,Cltyp (_,typ)) -> (n,typ.rebus)) (meta_list evd) +let map_metas_fvalue f evd = + { evd with metas = + Metamap.map + (function + | Clval(id,(c,s),typ) -> Clval(id,(mk_freelisted (f c.rebus),s),typ) + | x -> x) evd.metas } + let meta_opt_fvalue evd mv = match Metamap.find mv evd.metas with | Clval(_,b,_) -> Some b diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 352d3021d..71c6bb0dc 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -122,11 +122,28 @@ val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted type instance_constraint = IsSuperType | IsSubType | ConvUpToEta of int | UserGiven +(* Status of the unification of the type of an instance against the type of + the meta it instantiates: + - CoerceToType means that the unification of types has not been done + and that a coercion can still be inserted: the meta should not be + substituted freely (this happens for instance given via the + "with" binding clause). + - TypeProcessed means that the information obtainable from the + unification of types has been extracted. + - TypeNotProcessed means that the unification of types has not been + done but it is known that no coercion may be inserted: the meta + can be substituted freely. +*) + type instance_typing_status = CoerceToType | TypeNotProcessed | TypeProcessed +(* Status of an instance together with the status of its type unification *) + type instance_status = instance_constraint * instance_typing_status +(* Clausal environments *) + type clbinding = | Cltyp of name * constr freelisted | Clval of name * (constr freelisted * instance_status) * constr freelisted @@ -198,6 +215,7 @@ val meta_merge : evar_defs -> evar_defs -> evar_defs val undefined_metas : evar_defs -> metavariable list val metas_of : evar_defs -> metamap +val map_metas_fvalue : (constr -> constr) -> evar_defs -> evar_defs type metabinding = metavariable * constr * instance_status diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e118a659e..e825b3f48 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -946,7 +946,7 @@ let meta_reducible_instance evd b = (match try let g,s = List.assoc m metas in - if isConstruct g or s = TypeProcessed then Some g else None + if isConstruct g or s <> CoerceToType then Some g else None with Not_found -> None with | Some g -> irec (mkCase (ci,p,g,bl)) @@ -956,13 +956,13 @@ let meta_reducible_instance evd b = (match try let g,s = List.assoc m metas in - if isLambda g or s = TypeProcessed then Some g else None + if isLambda g or s <> CoerceToType then Some g else None with Not_found -> None with | Some g -> irec (mkApp (g,l)) | None -> mkApp (f,Array.map irec l)) | Meta m -> - (try let g,s = List.assoc m metas in if s=TypeProcessed then irec g else u + (try let g,s = List.assoc m metas in if s<>CoerceToType then irec g else u with Not_found -> u) | _ -> map_constr irec u in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index c5e9dff8b..b140ad51a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -24,6 +24,7 @@ open Pattern open Evarutil open Pretype_errors open Retyping +open Coercion.Default (* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms, gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *) @@ -380,14 +381,39 @@ let is_mimick_head f = (Const _|Var _|Rel _|Construct _|Ind _) -> true | _ -> false -let w_coerce env c ctyp target evd = +let pose_all_metas_as_evars env evd t = + let evdref = ref evd in + let rec aux t = match kind_of_term t with + | Meta mv -> + (match Evd.meta_opt_fvalue !evdref mv with + | Some ({rebus=c},_) -> c + | None -> + let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in + let ty = if mvs = Evd.Metaset.empty then ty else aux ty in + let ev = Evarutil.e_new_evar evdref env ~src:(dummy_loc,GoalEvar) ty in + evdref := meta_assign mv (ev,(ConvUpToEta 0,TypeNotProcessed)) !evdref; + ev) + | _ -> + map_constr aux t in + let c = aux t in + (* side-effect *) + (!evdref, c) + +let w_coerce_to_type env evd c cty mvty = try - let j = make_judge c ctyp in - let tycon = mk_tycon_type target in - let (evd',j') = Coercion.Default.inh_conv_coerce_to dummy_loc env evd j tycon in + let j = make_judge c cty in + let evd,mvty = pose_all_metas_as_evars env evd mvty in + let tycon = mk_tycon_type mvty in + let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in + let evd' = Evd.map_metas_fvalue (nf_evar (evars_of evd')) evd' in (evd',j'.uj_val) with e when precatchable_exception e -> - evd,c + (evd,c) + +let w_coerce env evd mv c = + let cty = get_type_of env (evars_of evd) c in + let mvty = Typing.meta_type evd mv in + w_coerce_to_type env evd c cty mvty let unify_to_type env evd flags c u = let sigma = evars_of evd in @@ -398,20 +424,6 @@ let unify_to_type env evd flags c u = try unify_0 env sigma Cumul flags t u with e when precatchable_exception e -> ([],[]) -let coerce_to_type env evd c u = - let c = refresh_universes c in - let t = get_type_of_with_meta env (evars_of evd) (metas_of evd) c in - w_coerce env c t u evd - -let unify_or_coerce_type env evd flags mv c = - let mvty = Typing.meta_type evd mv in - (* nf_betaiota was before in type_of - useful to reduce - types like (x:A)([x]P u) *) - if occur_meta mvty then - (evd,c),unify_to_type env evd flags c mvty - else - coerce_to_type env evd c mvty,([],[]) - let unify_type env evd flags mv c = let mvty = Typing.meta_type evd mv in if occur_meta mvty then @@ -471,7 +483,7 @@ let w_merge env with_types flags metas evars evd = if with_types & to_type <> TypeProcessed then if to_type = CoerceToType then (* Some coercion may have to be inserted *) - (unify_or_coerce_type env evd flags mv c,[]) + (w_coerce env evd mv c,([],[])),[] else (* No coercion needed: delay the unification of types *) ((evd,c),([],[])),(mv,c)::eqns diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 9156623f5..1b8f9ccd8 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -35,6 +35,11 @@ val w_unify_to_subterm : val w_unify_meta_types : env -> ?flags:unify_flags -> evar_defs -> evar_defs +(* [w_coerce_to_type env evd c ctyp typ] tries to coerce [c] of type + [ctyp] so that its gets type [typ]; [typ] may contain metavariables *) +val w_coerce_to_type : env -> evar_defs -> constr -> types -> types -> + evar_defs * constr + (*i This should be in another module i*) (* [abstract_list_all env evd t c l] *) diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index ca25c722c..a13f8bf70 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -16,6 +16,7 @@ open Rawterm open Util open Genarg open Pattern +open Decl_kinds type 'a or_metaid = AI of 'a | MetaId of loc * string @@ -325,4 +326,4 @@ type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type -type declaration_hook = Decl_kinds.strength -> global_reference -> unit +type declaration_hook = locality -> global_reference -> unit diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 5402e6120..e3e90c7ca 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -207,7 +207,7 @@ let classify_hintrewrite (_,x) = Libobject.Substitute x (* Declaration of the Hint Rewrite library object *) -let (in_hintrewrite,out_hintrewrite)= +let (inHintRewrite,outHintRewrite)= Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with Libobject.cache_function = cache_hintrewrite; Libobject.load_function = (fun _ -> cache_hintrewrite); @@ -223,4 +223,4 @@ let add_rew_rules base lrul = (c,mkProp (* dummy value *), b,Tacinterp.glob_tactic t) ) lrul in - Lib.add_anonymous_leaf (in_hintrewrite (base,lrul)) + Lib.add_anonymous_leaf (inHintRewrite (base,lrul)) diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index b19df1aee..dc8ff2b9c 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -923,7 +923,7 @@ let new_morphism m signature id hook = new_edited id (m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr); Pfedit.start_proof id (Global, Proof Lemma) - (Declare.clear_proofs (Global.named_context ())) + (Decls.clear_proofs (Global.named_context ())) lem hook; Flags.if_verbose msg (Printer.pr_open_subgoals ()); end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 34c2f690c..d3f7cc5f1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -909,10 +909,12 @@ let specialize mopt (c,lbind) g = (match kind_of_term (fst (decompose_app c)) with | Var id when List.exists (fun (i,_,_)-> i=id) (pf_hyps g) -> let id' = fresh_id [] id g in - tclTHENS (internal_cut id' (pf_type_of g term)) + tclTHENS (fun g -> internal_cut id' (pf_type_of g term) g) [ exact_no_check term; tclTHEN (clear [id]) (rename_hyp [id',id]) ] - | _ -> tclTHENLAST (cut (pf_type_of g term)) (exact_no_check term)) + | _ -> tclTHENLAST + (fun g -> cut (pf_type_of g term) g) + (exact_no_check term)) g (* Keeping only a few hypotheses *) @@ -2208,7 +2210,7 @@ let mapi f l = mapi_aux f 0 l -(* Instanciate all meta variables of elimclause using lid, some elts +(* Instantiate all meta variables of elimclause using lid, some elts of lid are parameters (first ones), the other are arguments. Returns the clause obtained. *) let recolle_clenv scheme lid elimclause gl = diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 014f6ffcd..3b4e8af21 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -163,3 +163,14 @@ apply H. try apply H. unfold ID; apply H0. Qed. + +(* Test coercion below product and on non meta-free terms in with bindings *) +(* Cf wishes #1408 from E. Makarov *) + +Parameter bool_Prop :> bool -> Prop. +Parameter r : bool -> bool -> bool. +Axiom ax : forall (A : Set) (R : A -> A -> Prop) (x y : A), R x y. + +Theorem t : r true false. +apply ax with (R := r). +Qed. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index faeecdf9d..f5cee92c7 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -32,17 +32,17 @@ Section identity_is_a_congruence. Lemma sym_id : identity x y -> identity y x. Proof. destruct 1; trivial. - Qed. + Defined. Lemma trans_id : identity x y -> identity y z -> identity x z. Proof. destruct 2; trivial. - Qed. + Defined. Lemma congr_id : identity x y -> identity (f x) (f y). Proof. destruct 1; trivial. - Qed. + Defined. Lemma sym_not_id : notT (identity x y) -> notT (identity y x). Proof. diff --git a/toplevel/class.ml b/toplevel/class.ml index f7d709480..7e5fc1297 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -27,28 +27,12 @@ open Nametab open Decl_kinds open Safe_typing -let strength_min4 stre1 stre2 stre3 stre4 = - strength_min ((strength_min (stre1,stre2)),(strength_min (stre3,stre4))) +let strength_min l = if List.mem Local l then Local else Global let id_of_varid c = match kind_of_term c with | Var id -> id | _ -> anomaly "class__id_of_varid" -(* lf liste des variable dont depend la coercion f - lc liste des variable dont depend la classe source *) - -let rec stre_unif_cond = function - | ([],[]) -> Global - | (v::l,[]) -> variable_strength v - | ([],v::l) -> variable_strength v - | (v1::l1,v2::l2) -> - if v1=v2 then - stre_unif_cond (l1,l2) - else - let stre1 = (variable_strength v1) - and stre2 = (variable_strength v2) in - strength_min (stre1,stre2) - (* Errors *) type coercion_error_kind = @@ -98,9 +82,9 @@ let check_reference_arity ref = let check_arity = function | CL_FUN | CL_SORT -> () - | CL_CONST sp -> check_reference_arity (ConstRef sp) - | CL_SECVAR sp -> check_reference_arity (VarRef sp) - | CL_IND sp -> check_reference_arity (IndRef sp) + | CL_CONST cst -> check_reference_arity (ConstRef cst) + | CL_SECVAR id -> check_reference_arity (VarRef id) + | CL_IND kn -> check_reference_arity (IndRef kn) (* Coercions *) @@ -184,20 +168,15 @@ let prods_of t = aux [] t let strength_of_cl = function - | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn)) - | CL_SECVAR sp -> variable_strength sp + | CL_CONST kn -> Global + | CL_SECVAR id -> Local | _ -> Global let get_strength stre ref cls clt = let stres = strength_of_cl cls in let stret = strength_of_cl clt in let stref = strength_of_global ref in -(* 01/00: Supprimé la prise en compte de la force des variables locales. Sens ? - let streunif = stre_unif_cond (s_vardep,f_vardep) in - *) - let streunif = Global in - let stre' = strength_min4 stres stret stref streunif in - strength_min (stre,stre') + strength_min [stre;stres;stret;stref] (* coercion identité *) diff --git a/toplevel/class.mli b/toplevel/class.mli index 34af2e326..3bbc2f043 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -22,28 +22,28 @@ open Nametab (* [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion from [src] to [tg] *) -val try_add_new_coercion_with_target : global_reference -> strength -> +val try_add_new_coercion_with_target : global_reference -> locality -> source:cl_typ -> target:cl_typ -> unit (* [try_add_new_coercion ref s] declares [ref], assumed to be of type [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *) -val try_add_new_coercion : global_reference -> strength -> unit +val try_add_new_coercion : global_reference -> locality -> unit (* [try_add_new_coercion_subclass cst s] expects that [cst] denotes a transparent constant which unfolds to some class [tg]; it declares an identity coercion from [cst] to [tg], named something like ["Id_cst_tg"] *) -val try_add_new_coercion_subclass : cl_typ -> strength -> unit +val try_add_new_coercion_subclass : cl_typ -> locality -> unit (* [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion from [src] to [tg] where the target is inferred from the type of [ref] *) -val try_add_new_coercion_with_source : global_reference -> strength -> +val try_add_new_coercion_with_source : global_reference -> locality -> source:cl_typ -> unit (* [try_add_new_identity_coercion id s src tg] enriches the environment with a new definition of name [id] declared as an identity coercion from [src] to [tg] *) -val try_add_new_identity_coercion : identifier -> strength -> +val try_add_new_identity_coercion : identifier -> locality -> source:cl_typ -> target:cl_typ -> unit val add_coercion_hook : Tacexpr.declaration_hook diff --git a/toplevel/command.ml b/toplevel/command.ml index bc8f6c9ee..8c368ec2e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -45,6 +45,7 @@ open Notation open Goptions open Mod_subst open Evd +open Decls let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,default_binder_kind,a,b)) let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,default_binder_kind,a,b)) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 6b8fcdead..976677f8c 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -220,8 +220,8 @@ type vernac_expr = export_flag option * specif_flag option * lreference list | VernacImport of export_flag * lreference list | VernacCanonical of lreference - | VernacCoercion of strength * lreference * class_rawexpr * class_rawexpr - | VernacIdentityCoercion of strength * lident * + | VernacCoercion of locality * lreference * class_rawexpr * class_rawexpr + | VernacIdentityCoercion of locality * lident * class_rawexpr * class_rawexpr (* Type classes *) |