Big commit to let Ferruccio try the merge_coercion patch.

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

diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml
index ce4a585b3e609d52b510af84c0632e74c1356453..dac1d6e051e6e81b05cf9eda4b5e038ddea3b410 100644 (file)
--- a/helm/ocaml/grafite/grafiteAstPp.ml
+++ b/helm/ocaml/grafite/grafiteAstPp.ml
@@ -206,30 +206,47 @@ 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_ast term do_composites =
+   sprintf "coercion %s (* %s *)" (pp_term_ast term) 
+     (if do_composites then "compounds" else "no compounds")
+
+let pp_coercion_cic term do_composites =
+   sprintf "coercion %s (* %s *)" (pp_term_cic term) 
+     (if do_composites then "compounds" else "no compounds")
+    
 let pp_command = function
   | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"
   | Drop _ -> "drop"
   | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
-  | Coercion (_,term, _do_composites) ->
-     sprintf "coercion %s" (pp_term_ast term)
+  | Coercion (_,term, do_composites) ->
+      pp_coercion_ast term do_composites
   | Alias (_,s) -> pp_alias s
   | Obj (_,obj) -> CicNotationPp.pp_obj obj
   | Default (_,what,uris) ->
-     sprintf "default \"%s\" %s" what
-      (String.concat " " (List.map UriManager.string_of_uri uris))
+      pp_default what uris
   | 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)
+      pp_interpretation dsc symbol arg_patterns cic_appl_pattern
   | 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)
+      pp_notation dir_opt l1_pattern assoc prec l2_pattern
   | Render _
   | Dump _ -> assert false  (* ZACK: debugging *)
 
@@ -275,20 +292,25 @@ let pp_statement = function
   | Executable (_, ex) -> pp_executable ex
   | Comment (_, c) -> pp_comment c
 
+
+  
 let pp_cic_command = function
   | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"
   | Drop _ -> "drop"
-  | Coercion (_,term,_add_composites) ->
-     sprintf "coercion %s" (CicPp.ppterm term)
-  | Set _
-  | Alias _
-  | Default _
-  | Render _
-  | Dump _
-  | Interpretation _
-  | Notation _
-  | Obj _ -> assert false (* not implemented *)
+  | Coercion (_,term, do_composites) ->
+      pp_coercion_cic term do_composites
+  | Obj (_,obj) -> CicPp.ppobj obj
+  | Set _-> assert false (* not implemented *)
+  | Alias (_, alias) -> pp_alias alias
+  | Default (_,what,uris) ->
+      pp_default what uris
+  | Render _ -> assert false (* not implemented *)
+  | Dump _ -> assert false (* not implemented *)
+  | 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
 
 let pp_dependency = function
   | IncludeDep str -> "include \"" ^ str ^ "\""