Traitement du pretty-print des Redexp

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

4 files changed, 39 insertions, 26 deletions

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 0c170ef3d..e17ca92f3 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+open Closure
 open Util
 open Names
 open Term
@@ -10,6 +11,7 @@ open Stamps
 open Environ
 open Evarutil
 open Proof_type
+open Tacred
 open Typing
 
 let is_bind = function
@@ -342,6 +344,37 @@ let rec ast_of_cvt_intro_pattern = function
   | ConjPat l -> ope ("CONJPATTERN",  (List.map ast_of_cvt_intro_pattern l))
   | ListPat l -> ope ("LISTPATTERN",  (List.map ast_of_cvt_intro_pattern l))
 
+(* Gives the ast list corresponding to a reduction flag *)
+let last_of_cvt_flags (_,red) =
+  (if (red_set red BETA) then [ope("Beta",[])]
+   else [])@
+  (let (n_unf,lconst) = red_get_const red in
+   let lnvar = List.map (fun sp -> nvar (print_basename sp)) lconst in
+   if lnvar = [] then []
+   else if n_unf then [ope("Delta",[]);ope("UnfBut",lnvar)]
+   else [ope("Delta",[]);ope("Unf",lnvar)])@
+  (if (red_set red IOTA) then [ope("Iota",[])]
+   else [])
+
+(* Gives the ast corresponding to a reduction expression *)
+let ast_of_cvt_redexp = function
+  | Red _ -> ope ("Red",[])
+  | Hnf -> ope("Hnf",[])
+  | Simpl -> ope("Simpl",[])
+  | Cbv flg -> ope("Cbv",last_of_cvt_flags flg)
+  | Lazy flg -> ope("Lazy",last_of_cvt_flags flg)
+  | Unfold l ->
+    ope("Unfold",List.map (fun (locc,sp) -> ope("UNFOLD",
+      [nvar (print_basename sp)]@(List.map num locc))) l)
+  | Fold l ->
+    ope("Fold",List.map (fun c -> ope ("COMMAND",
+      [ast_of_constr false (Global.env ()) c])) l)
+  | Pattern l ->
+    ope("Pattern",List.map (fun (locc,csr,_) -> ope("PATTERN",
+      [ope ("COMMAND",[ast_of_constr false (Global.env ()) csr])]@
+      (List.map num locc))) l)
+
+(* Gives the ast corresponding to a tactic argument *)
 let ast_of_cvt_arg = function
   | Identifier id   -> nvar (string_of_id id) 
   | Quoted_string s -> str s
@@ -364,11 +397,7 @@ let ast_of_cvt_arg = function
 		(ast_of_constr false (Global.env ()))) bl)
   | Tacexp ast      -> ope ("TACTIC",[ast])
   | Tac tac -> failwith "TODO: ast_of_cvt_arg: Tac"
-  | Redexp red ->
-    begin
-      wARNING [<'sTR "TODO: ast_of_cvt_arg: Redexp">];
-      nvar "REDEXP"
-    end
+  | Redexp red -> ope("REDEXP",[ast_of_cvt_redexp red])
   | Fixexp (id,n,c) -> ope ("FIXEXP",[(nvar (string_of_id id)); 
                                       (num n); 
                                       ope ("COMMAND",[c])]) 
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 9730652f5..c2b73c85d 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -86,4 +86,5 @@ val pr_evars     : (int * goal) list -> std_ppcmds
 val pr_evars_int : int -> (int * goal) list -> std_ppcmds
 val pr_subgoals_existential : enamed_declarations -> goal list -> std_ppcmds
 
+(* Gives the ast corresponding to a tactic argument *)
 val ast_of_cvt_arg : tactic_arg ->  Coqast.t 
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 6940f2a07..39630ec38 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -925,27 +925,12 @@ let interp_tacarg sign ast = unvarg (val_interp sign ast)
 (* Initial call for interpretation *)
 let interp = fun ast -> tac_interp [] [] !debug ast
 
-let is_just_undef_macro ast =
-  match ast with
-    | Node(_,"TACTICLIST",[Node(loc,"CALL",macro::_)]) ->
-        let id = nvar_of_ast macro in
-      	(try let _ = Macros.lookup id in None with Not_found -> Some id)
-    | _ -> None
-
-let vernac_interp_atomic =
-  let gentac =
-    hide_tactic "InterpretAtomic"
-      (fun argl gl -> match argl with 
-	 | (Identifier id)::args -> 
-	     interp_atomic dummy_loc (string_of_id id) args gl
-	 | _ -> assert false)
-  in 
-  fun opn args -> gentac ((Identifier opn)::args)
-
+(* For bad tactic calls *)
 let bad_tactic_args s =
   anomalylabstrm s
     [<'sTR "Tactic "; 'sTR s; 'sTR " called with bad arguments">]
 
+(* Declaration of the TACTIC-DEFINITION object *)
 let (inMD,outMD) =
   let add (na,td) = mactab := Gmap.add na td !mactab in
   let cache_md (_,(na,td)) =  
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index d0ec28ea0..800d89051 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -57,10 +57,8 @@ val val_interp : interp_sign -> Coqast.t -> value
 (* Interprets tactic arguments *)
 val interp_tacarg : interp_sign -> Coqast.t -> tactic_arg
 
+(* Initial call for interpretation *)
 val interp               : Coqast.t -> tactic
-(*i val vernac_interp        : Coqast.t -> tactic i*)
-val vernac_interp_atomic : identifier -> tactic_arg list -> tactic
-
-val is_just_undef_macro  : Coqast.t -> string option
 
+(* For bad tactic calls *)
 val bad_tactic_args : string -> 'a