diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/decl_kinds.ml | 21 | ||||
| -rw-r--r-- | library/decl_kinds.mli | 83 | ||||
| -rw-r--r-- | library/declare.ml | 175 | ||||
| -rw-r--r-- | library/declare.mli | 20 | ||||
| -rw-r--r-- | library/decls.ml | 76 | ||||
| -rw-r--r-- | library/decls.mli | 47 | ||||
| -rw-r--r-- | library/heads.ml | 190 | ||||
| -rw-r--r-- | library/heads.mli | 28 | ||||
| -rw-r--r-- | library/libobject.mli | 8 |
9 files changed, 473 insertions, 175 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 8ea1835094..20808f1e6e 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 0000000000..c9485fa5b2 --- /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 278acc6658..b524639ef8 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 96fd5eb9bc..93c8b9f919 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 0000000000..d84703271f --- /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 0000000000..96654bcbdd --- /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 0000000000..c341c835e0 --- /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 0000000000..4a086b9dc5 --- /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 15de388ea6..33ad67c84e 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 |