diff options
| -rw-r--r-- | CHANGES | 8 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 8 | ||||
| -rw-r--r-- | interp/notation.ml | 44 | ||||
| -rw-r--r-- | interp/notation.mli | 4 | ||||
| -rw-r--r-- | library/declare.ml | 60 | ||||
| -rw-r--r-- | library/dischargedhypsmap.ml | 14 | ||||
| -rw-r--r-- | library/impargs.ml | 299 | ||||
| -rw-r--r-- | library/impargs.mli | 11 | ||||
| -rw-r--r-- | library/lib.ml | 76 | ||||
| -rw-r--r-- | library/lib.mli | 6 | ||||
| -rw-r--r-- | library/libnames.ml | 15 | ||||
| -rw-r--r-- | library/libnames.mli | 6 | ||||
| -rw-r--r-- | library/libobject.ml | 10 | ||||
| -rw-r--r-- | library/libobject.mli | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 19 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 12 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 16 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 5 |
18 files changed, 332 insertions, 283 deletions
@@ -1,4 +1,10 @@ -Changes from V8.1beta to V8.1beta2 +Changes from V8.1gamma to ... +============================= + +- Added option Global to "Implicit Arguments" and "Arguments Scope" for + section surviving + +Changes from V8.1beta to V8.1gamma ================================== Syntax diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 1d710ed3d..601952292 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1979,7 +1979,7 @@ let rec xlate_vernac = | VernacOpenCloseScope(false, true, s) -> CT_open_scope(CT_ident s) | VernacOpenCloseScope(true, false, s) -> CT_local_close_scope(CT_ident s) | VernacOpenCloseScope(false, false, s) -> CT_close_scope(CT_ident s) - | VernacArgumentsScope(qid, l) -> + | VernacArgumentsScope(true, qid, l) -> CT_arguments_scope(loc_qualid_to_ct_ID qid, CT_id_opt_list (List.map @@ -1987,6 +1987,8 @@ let rec xlate_vernac = match x with None -> ctv_ID_OPT_NONE | Some x -> ctf_ID_OPT_SOME(CT_ident x)) l)) + | VernacArgumentsScope(false, qid, l) -> + xlate_error "TODO: Arguments Scope Global" | VernacDelimiters(s1,s2) -> CT_delim_scope(CT_ident s1, CT_ident s2) | VernacBindScope(id, a::l) -> let xlate_class_rawexpr = function @@ -2061,7 +2063,7 @@ let rec xlate_vernac = | VernacNop -> CT_proof_no_op | VernacComments l -> CT_scomments(CT_scomment_content_list (List.map xlate_comment l)) - | VernacDeclareImplicits(id, opt_positions) -> + | VernacDeclareImplicits(true, id, opt_positions) -> CT_implicits (reference_to_ct_ID id, match opt_positions with @@ -2074,6 +2076,8 @@ let rec xlate_vernac = -> xlate_error "explication argument by rank is obsolete" | ExplByName id -> CT_ident (string_of_id id)) l))) + | VernacDeclareImplicits(false, id, opt_positions) -> + xlate_error "TODO: Implicit Arguments Global" | VernacReserve((_,a)::l, f) -> CT_reserve(CT_id_ne_list(xlate_ident a, List.map (fun (_,x) -> xlate_ident x) l), diff --git a/interp/notation.ml b/interp/notation.ml index 3a162ce7e..d0734b3d8 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -446,19 +446,37 @@ let rec compute_arguments_scope t = let arguments_scope = ref Refmap.empty -let load_arguments_scope _ (_,(r,scl)) = +type arguments_scope_request = + | ArgsScopeAuto + | ArgsScopeManual of bool + +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 subst_arguments_scope (_,subst,(req,r,scl)) = + (None,fst (subst_global subst r),scl) + +let discharge_arguments_scope (_,(req,r,l)) = + match req,r with + | _, VarRef _ -> None + | Some (ArgsScopeManual true),_ -> None + | _ -> Some (req,pop_global_reference r,l) + +let rebuild_arguments_scope (req,r,l) = + match req with + | None | Some (ArgsScopeManual true) -> assert false + | Some ArgsScopeAuto -> + (req,r,compute_arguments_scope (Global.type_of_global r)) + | Some (ArgsScopeManual false) -> + (* Add to the manually given scopes the one found automatically + for the extra parameters of the section *) + let l' = compute_arguments_scope (Global.type_of_global r) in + let l1,_ = list_chop (List.length l' - List.length l) l' in + (req,r,l1@l) let (inArgumentsScope,outArgumentsScope) = declare_object {(default_object "ARGUMENTS-SCOPE") with @@ -466,10 +484,15 @@ let (inArgumentsScope,outArgumentsScope) = load_function = load_arguments_scope; subst_function = subst_arguments_scope; classify_function = (fun (_,o) -> Substitute o); + discharge_function = discharge_arguments_scope; + rebuild_function = rebuild_arguments_scope; export_function = (fun x -> Some x) } -let declare_arguments_scope r scl = - Lib.add_anonymous_leaf (inArgumentsScope (r,scl)) +let declare_arguments_scope_gen req r scl = + Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl)) + +let declare_arguments_scope local r scl = + declare_arguments_scope_gen (Some (ArgsScopeManual local)) r scl let find_arguments_scope r = try Refmap.find r !arguments_scope @@ -477,7 +500,8 @@ let find_arguments_scope r = let declare_ref_arguments_scope ref = let t = Global.type_of_global ref in - declare_arguments_scope ref (compute_arguments_scope t) + declare_arguments_scope_gen (Some ArgsScopeAuto) ref + (compute_arguments_scope t) (********************************) (* Encoding notations as string *) diff --git a/interp/notation.mli b/interp/notation.mli index 9822905c2..776db1a50 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -135,7 +135,9 @@ val exists_notation_in_scope : scope_name option -> notation -> interpretation -> bool (* Declares and looks for scopes associated to arguments of a global ref *) -val declare_arguments_scope: global_reference -> scope_name option list -> unit +val declare_arguments_scope : + bool (* true=local *) -> global_reference -> scope_name option list -> unit + val find_arguments_scope : global_reference -> scope_name option list val declare_class_scope : scope_name -> Classops.cl_typ -> unit diff --git a/library/declare.ml b/library/declare.ml index 446e42d3c..f729f133d 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -136,7 +136,7 @@ let _ = Summary.declare_summary "CONSTANT" (* 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)) = +let load_constant i ((sp,kn),(_,_,kind)) = if Nametab.exists_cci sp then errorlabstrm "cache_constant" (pr_id (basename sp) ++ str " already exists"); @@ -147,21 +147,17 @@ let load_constant i ((sp,kn),(_,_,_,kind)) = 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)) = +let cache_constant ((sp,kn),(cdt,dhyps,kind)) = 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 + if Idmap.mem id !vartab or 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; + csttab := Spmap.add sp kind !csttab (*s Registration as global tables and rollback. *) @@ -172,18 +168,18 @@ let discharged_hyps kn sechyps = 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 discharge_constant ((sp,kn),(cdt,dhyps,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 repl = replacement_context () in + let sechyps = section_segment_of_constant con in let recipe = { d_from=cb; d_modlist=repl; d_abstract=sechyps } in - Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,imps,kind) + Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,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,_,imps,mk) = dummy_constant_entry,[],imps,mk +let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk let export_constant cst = Some (dummy_constant cst) @@ -210,9 +206,10 @@ let hcons_constant_declaration = function | cd -> cd let declare_constant_common id dhyps (cd,kind) = - let imps = implicits_flags () in - let (sp,kn) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in + let (sp,kn) = add_leaf id (in_constant (cd,dhyps,kind)) in let kn = constant_of_kn kn in + declare_constant_implicits kn; + Notation.declare_ref_arguments_scope (ConstRef kn); kn let declare_constant_gen internal id (cd,kind) = @@ -261,16 +258,16 @@ let check_exists_inductive (sp,_) = let (_,id) = repr_path sp in 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 (Nametab.Exactly i) sp ref) names -let cache_inductive ((sp,kn),(dhyps,imps,mie)) = +let cache_inductive ((sp,kn),(dhyps,mie)) = let names = inductive_names sp kn mie in List.iter check_exists_inductive names; let id = basename sp in @@ -279,15 +276,13 @@ let cache_inductive ((sp,kn),(dhyps,imps,mie)) = 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 discharge_inductive ((sp,kn),(dhyps,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, + let sechyps = section_segment_of_mutual_inductive kn in + Some (discharged_hyps kn sechyps, Discharge.process_inductive sechyps repl mie) let dummy_one_inductive_entry mie = { @@ -298,7 +293,7 @@ let dummy_one_inductive_entry mie = { } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_inductive_entry (_,imps,m) = ([],imps,{ +let dummy_inductive_entry (_,m) = ([],{ mind_entry_params = []; mind_entry_record = false; mind_entry_finite = true; @@ -318,11 +313,12 @@ let (in_inductive, out_inductive) = (* for initial declaration *) let declare_mind isrecord mie = - 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 + let (sp,kn as oname) = add_leaf id (in_inductive ([],mie)) in + declare_mib_implicits kn; + declare_inductive_argument_scopes kn mie; !xml_declare_inductive (isrecord,oname); oname diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index 0e7bdef30..2a2e69e91 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -24,21 +24,9 @@ type discharged_hyps = section_path list let discharged_hyps_map = ref Spmap.empty -let load_discharged_hyps_map _ (_,(sp,hyps)) = +let set_discharged_hyps 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 = load_discharged_hyps_map; - export_function = (fun x -> Some x) } - -let set_discharged_hyps sp hyps = - add_anonymous_leaf (in_discharged_hyps_map (sp,hyps)) - let get_discharged_hyps sp = try Spmap.find sp !discharged_hyps_map diff --git a/library/impargs.ml b/library/impargs.ml index 1dcbcead8..296e53310 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -45,7 +45,7 @@ let is_contextual_implicit_args () = !contextual_implicit_args type implicits_flags = bool * bool * bool -let implicits_flags () = +let implicit_flags () = (!implicit_args, !strict_implicit_args, !contextual_implicit_args) let with_implicits (a,b,c) f x = @@ -167,12 +167,6 @@ let add_free_rels_until strict bound env m pos acc = (* calcule la liste des arguments implicites *) -let my_concrete_name avoid names t = function - | Anonymous -> Anonymous, avoid, Anonymous::names - | na -> - let id = Termops.next_name_not_occuring None na avoid names t in - Name id, id::avoid, Name id::names - let compute_implicits_gen strict contextual env t = let rec aux env avoid n names t = let t = whd_betadeltaiota env t in @@ -194,15 +188,50 @@ let compute_implicits_gen strict contextual env t = Array.to_list v | _ -> [] -let compute_implicits env t = - let strict = !strict_implicit_args in - let contextual = !contextual_implicit_args in +let compute_implicits_auto env (_,strict,contextual) t = let l = compute_implicits_gen strict contextual env t in List.map (function | (Name id, Some imp) -> Some (id,imp) | (Anonymous, Some _) -> anomaly "Unnamed implicit" | _ -> None) l +let compute_implicits env t = compute_implicits_auto env (implicit_flags()) t + +let set_implicit id imp = + Some (id,match imp with None -> Manual | Some imp -> imp) + +let compute_manual_implicits flags ref l = + let t = Global.type_of_global ref in + let autoimps = compute_implicits_gen false true (Global.env()) t in + let n = List.length autoimps in + if not (list_distinct l) then + error ("Some parameters are referred more than once"); + (* Compare with automatic implicits to recover printing data and names *) + let rec merge k l = function + | (Name id,imp)::imps -> + let l',imp = + try list_remove_first (ExplByPos k) l, set_implicit id imp + with Not_found -> + try list_remove_first (ExplByName id) l, set_implicit id imp + with Not_found -> + l, None in + imp :: merge (k+1) l' imps + | (Anonymous,imp)::imps -> + None :: merge (k+1) l imps + | [] when l = [] -> [] + | _ -> + match List.hd l with + | ExplByName id -> + error ("Wrong or not dependent implicit argument name: "^(string_of_id id)) + | ExplByPos i -> + if i<1 or i>n then + error ("Bad implicit argument number: "^(string_of_int i)) + else + errorlabstrm "" + (str "Cannot set implicit argument number " ++ int i ++ + str ": it has no name") in + merge 1 l autoimps + type implicit_status = (* None = Not implicit *) (identifier * implicit_explanation) option @@ -238,44 +267,18 @@ let positions_of_implicits = type strict_flag = bool (* true = strict *) type contextual_flag = bool (* true = contextual *) -type implicits = - | Impl_auto of strict_flag * contextual_flag * implicits_list - | Impl_manual of implicits_list - | No_impl - -let auto_implicits env ty = - if !implicit_args then - let l = compute_implicits env ty in - Impl_auto (!strict_implicit_args,!contextual_implicit_args,l) - else - No_impl - -let list_of_implicits = function - | Impl_auto (_,_,l) -> l - | Impl_manual l -> l - | No_impl -> [] - (*s Constants. *) -let constants_table = ref Cmap.empty - -let compute_constant_implicits cst = +let compute_constant_implicits flags cst = let env = Global.env () in - auto_implicits env (Typeops.type_of_constant env cst) - -let constant_implicits sp = - try Cmap.find sp !constants_table with Not_found -> No_impl + compute_implicits_auto env flags (Typeops.type_of_constant env cst) (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where $i$ are the implicit arguments of the inductive and $v$ the array of implicit arguments of the constructors. *) -let inductives_table = ref Indmap.empty - -let constructors_table = ref Constrmap.empty - -let compute_mib_implicits kn = +let compute_mib_implicits flags kn = let env = Global.env () in let mib = lookup_mind kn env in let ar = @@ -288,54 +291,55 @@ let compute_mib_implicits kn = let imps_one_inductive i mip = let ind = (kn,i) in let ar = type_of_inductive env (mib,mip) in - ((IndRef ind,auto_implicits env ar), - Array.mapi (fun j c -> (ConstructRef (ind,j+1),auto_implicits env_ar c)) + ((IndRef ind,compute_implicits_auto env flags ar), + Array.mapi (fun j c -> + (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags c)) mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets -let inductive_implicits indp = - try Indmap.find indp !inductives_table with Not_found -> No_impl - -let constructor_implicits consp = - try Constrmap.find consp !constructors_table with Not_found -> No_impl +let compute_all_mib_implicits flags kn = + let imps = compute_mib_implicits flags kn in + List.flatten + (array_map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps) (*s Variables. *) -let var_table = ref Idmap.empty - -let compute_var_implicits id = +let compute_var_implicits flags id = let env = Global.env () in let (_,_,ty) = lookup_named id env in - auto_implicits env ty - -let var_implicits id = - try Idmap.find id !var_table with Not_found -> No_impl + compute_implicits_auto env flags ty (* Implicits of a global reference. *) -let compute_global_implicits = function - | VarRef id -> compute_var_implicits id - | ConstRef kn -> compute_constant_implicits kn +let compute_global_implicits flags = function + | VarRef id -> compute_var_implicits flags id + | ConstRef kn -> compute_constant_implicits flags kn | IndRef (kn,i) -> - let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps + let ((_,imps),_) = (compute_mib_implicits flags kn).(i) in imps | ConstructRef ((kn,i),j) -> - let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1) + let (_,cimps) = (compute_mib_implicits flags kn).(i) in snd cimps.(j-1) (* Caching implicits *) -let cache_implicits_decl (r,imps) = - match r with - | VarRef id -> - var_table := Idmap.add id imps !var_table - | ConstRef kn -> - constants_table := Cmap.add kn imps !constants_table - | IndRef indp -> - inductives_table := Indmap.add indp imps !inductives_table; - | ConstructRef consp -> - constructors_table := Constrmap.add consp imps !constructors_table +type implicit_interactive_request = ImplAuto | ImplManual of explicitation list + +type implicit_discharge_request = + | ImplNoDischarge + | ImplConstant of constant * implicits_flags + | ImplMutualInductive of kernel_name * implicits_flags + | ImplInteractive of global_reference * implicits_flags * + implicit_interactive_request -let load_implicits _ (_,l) = List.iter cache_implicits_decl l +let implicits_table = ref Refmap.empty + +let implicits_of_global ref = + try Refmap.find ref !implicits_table with Not_found -> [] + +let cache_implicits_decl (ref,imps) = + implicits_table := Refmap.add ref imps !implicits_table + +let load_implicits _ (_,(_,l)) = List.iter cache_implicits_decl l let cache_implicits o = load_implicits 1 o @@ -343,121 +347,88 @@ let cache_implicits o = 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) -let subst_implicits (_,subst,l) = - list_smartmap (subst_implicits_decl subst) l - -let (in_implicits, _) = +let subst_implicits (_,subst,(req,l)) = + (ImplNoDischarge,list_smartmap (subst_implicits_decl subst) l) + +let discharge_implicits (_,(req,l)) = + match req with + | ImplNoDischarge -> None + | ImplInteractive (ref,flags,exp) -> + Some (ImplInteractive (pop_global_reference ref,flags,exp),l) + | ImplConstant (con,flags) -> + Some (ImplConstant (pop_con con,flags),l) + | ImplMutualInductive (kn,flags) -> + Some (ImplMutualInductive (pop_kn kn,flags),l) + +let rebuild_implicits (req,l) = + let l' = match req with + | ImplNoDischarge -> assert false + | ImplConstant (con,flags) -> + [ConstRef con,compute_constant_implicits flags con] + | ImplMutualInductive (kn,flags) -> + compute_all_mib_implicits flags kn + | ImplInteractive (ref,flags,o) -> + match o with + | ImplAuto -> [ref,compute_global_implicits flags ref] + | ImplManual l -> + error "Discharge of global manually given implicit arguments not implemented" in + (req,l') + + +let (inImplicits, _) = declare_object {(default_object "IMPLICITS") with cache_function = cache_implicits; load_function = load_implicits; subst_function = subst_implicits; classify_function = (fun (_,x) -> Substitute x); + discharge_function = discharge_implicits; + rebuild_function = rebuild_implicits; export_function = (fun x -> Some x) } -let declare_implicits_gen r = - add_anonymous_leaf (in_implicits [r,compute_global_implicits r]) +let declare_implicits_gen req flags ref = + let imps = compute_global_implicits flags ref in + add_anonymous_leaf (inImplicits (req,[ref,imps])) -let declare_implicits r = - with_implicits - (true,!strict_implicit_args,!contextual_implicit_args) - declare_implicits_gen r +let declare_implicits local ref = + let flags = (true,!strict_implicit_args,!contextual_implicit_args) in + let req = + if local then ImplNoDischarge else ImplInteractive(ref,flags,ImplAuto) in + declare_implicits_gen req flags ref let declare_var_implicits id = - if !implicit_args then declare_implicits_gen (VarRef id) + if !implicit_args then + declare_implicits_gen ImplNoDischarge (implicit_flags ()) (VarRef id) -let declare_constant_implicits kn = - if !implicit_args then declare_implicits_gen (ConstRef kn) +let declare_constant_implicits con = + if !implicit_args then + let flags = implicit_flags () in + declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con) let declare_mib_implicits kn = if !implicit_args then - let imps = compute_mib_implicits kn in - let imps = array_map_to_list - (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) imps in - add_anonymous_leaf (in_implicits (List.flatten imps)) - -let implicits_of_global_gen = function - | VarRef id -> var_implicits id - | ConstRef sp -> constant_implicits sp - | IndRef isp -> inductive_implicits isp - | ConstructRef csp -> constructor_implicits csp - -let implicits_of_global r = - list_of_implicits (implicits_of_global_gen r) + let flags = implicit_flags () 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 *) -let set_implicit id imp = - Some (id,match imp with None -> Manual | Some imp -> imp) - -let declare_manual_implicits r l = - let t = Global.type_of_global r in - let autoimps = compute_implicits_gen false true (Global.env()) t in - let n = List.length autoimps in - if not (list_distinct l) then - error ("Some parameters are referred more than once"); - (* Compare with automatic implicits to recover printing data and names *) - let rec merge k l = function - | (Name id,imp)::imps -> - let l',imp = - try list_remove_first (ExplByPos k) l, set_implicit id imp - with Not_found -> - try list_remove_first (ExplByName id) l, set_implicit id imp - with Not_found -> - l, None in - imp :: merge (k+1) l' imps - | (Anonymous,imp)::imps -> - None :: merge (k+1) l imps - | [] when l = [] -> [] - | _ -> - match List.hd l with - | ExplByName id -> - error ("Wrong or not dependent implicit argument name: "^(string_of_id id)) - | ExplByPos i -> - if i<1 or i>n then - error ("Bad implicit argument number: "^(string_of_int i)) - else - errorlabstrm "" - (str "Cannot set implicit argument number " ++ int i ++ - str ": it has no name") in - let l = Impl_manual (merge 1 l autoimps) in - add_anonymous_leaf (in_implicits [r,l]) - -(* Tests if declared implicit *) - -let test = function - | No_impl | Impl_manual _ -> false,false,false - | Impl_auto (s,c,_) -> true,s,c - -let test_if_implicit find a = - try let b = find a in test b - with Not_found -> (false,false,false) - -let is_implicit_constant sp = - test_if_implicit (Cmap.find sp) !constants_table - -let is_implicit_inductive_definition indp = - test_if_implicit (Indmap.find (indp,0)) !inductives_table - -let is_implicit_var id = - test_if_implicit (Idmap.find id) !var_table +let declare_manual_implicits local ref l = + let flags = !implicit_args,!strict_implicit_args,!contextual_implicit_args in + let l' = compute_manual_implicits flags ref l in + let local = local or (match ref with VarRef _ -> true | _ -> false) in + let req = + if local then ImplNoDischarge else ImplInteractive(ref,flags,ImplManual l) + in + add_anonymous_leaf (inImplicits (req,[ref,l'])) (*s Registration as global tables *) -let init () = - constants_table := Cmap.empty; - inductives_table := Indmap.empty; - constructors_table := Constrmap.empty; - var_table := Idmap.empty - -let freeze () = - (!constants_table, !inductives_table, - !constructors_table, !var_table) - -let unfreeze (ct,it,const,vt) = - constants_table := ct; - inductives_table := it; - constructors_table := const; - var_table := vt +let init () = implicits_table := Refmap.empty +let freeze () = !implicits_table +let unfreeze t = implicits_table := t let _ = Summary.declare_summary "implicits" diff --git a/library/impargs.mli b/library/impargs.mli index 23ed327ba..615861043 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -51,17 +51,10 @@ val declare_var_implicits : variable -> unit val declare_constant_implicits : constant -> unit val declare_mib_implicits : mutual_inductive -> unit -val declare_implicits : global_reference -> unit +val declare_implicits : bool -> global_reference -> unit (* Manual declaration of which arguments are expected implicit *) -val declare_manual_implicits : global_reference -> +val declare_manual_implicits : bool -> global_reference -> Topconstr.explicitation list -> unit -(* Get implicit arguments *) -val is_implicit_constant : constant -> implicits_flags -val is_implicit_inductive_definition : mutual_inductive -> implicits_flags -val is_implicit_var : variable -> implicits_flags - val implicits_of_global : global_reference -> implicits_list - -val implicits_flags : unit -> implicits_flags diff --git a/library/lib.ml b/library/lib.ml index ac710c357..4c822114e 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -188,9 +188,15 @@ let add_leaf id obj = if fst (current_prefix ()) = initial_path then error ("No session module started (use -top dir)"); let oname = make_oname id in - cache_object (oname,obj); - add_entry oname (Leaf obj); - oname + cache_object (oname,obj); + add_entry oname (Leaf obj); + oname + +let add_discharged_leaf id obj = + let oname = make_oname id in + let newobj = rebuild_object obj in + cache_object (oname,newobj); + add_entry oname (Leaf newobj) let add_leaves id objs = let oname = make_oname id in @@ -373,10 +379,17 @@ let what_is_opened () = find_entry_p is_something_opened (* Discharge tables *) +(* At each level of section, we remember + - the list of variables in this section + - the list of variables on which each constant depends in this section + - the list of variables on which each inductive depends in this section + - the list of substitution to do at section closing +*) + +type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t + let sectab = - ref ([] : (identifier list * - (identifier array Cmap.t * identifier array KNmap.t) * - (Sign.named_context Cmap.t * Sign.named_context KNmap.t)) list) + ref ([] : (identifier list * Cooking.work_list * abstr_list) list) let add_section () = sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab @@ -409,16 +422,18 @@ let add_section_constant kn = 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_segment_of_constant con = + Cmap.find con (fst (pi3 (List.hd !sectab))) + +let section_segment_of_mutual_inductive kn = + KNmap.find kn (snd (pi3 (List.hd !sectab))) -let section_instance r = - Sign.instance_from_named_context (List.rev (section_segment r)) +let section_instance = function + | VarRef id -> [||] + | ConstRef con -> + Cmap.find con (fst (pi2 (List.hd !sectab))) + | IndRef (kn,_) | ConstructRef ((kn,_),_) -> + KNmap.find kn (snd (pi2 (List.hd !sectab))) let init () = sectab := [] let freeze () = !sectab @@ -461,11 +476,14 @@ let open_section id = (* Restore lib_stk and summaries as before the section opening, and add a ClosedSection object. *) -let discharge_item = function - | ((sp,_ as oname),Leaf lobj) -> +let discharge_item ((sp,_ as oname),e) = + match e with + | Leaf lobj -> option_map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) - | _ -> - None + | FrozenState _ -> None + | ClosedSection -> None + | OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ -> + anomaly "discharge_item" let close_section id = let oname,fs = @@ -479,16 +497,16 @@ let close_section id = error "no opened section" in let (secdecls,_,before) = split_lib oname in - lib_stk := before; - let full_olddir = fst !path_prefix in - pop_path_prefix (); - add_entry (make_oname id) ClosedSection; - if !Options.xml_export then !xml_close_section id; - 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) + lib_stk := before; + let full_olddir = fst !path_prefix in + pop_path_prefix (); + add_entry (make_oname id) ClosedSection; + if !Options.xml_export then !xml_close_section id; + let newdecls = List.map discharge_item secdecls in + Summary.section_unfreeze_summaries fs; + List.iter (option_iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; + Cooking.clear_cooking_sharing (); + Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) (*****************) (* Backtracking. *) diff --git a/library/lib.mli b/library/lib.mli index 5639ffed7..9f5a3f78a 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -166,8 +166,10 @@ 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 section_segment_of_constant : constant -> Sign.named_context +val section_segment_of_mutual_inductive: mutual_inductive -> Sign.named_context + +val section_instance : global_reference -> identifier array val add_section_variable : identifier -> unit val add_section_constant : constant -> Sign.named_context -> unit diff --git a/library/libnames.ml b/library/libnames.ml index 424cf1f73..d951b616e 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -264,3 +264,18 @@ let loc_of_reference = function | Qualid (loc,qid) -> loc | Ident (loc,id) -> loc +(* popping one level of section in global names *) + +let pop_con con = + let (mp,dir,l) = repr_con con in + Names.make_con mp (dirpath_prefix dir) l + +let pop_kn kn = + let (mp,dir,l) = repr_kn kn in + Names.make_kn mp (dirpath_prefix dir) l + +let pop_global_reference = function + | ConstRef con -> ConstRef (pop_con con) + | IndRef (kn,i) -> IndRef (pop_kn kn,i) + | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j) + | VarRef id -> anomaly "VarRef not poppable" diff --git a/library/libnames.mli b/library/libnames.mli index 69710f431..2d5d5258f 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -141,3 +141,9 @@ val qualid_of_reference : reference -> qualid located val string_of_reference : reference -> string val pr_reference : reference -> std_ppcmds val loc_of_reference : reference -> loc + +(* popping one level of section in global names *) + +val pop_con : constant -> constant +val pop_kn : kernel_name -> kernel_name +val pop_global_reference : global_reference -> global_reference diff --git a/library/libobject.ml b/library/libobject.ml index 0a5379ee5..46cc55361 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -37,6 +37,7 @@ type 'a object_declaration = { classify_function : object_name * 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; + rebuild_function : 'a -> 'a; export_function : 'a -> 'a option } let yell s = anomaly s @@ -50,6 +51,7 @@ let default_object s = { yell ("The object "^s^" does not know how to substitute!")); classify_function = (fun (_,obj) -> Keep obj); discharge_function = (fun _ -> None); + rebuild_function = (fun x -> x); export_function = (fun _ -> None)} @@ -75,6 +77,7 @@ type dynamic_object_declaration = { 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_rebuild_function : obj -> obj; dyn_export_function : obj -> obj option } let object_tag lobj = Dyn.tag lobj @@ -112,6 +115,9 @@ let declare_object odecl = option_map infun (odecl.discharge_function (oname,outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the dischargefun" + and rebuild lobj = + if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj)) + else anomaly "somehow we got the wrong dynamic object in the rebuildfun" and exporter lobj = if Dyn.tag lobj = na then option_map infun (odecl.export_function (outfun lobj)) @@ -125,6 +131,7 @@ let declare_object odecl = dyn_subst_function = substituter; dyn_classify_function = classifier; dyn_discharge_function = discharge; + dyn_rebuild_function = rebuild; dyn_export_function = exporter }; (infun,outfun) @@ -166,5 +173,8 @@ let classify_object ((_,lobj) as node) = let discharge_object ((_,lobj) as node) = apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj +let rebuild_object lobj = + apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) 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 3d60e48ad..540b69feb 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -71,6 +71,7 @@ type 'a object_declaration = { classify_function : object_name * 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; + rebuild_function : 'a -> 'a; export_function : 'a -> 'a option } (* The default object is a "Keep" object with empty methods. @@ -105,4 +106,5 @@ 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 rebuild_object : obj -> obj val relax : bool -> unit diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 356c05e8f..d08a9b06c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -458,10 +458,14 @@ GEXTEND Gram VernacCoercion (Global, qid, s, t) (* Implicit *) - | IDENT "Implicit"; IDENT "Arguments"; qid = global; - pos = OPT [ "["; l = LIST0 ident; "]" -> l ] -> - let pos = option_map (List.map (fun id -> ExplByName id)) pos in - VernacDeclareImplicits (qid,pos) + | IDENT "Implicit"; IDENT "Arguments"; + (local,qid,pos) = + [ local = [ IDENT "Global" -> false | IDENT "Local" -> true ]; + qid = global -> (local,qid,None) + | qid = global; + l = OPT [ "["; l = LIST0 ident; "]" -> + List.map (fun id -> ExplByName id) l ] -> (true,qid,l) ] -> + VernacDeclareImplicits (local,qid,pos) | IDENT "Implicit"; ["Type" | IDENT "Types"]; idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ] @@ -712,8 +716,8 @@ GEXTEND Gram | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl) - | IDENT "Arguments"; IDENT "Scope"; qid = global; - "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl) + | IDENT "Arguments"; IDENT "Scope"; local = non_globality; qid = global; + "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (local,qid,scl) | IDENT "Infix"; local = locality; op = ne_string; ":="; p = global; @@ -746,6 +750,9 @@ GEXTEND Gram locality: [ [ IDENT "Local" -> true | -> false ] ] ; + non_globality: + [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> true ] ] + ; level: [ [ IDENT "level"; n = natural -> NumLevel n | IDENT "next"; IDENT "level" -> NextLevel ] ] diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 6213e4fda..e823a40d1 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -144,6 +144,7 @@ let pr_search a b pr_p = match a with | SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b let pr_locality local = if local then str "Local " else str "" +let pr_non_globality local = if local then str "" else str "Global " let pr_explanation imps = function | ExplByPos n -> pr_id (Impargs.name_of_implicit (List.nth imps (n-1))) @@ -447,10 +448,11 @@ let rec pr_vernac = function | VernacBindScope (sc,cll) -> str"Bind Scope" ++ spc () ++ str sc ++ spc() ++ str "with " ++ prlist_with_sep spc pr_class_rawexpr cll - | VernacArgumentsScope (q,scl) -> let pr_opt_scope = function + | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function | None -> str"_" | Some sc -> str sc in - str"Arguments Scope" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" + str"Arguments Scope" ++ spc() ++ pr_non_globality local ++ pr_reference q + ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" | VernacInfix (local,(s,mv),q,sn) -> (* A Verifier *) hov 0 (hov 0 (str"Infix " ++ pr_locality local ++ qs s ++ str " :=" ++ spc() ++ pr_reference q) ++ @@ -746,11 +748,11 @@ let rec pr_vernac = function (str"Notation " ++ pr_locality local ++ pr_id id ++ str" :=" ++ pr_constrarg c ++ pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) - | VernacDeclareImplicits (q,None) -> + | VernacDeclareImplicits (local,q,None) -> hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q) - | VernacDeclareImplicits (q,Some l) -> + | VernacDeclareImplicits (local,q,Some l) -> let r = Nametab.global q in - Impargs.declare_manual_implicits r l; + Impargs.declare_manual_implicits local r l; let imps = Impargs.implicits_of_global r in hov 1 (str"Implicit Arguments" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep (pr_explanation imps) l ++ str"]") diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 44e7cbad7..4c24f3505 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -284,8 +284,8 @@ let vernac_bind_scope sc cll = let vernac_open_close_scope = Notation.open_close_scope -let vernac_arguments_scope qid scl = - Notation.declare_arguments_scope (global qid) scl +let vernac_arguments_scope local qid scl = + Notation.declare_arguments_scope local (global qid) scl let vernac_infix = Metasyntax.add_infix @@ -666,9 +666,11 @@ let vernac_hints = Auto.add_hints let vernac_syntactic_definition = Command.syntax_definition -let vernac_declare_implicits locqid = function - | Some imps -> Impargs.declare_manual_implicits (Nametab.global locqid) imps - | None -> Impargs.declare_implicits (Nametab.global locqid) +let vernac_declare_implicits local locqid = function + | Some imps -> + Impargs.declare_manual_implicits local (Nametab.global locqid) imps + | None -> + Impargs.declare_implicits local (Nametab.global locqid) let vernac_reserve idl c = let t = Constrintern.interp_type Evd.empty (Global.env()) c in @@ -1122,7 +1124,7 @@ let interp c = match c with | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl | VernacOpenCloseScope sc -> vernac_open_close_scope sc - | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl + | VernacArgumentsScope (lcl,qid,scl) -> vernac_arguments_scope lcl qid scl | VernacInfix (local,mv,qid,sc) -> vernac_infix local mv qid sc | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc @@ -1193,7 +1195,7 @@ let interp c = match c with | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b - | VernacDeclareImplicits (qid,l) -> vernac_declare_implicits qid l + | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l | VernacReserve (idl,c) -> vernac_reserve idl c | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl | VernacSetOption (key,v) -> vernac_set_option key v diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index ffde10192..825e8d549 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -180,7 +180,7 @@ type vernac_expr = | VernacOpenCloseScope of (locality_flag * bool * scope_name) | VernacDelimiters of scope_name * lstring | VernacBindScope of scope_name * class_rawexpr list - | VernacArgumentsScope of lreference * scope_name option list + | VernacArgumentsScope of locality_flag * lreference * scope_name option list | VernacInfix of locality_flag * (lstring * syntax_modifier list) * lreference * scope_name option | VernacNotation of @@ -259,7 +259,8 @@ type vernac_expr = | VernacHints of locality_flag * lstring list * hints | VernacSyntacticDefinition of identifier * constr_expr * locality_flag * onlyparsing_flag - | VernacDeclareImplicits of lreference * explicitation list option + | VernacDeclareImplicits of locality_flag * lreference * + explicitation list option | VernacReserve of lident list * constr_expr | VernacSetOpacity of opacity_flag * lreference list | VernacUnsetOption of Goptions.option_name |