new tactics are almost ready

[helm.git] / helm / software / components / grafite / grafiteAstPp.ml

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 84facde66203a3e9ac62ba4c1afe4c1b5120f3c0..a33bf6d9de125941874d2de94be0d068d1f55fa3 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -89,6 +89,10 @@ let pp_just ~term_pp =
   | `Auto params -> pp_auto_params ~term_pp params
 ;;
 
+let pp_ntactic ~map_unicode_to_tex = function
+  | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+;;
+
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
  let pp_terms = pp_terms ~term_pp in
  let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in
@@ -114,14 +118,18 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   (* First order tactics *)
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
+  | ApplyRule (_, term) -> "apply rule " ^ term_pp term
+  | ApplyP (_, term) -> "applyP " ^ term_pp term
   | ApplyS (_, term, params) ->
      "applyS " ^ term_pp term ^ pp_auto_params ~term_pp params
   | AutoBatch (_,params) -> "autobatch " ^ 
       pp_auto_params ~term_pp params
   | Assumption _ -> "assumption"
-  | Cases (_, term, pattern, specs) -> Printf.sprintf "cases " ^ term_pp term ^
-      pp_tactic_pattern pattern ^
-      pp_intros_specs "names " specs 
+  | Cases (_, term, pattern, specs) -> 
+      Printf.sprintf "cases %s %s%s" 
+      (term_pp term)
+      (pp_tactic_pattern pattern)
+      (pp_intros_specs "names " specs)
   | Change (_, where, with_what) ->
       Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
   | Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids)
@@ -247,7 +255,7 @@ let pp_arg ~term_pp arg =
    else
      "(" ^ s ^ ")"
   
-let pp_macro ~term_pp = 
+let pp_macro ~term_pp ~lazy_term_pp = 
   let term_pp = pp_arg ~term_pp in
   let style_pp = function
      | Declarative         -> ""
@@ -257,6 +265,18 @@ let pp_macro ~term_pp =
   let prefix_pp prefix = 
      if prefix = "" then "" else Printf.sprintf " \"%s\"" prefix
   in
+  let flavour_pp = function
+     | None                   -> ""
+     | Some `Definition       -> " as definition"
+     | Some `MutualDefinition -> " as mutual"
+     | Some `Fact             -> " as fact"
+     | Some `Lemma            -> " as lemma"
+     | Some `Remark           -> " as remark"
+     | Some `Theorem          -> " as theorem"
+     | Some `Variant          -> " as variant"
+     | Some `Axiom            -> " as axiom"
+  in
+  let pp_reduction_kind = pp_reduction_kind ~term_pp:lazy_term_pp in
   function 
   (* Whelp *)
   | WInstance (_, term) -> "whelp instance " ^ term_pp term
@@ -265,12 +285,14 @@ let pp_macro ~term_pp =
   | WElim (_, t) -> "whelp elim " ^ term_pp t
   | WMatch (_, term) -> "whelp match " ^ term_pp term
   (* real macros *)
+  | Eval (_, kind, term) -> 
+      Printf.sprintf "eval %s on %s" (pp_reduction_kind kind) (term_pp term) 
   | Check (_, term) -> Printf.sprintf "check %s" (term_pp term)
   | Hint (_, true) -> "hint rewrite"
   | Hint (_, false) -> "hint"
   | 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) 
+  | Inline (_, style, suri, prefix, flavour) ->  
+      Printf.sprintf "inline %s\"%s\"%s%s" (style_pp style) suri (prefix_pp prefix) (flavour_pp flavour) 
 
 let pp_associativity = function
   | Gramext.LeftA -> "left associative"
@@ -288,15 +310,19 @@ let pp_default what uris =
   Printf.sprintf "default \"%s\" %s" what
     (String.concat " " (List.map UriManager.string_of_uri uris))
 
-let pp_coercion uri do_composites arity saturations=
+let pp_coercion ~term_pp t do_composites arity saturations=
    Printf.sprintf "coercion %s %d %d %s"
-    (UriManager.string_of_uri uri) arity saturations
+    (term_pp t) arity saturations
     (if do_composites then "" else "nocomposites")
     
 let pp_command ~term_pp ~obj_pp = function
   | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
-  | Coercion (_, uri, do_composites, i, j) ->
-     pp_coercion uri do_composites i j
+  | Coercion (_, t, do_composites, i, j) ->
+     pp_coercion ~term_pp t do_composites i j
+  | PreferCoercion (_,t) -> 
+     "prefer coercion " ^ term_pp t
+  | UnificationHint (_,t, n) -> 
+      "unification hint " ^ string_of_int n ^ " " ^ term_pp t
   | Default (_,what,uris) -> pp_default what uris
   | Drop _ -> "drop"
   | Include (_,path) -> "include \"" ^ path ^ "\""
@@ -315,8 +341,9 @@ let pp_command ~term_pp ~obj_pp = function
        | None -> "")
   | Print (_,s) -> "print " ^ s
   | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value
+  | NObj (_,o) -> "not supported"
 
-let pp_punctuation_tactical ~term_pp ~lazy_term_pp =
+let pp_punctuation_tactical =
   function
   | Dot _ -> "."
   | Semicolon _ -> ";"
@@ -326,7 +353,7 @@ let pp_punctuation_tactical ~term_pp ~lazy_term_pp =
   | Wildcard _ -> "*:"
   | Merge _ -> "]"
 
-let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp =
+let pp_non_punctuation_tactical =
   function
   | Focus (_, goals) ->
       Printf.sprintf "focus %s" (String.concat " " (List.map string_of_int goals))
@@ -335,15 +362,20 @@ let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp =
 
 let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =
   function
-  | Macro (_, macro) -> pp_macro ~term_pp macro ^ "."
+  | Macro (_, macro) -> pp_macro ~term_pp ~lazy_term_pp macro ^ "."
   | Tactic (_, Some tac, punct) ->
-      pp_tactic ~map_unicode_to_tex ~lazy_term_pp ~term_pp tac
-      ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+      pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp tac
+      ^ pp_punctuation_tactical punct
   | Tactic (_, None, punct) ->
-     pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+     pp_punctuation_tactical punct
+  | NTactic (_,Some tac, punct) ->
+     pp_ntactic ~map_unicode_to_tex tac
+     ^ pp_punctuation_tactical punct
+  | NTactic (_,None, punct) ->
+     pp_punctuation_tactical punct
   | NonPunctuationTactical (_, tac, punct) ->
-     pp_non_punctuation_tactical ~lazy_term_pp ~term_pp tac
-     ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+     pp_non_punctuation_tactical tac
+     ^ pp_punctuation_tactical punct
   | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "."
                       
 let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =