Traitement du pretty-print des Redexp

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

5 files changed, 47 insertions, 31 deletions

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 0c170ef3d6..e17ca92f39 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 9730652f52..c2b73c85d4 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 6940f2a078..39630ec388 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 d0ec28ea05..800d890517 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
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index ad74e47361..b1951775ec 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -216,7 +216,8 @@ Syntax tactic
   | reduce_simpl [<<(REDEXP (Simpl))>>] -> ["Simpl"]
   | reduce_cbv [<<(REDEXP (Cbv ($LIST $lf)))>>] -> ["Cbv" (FLAGS ($LIST $lf))]
   | reduce_compute [<<(REDEXP (Cbv (Beta) (Delta) (Iota)))>>] -> [ "Compute" ]
-  | reduce_lazy [<<(REDEXP (Lazy ($LIST $lf)))>>] -> ["Lazy" (FLAGS ($LIST $lf))]
+  | reduce_lazy [<<(REDEXP (Lazy ($LIST $lf)))>>] ->
+    ["Lazy" (FLAGS ($LIST $lf))]
   | reduce_unfold [<<(REDEXP (Unfold ($LIST $unf)))>>] ->
        [ [<hv 3> "Unfold " (UNFOLDLIST ($LIST $unf))] ]
   | reduce_fold [<<(REDEXP (Fold ($LIST $cl)))>>] ->
@@ -231,10 +232,12 @@ Syntax tactic
         [ [1 0] "Delta" (FLAGS ($LIST $F))]
   | flags_iota [<<(FLAGS (Iota) ($LIST $F))>>] ->
         [ [1 0] "Iota" (FLAGS ($LIST $F))]
-  | delta_unf [<<(FLAGS (Unf ($LIST $idl)))>>]
-         -> [ [1 0] "[" [<hov 0> (LISTSPC ($LIST $idl)) ] "]" ]
-  | delta_unfbut [<<(FLAGS (UnfBut ($LIST $idl)))>>]
-         -> [ [1 0] "-[" [<hov 0> (LISTSPC ($LIST $idl)) ] "]" ]
+  | delta_unf [<<(FLAGS (Unf ($LIST $idl)) ($LIST $F))>>]
+         -> [ [1 0] "[" [<hov 0> (LISTSPC ($LIST $idl)) ] "]"
+              (FLAGS ($LIST $F))]
+  | delta_unfbut [<<(FLAGS (UnfBut ($LIST $idl)) ($LIST $F))>>]
+         -> [ [1 0] "-[" [<hov 0> (LISTSPC ($LIST $idl)) ] "]"
+              (FLAGS ($LIST $F))]
   | flags_nil [<<(FLAGS)>>] -> [ ]