diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 181 |
1 files changed, 91 insertions, 90 deletions
diff --git a/library/declare.ml b/library/declare.ml index b338277d3..b67dbc6e2 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -28,6 +28,7 @@ open Impargs open Nametab open Library open Safe_typing +open Decl_kinds (**********************************************) @@ -39,38 +40,23 @@ open Safe_typing open Nametab -let depth_of_strength = function - | DischargeAt (sp',n) -> n - | NeverDischarge -> 0 - | NotDeclare -> assert false - -let make_strength_0 () = - let depth = Lib.sections_depth () in - let cwd = Lib.cwd() in - if depth > 0 then DischargeAt (cwd, depth) else NeverDischarge - -let make_strength_1 () = - let depth = Lib.sections_depth () in - let cwd = Lib.cwd() in - if depth > 1 then DischargeAt (extract_dirpath_prefix 1 cwd, depth-1) - else NeverDischarge - -let make_strength_2 () = - let depth = Lib.sections_depth () in - let cwd = Lib.cwd() in - if depth > 2 then DischargeAt (extract_dirpath_prefix 2 cwd, depth-2) - else NeverDischarge - -let is_less_persistent_strength = function - | (NeverDischarge,_) -> false - | (NotDeclare,_) -> false - | (_,NeverDischarge) -> true - | (_,NotDeclare) -> true - | (DischargeAt (sp1,_),DischargeAt (sp2,_)) -> - is_dirpath_prefix_of sp1 sp2 - let strength_min (stre1,stre2) = - if is_less_persistent_strength (stre1,stre2) then stre1 else 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 -> ()) +let xml_declare_constant = ref (fun sp -> ()) +let xml_declare_inductive = ref (fun sp -> ()) + +let if_xml f x = if !Options.xml_export then f x else () + +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. *) @@ -78,14 +64,13 @@ type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) | SectionLocalAssum of types -type variable_declaration = dir_path * section_variable_entry * strength +type variable_declaration = dir_path * section_variable_entry * local_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 * strength +type checked_variable_declaration = dir_path * checked_section_variable let vartab = ref (Idmap.empty : checked_variable_declaration Idmap.t) @@ -95,7 +80,7 @@ let _ = Summary.declare_summary "VARIABLE" Summary.init_function = (fun () -> vartab := Idmap.empty); Summary.survive_section = false } -let cache_variable ((sp,_),(id,(p,d,strength))) = +let cache_variable ((sp,_),(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"); @@ -109,23 +94,35 @@ let cache_variable ((sp,_),(id,(p,d,strength))) = 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); - vartab := Idmap.add id (p,vd,strength) !vartab + vartab := Idmap.add id (p,vd) !vartab let (in_variable, out_variable) = declare_object { (default_object "VARIABLE") with cache_function = cache_variable; classify_function = (fun _ -> Dispose) } -let declare_variable id obj = - let sp = add_leaf id (in_variable (id,obj)) in +let declare_variable_common id obj = + let oname = add_leaf id (in_variable (id,obj)) in if is_implicit_args() then declare_var_implicits id; - sp + oname + +(* for initial declaration *) +let declare_variable id obj = + let (_,kn as oname) = declare_variable_common id obj in + !xml_declare_variable kn; + Dischargedhypsmap.set_discharged_hyps (fst oname) []; + 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 * strength +type constant_declaration = constant_entry * global_kind -let csttab = ref (Spmap.empty : strength Spmap.t) +let csttab = ref (Spmap.empty : global_kind Spmap.t) let _ = Summary.declare_summary "CONSTANT" { Summary.freeze_function = (fun () -> !csttab); @@ -133,7 +130,7 @@ let _ = Summary.declare_summary "CONSTANT" Summary.init_function = (fun () -> csttab := Spmap.empty); Summary.survive_section = false } -let cache_constant ((sp,kn),(cdt,stre)) = +let cache_constant ((sp,kn),(cdt,kind)) = (if Idmap.mem (basename sp) !vartab then errorlabstrm "cache_constant" (pr_id (basename sp) ++ str " already exists")); @@ -144,35 +141,26 @@ let cache_constant ((sp,kn),(cdt,stre)) = let kn' = Global.add_constant dir (basename sp) cdt in if kn' <> kn then anomaly "Kernel and Library names do not match"; - (match stre with - | DischargeAt (dp,n) when not (is_dirpath_prefix_of dp (Lib.cwd ())) -> - (* Only qualifications including the sections segment from the current - section to the discharge section is available for Remark & Fact *) - Nametab.push (Nametab.Until ((*n-Lib.sections_depth()+*)1)) sp (ConstRef kn) - | (NeverDischarge| DischargeAt _) -> - (* All qualifications of Theorem, Lemma & Definition are visible *) - Nametab.push (Nametab.Until 1) sp (ConstRef kn) - | NotDeclare -> assert false); - csttab := Spmap.add sp stre !csttab + 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),(ce,stre)) = +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 stre !csttab; - Nametab.push (Nametab.Until ((*depth_of_strength stre + *)i)) sp (ConstRef kn) + csttab := Spmap.add sp kind !csttab; + Nametab.push (Nametab.Until i) sp (ConstRef kn) (* Opening means making the name without its module qualification available *) -let open_constant i ((sp,kn),(_,stre)) = - let n = depth_of_strength stre in - Nametab.push (Nametab.Exactly (i(*+n*))) sp (ConstRef kn) +let open_constant i ((sp,kn),_) = + Nametab.push (Nametab.Exactly i) sp (ConstRef kn) (* 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,stre) = dummy_constant_entry,stre +let dummy_constant (ce,mk) = dummy_constant_entry,mk let export_constant cst = Some (dummy_constant cst) @@ -195,15 +183,19 @@ let hcons_constant_declaration = function const_entry_opaque = ce.const_entry_opaque }, stre) | cd -> cd -let declare_constant id (cd,stre) = +let declare_constant id (cd,kind) = (* let cd = hcons_constant_declaration cd in *) - let oname = add_leaf id (in_constant (ConstantEntry cd,stre)) in - if is_implicit_args() then declare_constant_implicits (snd oname); + let (_,kn as oname) = add_leaf id (in_constant (ConstantEntry cd,kind)) in + if is_implicit_args() then declare_constant_implicits kn; + Dischargedhypsmap.set_discharged_hyps (fst oname) [] ; + !xml_declare_constant kn; oname -let redeclare_constant id (cd,stre) = - let _,kn = add_leaf id (in_constant (GlobalRecipe cd,stre)) in - if is_implicit_args() then declare_constant_implicits kn +(* when coming from discharge *) +let redeclare_constant id discharged_hyps (cd,kind) = + let _,kn as oname = add_leaf id (in_constant (GlobalRecipe cd,kind)) in + if is_implicit_args() then declare_constant_implicits kn; + Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps (* Inductives. *) @@ -282,7 +274,7 @@ let (in_inductive, out_inductive) = subst_function = ident_subst_function; export_function = export_inductive } -let declare_mind mie = +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" @@ -291,35 +283,46 @@ let declare_mind mie = if is_implicit_args() then declare_mib_implicits (snd oname); oname +(* for initial declaration *) +let declare_mind mie = + let (_,kn as oname) = declare_inductive_common mie in + Dischargedhypsmap.set_discharged_hyps (fst oname) [] ; + !xml_declare_inductive kn; + 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 = try let _ = Spmap.find sp !csttab in true with Not_found -> false -let constant_strength sp = Spmap.find sp !csttab +let constant_strength sp = Global +let constant_kind sp = Spmap.find sp !csttab let get_variable id = - let (p,x,str) = Idmap.find id !vartab in - let d = match x with + 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) in - (d,str) + | CheckedSectionLocalAssum (ty,cst) -> (id,None,ty) let get_variable_with_constraints id = - let (p,x,str) = Idmap.find id !vartab in + let (p,x) = Idmap.find id !vartab in match x with - | CheckedSectionLocalDef (c,ty,cst,opaq) -> ((id,Some c,ty),cst,str) - | CheckedSectionLocalAssum (ty,cst) -> ((id,None,ty),cst,str) + | CheckedSectionLocalDef (c,ty,cst,opaq) -> ((id,Some c,ty),cst) + | CheckedSectionLocalAssum (ty,cst) -> ((id,None,ty),cst) -let variable_strength id = - let (_,_,str) = Idmap.find id !vartab in str +let variable_strength _ = Local let find_section_variable id = - let (p,_,_) = Idmap.find id !vartab in Libnames.make_path p id + let (p,_) = Idmap.find id !vartab in Libnames.make_path p id let variable_opacity id = - let (_,x,_) = Idmap.find id !vartab in + let (_,x) = Idmap.find id !vartab in match x with | CheckedSectionLocalDef (c,ty,cst,opaq) -> opaq | CheckedSectionLocalAssum (ty,cst) -> false (* any.. *) @@ -369,7 +372,7 @@ let last_section_hyps dir = fold_named_context (fun (id,_,_) sec_ids -> try - let (p,_,_) = Idmap.find id !vartab in + 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())) @@ -436,23 +439,21 @@ let is_global id = with Not_found -> false -let strength_of_global ref = match ref with - | ConstRef kn -> constant_strength (sp_of_global None ref) - | VarRef id -> variable_strength id - | IndRef _ | ConstructRef _ -> NeverDischarge +let strength_of_global = function + | VarRef _ -> Local + | IndRef _ | ConstructRef _ | ConstRef _ -> Global let library_part ref = let sp = Nametab.sp_of_global None ref in let dir,_ = repr_path sp in match strength_of_global ref with - | DischargeAt (dp,n) -> - extract_dirpath_prefix n dp - | NeverDischarge -> + | Local -> + anomaly "TODO"; + extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) + | Global -> if is_dirpath_prefix_of dir (Lib.cwd ()) then - (* Theorem/Lemma not yet (fully) discharged *) - extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) + (* Not yet (fully) discharged *) + extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) else (* Theorem/Lemma outside its outer section of definition *) dir - | NotDeclare -> assert false - |