X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=df436e7097cefe67fb842f59414a9f3258ad6b12;hb=6a5e51c1cf9a56c74a8b53a9b8bc5aa686c9780e;hp=0b448659484067634158e73c91f023b0c6c02956;hpb=bb6a5a4cb3f8bc14764bb31eb46225004ad38cd0;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 0b4486594..df436e709 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -68,13 +68,29 @@ let pp_intros_specs s = function
    | None, idents     -> Printf.sprintf " %s%s" s (pp_idents idents)
    | Some num, idents -> Printf.sprintf " %s%i %s" s num (pp_idents idents)
 
-let terms_pp ~term_pp terms = String.concat ", " (List.map term_pp terms)
+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 pp_just ~term_pp =
+ function
+    `Term term -> "exact " ^ term_pp term
+  | `Auto params -> pp_auto_params ~term_pp params
+;;
 
 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
  let pp_reduction_kind = pp_reduction_kind ~term_pp in
  let pp_tactic_pattern =
@@ -98,15 +114,14 @@ 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
+  | ApplyP (_, term) -> "applyP " ^ 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 ^
+  | Cases (_, term, pattern, specs) -> Printf.sprintf "cases " ^ 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)
@@ -125,8 +140,9 @@ 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"
-  | Destruct (_, term) -> "destruct " ^ term_pp term
+  | Demodulate (_, params) -> "demodulate " ^ pp_auto_params ~term_pp params
+  | Destruct (_, None) -> "destruct" 
+  | Destruct (_, Some terms) -> "destruct " ^ pp_terms terms
   | Elim (_, what, using, pattern, specs) ->
       Printf.sprintf "elim %s%s %s%s" 
       (term_pp what)
@@ -158,7 +174,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
         (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 terms with [] -> "" | _ -> " to " ^ pp_terms terms)
         (match ident_opt with None -> "" | Some ident -> " as " ^ ident)
   | Left _ -> "left"
   | LetIn (_, term, ident) -> 
@@ -177,23 +193,35 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   | Right _ -> "right"
   | Ring _ -> "ring"
   | Split _ -> "split"
-  | Subst _ -> "subst"
   | Symmetry _ -> "symmetry"
   | Transitivity (_, term) -> "transitivity " ^ term_pp term
   (* Tattiche Aggiunte *)
   | Assume (_, ident , term) -> "assume" ^ ident ^ ":" ^ term_pp term 
   | Suppose (_, term, ident,term1) -> "suppose" ^ term_pp term ^ "("  ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
-  | Bydone (_, term) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "done"
-  | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term)  ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^
+  | Bydone (_, just) ->  pp_just ~term_pp just ^ "done"
+  | By_just_we_proved (_, just, term1, ident, term2) -> pp_just ~term_pp just  ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^
        (match term2 with  None -> " " | Some term2 -> term_pp term2)
   | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ (match ident with None -> "" | Some ident -> "(" ^ ident ^ ")") ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
   | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on" ^ term_pp term ^ "to prove" ^ term_pp term1
   | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ term_pp term ^ "to prove" ^ term_pp term1
   | Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ term_pp term ^ "(" ^ ident ^ ")"
   | 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 "")
+  | ExistsElim (_, just, ident, term, ident1, term1) -> pp_just ~term_pp just ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ lazy_term_pp term1 ^ "(" ^ ident1 ^ ")"
+  | AndElim (_, just, ident1, term1, ident2, term2) -> pp_just ~term_pp just ^ "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 ^ 
+      (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 " "
@@ -230,6 +258,17 @@ 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
   function 
   (* Whelp *)
   | WInstance (_, term) -> "whelp instance " ^ term_pp term
@@ -239,12 +278,11 @@ let pp_macro ~term_pp =
   | WMatch (_, term) -> "whelp match " ^ term_pp term
   (* real macros *)
   | Check (_, term) -> Printf.sprintf "check %s" (term_pp term)
-  | Hint _ -> "hint"
-  | AutoInteractive (_,params) -> "auto " ^ 
-      String.concat " " 
-        (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
-  | Inline (_, style, suri, prefix) ->  
-      Printf.sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix) 
+  | Hint (_, true) -> "hint rewrite"
+  | Hint (_, false) -> "hint"
+  | AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params
+  | 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"
@@ -262,13 +300,15 @@ 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 =
-   Printf.sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity
-     (if do_composites then "compounds" else "no compounds")
+let pp_coercion ~term_pp t do_composites arity saturations=
+   Printf.sprintf "coercion %s %d %d %s"
+    (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) -> pp_coercion uri do_composites i
+  | Coercion (_, t, do_composites, i, j) ->
+     pp_coercion ~term_pp t do_composites i j
   | Default (_,what,uris) -> pp_default what uris
   | Drop _ -> "drop"
   | Include (_,path) -> "include \"" ^ path ^ "\""