diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /toplevel/discharge.ml |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'toplevel/discharge.ml')
-rw-r--r-- | toplevel/discharge.ml | 328 |
1 files changed, 328 insertions, 0 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml new file mode 100644 index 00000000..688885b1 --- /dev/null +++ b/toplevel/discharge.ml @@ -0,0 +1,328 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: discharge.ml,v 1.81.2.1 2004/07/16 19:31:48 herbelin Exp $ *) + +open Pp +open Util +open Names +open Nameops +open Sign +open Term +open Declarations +open Entries +open Inductive +open Instantiate +open Reduction +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 + +let recalc_kn dir kn = + let (mp,_,l) = Names.repr_kn kn in + Names.make_kn mp dir l + +let rec find_var id = function + | [] -> false + | (x,b,_)::l -> if x = id then b=None else find_var id l + +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 + +(* Discharge of inductives is done here (while discharge of constants + is done by the kernel for efficiency). *) + +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 = + 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 finite = mib.mind_finite in + 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 + (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_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) + | Objdef 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 = label kn in + let cb = Environ.lookup_constant kn oldenv in + let imp = is_implicit_constant kn in + let newkn = recalc_kn 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_kn newdir kn)) info.s_PROJ } in + ((Struc ((newkn,i),strobj))::ops, ids_to_discard, work_alist) + + | "OBJDEF1" -> + let kn = outObjDef1 lobj in + let new_kn = recalc_kn newdir kn in + ((Objdef 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 ())) + | Objdef 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) |