From e4282ea99c664d8d58067bee199cbbcf881b60d5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 4 Jul 2009 13:28:35 +0200 Subject: Imported Upstream version 8.2.pl1+dfsg --- library/declare.ml | 6 ++-- library/declare.mli | 4 +-- library/declaremods.ml | 90 +++++++++++++++++++++++++------------------------- library/impargs.ml | 56 +++++++++++++------------------ library/impargs.mli | 4 +-- library/lib.ml | 22 +++++++----- library/lib.mli | 6 ++-- library/states.ml | 9 ++++- library/states.mli | 7 +++- 9 files changed, 106 insertions(+), 98 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 4bdc11c3..c349bef1 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: declare.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: declare.ml 12187 2009-06-13 19:36:59Z msozeau $ *) (** This module is about the low-level declaration of logical objects *) @@ -43,7 +43,7 @@ let set_xml_declare_inductive f = xml_declare_inductive := if_xml f type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) - | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *) + | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep *) type variable_declaration = dir_path * section_variable_entry * logical_kind @@ -58,7 +58,7 @@ let cache_variable ((sp,_),o) = | SectionLocalAssum (ty, impl, keep) -> let cst = Global.push_named_assum (id,ty) in let impl = if impl then Lib.Implicit else Lib.Explicit in - let keep = if keep then Some ty else None in + let keep = if keep <> [] then Some (ty, keep) else None in impl, true, cst, keep | SectionLocalDef (c,t,opaq) -> let cst = Global.push_named_def (id,c,t) in diff --git a/library/declare.mli b/library/declare.mli index 78d3f027..2f1cd06e 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declare.mli 10840 2008-04-23 21:29:34Z herbelin $ i*) +(*i $Id: declare.mli 12187 2009-06-13 19:36:59Z msozeau $ i*) (*i*) open Names @@ -34,7 +34,7 @@ open Nametab type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) - | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *) + | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep list *) type variable_declaration = dir_path * section_variable_entry * logical_kind diff --git a/library/declaremods.ml b/library/declaremods.ml index 3026143b..93021384 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.ml 11898 2009-02-10 10:52:45Z soubiran $ i*) +(*i $Id: declaremods.ml 12204 2009-06-22 16:06:49Z soubiran $ i*) open Pp open Util open Names @@ -642,29 +642,30 @@ let rec get_modtype_substobjs env = function (subst_key (map_msid msid mp) sub_alias) (map_msid msid mp) | _ -> sub_alias in - let sub3= + let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in + let mbid,mbids= (match mbids with + | mbid::mbids -> mbid,mbids + | [] -> match mexpr with + | MSEident _ -> error "Application of a non-functor" + | _ -> error "Application of a functor with too few arguments") in + let resolve = + Modops.resolver_of_environment farg_id farg_b mp sub_alias env in + let sub3= if sub1 = empty_subst then - update_subst sub_alias (map_mbid farg_id mp None) + update_subst sub_alias (map_mbid farg_id mp (Some resolve)) else - let sub1' = join_alias sub1 (map_mbid farg_id mp None) in + let sub1' = join_alias sub1 (map_mbid farg_id mp (Some resolve)) in let sub_alias' = update_subst sub_alias sub1' in join sub1' sub_alias' in - let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in - let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in - (match mbids with - | mbid::mbids -> - let resolve = - Modops.resolver_of_environment farg_id farg_b mp sub_alias env in - (* application outside the kernel, only for substitutive - objects (that are all non-logical objects) *) - ((join - (join subst sub3) - (map_mbid mbid mp (Some resolve))) - , mbids, msid, objs) - | [] -> match mexpr with - | MSEident _ -> error "Application of a non-functor" - | _ -> error "Application of a functor with too few arguments") + let sub3 = join sub3 + (update_subst sub_alias (map_mbid farg_id mp (Some resolve))) in + (* application outside the kernel, only for substitutive + objects (that are all non-logical objects) *) + ((join + (join subst sub3) + (map_mbid mbid mp (Some resolve))) + , mbids, msid, objs) | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr @@ -948,30 +949,32 @@ let rec get_module_substobjs env = function (subst_key (map_msid msid mp) sub_alias) (map_msid msid mp) | _ -> sub_alias in - + let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in + let mbid,mbids = + (match mbids with + | mbid::mbids ->mbid,mbids + + | [] -> match mexpr with + | MSEident _ -> error "Application of a non-functor" + | _ -> error "Application of a functor with too few arguments") in + let resolve = + Modops.resolver_of_environment farg_id farg_b mp sub_alias env in let sub3= if sub1 = empty_subst then - update_subst sub_alias (map_mbid farg_id mp None) + update_subst sub_alias (map_mbid farg_id mp (Some resolve)) else - let sub1' = join_alias sub1 (map_mbid farg_id mp None) in + let sub1' = join_alias sub1 (map_mbid farg_id mp (Some resolve)) in let sub_alias' = update_subst sub_alias sub1' in - join sub1' sub_alias' + join sub1' sub_alias' in - let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in - let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in - (match mbids with - | mbid::mbids -> - let resolve = - Modops.resolver_of_environment farg_id farg_b mp sub_alias env in - (* application outside the kernel, only for substitutive - objects (that are all non-logical objects) *) - ((join - (join subst sub3) - (map_mbid mbid mp (Some resolve))) - , mbids, msid, objs) - | [] -> match mexpr with - | MSEident _ -> error "Application of a non-functor" - | _ -> error "Application of a functor with too few arguments") + let sub3 = join sub3 (update_subst sub_alias + (map_mbid farg_id mp (Some resolve))) in + (* application outside the kernel, only for substitutive + objects (that are all non-logical objects) *) + ((join + (join subst sub3) + (map_mbid mbid mp (Some resolve))) + , mbids, msid, objs) | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr | MSEwith (mty, With_Definition _) -> get_module_substobjs env mty @@ -1061,12 +1064,9 @@ let rec update_include (sub,mbids,msid,objs) = | (id,obj)::tail -> if object_tag obj = "INCLUDE" then let ((me,is_mod),substobjs,substituted) = out_include obj in - if not (is_mod) then - let substobjs' = update_include substobjs in - (id, in_include ((me,true),substobjs',substituted)):: - (replace_include tail) - else - (id,obj)::(replace_include tail) + let substobjs' = update_include substobjs in + (id, in_include ((me,true),substobjs',substituted)):: + (replace_include tail) else (id,obj)::(replace_include tail) in @@ -1142,7 +1142,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = | _ -> let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in let (sub,mbids,msid,objs) = substobjs in - let sub' = subst_key (map_msid msid mp) sub in + let sub' = join_alias (subst_key (map_msid msid mp) sub) (map_msid msid mp) in let substobjs = (join sub sub',mbids,msid,objs) in let substituted = subst_substobjs dir mp substobjs in ignore (add_leaf diff --git a/library/impargs.ml b/library/impargs.ml index 2b2c607c..14f88728 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: impargs.ml 11576 2008-11-10 19:13:15Z msozeau $ *) +(* $Id: impargs.ml 12187 2009-06-13 19:36:59Z msozeau $ *) open Util open Names @@ -26,8 +26,7 @@ open Termops (*s Flags governing the computation of implicit arguments *) type implicits_flags = { - main : bool; - manual : bool; (* automatic or manual only *) + auto : bool; (* automatic or manual only *) strict : bool; (* true = strict *) strongly_strict : bool; (* true = strongly strict *) reversible_pattern : bool; @@ -38,8 +37,7 @@ type implicits_flags = { (* les implicites sont stricts par défaut en v8 *) let implicit_args = ref { - main = false; - manual = false; + auto = false; strict = true; strongly_strict = false; reversible_pattern = false; @@ -48,11 +46,7 @@ let implicit_args = ref { } let make_implicit_args flag = - implicit_args := { !implicit_args with main = flag } - -let make_manual_implicit_args flag = - implicit_args := { !implicit_args with main = if flag then true else !implicit_args.main; - manual = flag } + implicit_args := { !implicit_args with auto = flag } let make_strict_implicit_args flag = implicit_args := { !implicit_args with strict = flag } @@ -69,9 +63,7 @@ let make_contextual_implicit_args flag = let make_maximal_implicit_args flag = implicit_args := { !implicit_args with maximal = flag } -let is_implicit_args () = !implicit_args.main -let is_manual_implicit_args () = !implicit_args.manual -let is_auto_implicit_args () = !implicit_args.main && not (is_manual_implicit_args ()) +let is_implicit_args () = !implicit_args.auto let is_strict_implicit_args () = !implicit_args.strict let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern @@ -316,10 +308,10 @@ let const v _ = v let compute_implicits_auto env f manual t = match manual with | [] -> - let l = compute_implicits_flags env f false t in - if f.manual then List.map (const None) l - else prepare_implicits f l - | _ -> compute_manual_implicits env f t (not f.manual) manual + if not f.auto then [] + else let l = compute_implicits_flags env f false t in + prepare_implicits f l + | _ -> compute_manual_implicits env f t f.auto manual let compute_implicits env t = compute_implicits_auto env !implicit_args [] t @@ -523,7 +515,7 @@ let rebuild_implicits (req,l) = | ImplManual m -> let oldimpls = snd (List.hd l) in let auto = - if flags.main then + if flags.auto then let newimpls = compute_global_implicits flags [] ref in merge_impls oldimpls newimpls else oldimpls @@ -549,32 +541,30 @@ let declare_implicits_gen req flags ref = add_anonymous_leaf (inImplicits (req,[ref,imps])) let declare_implicits local ref = - let flags = { !implicit_args with main = true } in + let flags = { !implicit_args with auto = true } in let req = if local then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in - declare_implicits_gen req flags ref - + declare_implicits_gen req flags ref + let declare_var_implicits id = - if !implicit_args.main then - declare_implicits_gen ImplLocal !implicit_args (VarRef id) + let flags = !implicit_args in + declare_implicits_gen ImplLocal flags (VarRef id) let declare_constant_implicits con = - if !implicit_args.main then - let flags = !implicit_args in + let flags = !implicit_args in declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con) let declare_mib_implicits kn = - if !implicit_args.main then - let flags = !implicit_args in - let imps = array_map_to_list - (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) - (compute_mib_implicits flags [] kn) in + let flags = !implicit_args in + let imps = array_map_to_list + (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) + (compute_mib_implicits flags [] kn) in add_anonymous_leaf (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps)) - + (* Declare manual implicits *) type manual_explicitation = Topconstr.explicitation * (bool * bool) - + let compute_implicits_with_manual env typ enriching l = compute_manual_implicits env !implicit_args typ enriching l @@ -582,7 +572,7 @@ let declare_manual_implicits local ref ?enriching l = let flags = !implicit_args in let env = Global.env () in let t = Global.type_of_global ref in - let enriching = Option.default (is_auto_implicit_args ()) enriching in + let enriching = Option.default flags.auto enriching in let l' = compute_manual_implicits env flags t enriching l in let req = if local or isVarRef ref then ImplLocal diff --git a/library/impargs.mli b/library/impargs.mli index a363effa..c1f119e6 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: impargs.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) +(*i $Id: impargs.mli 12187 2009-06-13 19:36:59Z msozeau $ i*) (*i*) open Names @@ -20,7 +20,6 @@ open Nametab are outside the kernel, which knows nothing about implicit arguments. *) val make_implicit_args : bool -> unit -val make_manual_implicit_args : bool -> unit val make_strict_implicit_args : bool -> unit val make_strongly_strict_implicit_args : bool -> unit val make_reversible_pattern_implicit_args : bool -> unit @@ -28,7 +27,6 @@ val make_contextual_implicit_args : bool -> unit val make_maximal_implicit_args : bool -> unit val is_implicit_args : unit -> bool -val is_manual_implicit_args : unit -> bool val is_strict_implicit_args : unit -> bool val is_strongly_strict_implicit_args : unit -> bool val is_reversible_pattern_implicit_args : unit -> bool diff --git a/library/lib.ml b/library/lib.ml index 88bcd0b8..4a124cec 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml 11784 2009-01-14 11:36:32Z herbelin $ *) +(* $Id: lib.ml 12187 2009-06-13 19:36:59Z msozeau $ *) open Pp open Util @@ -452,7 +452,7 @@ type variable_context = variable_info list type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t let sectab = - ref ([] : ((Names.identifier * binding_kind * Term.types option) list * Cooking.work_list * abstr_list) list) + ref ([] : ((Names.identifier * binding_kind * (Term.types * Names.identifier list) option) list * Cooking.work_list * abstr_list) list) let add_section () = sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab @@ -460,13 +460,19 @@ let add_section () = let add_section_variable id impl keep = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) - | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl + | (vars,repl,abs)::sl -> + sectab := ((id,impl,keep)::vars,repl,abs)::sl -let rec extract_hyps = function - | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: extract_hyps (idl,hyps) - | ((id,impl,Some ty)::idl,hyps) -> (id,impl,None,ty) :: extract_hyps (idl,hyps) - | (id::idl,hyps) -> extract_hyps (idl,hyps) - | [], _ -> [] +let extract_hyps (secs,ohyps) = + let rec aux = function + | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: aux (idl,hyps) + | ((id,impl,Some (ty,keep))::idl,hyps) -> + if List.exists (fun (id,_,_) -> List.mem id keep) ohyps then + (id,impl,None,ty) :: aux (idl,hyps) + else aux (idl,hyps) + | (id::idl,hyps) -> aux (idl,hyps) + | [], _ -> [] + in aux (secs,ohyps) let instance_from_variable_context sign = let rec inst_rec = function diff --git a/library/lib.mli b/library/lib.mli index 23af7c17..dacfed59 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lib.mli 11671 2008-12-12 12:43:03Z herbelin $ i*) +(*i $Id: lib.mli 12187 2009-06-13 19:36:59Z msozeau $ i*) (*s This module provides a general mechanism to keep a trace of all operations @@ -182,7 +182,9 @@ val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_cont val section_instance : Libnames.global_reference -> Names.identifier array val is_in_section : Libnames.global_reference -> bool -val add_section_variable : Names.identifier -> binding_kind -> Term.types option -> unit +val add_section_variable : Names.identifier -> binding_kind -> + (Term.types * Names.identifier list) option -> unit + val add_section_constant : Names.constant -> Sign.named_context -> unit val add_section_kn : Names.kernel_name -> Sign.named_context -> unit val replacement_context : unit -> diff --git a/library/states.ml b/library/states.ml index 7f7fef47..c81f9614 100644 --- a/library/states.ml +++ b/library/states.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: states.ml 11313 2008-08-07 11:15:03Z barras $ *) +(* $Id: states.ml 12080 2009-04-11 16:56:20Z herbelin $ *) open System @@ -35,3 +35,10 @@ let with_heavy_rollback f x = f x with reraise -> (unfreeze st; raise reraise) + +let with_state_protection f x = + let st = freeze () in + try + let a = f x in unfreeze st; a + with reraise -> + (unfreeze st; raise reraise) diff --git a/library/states.mli b/library/states.mli index eff046ef..210e06b2 100644 --- a/library/states.mli +++ b/library/states.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: states.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: states.mli 12080 2009-04-11 16:56:20Z herbelin $ i*) (*s States of the system. In that module, we provide functions to get and set the state of the whole system. Internally, it is done by @@ -26,4 +26,9 @@ val unfreeze : state -> unit val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b +(*s [with_state_protection f x] applies [f] to [x] and restores the + state of the whole system as it was before the evaluation of f *) + +val with_state_protection : ('a -> 'b) -> 'a -> 'b + -- cgit v1.2.3