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

7 files changed, 205 insertions, 188 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index aef35cd7cf..66ed81d021 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -153,21 +153,35 @@ let lookup_pattern_path_between (s,t) =
 	 | Construct sp -> (sp, coe.coe_param)
 	 | _ -> raise Not_found) l
 
+(* find_class_type : constr -> cl_typ * int *)
+
+let find_class_type t =
+  let t', args = decompose_app (Reductionops.whd_betaiotazeta t) in
+  match kind_of_term t' with
+    | Var id -> CL_SECVAR id, args
+    | Const sp -> CL_CONST sp, args
+    | Ind ind_sp -> CL_IND ind_sp, args
+    | Prod (_,_,_) -> CL_FUN, []
+    | Sort _ -> CL_SORT, []
+    |  _ -> raise Not_found
+
 
 let subst_cl_typ subst ct = match ct with
     CL_SORT
   | CL_FUN
   | CL_SECVAR _ -> ct
   | CL_CONST kn -> 
-      let kn' = subst_con subst kn in 
+      let kn',t = subst_con subst kn in 
 	if kn' == kn then ct else
-	  CL_CONST kn'
+         fst (find_class_type t)
   | CL_IND (kn,i) ->
       let kn' = subst_kn subst kn in 
 	if kn' == kn then ct else
 	  CL_IND (kn',i)
 
-let subst_coe_typ = subst_global
+(*CSC: here we should change the datatype for coercions: it should be possible
+       to declare any term as a coercion *)
+let subst_coe_typ subst t = fst (subst_global subst t)
 
 let subst_coe_info subst info = 
   let jud = info.coe_value in
@@ -209,18 +223,6 @@ let _ =
 
 (* classe d'un terme *)
 
-(* find_class_type : constr -> cl_typ * int *)
-
-let find_class_type t =
-  let t', args = decompose_app (Reductionops.whd_betaiotazeta t) in
-  match kind_of_term t' with
-    | Var id -> CL_SECVAR id, args
-    | Const sp -> CL_CONST sp, args
-    | Ind ind_sp -> CL_IND ind_sp, args
-    | Prod (_,_,_) -> CL_FUN, []
-    | Sort _ -> CL_SORT, []
-    |  _ -> raise Not_found
-
 (* class_of : Term.constr -> int *)
 
 let class_of env sigma t = 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6a0ea00602..880605313a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -492,3 +492,117 @@ and detype_binder tenv bk avoid env na ty c =
     | BProd -> RProd (dummy_loc, na',detype tenv [] env ty, r)
     | BLambda -> RLambda (dummy_loc, na',detype tenv [] env ty, r)
     | BLetIn -> RLetIn (dummy_loc, na',detype tenv [] env ty, r)
+
+let rec subst_pat subst pat = 
+  match pat with
+  | PatVar _ -> pat
+  | PatCstr (loc,((kn,i),j),cpl,n) -> 
+      let kn' = subst_kn subst kn 
+      and cpl' = list_smartmap (subst_pat subst) cpl in
+	if kn' == kn && cpl' == cpl then pat else
+	  PatCstr (loc,((kn',i),j),cpl',n)
+
+let rec subst_raw subst raw = 
+  match raw with
+  | RRef (loc,ref) -> 
+      let ref',t = subst_global subst ref in 
+	if ref' == ref then raw else
+         detype (false,Global.env ()) [] [] t
+
+  | RVar _ -> raw
+  | REvar _ -> raw
+  | RPatVar _ -> raw
+
+  | RApp (loc,r,rl) -> 
+      let r' = subst_raw subst r 
+      and rl' = list_smartmap (subst_raw subst) rl in
+	if r' == r && rl' == rl then raw else
+	  RApp(loc,r',rl')
+
+  | RLambda (loc,n,r1,r2) -> 
+      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  RLambda (loc,n,r1',r2')
+
+  | RProd (loc,n,r1,r2) -> 
+      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  RProd (loc,n,r1',r2')
+
+  | RLetIn (loc,n,r1,r2) -> 
+      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  RLetIn (loc,n,r1',r2')
+
+  | RCases (loc,(ro,rtno),rl,branches) -> 
+      let ro' = option_smartmap (subst_raw subst) ro 
+      and rtno' = ref (option_smartmap (subst_raw subst) !rtno)
+      and rl' = list_smartmap (fun (a,x as y) ->
+        let a' = subst_raw subst a in
+        let (n,topt) = !x in 
+        let topt' = option_smartmap
+          (fun (loc,(sp,i),x as t) ->
+            let sp' = subst_kn subst sp in
+            if sp == sp' then t else (loc,(sp',i),x)) topt in
+        if a == a' && topt == topt' then y else (a',ref (n,topt'))) rl
+      and branches' = list_smartmap 
+			(fun (loc,idl,cpl,r as branch) ->
+			   let cpl' = list_smartmap (subst_pat subst) cpl
+			   and r' = subst_raw subst r in
+			     if cpl' == cpl && r' == r then branch else
+			       (loc,idl,cpl',r'))
+			branches
+      in
+	if ro' == ro && rl' == rl && branches' == branches then raw else
+	  RCases (loc,(ro',rtno'),rl',branches')
+
+  | ROrderedCase (loc,b,ro,r,ra,x) -> 
+      let ro' = option_smartmap (subst_raw subst) ro
+      and r' = subst_raw subst r 
+      and ra' = array_smartmap (subst_raw subst) ra in
+	if ro' == ro && r' == r && ra' == ra then raw else
+	  ROrderedCase (loc,b,ro',r',ra',x)
+
+  | RLetTuple (loc,nal,(na,po),b,c) ->
+      let po' = option_smartmap (subst_raw subst) po
+      and b' = subst_raw subst b 
+      and c' = subst_raw subst c in
+	if po' == po && b' == b && c' == c then raw else
+          RLetTuple (loc,nal,(na,po'),b',c')
+      
+  | RIf (loc,c,(na,po),b1,b2) ->
+      let po' = option_smartmap (subst_raw subst) po
+      and b1' = subst_raw subst b1 
+      and b2' = subst_raw subst b2 
+      and c' = subst_raw subst c in
+	if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else
+          RIf (loc,c',(na,po'),b1',b2')
+
+  | RRec (loc,fix,ida,bl,ra1,ra2) -> 
+      let ra1' = array_smartmap (subst_raw subst) ra1
+      and ra2' = array_smartmap (subst_raw subst) ra2 in
+      let bl' = array_smartmap
+        (list_smartmap (fun (na,obd,ty as dcl) ->
+          let ty' = subst_raw subst ty in
+          let obd' = option_smartmap (subst_raw subst) obd in
+          if ty'==ty & obd'==obd then dcl else (na,obd',ty')))
+        bl in
+	if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
+	  RRec (loc,fix,ida,bl',ra1',ra2')
+
+  | RSort _ -> raw
+
+  | RHole (loc,ImplicitArg (ref,i)) ->
+      let ref',_ = subst_global subst ref in 
+	if ref' == ref then raw else
+	  RHole (loc,InternalHole)
+  | RHole (loc, (BinderType _ | QuestionMark | CasesType |
+      InternalHole | TomatchTypeParameter _)) -> raw
+
+  | RCast (loc,r1,r2) -> 
+      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  RCast (loc,r1',r2')
+
+  | RDynamic _ -> raw
+
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 15743e7bf8..e4aa8a6573 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -16,8 +16,11 @@ open Sign
 open Environ
 open Rawterm
 open Termops
+open Mod_subst
 (*i*)
 
+val subst_raw : substitution -> rawconstr -> rawconstr
+
 (* [detype env avoid nenv c] turns [c], typed in [env], into a rawconstr. *)
 (* De Bruijn indexes are turned to bound names, avoiding names in [avoid] *)
 
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index b091d797ad..6e06f978f2 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -63,56 +63,11 @@ let rec occur_meta_pattern = function
   | PMeta _ | PSoApp _ -> true
   | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
 
-let rec subst_pattern subst pat = match pat with
-  | PRef ref ->
-      let ref' = subst_global subst ref in
-	if ref' == ref then pat else 
-	  PRef ref'
-  | PVar _ 
-  | PEvar _
-  | PRel _ -> pat
-  | PApp (f,args) ->
-      let f' = subst_pattern subst f in 
-      let args' = array_smartmap (subst_pattern subst) args in
-	if f' == f && args' == args then pat else
-	  PApp (f',args')
-  | PSoApp (i,args) ->
-      let args' = list_smartmap (subst_pattern subst) args in
-	if args' == args then pat else
-	  PSoApp (i,args')
-  | PLambda (name,c1,c2) ->
-      let c1' = subst_pattern subst c1 in
-      let c2' = subst_pattern subst c2 in
-	if c1' == c1 && c2' == c2 then pat else
-	  PLambda (name,c1',c2')
-  | PProd (name,c1,c2) ->
-      let c1' = subst_pattern subst c1 in
-      let c2' = subst_pattern subst c2 in
-	if c1' == c1 && c2' == c2 then pat else
-	  PProd (name,c1',c2')
-  | PLetIn (name,c1,c2) ->
-      let c1' = subst_pattern subst c1 in
-      let c2' = subst_pattern subst c2 in
-	if c1' == c1 && c2' == c2 then pat else
-	  PLetIn (name,c1',c2')
-  | PSort _ 
-  | PMeta _ -> pat
-  | PCase (cs,typ, c, branches) -> 
-      let typ' = option_smartmap (subst_pattern subst) typ in 
-      let c' = subst_pattern subst c in
-      let branches' = array_smartmap (subst_pattern subst) branches in
-	if typ' == typ && c' == c && branches' == branches then pat else
-	  PCase(cs,typ', c', branches') 
-  | PFix fixpoint ->
-      let cstr = mkFix fixpoint in
-      let fixpoint' = destFix (subst_mps subst cstr) in
-	if fixpoint' == fixpoint then pat else
-	  PFix fixpoint'
-  | PCoFix cofixpoint ->
-      let cstr = mkCoFix cofixpoint in
-      let cofixpoint' = destCoFix (subst_mps subst cstr) in
-	if cofixpoint' == cofixpoint then pat else
-	  PCoFix cofixpoint'
+type constr_label =
+  | ConstNode of constant
+  | IndNode of inductive
+  | CstrNode of constructor
+  | VarNode of identifier
 
 exception BoundPattern;;
 
@@ -177,6 +132,58 @@ let rec inst lvar = function
   | (PFix _ | PCoFix _ as r) ->
       error ("Not instantiable pattern")
 
+let rec subst_pattern subst pat = match pat with
+  | PRef ref ->
+      let ref',t = subst_global subst ref in
+	if ref' == ref then pat else
+	 pattern_of_constr t
+  | PVar _ 
+  | PEvar _
+  | PRel _ -> pat
+  | PApp (f,args) ->
+      let f' = subst_pattern subst f in 
+      let args' = array_smartmap (subst_pattern subst) args in
+	if f' == f && args' == args then pat else
+	  PApp (f',args')
+  | PSoApp (i,args) ->
+      let args' = list_smartmap (subst_pattern subst) args in
+	if args' == args then pat else
+	  PSoApp (i,args')
+  | PLambda (name,c1,c2) ->
+      let c1' = subst_pattern subst c1 in
+      let c2' = subst_pattern subst c2 in
+	if c1' == c1 && c2' == c2 then pat else
+	  PLambda (name,c1',c2')
+  | PProd (name,c1,c2) ->
+      let c1' = subst_pattern subst c1 in
+      let c2' = subst_pattern subst c2 in
+	if c1' == c1 && c2' == c2 then pat else
+	  PProd (name,c1',c2')
+  | PLetIn (name,c1,c2) ->
+      let c1' = subst_pattern subst c1 in
+      let c2' = subst_pattern subst c2 in
+	if c1' == c1 && c2' == c2 then pat else
+	  PLetIn (name,c1',c2')
+  | PSort _ 
+  | PMeta _ -> pat
+  | PCase (cs,typ, c, branches) -> 
+      let typ' = option_smartmap (subst_pattern subst) typ in 
+      let c' = subst_pattern subst c in
+      let branches' = array_smartmap (subst_pattern subst) branches in
+	if typ' == typ && c' == c && branches' == branches then pat else
+	  PCase(cs,typ', c', branches') 
+  | PFix fixpoint ->
+      let cstr = mkFix fixpoint in
+      let fixpoint' = destFix (subst_mps subst cstr) in
+	if fixpoint' == fixpoint then pat else
+	  PFix fixpoint'
+  | PCoFix cofixpoint ->
+      let cstr = mkCoFix cofixpoint in
+      let cofixpoint' = destCoFix (subst_mps subst cstr) in
+	if cofixpoint' == cofixpoint then pat else
+	  PCoFix cofixpoint'
+
+
 let instantiate_pattern = inst
 
 let rec pat_of_raw metas vars = function
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 054312ff34..b915313951 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -16,7 +16,6 @@ open Term
 open Libnames
 open Nametab
 open Evd
-open Mod_subst
 (*i*)
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
@@ -196,119 +195,6 @@ let occur_rawconstr id =
 
   in occur
 
-let rec subst_pat subst pat = 
-  match pat with
-  | PatVar _ -> pat
-  | PatCstr (loc,((kn,i),j),cpl,n) -> 
-      let kn' = subst_kn subst kn 
-      and cpl' = list_smartmap (subst_pat subst) cpl in
-	if kn' == kn && cpl' == cpl then pat else
-	  PatCstr (loc,((kn',i),j),cpl',n)
-
-let rec subst_raw subst raw = 
-  match raw with
-  | RRef (loc,ref) -> 
-      let ref' = subst_global subst ref in 
-	if ref' == ref then raw else
-	  RRef (loc,ref')
-
-  | RVar _ -> raw
-  | REvar _ -> raw
-  | RPatVar _ -> raw
-
-  | RApp (loc,r,rl) -> 
-      let r' = subst_raw subst r 
-      and rl' = list_smartmap (subst_raw subst) rl in
-	if r' == r && rl' == rl then raw else
-	  RApp(loc,r',rl')
-
-  | RLambda (loc,n,r1,r2) -> 
-      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  RLambda (loc,n,r1',r2')
-
-  | RProd (loc,n,r1,r2) -> 
-      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  RProd (loc,n,r1',r2')
-
-  | RLetIn (loc,n,r1,r2) -> 
-      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  RLetIn (loc,n,r1',r2')
-
-  | RCases (loc,(ro,rtno),rl,branches) -> 
-      let ro' = option_smartmap (subst_raw subst) ro 
-      and rtno' = ref (option_smartmap (subst_raw subst) !rtno)
-      and rl' = list_smartmap (fun (a,x as y) ->
-        let a' = subst_raw subst a in
-        let (n,topt) = !x in 
-        let topt' = option_smartmap
-          (fun (loc,(sp,i),x as t) ->
-            let sp' = subst_kn subst sp in
-            if sp == sp' then t else (loc,(sp',i),x)) topt in
-        if a == a' && topt == topt' then y else (a',ref (n,topt'))) rl
-      and branches' = list_smartmap 
-			(fun (loc,idl,cpl,r as branch) ->
-			   let cpl' = list_smartmap (subst_pat subst) cpl
-			   and r' = subst_raw subst r in
-			     if cpl' == cpl && r' == r then branch else
-			       (loc,idl,cpl',r'))
-			branches
-      in
-	if ro' == ro && rl' == rl && branches' == branches then raw else
-	  RCases (loc,(ro',rtno'),rl',branches')
-
-  | ROrderedCase (loc,b,ro,r,ra,x) -> 
-      let ro' = option_smartmap (subst_raw subst) ro
-      and r' = subst_raw subst r 
-      and ra' = array_smartmap (subst_raw subst) ra in
-	if ro' == ro && r' == r && ra' == ra then raw else
-	  ROrderedCase (loc,b,ro',r',ra',x)
-
-  | RLetTuple (loc,nal,(na,po),b,c) ->
-      let po' = option_smartmap (subst_raw subst) po
-      and b' = subst_raw subst b 
-      and c' = subst_raw subst c in
-	if po' == po && b' == b && c' == c then raw else
-          RLetTuple (loc,nal,(na,po'),b',c')
-      
-  | RIf (loc,c,(na,po),b1,b2) ->
-      let po' = option_smartmap (subst_raw subst) po
-      and b1' = subst_raw subst b1 
-      and b2' = subst_raw subst b2 
-      and c' = subst_raw subst c in
-	if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else
-          RIf (loc,c',(na,po'),b1',b2')
-
-  | RRec (loc,fix,ida,bl,ra1,ra2) -> 
-      let ra1' = array_smartmap (subst_raw subst) ra1
-      and ra2' = array_smartmap (subst_raw subst) ra2 in
-      let bl' = array_smartmap
-        (list_smartmap (fun (na,obd,ty as dcl) ->
-          let ty' = subst_raw subst ty in
-          let obd' = option_smartmap (subst_raw subst) obd in
-          if ty'==ty & obd'==obd then dcl else (na,obd',ty')))
-        bl in
-	if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
-	  RRec (loc,fix,ida,bl',ra1',ra2')
-
-  | RSort _ -> raw
-
-  | RHole (loc,ImplicitArg (ref,i)) ->
-      let ref' = subst_global subst ref in 
-	if ref' == ref then raw else
-	  RHole (loc,ImplicitArg (ref',i))
-  | RHole (loc, (BinderType _ | QuestionMark | CasesType |
-      InternalHole | TomatchTypeParameter _)) -> raw
-
-  | RCast (loc,r1,r2) -> 
-      let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  RCast (loc,r1',r2')
-
-  | RDynamic _ -> raw
-
 let loc_of_rawconstr = function
   | RRef (loc,_) -> loc
   | RVar (loc,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 127eb1dc6d..759e0adb6c 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -15,7 +15,6 @@ open Sign
 open Term
 open Libnames
 open Nametab
-open Mod_subst
 (*i*)
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
@@ -100,8 +99,6 @@ val occur_rawconstr : identifier -> rawconstr -> bool
 
 val loc_of_rawconstr : rawconstr -> loc
 
-val subst_raw : substitution -> rawconstr -> rawconstr
-
 type 'a raw_red_flag = {
   rBeta : bool;
   rIota : bool;
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 4cbd02ca4d..cc53ae7f3f 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -47,9 +47,12 @@ let cache_structure (_,(ind,struc)) =
 
 let subst_structure (_,subst,((kn,i),struc as obj)) = 
   let kn' = subst_kn subst kn in
-  let proj' = list_smartmap 
-		(option_smartmap (subst_con subst)) 
-		struc.s_PROJ 
+  let proj' =
+   (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
+   (* the first component of subst_con.                                   *)
+   list_smartmap 
+    (option_smartmap (fun kn -> fst (subst_con subst kn)))
+    struc.s_PROJ
   in
     if proj' == struc.s_PROJ && kn' == kn then obj else
       (kn',i),{struc with s_PROJ = proj'}
@@ -120,14 +123,19 @@ let cache_canonical_structure (_,(cst,lo)) =
       object_table := x :: (!object_table)) lo
 
 let subst_object subst ((r1,r2),o as obj) = 
-  let r1' = subst_global subst r1 in
-  let r2' = subst_global subst r2 in
+  (* invariant: r1 and r2 are evaluable references. Thus subst_global   *)
+  (* cannot instantiate them. Hence we can use just the first component *)
+  (* of the answer.                                                     *)
+  let r1',_ = subst_global subst r1 in
+  let r2',_ = subst_global subst r2 in
   let o' = subst_obj subst o in
   if r1' == r1 && r2' == r2 && o' == o then obj
   else (r1',r2'),o'
 
 let subst_canonical_structure (_,subst,(cst,lo as obj)) =
-  let cst' = subst_con subst cst in
+  (* invariant: cst is an evaluable reference. Thus we can take *)
+  (* the first component of subst_con.                                   *)
+  let cst' = fst (subst_con subst cst) in
   let lo' = list_smartmap (subst_object subst) lo in
   if cst' == cst & lo' == lo then obj else (cst',lo')