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

6 files changed, 56 insertions, 54 deletions

diff --git a/parsing/ast.ml b/parsing/ast.ml
index e366600c8..eef1ca4b7 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -588,22 +588,3 @@ let rec occur_var_ast s = function
   | Slam(_,sopt,body) -> (Some s <> sopt) & occur_var_ast s body
   | Id _ | Str _ | Num _ | Path _ | ConPath _ -> false
   | Dynamic _ -> (* Hum... what to do here *) false
-
-
-(**********************************************************************)
-(* Object substitution in modules *)
-
-let rec subst_astpat subst = function
-  | Pquote a -> Pquote (subst_ast subst a)
-  | Pmeta _ as p -> p
-  | Pnode (s,pl) -> Pnode (s,subst_astpatlist subst pl)
-  | Pslam (ido,p) -> Pslam (ido,subst_astpat subst p)
-  | Pmeta_slam (s,p) -> Pmeta_slam (s,subst_astpat subst p)
-
-and subst_astpatlist subst = function
-  | Pcons (p,pl) -> Pcons (subst_astpat subst p, subst_astpatlist subst pl)
-  | (Plmeta _ | Pnil) as pl -> pl
-
-let subst_pat subst = function
-  | AstListPat pl -> AstListPat (subst_astpatlist subst pl)
-  | PureAstPat p -> PureAstPat (subst_astpat subst p)
diff --git a/parsing/ast.mli b/parsing/ast.mli
index b915c6552..9c7eec43c 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -46,7 +46,7 @@ val meta_of_ast : Coqast.t -> string
 
 (* patterns of ast *)
 type astpat =
-  | Pquote of t
+  | Pquote of Coqast.t
   | Pmeta of string * tok_kind
   | Pnode of string * patlist
   | Pslam of identifier option * astpat
@@ -119,6 +119,3 @@ val find_all_matches : ('a -> astpat) -> env -> t -> 'a list -> ('a * env) list
 val first_matchl : ('a -> patlist) -> env -> Coqast.t list -> 'a list ->
   ('a * env) option
 val to_pat : entry_env -> Coqast.t -> (astpat * entry_env)
-
-(* Object substitution in modules *)
-val subst_astpat : substitution -> astpat -> astpat
diff --git a/parsing/coqast.ml b/parsing/coqast.ml
index a80982f8a..3811dd322 100644
--- a/parsing/coqast.ml
+++ b/parsing/coqast.ml
@@ -102,31 +102,3 @@ let hcons_ast (hstr,hid,hpath,hconpath) =
   let hloc = Hashcons.simple_hcons Hloc.f () in
   let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr,hid,hpath,hconpath) in
   (hast,hloc)
-
-let rec subst_ast subst ast = match ast with
-  | Node (l,s,astl) ->
-      let astl' = Util.list_smartmap (subst_ast subst) astl in
-	if astl' == astl then ast else
-	  Node (l,s,astl')
-  | Slam (l,ido,ast1) ->
-      let ast1' = subst_ast subst ast1 in
-	if ast1' == ast1 then ast else
-	  Slam (l,ido,ast1')
-  | Smetalam (l,s,ast1) ->
-      let ast1' = subst_ast subst ast1 in
-	if ast1' == ast1 then ast else
-	  Smetalam (l,s,ast1')
-  | Path (loc,kn) -> 
-      let kn' = subst_kn subst kn in
-	if kn' == kn then ast else
-	  Path(loc,kn')
-  | ConPath (loc,kn) -> 
-      let kn' = subst_con subst kn in
-	if kn' == kn then ast else
-	  ConPath(loc,kn')
-  | Nmeta _
-  | Nvar _ -> ast
-  | Num _
-  | Str _
-  | Id _
-  | Dynamic _ -> ast
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
index a769c66f9..b588d9cea 100644
--- a/parsing/coqast.mli
+++ b/parsing/coqast.mli
@@ -12,7 +12,6 @@
 open Util
 open Names
 open Libnames
-open Mod_subst
 (*i*)
 
 (* Abstract syntax trees. *)
@@ -43,8 +42,6 @@ val hcons_ast:
   * (kernel_name -> kernel_name) * (constant -> constant)
   -> (t -> t) * (loc -> loc)
 
-val subst_ast: substitution -> t -> t
-
 (*
 val map_tactic_expr : (t -> t) -> (tactic_expr -> tactic_expr) -> tactic_expr -> tactic_expr
 val fold_tactic_expr :
diff --git a/parsing/termast.ml b/parsing/termast.ml
index efa6c9206..ace1b47d2 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -26,6 +26,7 @@ open Ast
 open Rawterm
 open Pattern
 open Nametab
+open Mod_subst
 
 (* In this file, we translate rawconstr to ast, in order to print constr *)
 
@@ -390,6 +391,55 @@ let ast_of_constr at_top env t =
   ast_of_raw 
     (Detyping.detype (at_top,env) avoid (names_of_rel_context env) t')
 
+(**********************************************************************)
+(* Object substitution in modules *)
+
+let rec subst_ast subst ast = match ast with
+  | Node (l,s,astl) ->
+      let astl' = Util.list_smartmap (subst_ast subst) astl in
+	if astl' == astl then ast else
+	  Node (l,s,astl')
+  | Slam (l,ido,ast1) ->
+      let ast1' = subst_ast subst ast1 in
+	if ast1' == ast1 then ast else
+	  Slam (l,ido,ast1')
+  | Smetalam (l,s,ast1) ->
+      let ast1' = subst_ast subst ast1 in
+	if ast1' == ast1 then ast else
+	  Smetalam (l,s,ast1')
+  | Path (loc,kn) -> 
+      let kn' = subst_kn subst kn in
+	if kn' == kn then ast else
+	  Path(loc,kn')
+  | ConPath (loc,kn) -> 
+      let kn',t = subst_con subst kn in
+	if kn' == kn then ast else
+	  ast_of_constr false (Global.env ()) t
+  | Nmeta _
+  | Nvar _ -> ast
+  | Num _
+  | Str _
+  | Id _
+  | Dynamic _ -> ast
+
+let rec subst_astpat subst = function
+(*CSC: this is wrong since I am not recompiling the whole pattern.
+  However, this is V7-syntax code that is doomed to disappear. Hence I
+  prefer to be lazy and to not fix the bug. *)
+  | Pquote a -> Pquote (subst_ast subst a)
+  | Pmeta _ as p -> p
+  | Pnode (s,pl) -> Pnode (s,subst_astpatlist subst pl)
+  | Pslam (ido,p) -> Pslam (ido,subst_astpat subst p)
+  | Pmeta_slam (s,p) -> Pmeta_slam (s,subst_astpat subst p)
+
+and subst_astpatlist subst = function
+  | Pcons (p,pl) -> Pcons (subst_astpat subst p, subst_astpatlist subst pl)
+  | (Plmeta _ | Pnil) as pl -> pl
+
+let subst_pat subst = function
+  | AstListPat pl -> AstListPat (subst_astpatlist subst pl)
+  | PureAstPat p -> PureAstPat (subst_astpat subst p)
+
 let ast_of_constant env sp =
   let a = ast_of_constant_ref sp in
   a
diff --git a/parsing/termast.mli b/parsing/termast.mli
index f4c9466d3..da7e476be 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -18,6 +18,7 @@ open Libnames
 open Nametab
 open Rawterm
 open Pattern
+open Mod_subst
 (*i*)
 
 (* Translation of pattern, cases pattern, rawterm and term into syntax
@@ -32,6 +33,10 @@ val ast_of_pattern : env -> names_context -> constr_pattern -> Coqast.t
 
 val ast_of_constr : bool -> env -> constr -> Coqast.t
 
+(* Object substitution in modules *)
+val subst_ast: substitution -> Coqast.t -> Coqast.t
+val subst_astpat : substitution -> Ast.astpat -> Ast.astpat
+
 val ast_of_constant     : env -> constant -> Coqast.t
 val ast_of_existential  : env -> existential -> Coqast.t
 val ast_of_constructor  : env -> constructor -> Coqast.t