helm/software/helena/src/xml/xmlLibrary.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module KF = Filename
  13
  14 module U  = NUri
  15 module C  = Cps
  16 module G  = Options
  17 module H  = Hierarchy
  18 module N  = Layer
  19 module E  = Entity
  20
  21 IFDEF OBJECTS THEN
  22
  23 (* internal functions *******************************************************)
  24
  25 let base = "xml"
  26
  27 let ext = ".xml"
  28
  29 let obj_root = "CONSTANT"
  30
  31 let home = "http://lambdadelta.info/"
  32
  33 let system = KF.concat (KF.concat home base) "ld.dtd"
  34
  35 let xmlns = "xmlns", home
  36
  37 let path_of_uri xdir uri =
  38    let base = KF.concat xdir base in
  39    KF.concat base (Str.string_after (U.string_of_uri uri) 3)
  40
  41 (* interface functions ******************************************************)
  42
  43 type och = string -> unit
  44
  45 type attr = string * string
  46
  47 type pp = och -> int -> unit
  48
  49 let attribute out (name, contents) =
  50    if contents <> "" then begin
  51       out " "; out name; out "=\""; out contents; out "\""
  52    end
  53
  54 let xml out version encoding =
  55    out "<?xml";
  56       attribute out ("version", version);
  57       attribute out ("encoding", encoding);
  58    out "?>\n\n"
  59
  60 let doctype out root system =
  61    out "<!DOCTYPE "; out root; out " SYSTEM \""; out system; out "\">\n\n"
  62
  63 let tag tag attrs ?contents out indent =
  64    let spc = String.make indent ' ' in
  65    out spc; out "<"; out tag; List.iter (attribute out) attrs;
  66    match contents with
  67       | None      -> out "/>\n"
  68       | Some cont ->
  69          out ">\n"; cont out (indent + 3); out spc;
  70          out "</"; out tag; out ">\n"
  71
  72 let sort = "Sort"
  73
  74 let lref = "LRef"
  75
  76 let gref = "GRef"
  77
  78 let cast = "Cast"
  79
  80 let appl x = if x then "Appx" else "Appr"
  81
  82 let proj = "Proj"
  83
  84 let abst = "Abst"
  85
  86 let abbr = "Abbr"
  87
  88 let void = "Void"
  89
  90 let position i =
  91    "position", string_of_int i
  92
  93 let depth i =
  94    "depth", string_of_int i
  95
  96 let uri u =
  97    "uri", U.string_of_uri u
  98
  99 let name a =
 100    let err () = "name", "" in
 101    let f n r = "name", if r then n else "-" ^ n in
 102    E.name err f a
 103
 104 let layer st n =
 105    "layer", N.to_string st n
 106
 107 let main a =
 108    let sort, degr = a.E.b_main in
 109    ["main-position", string_of_int sort;
 110     "main-degree", string_of_int degr;
 111    ]
 112
 113 let side a =
 114    let sort, degr = a.E.b_side in
 115    ["side-position", string_of_int sort;
 116     "side-degree", string_of_int degr;
 117    ]
 118
 119 let apix a =
 120    "level", string_of_int a.E.n_apix
 121
 122 let meta a =
 123    let map = function
 124       | E.Main     -> "Main"
 125       | E.InProp   -> "InProp"
 126       | E.Progress -> "Progress"
 127       | E.Private  -> "Private"
 128    in
 129    "meta", String.concat " " (List.rev_map map a.E.r_meta)
 130
 131 (* TODO: the string tx must be quoted *)
 132 let info a =
 133    let err () = ["lang", ""; "info", ""] in
 134    let f lg tx = ["lang", lg; "info", tx] in
 135    E.info err f a
 136
 137 let export_entity pp_term (ra, na, u, b) =
 138    let path = path_of_uri !G.xdir u in
 139    let _ = Sys.command (Printf.sprintf "mkdir -p %s" (KF.dirname path)) in
 140    let och = open_out (path ^ ext) in
 141    let out = output_string och in
 142    xml out "1.0" "UTF-8"; doctype out obj_root system;
 143    let ba = E.bind_attrs ~name:(U.name_of_uri u, true) () in
 144    let attrs = uri u :: name ba :: apix na :: meta ra :: info ra in
 145    let contents = match b with
 146       | E.Abst w -> tag "GDec" attrs ~contents:(pp_term w)
 147       | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v)
 148       | E.Void   -> assert false
 149    in
 150    let opts = if !G.si then "si" else "" in
 151    let shp = H.string_of_graph () in
 152    let attrs = [xmlns; "hierarchy", shp; "options", opts] in
 153    tag obj_root attrs ~contents out 0;
 154    close_out och
 155
 156 END