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 F = Filename
  13 module U = NUri
  14 module C = Cps
  15 module H = Hierarchy
  16 module G = Options
  17 module E = Entity
  18 module N = Level
  19 module Q = Ccs
  20
  21 (* internal functions *******************************************************)
  22
  23 let base = "xml"
  24
  25 let ext = ".xml"
  26
  27 let obj_root = "ENTITY"
  28
  29 let ccs_name = "ccs.ldc"
  30
  31 let ccs_root = "CCS"
  32
  33 let home = "http://lambdadelta.info/"
  34
  35 let system = F.concat (F.concat home base) "ld.dtd"
  36
  37 let xmlns = "xmlns", home
  38
  39 let path_of_uri xdir uri =
  40    let base = F.concat xdir base in
  41    F.concat base (Str.string_after (U.string_of_uri uri) 3)
  42
  43 (* interface functions ******************************************************)
  44
  45 type och = string -> unit
  46
  47 type attr = string * string
  48
  49 type pp = och -> int -> unit
  50
  51 let attribute out (name, contents) =
  52    if contents <> "" then begin
  53       out " "; out name; out "=\""; out contents; out "\""
  54    end
  55
  56 let xml out version encoding =
  57    out "<?xml";
  58       attribute out ("version", version);
  59       attribute out ("encoding", encoding);
  60    out "?>\n\n"
  61
  62 let doctype out root system =
  63    out "<!DOCTYPE "; out root; out " SYSTEM \""; out system; out "\">\n\n"
  64
  65 let tag tag attrs ?contents out indent =
  66    let spc = String.make indent ' ' in
  67    out spc; out "<"; out tag; List.iter (attribute out) attrs;
  68    match contents with
  69       | None      -> out "/>\n"
  70       | Some cont ->
  71          out ">\n"; cont out (indent + 3); out spc;
  72          out "</"; out tag; out ">\n"
  73
  74 let sort = "Sort"
  75
  76 let lref = "LRef"
  77
  78 let gref = "GRef"
  79
  80 let cast = "Cast"
  81
  82 let appl = "Appl"
  83
  84 let proj = "Proj"
  85
  86 let abst = "Abst"
  87
  88 let abbr = "Abbr"
  89
  90 let void = "Void"
  91
  92 let position i =
  93    "position", string_of_int i
  94
  95 let offset j =
  96    let contents = if j > 0 then string_of_int j else "" in
  97    "offset", contents
  98
  99 let uri u =
 100    "uri", U.string_of_uri u
 101
 102 let arity ?n l =
 103    let n = match n with
 104       | None   -> List.length l
 105       | Some n -> n
 106    in
 107    let contents = if n > 1 then string_of_int n else "" in
 108    "arity", contents
 109
 110 let name a =
 111    let map f i n r s =
 112       let n = if r then n else "-" ^ n in
 113       let spc = if i then "" else " " in
 114       f (s ^ n ^ spc)
 115    in
 116    let f s = "name", s in
 117    E.names f map a ""
 118
 119 let apix a =
 120    let err () = "age", "" in
 121    let f i = "age", string_of_int i in
 122    E.apix err f a
 123
 124 let mark a =
 125    let err () = "mark", "" in
 126    let f i = "mark", string_of_int i in
 127    E.mark err f a
 128
 129 let level n =
 130    "level", N.to_string n
 131
 132 let meta a =
 133    let map = function
 134       | E.Main     -> "Main"
 135       | E.InProp   -> "InProp"
 136       | E.Progress -> "Progress"
 137       | E.Private  -> "Private"
 138    in
 139    let err () = "meta", "" in
 140    let f ms = "meta", String.concat " " (List.rev_map map ms) in
 141    E.meta err f a
 142
 143 (* TODO: the string tx must be quoted *)
 144 let info a =
 145    let err () = ["lang", ""; "info", ""] in
 146    let f lg tx = ["lang", lg; "info", tx] in
 147    E.info err f a
 148
 149 let export_entity pp_term (a, u, b) =
 150    let path = path_of_uri !G.xdir u in
 151    let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
 152    let och = open_out (path ^ ext) in
 153    let out = output_string och in
 154    xml out "1.0" "UTF-8"; doctype out obj_root system;
 155    let a = E.Name (U.name_of_uri u, true) :: a in
 156    let attrs = uri u :: name a :: apix a :: meta a :: info a in
 157    let contents = match b with
 158       | E.Abst (n, w) -> tag "GDec" (level n :: attrs) ~contents:(pp_term w)
 159       | E.Abbr v      -> tag "GDef" attrs ~contents:(pp_term v)
 160       | E.Void        -> assert false
 161    in
 162    let opts = if !G.si then "si" else "" in
 163    let shp = H.string_of_graph () in
 164    let attrs = [xmlns; "hierarchy", shp; "options", opts] in
 165    tag obj_root attrs ~contents out 0;
 166    close_out och
 167
 168 let prec_map (i, _) = string_of_int i
 169
 170 let next_map (_, i) = string_of_int i
 171
 172 let marks = function
 173    | [] -> "mark", ""
 174    | l  -> "mark", String.concat " " (List.rev_map string_of_int l)
 175
 176 let precs = function
 177    | [] -> "prec", ""
 178    | l  -> "prec", String.concat " " (List.rev_map prec_map l)
 179
 180 let nexts = function
 181    | [] -> "next", ""
 182    | l  -> "next", String.concat " " (List.rev_map next_map l)
 183
 184 let export_csys s =
 185    let path = path_of_uri !G.xdir s.Q.buri in
 186    let _ = Sys.command (Printf.sprintf "mkdir -p %s" path) in
 187    let name = F.concat path (ccs_name ^ ext) in
 188    let och = open_out name in
 189    let out = output_string och in
 190    xml out "1.0" "UTF-8"; doctype out ccs_root system;
 191    let attrs = [xmlns; uri s.Q.buri] in
 192    let contents out tab =
 193       tag "ToPositive" [arity s.Q.tp; marks s.Q.tp] out tab;
 194       tag "ToOne" [arity s.Q.t1; marks s.Q.t1] out tab;
 195       tag "ToNext" [arity s.Q.tn; precs s.Q.tn; nexts s.Q.tn] out tab
 196    in
 197    tag ccs_root attrs ~contents out 0;
 198    close_out och