X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fcommon%2Flibrary.ml;h=ff4c54198832220c4154e44d7a62ef3da1a50318;hb=fcbe3e8f67fa42c84a57e343ba5ef6a97ba8ca67;hp=23f156123bfc65802c97aaae19d067c02a58d7bd;hpb=de66af7241ad8ab71d5857d14570e4662f2488dc;p=helm.git

diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml
index 23f156123..ff4c54198 100644
--- a/helm/software/lambda-delta/common/library.ml
+++ b/helm/software/lambda-delta/common/library.ml
@@ -9,48 +9,169 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module F = Filename
+module F = Format
+module N = Filename
 module U = NUri
+module C = Cps
 module H = Hierarchy
+module Y = Entity
 
 (* internal functions *******************************************************)
 
 let base = "xml"
 
-let obj_ext = ".ld.xml"
+let obj_ext = ".xml"
+
+let root = "ENTITY"
 
 let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
 
 let path_of_uri uri =
-   F.concat base (Str.string_after (U.string_of_uri uri) 3)
+   N.concat base (Str.string_after (U.string_of_uri uri) 3)
 
 let pp_head frm = 
-   Format.fprintf frm "<?xml version=%S encoding=%S?>@,@," "1.0" "UTF-8"
+   F.fprintf frm "<?xml version=%S encoding=%S?>@,@," "1.0" "UTF-8"
 
 let pp_doctype frm =
-  Format.fprintf frm "<!DOCTYPE KERNEL SYSTEM %S>@,@," system
+  F.fprintf frm "<!DOCTYPE ENTITY SYSTEM %S>@,@," system
 
-let open_kernel si g frm =
+let open_entity si g frm =
    let opts = if si then "si" else "" in
    let f shp =
-      Format.fprintf frm "<KERNEL hierarchy=%S options=%S>" shp opts
+      F.fprintf frm "<ENTITY hierarchy=%S options=%S>" shp opts
    in
    H.string_of_graph f g
 
-let close_kernel frm =
-   Format.fprintf frm "</KERNEL>" 
+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
 
 (* interface functions ******************************************************)
 
-let export_item export_obj si g = function
-   | Some obj ->
-      let _, uri, bind = obj in
-      let path = path_of_uri uri in
-      let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
-      let och = open_out (path ^ obj_ext) in
-      let frm = Format.formatter_of_out_channel och in
-      Format.pp_set_margin frm max_int;
-      Format.fprintf frm "@[<v>%t%t%t%a%t@]@." 
-         pp_head pp_doctype (open_kernel si g) export_obj obj close_kernel;  
-      close_out och
-   | None     -> ()
+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 pp = och -> int -> unit
+
+let attribute out (name, contents) =
+   if contents <> "" then begin
+      out " "; out name; out "=\""; out contents; out "\""
+   end
+
+let xml out version encoding =
+   out "<?xml";
+      attribute out ("version", version);
+      attribute out ("encoding", encoding);
+   out "?>\n\n"
+
+let doctype out root system =
+   out "<!DOCTYPE "; out root; out " SYSTEM \""; out system; out "\">\n\n"
+
+let tag tag attrs ?contents out indent =
+   let spc = String.make indent ' ' in
+   out spc; out "<"; out tag; List.iter (attribute out) attrs;
+   match contents with
+      | None      -> out "/>\n"
+      | Some cont -> 
+         out ">\n"; cont out (indent + 3); out spc; 
+	 out "</"; out tag; out ">\n"
+
+let sort = "Sort"
+
+let lref = "LRef"
+
+let gref = "GRef"
+
+let cast = "Cast"
+
+let appl = "Appl"
+
+let proj = "Proj"
+
+let abst = "Abst"
+
+let abbr = "Abbr"
+
+let void = "Void"
+
+let position i =
+   "position", string_of_int i
+
+let offset j = 
+   let contents = if j > 0 then string_of_int j else "" in
+   "offset", contents
+
+let uri u =
+   "uri", U.string_of_uri u
+
+let arity n =
+   let contents = if n > 1 then string_of_int n else "" in
+   "arity", contents
+
+let name 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 pp_term si g (a, u, b) =
+   let path = path_of_uri u in
+   let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in
+   let och = open_out (path ^ obj_ext) in
+   let out = output_string och in
+   xml out "1.0" "UTF-8"; doctype out root system;
+   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) 
+   in
+   let opts = if si then "si" else "" in
+   let shp = H.string_of_graph C.start g in
+   let attrs = ["hierarchy", shp; "options", opts] in
+   tag root attrs ~contents out 0;
+   close_out och