diff options
| -rw-r--r-- | interp/topconstr.ml | 4 | ||||
| -rw-r--r-- | interp/topconstr.mli | 4 | ||||
| -rw-r--r-- | library/declaremods.ml | 103 | ||||
| -rw-r--r-- | library/declaremods.mli | 7 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 37 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 25 | ||||
| -rw-r--r-- | plugins/interface/xlate.ml | 12 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZAxioms.v | 50 | ||||
| -rw-r--r-- | theories/Structures/DecidableType2.v | 211 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 38 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 4 |
11 files changed, 228 insertions, 267 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index df48458e6..12ce52d1b 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -1012,8 +1012,8 @@ type module_type_ast = | CMTEwith of module_type_ast * with_declaration_ast type include_ast = - | CIMTE of module_type_ast - | CIME of module_ast + | CIMTE of module_type_ast * module_type_ast list + | CIME of module_ast * module_ast list let loc_of_notation f loc (args,_) ntn = if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 1966bf552..1b6514a65 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -256,8 +256,8 @@ type module_type_ast = | CMTEwith of module_type_ast * with_declaration_ast type include_ast = - | CIMTE of module_type_ast - | CIME of module_ast + | CIMTE of module_type_ast * module_type_ast list + | CIME of module_ast * module_ast list val ntn_loc : Util.loc -> constr_expr notation_substitution -> string -> int val patntn_loc : Util.loc -> cases_pattern_expr notation_substitution -> string -> int diff --git a/library/declaremods.ml b/library/declaremods.ml index c40e94c51..42d3652aa 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -663,7 +663,7 @@ let end_modtype () = mp -let declare_modtype interp_modtype id args mty = +let declare_modtype_real interp_modtype id args mty = let fs = Summary.freeze_summaries () in try @@ -824,7 +824,7 @@ let rec update_include (mbids,mp,objs) = in (mbids,mp,replace_include objs) -let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = +let declare_module_real interp_modtype interp_modexpr id args mty_o mexpr_o = let fs = Summary.freeze_summaries () in @@ -892,48 +892,42 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = Summary.unfreeze_summaries fs; raise e -let declare_include interp_struct me_ast is_mod is_self = - - let fs = Summary.freeze_summaries () in +let declare_one_include interp_struct me_ast is_mod is_self = + let env = Global.env() in + let me = interp_struct env me_ast in + let mp1,_ = current_prefix () in + let compute_objs objs = function + | MSEident mp -> + let mb_mp = if is_mod then + Environ.lookup_module mp env else + Modops.module_body_of_type mp (Environ.lookup_modtype mp env) in + (match objs with + |([],_,_) -> objs + |(mbids,mp_self,objects) -> + let mb = Global.pack_module() in + let rec compute_subst mbids sign = + match mbids with + [] -> empty_subst + | mbid::mbids -> + let farg_id, farg_b, fbody_b = + Modops.destr_functor env sign in + let subst=compute_subst mbids fbody_b in + let mp_delta = + Modops.complete_inline_delta_resolver env mb.mod_mp + farg_id farg_b mb.mod_delta in + join (map_mbid mbid mb.mod_mp mp_delta) subst + in + let subst = compute_subst mbids mb_mp.mod_type in + ([],mp_self,subst_objects subst objects)) + | _ -> objs + in - try - let env = Global.env() in - let me = interp_struct env me_ast in - let mp1,_ = current_prefix () in - let compute_objs objs = function - | MSEident mp -> - let mb_mp = if is_mod then - Environ.lookup_module mp env else - Modops.module_body_of_type mp (Environ.lookup_modtype mp env) in - (match objs with - |([],_,_) -> objs - |(mbids,mp_self,objects) -> - let mb = Global.pack_module() in - let rec compute_subst mbids sign = - match mbids with - [] -> empty_subst - | mbid::mbids -> - let farg_id, farg_b, fbody_b = - Modops.destr_functor env sign in - let subst=compute_subst mbids fbody_b in - let mp_delta = - Modops.complete_inline_delta_resolver env mb.mod_mp - farg_id farg_b mb.mod_delta in - join (map_mbid mbid mb.mod_mp mp_delta) subst - in - let subst = compute_subst mbids mb_mp.mod_type in - ([],mp_self,subst_objects subst objects) - - ) - | _ -> objs - in - let (mbids,mp,objs)= if is_mod then get_module_substobjs env mp1 me else get_modtype_substobjs env mp1 me in - let (mbids,mp,objs) = if is_self + let (mbids,mp,objs) = if is_self then compute_objs (mbids,mp,objs) me else (mbids,mp,objs) in let id = current_mod_id() in let resolver = Global.add_include me is_mod in @@ -941,9 +935,36 @@ let declare_include interp_struct me_ast is_mod is_self = subst_objects (map_mp mp mp1 resolver) objs) in ignore (add_leaf id (in_include ((me,is_mod), substobjs))) - with e -> - (* Something wrong: undo the whole process *) - Summary.unfreeze_summaries fs; raise e + + +let declare_include interp_struct me_ast me_asts is_mod is_self = + let fs = Summary.freeze_summaries () in + try + declare_one_include interp_struct me_ast is_mod is_self; + List.iter + (fun me -> declare_one_include interp_struct me is_mod true) + me_asts + with e -> + (* Something wrong: undo the whole process *) + Summary.unfreeze_summaries fs; raise e + + +let declare_modtype interp_mt id args = function + | [] -> assert false + | [mty] -> declare_modtype_real interp_mt id args mty + | mty :: mty_l -> + ignore (start_modtype interp_mt id args); + declare_include interp_mt mty mty_l false false; + end_modtype () + +let declare_module interp_mt interp_me id args mty_o = function + | [] -> declare_module_real interp_mt interp_me id args mty_o None + | [me] -> declare_module_real interp_mt interp_me id args mty_o (Some me) + | me :: me_l -> + ignore (start_module interp_mt None id args mty_o); + declare_include interp_me me me_l true false; + end_module () + (*s Iterators. *) diff --git a/library/declaremods.mli b/library/declaremods.mli index 4a037b005..3d16a287f 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -40,7 +40,7 @@ val declare_module : (env -> 'modtype -> module_struct_entry) -> (env -> 'modexpr -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> ('modtype * bool) option -> - 'modexpr option -> module_path + 'modexpr list -> module_path val start_module : (env -> 'modtype -> module_struct_entry) -> bool option -> identifier -> (identifier located list * 'modtype) list -> @@ -53,7 +53,8 @@ val end_module : unit -> module_path (*s Module types *) val declare_modtype : (env -> 'modtype -> module_struct_entry) -> - identifier -> (identifier located list * 'modtype) list -> 'modtype -> module_path + identifier -> (identifier located list * 'modtype) list -> + 'modtype list -> module_path val start_modtype : (env -> 'modtype -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> module_path @@ -100,7 +101,7 @@ val import_module : bool -> module_path -> unit (* Include *) val declare_include : (env -> 'struct_expr -> module_struct_entry) -> - 'struct_expr -> bool -> bool -> unit + 'struct_expr -> 'struct_expr list -> bool -> bool -> unit (*s [iter_all_segments] iterate over all segments, the modules' segments first and then the current segment. Modules are presented diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3a99b2473..38ab689f5 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -389,13 +389,13 @@ GEXTEND Gram [ [ (* Interactive module declaration *) IDENT "Module"; export = export_token; id = identref; bl = LIST0 module_binder; mty_o = OPT of_module_type; - mexpr_o = OPT is_module_expr -> - VernacDefineModule (export, id, bl, mty_o, mexpr_o) - + o = OPT is_module_expr -> + VernacDefineModule (export, id, bl, mty_o, + match o with None -> [] | Some l -> l) | IDENT "Module"; "Type"; id = identref; - bl = LIST0 module_binder; mty_o = OPT is_module_type -> - VernacDeclareModuleType (id, bl, mty_o) - + bl = LIST0 module_binder; o = OPT is_module_type -> + VernacDeclareModuleType (id, bl, + match o with None -> [] | Some l -> l) | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; bl = LIST0 module_binder; ":"; mty = module_type -> VernacDeclareModule (export, id, bl, (mty,true)) @@ -413,28 +413,35 @@ GEXTEND Gram VernacRequireFrom (export, None, filename) | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) - | IDENT "Include"; expr = module_expr -> VernacInclude(false,CIME(expr)) - | IDENT "Include"; "Type"; expr = module_type -> - VernacInclude(false,CIMTE(expr)) - | IDENT "Include"; "Self"; expr = module_expr -> - VernacInclude(true,CIME(expr)) - | IDENT "Include"; "Self"; "Type"; expr = module_type -> - VernacInclude(true,CIMTE(expr)) ] ] + | IDENT "Include"; e = module_expr; l = LIST0 ext_module_expr -> + VernacInclude(false,CIME(e,l)) + | IDENT "Include"; "Type"; e = module_type; l = LIST0 ext_module_type -> + VernacInclude(false,CIMTE(e,l)) + | IDENT "Include"; "Self"; e = module_expr -> + VernacInclude(true,CIME(e,[])) + | IDENT "Include"; "Self"; "Type"; e = module_type -> + VernacInclude(true,CIMTE(e,[])) ] ] ; export_token: [ [ IDENT "Import" -> Some false | IDENT "Export" -> Some true | -> None ] ] ; + ext_module_type: + [ [ "<+"; mty = module_type -> mty ] ] + ; + ext_module_expr: + [ [ "<+"; mexpr = module_expr -> mexpr ] ] + ; of_module_type: [ [ ":"; mty = module_type -> (mty, true) | "<:"; mty = module_type -> (mty, false) ] ] ; is_module_type: - [ [ ":="; mty = module_type -> mty ] ] + [ [ ":="; mty = module_type ; l = LIST0 ext_module_type -> (mty::l) ] ] ; is_module_expr: - [ [ ":="; mexpr = module_expr -> mexpr ] ] + [ [ ":="; mexpr = module_expr; l = LIST0 ext_module_expr -> (mexpr::l) ] ] ; (* Module binder *) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 52ef1875f..4407ca6aa 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -751,7 +751,8 @@ let rec pr_vernac = function hov 2 (str"Module" ++ spc() ++ pr_require_token export ++ pr_lident m ++ b ++ pr_opt (pr_of_module_type pr_lconstr) ty ++ - pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd) + (if bd = [] then mt () else str ":= ") ++ + prlist_with_sep (fun () -> str " <+ ") pr_module_expr bd) | VernacDeclareModule (export,id,bl,m1) -> let b = pr_module_binders_list bl pr_lconstr in hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++ @@ -760,17 +761,17 @@ let rec pr_vernac = function | VernacDeclareModuleType (id,bl,m) -> let b = pr_module_binders_list bl pr_lconstr in hov 2 (str"Module Type " ++ pr_lident id ++ b ++ - pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m) - | VernacInclude (b,in_ast) -> - begin - match in_ast with - | CIMTE mty -> - hov 2 (str"Include " ++ str (if b then "Self " else "") ++ - pr_module_type pr_lconstr mty) - | CIME mexpr -> - hov 2 (str"Include " ++ str (if b then "Self " else "") ++ - pr_module_expr mexpr) - end + (if m = [] then mt () else str ":= ") ++ + prlist_with_sep (fun () -> str " <+ ") + (pr_module_type pr_lconstr) m) + | VernacInclude (b,CIMTE(mty,mtys)) -> + let pr_mty = pr_module_type pr_lconstr in + hov 2 (str"Include " ++ str (if b then "Self " else "") ++ str "Type " ++ + prlist_with_sep (fun () -> str " <+ ") pr_mty (mty::mtys)) + | VernacInclude (b,CIME(mexpr,mexprs)) -> + let pr_me = pr_module_expr in + hov 2 (str"Include " ++ str (if b then "Self " else "") ++ + prlist_with_sep (fun () -> str " <+ ") pr_me (mexpr::mexprs)) (* Solving *) | VernacSolve (i,tac,deftac) -> (if i = 1 then mt() else int i ++ str ": ") ++ diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index 7b35f4021..97ab9efc8 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -2038,19 +2038,21 @@ let rec xlate_vernac = CT_module_type_decl(xlate_ident id, xlate_module_binder_list bl, match mty_o with - None -> + [] -> CT_coerce_ID_OPT_to_MODULE_TYPE_OPT ctv_ID_OPT_NONE - | Some mty1 -> + | [mty1] -> CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT - (xlate_module_type mty1)) + (xlate_module_type mty1) + | _ -> failwith "TODO: Include Self") | VernacDefineModule(_,(_, id), bl, mty_o, mexpr_o) -> CT_module(xlate_ident id, xlate_module_binder_list bl, xlate_module_type_check_opt mty_o, match mexpr_o with - None -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE - | Some m -> xlate_module_expr m) + [] -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE + | [m] -> xlate_module_expr m + | _ -> failwith "TODO Include Self") | VernacDeclareModule(_,(_, id), bl, mty_o) -> CT_declare_module(xlate_ident id, xlate_module_binder_list bl, diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index c85e84b04..889d9c2e5 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -23,7 +23,7 @@ Local Open Scope NumScope. for instance [Z/nZ] (See file [NZDomain for a study of that). *) -Module Type NZDomain_fun (Import E : EqualityType). +Module Type NZDomain (Import E : EqualityType). (** [E] provides [t], [eq], [eq_equiv : Equivalence eq] *) Notation "x == y" := (eq x y) (at level 70) : NumScope. @@ -47,21 +47,18 @@ Axiom bi_induction : forall A : t -> Prop, Proper (eq==>iff) A -> A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n. -End NZDomain_fun. +End NZDomain. -Module Type NZDomainSig. - Include Type EqualityType. - Include Self Type NZDomain_fun. -End NZDomainSig. +Module Type NZDomainSig := EqualityType <+ NZDomain. + +(** A version with decidable type *) + +Module Type NZDecDomainSig := DecidableType <+ NZDomain. -Module Type NZDecDomainSig. - Include Type DecidableType. - Include Self Type NZDomain_fun. -End NZDecDomainSig. (** Axiomatization of basic operations : [+] [-] [*] *) -Module Type NZBasicFuns_fun (Import NZ : NZDomainSig). +Module Type NZHasBasicFuns (Import NZ : NZDomainSig). Parameter Inline add : t -> t -> t. Parameter Inline sub : t -> t -> t. @@ -84,12 +81,10 @@ Axiom sub_succ_r : forall n m, n - (S m) == P (n - m). Axiom mul_0_l : forall n, 0 * n == 0. Axiom mul_succ_l : forall n m, S n * m == n * m + m. -End NZBasicFuns_fun. +End NZHasBasicFuns. + +Module Type NZBasicFunsSig := NZDomainSig <+ NZHasBasicFuns. -Module Type NZBasicFunsSig. - Include Type NZDomainSig. - Include Self Type NZBasicFuns_fun. -End NZBasicFunsSig. (** Old name for the same interface: *) @@ -98,7 +93,7 @@ Module Type NZAxiomsSig := NZBasicFunsSig. (** Axiomatization of order *) -Module Type NZOrd_fun (Import NZ : NZDomainSig). +Module Type NZHasOrd (Import NZ : NZDomainSig). Parameter Inline lt : t -> t -> Prop. Parameter Inline le : t -> t -> Prop. @@ -116,17 +111,14 @@ Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. Axiom lt_irrefl : forall n, ~ (n < n). Axiom lt_succ_r : forall n m, n < S m <-> n <= m. -End NZOrd_fun. +End NZHasOrd. -Module Type NZOrdSig. - Include Type NZDomainSig. - Include Self Type NZOrd_fun. -End NZOrdSig. +Module Type NZOrdSig := NZDomainSig <+ NZHasOrd. (** Axiomatization of minimum and maximum *) -Module Type NZMinMax_fun (Import NZ : NZOrdSig). +Module Type NZHasMinMax (Import NZ : NZOrdSig). Parameter Inline min : t -> t -> t. Parameter Inline max : t -> t -> t. @@ -138,11 +130,9 @@ Axiom min_r : forall n m, m <= n -> min n m == m. Axiom max_l : forall n m, m <= n -> max n m == n. Axiom max_r : forall n m, n <= m -> max n m == m. -End NZMinMax_fun. +End NZHasMinMax. + + +Module Type NZOrdAxiomsSig := + NZDomainSig <+ NZHasBasicFuns <+ NZHasOrd <+ NZHasMinMax. -Module Type NZOrdAxiomsSig. - Include Type NZDomainSig. - Include Self Type NZBasicFuns_fun. - Include Self Type NZOrd_fun. - Include Self Type NZMinMax_fun. -End NZOrdAxiomsSig. diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v index 7cae4358b..111f45ca7 100644 --- a/theories/Structures/DecidableType2.v +++ b/theories/Structures/DecidableType2.v @@ -22,135 +22,98 @@ End BareEquality. (** * Specification of the equality by the Type Classe [Equivalence] *) -Module Type Equality_fun (Import E:BareEquality). +Module Type IsEq (Import E:BareEquality). Instance eq_equiv : Equivalence eq. Hint Resolve (@Equivalence_Reflexive _ _ eq_equiv). Hint Resolve (@Equivalence_Transitive _ _ eq_equiv). Hint Immediate (@Equivalence_Symmetric _ _ eq_equiv). -End Equality_fun. +End IsEq. (** * Earlier specification of equality by three separate lemmas. *) -Module Type EqualityOrig_fun(Import E:BareEquality). +Module Type IsEqOrig (Import E:BareEquality). Axiom eq_refl : forall x : t, eq x x. Axiom eq_sym : forall x y : t, eq x y -> eq y x. Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. Hint Immediate eq_sym. Hint Resolve eq_refl eq_trans. -End EqualityOrig_fun. +End IsEqOrig. (** * Types with decidable equality *) -Module Type Decidable_fun (Import E:BareEquality). +Module Type HasEqDec (Import E:BareEquality). Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }. -End Decidable_fun. +End HasEqDec. (** * Boolean Equality *) (** Having [eq_dec] is the same as having a boolean equality plus a correctness proof. *) -Module Type BoolEq_fun (Import E:BareEquality). +Module Type HasEqBool (Import E:BareEquality). Parameter Inline eqb : t -> t -> bool. Parameter eqb_eq : forall x y, eqb x y = true <-> eq x y. -End BoolEq_fun. +End HasEqBool. (** From these basic blocks, we can build many combinations of static standalone module types. *) -Module Type EqualityType. - Include Type BareEquality. - Include Self Type Equality_fun. -End EqualityType. - -Module Type EqualityTypeOrig. - Include Type BareEquality. - Include Self Type EqualityOrig_fun. -End EqualityTypeOrig. - -Module Type EqualityTypeBoth. (* <: EqualityType <: EqualityTypeOrig *) - Include Type BareEquality. - Include Self Type Equality_fun. - Include Self Type EqualityOrig_fun. -End EqualityTypeBoth. - -Module Type DecidableType. (* <: EqualityType *) - Include Type BareEquality. - Include Self Type Equality_fun. - Include Self Type Decidable_fun. -End DecidableType. - -Module Type DecidableTypeOrig. (* <: EqualityTypeOrig *) - Include Type BareEquality. - Include Self Type EqualityOrig_fun. - Include Self Type Decidable_fun. -End DecidableTypeOrig. - -Module Type DecidableTypeBoth. (* <: DecidableType <: DecidableTypeOrig *) - Include Type EqualityTypeBoth. - Include Self Type Decidable_fun. -End DecidableTypeBoth. - -Module Type BooleanEqualityType. (* <: EqualityType *) - Include Type BareEquality. - Include Self Type Equality_fun. - Include Self Type BoolEq_fun. -End BooleanEqualityType. - -Module Type BooleanDecidableType. (* <: DecidableType <: BooleanEqualityType *) - Include Type BareEquality. - Include Self Type Equality_fun. - Include Self Type Decidable_fun. - Include Self Type BoolEq_fun. -End BooleanDecidableType. - -Module Type DecidableTypeFull. (* <: all previous interfaces *) - Include Type BareEquality. - Include Self Type Equality_fun. - Include Self Type EqualityOrig_fun. - Include Self Type Decidable_fun. - Include Self Type BoolEq_fun. -End DecidableTypeFull. +Module Type EqualityType := BareEquality <+ IsEq. + +Module Type EqualityTypeOrig := BareEquality <+ IsEqOrig. + +Module Type EqualityTypeBoth (* <: EqualityType <: EqualityTypeOrig *) + := BareEquality <+ IsEq <+ IsEqOrig. + +Module Type DecidableType (* <: EqualityType *) + := BareEquality <+ IsEq <+ HasEqDec. + +Module Type DecidableTypeOrig (* <: EqualityTypeOrig *) + := BareEquality <+ IsEqOrig <+ HasEqDec. + +Module Type DecidableTypeBoth (* <: DecidableType <: DecidableTypeOrig *) + := EqualityTypeBoth <+ HasEqDec. + +Module Type BooleanEqualityType (* <: EqualityType *) + := BareEquality <+ IsEq <+ HasEqBool. + +Module Type BooleanDecidableType (* <: DecidableType <: BooleanEqualityType *) + := BareEquality <+ IsEq <+ HasEqDec <+ HasEqBool. + +Module Type DecidableTypeFull (* <: all previous interfaces *) + := BareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool. (** * Compatibility wrapper from/to the old version of [EqualityType] and [DecidableType] *) -Module Backport_ET_fun (E:BareEquality)(F:Equality_fun E) <: EqualityOrig_fun E. +Module BackportEq (E:BareEquality)(F:IsEq E) <: IsEqOrig E. Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv. Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv. Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv. -End Backport_ET_fun. +End BackportEq. -Module Update_ET_fun (E:BareEquality)(F:EqualityOrig_fun E) <: Equality_fun E. +Module UpdateEq (E:BareEquality)(F:IsEqOrig E) <: IsEq E. Instance eq_equiv : Equivalence E.eq. Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed. -End Update_ET_fun. +End UpdateEq. -Module Backport_ET (E:EqualityType) <: EqualityTypeBoth. - Include E. - Include Backport_ET_fun E E. -End Backport_ET. +Module Backport_ET (E:EqualityType) <: EqualityTypeBoth + := E <+ BackportEq E E. -Module Update_ET (E:EqualityTypeOrig) <: EqualityTypeBoth. - Include E. - Include Update_ET_fun E E. -End Update_ET. +Module Update_ET (E:EqualityTypeOrig) <: EqualityTypeBoth + := E <+ UpdateEq E E. -Module Backport_DT (E:DecidableType) <: DecidableTypeBoth. - Include E. - Include Backport_ET_fun E E. -End Backport_DT. +Module Backport_DT (E:DecidableType) <: DecidableTypeBoth + := E <+ BackportEq E E. -Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth. - Include E. - Include Update_ET_fun E E. -End Update_DT. +Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth + := E <+ UpdateEq E E. (** * Having [eq_dec] is equivalent to having [eqb] and its spec. *) -Module Dec2Bool_fun (E:BareEquality)(F:Decidable_fun E) <: BoolEq_fun E. +Module HasEqDec2Bool (E:BareEquality)(F:HasEqDec E) <: HasEqBool E. Definition eqb x y := if F.eq_dec x y then true else false. Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y. Proof. @@ -158,9 +121,9 @@ Module Dec2Bool_fun (E:BareEquality)(F:Decidable_fun E) <: BoolEq_fun E. auto with *. split. discriminate. intro EQ; elim NEQ; auto. Qed. -End Dec2Bool_fun. +End HasEqDec2Bool. -Module Bool2Dec_fun (E:BareEquality)(F:BoolEq_fun E) <: Decidable_fun E. +Module HasEqBool2Dec (E:BareEquality)(F:HasEqBool E) <: HasEqDec E. Lemma eq_dec : forall x y, {E.eq x y}+{~E.eq x y}. Proof. intros x y. assert (H:=F.eqb_eq x y). @@ -168,17 +131,13 @@ Module Bool2Dec_fun (E:BareEquality)(F:BoolEq_fun E) <: Decidable_fun E. apply -> H; auto. intro EQ. apply H in EQ. discriminate. Defined. -End Bool2Dec_fun. +End HasEqBool2Dec. -Module Dec2Bool (E:DecidableType) <: BooleanDecidableType. - Include E. - Include Dec2Bool_fun E E. -End Dec2Bool. +Module Dec2Bool (E:DecidableType) <: BooleanDecidableType + := E <+ HasEqDec2Bool E E. -Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType. - Include E. - Include Bool2Dec_fun E E. -End Bool2Dec. +Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType + := E <+ HasEqBool2Dec E E. @@ -192,46 +151,30 @@ Module Type UsualBareEquality. (* <: BareEquality *) Definition eq := @eq t. End UsualBareEquality. -Module UsualEquality_fun (E:UsualBareEquality) <: Equality_fun E. +Module UsualIsEq (E:UsualBareEquality) <: IsEq E. Program Instance eq_equiv : Equivalence E.eq. -End UsualEquality_fun. +End UsualIsEq. -Module UsualEqualityOrig_fun (E:UsualBareEquality) <: EqualityOrig_fun E. +Module UsualIsEqOrig (E:UsualBareEquality) <: IsEqOrig E. Definition eq_refl := @eq_refl E.t. Definition eq_sym := @eq_sym E.t. Definition eq_trans := @eq_trans E.t. -End UsualEqualityOrig_fun. - -Module Type UsualEqualityType. (* <: EqualityType *) - Include Type UsualBareEquality. - Include Self Type Equality_fun. -End UsualEqualityType. - -Module Type UsualDecidableType. (* <: DecidableType *) - Include Type UsualBareEquality. - Include Self Type Equality_fun. - Include Self Type Decidable_fun. -End UsualDecidableType. - -Module Type UsualDecidableTypeBoth. (* <: DecidableTypeBoth *) - Include Type UsualBareEquality. - Include Self Type Equality_fun. - Include Self Type EqualityOrig_fun. - Include Self Type Decidable_fun. -End UsualDecidableTypeBoth. - -Module Type UsualBoolEq. - Include Type UsualBareEquality. - Include Self Type BoolEq_fun. -End UsualBoolEq. - -Module Type UsualDecidableTypeFull. (* <: DecidableTypeFull *) - Include Type UsualBareEquality. - Include Self Type Equality_fun. - Include Self Type EqualityOrig_fun. - Include Self Type Decidable_fun. - Include Self Type BoolEq_fun. -End UsualDecidableTypeFull. +End UsualIsEqOrig. + +Module Type UsualEqualityType (* <: EqualityType *) + := UsualBareEquality <+ IsEq. + +Module Type UsualDecidableType (* <: DecidableType *) + := UsualBareEquality <+ IsEq <+ HasEqDec. + +Module Type UsualDecidableTypeBoth (* <: DecidableTypeBoth *) + := UsualBareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec. + +Module Type UsualBoolEq := UsualBareEquality <+ HasEqBool. + +Module Type UsualDecidableTypeFull (* <: DecidableTypeFull *) + := UsualBareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool. + (** a [UsualDecidableType] is in particular an [DecidableType]. *) @@ -247,14 +190,10 @@ End MiniDecidableType. Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth. Include M. Definition eq := @eq M.t. - Include Self UsualEquality_fun. - Include Self UsualEqualityOrig_fun. + Include Self UsualIsEq. + Include Self UsualIsEqOrig. End Make_UDT. -Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull. - Include M. (* t, eq, eqb, eqb_eq *) - Include UsualEquality_fun M. - Include UsualEqualityOrig_fun M. - Include Bool2Dec_fun M M. -End Make_UDTF. +Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull + := M <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqBool2Dec. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2008e5f01..76e7eb0b8 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -460,19 +460,19 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o = else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr - id binders_ast (Some mty_ast_o) None + id binders_ast (Some mty_ast_o) [] in Dumpglob.dump_moddef loc mp "mod"; if_verbose message ("Module "^ string_of_id id ^" is declared"); Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export -let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = +let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then error "Modules and Module Types are not allowed inside sections."; - match mexpr_ast_o with - | None -> + match mexpr_ast_l with + | [] -> check_no_pending_proofs (); let binders_ast,argsexport = List.fold_right @@ -490,7 +490,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export ) argsexport - | Some _ -> + | _::_ -> let binders_ast = List.map (fun (export,idl,ty) -> if export <> None then @@ -500,7 +500,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr - id binders_ast mty_ast_o mexpr_ast_o + id binders_ast mty_ast_o mexpr_ast_l in Dumpglob.dump_moddef loc mp "mod"; if_verbose message @@ -514,12 +514,12 @@ let vernac_end_module export (loc,id as lid) = if_verbose message ("Module "^ string_of_id id ^" is defined") ; Option.iter (fun export -> vernac_import export [Ident lid]) export -let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = +let vernac_declare_module_type (loc,id) binders_ast mty_ast_l = if Lib.sections_are_opened () then error "Modules and Module Types are not allowed inside sections."; - match mty_ast_o with - | None -> + match mty_ast_l with + | [] -> check_no_pending_proofs (); let binders_ast,argsexport = List.fold_right @@ -536,7 +536,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = (fun export -> vernac_import export [Ident (dummy_loc,id)]) export ) argsexport - | Some base_mty -> + | _ :: _ -> let binders_ast = List.map (fun (export,idl,ty) -> if export <> None then @@ -545,7 +545,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = "and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in let mp = Declaremods.declare_modtype Modintern.interp_modtype - id binders_ast base_mty in + id binders_ast mty_ast_l in Dumpglob.dump_moddef loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") @@ -556,12 +556,12 @@ let vernac_end_modtype (loc,id) = if_verbose message ("Module Type "^ string_of_id id ^" is defined") let vernac_include is_self = function - | CIMTE mty_ast -> + | CIMTE (mty,mtys) -> Declaremods.declare_include - Modintern.interp_modtype mty_ast false is_self - | CIME mexpr_ast -> + Modintern.interp_modtype mty mtys false is_self + | CIME (mexpr, mexprs) -> Declaremods.declare_include - Modintern.interp_modexpr mexpr_ast true is_self + Modintern.interp_modexpr mexpr mexprs true is_self (**********************) (* Gallina extensions *) @@ -1329,12 +1329,12 @@ let interp c = match c with (* Modules *) | VernacDeclareModule (export,lid,bl,mtyo) -> vernac_declare_module export lid bl mtyo - | VernacDefineModule (export,lid,bl,mtyo,mexpro) -> - vernac_define_module export lid bl mtyo mexpro + | VernacDefineModule (export,lid,bl,mtyo,mexprl) -> + vernac_define_module export lid bl mtyo mexprl | VernacDeclareModuleType (lid,bl,mtyo) -> vernac_declare_module_type lid bl mtyo - | VernacInclude (is_self,in_ast) -> - vernac_include is_self in_ast + | VernacInclude (is_self,in_asts) -> + vernac_include is_self in_asts (* Gallina extensions *) | VernacBeginSection lid -> vernac_begin_section lid diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 366308bfa..ccb850651 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -261,9 +261,9 @@ type vernac_expr = | VernacDeclareModule of bool option * lident * module_binder list * (module_type_ast * bool) | VernacDefineModule of bool option * lident * - module_binder list * (module_type_ast * bool) option * module_ast option + module_binder list * (module_type_ast * bool) option * module_ast list | VernacDeclareModuleType of lident * - module_binder list * module_type_ast option + module_binder list * module_type_ast list | VernacInclude of bool * include_ast (* Solving *) |