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