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

4 files changed, 101 insertions, 97 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 60e16e709..f90219b24 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -369,7 +369,7 @@ let cache_arguments_scope (_,(r,scl)) =
   List.iter (option_iter check_scope) scl;
   arguments_scope := Refmap.add r scl !arguments_scope
 
-let subst_arguments_scope (_,subst,(r,scl)) = (subst_global subst r,scl)
+let subst_arguments_scope (_,subst,(r,scl)) = (fst (subst_global subst r),scl)
 
 let (inArgumentsScope,outArgumentsScope) = 
   declare_object {(default_object "ARGUMENTS-SCOPE") with
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index f2a31f9de..17c0e96c8 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -48,7 +48,7 @@ let cache_syntax_constant d =
   load_syntax_constant 1 d
 
 let subst_syntax_constant ((sp,kn),subst,(local,c,onlyparse)) =
-  (local,subst_aconstr subst c,onlyparse)
+  (local,subst_aconstr subst [] c,onlyparse)
 
 let classify_syntax_constant (_,(local,_,_ as o)) =
   if local then Dispose else Substitute o
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 56e2171e9..f18be16cc 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -111,100 +111,6 @@ let rec subst_pat subst pat =
         if kn' == kn && cpl' == cpl then pat else
           PatCstr (loc,((kn',i),j),cpl',n)
 
-let rec subst_aconstr subst raw =
-  match raw with
-  | ARef ref -> 
-      let ref' = subst_global subst ref in 
-	if ref' == ref then raw else
-	  ARef ref'
-
-  | AVar _ -> raw
-
-  | AApp (r,rl) -> 
-      let r' = subst_aconstr subst r 
-      and rl' = list_smartmap (subst_aconstr subst) rl in
-	if r' == r && rl' == rl then raw else
-	  AApp(r',rl')
-
-  | AList (id1,id2,r1,r2,b) -> 
-      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  AList (id1,id2,r1',r2',b)
-
-  | ALambda (n,r1,r2) -> 
-      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  ALambda (n,r1',r2')
-
-  | AProd (n,r1,r2) -> 
-      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  AProd (n,r1',r2')
-
-  | ALetIn (n,r1,r2) -> 
-      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  ALetIn (n,r1',r2')
-
-  | ACases (ro,rtntypopt,rl,branches) -> 
-      let ro' = option_smartmap (subst_aconstr subst) ro 
-      and rtntypopt' = option_smartmap (subst_aconstr subst) rtntypopt
-      and rl' = list_smartmap
-        (fun (a,(n,signopt) as x) -> 
-	  let a' = subst_aconstr subst a in
-	  let signopt' = option_app (fun ((indkn,i),nal as z) ->
-	    let indkn' = subst_kn subst indkn in
-	    if indkn == indkn' then z else ((indkn',i),nal)) signopt in
-	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
-        rl
-      and branches' = list_smartmap 
-                        (fun (idl,cpl,r as branch) ->
-                           let cpl' = list_smartmap (subst_pat subst) cpl
-                           and r' = subst_aconstr subst r in
-                             if cpl' == cpl && r' == r then branch else
-                               (idl,cpl',r'))
-                        branches
-      in
-        if ro' == ro && rtntypopt == rtntypopt' &
-          rl' == rl && branches' == branches then raw else
-          ACases (ro',rtntypopt',rl',branches')
-
-  | AOrderedCase (b,ro,r,ra) -> 
-      let ro' = option_smartmap (subst_aconstr subst) ro
-      and r' = subst_aconstr subst r 
-      and ra' = array_smartmap (subst_aconstr subst) ra in
-	if ro' == ro && r' == r && ra' == ra then raw else
-	  AOrderedCase (b,ro',r',ra')
-
-  | ALetTuple (nal,(na,po),b,c) ->
-      let po' = option_smartmap (subst_aconstr subst) po
-      and b' = subst_aconstr subst b 
-      and c' = subst_aconstr subst c in
-	if po' == po && b' == b && c' == c then raw else
-	  ALetTuple (nal,(na,po'),b',c')
-
-  | AIf (c,(na,po),b1,b2) ->
-      let po' = option_smartmap (subst_aconstr subst) po
-      and b1' = subst_aconstr subst b1
-      and b2' = subst_aconstr subst b2 
-      and c' = subst_aconstr subst c in
-	if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
-	  AIf (c',(na,po'),b1',b2')
-
-  | APatVar _ | ASort _ -> raw
-
-  | AHole (Evd.ImplicitArg (ref,i)) ->
-      let ref' = subst_global subst ref in 
-	if ref' == ref then raw else
-	  AHole (Evd.ImplicitArg (ref',i))
-  | AHole (Evd.BinderType _ | Evd.QuestionMark | Evd.CasesType |
-      Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw
-
-  | ACast (r1,r2) -> 
-      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  ACast (r1',r2')
-
 let add_name r = function
   | Anonymous -> ()
   | Name id -> r := id :: !r
@@ -334,6 +240,104 @@ let aconstr_of_rawconstr vars a =
   List.iter check_type vars;
   a
 
+let aconstr_of_constr avoiding t =
+ aconstr_of_rawconstr [] (Detyping.detype (false,Global.env()) avoiding [] t)
+
+let rec subst_aconstr subst bound raw =
+  match raw with
+  | ARef ref -> 
+      let ref',t = subst_global subst ref in 
+	if ref' == ref then raw else
+	  aconstr_of_constr bound t
+
+  | AVar _ -> raw
+
+  | AApp (r,rl) -> 
+      let r' = subst_aconstr subst bound r 
+      and rl' = list_smartmap (subst_aconstr subst bound) rl in
+	if r' == r && rl' == rl then raw else
+	  AApp(r',rl')
+
+  | AList (id1,id2,r1,r2,b) -> 
+      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  AList (id1,id2,r1',r2',b)
+
+  | ALambda (n,r1,r2) -> 
+      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  ALambda (n,r1',r2')
+
+  | AProd (n,r1,r2) -> 
+      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  AProd (n,r1',r2')
+
+  | ALetIn (n,r1,r2) -> 
+      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  ALetIn (n,r1',r2')
+
+  | ACases (ro,rtntypopt,rl,branches) -> 
+      let ro' = option_smartmap (subst_aconstr subst bound) ro 
+      and rtntypopt' = option_smartmap (subst_aconstr subst bound) rtntypopt
+      and rl' = list_smartmap
+        (fun (a,(n,signopt) as x) -> 
+	  let a' = subst_aconstr subst bound a in
+	  let signopt' = option_app (fun ((indkn,i),nal as z) ->
+	    let indkn' = subst_kn subst indkn in
+	    if indkn == indkn' then z else ((indkn',i),nal)) signopt in
+	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
+        rl
+      and branches' = list_smartmap 
+                        (fun (idl,cpl,r as branch) ->
+                           let cpl' = list_smartmap (subst_pat subst) cpl
+                           and r' = subst_aconstr subst bound r in
+                             if cpl' == cpl && r' == r then branch else
+                               (idl,cpl',r'))
+                        branches
+      in
+        if ro' == ro && rtntypopt == rtntypopt' &
+          rl' == rl && branches' == branches then raw else
+          ACases (ro',rtntypopt',rl',branches')
+
+  | AOrderedCase (b,ro,r,ra) -> 
+      let ro' = option_smartmap (subst_aconstr subst bound) ro
+      and r' = subst_aconstr subst bound r 
+      and ra' = array_smartmap (subst_aconstr subst bound) ra in
+	if ro' == ro && r' == r && ra' == ra then raw else
+	  AOrderedCase (b,ro',r',ra')
+
+  | ALetTuple (nal,(na,po),b,c) ->
+      let po' = option_smartmap (subst_aconstr subst bound) po
+      and b' = subst_aconstr subst bound b 
+      and c' = subst_aconstr subst bound c in
+	if po' == po && b' == b && c' == c then raw else
+	  ALetTuple (nal,(na,po'),b',c')
+
+  | AIf (c,(na,po),b1,b2) ->
+      let po' = option_smartmap (subst_aconstr subst bound) po
+      and b1' = subst_aconstr subst bound b1
+      and b2' = subst_aconstr subst bound b2 
+      and c' = subst_aconstr subst bound c in
+	if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
+	  AIf (c',(na,po'),b1',b2')
+
+  | APatVar _ | ASort _ -> raw
+
+  | AHole (Evd.ImplicitArg (ref,i)) ->
+      let ref',t = subst_global subst ref in 
+	if ref' == ref then raw else
+	  AHole (Evd.InternalHole)
+  | AHole (Evd.BinderType _ | Evd.QuestionMark | Evd.CasesType |
+      Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw
+
+  | ACast (r1,r2) -> 
+      let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  ACast (r1',r2')
+
+
 let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
 
 (* Pattern-matching rawconstr and aconstr *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 152a54dc0..9b9dd80dc 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -48,7 +48,7 @@ val rawconstr_of_aconstr_with_binders : loc ->
   (identifier -> 'a -> identifier * 'a) ->
   ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
 
-val subst_aconstr : substitution -> aconstr -> aconstr
+val subst_aconstr : substitution -> Names.identifier list -> aconstr -> aconstr
 
 val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr