X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite%2FgrafiteAstPp.ml;h=8bd5c96f15862677345877c9487e4ce6a96c5501;hb=7be6aeb94aa8da17732511a4844bd108976f947f;hp=7be8c816ebb049a87b408bd3fb0ed8e69c47b11f;hpb=059c1bb4766e823aa53b39fed7d3dd55b4a06101;p=helm.git

diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml
index 7be8c816e..8bd5c96f1 100644
--- a/helm/ocaml/grafite/grafiteAstPp.ml
+++ b/helm/ocaml/grafite/grafiteAstPp.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 open GrafiteAst
@@ -34,6 +36,7 @@ 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"
@@ -170,25 +173,6 @@ let pp_macro ~term_pp = function
   | Print (_, name) -> sprintf "Print \"%s\"" name
   | Quit _ -> "Quit"
 
-let pp_alias = function
-  | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri
-  | Symbol_alias (symb, instance, desc) ->
-      sprintf "alias symbol \"%s\" (instance %d) = \"%s\""
-        symb instance desc
-  | Number_alias (instance,desc) ->
-      sprintf "alias num (instance %d) = \"%s\"" instance desc
-  
-let pp_argument_pattern = function
-  | CicNotationPt.IdentArg (eta_depth, name) ->
-      let eta_buf = Buffer.create 5 in
-      for i = 1 to eta_depth do
-        Buffer.add_string eta_buf "\\eta."
-      done;
-      sprintf "%s%s" (Buffer.contents eta_buf) name
-
-let pp_l1_pattern = CicNotationPp.pp_term
-let pp_l2_pattern = CicNotationPp.pp_term
-
 let pp_associativity = function
   | Gramext.LeftA -> "left associative"
   | Gramext.RightA -> "right associative"
@@ -201,24 +185,10 @@ let pp_dir_opt = function
   | Some `LeftToRight -> "> "
   | Some `RightToLeft -> "< "
 
-let pp_interpretation dsc symbol arg_patterns cic_appl_pattern = 
-  sprintf "interpretation \"%s\" '%s %s = %s"
-    dsc symbol
-    (String.concat " " (List.map pp_argument_pattern arg_patterns))
-    (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern)
- 
 let pp_default what uris = 
   sprintf "default \"%s\" %s" what
     (String.concat " " (List.map UriManager.string_of_uri uris))
 
-let pp_notation dir_opt l1_pattern assoc prec l2_pattern = 
-  sprintf "notation %s\"%s\" %s %s for %s"
-    (pp_dir_opt dir_opt)
-    (pp_l1_pattern l1_pattern)
-    (pp_associativity assoc)
-    (pp_precedence prec)
-    (pp_l2_pattern l2_pattern)
-    
 let pp_coercion uri do_composites =
    sprintf "coercion %s (* %s *)" (UriManager.string_of_uri uri)
      (if do_composites then "compounds" else "no compounds")
@@ -229,16 +199,9 @@ let pp_command ~obj_pp = function
   | Drop _ -> "drop"
   | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
   | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites
-  | Alias (_,s) -> pp_alias s
   | Obj (_,obj) -> obj_pp obj
   | Default (_,what,uris) ->
       pp_default what uris
-  | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
-      pp_interpretation dsc symbol arg_patterns cic_appl_pattern
-  | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
-      pp_notation dir_opt l1_pattern assoc prec l2_pattern
-  | Render _
-  | Dump _ -> assert false  (* ZACK: debugging *)
 
 let rec pp_tactical ~term_pp ~lazy_term_pp =
   let pp_tactic = pp_tactic ~lazy_term_pp ~term_pp in
@@ -289,9 +252,3 @@ let pp_statement ~term_pp ~lazy_term_pp ~obj_pp =
   function
   | Executable (_, ex) -> pp_executable ~lazy_term_pp ~term_pp ~obj_pp ex
   | Comment (_, c) -> pp_comment ~term_pp ~lazy_term_pp ~obj_pp c
-  
-let pp_dependency = function
-  | IncludeDep str -> "include \"" ^ str ^ "\""
-  | BaseuriDep str -> "set \"baseuri\" \"" ^ str ^ "\""
-  | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\""
-