diff options
Diffstat (limited to 'library/declare.ml')
-rw-r--r-- | library/declare.ml | 262 |
1 files changed, 131 insertions, 131 deletions
diff --git a/library/declare.ml b/library/declare.ml index cfa8890a..b1e55c20 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: declare.ml,v 1.128.2.2 2005/11/29 21:40:52 letouzey Exp $ *) +(* $Id: declare.ml 7941 2006-01-28 23:07:59Z herbelin $ *) open Pp open Util @@ -31,11 +31,7 @@ open Decl_kinds (**********************************************) -(* For [DischargeAt (dir,n)], [dir] is the minimum prefix that a - construction keeps in its name (if persistent), or the section name - beyond which it is discharged (if volatile); the integer [n] - (useful only for persistent constructions), is the length of the section - part in [dir] *) +(* Strength *) open Nametab @@ -47,9 +43,9 @@ let string_of_strength = function | Global -> "(global)" (* XML output hooks *) -let xml_declare_variable = ref (fun sp -> ()) -let xml_declare_constant = ref (fun sp -> ()) -let xml_declare_inductive = ref (fun sp -> ()) +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 if_xml f x = if !Options.xml_export then f x else () @@ -63,25 +59,28 @@ type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) | SectionLocalAssum of types -type variable_declaration = dir_path * section_variable_entry * local_kind +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 * local_kind + 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,_),(id,(p,d,mk))) = + { 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 errorlabstrm "cache_variable" (pr_id id ++ str " already exists"); @@ -95,36 +94,38 @@ let cache_variable ((sp,_),(id,(p,d,mk))) = let (_,bd,ty) = Global.lookup_named id in CheckedSectionLocalDef (out_some bd,ty,cst,opaq) in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); + add_section_variable id; + 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 + +let discharge_variable (_,o) = match o with + | Inr (id,_) -> Some (Inl (get_variable_constraints id)) + | Inl _ -> Some o + let (in_variable, out_variable) = declare_object { (default_object "VARIABLE") with cache_function = cache_variable; + discharge_function = discharge_variable; classify_function = (fun _ -> Dispose) } -let declare_variable_common id obj = - let oname = add_leaf id (in_variable (id,obj)) in - declare_var_implicits id; - Symbols.declare_ref_arguments_scope (VarRef id); - oname - (* for initial declaration *) let declare_variable id obj = - let (sp,kn as oname) = declare_variable_common id obj in + let oname = add_leaf id (in_variable (Inr (id,obj))) in + declare_var_implicits id; + Notation.declare_ref_arguments_scope (VarRef id); !xml_declare_variable oname; - Dischargedhypsmap.set_discharged_hyps sp []; oname -(* when coming from discharge: no xml output *) -let redeclare_variable id discharged_hyps obj = - let oname = declare_variable_common id obj in - Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps - (* Globals: constants and parameters *) -type constant_declaration = constant_entry * global_kind +type constant_declaration = constant_entry * logical_kind -let csttab = ref (Spmap.empty : global_kind Spmap.t) +let csttab = ref (Spmap.empty : logical_kind Spmap.t) let _ = Summary.declare_summary "CONSTANT" { Summary.freeze_function = (fun () -> !csttab); @@ -133,37 +134,56 @@ let _ = Summary.declare_summary "CONSTANT" Summary.survive_module = false; Summary.survive_section = false } -let cache_constant ((sp,kn),(cdt,kind)) = - (if Idmap.mem (basename sp) !vartab then - errorlabstrm "cache_constant" - (pr_id (basename sp) ++ str " already exists")); - (if Nametab.exists_cci sp then - let (_,id) = repr_path sp in - errorlabstrm "cache_constant" (pr_id id ++ str " already exists")); - let _,dir,_ = repr_kn kn in - let kn' = Global.add_constant dir (basename sp) cdt in - if kn' <> kn then - anomaly "Kernel and Library names do not match"; - Nametab.push (Nametab.Until 1) sp (ConstRef kn); - csttab := Spmap.add sp kind !csttab - (* 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)) = - (if Nametab.exists_cci sp then - let (_,id) = repr_path sp in - errorlabstrm "cache_constant" (pr_id id ++ str " already exists")); - csttab := Spmap.add sp kind !csttab; - Nametab.push (Nametab.Until i) sp (ConstRef kn) +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)); + csttab := Spmap.add sp kind !csttab (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn),_) = - Nametab.push (Nametab.Exactly i) sp (ConstRef kn) + Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn)) + +let cache_constant ((sp,kn),(cdt,dhyps,imps,kind)) = + let id = basename sp in + let _,dir,_ = repr_kn kn in + if Idmap.mem id !vartab then + errorlabstrm "cache_constant" (pr_id id ++ str " already exists"); + if 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; + with_implicits imps declare_constant_implicits kn'; + Notation.declare_ref_arguments_scope (ConstRef kn'); + csttab := Spmap.add sp kind !csttab + +(*s Registration as global tables and rollback. *) + +open Cooking + +let discharged_hyps kn sechyps = + let (_,dir,_) = repr_kn kn in + let args = array_map_to_list destVar (instance_from_named_context sechyps) in + List.rev (List.map (Libnames.make_path dir) args) + +let discharge_constant ((sp,kn),(cdt,dhyps,imps,kind)) = + let con = constant_of_kn kn in + let cb = Global.lookup_constant con in + let (repl1,_ as repl) = replacement_context () in + let sechyps = section_segment (ConstRef con) in + let recipe = { d_from=cb; d_modlist=repl; d_abstract=sechyps } in + Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,imps,kind) (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp) -let dummy_constant (ce,mk) = dummy_constant_entry,mk +let dummy_constant (ce,_,imps,mk) = dummy_constant_entry,[],imps,mk let export_constant cst = Some (dummy_constant cst) @@ -176,40 +196,43 @@ let (in_constant, out_constant) = open_function = open_constant; classify_function = classify_constant; subst_function = ident_subst_function; + discharge_function = discharge_constant; export_function = export_constant } let hcons_constant_declaration = function - | DefinitionEntry ce -> + | DefinitionEntry ce when !Options.hash_cons_proofs -> let (hcons1_constr,_) = hcons_constr (hcons_names()) in DefinitionEntry { const_entry_body = hcons1_constr ce.const_entry_body; const_entry_type = option_app 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 discharged_hyps (cd,kind) = - let (sp,kn as oname) = add_leaf id (in_constant (cd,kind)) in - declare_constant_implicits kn; - Symbols.declare_ref_arguments_scope (ConstRef kn); - Dischargedhypsmap.set_discharged_hyps sp discharged_hyps; - oname +let declare_constant_common id dhyps (cd,kind) = + let imps = implicits_flags () in + let (sp,kn) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in + let kn = constant_of_kn kn in + kn let declare_constant_gen internal id (cd,kind) = let cd = hcons_constant_declaration cd in - let oname = declare_constant_common id [] (ConstantEntry cd,kind) in - !xml_declare_constant (internal,oname); - oname + let kn = declare_constant_common id [] (ConstantEntry cd,kind) in + !xml_declare_constant (internal,kn); + kn let declare_internal_constant = declare_constant_gen true let declare_constant = declare_constant_gen false -(* when coming from discharge *) -let redeclare_constant id discharged_hyps (cd,kind) = - let _ = declare_constant_common id discharged_hyps (GlobalRecipe cd,kind) in - () - (* Inductives. *) +let declare_inductive_argument_scopes kn mie = + list_iter_i (fun i {mind_entry_consnames=lc} -> + Notation.declare_ref_arguments_scope (IndRef (kn,i)); + for j=1 to List.length lc do + Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j)); + done) mie.mind_entry_inds + let inductive_names sp kn mie = let (dp,_) = repr_path sp in let names, _ = @@ -230,39 +253,44 @@ let inductive_names sp kn mie = ([], 0) mie.mind_entry_inds in names - let check_exists_inductive (sp,_) = (if Idmap.mem (basename sp) !vartab then - errorlabstrm "cache_inductive" + errorlabstrm "" (pr_id (basename sp) ++ str " already exists")); if Nametab.exists_cci sp then let (_,id) = repr_path sp in - errorlabstrm "cache_inductive" (pr_id id ++ str " already exists") + errorlabstrm "" (pr_id id ++ str " already exists") -let cache_inductive ((sp,kn),mie) = - let names = inductive_names sp kn mie in - List.iter check_exists_inductive names; - let _,dir,_ = repr_kn kn in - let kn' = Global.add_mind dir (basename sp) mie in - if kn' <> kn then - anomaly "Kernel and Library names do not match"; - - List.iter - (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) - names - -let load_inductive i ((sp,kn),mie) = +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 -let open_inductive i ((sp,kn),mie) = +let open_inductive i ((sp,kn),(_,_,mie)) = let names = inductive_names sp kn mie in -(* List.iter (fun (sp, ref) -> Nametab.push 0 (restrict_path 0 sp) ref) names*) List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names +let cache_inductive ((sp,kn),(dhyps,imps,mie)) = + let names = inductive_names sp kn mie in + List.iter check_exists_inductive names; + 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; + Dischargedhypsmap.set_discharged_hyps sp dhyps; + with_implicits imps declare_mib_implicits kn; + declare_inductive_argument_scopes kn mie; + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names + +let discharge_inductive ((sp,kn),(dhyps,imps,mie)) = + let mie = Global.lookup_mind kn in + let repl = replacement_context () in + let sechyps = section_segment (IndRef (kn,0)) in + Some (discharged_hyps kn sechyps,imps, + Discharge.process_inductive sechyps repl mie) + let dummy_one_inductive_entry mie = { - mind_entry_params = []; mind_entry_typename = mie.mind_entry_typename; mind_entry_arity = mkProp; mind_entry_consnames = mie.mind_entry_consnames; @@ -270,10 +298,11 @@ let dummy_one_inductive_entry mie = { } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_inductive_entry m = { +let dummy_inductive_entry (_,imps,m) = ([],imps,{ + mind_entry_params = []; mind_entry_record = false; mind_entry_finite = true; - mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds } + mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }) let export_inductive x = Some (dummy_inductive_entry x) @@ -284,38 +313,19 @@ let (in_inductive, out_inductive) = open_function = open_inductive; classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a)); subst_function = ident_subst_function; + discharge_function = discharge_inductive; export_function = export_inductive } -let declare_inductive_argument_scopes kn mie = - list_iter_i (fun i {mind_entry_consnames=lc} -> - Symbols.declare_ref_arguments_scope (IndRef (kn,i)); - for j=1 to List.length lc do - Symbols.declare_ref_arguments_scope (ConstructRef ((kn,i),j)); - done) mie.mind_entry_inds - -let declare_inductive_common mie = - let id = match mie.mind_entry_inds with - | ind::_ -> ind.mind_entry_typename - | [] -> anomaly "cannot declare an empty list of inductives" - in - let oname = add_leaf id (in_inductive mie) in - declare_mib_implicits (snd oname); - declare_inductive_argument_scopes (snd oname) mie; - oname - (* for initial declaration *) let declare_mind isrecord mie = - let (sp,kn as oname) = declare_inductive_common mie in - Dischargedhypsmap.set_discharged_hyps sp [] ; + let imps = implicits_flags () in + let id = match mie.mind_entry_inds with + | ind::_ -> ind.mind_entry_typename + | [] -> anomaly "cannot declare an empty list of inductives" in + let oname = add_leaf id (in_inductive ([],imps,mie)) in !xml_declare_inductive (isrecord,oname); oname -(* when coming from discharge: no xml output *) -let redeclare_inductive discharged_hyps mie = - let oname = declare_inductive_common mie in - Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps ; - oname - (*s Test and access functions. *) let is_constant sp = @@ -330,12 +340,6 @@ let get_variable id = | CheckedSectionLocalDef (c,ty,cst,opaq) -> (id,Some c,ty) | CheckedSectionLocalAssum (ty,cst) -> (id,None,ty) -let get_variable_with_constraints id = - let (p,x,_) = Idmap.find id !vartab in - match x with - | CheckedSectionLocalDef (c,ty,cst,opaq) -> ((id,Some c,ty),cst) - | CheckedSectionLocalAssum (ty,cst) -> ((id,None,ty),cst) - let variable_strength _ = Local let find_section_variable id = @@ -351,8 +355,10 @@ let variable_kind id = pi3 (Idmap.find id !vartab) let clear_proofs sign = - List.map - (fun (id,c,t as d) -> if variable_opacity id then (id,None,t) else d) 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. *) @@ -378,12 +384,6 @@ let mind_oper_of_id sp id mib = mip.mind_consnames) mib.mind_packets -let context_of_global_reference = function - | VarRef id -> [] - | ConstRef sp -> (Global.lookup_constant sp).const_hyps - | IndRef (sp,_) -> (Global.lookup_mind sp).mind_hyps - | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps - let last_section_hyps dir = fold_named_context (fun (id,_,_) sec_ids -> |