X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fxml%2FxmlLibrary.ml;h=4667b3aa57db8fd9009d17b1416a2fab6c7866c4;hb=f7d7f2459b3b0409be5f168822be3b836ccc929b;hp=5ca87bdfd69231a2ac266e461dba9259479cc97e;hpb=a8a42ce5976221949b3999446eebc5d5457b81bd;p=helm.git

diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml
index 5ca87bdfd..4667b3aa5 100644
--- a/helm/software/helena/src/xml/xmlLibrary.ml
+++ b/helm/software/helena/src/xml/xmlLibrary.ml
@@ -9,14 +9,16 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module F = Filename
-module U = NUri
-module C = Cps
-module H = Hierarchy
-module G = Options
-module E = Entity
-module N = Level
-module Q = Ccs
+module KF = Filename
+
+module U  = NUri
+module C  = Cps
+module G  = Options
+module H  = Hierarchy
+module N  = Layer
+module E  = Entity
+
+IFDEF OBJECTS THEN
 
 (* internal functions *******************************************************)
 
@@ -24,21 +26,17 @@ let base = "xml"
 
 let ext = ".xml"
 
-let obj_root = "ENTITY"
-
-let ccs_name = "ccs.ldc"
+let obj_root = "CONSTANT"
 
-let ccs_root = "CCS"
+let home = "http://lambdadelta.info/"
 
-let home = "http://lambdadelta.info"
-
-let system = home ^ "/" ^ base ^ "/ld.dtd"
+let system = KF.concat (KF.concat home base) "ld.dtd"
 
 let xmlns = "xmlns", home
 
 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)
+   let base = KF.concat xdir base in 
+   KF.concat base (Str.string_after (U.string_of_uri uri) 3)
 
 (* interface functions ******************************************************)
 
@@ -79,7 +77,7 @@ let gref = "GRef"
 
 let cast = "Cast"
 
-let appl = "Appl"
+let appl x = if x then "Appx" else "Appr"
 
 let proj = "Proj"
 
@@ -92,37 +90,34 @@ 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 depth i =
+   "depth", string_of_int i
 
 let uri u =
    "uri", U.string_of_uri u
 
-let arity ?n l =
-   let n = match n with 
-      | None   -> List.length l
-      | Some n -> n   
-   in
-   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
-   E.names f map a ""
+   let err () = "name", "" in
+   let f n r = "name", if r then n else "-" ^ n in 
+   E.name err f a
+
+let layer st n =
+   "layer", N.to_string st n
+
+let main a =
+   let sort, degr = a.E.b_main in
+   ["main-position", string_of_int sort;
+    "main-degree", string_of_int degr;
+   ]
 
-let mark a =
-   let err () = "mark", "" in
-   let f i = "mark", string_of_int i in
-   E.mark err f a
+let side a =
+   let sort, degr = a.E.b_side in
+   ["side-position", string_of_int sort;
+    "side-degree", string_of_int degr;
+   ]
 
-let level n =
-   "level", N.to_string n
+let apix a =
+   "level", string_of_int a.E.n_apix
 
 let meta a =
    let map = function
@@ -131,9 +126,7 @@ let meta a =
       | E.Progress -> "Progress"
       | E.Private  -> "Private"
    in
-   let err () = "meta", "" in
-   let f ms = "meta", String.concat " " (List.rev_map map ms) in
-   E.meta err f a
+   "meta", String.concat " " (List.rev_map map a.E.r_meta)
 
 (* TODO: the string tx must be quoted *)
 let info a =
@@ -141,18 +134,18 @@ let info a =
    let f lg tx = ["lang", lg; "info", tx] in
    E.info err f a
 
-let export_entity pp_term (a, u, b) = 
+let export_entity pp_term (ra, na, u, b) = 
    let path = path_of_uri !G.xdir u in
-   let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
+   let _ = Sys.command (Printf.sprintf "mkdir -p %s" (KF.dirname path)) in
    let och = open_out (path ^ ext) in
    let out = output_string och in
    xml out "1.0" "UTF-8"; doctype out obj_root system;
-   let a = E.Name (U.name_of_uri u, true) :: a in
-   let attrs = uri u :: name a :: mark a :: meta a :: info a in 
+   let ba = E.bind_attrs ~name:(U.name_of_uri u, true) () in
+   let attrs = uri u :: name ba :: apix na :: meta ra :: info ra in 
    let contents = match b with
-      | E.Abst (n, w) -> tag "ABST" (level n :: attrs) ~contents:(pp_term w) 
-      | E.Abbr v      -> tag "ABBR" attrs ~contents:(pp_term v)
-      | E.Void        -> assert false
+      | E.Abst w -> tag "GDec" attrs ~contents:(pp_term w) 
+      | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v)
+      | E.Void   -> assert false
    in
    let opts = if !G.si then "si" else "" in
    let shp = H.string_of_graph () in
@@ -160,34 +153,4 @@ let export_entity pp_term (a, u, b) =
    tag obj_root attrs ~contents out 0;
    close_out och
 
-let prec_map (i, _) = string_of_int i
-
-let next_map (_, i) = string_of_int i
-
-let marks = function
-   | [] -> "mark", ""
-   | l  -> "mark", String.concat " " (List.rev_map string_of_int l)
-
-let precs = function
-   | [] -> "prec", ""
-   | l  -> "prec", String.concat " " (List.rev_map prec_map l)
-
-let nexts = function
-   | [] -> "next", ""
-   | l  -> "next", String.concat " " (List.rev_map next_map l)
-
-let export_csys s = 
-   let path = path_of_uri !G.xdir s.Q.uri in
-   let _ = Sys.command (Printf.sprintf "mkdir -p %s" path) in
-   let name = F.concat path (ccs_name ^ ext) in
-   let och = open_out name in
-   let out = output_string och in
-   xml out "1.0" "UTF-8"; doctype out ccs_root system;
-   let attrs = [xmlns; uri s.Q.uri] in
-   let contents out tab =
-      tag "ToPositive" [arity s.Q.tp; marks s.Q.tp] out tab;
-      tag "ToOne" [arity s.Q.t1; marks s.Q.t1] out tab;
-      tag "ToNext" [arity s.Q.tn; precs s.Q.tn; nexts s.Q.tn] out tab
-   in
-   tag ccs_root attrs ~contents out 0;
-   close_out och
+END