diff options
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | interp/notation.ml | 8 | ||||
| -rw-r--r-- | interp/topconstr.ml | 11 | ||||
| -rw-r--r-- | interp/topconstr.mli | 11 | ||||
| -rw-r--r-- | library/declaremods.ml | 106 | ||||
| -rw-r--r-- | library/declaremods.mli | 54 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 31 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 18 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 77 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 79 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Binary/NBinary.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 5 | ||||
| -rw-r--r-- | toplevel/command.mli | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
19 files changed, 234 insertions, 193 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 9403a4ccad..476e2111e8 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -90,6 +90,7 @@ Coercion Unification Cases Pretyping +Declaremods Tok Lexer diff --git a/interp/notation.ml b/interp/notation.ml index 86a5155374..6be016c180 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -435,7 +435,8 @@ open Classops let class_scope_map = ref (Gmap.empty : (cl_typ,scope_name) Gmap.t) -let _ = Gmap.add CL_SORT "type_scope" Gmap.empty +let _ = + class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty let declare_class_scope sc cl = class_scope_map := Gmap.add cl sc !class_scope_map @@ -479,7 +480,9 @@ let cache_arguments_scope o = load_arguments_scope 1 o let subst_arguments_scope (subst,(req,r,scl)) = - (ArgsScopeNoDischarge,fst (subst_global subst r),scl) + let r' = fst (subst_global subst r) in + let scl' = list_smartmap (Option.smartmap Declaremods.subst_scope) scl in + (ArgsScopeNoDischarge,r',scl') let discharge_arguments_scope (_,(req,r,l)) = if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None @@ -527,6 +530,7 @@ let declare_ref_arguments_scope ref = let t = Global.type_of_global ref in declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope t) + (********************************) (* Encoding notations as string *) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 81b4e8e94d..7539d8bd0b 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -1218,17 +1218,6 @@ type module_ast = | CMapply of module_ast * module_ast | CMwith of module_ast * with_declaration_ast -(* Which inline annotations should we honor, either None or the ones - whose level is less or equal to the given integer *) - -type inline = int option - -type module_ast_inl = module_ast * inline - -type 'a module_signature = - | Enforce of 'a (* ... : T *) - | Check of 'a list (* ... <: T1 <: T2, possibly empty *) - (* Returns the ranges of locs of the notation that are not occupied by args *) (* and which are then occupied by proper symbols of the notation (or spaces) *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index b7bac17bd0..fad1281a69 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -264,17 +264,6 @@ type module_ast = | CMapply of module_ast * module_ast | CMwith of module_ast * with_declaration_ast -(* Which inline annotations should we honor, either None or the ones - whose level is less or equal to the given integer *) - -type inline = int option - -type module_ast_inl = module_ast * inline - -type 'a module_signature = - | Enforce of 'a (** ... : T *) - | Check of 'a list (** ... <: T1 <: T2, possibly empty *) - val ntn_loc : Util.loc -> constr_notation_substitution -> string -> (int * int) list val patntn_loc : diff --git a/library/declaremods.ml b/library/declaremods.ml index b6b3a766fd..68d928aef0 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -17,8 +17,55 @@ open Lib open Nametab open Mod_subst -(* modules and components *) +(** Rigid / flexible signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Should we adapt a few scopes during functor application ? *) + +type scope_subst = (string * string) list + +let scope_subst = ref (Stringmap.empty : string Stringmap.t) + +let add_scope_subst sc sc' = + scope_subst := Stringmap.add sc sc' !scope_subst + +let register_scope_subst scl = + List.iter (fun (sc1,sc2) -> add_scope_subst sc1 sc2) scl + +let subst_scope sc = + try Stringmap.find sc !scope_subst with Not_found -> sc + +let reset_scope_subst () = + scope_subst := Stringmap.empty + +(** Which inline annotations should we honor, either None or the ones + whose level is less or equal to the given integer *) + +type inline = + | NoInline + | DefaultInline + | InlineAt of int + +let default_inline () = Some (Flags.get_inline_level ()) +let inl2intopt = function + | NoInline -> None + | InlineAt i -> Some i + | DefaultInline -> default_inline () + +type funct_app_annot = + { ann_inline : inline; + ann_scope_subst : scope_subst } + +let inline_annot a = inl2intopt a.ann_inline + +type 'a annotated = ('a * funct_app_annot) + + +(* modules and components *) (* OBSOLETE This type is a functional closure of substitutive lib_objects. @@ -78,7 +125,8 @@ let modtab_objects = let openmod_info = ref ((MPfile(initial_dir),[],None,[]) : module_path * mod_bound_id list * - (module_struct_entry * inline) option * module_type_body list) + (module_struct_entry * int option) option * + module_type_body list) (* The library_cache here is needed to avoid recalculations of substituted modules object during "reloading" of libraries *) @@ -152,7 +200,8 @@ let funct_entry args m = let build_subtypes interp_modtype mp args mtys = List.map - (fun (m,inl) -> + (fun (m,ann) -> + let inl = inline_annot ann in let mte = interp_modtype (Global.env()) m in let mtb = Mod_typing.translate_module_type (Global.env()) mp inl mte in let funct_mtb = @@ -465,18 +514,19 @@ let rec get_modtype_substobjs env mp_from inline = function (* push names of bound modules (and their components) to Nametab *) (* add objects associated to them *) let process_module_bindings argids args = - let process_arg id (mbid,(mty,inl)) = + let process_arg id (mbid,(mty,ann)) = let dir = make_dirpath [id] in let mp = MPbound mbid in let (mbids,mp_from,objs) = - get_modtype_substobjs (Global.env()) mp inl mty in + get_modtype_substobjs (Global.env()) mp (inline_annot ann) mty in let substobjs = (mbids,mp,subst_objects (map_mp mp_from mp empty_delta_resolver) objs)in do_module false "start" load_objects 1 dir mp substobjs [] in List.iter2 process_arg argids args -let intern_args interp_modtype (idl,(arg,inl)) = +let intern_args interp_modtype (idl,(arg,ann)) = + let inl = inline_annot ann in let lib_dir = Lib.library_dp() in let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in let mty = interp_modtype (Global.env()) arg in @@ -497,11 +547,12 @@ let start_module_ interp_modtype export id args res fs = let mp = Global.start_module id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let res_entry_o, sub_body_l = match res with - | Topconstr.Enforce (res,inl) -> + | Enforce (res,ann) -> + let inl = inline_annot ann in let mte = interp_modtype (Global.env()) res in let _ = Mod_typing.translate_struct_type_entry (Global.env()) inl mte in Some (mte,inl), [] - | Topconstr.Check resl -> + | Check resl -> None, build_subtypes interp_modtype mp arg_entries resl in let mbids = List.map fst arg_entries in @@ -691,7 +742,8 @@ let end_modtype () = mp -let declare_modtype_ interp_modtype id args mtys (mty,inl) fs = +let declare_modtype_ interp_modtype id args mtys (mty,ann) fs = + let inl = inline_annot ann in let mmp = Global.start_modtype id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let entry = funct_entry arg_entries (interp_modtype (Global.env()) mty) in @@ -701,9 +753,11 @@ let declare_modtype_ interp_modtype id args mtys (mty,inl) fs = (* Undo the simulated interactive building of the module type *) (* and declare the module type as a whole *) + register_scope_subst ann.ann_scope_subst; let substobjs = (mbids,mmp, subst_objects (map_mp mp_from mmp empty_delta_resolver) objs) in + reset_scope_subst (); Summary.unfreeze_summaries fs; ignore (add_leaf id (in_modtype (Some (entry,inl), substobjs, sub_mty_l))); mmp @@ -744,17 +798,20 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = let funct f m = funct_entry arg_entries (f (Global.env ()) m) in let env = Global.env() in - let default_inl = Some (Flags.get_inline_level ()) in (* PLTODO *) let mty_entry_o, subs, inl_res = match res with - | Topconstr.Enforce (mty,inl) -> Some (funct interp_modtype mty), [], inl - | Topconstr.Check mtys -> - None, build_subtypes interp_modtype mmp arg_entries mtys, default_inl + | Enforce (mty,ann) -> + Some (funct interp_modtype mty), [], inline_annot ann + | Check mtys -> + None, build_subtypes interp_modtype mmp arg_entries mtys, + default_inline () in (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in *) - let mexpr_entry_o, inl_expr = match mexpr_o with - | None -> None, default_inl - | Some (mexpr, inl) -> Some (funct interp_modexpr mexpr), inl + let mexpr_entry_o, inl_expr, scl = match mexpr_o with + | None -> None, default_inline (), [] + | Some (mexpr,ann) -> + Some (funct interp_modexpr mexpr), inline_annot ann, ann.ann_scope_subst + in let entry = {mod_entry_type = mty_entry_o; @@ -779,9 +836,10 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = check_subtypes mp subs; - + register_scope_subst scl; let substobjs = (mbids,mp_env, subst_objects(map_mp mp_from mp_env resolver) objs) in + reset_scope_subst (); ignore (add_leaf id (in_module (Some (entry), substobjs))); @@ -889,9 +947,13 @@ let get_includeself_substobjs env objs me is_mod inline = ([],mp_self,subst_objects subst objects) with NothingToDo -> objs -let declare_one_include_inner inl (me,is_mod) = + + + +let declare_one_include_inner annot (me,is_mod) = let env = Global.env() in let mp1,_ = current_prefix () in + let inl = inline_annot annot in let (mbids,mp,objs)= if is_mod then get_module_substobjs env mp1 inl me @@ -904,14 +966,16 @@ let declare_one_include_inner inl (me,is_mod) = (mbids,mp,objs) in let id = current_mod_id() in let resolver = Global.add_include me is_mod inl in + register_scope_subst annot.ann_scope_subst; let substobjs = (mbids,mp1, subst_objects (map_mp mp mp1 resolver) objs) in + reset_scope_subst (); ignore (add_leaf id (in_include ((me,is_mod), substobjs))) -let declare_one_include interp_struct me_ast = - declare_one_include_inner (snd me_ast) - (interp_struct (Global.env()) (fst me_ast)) +let declare_one_include interp_struct (me_ast,annot) = + declare_one_include_inner annot + (interp_struct (Global.env()) me_ast) let declare_include_ interp_struct me_asts = List.iter (declare_one_include interp_struct) me_asts diff --git a/library/declaremods.mli b/library/declaremods.mli index b1978c282e..21a7aeabef 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -17,6 +17,33 @@ open Lib (** This modules provides official functions to declare modules and module types *) +(** Rigid / flexible signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Should we adapt a few scopes during functor application ? *) + +type scope_subst = (string * string) list + +val subst_scope : string -> string + +(** Which inline annotations should we honor, either None or the ones + whose level is less or equal to the given integer *) + +type inline = + | NoInline + | DefaultInline + | InlineAt of int + +(** The type of annotations for functor applications *) + +type funct_app_annot = + { ann_inline : inline; + ann_scope_subst : scope_subst } + +type 'a annotated = ('a * funct_app_annot) (** {6 Modules } *) @@ -37,13 +64,14 @@ val declare_module : (env -> 'modast -> module_struct_entry) -> (env -> 'modast -> module_struct_entry * bool) -> identifier -> - (identifier located list * ('modast * inline)) list -> - ('modast * inline) Topconstr.module_signature -> - ('modast * inline) list -> module_path + (identifier located list * ('modast annotated)) list -> + ('modast annotated) module_signature -> + ('modast annotated) list -> module_path val start_module : (env -> 'modast -> module_struct_entry) -> - bool option -> identifier -> (identifier located list * ('modast * inline)) list -> - ('modast * inline) Topconstr.module_signature -> module_path + bool option -> identifier -> + (identifier located list * ('modast annotated)) list -> + ('modast annotated) module_signature -> module_path val end_module : unit -> module_path @@ -53,12 +81,15 @@ val end_module : unit -> module_path val declare_modtype : (env -> 'modast -> module_struct_entry) -> (env -> 'modast -> module_struct_entry * bool) -> - identifier -> (identifier located list * ('modast * inline)) list -> - ('modast * inline) list -> ('modast * inline) list -> module_path + identifier -> + (identifier located list * ('modast annotated)) list -> + ('modast annotated) list -> + ('modast annotated) list -> + module_path val start_modtype : (env -> 'modast -> module_struct_entry) -> - identifier -> (identifier located list * ('modast * inline)) list -> - ('modast * inline) list -> module_path + identifier -> (identifier located list * ('modast annotated)) list -> + ('modast annotated) list -> module_path val end_modtype : unit -> module_path @@ -103,7 +134,7 @@ val import_module : bool -> module_path -> unit (** Include *) val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) -> - ('struct_expr * inline) list -> unit + ('struct_expr annotated) list -> unit (** {6 ... } *) (** [iter_all_segments] iterate over all segments, the modules' @@ -120,5 +151,4 @@ val debug_print_modtab : unit -> Pp.std_ppcmds (** For translator *) val process_module_bindings : module_ident list -> - (mod_bound_id * (module_struct_entry * inline)) list -> unit - + (mod_bound_id * (module_struct_entry annotated)) list -> unit diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 0c7dbeeb03..e550cfa26a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -23,6 +23,7 @@ open Decl_kinds open Genarg open Ppextend open Goptions +open Declaremods open Prim open Constr @@ -444,15 +445,33 @@ GEXTEND Gram [ [ ":="; mexpr = module_expr_inl; l = LIST0 ext_module_expr -> (mexpr::l) | -> [] ] ] ; + functor_app_annot: + [ [ IDENT "inline"; "at"; IDENT "level"; i = INT -> + [InlineAt (int_of_string i)], [] + | IDENT "no"; IDENT "inline" -> [NoInline], [] + | IDENT "scope"; sc1 = IDENT; IDENT "to"; sc2 = IDENT -> [], [sc1,sc2] + ] ] + ; + functor_app_annots: + [ [ "["; l = LIST1 functor_app_annot SEP ","; "]" -> + let inl,scs = List.split l in + let inl = match List.concat inl with + | [] -> DefaultInline + | [inl] -> inl + | _ -> error "Functor application with redundant inline annotations" + in { ann_inline = inl; ann_scope_subst = List.concat scs } + | -> { ann_inline = DefaultInline; ann_scope_subst = [] } + ] ] + ; module_expr_inl: - [ [ "!"; me = module_expr -> (me,None) - | "<"; i = INT; ">"; me = module_expr -> (me,Some (int_of_string i)) - | me = module_expr -> (me,Some (Flags.get_inline_level())) ] ] + [ [ "!"; me = module_expr -> + (me, { ann_inline = NoInline; ann_scope_subst = []}) + | me = module_expr; a = functor_app_annots -> (me,a) ] ] ; module_type_inl: - [ [ "!"; me = module_type -> (me,None) - | "<"; i = INT; ">"; me = module_type -> (me,Some (int_of_string i)) - | me = module_type -> (me,Some (Flags.get_inline_level())) ] ] + [ [ "!"; me = module_type -> + (me, { ann_inline = NoInline; ann_scope_subst = []}) + | me = module_type; a = functor_app_annots -> (me,a) ] ] ; (* Module binder *) module_binder: diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 42007e4b06..bba1e1a8fb 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -24,6 +24,7 @@ open Ppextend open Topconstr open Decl_kinds open Tacinterp +open Declaremods let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr @@ -227,8 +228,21 @@ let rec pr_module_ast pr_c = function pr_module_ast pr_c me1 ++ spc() ++ hov 1 (str"(" ++ pr_module_ast pr_c me2 ++ str")") -let pr_module_ast_inl pr_c (mast,o) = - (if o=None then str "!" else mt ()) ++ pr_module_ast pr_c mast +let pr_annot { ann_inline = ann; ann_scope_subst = scl } = + let sep () = if scl=[] then mt () else str "," in + if ann = DefaultInline && scl = [] then mt () + else + str " [" ++ + (match ann with + | DefaultInline -> mt () + | NoInline -> str "no inline" ++ sep () + | InlineAt i -> str "inline at level " ++ int i ++ sep ()) ++ + prlist_with_sep (fun () -> str ", ") + (fun (sc1,sc2) -> str ("scope "^sc1^" to "^sc2)) scl ++ + str "]" + +let pr_module_ast_inl pr_c (mast,ann) = + pr_module_ast pr_c mast ++ pr_annot ann let pr_of_module_type prc = function | Enforce mty -> str ":" ++ pr_module_ast_inl prc mty diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 583491386d..9748a43666 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -24,65 +24,24 @@ Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake. *) +Delimit Scope bigZ_scope with bigZ. Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder := - ZMake.Make BigN <+ ZTypeIsZAxioms <+ !ZProp <+ HasEqBool2Dec - <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. + ZMake.Make BigN [scope abstract_scope to bigZ_scope] + <+ ZTypeIsZAxioms [scope abstract_scope to bigZ_scope] + <+ ZProp [no inline, scope abstract_scope to bigZ_scope] + <+ HasEqBool2Dec [no inline, scope abstract_scope to bigZ_scope] + <+ MinMaxLogicalProperties [no inline, scope abstract_scope to bigZ_scope] + <+ MinMaxDecProperties [no inline, scope abstract_scope to bigZ_scope]. (** Notations about [BigZ] *) -Notation bigZ := BigZ.t. +Local Open Scope bigZ_scope. -Delimit Scope bigZ_scope with bigZ. -Bind Scope bigZ_scope with bigZ. -Bind Scope bigZ_scope with BigZ.t. -Bind Scope bigZ_scope with BigZ.t_. -(* Bind Scope has no retroactive effect, let's declare scopes by hand. *) +Notation bigZ := BigZ.t. +Bind Scope bigZ_scope with bigZ BigZ.t BigZ.t_. Arguments Scope BigZ.Pos [bigN_scope]. Arguments Scope BigZ.Neg [bigN_scope]. -Arguments Scope BigZ.to_Z [bigZ_scope]. -Arguments Scope BigZ.succ [bigZ_scope]. -Arguments Scope BigZ.pred [bigZ_scope]. -Arguments Scope BigZ.opp [bigZ_scope]. -Arguments Scope BigZ.square [bigZ_scope]. -Arguments Scope BigZ.add [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.sub [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.mul [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.div [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.eq [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.lt [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.le [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.eq [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.compare [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.min [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.max [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.eq_bool [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.pow_pos [bigZ_scope positive_scope]. -Arguments Scope BigZ.pow_N [bigZ_scope N_scope]. -Arguments Scope BigZ.pow [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.log2 [bigZ_scope]. -Arguments Scope BigZ.sqrt [bigZ_scope]. -Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.quot [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.rem [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.lcm [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.even [bigZ_scope]. -Arguments Scope BigZ.odd [bigZ_scope]. -Arguments Scope BigN.testbit [bigZ_scope bigZ_scope]. -Arguments Scope BigN.shiftl [bigZ_scope bigZ_scope]. -Arguments Scope BigN.shiftr [bigZ_scope bigZ_scope]. -Arguments Scope BigN.lor [bigZ_scope bigZ_scope]. -Arguments Scope BigN.land [bigZ_scope bigZ_scope]. -Arguments Scope BigN.ldiff [bigZ_scope bigZ_scope]. -Arguments Scope BigN.lxor [bigZ_scope bigZ_scope]. -Arguments Scope BigN.setbit [bigZ_scope bigZ_scope]. -Arguments Scope BigN.clearbit [bigZ_scope bigZ_scope]. -Arguments Scope BigN.lnot [bigZ_scope]. -Arguments Scope BigN.div2 [bigZ_scope]. -Arguments Scope BigN.ones [bigZ_scope]. - Local Notation "0" := BigZ.zero : bigZ_scope. Local Notation "1" := BigZ.one : bigZ_scope. Local Notation "2" := BigZ.two : bigZ_scope. @@ -94,21 +53,19 @@ Infix "/" := BigZ.div : bigZ_scope. Infix "^" := BigZ.pow : bigZ_scope. Infix "?=" := BigZ.compare : bigZ_scope. Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope. -Notation "x != y" := (~x==y)%bigZ (at level 70, no associativity) : bigZ_scope. +Notation "x != y" := (~x==y) (at level 70, no associativity) : bigZ_scope. Infix "<" := BigZ.lt : bigZ_scope. Infix "<=" := BigZ.le : bigZ_scope. -Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope. -Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope. -Notation "x < y < z" := (x<y /\ y<z)%bigZ : bigZ_scope. -Notation "x < y <= z" := (x<y /\ y<=z)%bigZ : bigZ_scope. -Notation "x <= y < z" := (x<=y /\ y<z)%bigZ : bigZ_scope. -Notation "x <= y <= z" := (x<=y /\ y<=z)%bigZ : bigZ_scope. +Notation "x > y" := (y < x) (only parsing) : bigZ_scope. +Notation "x >= y" := (y <= x) (only parsing) : bigZ_scope. +Notation "x < y < z" := (x<y /\ y<z) : bigZ_scope. +Notation "x < y <= z" := (x<y /\ y<=z) : bigZ_scope. +Notation "x <= y < z" := (x<=y /\ y<z) : bigZ_scope. +Notation "x <= y <= z" := (x<=y /\ y<=z) : bigZ_scope. Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope. Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigZ_scope. Infix "รท" := BigZ.quot (at level 40, left associativity) : bigZ_scope. -Local Open Scope bigZ_scope. - (** Some additional results about [BigZ] *) Theorem spec_to_Z: forall n : bigZ, diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 7534628fa1..57b98e8603 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -29,6 +29,8 @@ Module Make (N:NType) <: ZType. Definition t := t_. + Bind Scope abstract_scope with t t_. + Definition zero := Pos N.zero. Definition one := Pos N.one. Definition two := Pos N.two. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 3664180357..fbb91ef7f2 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -223,8 +223,9 @@ Definition eq := (@eq Z). (** Now the generic properties. *) -Include ZProp - <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. +Include ZProp [scope abstract_scope to Z_scope] + <+ UsualMinMaxLogicalProperties [scope abstract_scope to Z_scope] + <+ UsualMinMaxDecProperties [scope abstract_scope to Z_scope]. End Z. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 56fad9347d..65b6463569 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -12,6 +12,11 @@ Require Import NZAxioms. Module Type NZBaseProp (Import NZ : NZDomainSig'). +(** An artificial scope meant to be substituted later *) + +Delimit Scope abstract_scope with abstract. +Bind Scope abstract_scope with t. + Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *) Lemma eq_sym_iff : forall x y, x==y <-> y==x. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 315876656d..858c066581 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -26,62 +26,23 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake *) -Module BigN <: NType <: OrderedTypeFull <: TotalOrder := - NMake.Make Int31Cyclic <+ NTypeIsNAxioms - <+ !NProp <+ HasEqBool2Dec - <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. +Delimit Scope bigN_scope with bigN. +Module BigN <: NType <: OrderedTypeFull <: TotalOrder := + NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope] + <+ NTypeIsNAxioms [scope abstract_scope to bigN_scope] + <+ NProp [no inline, scope abstract_scope to bigN_scope] + <+ HasEqBool2Dec [no inline, scope abstract_scope to bigN_scope] + <+ MinMaxLogicalProperties [no inline, scope abstract_scope to bigN_scope] + <+ MinMaxDecProperties [no inline, scope abstract_scope to bigN_scope]. (** Notations about [BigN] *) -Notation bigN := BigN.t. - -Delimit Scope bigN_scope with bigN. -Bind Scope bigN_scope with bigN. -Bind Scope bigN_scope with BigN.t. -Bind Scope bigN_scope with BigN.t'. -(* Bind Scope has no retroactive effect, let's declare scopes by hand. *) -Arguments Scope BigN.to_Z [bigN_scope]. -Arguments Scope BigN.to_N [bigN_scope]. -Arguments Scope BigN.succ [bigN_scope]. -Arguments Scope BigN.pred [bigN_scope]. -Arguments Scope BigN.square [bigN_scope]. -Arguments Scope BigN.add [bigN_scope bigN_scope]. -Arguments Scope BigN.sub [bigN_scope bigN_scope]. -Arguments Scope BigN.mul [bigN_scope bigN_scope]. -Arguments Scope BigN.div [bigN_scope bigN_scope]. -Arguments Scope BigN.eq [bigN_scope bigN_scope]. -Arguments Scope BigN.lt [bigN_scope bigN_scope]. -Arguments Scope BigN.le [bigN_scope bigN_scope]. -Arguments Scope BigN.eq [bigN_scope bigN_scope]. -Arguments Scope BigN.compare [bigN_scope bigN_scope]. -Arguments Scope BigN.min [bigN_scope bigN_scope]. -Arguments Scope BigN.max [bigN_scope bigN_scope]. -Arguments Scope BigN.eq_bool [bigN_scope bigN_scope]. -Arguments Scope BigN.pow_pos [bigN_scope positive_scope]. -Arguments Scope BigN.pow_N [bigN_scope N_scope]. -Arguments Scope BigN.pow [bigN_scope bigN_scope]. -Arguments Scope BigN.log2 [bigN_scope]. -Arguments Scope BigN.sqrt [bigN_scope]. -Arguments Scope BigN.div_eucl [bigN_scope bigN_scope]. -Arguments Scope BigN.modulo [bigN_scope bigN_scope]. -Arguments Scope BigN.gcd [bigN_scope bigN_scope]. -Arguments Scope BigN.lcm [bigN_scope bigN_scope]. -Arguments Scope BigN.even [bigN_scope]. -Arguments Scope BigN.odd [bigN_scope]. -Arguments Scope BigN.testbit [bigN_scope bigN_scope]. -Arguments Scope BigN.shiftl [bigN_scope bigN_scope]. -Arguments Scope BigN.shiftr [bigN_scope bigN_scope]. -Arguments Scope BigN.lor [bigN_scope bigN_scope]. -Arguments Scope BigN.land [bigN_scope bigN_scope]. -Arguments Scope BigN.ldiff [bigN_scope bigN_scope]. -Arguments Scope BigN.lxor [bigN_scope bigN_scope]. -Arguments Scope BigN.setbit [bigN_scope bigN_scope]. -Arguments Scope BigN.clearbit [bigN_scope bigN_scope]. -Arguments Scope BigN.lnot [bigN_scope bigN_scope]. -Arguments Scope BigN.div2 [bigN_scope]. -Arguments Scope BigN.ones [bigN_scope]. +Local Open Scope bigN_scope. +Notation bigN := BigN.t. +Bind Scope bigN_scope with bigN BigN.t BigN.t'. +Arguments Scope BigN.N0 [int31_scope]. Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *) Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *) Local Notation "2" := BigN.two : bigN_scope. (* temporary notation *) @@ -92,20 +53,18 @@ Infix "/" := BigN.div : bigN_scope. Infix "^" := BigN.pow : bigN_scope. Infix "?=" := BigN.compare : bigN_scope. Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope. -Notation "x != y" := (~x==y)%bigN (at level 70, no associativity) : bigN_scope. +Notation "x != y" := (~x==y) (at level 70, no associativity) : bigN_scope. Infix "<" := BigN.lt : bigN_scope. Infix "<=" := BigN.le : bigN_scope. -Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope. -Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope. -Notation "x < y < z" := (x<y /\ y<z)%bigN : bigN_scope. -Notation "x < y <= z" := (x<y /\ y<=z)%bigN : bigN_scope. -Notation "x <= y < z" := (x<=y /\ y<z)%bigN : bigN_scope. -Notation "x <= y <= z" := (x<=y /\ y<=z)%bigN : bigN_scope. +Notation "x > y" := (y < x) (only parsing) : bigN_scope. +Notation "x >= y" := (y <= x) (only parsing) : bigN_scope. +Notation "x < y < z" := (x<y /\ y<z) : bigN_scope. +Notation "x < y <= z" := (x<y /\ y<=z) : bigN_scope. +Notation "x <= y < z" := (x<=y /\ y<z) : bigN_scope. +Notation "x <= y <= z" := (x<=y /\ y<=z) : bigN_scope. Notation "[ i ]" := (BigN.to_Z i) : bigN_scope. Infix "mod" := BigN.modulo (at level 40, no associativity) : bigN_scope. -Local Open Scope bigN_scope. - (** Example of reasoning about [BigN] *) Theorem succ_pred: forall q : bigN, diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index b5cc4c51d8..f095a34821 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -138,6 +138,8 @@ pr pr ""; pr " Definition t := t'."; pr ""; + pr " Bind Scope abstract_scope with t t'."; + pr ""; pr " (** * A generic toolbox for building and deconstructing [t] *)"; pr ""; diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index bd59ef494b..cf284a2f19 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -234,8 +234,9 @@ Definition lor := Nor. Definition ldiff := Ndiff. Definition div2 := Ndiv2. -Include NProp - <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. +Include NProp [scope abstract_scope to N_scope] + <+ UsualMinMaxLogicalProperties [scope abstract_scope to N_scope] + <+ UsualMinMaxDecProperties [scope abstract_scope to N_scope]. End N. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 0cf9ae4416..4578851e27 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -756,8 +756,9 @@ Definition div2_spec a : div2 a = shiftr a 1 := eq_refl _. (** Generic Properties *) -Include NProp - <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. +Include NProp [scope abstract_scope to nat_scope] + <+ UsualMinMaxLogicalProperties [scope abstract_scope to nat_scope] + <+ UsualMinMaxDecProperties [scope abstract_scope to nat_scope]. End Nat. diff --git a/toplevel/command.mli b/toplevel/command.mli index 2c90b6bd54..8ffdbdec4a 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -44,11 +44,11 @@ val interp_assumption : val declare_assumption : coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits -> - bool (** implicit *) -> inline -> variable located -> unit + bool (** implicit *) -> Entries.inline -> variable located -> unit val declare_assumptions : variable located list -> coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits -> - bool -> inline -> unit + bool -> Entries.inline -> unit (** {6 Inductive and coinductive types} *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index ccbaa6d306..ca4a82ea69 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -32,6 +32,7 @@ open Pretyping open Redexpr open Syntax_def open Lemmas +open Declaremods (* Pcoq hooks *) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 3091f10c53..ac3b3964ab 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -15,6 +15,7 @@ open Genarg open Topconstr open Decl_kinds open Ppextend +open Declaremods (* Toplevel control exceptions *) exception Drop @@ -168,6 +169,7 @@ type inductive_expr = type one_inductive_expr = lident * local_binder list * constr_expr option * constructor_expr list +type module_ast_inl = module_ast annotated type module_binder = bool option * lident list * module_ast_inl type grammar_tactic_prod_item_expr = |