X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fcommon%2Flibrary.ml;h=91272c6f839c10bffef60ad44d47ed1334e93ec5;hb=e17c4da82bd52712f03c112660c52eb8f1783843;hp=4951e8c608987e1b5fdb7b8527a83fe066325dee;hpb=cd798346d31b14b8947e5801b87dc4f363607862;p=helm.git

diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml
index 4951e8c60..91272c6f8 100644
--- a/helm/software/lambda-delta/common/library.ml
+++ b/helm/software/lambda-delta/common/library.ml
@@ -9,8 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module F = Format
-module N = Filename
+module F = Filename
 module U = NUri
 module C = Cps
 module H = Hierarchy
@@ -26,68 +25,17 @@ let root = "ENTITY"
 
 let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
 
-let path_of_uri uri =
-   N.concat base (Str.string_after (U.string_of_uri uri) 3)
-
-let pp_head frm = 
-   F.fprintf frm "<?xml version=%S encoding=%S?>@,@," "1.0" "UTF-8"
-
-let pp_doctype frm =
-  F.fprintf frm "<!DOCTYPE ENTITY SYSTEM %S>@,@," system
-
-let open_entity si g frm =
-   let opts = if si then "si" else "" in
-   let f shp =
-      F.fprintf frm "<ENTITY hierarchy=%S options=%S>" shp opts
-   in
-   H.string_of_graph f g
-
-let close_entity frm =
-   F.fprintf frm "</ENTITY>"
-
-let name frm a =
-   let f s = function
-      | true  -> F.fprintf frm " name=%S" s
-      | false -> F.fprintf frm " name=%S" ("^" ^ s)
-   in      
-   Y.name C.start f a
-
-let pp_entity pp_term frm = function
-   | a, u, Y.Abst w -> 
-      let str = U.string_of_uri u in
-      let a = Y.Name (U.name_of_uri u, true) :: a in
-      F.fprintf frm "<ABST uri=%S%a>%a</ABST>" str name a pp_term w
-   | a, u, Y.Abbr v -> 
-      let str = U.string_of_uri u in
-      let a = Y.Name (U.name_of_uri u, true) :: a in
-      F.fprintf frm "<ABBR uri=%S%a>%a</ABBR>" str name a pp_term v
-
-let pp_boxed pp_term frm entity =
-   F.fprintf frm "@,@[<v3>   %a@]@," (pp_entity pp_term) entity
+let path_of_uri xdir uri =
+   let base = F.concat xdir base in 
+   F.concat base (Str.string_after (U.string_of_uri uri) 3)
 
 (* interface functions ******************************************************)
 
-let old_export_entity pp_term si g entity =
-   let _, uri, _ = entity in
-   let path = path_of_uri uri in
-   let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in
-   let och = open_out (path ^ obj_ext) in
-   let frm = F.formatter_of_out_channel och in
-   F.pp_set_margin frm max_int;
-   F.fprintf frm "@[<v>%t%t%t%a%t@]@." 
-      pp_head pp_doctype
-      (open_entity si g) (pp_boxed pp_term) entity close_entity;  
-   close_out och
-
-let old_name = name
-
-(****************************************************************************)
-
 type och = string -> unit
 
 type attr = string * string
 
-type 'a pp = (och -> int -> 'a) -> och -> int -> 'a
+type pp = och -> int -> unit
 
 let attribute out (name, contents) =
    if contents <> "" then begin
@@ -103,14 +51,14 @@ let xml out version encoding =
 let doctype out root system =
    out "<!DOCTYPE "; out root; out " SYSTEM \""; out system; out "\">\n\n"
 
-let tag tag attrs ?contents f out indent =
+let tag tag attrs ?contents out indent =
    let spc = String.make indent ' ' in
-   out spc; out "<"; out "tag"; List.iter (attribute out) attrs;
+   out spc; out "<"; out tag; List.iter (attribute out) attrs;
    match contents with
-      | None      -> out "/>\n"; f out indent
-      | Some cont ->
-         let f _ _ = out spc; out "</"; out tag; out ">\n"; f out indent in
-	 cont f out (indent + 3)
+      | None      -> out "/>\n"
+      | Some cont -> 
+         out ">\n"; cont out (indent + 3); out spc; 
+	 out "</"; out tag; out ">\n"
 
 let sort = "Sort"
 
@@ -145,33 +93,34 @@ let arity n =
    "arity", contents
 
 let name a =
-   let err () = "name", "" in
-   let f s = function
-      | true  -> "name", s
-      | false -> "name", ("^" ^ s)
-   in      
-   Y.name err f a
+   let map f i n r s =
+      let n = if r then n else "^" ^ n in 
+      let spc = if i then "" else " " in
+      f (s ^ n ^ spc)
+   in
+   let f s = "name", s in
+   Y.names f map a ""
 
 let mark a =
    let err () = "mark", "" in
    let f i = "mark", string_of_int i in
    Y.mark err f a
 
-let export_entity f pp_term si g (a, uri, b) =
-   let path = path_of_uri uri in
-   let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in
+let export_entity pp_term si xdir (a, u, b) =
+   let path = path_of_uri xdir u in
+   let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
    let och = open_out (path ^ obj_ext) in
    let out = output_string och in
-   let f _ _ = close_out och; f () in
    xml out "1.0" "UTF-8"; doctype out root system;
-   let str = U.string_of_uri uri in
-   let a = Y.Name (U.name_of_uri uri, true) :: a in
-   let attrs = ["uri", str; name a] in 
+   let a = Y.Name (U.name_of_uri u, true) :: a in
+   let attrs = [uri u; name a; mark a] in 
    let contents = match b with
       | Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w) 
-      | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v) 
+      | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
+      | Y.Void   -> assert false
    in
    let opts = if si then "si" else "" in
-   let shp = H.string_of_graph C.start g in
+   let shp = H.string_of_graph () in
    let attrs = ["hierarchy", shp; "options", opts] in
-   tag root attrs ~contents f out 0;
+   tag root attrs ~contents out 0;
+   close_out och