Réforme de l'interprétation des termes :

- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
  pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
  se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
  constrextern.ml est l'équivalent de termast.ml pour le nouveau
  printer; topconstr.ml; contient la définition de "constr_expr";
  modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 80 insertions, 61 deletions

diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli
index 3c5a56c1df..b761da60ea 100644
--- a/contrib/correctness/past.mli
+++ b/contrib/correctness/past.mli
@@ -14,10 +14,11 @@
 
 open Names
 open Ptype
+open Topconstr
 
 type termination = 
   | RecArg of int 
-  | Wf of Coqast.t * Coqast.t
+  | Wf of constr_expr * constr_expr
 
 type variable = identifier
 
@@ -43,7 +44,7 @@ type ('a, 'b) t = {
   desc : ('a, 'b) t_desc;
   pre  : 'b Ptype.precondition list;
   post : 'b Ptype.postcondition option;
-  loc  : Coqast.loc;
+  loc  : Util.loc;
   info : 'a 
 }
 
@@ -73,7 +74,7 @@ and ('a, 'b) arg =
   | Refarg of variable
   | Type of 'b Ptype.ml_type_v
 
-type program = (unit, Coqast.t) t
+type program = (unit, Topconstr.constr_expr) t
 
 (*s Intermediate type for CC terms. *)
 
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index 30959acdad..488819bc24 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -10,7 +10,9 @@
 
 (* $Id$ *)
 
+open Util
 open Names
+open Nameops
 open Libnames
 open Term
 open Termops
@@ -21,6 +23,7 @@ open Sign
 open Rawterm
 open Typeops
 open Entries
+open Topconstr
 
 open Pmisc
 open Past
@@ -39,26 +42,21 @@ let tuple_exists id =
   try let _ = Nametab.locate (make_short_qualid id) in true
   with Not_found -> false
 
-let ast_set = Ast.ope ("SET", [])
+let ast_set = CSort (dummy_loc,RProp Pos)
 
 let tuple_n n =
-  let name = "tuple_" ^ string_of_int n in
-  let id = id_of_string name in
+  let id = make_ident "tuple_" (Some n) in
   let l1n = Util.interval 1 n in
-  let params = 
-    List.map 
-      (fun i -> let id = id_of_string ("T" ^ string_of_int i) in (id, ast_set))
-      l1n
-  in
+  let params = List.map (fun i -> (make_ident "T" (Some i), ast_set)) l1n in
   let fields = 
     List.map
       (fun i -> 
-	 let id = id_of_string 
-		    ("proj_" ^ string_of_int n ^ "_" ^ string_of_int i) in
-	 (false, Vernacexpr.AssumExpr (id, Ast.nvar (id_of_string ("T" ^ string_of_int i)))))
+	 let id = make_ident ("proj_" ^ string_of_int n ^ "_") (Some i) in
+	 let id' = make_ident "T" (Some i) in
+	 (false, Vernacexpr.AssumExpr (id, mkIdentC id')))
       l1n 
   in
-  let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in
+  let cons = make_ident "Build_tuple_" (Some n) in
   Record.definition_structure ((false, id), params, fields, cons, mk_Set)
 
 (*s [(sig_n n)] generates the inductive
@@ -68,12 +66,11 @@ let tuple_n n =
     \end{verbatim} *)
 
 let sig_n n =
-  let name = "sig_" ^ string_of_int n in
-  let id = id_of_string name in
+  let id = make_ident "sig_" (Some n) in
   let l1n = Util.interval 1 n in
-  let lT = List.map (fun i -> id_of_string ("T" ^ string_of_int i)) l1n in
-  let lx = List.map (fun i -> id_of_string ("x" ^ string_of_int i)) l1n in
-  let idp = id_of_string "P" in
+  let lT = List.map (fun i -> make_ident "T" (Some i)) l1n in
+  let lx = List.map (fun i -> make_ident "x" (Some i)) l1n in
+  let idp = make_ident "P" None in
   let params =
     let typ = List.fold_right (fun _ c -> mkArrow (mkRel n) c) lT mkProp in
     (idp, LocalAssum typ) :: 
@@ -87,7 +84,7 @@ let sig_n n =
     let c = mkArrow app_p app_sig in
     List.fold_right (fun id c -> mkProd (Name id, mkRel (n+1), c)) lx c
   in
-  let cname = id_of_string ("exist_" ^ string_of_int n) in
+  let cname = make_ident "exist_" (Some n) in
   Declare.declare_mind 
     { mind_entry_finite = true;
       mind_entry_inds = 
@@ -123,14 +120,12 @@ let tuple_ref dep n =
       if n = 1 then 
 	exist
       else begin
-	let name = Printf.sprintf "exist_%d" n in
-	let id = id_of_string name in
+	let id = make_ident "exist_" (Some n) in
 	if not (tuple_exists id) then ignore (sig_n n);
 	Nametab.locate (make_short_qualid id)
       end
     else begin
-      let name = Printf.sprintf "Build_tuple_%d" n in
-      let id = id_of_string name in
+      let id = make_ident "Build_tuple_%d" (Some n) in
       if not (tuple_exists id) then tuple_n n;
       Nametab.locate (make_short_qualid id)
     end
@@ -185,7 +180,7 @@ let rawconstr_of_prog p =
 	let (bl',avoid',nenv') = push_vars avoid nenv bl in
 	let c1 = trad avoid nenv e1
 	and c2 = trad avoid' nenv' e2 in
-	ROldCase (dummy_loc, false, None, c1, [| raw_lambda bl' c2 |])
+	ROrderedCase (dummy_loc, LetStyle, None, c1, [| raw_lambda bl' c2 |])
 
     | CC_lam (bl,e) ->
 	let bl',avoid',nenv' = push_vars avoid nenv bl in
@@ -219,7 +214,7 @@ let rawconstr_of_prog p =
 	let c = trad avoid nenv b in
 	let cl = List.map (trad avoid nenv) el in
 	let ty = Detyping.detype (Global.env()) avoid nenv ty in
-	ROldCase (dummy_loc, false, Some ty, c, Array.of_list cl)
+	ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl)
 
     | CC_expr c -> 
 	Detyping.detype (Global.env()) avoid nenv c
diff --git a/contrib/correctness/perror.mli b/contrib/correctness/perror.mli
index 81bed4404c..3664ebf787 100644
--- a/contrib/correctness/perror.mli
+++ b/contrib/correctness/perror.mli
@@ -11,10 +11,10 @@
 (* $Id$ *)
 
 open Pp
+open Util
 open Names
 open Ptype
 open Past
-open Coqast
 
 val unbound_variable : identifier -> loc option -> 'a
 val unbound_reference : identifier -> loc option -> 'a
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index bb660ddb4c..60f7306ac5 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -12,10 +12,11 @@
 
 open Pp
 open Util
-open Coqast
 open Names
 open Nameops
 open Term
+open Libnames
+open Topconstr
 
 (* debug *)
 
@@ -122,6 +123,7 @@ let subst_in_constr alist =
   let alist' = List.map (fun (id,id') -> (id, mkVar id')) alist in
   replace_vars alist'
 
+(*
 let subst_in_ast alist ast =
   let rec subst = function
       Nvar(l,s) -> Nvar(l,try List.assoc s alist with Not_found -> s)
@@ -130,7 +132,8 @@ let subst_in_ast alist ast =
     | x -> x
   in
     subst ast
-
+*)
+(*
 let subst_ast_in_ast alist ast =
   let rec subst = function
       Nvar(l,s) as x -> (try List.assoc s alist with Not_found -> x)
@@ -139,6 +142,17 @@ let subst_ast_in_ast alist ast =
     | x -> x
   in
     subst ast
+*)
+
+let rec subst_in_ast alist = function
+  | CRef (Ident (loc,id)) ->
+      CRef (Ident (loc,(try List.assoc id alist with Not_found -> id)))
+  | x -> map_constr_expr_with_binders subst_in_ast List.remove_assoc alist x
+
+let rec subst_ast_in_ast alist = function
+  | CRef (Ident (_,id)) as x -> (try List.assoc id alist with Not_found -> x)
+  | x ->
+      map_constr_expr_with_binders subst_ast_in_ast List.remove_assoc alist x
 
 (* subst. of variables by constr *)
 let real_subst_in_constr = replace_vars
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli
index 207e74b2be..a07eed5659 100644
--- a/contrib/correctness/pmisc.mli
+++ b/contrib/correctness/pmisc.mli
@@ -13,10 +13,11 @@
 open Names
 open Term
 open Ptype
+open Topconstr
 
 (* Some misc. functions *)
 
-val reraise_with_loc : Coqast.loc -> ('a -> 'b) -> 'a -> 'b
+val reraise_with_loc : Util.loc -> ('a -> 'b) -> 'a -> 'b
 
 val list_of_some : 'a option -> 'a list
 val difference : 'a list -> 'a list -> 'a list
@@ -49,8 +50,9 @@ val id_of_name : name -> identifier
 val isevar : constr
 
 val subst_in_constr : (identifier * identifier) list -> constr -> constr
-val subst_in_ast : (identifier * identifier) list -> Coqast.t -> Coqast.t
-val subst_ast_in_ast : (identifier * Coqast.t) list -> Coqast.t -> Coqast.t
+val subst_in_ast : (identifier * identifier) list -> constr_expr -> constr_expr
+val subst_ast_in_ast :
+  (identifier * constr_expr) list -> constr_expr -> constr_expr
 val real_subst_in_constr : (identifier * constr) list -> constr -> constr
 
 val constant : string -> constr
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 591076bddb..8e4c9b2bd3 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -13,11 +13,14 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Options
+open Util
 open Names
 open Nameops
 open Vernacentries
 open Reduction
 open Term
+open Libnames
+open Topconstr
 
 open Prename
 open Pmisc
@@ -92,17 +95,23 @@ module Programs =
 open Programs
 
 let ast_of_int n =
-  G_zsyntax.z_of_string true n Ast.dummy_loc
+  G_zsyntax.z_of_string true n dummy_loc
 
 let constr_of_int n =
-  Astterm.interp_constr Evd.empty (Global.env ()) (ast_of_int n)
+  Constrintern.interp_constr Evd.empty (Global.env ()) (ast_of_int n)
+
+open Util
+open Coqast
 
-let ast_constant loc s = <:ast< (QUALID ($VAR $s)) >>
+let mk_id loc id = mkRefC (Ident (loc, id))
+let mk_ref loc s = mk_id loc (id_of_string s)
+let mk_appl loc1 loc2 f args =
+  CApp (join_loc loc1 loc2, mk_ref loc1 f, List.map (fun a -> a,None) args)
 
 let conj_assert {a_name=n;a_value=a} {a_value=b} = 
-  let loc = Ast.loc a in
-  let et = ast_constant loc "and" in
-  { a_value = <:ast< (APPLIST $et $a $b) >>; a_name = n }
+  let loc1 = constr_loc a in
+  let loc2 = constr_loc a in
+  { a_value = mk_appl loc1 loc2 "and" [a;b]; a_name = n }
 
 let conj = function
     None,None     -> None
@@ -137,28 +146,26 @@ let bool_not loc a =
   let d = SApp ( [Variable connective_not ], [a]) in
   w d
 
-let ast_zwf_zero loc =
-  let zwf = ast_constant loc "Zwf" and zero = ast_constant loc "ZERO" in
-    <:ast< (APPLIST $zwf $zero) >>
+let ast_zwf_zero loc = mk_appl loc loc "Zwf" [mk_ref loc "ZERO"]
 
 (* program -> Coq AST *)
 
-let bdize c = 
+let bdize c =
   let env = 
     Global.env_of_context (Pcicenv.cci_sign_of Prename.empty_ren Penv.empty)
   in
-  Termast.ast_of_constr true env c
+  Constrextern.extern_constr true env c
 
 let rec coqast_of_program loc = function
-  | Variable id -> let s = string_of_id id in <:ast< ($VAR $s) >>
-  | Acc id -> let s = string_of_id id in <:ast< ($VAR $s) >>
+  | Variable id -> mk_id loc id
+  | Acc id -> mk_id loc id
   | Apply (f,l) -> 
       let f = coqast_of_program f.loc f.desc in
       let args = List.map 
-		   (function Term t -> coqast_of_program t.loc t.desc
+		   (function Term t -> (coqast_of_program t.loc t.desc,None)
 		      | _ -> invalid_arg "coqast_of_program") l
       in
-      <:ast< (APPLIST $f ($LIST $args)) >>
+      CApp (dummy_loc, f, args)
   | Expression c -> bdize c
   | _ -> invalid_arg "coqast_of_program"
 
@@ -174,9 +181,8 @@ let rec coqast_of_program loc = function
  *)
 
 let ast_plus_un loc ast =
-  let zplus = ast_constant loc "Zplus" in
   let un = ast_of_int "1" in
-  <:ast< (APPLIST $zplus $ast $un) >>
+  mk_appl loc loc "Zplus" [ast;un]
 
 let make_ast_for loc i v1 v2 inv block =
   let f = for_name() in
@@ -197,22 +203,20 @@ let make_ast_for loc i v1 v2 inv block =
       without_effect loc (Seq (block @ [Statement f_succ_i]))
     in
     let inv' = 
-      let zle = ast_constant loc "Zle" in
-      let i_le_sv2 = <:ast< (APPLIST $zle ($VAR $i) $succ_v2) >> in
+      let i_le_sv2 = mk_appl loc loc "Zle" [mk_ref loc i; succ_v2] in
       conj_assert {a_value=i_le_sv2;a_name=inv.a_name} inv
     in
     { desc = If(test,br_t,br_f); loc = loc; 
       pre = [pre_of_assert false inv']; post = Some post; info = () } 
   in
   let bl = 
-    let typez = ast_constant loc "Z" in
+    let typez = mk_ref loc "Z" in
     [(id_of_string i, BindType (TypePure typez))] 
   in
   let fv1 = without_effect loc (Apply (var_f, [Term v1])) in
-  let v = TypePure (ast_constant loc "unit") in
+  let v = TypePure (mk_ref loc "unit") in
   let var = 
-    let zminus = ast_constant loc "Zminus" in
-    let a = <:ast< (APPLIST $zminus $succ_v2 ($VAR $i)) >> in
+    let a = mk_appl loc loc "Zminus" [succ_v2;mk_ref loc i] in
     (a, ast_zwf_zero loc)
   in
   Let (f, without_effect loc (LetRec (f,bl,v,var,e1)), fv1)
diff --git a/contrib/correctness/psyntax.mli b/contrib/correctness/psyntax.mli
index f5128fdef9..dac571de55 100644
--- a/contrib/correctness/psyntax.mli
+++ b/contrib/correctness/psyntax.mli
@@ -13,13 +13,14 @@
 open Pcoq
 open Ptype
 open Past
+open Topconstr
 
 (* Grammar for the programs and the tactic Correctness *)
 
 module Programs :
   sig
     val program : program Gram.Entry.e
-    val type_v  : Coqast.t ml_type_v Gram.Entry.e
-    val type_c  : Coqast.t ml_type_c Gram.Entry.e
+    val type_v  : constr_expr ml_type_v Gram.Entry.e
+    val type_c  : constr_expr ml_type_c Gram.Entry.e
   end
 
diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml
index a6f7a0ae95..6c870c85a8 100644
--- a/contrib/correctness/ptyping.ml
+++ b/contrib/correctness/ptyping.ml
@@ -16,9 +16,10 @@ open Names
 open Term
 open Termops
 open Environ
-open Astterm
+open Constrintern
 open Himsg
 open Proof_trees
+open Topconstr
 
 open Pmisc
 open Putil
@@ -110,7 +111,7 @@ let effect_app ren env f args =
 let state_coq_ast sign a =
   let env = Global.env_of_context sign in
   let j =
-    reraise_with_loc (Ast.loc a) (judgment_of_rawconstr Evd.empty env) a in
+    reraise_with_loc (constr_loc a) (judgment_of_rawconstr Evd.empty env) a in
   let ids = global_vars env j.uj_val in
   j.uj_val, j.uj_type, ids
 
diff --git a/contrib/correctness/ptyping.mli b/contrib/correctness/ptyping.mli
index bfb7a9a869..968f4fd31e 100644
--- a/contrib/correctness/ptyping.mli
+++ b/contrib/correctness/ptyping.mli
@@ -12,6 +12,7 @@
 
 open Names
 open Term
+open Topconstr
 
 open Ptype
 open Past
@@ -19,7 +20,7 @@ open Penv
 
 (* This module realizes type and effect inference *)
 
-val cic_type_v : local_env -> Prename.t -> Coqast.t ml_type_v -> type_v
+val cic_type_v : local_env -> Prename.t -> constr_expr ml_type_v -> type_v
 
 val effect_app : Prename.t -> local_env
             -> (typing_info,'b) Past.t