From 60de53d159c85b8300226a61aa502a7e0dd2f04b Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 26 Feb 2013 18:52:24 +0000 Subject: kernel/declarations becomes a pure mli - constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml - the functions that were in declarations.ml (mostly substitution utilities and hashcons) are now in kernel/declareops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/extraction/extract_env.ml | 2 +- plugins/extraction/extraction.ml | 24 +++++++++++++++--------- plugins/extraction/mlutil.ml | 1 + plugins/funind/functional_principles_proofs.ml | 5 +++-- plugins/funind/functional_principles_types.ml | 5 +++-- plugins/funind/indfun.ml | 3 ++- plugins/funind/indfun_common.ml | 4 ++-- plugins/funind/recdef.ml | 3 ++- plugins/xml/xmlcommand.ml | 21 ++++++++++----------- 9 files changed, 39 insertions(+), 29 deletions(-) (limited to 'plugins') diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 5aee45dcc..ae60259e9 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -136,7 +136,7 @@ let check_arity env cb = let check_fix env cb i = match cb.const_body with | Def lbody -> - (match kind_of_term (Declarations.force lbody) with + (match kind_of_term (Lazyconstr.force lbody) with | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd) | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd) | _ -> raise Impossible) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index c8f376565..035f8e3bb 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -11,6 +11,7 @@ open Util open Names open Term open Declarations +open Declareops open Environ open Reduction open Reductionops @@ -277,7 +278,7 @@ let rec extract_type env db j c args = | Undef _ | OpaqueDef _ -> mlt | Def _ when is_custom r -> mlt | Def lbody -> - let newc = applist (Declarations.force lbody, args) in + let newc = applist (Lazyconstr.force lbody, args) in let mlt' = extract_type env db j newc [] in (* ML type abbreviations interact badly with Coq *) (* reduction, so [mlt] and [mlt'] might be different: *) @@ -291,7 +292,7 @@ let rec extract_type env db j c args = | Undef _ | OpaqueDef _ -> Tunknown (* Brutal approx ... *) | Def lbody -> (* We try to reduce. *) - let newc = applist (Declarations.force lbody, args) in + let newc = applist (Lazyconstr.force lbody, args) in extract_type env db j newc [])) | Ind (kn,i) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in @@ -515,7 +516,7 @@ and mlt_env env r = match r with | Def l_body -> (match flag_of_type env typ with | Info,TypeScheme -> - let body = Declarations.force l_body in + let body = Lazyconstr.force l_body in let s,vl = type_sign_vl env typ in let db = db_from_sign s in let t = extract_type_scheme env db body (List.length s) @@ -986,17 +987,21 @@ let extract_constant env kn cb = | (Info,TypeScheme) -> (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () - | Def c -> mk_typ (force c) + | Def c -> mk_typ (Lazyconstr.force c) | OpaqueDef c -> add_opaque r; - if access_opaque () then mk_typ (force_opaque c) else mk_typ_ax ()) + if access_opaque () then + mk_typ (Lazyconstr.force_opaque c) + else mk_typ_ax ()) | (Info,Default) -> (match cb.const_body with | Undef _ -> warn_info (); mk_ax () - | Def c -> mk_def (force c) + | Def c -> mk_def (Lazyconstr.force c) | OpaqueDef c -> add_opaque r; - if access_opaque () then mk_def (force_opaque c) else mk_ax ()) + if access_opaque () then + mk_def (Lazyconstr.force_opaque c) + else mk_ax ()) let extract_constant_spec env kn cb = let r = ConstRef kn in @@ -1010,7 +1015,8 @@ let extract_constant_spec env kn cb = | Undef _ | OpaqueDef _ -> Stype (r, vl, None) | Def body -> let db = db_from_sign s in - let t = extract_type_scheme env db (force body) (List.length s) + let body = Lazyconstr.force body in + let t = extract_type_scheme env db body (List.length s) in Stype (r, vl, Some t)) | (Info, Default) -> let t = snd (record_constant_type env kn (Some typ)) in @@ -1023,7 +1029,7 @@ let extract_with_type env cb = let s,vl = type_sign_vl env typ in let db = db_from_sign s in let c = match cb.const_body with - | Def body -> force body + | Def body -> Lazyconstr.force body (* A "with Definition ..." is necessarily transparent *) | Undef _ | OpaqueDef _ -> assert false in diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 8ecd8cd7c..4407c6798 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1289,6 +1289,7 @@ let is_not_strict t = *) open Declarations +open Declareops let inline_test r t = if not (auto_inline ()) then false diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 450b3ef40..3c92bb5bd 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -5,6 +5,7 @@ open Term open Namegen open Names open Declarations +open Declareops open Pp open Hiddentac open Tacmach @@ -947,7 +948,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let f_def = Global.lookup_constant (destConst f) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in let f_body = - force (Option.get (body_of_constant f_def)) + Lazyconstr.force (Option.get (body_of_constant f_def)) in let params,f_body_with_params = decompose_lam_n nb_params f_body in let (_,num),(_,_,bodies) = destFix f_body_with_params in @@ -1065,7 +1066,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let get_body const = match body_of_constant (Global.lookup_constant const) with | Some b -> - let body = force b in + let body = Lazyconstr.force b in Tacred.cbv_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) (Global.env ()) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 9916ed95a..debf96345 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -5,6 +5,7 @@ open Term open Namegen open Names open Declarations +open Declareops open Pp open Entries open Tactics @@ -404,7 +405,7 @@ let get_funs_constant mp dp = let find_constant_body const = match body_of_constant (Global.lookup_constant const) with | Some b -> - let body = force b in + let body = Lazyconstr.force b in let body = Tacred.cbv_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) (Global.env ()) @@ -539,7 +540,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis let finfos = find_Function_infos this_block_funs.(0) in try let equation = Option.get finfos.equation_lemma in - Declarations.is_opaque (Global.lookup_constant equation) + Declareops.is_opaque (Global.lookup_constant equation) with Option.IsNone -> (* non recursive definition *) false in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 99bf66d1f..fd4e23de7 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -8,6 +8,7 @@ open Libnames open Globnames open Glob_term open Declarations +open Declareops open Misctypes open Decl_kinds @@ -770,7 +771,7 @@ let make_graph (f_ref:global_reference) = | None -> error "Cannot build a graph over an axiom !" | Some b -> let env = Global.env () in - let body = (force b) in + let body = Lazyconstr.force b in let extern_body,extern_type = with_full_print (fun () -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 92d2fe680..9879f08a0 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -121,8 +121,8 @@ let const_of_id id = let def_of_const t = match (Term.kind_of_term t) with Term.Const sp -> - (try (match Declarations.body_of_constant (Global.lookup_constant sp) with - | Some c -> Declarations.force c + (try (match Declareops.body_of_constant (Global.lookup_constant sp) with + | Some c -> Lazyconstr.force c | _ -> assert false) with _ -> assert false) |_ -> assert false diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d5e1ee53a..bea019259 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -10,6 +10,7 @@ open Term open Namegen open Environ open Declarations +open Declareops open Entries open Pp open Names @@ -68,7 +69,7 @@ let def_of_const t = match (kind_of_term t) with Const sp -> (try (match body_of_constant (Global.lookup_constant sp) with - | Some c -> Declarations.force c + | Some c -> Lazyconstr.force c | _ -> assert false) with _ -> anomaly (str "Cannot find definition of constant " ++ diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 033c84691..4d9541ebc 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -229,12 +229,11 @@ let mk_constant_obj id bo ty variables hyps = Acic.Constant (Names.Id.to_string id,None,ty,params) | Some c -> Acic.Constant - (Names.Id.to_string id, Some (Unshare.unshare (Declarations.force c)), + (Names.Id.to_string id, Some (Unshare.unshare (Lazyconstr.force c)), ty,params) ;; let mk_inductive_obj sp mib packs variables nparams hyps finite = - let module D = Declarations in let hyps = string_list_of_named_context_list hyps in let params = filter_params variables hyps in (* let nparams = extract_nparams packs in *) @@ -243,8 +242,8 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite = Array.fold_right (fun p i -> decr tyno ; - let {D.mind_consnames=consnames ; - D.mind_typename=typename } = p + let {Declarations.mind_consnames=consnames ; + Declarations.mind_typename=typename } = p in let arity = Inductive.type_of_inductive (Global.env()) (mib,p) in let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in @@ -368,7 +367,7 @@ let print_object_kind uri (xmltag,variation) = (* form of the definition (all the parameters are *) (* lambda-abstracted, but the object can still refer to variables) *) let print internal glob_ref kind xml_library_root = - let module D = Declarations in + let module D = Declareops in let module De = Declare in let module G = Global in let module N = Names in @@ -392,16 +391,16 @@ let print internal glob_ref kind xml_library_root = let id = N.Label.to_id (N.con_label kn) in let cb = G.lookup_constant kn in let val0 = D.body_of_constant cb in - let typ = cb.D.const_type in - let hyps = cb.D.const_hyps in + let typ = cb.Declarations.const_type in + let hyps = cb.Declarations.const_hyps in let typ = Typeops.type_of_constant_type (Global.env()) typ in Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps | Gn.IndRef (kn,_) -> let mib = G.lookup_mind kn in - let {D.mind_nparams=nparams; - D.mind_packets=packs ; - D.mind_hyps=hyps; - D.mind_finite=finite} = mib in + let {Declarations.mind_nparams=nparams; + Declarations.mind_packets=packs ; + Declarations.mind_hyps=hyps; + Declarations.mind_finite=finite} = mib in Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite | Gn.ConstructRef _ -> Errors.error ("a single constructor cannot be printed in XML") -- cgit v1.2.3