X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=a98fb8e9d6cd70116d799750b65b06e285ba7bb4;hb=5649890273cf8e660bba744e84ce5fee1e5efe69;hp=fd3c444b9d26e009e55b23453949e60bd1df5ebe;hpb=b2a190e3c2d5b594d409db937e88f9f4f7d22b8c;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index fd3c444b9..a98fb8e9d 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -73,6 +73,15 @@ let pp_terms ~term_pp terms = String.concat ", " (List.map term_pp terms)
 let opt_string_pp = function
    | None -> ""
    | Some what -> what ^ " "
+ 
+let pp_auto_params ~term_pp (univ, params) = 
+   String.concat " " 
+     (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) ^
+   if univ <> [] then 
+     (if params <> [] then " " else "") ^ "by " ^ 
+     String.concat " " (List.map term_pp univ)
+   else ""
+;;
 
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
  let pp_terms = pp_terms ~term_pp in
@@ -100,12 +109,9 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
   | ApplyS (_, term, params) ->
-     "applyS " ^ term_pp term ^
-      String.concat " " 
-        (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
-  | AutoBatch (_,params) -> "auto batch " ^ 
-      String.concat " " 
-        (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
+     "applyS " ^ term_pp term ^ pp_auto_params ~term_pp params
+  | AutoBatch (_,params) -> "autobatch " ^ 
+      pp_auto_params ~term_pp params
   | Assumption _ -> "assumption"
   | Cases (_, term, specs) -> Printf.sprintf "cases " ^ term_pp term ^
       pp_intros_specs "names " specs 
@@ -126,7 +132,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   | Decompose (_, names) ->
       Printf.sprintf "decompose%s" 
       (pp_intros_specs "names " (None, names)) 
-  | Demodulate _ -> "demodulate"
+  | Demodulate (_, params) -> "demodulate " ^ pp_auto_params ~term_pp params
   | Destruct (_, None) -> "destruct" 
   | Destruct (_, Some terms) -> "destruct " ^ pp_terms terms
   | Elim (_, what, using, pattern, specs) ->
@@ -194,7 +200,20 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   | Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term
   | ExistsElim (_, term0, ident, term, ident1, term1) -> "by " ^ (match term0 with None -> "_" | Some term -> term_pp term) ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ lazy_term_pp term1 ^ "(" ^ ident1 ^ ")"
   | AndElim (_, term, ident1, term1, ident2, term2) -> "by " ^ term_pp term ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")" 
-  | RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some (None,term) -> "conclude " ^ term_pp term | Some (Some name,term) -> "obtain (" ^ name ^ ") " ^ term_pp term) ^ "=" ^ term_pp term1 ^ " by " ^ (match term2 with `Auto params -> "_" ^ String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)  | `Term term2 -> term_pp term2 | `Proof -> "proof") ^ (if cont then " done" else "")
+  | RewritingStep (_, term, term1, term2, cont) -> 
+      (match term with 
+      | None -> " " 
+      | Some (None,term) -> "conclude " ^ term_pp term 
+      | Some (Some name,term) -> 
+          "obtain (" ^ name ^ ") " ^ term_pp term) 
+      ^ "=" ^
+      term_pp term1 ^ 
+      (match term2 with 
+      | `Auto params -> pp_auto_params ~term_pp params
+      | `Term term2 -> " exact " ^ term_pp term2 
+      | `Proof -> " proof"
+      | `SolveWith term -> " using " ^ term_pp term)
+      ^ (if cont then " done" else "")
   | Case (_, id, args) ->
      "case" ^ id ^
        String.concat " "
@@ -242,9 +261,7 @@ let pp_macro ~term_pp =
   | Check (_, term) -> Printf.sprintf "check %s" (term_pp term)
   | Hint (_, true) -> "hint rewrite"
   | Hint (_, false) -> "hint"
-  | AutoInteractive (_,params) -> "auto " ^ 
-      String.concat " " 
-        (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
+  | AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params
   | Inline (_, style, suri, prefix) ->  
       Printf.sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix)