diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-07 15:24:13 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-07 15:24:13 +0000 |
commit | 35159e8aa9bf33b4882bc7f17c2e363f769624c7 (patch) | |
tree | b4791a8db7bcc1369025b1d261dc6d2a6301278c | |
parent | 78ad7ad114f3872c3e1c48e8427bee1351c25962 (diff) |
No more specific syntax "Include Self" for inclusion of partially-applied functors
For Module F(X:SIG), making now a Include F will try to find the X fields in
the current context, just as was doing earlier Include Self F. This specific
syntax is removed, freeing the keyword "Self". Anyway, with the use of the
syntax "<+" there was already hardly any need for syntax "Include Self".
Idem for Include Type.
Beware that a typo such as "Include F" instead of "Include F G" will
produce a different message now, about a missing field instead of
a not-enough-applied functor.
By the way, some code clean-up and factorisation of inner recursive
functions in declaremods.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12566 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | interp/topconstr.ml | 4 | ||||
-rw-r--r-- | interp/topconstr.mli | 4 | ||||
-rw-r--r-- | library/declaremods.ml | 243 | ||||
-rw-r--r-- | library/declaremods.mli | 2 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 8 | ||||
-rw-r--r-- | parsing/ppvernac.ml | 12 | ||||
-rw-r--r-- | theories/QArith/QOrderedType.v | 4 | ||||
-rw-r--r-- | theories/Structures/DecidableType2.v | 12 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 14 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 2 |
10 files changed, 132 insertions, 173 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index ecb61e15b..3d2e3fde0 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -1024,8 +1024,8 @@ type module_type_ast = | CMTEwith of module_type_ast * with_declaration_ast type include_ast = - | CIMTE of module_type_ast * module_type_ast list - | CIME of module_ast * module_ast list + | CIMTE of module_type_ast list + | CIME of module_ast list type 'a module_signature = | Enforce of 'a (* ... : T *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index b7e389d6b..36f8cfad3 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -257,8 +257,8 @@ type module_type_ast = | CMTEwith of module_type_ast * with_declaration_ast type include_ast = - | CIMTE of module_type_ast * module_type_ast list - | CIME of module_ast * module_ast list + | CIMTE of module_type_ast list + | CIME of module_ast list type 'a module_signature = | Enforce of 'a (* ... : T *) diff --git a/library/declaremods.ml b/library/declaremods.ml index 46c9933c7..62b78af93 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -428,6 +428,22 @@ let rec get_objs_modtype_application env = function Modops.error_application_to_not_path mexpr | _ -> error "Application of a non-functor." +let rec compute_subst env mbids sign mp_l = + match mbids,mp_l with + | _,[] -> mbids,empty_subst + | [],r -> error "Application of a functor with too few arguments." + | mbid::mbids,mp::mp_l -> + let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in + let mb = Environ.lookup_module mp env in + let mbid_left,subst = compute_subst env mbids fbody_b mp_l in + match discr_resolver mb with + | None -> + mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst + | Some mp_delta -> + let mp_delta = Modops.complete_inline_delta_resolver env mp + farg_id farg_b mp_delta in + mbid_left,join (map_mbid mbid mp mp_delta) subst + let rec get_modtype_substobjs env mp_from= function MSEident ln -> MPmap.find ln !modtypetab @@ -439,28 +455,13 @@ let rec get_modtype_substobjs env mp_from= function let substobjs = get_modtype_substobjs env mp_from mty in let modobjs = MPmap.find mp1 !modtab_substobjs in replace_module_object idl substobjs modobjs mp1 - | MSEapply (fexpr, MSEident mp) -> - let (mbids, mp1, objs),mtb_mp1,mp_l = - get_objs_modtype_application env (MSEapply(fexpr, MSEident mp)) in - let rec compute_subst mbids sign mp_l = - match mbids,mp_l with - [],[] -> [],empty_subst - | mbid,[] -> mbid,empty_subst - | [],r -> error ("Application of a functor with too few arguments.") - | mbid::mbids,mp::mp_l -> - let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in - let mb = Environ.lookup_module mp env in - let mp_delta = discr_resolver mb in - let mbid_left,subst=compute_subst mbids fbody_b mp_l in - if mp_delta = None then - mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst - else - let mp_delta = Modops.complete_inline_delta_resolver env mp - farg_id farg_b (Option.get mp_delta) in - mbid_left,join (map_mbid mbid mp mp_delta) subst + | MSEapply (fexpr, MSEident mp) as me -> + let (mbids, mp1, objs),mtb_mp1,mp_l = + get_objs_modtype_application env me in + let mbids_left,subst = + compute_subst env mbids mtb_mp1.typ_expr (List.rev mp_l) in - let mbids_left,subst = compute_subst mbids mtb_mp1.typ_expr (List.rev mp_l) in - (mbids_left, mp1,subst_objects subst objs) + (mbids_left, mp1,subst_objects subst objs) | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr @@ -724,46 +725,14 @@ let rec get_module_substobjs env mp_from = function | MSEfunctor (mbid,mty,mexpr) -> let (mbids, mp, objs) = get_module_substobjs env mp_from mexpr in (mbid::mbids, mp, objs) - | MSEapply (fexpr, MSEident mp) -> - let (mbids, mp1, objs),mb_mp1,mp_l = - get_objs_module_application env (MSEapply(fexpr, MSEident mp)) in - let rec compute_subst mbids sign mp_l = - match mbids,mp_l with - [],[] -> [],empty_subst - | mbid,[] -> mbid,empty_subst - | [],r -> error ("Application of a functor with too few arguments.") - | mbid::mbids,mp::mp_l -> - let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in - let mb = Environ.lookup_module mp env in - let mp_delta = discr_resolver mb in - let mbid_left,subst=compute_subst mbids fbody_b mp_l in - if mp_delta = None then - mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst - else - let mp_delta = Modops.complete_inline_delta_resolver env mp - farg_id farg_b (Option.get mp_delta) in - mbid_left,join (map_mbid mbid mp mp_delta) subst + | MSEapply (fexpr, MSEident mp) as me -> + let (mbids, mp1, objs),mb_mp1,mp_l = + get_objs_module_application env me in - let mbids_left,subst = compute_subst mbids mb_mp1.mod_type (List.rev mp_l) in - (mbids_left, mp1,subst_objects subst objs) - (* let sign,alg,equiv,_ = Mod_typing.translate_struct_module_entry env mp_from fexpr in - let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in - let mb = Environ.lookup_module mp env in - let mp_delta = discr_resolver mb in - let (mbids, mp1, objs) = get_module_substobjs env mp_from fexpr in - (match mbids with - | mbid::mbids -> - if mp_delta = None then - (mbids, mp1,subst_objects (map_mbid mbid mp empty_delta_resolver) objs) - else - let mp_delta = Modops.complete_inline_delta_resolver env mp - farg_id farg_b (Option.get mp_delta) in - (mbids, mp1,subst_objects (map_mbid mbid mp mp_delta) objs) - | [] -> match fexpr with - | MSEident _ -> error "Application of a non-functor." - | _ -> error "Application of a functor with too few arguments.")*) - | MSEapply (_,mexpr) -> - Modops.error_application_to_not_path mexpr + let mbids_left,subst = + compute_subst env mbids mb_mp1.mod_type (List.rev mp_l) in + (mbids_left, mp1,subst_objects subst objs) + | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from mty | MSEwith (mty, With_Module (idl,mp)) -> assert false @@ -885,85 +854,79 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = mmp -let declare_one_include interp_struct me_ast is_mod is_self = +let rec include_subst env mb mbids sign = + match mbids with + | [] -> empty_subst + | mbid::mbids -> + let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in + let subst = include_subst env mb 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 + +exception NothingToDo + +let get_includeself_substobjs env objs me is_mod = + try + let mb_mp = match me with + | MSEident mp -> + if is_mod then + Environ.lookup_module mp env + else + Modops.module_body_of_type mp (Environ.lookup_modtype mp env) + | MSEapply(fexpr, MSEident p) as mexpr -> + let _,mb_mp,mp_l = + if is_mod then + get_objs_module_application env mexpr + else + let o,mtb_mp,mp_l = get_objs_modtype_application env mexpr in + o,Modops.module_body_of_type mtb_mp.typ_mp mtb_mp,mp_l + in + List.fold_left + (fun mb _ -> + match mb.mod_type with + | SEBfunctor(_,_,str) -> {mb with mod_type = str} + | _ -> error "Application of a functor with too much arguments.") + mb_mp mp_l + | _ -> raise NothingToDo + in + let (mbids,mp_self,objects) = objs in + let mb = Global.pack_module() in + let subst = include_subst env mb mbids mb_mp.mod_type in + ([],mp_self,subst_objects subst objects) + with NothingToDo -> objs + +let id_of_mp = function + | MPfile dir -> List.hd (repr_dirpath dir) + | MPbound mbid -> id_of_mbid mbid + | MPdot (_,l) -> id_of_label l + +let declare_one_include interp_struct me_ast is_mod = 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)) - | MSEapply(fexpr, MSEident p) as mexpr -> - let _,mb_mp,mp_l = if is_mod then - get_objs_module_application env mexpr - else - let o,mtb_mp,mp_l = get_objs_modtype_application env mexpr in - o,Modops.module_body_of_type mtb_mp.typ_mp mtb_mp,mp_l in - let mb_mp = - List.fold_left (fun mb _ -> - match mb.mod_type with - | SEBfunctor(_,_,str) -> {mb with mod_type = str} - | _ -> error ("Application of a functor with too much arguments.")) - mb_mp mp_l 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 mbids <> [] then + get_includeself_substobjs env (mbids,mp,objs) me is_mod + else + (mbids,mp,objs) in + let id = current_mod_id() in + let resolver = Global.add_include me is_mod in + let substobjs = (mbids,mp1, + subst_objects (map_mp mp mp1 resolver) objs) in + ignore (add_leaf id + (in_include ((me,is_mod), substobjs))) - 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 - 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 - let substobjs = (mbids,mp1, - subst_objects (map_mp mp mp1 resolver) objs) in - ignore (add_leaf id - (in_include ((me,is_mod), substobjs))) - - -let declare_include_ interp_struct me_ast me_asts is_mod is_self = - declare_one_include interp_struct me_ast is_mod is_self; + +let declare_include_ interp_struct me_asts is_mod = List.iter - (fun me -> declare_one_include interp_struct me is_mod true) + (fun me -> declare_one_include interp_struct me is_mod) me_asts (** Versions of earlier functions taking care of the freeze/unfreeze @@ -976,17 +939,17 @@ let protect_summaries f = (* 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 declare_include interp_struct me_asts is_mod = protect_summaries - (fun _ -> declare_include_ interp_struct me_ast me_asts is_mod is_self) + (fun _ -> declare_include_ interp_struct me_asts is_mod) let declare_modtype interp_mt id args mtys mty_l = let declare_mt fs = match mty_l with | [] -> assert false | [mty] -> declare_modtype_ interp_mt id args mtys mty fs - | mty :: mty_l -> + | mty_l -> ignore (start_modtype_ interp_mt id args mtys fs); - declare_include_ interp_mt mty mty_l false false; + declare_include_ interp_mt mty_l false; end_modtype () in protect_summaries declare_mt @@ -998,9 +961,9 @@ let declare_module interp_mt interp_me id args mtys me_l = let declare_me fs = match me_l with | [] -> declare_module_ interp_mt interp_me id args mtys None fs | [me] -> declare_module_ interp_mt interp_me id args mtys (Some me) fs - | me :: me_l -> + | me_l -> ignore (start_module_ interp_mt None id args mtys fs); - declare_include_ interp_me me me_l true false; + declare_include_ interp_me me_l true; end_module () in protect_summaries declare_me diff --git a/library/declaremods.mli b/library/declaremods.mli index f20be9cd0..ae0b0aa10 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -104,7 +104,7 @@ val import_module : bool -> module_path -> unit (* Include *) val declare_include : (env -> 'struct_expr -> module_struct_entry) -> - 'struct_expr -> 'struct_expr list -> bool -> bool -> unit + 'struct_expr list -> 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 54cf671cc..89d06d2dd 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -396,13 +396,9 @@ GEXTEND Gram | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) | IDENT "Include"; e = module_expr; l = LIST0 ext_module_expr -> - VernacInclude(false,CIME(e,l)) + VernacInclude(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,[])) ] ] + VernacInclude(CIMTE(e::l)) ] ] ; export_token: [ [ IDENT "Import" -> Some false diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 4f31607aa..224b2e2bf 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -762,14 +762,14 @@ let rec pr_vernac = function prlist_strict (fun m -> str " <: " ++ pr_mt m) tyl ++ (if m = [] then mt () else str ":= ") ++ prlist_with_sep (fun () -> str " <+ ") pr_mt m) - | VernacInclude (b,CIMTE(mty,mtys)) -> + | VernacInclude (CIMTE(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)) -> + hov 2 (str"Include Type " ++ + prlist_with_sep (fun () -> str " <+ ") pr_mty mtys) + | VernacInclude (CIME(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)) + hov 2 (str"Include " ++ + prlist_with_sep (fun () -> str " <+ ") pr_me mexprs) (* Solving *) | VernacSolve (i,tac,deftac) -> (if i = 1 then mt() else int i ++ str ": ") ++ diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v index cad77b4eb..c49ded740 100644 --- a/theories/QArith/QOrderedType.v +++ b/theories/QArith/QOrderedType.v @@ -20,8 +20,8 @@ Module Q_as_DT <: DecidableTypeFull. Definition eqb := Qeq_bool. Definition eqb_eq := Qeq_bool_iff. - Include Self Backport_ET_fun. (** eq_refl, eq_sym, eq_trans *) - Include Self Bool2Dec_fun. (** eq_dec *) + Include Backport_ET_fun. (** eq_refl, eq_sym, eq_trans *) + Include Bool2Dec_fun. (** eq_dec *) End Q_as_DT. diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v index afc5b9122..087a6a7dd 100644 --- a/theories/Structures/DecidableType2.v +++ b/theories/Structures/DecidableType2.v @@ -99,16 +99,16 @@ Module UpdateEq (E:BareEquality)(F:IsEqOrig E) <: IsEq E. End UpdateEq. Module Backport_ET (E:EqualityType) <: EqualityTypeBoth - := E <+ BackportEq E E. + := E <+ BackportEq. Module Update_ET (E:EqualityTypeOrig) <: EqualityTypeBoth - := E <+ UpdateEq E E. + := E <+ UpdateEq. Module Backport_DT (E:DecidableType) <: DecidableTypeBoth - := E <+ BackportEq E E. + := E <+ BackportEq. Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth - := E <+ UpdateEq E E. + := E <+ UpdateEq. (** * Having [eq_dec] is equivalent to having [eqb] and its spec. *) @@ -134,10 +134,10 @@ Module HasEqBool2Dec (E:BareEquality)(F:HasEqBool E) <: HasEqDec E. End HasEqBool2Dec. Module Dec2Bool (E:DecidableType) <: BooleanDecidableType - := E <+ HasEqDec2Bool E E. + := E <+ HasEqDec2Bool. Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType - := E <+ HasEqBool2Dec E E. + := E <+ HasEqBool2Dec. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e7d32782d..69a76bcc8 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -550,13 +550,13 @@ let vernac_end_modtype (loc,id) = Dumpglob.dump_modref loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") -let vernac_include is_self = function - | CIMTE (mty,mtys) -> +let vernac_include = function + | CIMTE mtys -> Declaremods.declare_include - Modintern.interp_modtype mty mtys false is_self - | CIME (mexpr, mexprs) -> + Modintern.interp_modtype mtys false + | CIME mexprs -> Declaremods.declare_include - Modintern.interp_modexpr mexpr mexprs true is_self + Modintern.interp_modexpr mexprs true (**********************) (* Gallina extensions *) @@ -1328,8 +1328,8 @@ let interp c = match c with vernac_define_module export lid bl mtys mexprl | VernacDeclareModuleType (lid,bl,mtys,mtyo) -> vernac_declare_module_type lid bl mtys mtyo - | VernacInclude (is_self,in_asts) -> - vernac_include is_self in_asts + | VernacInclude in_asts -> + vernac_include in_asts (* Gallina extensions *) | VernacBeginSection lid -> vernac_begin_section lid diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index f75e1771d..74974c9d1 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -270,7 +270,7 @@ type vernac_expr = module_binder list * module_type_ast module_signature * module_ast list | VernacDeclareModuleType of lident * module_binder list * module_type_ast list * module_type_ast list - | VernacInclude of bool * include_ast + | VernacInclude of include_ast (* Solving *) |