diff options
Diffstat (limited to 'toplevel/discharge.ml')
| -rw-r--r-- | toplevel/discharge.ml | 364 |
1 files changed, 61 insertions, 303 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 281ff1b6..6c543079 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -6,325 +6,83 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: discharge.ml,v 1.81.2.2 2005/11/29 21:40:53 letouzey Exp $ *) +(* $Id: discharge.ml 7493 2005-11-02 22:12:16Z mohring $ *) -open Pp -open Util open Names -open Nameops +open Util open Sign open Term -open Declarations open Entries -open Inductive -open Instantiate -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 rec find_var id = function - | [] -> false - | (x,b,_)::l -> if x = id then b=None else find_var id l +(* Replace -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 + Var(y1)..Var(yq):C1..Cq |- Ij:Bj + Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti -(* Discharge of inductives is done here (while discharge of constants - is done by the kernel for efficiency). *) + by -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) + |- 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 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 abstract_inductive hyps nparams 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 (tname,arity,cnames,lc) -> + 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 + (tname,arity',cnames,lc'')) + inds in + let nparams' = nparams + Array.length args in +(* To be sure to be the same as before, should probably be moved to process_inductive *) + let params' = let (_,arity,_,_) = List.hd inds' in + let (params,_) = decompose_prod_n_assum nparams' arity in + List.map detype_param params + in + let ind'' = + List.map + (fun (a,arity,c,lc) -> + let _, short_arity = decompose_prod_n_assum nparams' arity in + let shortlc = + List.map (fun c -> snd (decompose_prod_n_assum nparams' c)) lc in + { mind_entry_typename = a; + mind_entry_arity = short_arity; + mind_entry_consnames = c; + mind_entry_lc = shortlc }) + inds' + in (params',ind'') + + +let process_inductive sechyps modlist mib = + let nparams = mib.mind_nparams 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, + let arity = expmod_constr modlist mip.mind_user_arity in + let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in + (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) - | 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) + mib.mind_packets in + let sechyps' = map_named_context (expmod_constr modlist) sechyps in + let (params',inds') = abstract_inductive sechyps' nparams inds in + { mind_entry_record = mib.mind_record; + mind_entry_finite = mib.mind_finite; + mind_entry_params = params'; + mind_entry_inds = inds' } |