diff options
author | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-01-03 19:25:36 +0000 |
---|---|---|
committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-01-03 19:25:36 +0000 |
commit | 977ed2c9596ce455719521d3bcb2a02fac98ceb8 (patch) | |
tree | ee41075c643a206404e09ec5b127e77abe54832e /library/declaremods.ml | |
parent | 0c9329df2466c38b5cea09426e1981dc35278fa2 (diff) |
HUGE COMMIT
1. when applying a functor F(X) := B to a module M, the obtained module
is no longer B{X.t := M.t for all t}, but B{X.t := b where b is the
body of t in M}. In principle it is now easy to fine tune the behaviour
to choose whether b or M.t must be used. This change implies modifications
both inside and outside the kernel.
2. for each object in the library it is now necessary to define the behaviour
w.r.t. the substitution {X.t := b}. Notice that in many many cases the
pre-existing behaviour w.r.t. the substitution {X.t := M.t} was broken
(in the sense that it used to break several invariants). This commit
fixes the behaviours for most of the objects, excluded
a) coercions: a future commit should allow any term to be declared
as a coercion; moreover the invariant that just a coercion path
exists between two classes will be broken by the instantiation.
b) global references when used as arguments of a few tactics/commands
In all the other cases the behaviour implemented is the one that looks
to me as the one expected by the user (if possible):
[ terminology: not expanded (X.t := M.t) vs expanded (X.t := b) ]
a) argument scopes: not expanded
b) SYNTAXCONSTANT: expanded
c) implicit arguments: not expanded
d) coercions: expansion to be done (for now not expanded)
e) concrete syntax tree for patterns: expanded
f) concrete syntax tree for raw terms: expanded
g) evaluable references (used by unfold, delta expansion, etc.): not
expanded
h) auto's hints: expanded when possible (i.e. when the expansion of the
head of the pattern is rigid)
i) realizers (for program extraction): nothing is done since the actual
code does not look for the realizer of definitions with a body;
however this solution is fragile.
l) syntax and notation: expanded
m) structures and canonical structures: an invariant says that no
parameter can happear in them ==> the substitution always yelds the
original term
n) stuff related to V7 syntax: since this part of the code is doomed
to disappear, I have made no effort to fix a reasonable semantics;
not expanded is the default one applied
o) RefArgTypes: to be understood. For now a warning is issued whether
expanded != not expanded, and the not expanded solution is chosen.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6555 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.ml')
-rw-r--r-- | library/declaremods.ml | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index e1a27314f..ddcfd1bcd 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -698,21 +698,25 @@ let declare_modtype interp_modtype id args mty = ignore (add_leaf id (in_modtype (Some entry, substobjs))) - -let rec get_module_substobjs = function +let rec get_module_substobjs env = function | MEident mp -> MPmap.find mp !modtab_substobjs | MEfunctor (mbid,mty,mexpr) -> - let (subst, mbids, msid, objs) = - get_module_substobjs mexpr - in + let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (subst, mbid::mbids, msid, objs) | MEstruct (msid,_) -> (empty_subst, [], msid, []) | MEapply (mexpr, MEident mp) -> - let (subst, mbids, msid, objs) = get_module_substobjs mexpr in + let feb,ftb = Mod_typing.translate_mexpr env mexpr in + let ftb = Modops.scrape_modtype env ftb in + let farg_id, farg_b, fbody_b = Modops.destr_functor ftb in + let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (match mbids with | mbid::mbids -> - (add_mbid mbid mp subst, mbids, msid, objs) + let resolve = + Modops.resolver_of_environment farg_id farg_b mp env in + (* application outside the kernel, only for substitutive + objects (that are all non-logical objects) *) + (add_mbid mbid mp (Some resolve) subst, mbids, msid, objs) | [] -> match mexpr with | MEident _ | MEstruct _ -> error "Application of a non-functor" | _ -> error "Application of a functor with too few arguments") @@ -758,7 +762,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = let substobjs = match entry with | {mod_entry_type = Some mte} -> get_modtype_substobjs mte - | {mod_entry_expr = Some mexpr} -> get_module_substobjs mexpr + | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mexpr | _ -> anomaly "declare_module: No type, no body ..." in Summary.unfreeze_summaries fs; |