diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 153 |
1 files changed, 99 insertions, 54 deletions
diff --git a/library/declare.ml b/library/declare.ml index c349bef1..3e4853c8 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: declare.ml 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id$ *) (** This module is about the low-level declaration of logical objects *) @@ -27,11 +27,17 @@ open Cooking open Decls open Decl_kinds +(** flag for internal message display *) +type internal_flag = + | KernelVerbose (* kernel action, a message is displayed *) + | KernelSilent (* kernel action, no message is displayed *) + | UserVerbose (* user action, a message is displayed *) + (** 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) -> ()) +let xml_declare_constant = ref (fun (sp:internal_flag * constant)-> ()) +let xml_declare_inductive = ref (fun (sp:internal_flag * object_name) -> ()) let if_xml f x = if !Flags.xml_export then f x else () @@ -39,11 +45,14 @@ 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 +let cache_hook = ref ignore +let add_cache_hook f = cache_hook := f + (** Declaration of section variables and local definitions *) type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) - | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep *) + | SectionLocalAssum of types * bool (* Implicit status *) type variable_declaration = dir_path * section_variable_entry * logical_kind @@ -53,18 +62,17 @@ let cache_variable ((sp,_),o) = | Inr (id,(p,d,mk)) -> (* Constr raisonne sur les noms courts *) if variable_exists id then - errorlabstrm "cache_variable" (pr_id id ++ str " already exists"); - let impl,opaq,cst,keep = match d with (* Fails if not well-typed *) - | SectionLocalAssum (ty, impl, keep) -> + alreadydeclared (pr_id id ++ str " already exists"); + let impl,opaq,cst = match d with (* Fails if not well-typed *) + | SectionLocalAssum (ty, impl) -> let cst = Global.push_named_assum (id,ty) in let impl = if impl then Lib.Implicit else Lib.Explicit in - let keep = if keep <> [] then Some (ty, keep) else None in - impl, true, cst, keep - | SectionLocalDef (c,t,opaq) -> + impl, true, cst + | SectionLocalDef (c,t,opaq) -> let cst = Global.push_named_def (id,c,t) in - Lib.Explicit, opaq, cst, None in + Lib.Explicit, opaq, cst in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); - add_section_variable id impl keep; + add_section_variable id impl; Dischargedhypsmap.set_discharged_hyps sp []; add_variable_data id (p,opaq,cst,mk) @@ -72,7 +80,7 @@ let discharge_variable (_,o) = match o with | Inr (id,_) -> Some (Inl (variable_constraints id)) | Inl _ -> Some o -let (inVariable, outVariable) = +let (inVariable,_) = declare_object { (default_object "VARIABLE") with cache_function = cache_variable; discharge_function = discharge_variable; @@ -87,6 +95,7 @@ let declare_variable id obj = !xml_declare_variable oname; oname + (** Declaration of constants and parameters *) type constant_declaration = constant_entry * logical_kind @@ -95,26 +104,28 @@ type constant_declaration = constant_entry * logical_kind (* section (if Remark or Fact) is needed to access a construction *) let load_constant i ((sp,kn),(_,_,kind)) = if Nametab.exists_cci sp then - errorlabstrm "cache_constant" - (pr_id (basename sp) ++ str " already exists"); - Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn)); - add_constant_kind (constant_of_kn kn) kind + alreadydeclared (pr_id (basename sp) ++ str " already exists"); + let con = Global.constant_of_delta (constant_of_kn kn) in + Nametab.push (Nametab.Until i) sp (ConstRef con); + add_constant_kind con kind (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn),_) = - Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn)) + let con = Global.constant_of_delta (constant_of_kn kn) in + Nametab.push (Nametab.Exactly i) sp (ConstRef con) let cache_constant ((sp,kn),(cdt,dhyps,kind)) = let id = basename sp in let _,dir,_ = repr_kn kn in if variable_exists id or Nametab.exists_cci sp then - errorlabstrm "cache_constant" (pr_id id ++ str " already exists"); + alreadydeclared (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; - add_constant_kind (constant_of_kn kn) kind + add_constant_kind (constant_of_kn kn) kind; + !cache_hook sp let discharged_hyps kn sechyps = let (_,dir,_) = repr_kn kn in @@ -134,19 +145,16 @@ let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,false)) let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk -let export_constant cst = Some (dummy_constant cst) - -let classify_constant (_,cst) = Substitute (dummy_constant cst) +let classify_constant cst = Substitute (dummy_constant cst) -let (inConstant, outConstant) = +let (inConstant,_) = declare_object { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; open_function = open_constant; classify_function = classify_constant; subst_function = ident_subst_function; - discharge_function = discharge_constant; - export_function = export_constant } + discharge_function = discharge_constant } let hcons_constant_declaration = function | DefinitionEntry ce when !Flags.hash_cons_proofs -> @@ -154,17 +162,17 @@ let hcons_constant_declaration = function DefinitionEntry { const_entry_body = hcons1_constr ce.const_entry_body; const_entry_type = Option.map hcons1_constr ce.const_entry_type; - const_entry_opaque = ce.const_entry_opaque; + const_entry_opaque = ce.const_entry_opaque; const_entry_boxed = ce.const_entry_boxed } | cd -> cd let declare_constant_common id dhyps (cd,kind) = 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 + let c = Global.constant_of_delta (constant_of_kn kn) in + declare_constant_implicits c; + Heads.declare_head (EvalConstRef c); + Notation.declare_ref_arguments_scope (ConstRef c); + c let declare_constant_gen internal id (cd,kind) = let cd = hcons_constant_declaration cd in @@ -172,8 +180,10 @@ let declare_constant_gen internal id (cd,kind) = !xml_declare_constant (internal,kn); kn -let declare_internal_constant = declare_constant_gen true -let declare_constant = declare_constant_gen false +(* TODO: add a third function to distinguish between KernelVerbose + * and user Verbose *) +let declare_internal_constant = declare_constant_gen KernelSilent +let declare_constant = declare_constant_gen UserVerbose (** Declaration of inductive blocks *) @@ -186,14 +196,15 @@ let declare_inductive_argument_scopes kn mie = let inductive_names sp kn mie = let (dp,_) = repr_path sp in - let names, _ = + let kn = Global.mind_of_delta (mind_of_kn kn) in + let names, _ = List.fold_left (fun (names, n) ind -> let ind_p = (kn,n) in let names, _ = List.fold_left (fun (names, p) l -> - let sp = + let sp = Libnames.make_path dp l in ((sp, ConstructRef (ind_p,p)) :: names, p+1)) @@ -206,16 +217,15 @@ let inductive_names sp kn mie = let check_exists_inductive (sp,_) = (if variable_exists (basename sp) then - errorlabstrm "" - (pr_id (basename sp) ++ str " already exists")); + alreadydeclared (pr_id (basename sp) ++ str " already exists")); if Nametab.exists_cci sp then let (_,id) = repr_path sp in - errorlabstrm "" (pr_id id ++ str " already exists") + alreadydeclared (pr_id id ++ str " already exists") let load_inductive i ((sp,kn),(_,mie)) = let names = inductive_names sp kn mie in List.iter check_exists_inductive names; - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref) names + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names let open_inductive i ((sp,kn),(_,mie)) = let names = inductive_names sp kn mie in @@ -227,15 +237,18 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = let id = basename sp in let _,dir,_ = repr_kn kn in let kn' = Global.add_mind dir id mie in - assert (kn'=kn); - add_section_kn kn (Global.lookup_mind kn').mind_hyps; + assert (kn'= mind_of_kn kn); + add_section_kn kn' (Global.lookup_mind kn').mind_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names; + List.iter (fun (sp,_) -> !cache_hook sp) (inductive_names sp kn mie) + let discharge_inductive ((sp,kn),(dhyps,mie)) = - let mie = Global.lookup_mind kn in + let mind = (Global.mind_of_delta (mind_of_kn kn)) in + let mie = Global.lookup_mind mind in let repl = replacement_context () in - let sechyps = section_segment_of_mutual_inductive kn in + let sechyps = section_segment_of_mutual_inductive mind in Some (discharged_hyps kn sechyps, Discharge.process_inductive (named_of_variable_context sechyps) repl mie) @@ -253,17 +266,14 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_finite = true; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }) -let export_inductive x = Some (dummy_inductive_entry x) - -let (inInductive, outInductive) = - declare_object {(default_object "INDUCTIVE") with +let (inInductive,_) = + declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; open_function = open_inductive; - classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a)); + classify_function = (fun a -> Substitute (dummy_inductive_entry a)); subst_function = ident_subst_function; - discharge_function = discharge_inductive; - export_function = export_inductive } + discharge_function = discharge_inductive } (* for initial declaration *) let declare_mind isrecord mie = @@ -271,8 +281,43 @@ let declare_mind isrecord mie = | ind::_ -> ind.mind_entry_typename | [] -> anomaly "cannot declare an empty list of inductives" in let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in - declare_mib_implicits kn; - declare_inductive_argument_scopes kn mie; + let mind = (Global.mind_of_delta (mind_of_kn kn)) in + declare_mib_implicits mind; + declare_inductive_argument_scopes mind mie; !xml_declare_inductive (isrecord,oname); oname +(* Declaration messages *) + +let pr_rank i = str (ordinal (i+1)) + +let fixpoint_message indexes l = + Flags.if_verbose msgnl (match l with + | [] -> anomaly "no recursive definition" + | [id] -> pr_id id ++ str " is recursively defined" ++ + (match indexes with + | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" + | _ -> mt ()) + | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ + spc () ++ str "are recursively defined" ++ + match indexes with + | Some a -> spc () ++ str "(decreasing respectively on " ++ + prlist_with_sep pr_comma pr_rank (Array.to_list a) ++ + str " arguments)" + | None -> mt ())) + +let cofixpoint_message l = + Flags.if_verbose msgnl (match l with + | [] -> anomaly "No corecursive definition." + | [id] -> pr_id id ++ str " is corecursively defined" + | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ + spc () ++ str "are corecursively defined")) + +let recursive_message isfix i l = + (if isfix then fixpoint_message i else cofixpoint_message) l + +let definition_message id = + Flags.if_verbose msgnl (pr_id id ++ str " is defined") + +let assumption_message id = + Flags.if_verbose msgnl (pr_id id ++ str " is assumed") |