lambda-delta/toplevel: improved transformation from automath (20 secs gained)

[helm.git] / helm / software / lambda-delta / toplevel / metaOutput.ml

diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml
index 7a15d07c250c5fa844958d63beeaab9a5b104384..a12818ee358b8b2234a89273cc0294a13545b5c3 100644 (file)
--- a/helm/software/lambda-delta/toplevel/metaOutput.ml
+++ b/helm/software/lambda-delta/toplevel/metaOutput.ml
@@ -24,6 +24,7 @@
  *)
 
 module F = Format
+module U = NUri
 module M = Meta
 
 type counters = {
@@ -103,10 +104,6 @@ let string_of_sort = function
    | true -> "Type"
    | false -> "Prop"
 
-let string_of_qid (id, path) =
-   let path = String.concat "/" path in
-   Filename.concat path id
-
 let string_of_transparent = function
    | true  -> "="
    | false -> "~"
@@ -124,17 +121,17 @@ let rec pp_args frm args = pp_list pp_term "(" "," ")" frm args
 and pp_term frm = function
    | M.Sort s            -> 
       F.fprintf frm "@[*%s@]" (string_of_sort s)
-   | M.LRef i            ->
-      F.fprintf frm "@[#%u@]" i
-   | M.GRef (l, qid, ts) ->
-      F.fprintf frm "@[%u@@$%s%a@]" l (string_of_qid qid) pp_args ts
+   | M.LRef (l, i)       ->
+      F.fprintf frm "@[%u@@#%u@]" l i
+   | M.GRef (l, uri, ts) ->
+      F.fprintf frm "@[%u@@$%s%a@]" l (U.string_of_uri uri) pp_args ts
    | M.Appl (v, t)       ->
       F.fprintf frm "@[(%a).%a@]" pp_term v pp_term t
    | M.Abst (id, w, t)   ->
       F.fprintf frm "@[[%s:%a].%a@]" id pp_term w pp_term t
 
-let pp_par frm (qid, w) =
-    F.fprintf frm "%s:%a" (string_of_qid qid) pp_term w
+let pp_par frm (id, w) =
+    F.fprintf frm "%s:%a" id pp_term w
 
 let pp_pars = pp_list pp_par "[" "," "]"
 
@@ -143,9 +140,9 @@ let pp_body frm = function
    | Some (trans, t) ->
       F.fprintf frm "%s%a" (string_of_transparent trans) pp_term t
 
-let pp_entry frm (l, pars, qid, u, body) =
+let pp_entry frm (l, pars, uri, u, body) =
    F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" 
-      l (string_of_qid qid) pp_pars pars pp_body body pp_term u
+      l (U.string_of_uri uri) pp_pars pars pp_body body pp_term u
 
 let pp_item f frm = function 
    | Some entry -> pp_entry frm entry; f ()