]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataPp.ml
fixed Makefile
[helm.git] / helm / ocaml / metadata / metadataPp.ml
index e2e21662b371a3c58711d30d569aa4b27ecdc92e..63a1a0955a55b8ee1f5189aaa3b58f3672c1e06d 100644 (file)
@@ -59,7 +59,7 @@ let uri_of_pos pos = String.concat "#" [metadata_ns; pp_position pos]
 
 type t = [ `Int of int | `String of string | `Null ]
 
-let columns_of_metadata ~about metadatas =
+let columns_of_metadata_aux ~about metadata =
   let sort s = `String (CicPp.ppsort s) in
   let source = `String about in
   let occurrence u = `String u in
@@ -76,15 +76,24 @@ let columns_of_metadata ~about metadatas =
           let (p, d) = columns_of_position p in
           sort_cols, rel_cols,
           [source; occurrence o; p; d] :: obj_cols)
-    ([], [], []) metadatas
+    ([], [], []) metadata
 
-let columns_of_ind_metadata ind_metadata =
+let columns_of_metadata metadata =
   List.fold_left
-    (fun (sort_cols, rel_cols, obj_cols) (uri, _, metadatas) ->
-      let (s, r, o) = columns_of_metadata ~about:uri metadatas in
+    (fun (sort_cols, rel_cols, obj_cols) (uri, _, metadata) ->
+      let (s, r, o) = columns_of_metadata_aux ~about:uri metadata in
       (List.append sort_cols s, List.append rel_cols r, List.append obj_cols o))
-    ([], [], []) ind_metadata
+    ([], [], []) metadata
 
+let pp_constr =
+  function
+    | `Sort (sort, p) -> 
+       sprintf "Sort %s; [%s]" 
+         (CicPp.ppsort sort) (String.concat ";" (List.map pp_position p))
+    | `Rel p -> sprintf "Rel [%s]" (String.concat ";" (List.map pp_position p))
+    | `Obj (uri, p) -> sprintf "Obj %s; [%s]" 
+       uri (String.concat ";" (List.map pp_position p))
 (*
 let pp_columns ?(sep = "\n") (sort_cols, rel_cols, obj_cols) =
   String.concat sep