X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fxml%2FxmlLibrary.ml;h=3bc0c54e00fb6ea586115bc803d926bb4bda1a8b;hb=e7f64fe2cc67f3514131c8831f87311ff600d005;hp=8a6801159cea80c6c052bfaf82b54478293ae45c;hpb=bb2a0b22a2c38b59ca664b550f34e5e40e6f04c7;p=helm.git

diff --git a/helm/software/lambda-delta/src/xml/xmlLibrary.ml b/helm/software/lambda-delta/src/xml/xmlLibrary.ml
index 8a6801159..3bc0c54e0 100644
--- a/helm/software/lambda-delta/src/xml/xmlLibrary.ml
+++ b/helm/software/lambda-delta/src/xml/xmlLibrary.ml
@@ -13,15 +13,22 @@ module F = Filename
 module U = NUri
 module C = Cps
 module H = Hierarchy
-module Y = Entity
+module G = Options
+module E = Entity
+module N = Level
+module Q = Ccs
 
 (* internal functions *******************************************************)
 
 let base = "xml"
 
-let obj_ext = ".xml"
+let ext = ".xml"
 
-let root = "ENTITY"
+let obj_root = "ENTITY"
+
+let ccs_name = "ccs.ldc"
+
+let ccs_root = "CCS"
 
 let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
 
@@ -88,45 +95,68 @@ let offset j =
 let uri u =
    "uri", U.string_of_uri u
 
-let arity n =
+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 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 ""
+   E.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
+   E.mark err f a
+
+let level n =
+   "level", N.to_string n
 
 (* TODO: the string s must be quoted *)
 let meta a =
    let err () = "meta", "" in
    let f s = "meta", s in
-   Y.meta err f a
+   E.meta err f a
 
-let export_entity pp_term si xdir (a, u, b) =
-   let path = path_of_uri xdir u in
+let export_entity pp_term (a, u, b) = 
+   let path = path_of_uri !G.xdir u in
    let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
-   let och = open_out (path ^ obj_ext) in
+   let och = open_out (path ^ 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
+   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] 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.Void   -> assert false
+      | 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
    in
-   let opts = if si then "si" else "" in
+   let opts = if !G.si then "si" else "" in
    let shp = H.string_of_graph () in
    let attrs = ["hierarchy", shp; "options", opts] in
-   tag root attrs ~contents out 0;
+   tag obj_root attrs ~contents out 0;
+   close_out och
+
+let marks = function
+   | [] -> "mark", ""
+   | l  -> "mark", String.concat " " (List.rev_map string_of_int 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 = [uri s.Q.uri] in
+   let contents = tag "ToInfinity" [arity s.Q.is; marks s.Q.is] in
+   tag ccs_root attrs ~contents out 0;
    close_out och