From 7b2a24d0beee17b61281a5c64fca5cf7388479d3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 18 Feb 2005 22:17:50 +0000 Subject: Moving centralised discharge into dispatched discharge_function; required to delay some computation from before to after caching time + various simplifications and uniformisations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile | 7 +- interp/notation.ml | 71 +++++---- kernel/cooking.ml | 223 +++++++++++---------------- kernel/cooking.mli | 16 +- library/declare.ml | 222 ++++++++++++++------------- library/declare.mli | 18 --- library/dischargedhypsmap.ml | 7 +- library/impargs.ml | 40 +++-- library/impargs.mli | 2 + library/lib.ml | 134 +++++++++++++++-- library/lib.mli | 24 ++- library/libobject.ml | 12 ++ library/libobject.mli | 2 + library/library.ml | 3 + library/library.mli | 6 - pretyping/classops.ml | 149 +++++++++--------- pretyping/classops.mli | 19 +-- pretyping/recordops.ml | 190 +++++++++++++++-------- pretyping/recordops.mli | 36 ++--- toplevel/class.ml | 172 +++------------------ toplevel/class.mli | 17 +-- toplevel/discharge.ml | 349 ++++++------------------------------------- toplevel/discharge.mli | 13 +- toplevel/recordobj.ml | 65 -------- toplevel/recordobj.mli | 2 - 25 files changed, 738 insertions(+), 1061 deletions(-) diff --git a/Makefile b/Makefile index dc366cd91..e9c7e0bdb 100644 --- a/Makefile +++ b/Makefile @@ -161,7 +161,7 @@ INTERP=\ interp/genarg.cmo interp/syntax_def.cmo interp/reserve.cmo \ library/impargs.cmo interp/constrintern.cmo \ interp/modintern.cmo interp/constrextern.cmo interp/coqlib.cmo \ - library/declare.cmo + toplevel/discharge.cmo library/declare.cmo PROOFS=\ proofs/tacexpr.cmo proofs/proof_type.cmo proofs/redexpr.cmo \ @@ -206,9 +206,8 @@ TACTICS=\ TOPLEVEL=\ toplevel/himsg.cmo toplevel/cerrors.cmo toplevel/class.cmo \ toplevel/vernacexpr.cmo toplevel/metasyntax.cmo \ - toplevel/command.cmo \ - toplevel/record.cmo toplevel/recordobj.cmo \ - toplevel/discharge.cmo translate/ppvernacnew.cmo \ + toplevel/command.cmo toplevel/record.cmo \ + translate/ppvernacnew.cmo \ toplevel/vernacinterp.cmo toplevel/mltop.cmo \ toplevel/vernacentries.cmo toplevel/vernac.cmo \ toplevel/line_oriented_parser.cmo toplevel/protectedtoplevel.cmo \ diff --git a/interp/notation.ml b/interp/notation.ml index f90219b24..c3903cfc1 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -13,6 +13,7 @@ open Util open Pp open Bigint open Names +open Term open Nametab open Libnames open Summary @@ -93,9 +94,14 @@ let current_scopes () = !scope_stack (* TODO: push nat_scope, z_scope, ... in scopes summary *) (* Exportation of scopes *) -let cache_scope (_,(local,op,sc)) = +let open_scope i (_,(local,op,sc)) = + if i=1 then begin (match sc with Scope sc -> check_scope sc | _ -> ()); scope_stack := if op then sc :: !scope_stack else list_except sc !scope_stack + end + +let cache_scope o = + open_scope 1 o let subst_scope (_,subst,sc) = sc @@ -109,7 +115,7 @@ let export_scope (local,_,_ as x) = if local then None else Some x let (inScope,outScope) = declare_object {(default_object "SCOPE") with cache_function = cache_scope; - open_function = (fun i o -> if i=1 then cache_scope o); + open_function = open_scope; subst_function = subst_scope; classify_function = classify_scope; export_function = export_scope } @@ -361,31 +367,6 @@ let exists_notation_in_scope scopt ntn r = r' = r, pp8only with Not_found -> false, false -(* Special scopes associated to arguments of a global reference *) - -let arguments_scope = ref Refmap.empty - -let cache_arguments_scope (_,(r,scl)) = - List.iter (option_iter check_scope) scl; - arguments_scope := Refmap.add r scl !arguments_scope - -let subst_arguments_scope (_,subst,(r,scl)) = (fst (subst_global subst r),scl) - -let (inArgumentsScope,outArgumentsScope) = - declare_object {(default_object "ARGUMENTS-SCOPE") with - cache_function = cache_arguments_scope; - load_function = (fun _ o -> cache_arguments_scope o); - subst_function = subst_arguments_scope; - classify_function = (fun (_,o) -> Substitute o); - export_function = (fun x -> Some x) } - -let declare_arguments_scope r scl = - Lib.add_anonymous_leaf (inArgumentsScope (r,scl)) - -let find_arguments_scope r = - try Refmap.find r !arguments_scope - with Not_found -> [] - (**********************************************************************) (* Mapping classes to scopes *) @@ -401,8 +382,6 @@ let declare_class_scope sc cl = let find_class_scope cl = Gmap.find cl !class_scope_map -open Term - let find_class t = let t, _ = decompose_app (Reductionops.whd_betaiotazeta t) in match kind_of_term t with @@ -413,6 +392,9 @@ let find_class t = | Sort _ -> CL_SORT | _ -> raise Not_found +(**********************************************************************) +(* Special scopes associated to arguments of a global reference *) + let rec compute_arguments_scope t = match kind_of_term (Reductionops.whd_betaiotazeta t) with | Prod (_,t,u) -> @@ -421,6 +403,37 @@ let rec compute_arguments_scope t = sc :: compute_arguments_scope u | _ -> [] +let arguments_scope = ref Refmap.empty + +let load_arguments_scope _ (_,(r,scl)) = + List.iter (option_iter check_scope) scl; + arguments_scope := Refmap.add r scl !arguments_scope + +let cache_arguments_scope o = + load_arguments_scope 1 o + +let subst_arguments_scope (_,subst,(r,scl)) = (fst (subst_global subst r),scl) + +let discharge_arguments_scope (r,_) = + match r with + | VarRef _ -> None + | _ -> Some (r,compute_arguments_scope (Global.type_of_global r)) + +let (inArgumentsScope,outArgumentsScope) = + declare_object {(default_object "ARGUMENTS-SCOPE") with + cache_function = cache_arguments_scope; + load_function = load_arguments_scope; + subst_function = subst_arguments_scope; + classify_function = (fun (_,o) -> Substitute o); + export_function = (fun x -> Some x) } + +let declare_arguments_scope r scl = + Lib.add_anonymous_leaf (inArgumentsScope (r,scl)) + +let find_arguments_scope r = + try Refmap.find r !arguments_scope + with Not_found -> [] + let declare_ref_arguments_scope ref = let t = Global.type_of_global ref in declare_arguments_scope ref (compute_arguments_scope t) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 9869afcf5..53a9b9644 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -19,155 +19,110 @@ open Reduction (*s Cooking the constants. *) -type 'a modification = - | NOT_OCCUR - | DO_ABSTRACT of 'a * constr array - | DO_REPLACE of constant_body +type work_list = identifier array Cmap.t * identifier array KNmap.t -type work_list = - (constant * constant modification) list - * (inductive * inductive modification) list - * (constructor * constructor modification) list +let dirpath_prefix p = match repr_dirpath p with + | [] -> anomaly "dirpath_prefix: empty dirpath" + | _::l -> make_dirpath l -type recipe = { - d_from : constant_body; - d_abstract : identifier list; - d_modlist : work_list } +let pop_kn kn = + let (mp,dir,l) = Names.repr_kn kn in + Names.make_kn mp (dirpath_prefix dir) l + +let pop_con con = + let (mp,dir,l) = Names.repr_con con in + Names.make_con mp (dirpath_prefix dir) l + +type my_global_reference = + | ConstRef of constant + | IndRef of inductive + | ConstructRef of constructor + +let cache = (Hashtbl.create 13 : (my_global_reference, constr) Hashtbl.t) + +let clear_cooking_sharing () = Hashtbl.clear cache + +let share r (cstl,knl) = + try Hashtbl.find cache r + with Not_found -> + let f,l = + match r with + | IndRef (kn,i) -> + mkInd (pop_kn kn,i), KNmap.find kn knl + | ConstructRef ((kn,i),j) -> + mkConstruct ((pop_kn kn,i),j), KNmap.find kn knl + | ConstRef cst -> + mkConst (pop_con cst), Cmap.find cst cstl in + let c = mkApp (f, Array.map mkVar l) in + Hashtbl.add cache r c; + (* has raised Not_found if not in work_list *) + c -let failure () = - anomalylabstrm "generic__modify_opers" - (str"An oper which was never supposed to appear has just appeared" ++ - spc () ++ str"Either this is in system code, and you need to" ++ spc () ++ - str"report this error," ++ spc () ++ - str"Or you are using a user-written tactic which calls" ++ spc () ++ - str"generic__modify_opers, in which case the user-written code" ++ - spc () ++ str"is broken - this function is an internal system" ++ - spc () ++ str"for internal system use only") - -let modify_opers replfun (constl,indl,cstrl) = +let update_case_info ci modlist = + try + let ind, n = + match kind_of_term (share (IndRef ci.ci_ind) modlist) with + | App (f,l) -> (destInd f, Array.length l) + | Ind ind -> ind, 0 + | _ -> assert false in + { ci with ci_ind = ind; ci_npar = ci.ci_npar + n } + with Not_found -> + ci + +let empty_modlist = (Cmap.empty, KNmap.empty) + +let expmod_constr modlist c = let rec substrec c = - let c' = map_constr substrec c in - match kind_of_term c' with + match kind_of_term c with | Case (ci,p,t,br) -> + map_constr substrec (mkCase (update_case_info ci modlist,p,t,br)) + + | Ind ind -> (try - match List.assoc ci.ci_ind indl with - | DO_ABSTRACT (ind,abs_vars) -> - let n' = Array.length abs_vars + ci.ci_npar in - let ci' = { ci with - ci_ind = ind; - ci_npar = n' } in - mkCase (ci',p,t,br) - | _ -> raise Not_found - with - | Not_found -> c') - - | Ind spi -> - (try - (match List.assoc spi indl with - | NOT_OCCUR -> failure () - | DO_ABSTRACT (oper',abs_vars) -> - mkApp (mkInd oper', abs_vars) - | DO_REPLACE _ -> assert false) + share (IndRef ind) modlist with - | Not_found -> c') - - | Construct spi -> + | Not_found -> map_constr substrec c) + + | Construct cstr -> (try - (match List.assoc spi cstrl with - | NOT_OCCUR -> failure () - | DO_ABSTRACT (oper',abs_vars) -> - mkApp (mkConstruct oper', abs_vars) - | DO_REPLACE _ -> assert false) + share (ConstructRef cstr) modlist with - | Not_found -> c') - - | Const kn -> + | Not_found -> map_constr substrec c) + + | Const cst -> (try - (match List.assoc kn constl with - | NOT_OCCUR -> failure () - | DO_ABSTRACT (oper',abs_vars) -> - mkApp (mkConst oper', abs_vars) - | DO_REPLACE cb -> substrec (replfun (kn,cb))) + share (ConstRef cst) modlist with - | Not_found -> c') - - | _ -> c' - in - if (constl,indl,cstrl) = ([],[],[]) then fun x -> x else substrec + | Not_found -> map_constr substrec c) + + | _ -> map_constr substrec c -let expmod_constr modlist c = - let simpfun = - if modlist = ([],[],[]) then fun x -> x else nf_betaiota in - let expfun (kn,cb) = - if cb.const_opaque then - errorlabstrm "expmod_constr" - (str"Cannot unfold the value of " ++ - str(string_of_con kn) ++ spc () ++ - str"You cannot declare local lemmas as being opaque" ++ spc () ++ - str"and then require that theorems which use them" ++ spc () ++ - str"be transparent"); - match cb.const_body with - | Some body -> Declarations.force body - | None -> assert false - in - let c' = modify_opers expfun modlist c in - match kind_of_term c' with - | Cast (value,typ) -> mkCast (simpfun value,simpfun typ) - | _ -> simpfun c' - -let expmod_type modlist c = - type_app (expmod_constr modlist) c - -let abstract_constant ids_to_abs hyps (body,typ) = - let abstract_once_typ ((hyps,typ) as sofar) id = - match hyps with - | (hyp,c,t as decl)::rest when hyp = id -> - let typ' = mkNamedProd_wo_LetIn decl typ in - (rest, typ') - | _ -> - sofar - in - let abstract_once_body ((hyps,body) as sofar) id = - match hyps with - | (hyp,c,t as decl)::rest when hyp = id -> - let body' = mkNamedLambda_or_LetIn decl body in - (rest, body') - | _ -> - sofar - in - let (_,typ') = - List.fold_left abstract_once_typ (hyps,typ) ids_to_abs - in - let body' = match body with - None -> None - | Some l_body -> - Some (Declarations.from_val - (let body = Declarations.force l_body in - let (_,body') = - List.fold_left abstract_once_body (hyps,body) ids_to_abs - in - body')) in - (body',typ') + if modlist = empty_modlist then c + else under_outer_cast nf_betaiota (substrec c) + +let abstract_constant_type = + List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c) + +let abstract_constant_body = + List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c) + +type recipe = { + d_from : constant_body; + d_abstract : named_context; + d_modlist : work_list } + +let on_body f = + option_app (fun c -> Declarations.from_val (f (Declarations.force c))) let cook_constant env r = let cb = r.d_from in - let typ = expmod_type r.d_modlist cb.const_type in - let body = - option_app - (fun lconstr -> - Declarations.from_val - (expmod_constr r.d_modlist (Declarations.force lconstr))) - cb.const_body - in - let hyps = - Sign.fold_named_context - (fun d ctxt -> - Sign.add_named_decl - (map_named_declaration (expmod_constr r.d_modlist) d) - ctxt) - cb.const_hyps - ~init:empty_named_context in - let body,typ = abstract_constant r.d_abstract hyps (body,typ) in + let hyps = Sign.map_named_context (expmod_constr r.d_modlist) r.d_abstract in + let body = + on_body (fun c -> + abstract_constant_body (expmod_constr r.d_modlist c) hyps) + cb.const_body in + let typ = + abstract_constant_type (expmod_constr r.d_modlist cb.const_type) hyps in let boxed = Cemitcodes.is_boxed cb.const_body_code in (body, typ, cb.const_constraints, cb.const_opaque, boxed) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 289373eff..2e7a3639a 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -16,19 +16,11 @@ open Univ (*s Cooking the constants. *) -type 'a modification = - | NOT_OCCUR - | DO_ABSTRACT of 'a * constr array - | DO_REPLACE of constant_body - -type work_list = - (constant * constant modification) list - * (inductive * inductive modification) list - * (constructor * constructor modification) list +type work_list = identifier array Cmap.t * identifier array KNmap.t type recipe = { d_from : constant_body; - d_abstract : identifier list; + d_abstract : Sign.named_context; d_modlist : work_list } val cook_constant : @@ -38,6 +30,8 @@ val cook_constant : (*s Utility functions used in module [Discharge]. *) val expmod_constr : work_list -> constr -> constr -val expmod_type : work_list -> types -> types + +val clear_cooking_sharing : unit -> unit + diff --git a/library/declare.ml b/library/declare.ml index 2109c6325..6bace2654 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -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 @@ -75,13 +71,16 @@ type checked_variable_declaration = 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,31 +94,33 @@ 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; - Notation.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 @@ -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' <> (constant_of_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 (constant_of_kn 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 (constant_of_kn kn)) +let cache_constant ((sp,kn),(cdt,dhyps,imps,kind) as o) = + 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,6 +196,7 @@ 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 @@ -188,12 +209,10 @@ let hcons_constant_declaration = function 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 +let declare_constant_common id dhyps (cd,kind) = + let imps = implicits_flags () in + let (sp,kn as oname) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in let kn = constant_of_kn kn in - declare_constant_implicits kn; - Notation.declare_ref_arguments_scope (ConstRef kn); - Dischargedhypsmap.set_discharged_hyps sp discharged_hyps; kn let declare_constant_gen internal id (cd,kind) = @@ -205,13 +224,15 @@ let declare_constant_gen internal id (cd,kind) = 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, _ = @@ -232,37 +253,43 @@ 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") - -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 + errorlabstrm "" (pr_id id ++ str " already exists") -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; @@ -272,10 +299,10 @@ 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_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) @@ -286,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} -> - 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 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 = @@ -332,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 = @@ -380,12 +382,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 -> diff --git a/library/declare.mli b/library/declare.mli index 6af513888..c141985be 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -40,10 +40,6 @@ type variable_declaration = dir_path * section_variable_entry * local_kind val declare_variable : variable -> variable_declaration -> object_name -(* Declaration from Discharge *) -val redeclare_variable : - variable -> Dischargedhypsmap.discharged_hyps -> variable_declaration -> unit - (* Declaration of global constructions *) (* i.e. Definition/Theorem/Axiom/Parameter/... *) @@ -58,21 +54,11 @@ val declare_constant : val declare_internal_constant : identifier -> constant_declaration -> constant -val redeclare_constant : - identifier -> Dischargedhypsmap.discharged_hyps -> - Cooking.recipe * global_kind -> unit - (* [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of the whole block (boolean must be true iff it is a record) *) val declare_mind : bool -> mutual_inductive_entry -> object_name -(* Declaration from Discharge *) -val redeclare_inductive : - Dischargedhypsmap.discharged_hyps -> mutual_inductive_entry -> object_name - -val out_inductive : Libobject.obj -> mutual_inductive_entry - val strength_min : strength * strength -> strength val string_of_strength : strength -> string @@ -82,10 +68,7 @@ val is_constant : section_path -> bool val constant_strength : section_path -> strength val constant_kind : section_path -> global_kind -val out_variable : Libobject.obj -> identifier * variable_declaration val get_variable : variable -> named_declaration -val get_variable_with_constraints : - variable -> named_declaration * Univ.constraints val variable_strength : variable -> strength val variable_kind : variable -> local_kind val find_section_variable : variable -> section_path @@ -94,7 +77,6 @@ val clear_proofs : named_context -> named_context (*s Global references *) -val context_of_global_reference : global_reference -> section_context val strength_of_global : global_reference -> strength (* hooks for XML output *) diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index 96ed944b2..0e7bdef30 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -24,13 +24,16 @@ type discharged_hyps = section_path list let discharged_hyps_map = ref Spmap.empty -let cache_discharged_hyps_map (_,(sp,hyps)) = +let load_discharged_hyps_map _ (_,(sp,hyps)) = discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map +let cache_discharged_hyps_map o = + load_discharged_hyps_map 1 o + let (in_discharged_hyps_map, _) = declare_object { (default_object "DISCHARGED-HYPS-MAP") with cache_function = cache_discharged_hyps_map; - load_function = (fun _ -> cache_discharged_hyps_map); + load_function = load_discharged_hyps_map; export_function = (fun x -> Some x) } let set_discharged_hyps sp hyps = diff --git a/library/impargs.ml b/library/impargs.ml index 8daf939ef..f41d26c99 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -55,6 +55,14 @@ let is_contextual_implicit_args () = !contextual_implicit_args type implicits_flags = (bool * bool * bool) * (bool * bool * bool) +let implicits_flags () = + (!implicit_args, + !strict_implicit_args, + !contextual_implicit_args), + (!implicit_args_out, + !strict_implicit_args_out, + !contextual_implicit_args_out) + let with_implicits ((a,b,c),(d,e,g)) f x = let oa = !implicit_args in let ob = !strict_implicit_args in @@ -342,6 +350,16 @@ let compute_var_implicits id = let var_implicits id = try Idmap.find id !var_table with Not_found -> No_impl,No_impl +(* Implicits of a global reference. *) + +let compute_global_implicits = function + | VarRef id -> compute_var_implicits id + | ConstRef kn -> compute_constant_implicits kn + | IndRef (kn,i) -> + let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps + | ConstructRef ((kn,i),j) -> + let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1) + (* Caching implicits *) let cache_implicits_decl (r,imps) = @@ -355,7 +373,15 @@ let cache_implicits_decl (r,imps) = | ConstructRef consp -> constructors_table := Constrmap.add consp imps !constructors_table -let cache_implicits (_,l) = List.iter cache_implicits_decl l +let load_implicits _ (_,l) = List.iter cache_implicits_decl l + +let cache_implicits o = + load_implicits 1 o + +(* +let discharge_implicits (_,(r,imps)) = + match r with VarRef _ -> None | _ -> Some (r,compute_global_implicits r) +*) let subst_implicits_decl subst (r,imps as o) = let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) @@ -366,21 +392,11 @@ let subst_implicits (_,subst,l) = let (in_implicits, _) = declare_object {(default_object "IMPLICITS") with cache_function = cache_implicits; - load_function = (fun _ -> cache_implicits); + load_function = load_implicits; subst_function = subst_implicits; classify_function = (fun (_,x) -> Substitute x); export_function = (fun x -> Some x) } -(* Implicits of a global reference. *) - -let compute_global_implicits = function - | VarRef id -> compute_var_implicits id - | ConstRef kn -> compute_constant_implicits kn - | IndRef (kn,i) -> - let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps - | ConstructRef ((kn,i),j) -> - let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1) - let declare_implicits_gen r = add_anonymous_leaf (in_implicits [r,compute_global_implicits r]) diff --git a/library/impargs.mli b/library/impargs.mli index c1eba6923..212a93a0f 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -64,6 +64,8 @@ val is_implicit_var : variable -> implicits_flags val implicits_of_global : global_reference -> implicits_list +val implicits_flags : unit -> implicits_flags + (* For translator *) val implicits_of_global_out : global_reference -> implicits_list val is_implicit_args_out : unit -> bool diff --git a/library/lib.ml b/library/lib.ml index babb3863b..548b80d42 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -215,6 +215,7 @@ let is_something_opened = function | (_,OpenedModtype _) -> true | _ -> false +(* let export_segment seg = let rec clean acc = function | (_,CompilingLibrary _) :: _ | [] -> acc @@ -229,7 +230,7 @@ let export_segment seg = | (_,FrozenState _) :: stk -> clean acc stk in clean [] seg - +*) let start_module export id mp nametab = let dir = extend_dirpath (fst !path_prefix) id in @@ -383,6 +384,70 @@ let is_module () = (* Returns the most recent OpenedThing node *) let what_is_opened () = find_entry_p is_something_opened +(* Discharge tables *) + +let sectab = + ref ([] : (identifier list * + (identifier array Cmap.t * identifier array KNmap.t) * + (Sign.named_context Cmap.t * Sign.named_context KNmap.t)) list) + +let add_section () = + sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab + +let add_section_variable id = + match !sectab with + | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) + | (vars,repl,abs)::sl -> sectab := (id::vars,repl,abs)::sl + +let rec extract_hyps = function + | (id::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps) + | (id::idl,hyps) -> extract_hyps (idl,hyps) + | [], _ -> [] + +let add_section_replacement f g hyps = + match !sectab with + | [] -> () + | (vars,exps,abs)::sl -> + let sechyps = extract_hyps (vars,hyps) in + let args = Sign.instance_from_named_context (List.rev sechyps) in + sectab := (vars,f (Array.map Term.destVar args) exps,g sechyps abs)::sl + +let add_section_kn kn = + let f = (fun x (l1,l2) -> (l1,KNmap.add kn x l2)) in + add_section_replacement f f + +let add_section_constant kn = + let f = (fun x (l1,l2) -> (Cmap.add kn x l1,l2)) in + add_section_replacement f f + +let replacement_context () = pi2 (List.hd !sectab) + +let section_segment = function + | VarRef id -> + [] + | ConstRef con -> + Cmap.find con (fst (pi3 (List.hd !sectab))) + | IndRef (kn,_) | ConstructRef ((kn,_),_) -> + KNmap.find kn (snd (pi3 (List.hd !sectab))) + +let section_instance r = + Sign.instance_from_named_context (List.rev (section_segment r)) + +let init () = sectab := [] +let freeze () = !sectab +let unfreeze s = sectab := s + +let _ = + Summary.declare_summary "section-context" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = false } + +(*************) +(* Sections. *) + (* XML output hooks *) let xml_open_section = ref (fun id -> ()) let xml_close_section = ref (fun id -> ()) @@ -390,8 +455,6 @@ let xml_close_section = ref (fun id -> ()) let set_xml_open_section f = xml_open_section := f let set_xml_close_section f = xml_close_section := f -(* Sections. *) - let open_section id = let olddir,(mp,oldsec) = !path_prefix in let dir = extend_dirpath olddir id in @@ -405,11 +468,19 @@ let open_section id = Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); path_prefix := prefix; if !Options.xml_export then !xml_open_section id; + add_section (); prefix (* Restore lib_stk and summaries as before the section opening, and add a ClosedSection object. *) + +let discharge_item = function + | ((sp,_ as oname),Leaf lobj) -> + option_app (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) + | _ -> + None + let close_section ~export id = let oname,fs = try match find_entry_p is_something_opened with @@ -421,25 +492,31 @@ let close_section ~export id = with Not_found -> error "no opened section" in - let (after,_,before) = split_lib oname in + let (secdecls,_,before) = split_lib oname in lib_stk := before; - let prefix = !path_prefix in + let full_olddir = fst !path_prefix in pop_path_prefix (); +(* let closed_sec = - ClosedSection (export, (fst prefix), export_segment after) - in + ClosedSection (export, full_olddir, export_segment secdecls) in let name = make_path id, make_kn id in add_entry name closed_sec; +*) if !Options.xml_export then !xml_close_section id; - (prefix, after, fs) + let newdecls = List.map discharge_item secdecls in + Summary.section_unfreeze_summaries fs; + List.iter (option_iter (fun (id,o) -> ignore (add_leaf id o))) newdecls; + Cooking.clear_cooking_sharing (); + Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) +(*****************) (* Backtracking. *) let recache_decl = function | (sp, Leaf o) -> cache_object (sp,o) + | (_,OpenedSection _) -> add_section () | _ -> () - let recache_context ctx = List.iter recache_decl ctx @@ -475,7 +552,7 @@ let is_mod_node = function the same name *) let reset_mod (loc,id) = - let (ent,before) = + let (_,before) = try find_split_p (fun (sp,node) -> let (_,spi) = repr_path (fst sp) in id = spi @@ -583,3 +660,40 @@ let library_part ref = else (* Theorem/Lemma outside its outer section of definition *) dir + +(************************) +(* Discharging names *) + +let pop_kn kn = + let (mp,dir,l) = Names.repr_kn kn in + Names.make_kn mp (dirpath_prefix dir) l + +let pop_con con = + let (mp,dir,l) = Names.repr_con con in + Names.make_con mp (dirpath_prefix dir) l + +let con_defined_in_sec kn = + let _,dir,_ = repr_con kn in + dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ()) + +let defined_in_sec kn = + let _,dir,_ = repr_kn kn in + dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ()) + +let discharge_global = function + | ConstRef kn when con_defined_in_sec kn -> + ConstRef (pop_con kn) + | IndRef (kn,i) when defined_in_sec kn -> + IndRef (pop_kn kn,i) + | ConstructRef ((kn,i),j) when defined_in_sec kn -> + ConstructRef ((pop_kn kn,i),j) + | r -> r + +let discharge_kn kn = + if defined_in_sec kn then pop_kn kn else kn + +let discharge_con cst = + if con_defined_in_sec cst then pop_con cst else cst + +let discharge_inductive (kn,i) = + (discharge_kn kn,i) diff --git a/library/lib.mli b/library/lib.mli index 0433897ba..9a4a810ae 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -128,8 +128,7 @@ val library_part : global_reference -> dir_path val open_section : identifier -> object_prefix -val close_section : export:bool -> identifier -> - object_prefix * library_segment * Summary.frozen +val close_section : export:bool -> identifier -> unit (*s Backtracking (undo). *) @@ -157,3 +156,24 @@ val reset_initial : unit -> unit (* XML output hooks *) val set_xml_open_section : (identifier -> unit) -> unit val set_xml_close_section : (identifier -> unit) -> unit + + +(*s Section management for discharge *) + +val section_segment : global_reference -> Sign.named_context +val section_instance : global_reference -> Term.constr array + +val add_section_variable : identifier -> unit +val add_section_constant : constant -> Sign.named_context -> unit +val add_section_kn : kernel_name -> Sign.named_context -> unit +val replacement_context : unit -> + (identifier array Cmap.t * identifier array KNmap.t) + +(*s Discharge: decrease the section level if in the current section *) + +val discharge_kn : kernel_name -> kernel_name +val discharge_con : constant -> constant +val discharge_global : global_reference -> global_reference +val discharge_inductive : inductive -> inductive + + diff --git a/library/libobject.ml b/library/libobject.ml index 25d5a329f..d84e0bc26 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -36,6 +36,7 @@ type 'a object_declaration = { open_function : int -> object_name * 'a -> unit; classify_function : object_name * 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; + discharge_function : object_name * 'a -> 'a option; export_function : 'a -> 'a option } let yell s = anomaly s @@ -48,6 +49,7 @@ let default_object s = { subst_function = (fun _ -> yell ("The object "^s^" does not know how to substitute!")); classify_function = (fun (_,obj) -> Keep obj); + discharge_function = (fun _ -> None); export_function = (fun _ -> None)} @@ -72,6 +74,7 @@ type dynamic_object_declaration = { dyn_open_function : int -> object_name * obj -> unit; dyn_subst_function : object_name * substitution * obj -> obj; dyn_classify_function : object_name * obj -> obj substitutivity; + dyn_discharge_function : object_name * obj -> obj option; dyn_export_function : obj -> obj option } let object_tag lobj = Dyn.tag lobj @@ -104,6 +107,11 @@ let declare_object odecl = | Anticipate (obj) -> Anticipate (infun obj) else anomaly "somehow we got the wrong dynamic object in the classifyfun" + and discharge (oname,lobj) = + if Dyn.tag lobj = na then + option_app infun (odecl.discharge_function (oname,outfun lobj)) + else + anomaly "somehow we got the wrong dynamic object in the dischargefun" and exporter lobj = if Dyn.tag lobj = na then option_app infun (odecl.export_function (outfun lobj)) @@ -116,6 +124,7 @@ let declare_object odecl = dyn_open_function = opener; dyn_subst_function = substituter; dyn_classify_function = classifier; + dyn_discharge_function = discharge; dyn_export_function = exporter }; (infun,outfun) @@ -154,5 +163,8 @@ let subst_object ((_,_,lobj) as node) = let classify_object ((_,lobj) as node) = apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj +let discharge_object ((_,lobj) as node) = + apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj + let export_object lobj = apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj diff --git a/library/libobject.mli b/library/libobject.mli index 37447ffbe..3d60e48ad 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -70,6 +70,7 @@ type 'a object_declaration = { open_function : int -> object_name * 'a -> unit; classify_function : object_name * 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; + discharge_function : object_name * 'a -> 'a option; export_function : 'a -> 'a option } (* The default object is a "Keep" object with empty methods. @@ -103,4 +104,5 @@ val open_object : int -> object_name * obj -> unit val subst_object : object_name * substitution * obj -> obj val classify_object : object_name * obj -> obj substitutivity val export_object : obj -> obj option +val discharge_object : object_name * obj -> obj option val relax : bool -> unit diff --git a/library/library.ml b/library/library.ml index fee383233..09169c4ae 100644 --- a/library/library.ml +++ b/library/library.ml @@ -554,11 +554,14 @@ let load_require _ (_,(modl,_)) = OS dependent fields from .vo files for cross-platform compatibility *) let export_require (l,e) = Some (l,e) +let discharge_require (_,o) = Some o + let (in_require, out_require) = declare_object {(default_object "REQUIRE") with cache_function = cache_require; load_function = load_require; export_function = export_require; + discharge_function = discharge_require; classify_function = (fun (_,o) -> Anticipate o) } (* Require libraries, import them if [export <> None], mark them for export diff --git a/library/library.mli b/library/library.mli index 4ecc76809..bfcc04eb9 100644 --- a/library/library.mli +++ b/library/library.mli @@ -76,9 +76,3 @@ val locate_qualified_library : (*s Statistics: display the memory use of a library. *) val mem : dir_path -> Pp.std_ppcmds - -(*s For discharge *) -type library_reference - -val out_require : Libobject.obj -> library_reference -val reload_library : library_reference -> unit diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 66ed81d02..6d49baf52 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -36,14 +36,14 @@ type cl_typ = | CL_IND of inductive type cl_info_typ = { - cl_strength : strength; cl_param : int } type coe_typ = global_reference type coe_info_typ = { - coe_value : unsafe_judgment; + coe_value : constr; + coe_type : types; coe_strength : strength; coe_is_identity : bool; coe_param : int } @@ -92,11 +92,7 @@ let unfreeze (fcl,fco,fig) = (* ajout de nouveaux "objets" *) let add_new_class cl s = - try - let n,s' = Bijint.revmap cl !class_tab in - if s.cl_strength = Global & s'.cl_strength <> Global then - class_tab := Bijint.replace n cl s !class_tab - with Not_found -> + if not (Bijint.mem cl !class_tab) then class_tab := Bijint.add cl s !class_tab let add_new_coercion coe s = @@ -107,11 +103,19 @@ let add_new_path x y = let init () = class_tab:= Bijint.empty; - add_new_class CL_FUN { cl_param = 0; cl_strength = Global }; - add_new_class CL_SORT { cl_param = 0; cl_strength = Global }; + add_new_class CL_FUN { cl_param = 0 }; + add_new_class CL_SORT { cl_param = 0 }; coercion_tab:= Gmap.empty; inheritance_graph:= Gmap.empty +let _ = + Summary.declare_summary "inh_graph" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = false } + let _ = init() (* class_info : cl_typ -> int * cl_info_typ *) @@ -147,7 +151,7 @@ let lookup_pattern_path_between (s,t) = (fun coe -> let c, _ = Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty - coe.coe_value.uj_val + coe.coe_value in match kind_of_term c with | Construct sp -> (sp, coe.coe_param) @@ -183,44 +187,6 @@ let subst_cl_typ subst ct = match ct with to declare any term as a coercion *) let subst_coe_typ subst t = fst (subst_global subst t) -let subst_coe_info subst info = - let jud = info.coe_value in - let val' = subst_mps subst (j_val jud) in - let type' = subst_mps subst (j_type jud) in - if val' == j_val jud && type' == j_type jud then info else - {info with coe_value = make_judge val' type'} - -(* library, summary *) - -(*val inClass : (cl_typ * cl_info_typ) -> Libobject.object = - val outClass : Libobject.object -> (cl_typ * cl_info_typ) = *) - -let cache_class (_,(x,y)) = add_new_class x y - -let subst_class (_,subst,(ct,ci as obj)) = - let ct' = subst_cl_typ subst ct in - if ct' == ct then obj else - (ct',ci) - -let (inClass,outClass) = - declare_object {(default_object "CLASS") with - load_function = (fun _ o -> cache_class o); - cache_function = cache_class; - subst_function = subst_class; - classify_function = (fun (_,x) -> Substitute x); - export_function = (function x -> Some x) } - -let declare_class (cl,stre,p) = - Lib.add_anonymous_leaf (inClass ((cl,{ cl_strength = stre; cl_param = p }))) - -let _ = - Summary.declare_summary "inh_graph" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } - (* classe d'un terme *) (* class_of : Term.constr -> int *) @@ -257,7 +223,8 @@ let pr_class x = str (string_of_class x) (* coercion_value : coe_index -> unsafe_judgment * bool *) -let coercion_value { coe_value = j; coe_is_identity = b } = (j,b) +let coercion_value { coe_value = c; coe_type = t; coe_is_identity = b } = + (make_judge c t, b) (* pretty-print functions are now in Pretty *) (* rajouter une coercion dans le graphe *) @@ -322,49 +289,81 @@ let add_coercion_in_graph (ic,source,target) = if (!ambig_paths <> []) && is_verbose () then ppnl (message_ambig !ambig_paths) -type coercion = coe_typ * coe_info_typ * cl_typ * cl_typ +type coercion = coe_typ * strength * bool * cl_typ * cl_typ * int -let cache_coercion (_,(coe,xf,cls,clt)) = +(* Calcul de l'arité d'une classe *) + +let reference_arity_length ref = + let t = Global.type_of_global ref in + List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty t)) + +let class_params = function + | CL_FUN | CL_SORT -> 0 + | CL_CONST sp -> reference_arity_length (ConstRef sp) + | CL_SECVAR sp -> reference_arity_length (VarRef sp) + | CL_IND sp -> reference_arity_length (IndRef sp) + +(* add_class : cl_typ -> strength option -> bool -> unit *) + +let add_class cl = + add_new_class cl { cl_param = class_params cl } + +let load_coercion i (_,(coe,stre,isid,cls,clt,ps)) = + add_class cls; + add_class clt; let is,_ = class_info cls in let it,_ = class_info clt in + let xf = + { coe_value = constr_of_global coe; + coe_type = Global.type_of_global coe; + coe_strength = stre; + coe_is_identity = isid; + coe_param = ps } in add_new_coercion coe xf; add_coercion_in_graph (xf,is,it) -let subst_coercion (_,subst,(coe,xf,cls,clt as obj)) = +let cache_coercion o = + load_coercion 1 o + +let subst_coercion (_,subst,(coe,stre,isid,cls,clt,ps as obj)) = let coe' = subst_coe_typ subst coe in - let xf' = subst_coe_info subst xf in let cls' = subst_cl_typ subst cls in let clt' = subst_cl_typ subst clt in - if coe' == coe && xf' == xf && cls' == cls & clt' == clt then obj else - (coe',xf',cls',clt') - - -(* val inCoercion : coercion -> Libobject.object - val outCoercion : Libobject.object -> coercion *) + if coe' == coe && cls' == cls & clt' == clt then obj else + (coe',stre,isid,cls',clt',ps) + +let discharge_cl = function + | CL_CONST kn -> CL_CONST (Lib.discharge_con kn) + | CL_IND ind -> CL_IND (Lib.discharge_inductive ind) + | cl -> cl + +let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) = + if stre = Local then None else + let n = try Array.length (Lib.section_instance coe) with Not_found -> 0 in + Some (Lib.discharge_global coe, + stre, + isid, + discharge_cl cls, + discharge_cl clt, + n + ps) let (inCoercion,outCoercion) = declare_object {(default_object "COERCION") with - load_function = (fun _ o -> cache_coercion o); - cache_function = cache_coercion; - subst_function = subst_coercion; - classify_function = (fun (_,x) -> Substitute x); - export_function = (function x -> Some x) } - -let declare_coercion coef v stre ~isid ~src:cls ~target:clt ~params:ps = - Lib.add_anonymous_leaf - (inCoercion - (coef, - { coe_value = v; - coe_strength = stre; - coe_is_identity = isid; - coe_param = ps }, - cls, clt)) + load_function = load_coercion; + cache_function = cache_coercion; + subst_function = subst_coercion; + classify_function = (fun (_,x) -> Substitute x); + discharge_function = discharge_coercion; + export_function = (function x -> Some x) } + +let declare_coercion coef stre ~isid ~src:cls ~target:clt ~params:ps = + Lib.add_anonymous_leaf (inCoercion (coef,stre,isid,cls,clt,ps)) let coercion_strength v = v.coe_strength let coercion_identity v = v.coe_is_identity (* For printing purpose *) -let get_coercion_value v = v.coe_value.uj_val +let get_coercion_value v = v.coe_value let classes () = Bijint.dom !class_tab let coercions () = Gmap.rng !coercion_tab diff --git a/pretyping/classops.mli b/pretyping/classops.mli index c1590f6a8..dd51ee970 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -30,7 +30,6 @@ val subst_cl_typ : substitution -> cl_typ -> cl_typ (* This is the type of infos for declared classes *) type cl_info_typ = { - cl_strength : strength; cl_param : int } (* This is the type of coercion kinds *) @@ -48,9 +47,6 @@ type coe_index (* This is the type of paths from a class to another *) type inheritance_path = coe_index list -(*s [declare_class] adds a class to the set of declared classes *) -val declare_class : cl_typ * strength * int -> unit - (*s Access to classes infos *) val class_info : cl_typ -> (cl_index * cl_info_typ) val class_exists : cl_typ -> bool @@ -70,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 -> unsafe_judgment -> strength -> isid:bool -> + coe_typ -> strength -> isid:bool -> src:cl_typ -> target:cl_typ -> params:int -> unit (*s Access to coercions infos *) @@ -85,19 +81,6 @@ val lookup_path_to_sort_from : cl_index -> inheritance_path val lookup_pattern_path_between : cl_index * cl_index -> (constructor * int) list -(*i Pour le discharge *) -type coercion = coe_typ * coe_info_typ * cl_typ * cl_typ - -open Libobject -val inClass : (cl_typ * cl_info_typ) -> Libobject.obj -val outClass : Libobject.obj -> (cl_typ * cl_info_typ) -val inCoercion : coercion -> Libobject.obj -val outCoercion : Libobject.obj -> coercion -val coercion_strength : coe_info_typ -> strength -val coercion_identity : coe_info_typ -> bool -val coercion_params : coe_info_typ -> int -(*i*) - (*i Crade *) open Pp val install_path_printer : diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index cfccdb5e6..7f557d9b3 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -21,17 +21,19 @@ open Library open Classops open Mod_subst -(*s Une structure S est un type inductif non récursif à un seul - constructeur (de nom par défaut Build_S) *) +(*s A structure S is a non recursive inductive type with a single + constructor (the name of which defaults to Build_S) *) (* Table des structures: le nom de la structure (un [inductive]) donne le nom du constructeur, le nombre de paramètres et pour chaque - argument réels du constructeur, le noms de la projection - correspondante, si valide *) + argument réel du constructeur, le nom de la projection + correspondante, si valide, et un booléen disant si c'est une vraie + projection ou bien une fonction constante (associée à un LetIn) *) type struc_typ = { s_CONST : identifier; s_PARAM : int; + s_PROJKIND : bool list; s_PROJ : constant option list } let structure_table = ref (Indmap.empty : struc_typ Indmap.t) @@ -39,121 +41,177 @@ let projection_table = ref Cmap.empty let option_fold_right f p e = match p with Some a -> f a e | None -> e -let cache_structure (_,(ind,struc)) = +let load_structure i (_,(ind,id,kl,projs)) = + let n = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in + let struc = + { s_CONST = id; s_PARAM = n; s_PROJ = projs; s_PROJKIND = kl } in structure_table := Indmap.add ind struc !structure_table; projection_table := List.fold_right (option_fold_right (fun proj -> Cmap.add proj struc)) - struc.s_PROJ !projection_table + projs !projection_table -let subst_structure (_,subst,((kn,i),struc as obj)) = +let cache_structure o = + load_structure 1 o + +let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) = let kn' = subst_kn subst kn in - let proj' = + let projs' = (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) list_smartmap - (option_smartmap (fun kn -> fst (subst_con subst kn))) - struc.s_PROJ + (option_smartmap (fun kn -> fst (subst_con subst kn))) + projs in - if proj' == struc.s_PROJ && kn' == kn then obj else - (kn',i),{struc with s_PROJ = proj'} + if projs' == projs && kn' == kn then obj else + ((kn',i),id,kl,projs') + +let discharge_structure (_,(ind,id,kl,projs)) = + Some (Lib.discharge_inductive ind, id, kl, + List.map (option_app Lib.discharge_con) projs) let (inStruc,outStruc) = declare_object {(default_object "STRUCTURE") with - cache_function = cache_structure; - load_function = (fun _ o -> cache_structure o); - subst_function = subst_structure; - classify_function = (fun (_,x) -> Substitute x); - export_function = (function x -> Some x) } + cache_function = cache_structure; + load_function = load_structure; + subst_function = subst_structure; + classify_function = (fun (_,x) -> Substitute x); + discharge_function = discharge_structure; + export_function = (function x -> Some x) } -let add_new_struc (s,c,n,l) = - Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l})) +let declare_structure (s,c,_,kl,pl) = + Lib.add_anonymous_leaf (inStruc (s,c,kl,pl)) -let find_structure indsp = Indmap.find indsp !structure_table +let lookup_structure indsp = Indmap.find indsp !structure_table let find_projection_nparams = function | ConstRef cst -> (Cmap.find cst !projection_table).s_PARAM | _ -> raise Not_found -(*s Un "object" est une fonction construisant une instance d'une structure *) + +(************************************************************************) +(*s A canonical structure declares "canonical" conversion hints between *) +(* the effective components of a structure and the projections of the *) +(* structure *) (* Table des definitions "object" : pour chaque object c, c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n) - avec ti = (ci ui1...uir) + If ti has the form (ci ui1...uir) where ci is a global reference and +if the corresponding projection Li of the structure R is defined, one +declare a "conversion" between ci and Li + + x1:B1..xk:Bk |- (Li a1..am (c x1..xk)) =_conv (ci ui1...uir) - Pour tout ci, et Li, la ième projection de la structure R (si - définie), on déclare une "coercion" +that maps the pair (Li,ci) to the following data o_DEF = c o_TABS = B1...Bk o_PARAMS = a1...am o_TCOMP = ui1...uir + *) type obj_typ = { o_DEF : constr; - o_TABS : constr list; (* dans l'ordre *) - o_TPARAMS : constr list; (* dans l'ordre *) - o_TCOMPS : constr list } (* dans l'ordre *) - -let subst_obj subst obj = - let o_DEF' = subst_mps subst obj.o_DEF in - let o_TABS' = list_smartmap (subst_mps subst) obj.o_TABS in - let o_TPARAMS' = list_smartmap (subst_mps subst) obj.o_TPARAMS in - let o_TCOMPS' = list_smartmap (subst_mps subst) obj.o_TCOMPS in - if o_DEF' == obj.o_DEF - && o_TABS' == obj.o_TABS - && o_TPARAMS' == obj.o_TPARAMS - && o_TCOMPS' == obj.o_TCOMPS - then - obj - else - { o_DEF = o_DEF' ; - o_TABS = o_TABS' ; - o_TPARAMS = o_TPARAMS' ; - o_TCOMPS = o_TCOMPS' } + o_TABS : constr list; (* ordered *) + o_TPARAMS : constr list; (* ordered *) + o_TCOMPS : constr list } (* ordered *) let object_table = (ref [] : ((global_reference * global_reference) * obj_typ) list ref) -let canonical_structures () = !object_table - -let cache_canonical_structure (_,(cst,lo)) = - List.iter (fun (o,_ as x) -> - if not (List.mem_assoc o !object_table) then - object_table := x :: (!object_table)) lo - -let subst_object subst ((r1,r2),o as obj) = - (* invariant: r1 and r2 are evaluable references. Thus subst_global *) - (* cannot instantiate them. Hence we can use just the first component *) - (* of the answer. *) - let r1',_ = subst_global subst r1 in - let r2',_ = subst_global subst r2 in - let o' = subst_obj subst o in - if r1' == r1 && r2' == r2 && o' == o then obj - else (r1',r2'),o' - -let subst_canonical_structure (_,subst,(cst,lo as obj)) = +let canonical_projections () = !object_table + +let keep_true_projections projs kinds = + map_succeed (function (p,true) -> p | _ -> failwith "") + (List.combine projs kinds) + +(* Intended to always success *) +let compute_canonical_projections (con,ind) = + let v = mkConst con in + let c = Environ.constant_value (Global.env()) con in + let lt,t = Reductionops.splay_lambda (Global.env()) Evd.empty c in + let lt = List.rev (List.map snd lt) in + let args = snd (decompose_app t) in + let { s_PARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in + let params, projs = list_chop p args in + let lpj = keep_true_projections lpj kl in + let lps = List.combine lpj projs in + let comp = + List.fold_left + (fun l (spopt,t) -> (* comp=components *) + match spopt with + | Some proji_sp -> + let c, args = decompose_app t in + (try (ConstRef proji_sp, reference_of_constr c, args) :: l + with Not_found -> l) + | _ -> l) + [] lps in + List.map (fun (refi,c,argj) -> + (refi,c),{o_DEF=v; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj}) + comp + +let open_canonical_structure i (_,o) = + if i=1 then + let lo = compute_canonical_projections o in + List.iter (fun (o,_ as x) -> + if not (List.mem_assoc o !object_table) then + object_table := x :: (!object_table)) lo + +let cache_canonical_structure o = + open_canonical_structure 1 o + +let subst_canonical_structure (_,subst,(cst,ind as obj)) = (* invariant: cst is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) let cst' = fst (subst_con subst cst) in - let lo' = list_smartmap (subst_object subst) lo in - if cst' == cst & lo' == lo then obj else (cst',lo') + let ind' = Inductiveops.subst_inductive subst ind in + if cst' == cst & ind' == ind then obj else (cst',ind') + +let discharge_canonical_structure (_,(cst,ind)) = + Some (Lib.discharge_con cst,Lib.discharge_inductive ind) let (inCanonStruc,outCanonStruct) = declare_object {(default_object "CANONICAL-STRUCTURE") with - open_function = (fun i o -> if i=1 then cache_canonical_structure o); + open_function = open_canonical_structure; cache_function = cache_canonical_structure; subst_function = subst_canonical_structure; classify_function = (fun (_,x) -> Substitute x); + discharge_function = discharge_canonical_structure; export_function = (function x -> Some x) } let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) +(*s High-level declaration of a canonical structure *) + +let error_not_structure ref = + errorlabstrm "object_declare" + (Nameops.pr_id (id_of_global ref) ++ str" is not a structure object") + +let check_and_decompose_canonical_structure ref = + let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in + let env = Global.env () in + let vc = match Environ.constant_opt_value env sp with + | Some vc -> vc + | None -> error_not_structure ref in + let f,args = match kind_of_term (snd (decompose_lam vc)) with + | App (f,args) -> f,args + | _ -> error_not_structure ref in + let indsp = match kind_of_term f with + | Construct (indsp,1) -> indsp + | _ -> error_not_structure ref in + let s = try lookup_structure indsp with Not_found -> error_not_structure ref in + if s.s_PARAM + List.length s.s_PROJ > Array.length args then + error_not_structure ref; + (sp,indsp) + +let declare_canonical_structure ref = + add_canonical_structure (check_and_decompose_canonical_structure ref) + let outCanonicalStructure x = fst (outCanonStruct x) -let canonical_structure_info o = List.assoc o !object_table +let lookup_canonical_conversion o = List.assoc o !object_table let freeze () = !structure_table, !projection_table, !object_table diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 7402f74c9..d6f90e11e 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -18,36 +18,36 @@ open Libobject open Library (*i*) +(*s A structure S is a non recursive inductive type with a single + constructor (the name of which defaults to Build_S) *) + type struc_typ = { s_CONST : identifier; s_PARAM : int; + s_PROJKIND : bool list; s_PROJ : constant option list } -val add_new_struc : - inductive * identifier * int * constant option list -> unit +val declare_structure : + inductive * identifier * int * bool list * constant option list -> unit -(* [find_structure isp] returns the infos associated to inductive path +(* [lookup_structure isp] returns the infos associated to inductive path [isp] if it corresponds to a structure, otherwise fails with [Not_found] *) -val find_structure : inductive -> struc_typ +val lookup_structure : inductive -> struc_typ (* raise [Not_found] if not a projection *) val find_projection_nparams : global_reference -> int +(*s A canonical structure declares "canonical" conversion hints between *) +(* the effective components of a structure and the projections of the *) +(* structure *) + type obj_typ = { o_DEF : constr; - o_TABS : constr list; (* dans l'ordre *) - o_TPARAMS : constr list; (* dans l'ordre *) - o_TCOMPS : constr list } (* dans l'ordre *) + o_TABS : constr list; (* ordered *) + o_TPARAMS : constr list; (* ordered *) + o_TCOMPS : constr list } (* ordered *) -val canonical_structure_info : - (global_reference * global_reference) -> obj_typ -val add_canonical_structure : - constant * ((global_reference * global_reference) * obj_typ) list -> unit - -val inStruc : inductive * struc_typ -> obj -val outStruc : obj -> inductive * struc_typ - -val outCanonicalStructure : obj -> constant - -val canonical_structures : unit -> +val lookup_canonical_conversion : (global_reference * global_reference) -> obj_typ +val declare_canonical_structure : global_reference -> unit +val canonical_projections : unit -> ((global_reference * global_reference) * obj_typ) list diff --git a/toplevel/class.ml b/toplevel/class.ml index 9d288c81e..88983637a 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -92,42 +92,16 @@ let explain_coercion_error g = function (* Verifications pour l'ajout d'une classe *) -let rec arity_sort (ctx,a) = match kind_of_term a with - | Sort (Prop _ | Type _) -> List.length ctx - | _ -> raise Not_found - let check_reference_arity ref = - let t = Global.type_of_global ref in - try arity_sort (Reductionops.splay_prod (Global.env()) Evd.empty t) - with Not_found -> raise (CoercionError (NotAClass ref)) + if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global ref)) then + raise (CoercionError (NotAClass ref)) let check_arity = function - | CL_FUN | CL_SORT -> 0 + | 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) -(* try_add_class : cl_typ -> strength option -> bool -> unit *) - -let strength_of_cl = function - | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn)) - | CL_SECVAR sp -> variable_strength sp - | _ -> Global - -let try_add_class cl streopt fail_if_exists = - if not (class_exists cl) then - let p = check_arity cl in - let stre' = strength_of_cl cl in - let stre = match streopt with - | Some stre -> strength_min (stre,stre') - | None -> stre' - in - declare_class (cl,stre,p) - else - if fail_if_exists then errorlabstrm "try_add_new_class" - (pr_class cl ++ str " is already a class") - - (* Coercions *) (* check that the computed target is the provided one *) @@ -154,12 +128,12 @@ let id_of_cl = function mip.mind_typename | CL_SECVAR id -> id -let class_of_ref = function +let class_of_global = function | ConstRef sp -> CL_CONST sp | IndRef sp -> CL_IND sp | VarRef id -> CL_SECVAR id | ConstructRef _ as c -> - errorlabstrm "class_of_ref" + errorlabstrm "class_of_global" (str "Constructors, such as " ++ Printer.pr_global c ++ str " cannot be used as class") @@ -209,9 +183,14 @@ let prods_of t = in aux [] t +let strength_of_cl = function + | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn)) + | CL_SECVAR sp -> variable_strength sp + | _ -> Global + let get_strength stre ref cls clt = - let stres = (snd (class_info cls)).cl_strength in - let stret = (snd (class_info clt)).cl_strength in + 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 @@ -290,10 +269,10 @@ lorque source est None alors target est None aussi. let add_new_coercion_core coef stre source target isid = check_source source; let env = Global.env () in - let v = constr_of_reference coef in - let vj = Retyping.get_judgment_of env Evd.empty v in + let v = constr_of_global coef in + let t = Global.type_of_global coef in if coercion_exists coef then raise (CoercionError AlreadyExists); - let tg,lp = prods_of (vj.uj_type) in + let tg,lp = prods_of t in let llp = List.length lp in if llp = 0 then raise (CoercionError NotAFunction); let (cls,lvs,ind) = @@ -312,10 +291,10 @@ let add_new_coercion_core coef stre source target isid = raise (CoercionError NoTarget) in check_target clt target; - try_add_class cls None false; - try_add_class clt None false; + check_arity cls; + check_arity clt; let stre' = get_strength stre coef cls clt in - declare_coercion coef vj stre' isid cls clt (List.length lvs) + declare_coercion coef stre' isid cls clt (List.length lvs) let try_add_new_coercion_core ref b c d e = try add_new_coercion_core ref b c d e @@ -346,118 +325,5 @@ let add_coercion_hook stre ref = ^ " is now a coercion") let add_subclass_hook stre ref = - let cl = class_of_ref ref in + let cl = class_of_global ref in try_add_new_coercion_subclass cl stre - -(* try_add_new_class : global_reference -> strength -> unit *) - -let class_of_global = function - | VarRef sp -> CL_SECVAR sp - | ConstRef sp -> CL_CONST sp - | IndRef sp -> CL_IND sp - | ConstructRef _ as ref -> raise (CoercionError (NotAClass ref)) - -let try_add_new_class ref stre = - try try_add_class (class_of_global ref) (Some stre) true - with CoercionError e -> - errorlabstrm "try_add_new_class" (explain_coercion_error ref e) - -(* fonctions pour le discharge: encore un peu sale mais ça s'améliore *) - -type coercion_entry = - global_reference * strength * bool * cl_typ * cl_typ * int - -let add_new_coercion (ref,stre,isid,cls,clt,n) = - (* Un peu lourd, tout cela pour trouver l'instance *) - let env = Global.env () in - let v = constr_of_reference ref in - let vj = Retyping.get_judgment_of env Evd.empty v in - declare_coercion ref vj stre isid cls clt n - -let count_extra_abstractions hyps ids_to_discard = - let _,n = - List.fold_left - (fun (hyps,n as sofar) id -> - match hyps with - | (hyp,None,_)::rest when id = hyp ->(rest, n+1) - | _ -> sofar) - (hyps,0) ids_to_discard - in n - -let defined_in_sec kn olddir = - let _,dir,_ = repr_kn kn in - dir = olddir - -let con_defined_in_sec kn olddir = - let _,dir,_ = repr_con kn in - dir = olddir - -(* This moves the global path one step below *) -let process_global olddir = function - | VarRef _ -> - anomaly "process_global only processes global surviving the section" - | ConstRef kn as x -> - if con_defined_in_sec kn olddir then - let newkn = Lib.make_con (id_of_label (con_label kn)) in - ConstRef newkn - else x - | IndRef (kn,i) as x -> - if defined_in_sec kn olddir then - let newkn = Lib.make_kn (id_of_label (label kn)) in - IndRef (newkn,i) - else x - | ConstructRef ((kn,i),j) as x -> - if defined_in_sec kn olddir then - let newkn = Lib.make_kn (id_of_label (label kn)) in - ConstructRef ((newkn,i),j) - else x - -let process_class olddir ids_to_discard x = - let (cl,{cl_strength=stre; cl_param=p}) = x in -(* let env = Global.env () in*) - match cl with - | CL_SECVAR _ -> x - | CL_CONST kn -> - if con_defined_in_sec kn olddir then - let newkn = Lib.make_con (id_of_label (con_label kn)) in - let hyps = (Global.lookup_constant kn).const_hyps in - let n = count_extra_abstractions hyps ids_to_discard in - (CL_CONST newkn,{cl_strength=stre;cl_param=p+n}) - else - x - | CL_IND (kn,i) -> - if defined_in_sec kn olddir then - let newkn = Lib.make_kn (id_of_label (label kn)) in - let hyps = (Global.lookup_mind kn).mind_hyps in - let n = count_extra_abstractions hyps ids_to_discard in - (CL_IND (newkn,i),{cl_strength=stre;cl_param=p+n}) - else - x - | _ -> anomaly "process_class" - -let process_cl sec_sp cl = - match cl with - | CL_SECVAR id -> cl - | CL_CONST kn -> - if con_defined_in_sec kn sec_sp then - let newkn = Lib.make_con (id_of_label (con_label kn)) in - CL_CONST newkn - else - cl - | CL_IND (kn,i) -> - if defined_in_sec kn sec_sp then - let newkn = Lib.make_kn (id_of_label (label kn)) in - CL_IND (newkn,i) - else - cl - | _ -> cl - -let process_coercion olddir ids_to_discard (coe,coeinfo,cls,clt) = - let hyps = context_of_global_reference coe in - let nargs = count_extra_abstractions hyps ids_to_discard in - (process_global olddir coe, - coercion_strength coeinfo, - coercion_identity coeinfo, - process_cl olddir cls, - process_cl olddir clt, - nargs + coercion_params coeinfo) diff --git a/toplevel/class.mli b/toplevel/class.mli index bf3425102..34af2e326 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -50,19 +50,4 @@ val add_coercion_hook : Tacexpr.declaration_hook val add_subclass_hook : Tacexpr.declaration_hook -(* [try_add_new_class ref] declares [ref] as a new class; usually, - this is done implicitely by [try_add_new_coercion]'s functions *) -val try_add_new_class : global_reference -> strength -> unit - -(*s This is used for the discharge *) -type coercion_entry - -val add_new_coercion : coercion_entry -> unit - -val process_class : - dir_path -> identifier list -> - (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ) -val process_coercion : - dir_path -> identifier list -> coercion -> coercion_entry - -val class_of_ref : global_reference -> cl_typ +val class_of_global : global_reference -> cl_typ diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index adca0d47d..8c71c0513 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -8,326 +8,75 @@ (* $Id$ *) -open Pp -open Util open Names -open Nameops +open Util open Sign open Term -open Declarations open Entries -open Inductive -open Reduction +open Declarations open Cooking -open Typeops -open Libnames -open Libobject -open Lib -open Nametab -open Declare -open Impargs -open Classops -open Class -open Recordops -open Library -open Indtypes -open Nametab -open Decl_kinds -let recalc_sp dir sp = - let (_,spid) = repr_path sp in Libnames.make_path dir spid +(********************************) +(* Discharging mutual inductive *) -let recalc_kn dir kn = - let (mp,_,l) = Names.repr_kn kn in - Names.make_kn mp dir l +let detype_param = function + | (Name id,None,p) -> id, Entries.LocalAssum p + | (Name id,Some p,_) -> id, Entries.LocalDef p + | (Anonymous,_,_) -> anomaly"Unnamed inductive local variable" -let recalc_con dir con = - let (mp,_,l) = Names.repr_con con in - Names.make_con mp dir l +(* Replace -let rec find_var id = function - | [] -> false - | (x,b,_)::l -> if x = id then b=None else find_var id l + Var(y1)..Var(yq):C1..Cq |- Ij:Bj + Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti -let build_abstract_list sec_sp hyps ids_to_discard = - let l1,l2 = - List.split - (List.fold_left - (fun vars id -> - if find_var id hyps then (mkVar id, Libnames.make_path sec_sp id)::vars - else vars) - [] ids_to_discard) in - Array.of_list l1, l2 + by -(* Discharge of inductives is done here (while discharge of constants - is done by the kernel for efficiency). *) + |- Ij: (y1..yq:C1..Cq)Bj + I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)] +*) -let abstract_inductive sec_sp ids_to_abs hyps inds = - let abstract_one_assum id t inds = - let ntyp = List.length inds in - let new_refs = - list_tabulate (fun k -> applist(mkRel (k+2),[mkRel 1])) ntyp in - let inds' = - List.map - (function (np,tname,arity,cnames,lc) -> - let arity' = mkNamedProd id t arity in - let lc' = - List.map (fun b -> mkNamedProd id t (substl new_refs b)) lc - in - (np,tname,arity',cnames,lc')) - inds - in - inds' in - let abstract_one_def id c inds = +let abstract_inductive hyps inds = + let ntyp = List.length inds in + let nhyp = named_context_length hyps in + let args = instance_from_named_context (List.rev hyps) in + let subs = list_tabulate (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) ntyp in + let inds' = List.map (function (np,tname,arity,cnames,lc) -> - let arity' = replace_vars [id, c] arity in - let lc' = List.map (replace_vars [id, c]) lc in - (np,tname,arity',cnames,lc')) - inds in - let abstract_once ((hyps,inds,vars) as sofar) id = - match hyps with - | (hyp,None,t as d)::rest when id = hyp -> - let inds' = abstract_one_assum hyp t inds in - (rest, inds', (mkVar id, Libnames.make_path sec_sp id)::vars) - | (hyp,Some b,t as d)::rest when id = hyp -> - let inds' = abstract_one_def hyp b inds in - (rest, inds', vars) - | _ -> sofar in - let (_,inds',vars) = - List.fold_left abstract_once (hyps,inds,[]) ids_to_abs in - let inds'' = - List.map - (fun (nparams,a,arity,c,lc) -> - let nparams' = nparams + (List.length vars) in - let params, short_arity = decompose_prod_n_assum nparams' arity in - let shortlc = - List.map (fun c -> snd (decompose_prod_n_assum nparams' c))lc in - let params' = - List.map - (function - | (Name id,None,p) -> id, Entries.LocalAssum p - | (Name id,Some p,_) -> id, Entries.LocalDef p - | (Anonymous,_,_) -> anomaly"Unnamed inductive local variable") - params in - { mind_entry_params = params'; - mind_entry_typename = a; - mind_entry_arity = short_arity; - mind_entry_consnames = c; - mind_entry_lc = shortlc }) - inds' in - let l1,l2 = List.split vars in - (inds'', Array.of_list l1, l2) - -let process_inductive sec_sp osecsp nsecsp oldenv (ids_to_discard,modlist) mib = - assert (Array.length mib.mind_packets > 0); - let record = mib.mind_record in - let finite = mib.mind_finite in + let lc' = List.map (substl subs) lc in + let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b hyps) lc' in + let arity' = Termops.it_mkNamedProd_wo_LetIn arity hyps in + (np,tname,arity',cnames,lc'')) + inds in + List.map + (fun (nparams,a,arity,c,lc) -> + let nparams' = nparams + Array.length args in + let params, short_arity = decompose_prod_n_assum nparams' arity in + let shortlc = + List.map (fun c -> snd (decompose_prod_n_assum nparams' c))lc in + let params' = List.map detype_param params in + { mind_entry_params = params'; + mind_entry_typename = a; + mind_entry_arity = short_arity; + mind_entry_consnames = c; + mind_entry_lc = shortlc }) + inds' + +let process_inductive sechyps modlist mib = let inds = array_map_to_list (fun mip -> let nparams = mip.mind_nparams in - let arity = expmod_type modlist mip.mind_user_arity in - let lc = Array.map (expmod_type modlist) mip.mind_user_lc in + let arity = expmod_constr modlist mip.mind_user_arity in + let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in (nparams, mip.mind_typename, arity, Array.to_list mip.mind_consnames, Array.to_list lc)) - mib.mind_packets - in - let hyps = mib.mind_hyps in - let hyps' = - Sign.fold_named_context - (fun (x,b,t) sgn -> - Sign.add_named_decl - (x, option_app (expmod_constr modlist) b,expmod_constr modlist t) - sgn) - mib.mind_hyps ~init:empty_named_context in - let (inds',abs_vars,discharged_hyps ) = - abstract_inductive sec_sp ids_to_discard hyps' inds in - let lmodif_one_mind i = - let nbc = Array.length mib.mind_packets.(i).mind_consnames in - (((osecsp,i), DO_ABSTRACT ((nsecsp,i),abs_vars)), - list_tabulate - (function j -> - let j' = j + 1 in - (((osecsp,i),j'), DO_ABSTRACT (((nsecsp,i),j'),abs_vars))) - nbc) - in - let indmodifs,cstrmodifs = - List.split (list_tabulate lmodif_one_mind mib.mind_ntypes) in - ({ mind_entry_record = record; - mind_entry_finite = finite; - mind_entry_inds = inds' }, - indmodifs, - List.flatten cstrmodifs, - discharged_hyps) - -(* Discharge messages. *) - -let constant_message id = - Options.if_verbose ppnl (pr_id id ++ str " is discharged.") - -let inductive_message inds = - Options.if_verbose - ppnl - (hov 0 - (match inds with - | [] -> assert false - | [ind] -> - (pr_id ind.mind_entry_typename ++ str " is discharged.") - | l -> - (prlist_with_sep pr_coma - (fun ind -> pr_id ind.mind_entry_typename) l ++ - spc () ++ str "are discharged."))) - -(* Discharge operations for the various objects of the environment. *) - -type opacity = bool - -type discharge_operation = - | Variable of identifier * section_variable_entry * local_kind * - implicits_flags * Dischargedhypsmap.discharged_hyps - | Constant of identifier * recipe * global_kind * constant * - implicits_flags * Dischargedhypsmap.discharged_hyps - | Inductive of mutual_inductive_entry * implicits_flags * - Dischargedhypsmap.discharged_hyps - | Class of cl_typ * cl_info_typ - | Struc of inductive * (unit -> struc_typ) - | CanonStruc of constant - | Coercion of coercion_entry - | Require of library_reference - | Constraints of Univ.constraints - -(* Main function to traverse the library segment and compute the various - discharge operations. *) - -let process_object oldenv olddir full_olddir newdir -(* {dir -> newdir} {sec_sp -> full_olddir, olddir} *) - (ops,ids_to_discard,(constl,indl,cstrl as work_alist)) ((sp,kn),lobj) = - let tag = object_tag lobj in - match tag with - | "VARIABLE" -> - let ((id,c,t),cst) = get_variable_with_constraints (basename sp) in - (* VARIABLE means local (entry Variable/Hypothesis/Local and are *) - (* always discharged *) - (Constraints cst :: ops, id :: ids_to_discard, work_alist) - - | "CONSTANT" -> - (* CONSTANT means never discharge (though visibility may vary) *) - let kind = constant_kind sp in - let kn = Nametab.locate_constant (qualid_of_sp sp) in - let lab = con_label kn in - let cb = Environ.lookup_constant kn oldenv in - let imp = is_implicit_constant kn in - let newkn = recalc_con newdir kn in - let abs_vars,discharged_hyps0 = - build_abstract_list full_olddir cb.const_hyps ids_to_discard in - (* let's add the new discharged hypothesis to those already discharged*) - let discharged_hyps = - discharged_hyps0 @ Dischargedhypsmap.get_discharged_hyps sp in - let mods = [ (kn, DO_ABSTRACT(newkn,abs_vars)) ] - in - let r = { d_from = cb; - d_modlist = work_alist; - d_abstract = ids_to_discard } in - let op = Constant (id_of_label lab,r,kind,newkn,imp,discharged_hyps) in - (op :: ops, ids_to_discard, (mods@constl, indl, cstrl)) - - | "INDUCTIVE" -> - let kn = Nametab.locate_mind (qualid_of_sp sp) in - let mib = Environ.lookup_mind kn oldenv in - let newkn = recalc_kn newdir kn in - let imp = is_implicit_inductive_definition kn in -(* let imp = is_implicit_args (* CHANGE *) in*) - let (mie,indmods,cstrmods,discharged_hyps0) = - process_inductive full_olddir kn newkn oldenv (ids_to_discard,work_alist) mib in - (* let's add the new discharged hypothesis to those already discharged*) - let discharged_hyps = - discharged_hyps0 @ Dischargedhypsmap.get_discharged_hyps sp in - ((Inductive(mie,imp,discharged_hyps)) :: ops, ids_to_discard, - (constl,indmods@indl,cstrmods@cstrl)) - - | "CLASS" -> - let ((cl,clinfo) as x) = outClass lobj in - if clinfo.cl_strength = Local then - (ops,ids_to_discard,work_alist) - else - let (y1,y2) = process_class olddir ids_to_discard x in - ((Class (y1,y2))::ops, ids_to_discard, work_alist) - - | "COERCION" -> - let (_,coeinfo,_,_ as x) = outCoercion lobj in - if coercion_strength coeinfo = Local then - (ops,ids_to_discard,work_alist) - else - let y = process_coercion olddir ids_to_discard x in - ((Coercion y)::ops, ids_to_discard, work_alist) - - | "STRUCTURE" -> - let ((kn,i),info) = outStruc lobj in - let newkn = recalc_kn newdir kn in - let strobj () = - let mib = Environ.lookup_mind newkn (Global.env ()) in - { s_CONST = info.s_CONST; - s_PARAM = mib.mind_packets.(0).mind_nparams; - s_PROJ = List.map (option_app (fun kn -> recalc_con newdir kn)) info.s_PROJ } in - ((Struc ((newkn,i),strobj))::ops, ids_to_discard, work_alist) - - | "CANONICAL-STRUCTURE" -> - let kn = outCanonicalStructure lobj in - let new_kn = recalc_con newdir kn in - ((CanonStruc new_kn)::ops, ids_to_discard, work_alist) - - | "REQUIRE" -> - let c = out_require lobj in - ((Require c)::ops, ids_to_discard, work_alist) - - | _ -> (ops,ids_to_discard,work_alist) - -let process_item oldenv olddir full_olddir newdir acc = function - | (sp,Leaf lobj) -> - process_object oldenv olddir full_olddir newdir acc (sp,lobj) - | (_,_) -> acc - -let process_operation = function - | Variable (id,expmod_a,stre,imp,discharged_hyps) -> - (* Warning:parentheses needed to get a side-effect from with_implicits *) - with_implicits imp (redeclare_variable id discharged_hyps) - (Lib.cwd(),expmod_a,stre) - | Constant (id,r,stre,kn,imp,discharged_hyps) -> - with_implicits imp (redeclare_constant id discharged_hyps) (r,stre); - constant_message id - | Inductive (mie,imp,discharged_hyps) -> - let _ = with_implicits imp (redeclare_inductive discharged_hyps) mie in - inductive_message mie.mind_entry_inds - | Class (y1,y2) -> - Lib.add_anonymous_leaf (inClass (y1,y2)) - | Struc (newsp,strobj) -> - Lib.add_anonymous_leaf (inStruc (newsp,strobj ())) - | CanonStruc newsp -> - begin try Recordobj.objdef_declare (ConstRef newsp) with _ -> () end - | Coercion y -> add_new_coercion y - | Require y -> reload_library y - | Constraints y -> Global.add_constraints y - -let catch_not_found f x = - try f x - with Not_found -> - error ("Something is missing; perhaps a reference to a"^ - " module required inside the section") - -let close_section _ s = - let oldenv = Global.env() in - let prefix,decls,fs = close_section false s in - let full_olddir, (_,olddir) = prefix in - let newdir = fst (split_dirpath olddir) in - let (ops,ids,_) = - List.fold_left - (process_item oldenv olddir full_olddir newdir) ([],[],([],[],[])) decls - in - let ids = last_section_hyps olddir in - Summary.section_unfreeze_summaries fs; - catch_not_found (List.iter process_operation) (List.rev ops); - Nametab.push_dir (Until 1) full_olddir (DirClosedSection full_olddir) + mib.mind_packets in + let sechyps' = map_named_context (expmod_constr modlist) sechyps in + let inds' = abstract_inductive sechyps' inds in + { mind_entry_record = mib.mind_record; + mind_entry_finite = mib.mind_finite; + mind_entry_inds = inds' } diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli index b8db027ba..c8af4d1da 100644 --- a/toplevel/discharge.mli +++ b/toplevel/discharge.mli @@ -8,11 +8,10 @@ (*i $Id$ i*) -open Names +open Sign +open Cooking +open Declarations +open Entries -(* This module implements the discharge mechanism. It provides a function to - close the last opened section. That function calls [Lib.close_section] and - then re-introduce all the discharged versions of the objects that were - defined in the section. *) - -val close_section : bool -> identifier -> unit +val process_inductive : + named_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml index 6457fb538..4c1e2210a 100755 --- a/toplevel/recordobj.ml +++ b/toplevel/recordobj.ml @@ -8,68 +8,3 @@ (* $Id$ *) -open Util -open Pp -open Names -open Libnames -open Nameops -open Term -open Lib -open Declare -open Recordops -open Classops -open Nametab - -(***** object definition ******) - -let typ_lams_of t = - let rec aux acc c = match kind_of_term c with - | Lambda (x,c1,c2) -> aux (c1::acc) c2 - | Cast (c,_) -> aux acc c - | t -> acc,t - in aux [] t - -let objdef_err ref = - errorlabstrm "object_declare" - (pr_id (id_of_global ref) ++ - str" is not a structure object") - -let objdef_declare ref = - let sp = match ref with ConstRef sp -> sp | _ -> objdef_err ref in - let env = Global.env () in - let v = constr_of_reference ref in - let vc = match Environ.constant_opt_value env sp with - | Some vc -> vc - | None -> objdef_err ref in - let lt,t = decompose_lam vc in - let lt = List.rev (List.map snd lt) in - let f,args = match kind_of_term t with - | App (f,args) -> f,args - | _ -> objdef_err ref in - let { s_PARAM = p; s_PROJ = lpj } = - try (find_structure - (match kind_of_term f with - | Construct (indsp,1) -> indsp - | _ -> objdef_err ref)) - with Not_found -> objdef_err ref in - let params, projs = - try list_chop p (Array.to_list args) - with _ -> objdef_err ref in - let lps = - try List.combine lpj projs - with _ -> objdef_err ref in - let comp = - List.fold_left - (fun l (spopt,t) -> (* comp=components *) - match spopt with - | None -> l - | Some proji_sp -> - let c, args = decompose_app t in - try (ConstRef proji_sp, reference_of_constr c, args) :: l - with Not_found -> l) - [] lps in - let comp' = List.map (fun (refi,c,argj) -> - (refi,c),{o_DEF=v; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj}) comp in - add_canonical_structure (sp, comp') - -let add_object_hook _ = objdef_declare diff --git a/toplevel/recordobj.mli b/toplevel/recordobj.mli index 02c3126dd..5bbeecc2c 100755 --- a/toplevel/recordobj.mli +++ b/toplevel/recordobj.mli @@ -8,5 +8,3 @@ (*i $Id$ i*) -val objdef_declare : Libnames.global_reference -> unit -val add_object_hook : Tacexpr.declaration_hook -- cgit v1.2.3