Déplacement du type reference dans Term

Découpage de tactics/pattern en proofs/pattern et tactics/hipattern
Renommage des fonctions somatch and co dans Pattern et Tacticals
Divers extensions pour utiliser les constr_pattern


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

1 files changed, 51 insertions, 49 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 36f8d11a36..3e286462e8 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -26,7 +26,7 @@ let pr_global k oper =
   [< 'sTR (string_of_id id) >]
 *)
 
-let globpr k gt = match gt with
+let globpr gt = match gt with
   | Nvar(_,s) -> [< 'sTR s >]
 (*
   | Node(_,"EVAR", (Num (_,ev))::_) ->
@@ -63,62 +63,64 @@ let tactic_syntax_universe = "tactic"
 let constr_initial_prec = Some ((constr_syntax_universe,(9,0,0)),Extend.L)
 let tactic_initial_prec = Some ((tactic_syntax_universe,(9,0,0)),Extend.L)
 
-let gencompr k gt =
-  let uni = match k with
-    | CCI | FW -> constr_syntax_universe
-    | _ -> anomaly "gencompr: not a construction"
-	(* WAS "<undefined>" *)
-  in Esyntax.genprint (globpr k) uni constr_initial_prec gt
+let gentermpr_fail gt =
+  Esyntax.genprint globpr constr_syntax_universe constr_initial_prec gt
 
-(* [at_top] means ids of env must be avoided in bound variables *)
-let gentermpr_core at_top k env t =
-  let uenv = unitize_env env in
-  try gencompr k (Termast.bdize at_top uenv t)
+let gentermpr gt =
+  try gentermpr_fail gt
   with s -> wrap_exception s
 
-let gentermpr k = gentermpr_core false k
-let gentermpr_at_top k = gentermpr_core true k
+(* [at_top] means ids of env must be avoided in bound variables *)
+let gentermpr_core at_top env t =
+  gentermpr (Termast.ast_of_constr at_top (unitize_env env) t)
 
-let prterm_env_at_top a = gentermpr_core true CCI a
-let prterm_env a = gentermpr CCI a
+let prterm_env_at_top env = gentermpr_core true env
+let prterm_env env = gentermpr_core false env
 let prterm = prterm_env (gLOB nil_sign)
 
-let fprterm_env a = gentermpr FW a
-let fprterm = fprterm_env (gLOB nil_sign)
-
 let prtype_env env typ = prterm_env env (incast_type typ)
 let prtype = prtype_env (gLOB nil_sign)
 
+(* Plus de "k"...
+let gentermpr k = gentermpr_core false
+let gentermpr_at_top k = gentermpr_core true
+
+let fprterm_env a = gentermpr FW a
+let fprterm = fprterm_env (gLOB nil_sign)
+
 let fprtype_env env typ = fprterm_env env (incast_type typ)
 let fprtype = fprtype_env (gLOB nil_sign)
+*)
+
+let fprterm_env a = failwith "Fw printing not implemented"
+let fprterm = failwith "Fw printing not implemented"
 
-let pr_constant cst = gencompr CCI (ast_of_constant cst)
-let pr_existential ev = gencompr CCI (ast_of_existential ev)
-let pr_inductive ind = gencompr CCI (ast_of_inductive ind)
-let pr_constructor cstr = gencompr CCI (ast_of_constructor cstr)
+let fprtype_env env typ = failwith "Fw printing not implemented"
+let fprtype = failwith "Fw printing not implemented"
 
-open Rawterm
+(* For compatibility *)
+let fterm0 = fprterm_env
+
+let pr_constant cst = gentermpr (ast_of_constant cst)
+let pr_existential ev = gentermpr (ast_of_existential ev)
+let pr_inductive ind = gentermpr (ast_of_inductive ind)
+let pr_constructor cstr = gentermpr (ast_of_constructor cstr)
+
+open Pattern
 let pr_ref_label = function (* On triche sur le contexte *)
   | ConstNode sp -> pr_constant (sp,[||])
   | IndNode sp -> pr_inductive (sp,[||])
   | CstrNode sp -> pr_constructor (sp,[||])
   | VarNode id -> print_id id
 
+let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t)
+let pr_rawterm t = gentermpr (Termast.ast_of_rawconstr t)
+let pr_pattern_env env t =
+  gentermpr (Termast.ast_of_pattern (unitize_env env) t)
+let pr_pattern t = pr_pattern_env (gLOB nil_sign) t
+
 (* For compatibility *)
 let term0 = prterm_env
-let fterm0 = fprterm_env
-
-let genpatternpr k t =
-  try gencompr k (Termast.ast_of_pattern t)
-  with s -> wrap_exception s
-
-let prpattern = genpatternpr CCI
-
-let genrawtermpr k env t =
-  try gencompr k (Termast.ast_of_rawconstr t)
-  with s -> wrap_exception s
-
-let prrawterm = genrawtermpr CCI (gLOB nil_sign)
 
 let rec gentacpr gt =
   Esyntax.genprint default_tacpr tactic_syntax_universe tactic_initial_prec gt
@@ -130,12 +132,12 @@ and default_tacpr = function
 	[< 'sTR s; 'bRK(1,2); hOV 0 (prlist_with_sep pr_spc gentacpr ta) >]
     | gt -> dfltpr gt
 
-let print_decl k sign (s,typ) =
-  let ptyp = gentermpr k (gLOB sign) (body_of_type typ) in
+let print_decl sign (s,typ) =
+  let ptyp = prterm_env (gLOB sign) (body_of_type typ) in
   [< print_id s ; 'sTR" : "; ptyp >]
 
-let print_binding k env (na,typ) =
-  let ptyp = gentermpr k env (body_of_type typ) in
+let print_binding env (na,typ) =
+  let ptyp = prterm_env env (body_of_type typ) in
   match na with
     | Anonymous -> [< 'sTR"<>" ; 'sTR" : " ; ptyp >]
     | Name id -> [< print_id id ; 'sTR" : "; ptyp >]
@@ -164,34 +166,34 @@ let dbenv_it_with f env e =
 (* Prints a signature, all declarations on the same line if possible *)
 let pr_sign sign =
   hV 0 [< (sign_it_with (fun id t sign pps ->
-                           [< pps; 'wS 2; print_decl CCI sign (id,t) >])
+                           [< pps; 'wS 2; print_decl sign (id,t) >])
              sign) [< >] >]
 
 (* Prints an env (variables and de Bruijn). Separator: newline *)
-let pr_env k env =
+let pr_env env =
   let sign_env =
     sign_it_with
       (fun id t sign pps ->
-         let pidt =  print_decl k sign (id,t) in [< pps; 'fNL; pidt >])
+         let pidt =  print_decl sign (id,t) in [< pps; 'fNL; pidt >])
       (get_globals env) [< >] 
   in
   let db_env =
     dbenv_it_with 
       (fun na t env pps ->
-         let pnat = print_binding k env (na,t) in [< pps; 'fNL; pnat >])
+         let pnat = print_binding env (na,t) in [< pps; 'fNL; pnat >])
       env [< >]
   in 
   [< sign_env; db_env >]
 
 let pr_ne_env header k = function
   | ENVIRON (sign,_) as env when isnull_sign sign & isnull_rel_env env -> [< >]
-  | env -> let penv = pr_env k env in [< header; penv >]
+  | env -> let penv = pr_env env in [< header; penv >]
 
 let pr_env_limit n env =
   let sign = get_globals env in
   let lgsign = sign_length sign in
   if n >= lgsign then 
-    pr_env CCI env
+    pr_env env
   else
     let k = lgsign-n in
     let sign_env =
@@ -200,7 +202,7 @@ let pr_env_limit n env =
            if i < k then 
 	     [< pps ;'sTR "." >] 
 	   else
-             let pidt = print_decl CCI sign (id,t) in
+             let pidt = print_decl sign (id,t) in
 	     [< pps ; 'fNL ;
 		'sTR (emacs_str (String.make 1 (Char.chr 253)));
 		pidt >])
@@ -209,7 +211,7 @@ let pr_env_limit n env =
     let db_env =
       dbenv_it_with
         (fun na t env pps ->
-           let pnat = print_binding CCI env (na,t) in
+           let pnat = print_binding env (na,t) in
 	   [< pps; 'fNL;
 	      'sTR (emacs_str (String.make 1 (Char.chr 253)));
 	      pnat >])
@@ -218,5 +220,5 @@ let pr_env_limit n env =
     [< sign_env; db_env >]
 
 let pr_env_opt env = match Options.print_hyps_limit () with 
-  | None -> hV 0 (pr_env CCI env)
+  | None -> hV 0 (pr_env env)
   | Some n -> hV 0 (pr_env_limit n env)