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

diff --git a/helm/software/lambda-delta/src/xml/xmlLibrary.ml b/helm/software/lambda-delta/src/xml/xmlLibrary.ml
index af6245c9f..3bc0c54e0 100644
--- a/helm/software/lambda-delta/src/xml/xmlLibrary.ml
+++ b/helm/software/lambda-delta/src/xml/xmlLibrary.ml
@@ -13,16 +13,22 @@ module F = Filename
 module U = NUri
 module C = Cps
 module H = Hierarchy
+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"
 
@@ -89,7 +95,11 @@ 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
 
@@ -116,12 +126,12 @@ let meta a =
    let f s = "meta", s in
    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;
+   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
@@ -129,8 +139,24 @@ let export_entity pp_term si xdir (a, u, b) =
       | 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