X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite%2FgrafiteAstPp.ml;h=710761ed9a44537881a73c825f2618eb59ee7900;hb=cd91767a396b7bbc72e6e3ee90a3b758421f935d;hp=d7ed16efd103aa6cdea44040794c135c4fac44ef;hpb=324d594e5e37081d945d631986447a95a1937634;p=helm.git

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index d7ed16efd..710761ed9 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -74,6 +74,21 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   let pp_reduction_kind = pp_reduction_kind ~term_pp in
   let pp_tactic_pattern = pp_tactic_pattern ~lazy_term_pp ~term_pp in
   function
+  (* Higher order tactics *)
+  | Do (_, count, tac) ->
+      sprintf "do %d %s" count (pp_tactic ~term_pp ~lazy_term_pp tac)
+  | Repeat (_, tac) -> "repeat " ^ pp_tactic ~term_pp ~lazy_term_pp tac
+  | Seq (_, tacs) -> pp_tactics ~term_pp ~lazy_term_pp ~sep:"; " tacs
+  | Then (_, tac, tacs) ->
+      sprintf "%s; [%s]" (pp_tactic ~term_pp ~lazy_term_pp tac)
+        (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tacs)
+  | First (_, tacs) ->
+     sprintf "tries [%s]" (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tacs)
+  | Try (_, tac) -> "try " ^ pp_tactic ~term_pp ~lazy_term_pp tac
+  | Solve (_, tac) ->
+     sprintf "solve [%s]" (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tac)
+  | Progress (_, tac) -> "progress " ^ pp_tactic ~term_pp ~lazy_term_pp tac
+  (* First order tactics *)
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
   | ApplyS (_, term, params) ->
@@ -120,7 +135,6 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Generalize (_, pattern, ident) ->
      sprintf "generalize %s%s" (pp_tactic_pattern pattern)
       (match ident with None -> "" | Some id -> " as " ^ id)
-  | Goal (_, n) -> "goal " ^ string_of_int n
   | Fail _ -> "fail"
   | Fourier _ -> "fourier"
   | IdTac _ -> "id"
@@ -177,6 +191,9 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
         (List.map (function (id,term) -> "(" ^ id ^ ": " ^ term_pp term ^  ")")
 	  args)
 
+and pp_tactics ~term_pp ~lazy_term_pp ~sep tacs =
+  String.concat sep (List.map (pp_tactic ~lazy_term_pp ~term_pp) tacs)
+
  let pp_search_kind = function
   | `Locate -> "locate"
   | `Hint -> "hint"
@@ -257,23 +274,8 @@ let pp_command ~term_pp ~obj_pp = function
   | Print (_,s) -> "print " ^ s
   | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
 
-let rec pp_tactical ~term_pp ~lazy_term_pp =
-  let pp_tactic = pp_tactic ~lazy_term_pp ~term_pp in
-  let pp_tacticals = pp_tacticals ~lazy_term_pp ~term_pp in
+let pp_punctuation_tactical ~term_pp ~lazy_term_pp =
   function
-  | Tactic (_, tac) -> pp_tactic tac
-  | Do (_, count, tac) ->
-      sprintf "do %d %s" count (pp_tactical ~term_pp ~lazy_term_pp tac)
-  | Repeat (_, tac) -> "repeat " ^ pp_tactical ~term_pp ~lazy_term_pp tac
-  | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs
-  | Then (_, tac, tacs) ->
-      sprintf "%s; [%s]" (pp_tactical ~term_pp ~lazy_term_pp tac)
-        (pp_tacticals ~sep:" | " tacs)
-  | First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
-  | Try (_, tac) -> "try " ^ pp_tactical ~term_pp ~lazy_term_pp tac
-  | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
-  | Progress (_, tac) -> "progress " ^ pp_tactical ~term_pp ~lazy_term_pp tac
-
   | Dot _ -> "."
   | Semicolon _ -> ";"
   | Branch _ -> "["
@@ -281,21 +283,25 @@ let rec pp_tactical ~term_pp ~lazy_term_pp =
   | Pos (_, i) -> sprintf "%s:" (String.concat "," (List.map string_of_int i))
   | Wildcard _ -> "*:"
   | Merge _ -> "]"
+
+let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp =
+  function
   | Focus (_, goals) ->
       sprintf "focus %s" (String.concat " " (List.map string_of_int goals))
   | Unfocus _ -> "unfocus"
   | Skip _ -> "skip"
 
-and pp_tacticals ~term_pp ~lazy_term_pp ~sep tacs =
-  String.concat sep (List.map (pp_tactical~lazy_term_pp ~term_pp) tacs)
-
 let pp_executable ~term_pp ~lazy_term_pp ~obj_pp =
   function
   | Macro (_, macro) -> pp_macro ~term_pp macro ^ "."
-  | Tactical (_, tac, Some punct) ->
-      pp_tactical ~lazy_term_pp ~term_pp tac
-      ^ pp_tactical ~lazy_term_pp ~term_pp punct
-  | Tactical (_, tac, None) -> pp_tactical ~lazy_term_pp ~term_pp tac
+  | Tactic (_, Some tac, punct) ->
+      pp_tactic ~lazy_term_pp ~term_pp tac
+      ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+  | Tactic (_, None, punct) ->
+     pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+  | NonPunctuationTactical (_, tac, punct) ->
+     pp_non_punctuation_tactical ~lazy_term_pp ~term_pp tac
+     ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
   | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ ".\n"
                       
 let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =