helm/software/lambda-delta/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 F = Filename
  13 module U = NUri
  14 module C = Cps
  15 module H = Hierarchy
  16 module E = Entity
  17
  18 (* internal functions *******************************************************)
  19
  20 let base = "xml"
  21
  22 let obj_ext = ".xml"
  23
  24 let root = "ENTITY"
  25
  26 let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
  27
  28 let path_of_uri xdir uri =
  29    let base = F.concat xdir base in
  30    F.concat base (Str.string_after (U.string_of_uri uri) 3)
  31
  32 (* interface functions ******************************************************)
  33
  34 type och = string -> unit
  35
  36 type attr = string * string
  37
  38 type pp = och -> int -> unit
  39
  40 let attribute out (name, contents) =
  41    if contents <> "" then begin
  42       out " "; out name; out "=\""; out contents; out "\""
  43    end
  44
  45 let xml out version encoding =
  46    out "<?xml";
  47       attribute out ("version", version);
  48       attribute out ("encoding", encoding);
  49    out "?>\n\n"
  50
  51 let doctype out root system =
  52    out "<!DOCTYPE "; out root; out " SYSTEM \""; out system; out "\">\n\n"
  53
  54 let tag tag attrs ?contents out indent =
  55    let spc = String.make indent ' ' in
  56    out spc; out "<"; out tag; List.iter (attribute out) attrs;
  57    match contents with
  58       | None      -> out "/>\n"
  59       | Some cont ->
  60          out ">\n"; cont out (indent + 3); out spc;
  61          out "</"; out tag; out ">\n"
  62
  63 let sort = "Sort"
  64
  65 let lref = "LRef"
  66
  67 let gref = "GRef"
  68
  69 let cast = "Cast"
  70
  71 let appl = "Appl"
  72
  73 let proj = "Proj"
  74
  75 let abst = "Abst"
  76
  77 let abbr = "Abbr"
  78
  79 let void = "Void"
  80
  81 let position i =
  82    "position", string_of_int i
  83
  84 let offset j =
  85    let contents = if j > 0 then string_of_int j else "" in
  86    "offset", contents
  87
  88 let uri u =
  89    "uri", U.string_of_uri u
  90
  91 let arity n =
  92    let contents = if n > 1 then string_of_int n else "" in
  93    "arity", contents
  94
  95 let name a =
  96    let map f i n r s =
  97       let n = if r then n else "-" ^ n in
  98       let spc = if i then "" else " " in
  99       f (s ^ n ^ spc)
 100    in
 101    let f s = "name", s in
 102    E.names f map a ""
 103
 104 let mark a =
 105    let err () = "mark", "" in
 106    let f i = "mark", string_of_int i in
 107    E.mark err f a
 108
 109 (* TODO: the string s must be quoted *)
 110 let meta a =
 111    let err () = "meta", "" in
 112    let f s = "meta", s in
 113    E.meta err f a
 114
 115 let export_entity pp_term si xdir (a, u, b) =
 116    let path = path_of_uri xdir u in
 117    let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
 118    let och = open_out (path ^ obj_ext) in
 119    let out = output_string och in
 120    xml out "1.0" "UTF-8"; doctype out root system;
 121    let a = E.Name (U.name_of_uri u, true) :: a in
 122    let attrs = [uri u; name a; mark a; meta a] in
 123    let contents = match b with
 124       | E.Abst w -> tag "ABST" attrs ~contents:(pp_term w)
 125       | E.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
 126       | E.Void   -> assert false
 127    in
 128    let opts = if si then "si" else "" in
 129    let shp = H.string_of_graph () in
 130    let attrs = ["hierarchy", shp; "options", opts] in
 131    tag root attrs ~contents out 0;
 132    close_out och