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

4 files changed, 157 insertions, 74 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index dd2f1b5d8b..a096c833a0 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -12,6 +12,7 @@ open Evd
 open Reduction
 open Impargs
 open Rawterm
+open Pattern
 open Typing
 open Pretyping
 open Evarutil
@@ -569,7 +570,7 @@ let rec pat_of_ref metas vars = function
   | RInd (ip,ctxt) -> RInd (ip, ctxt)
   | RConstruct(cp,ctxt) ->RConstruct(cp, ctxt)
   | REVar (n,ctxt) -> REVar (n, ctxt)
-  | RMeta n -> RMeta n
+  | RMeta n -> metas := n::!metas; RMeta n
   | RAbst _ -> error "pattern_of_rawconstr: not implemented"
   | RVar _ -> assert false (* Capturé dans pattern_of_raw *)
 
@@ -587,11 +588,8 @@ and pat_of_raw metas vars = function
 	       pat_of_raw metas (na::vars) c2)
   | RSort (_,s) ->
       PSort s
-  | RHole _ -> error "Place-holders must be numbered in patterns"
-(*
-      let n = new_meta () in
-      metas := n::!metas;
-      PMeta n *)
+  | RHole _ ->
+      PMeta None
   | RCast (_,c,t) ->
       warning "Cast not taken into account in constr pattern";
       pat_of_raw metas vars c
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 10e43172b7..19773d6869 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -47,15 +47,22 @@ let print_typed_value_in_env env (trm,typ) =
      'sTR "     : "; prterm_env (gLOB sign) typ ; 'fNL >]
 
 let print_typed_value x = print_typed_value_in_env (Global.env ()) x
+
+let pkprinters = function
+  | FW -> (fprterm,fprterm_env)
+  | CCI -> (prterm,prterm_env)
+  | _ -> anomaly "pkprinters"
 			  		  
 let print_recipe = function
   | Some { contents = Cooked c } -> prterm c
   | Some { contents = Recipe _ } -> [< 'sTR"<recipe>" >]
   | None -> [< 'sTR"<uncookable>" >]
 
+(*
 let fprint_recipe = function
   | Some c -> fprterm c
   | None -> [< 'sTR"<uncookable>" >]
+*)
 
 let print_typed_recipe (val_0,typ) =
   [< print_recipe val_0; 'fNL; 'sTR "     : "; prtype typ; 'fNL >]
@@ -77,7 +84,7 @@ let print_var name typ =
   [< 'sTR "*** [" ; 'sTR name ; 'sTR " : "; prtype typ; 'sTR "]"; 'fNL >]
 
 let print_env pk = 
-  let pterminenv = if pk = FW then fprterm_env else prterm_env in
+  let pterminenv = (* if pk = FW then fprterm_env else *) prterm_env in
   let pr_binder env (na,c) =
     match na with
       | Name id as name ->
@@ -99,8 +106,7 @@ let assumptions_for_print lna =
     (ENVIRON(nil_sign,nil_dbsign))
 
 let print_constructors_with_sep pk fsep mip = 
-  let pterm,pterminenv =
-    if pk = FW then (fprterm,fprterm_env) else (prterm,prterm_env) in
+  let pterm,pterminenv = pkprinters pk in
   let (lna,lC) = decomp_all_DLAMV_name mip.mind_lc in
   let ass_name = assumptions_for_print lna in
   let lidC = Array.to_list 
@@ -131,8 +137,7 @@ let implicit_args_msg sp mipv =
 
 let print_mutual sp mib = 
   let pk = kind_of_path sp in
-  let pterm,pterminenv =
-    if pk = FW then (fprterm,fprterm_env) else (prterm,prterm_env) in
+  let pterm,pterminenv = pkprinters pk in
   let env = Global.env () in
   let evd = Evd.empty in
   let {mind_packets=mipv; mind_nparams=nparams} = mib in 
@@ -271,7 +276,7 @@ let print_leaf_entry with_values sep (sp,lobj) =
       	   print_id id ; 'sTR sep;  
            if with_values then 
              let c = Syntax_def.search_syntactic_definition id in 
-	     [< prrawterm c >]
+	     [< pr_rawterm c >]
            else [<>]; 'fNL >]
     | (_,"PPSYNTAX") -> 
 	[< 'sTR" Syntax Marker"; 'fNL >]
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)
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 3587ba01e5..dda005f8bb 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -14,6 +14,7 @@ open Impargs
 open Coqast
 open Ast
 open Rawterm
+open Pattern
 
 (* In this file, we translate rawconstr to ast, in order to print constr *)
 
@@ -130,24 +131,24 @@ let ast_of_ref = function
 	    ::(List.map ast_of_ident (* on triche *) []))
   | RInd (ind,ctxt) -> ast_of_inductive_ref (ind,ids_of_ctxt ctxt)
   | RConstruct (cstr,ctxt) -> ast_of_constructor_ref (cstr,ids_of_ctxt ctxt)
-  | RVar id -> nvar (string_of_id id)
+  | RVar id -> ast_of_ident id
   | REVar (ev,ctxt) -> ast_of_existential_ref (ev,ids_of_ctxt ctxt)
   | RMeta n -> ope("META",[num n])
 
 (**********************************************************************)
 (* conversion of patterns                                             *)
 
-let rec ast_of_pattern = function   (* loc is thrown away for printing *)
+let rec ast_of_cases_pattern = function   (* loc is thrown away for printing *)
   | PatVar (loc,Name id) -> nvar (string_of_id id)
   | PatVar (loc,Anonymous) -> nvar "_"
   | PatCstr(loc,cstr,args,Name id) ->
+      let args = List.map ast_of_cases_pattern args in
       ope("PATTAS",
 	  [nvar (string_of_id id);
-	   ope("PATTCONSTRUCT",
-	       (ast_of_constructor_ref cstr)::List.map ast_of_pattern args)])
+	   ope("PATTCONSTRUCT", (ast_of_constructor_ref cstr)::args)])
   | PatCstr(loc,cstr,args,Anonymous) ->
       ope("PATTCONSTRUCT",
-	  (ast_of_constructor_ref cstr)::List.map ast_of_pattern args)
+	  (ast_of_constructor_ref cstr)::List.map ast_of_cases_pattern args)
 	
 let ast_dependent na aty =
   match na with
@@ -177,18 +178,18 @@ let implicit_of_ref = function
   | RVar id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *)
   | _ -> []
 
-let rec skip_coercion (f,args as app) =
+let rec skip_coercion dest_ref (f,args as app) =
   if !print_coercions then app
   else
     try
-      match f with
-	| RRef (_,r) ->
+      match dest_ref f with
+	| Some r ->
 	    let n = Classops.coercion_params r in
 	    if n >= List.length args then app
 	    else (* We skip a coercion *)
 	      let _,fargs = list_chop n args in
-	      skip_coercion (List.hd fargs,List.tl fargs)
-	| _ -> app
+	      skip_coercion dest_ref (List.hd fargs,List.tl fargs)
+	| None -> app
     with Not_found -> app
 
 let ast_of_app impl f args =
@@ -216,7 +217,8 @@ let ast_of_app impl f args =
 let rec ast_of_raw = function
   | RRef (_,ref) -> ast_of_ref ref
   | RApp (_,f,args) ->
-      let (f,args) = skip_coercion (f,args) in
+      let (f,args) =
+	skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args) in
       let astf = ast_of_raw f in
       let astargs = List.map ast_of_raw args in
       (match f with 
@@ -296,7 +298,7 @@ let rec ast_of_raw = function
   | RCast (_,c,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t])
 	
 and ast_of_eqn (ids,pl,c) =
-  ope("EQN", (ast_of_raw c)::(List.map ast_of_pattern pl))
+  ope("EQN", (ast_of_raw c)::(List.map ast_of_cases_pattern pl))
 
 and ast_of_rawopt = function
   | None -> (str "SYNTH")
@@ -730,7 +732,7 @@ let old_bdize at_top env t =
 (* FIN TO EJECT *)
 (******************************************************************)
        
-let bdize at_top env t =
+let ast_of_constr at_top env t =
   let t' =
     if !print_casts then t
     else Reduction.strong (fun _ _ -> strip_outer_cast)
@@ -740,3 +742,79 @@ let bdize at_top env t =
     ast_of_raw (Detyping.detype avoid env t')
   with Detyping.StillDLAM ->
     old_bdize at_top env t'
+
+let rec ast_of_pattern env = function
+  | PRef ref -> ast_of_ref ref
+  | PRel n ->
+      (try match fst (lookup_rel n env) with
+	 | Name id   -> ast_of_ident id
+	 | Anonymous ->
+	     anomaly "ast_of_pattern: index to an anonymous variable"
+       with Not_found ->
+	 let s = "[REL "^(string_of_int (number_of_rels env - n))^"]"
+	 in nvar s)
+
+  | PApp (f,args) ->
+      let (f,args) = 
+	skip_coercion (function PRef r -> Some r | _ -> None)
+	  (f,Array.to_list args) in
+      let astf = ast_of_pattern env f in
+      let astargs = List.map (ast_of_pattern env) args in
+      (match f with 
+	 | PRef ref -> ast_of_app (implicit_of_ref ref) astf astargs
+	 | _        -> ast_of_app [] astf astargs)
+
+  | PSoApp (n,args) ->
+      ope("SOAPP",(ope ("META",[num n])):: 
+		  (List.map (ast_of_constr false env) args))
+
+  | PBinder (BProd,Anonymous,t,c) ->
+      ope("PROD",[ast_of_pattern env t; slam(None,ast_of_pattern env c)])
+  | PBinder (bk,na,t,c) ->
+      let env' = add_rel (na,()) env in
+      let (n,a) = factorize_binder_pattern
+		    env' 1 bk na (ast_of_pattern env t) c in
+      let tag = match bk with
+	  (* LAMBDA et LAMBDALIST se comportent pareil *)
+	| BLambda -> if n=1 then "LAMBDA" else "LAMBDALIST"
+	  (* PROD et PRODLIST doivent être distingués à cause du cas *)
+	  (* non dépendant, pour isoler l'implication; peut-être un *)
+	  (* constructeur ARROW serait-il plus justifié ? *) 
+	| BProd -> if n=1 then "PROD" else "PRODLIST" 
+      in
+      ope(tag,[ast_of_pattern env t;a])
+
+  | PLet (id,a,t,c) ->
+      let c' = ast_of_pattern (add_rel (Name id,()) env) c in
+      ope("LET",[ast_of_pattern env a; 	slam(Some (string_of_id id),c')])
+		
+
+  | PCase (typopt,tm,bv) ->
+      warning "Old Case syntax";
+      ope("MUTCASE",(ast_of_patopt env typopt)
+	    ::(ast_of_pattern env tm)
+	    ::(Array.to_list (Array.map (ast_of_pattern env) bv)))
+
+  | PSort s ->
+      (match s with
+	 | RProp Null -> ope("PROP",[])
+	 | RProp Pos -> ope("SET",[])
+	 | RType -> ope("TYPE",[]))
+
+  | PMeta (Some n) -> ope("META",[num n])
+  | PMeta None -> ope("ISEVAR",[])
+	
+and ast_of_patopt env = function
+  | None -> (str "SYNTH")
+  | Some p -> ast_of_pattern env p
+
+and factorize_binder_pattern env n oper na aty c =
+  let (p,body) = match c with
+    | PBinder(oper',na',ty',c')
+	when (oper = oper') & (aty = ast_of_pattern env ty')
+	  & not (na' = Anonymous & oper = BProd)
+	  ->
+	factorize_binder_pattern (add_rel (na',()) env) (n+1) oper na' aty c'
+    | _ -> (n,ast_of_pattern env c)
+  in
+  (p,slam(stringopt_of_name na, body))