GrafiteAst.Quit (unused) removed.

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

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 9e1dffdcd48c226207b7da9ffd718303eb3ad1c2..d35a8af114936570f77f4be4366d655d04bd0b2b 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -36,7 +36,6 @@ let command_terminator = tactical_terminator
 let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
 
 let pp_reduction_kind ~term_pp = function
-  | `Demodulate -> "demodulate"
   | `Normalize -> "normalize"
   | `Reduce -> "reduce"
   | `Simpl -> "simplify"
@@ -66,6 +65,10 @@ let pp_intros_specs = function
 
 let terms_pp ~term_pp terms = String.concat ", " (List.map term_pp terms)
 
+let opt_string_pp = function
+   | None -> ""
+   | Some what -> what ^ " "
+
 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
@@ -73,12 +76,13 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
   | ApplyS (_, term) -> "applyS " ^ term_pp term
-  | Auto (_,_,_,Some kind,_) -> "auto " ^ kind
-  | Auto _ -> "auto"
+  | Auto (_,params) -> "auto " ^ 
+      String.concat " " 
+        (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
   | Assumption _ -> "assumption"
   | Change (_, where, with_what) ->
       sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
-  | Clear (_,id) -> sprintf "clear %s" id
+  | Clear (_,ids) -> sprintf "clear %s" (pp_idents ids)
   | ClearBody (_,id) -> sprintf "clearbody %s" id
   | Constructor (_,n) -> "constructor " ^ string_of_int n
   | Contradiction _ -> "contradiction"
@@ -86,14 +90,15 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
      "cut " ^ term_pp term ^
       (match ident with None -> "" | Some id -> " as " ^ id)
   | Decompose (_, [], what, names) ->
-      sprintf "decompose %s%s" what (pp_intros_specs (None, names)) 
+      sprintf "decompose %s%s" (opt_string_pp what) (pp_intros_specs (None, names)) 
   | Decompose (_, types, what, names) ->
       let to_ident = function
          | Ident id -> id
         | Type _   -> assert false 
       in
       let types = List.rev_map to_ident types in
-      sprintf "decompose %s %s%s" (pp_idents types) what (pp_intros_specs (None, names)) 
+      sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names)) 
+  | Demodulate _ -> "demodulate"
   | Discriminate (_, term) -> "discriminate " ^ term_pp term
   | Elim (_, term, using, num, idents) ->
       sprintf "elim " ^ term_pp term ^
@@ -110,7 +115,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
        (lazy_term_pp term) (pp_tactic_pattern pattern)
   | FwdSimpl (_, hyp, idents) -> 
       sprintf "fwd %s%s" hyp 
-        (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
+        (match idents with [] -> "" | idents -> " as " ^ pp_idents idents)
   | Generalize (_, pattern, ident) ->
      sprintf "generalize %s%s" (pp_tactic_pattern pattern)
       (match ident with None -> "" | Some id -> " as " ^ id)
@@ -125,9 +130,10 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       sprintf "intros%s%s"
         (match num with None -> "" | Some num -> " " ^ string_of_int num)
         (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
-  | LApply (_, level_opt, terms, term, ident_opt) -> 
-      sprintf "lapply %s%s%s%s" 
-        (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")  
+  | LApply (_, linear, level_opt, terms, term, ident_opt) -> 
+      sprintf "lapply %s%s%s%s%s" 
+        (if linear then " linear " else "")
+       (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")  
         (term_pp term) 
         (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms)
         (match ident_opt with None -> "" | Some ident -> " as " ^ ident)
@@ -148,8 +154,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Split _ -> "split"
   | Symmetry _ -> "symmetry"
   | Transitivity (_, term) -> "transitivity " ^ term_pp term
-
-let pp_search_kind = function
+  
+  let pp_search_kind = function
   | `Locate -> "locate"
   | `Hint -> "hint"
   | `Match -> "match"
@@ -176,12 +182,6 @@ let pp_macro ~term_pp =
   (* real macros *)
   | Check (_, term) -> sprintf "Check %s" (term_pp term)
   | Hint _ -> "hint"
-  | Search_pat (_, kind, pat) ->
-      sprintf "search %s \"%s\"" (pp_search_kind kind) pat
-  | Search_term (_, kind, term) ->
-      sprintf "search %s %s" (pp_search_kind kind) (term_pp term)
-  | Print (_, name) -> sprintf "Print \"%s\"" name
-  | Quit _ -> "Quit"
 
 let pp_associativity = function
   | Gramext.LeftA -> "left associative"