]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/xml/xmlLibrary.ml
last commit for helena 0.8.1
[helm.git] / helm / software / lambda-delta / src / xml / xmlLibrary.ml
index 3bc0c54e00fb6ea586115bc803d926bb4bda1a8b..7355c98a76d8d4516c99fb411c6bad3c66e6f8d8 100644 (file)
@@ -145,10 +145,22 @@ 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
@@ -157,6 +169,10 @@ let export_csys s =
    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
+   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