helm/software/lambda-delta/common/library.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 = Format
  13 module N = Filename
  14 module U = NUri
  15 module C = Cps
  16 module H = Hierarchy
  17 module Y = Entity
  18
  19 (* internal functions *******************************************************)
  20
  21 let base = "xml"
  22
  23 let obj_ext = ".xml"
  24
  25 let root = "ENTITY"
  26
  27 let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
  28
  29 let path_of_uri uri =
  30    N.concat base (Str.string_after (U.string_of_uri uri) 3)
  31
  32 let pp_head frm =
  33    F.fprintf frm "<?xml version=%S encoding=%S?>@,@," "1.0" "UTF-8"
  34
  35 let pp_doctype frm =
  36   F.fprintf frm "<!DOCTYPE ENTITY SYSTEM %S>@,@," system
  37
  38 let open_entity si g frm =
  39    let opts = if si then "si" else "" in
  40    let f shp =
  41       F.fprintf frm "<ENTITY hierarchy=%S options=%S>" shp opts
  42    in
  43    H.string_of_graph f g
  44
  45 let close_entity frm =
  46    F.fprintf frm "</ENTITY>"
  47
  48 let name frm a =
  49    let f s = function
  50       | true  -> F.fprintf frm " name=%S" s
  51       | false -> F.fprintf frm " name=%S" ("^" ^ s)
  52    in
  53    Y.name C.start f a
  54
  55 let pp_entity pp_term frm = function
  56    | a, u, Y.Abst w ->
  57       let str = U.string_of_uri u in
  58       let a = Y.Name (U.name_of_uri u, true) :: a in
  59       F.fprintf frm "<ABST uri=%S%a>%a</ABST>" str name a pp_term w
  60    | a, u, Y.Abbr v ->
  61       let str = U.string_of_uri u in
  62       let a = Y.Name (U.name_of_uri u, true) :: a in
  63       F.fprintf frm "<ABBR uri=%S%a>%a</ABBR>" str name a pp_term v
  64
  65 let pp_boxed pp_term frm entity =
  66    F.fprintf frm "@,@[<v3>   %a@]@," (pp_entity pp_term) entity
  67
  68 (* interface functions ******************************************************)
  69
  70 let old_export_entity pp_term si g entity =
  71    let _, uri, _ = entity in
  72    let path = path_of_uri uri in
  73    let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in
  74    let och = open_out (path ^ obj_ext) in
  75    let frm = F.formatter_of_out_channel och in
  76    F.pp_set_margin frm max_int;
  77    F.fprintf frm "@[<v>%t%t%t%a%t@]@."
  78       pp_head pp_doctype
  79       (open_entity si g) (pp_boxed pp_term) entity close_entity;
  80    close_out och
  81
  82 let old_name = name
  83
  84 (****************************************************************************)
  85
  86 type och = string -> unit
  87
  88 type attr = string * string
  89
  90 type pp = och -> int -> unit
  91
  92 let attribute out (name, contents) =
  93    if contents <> "" then begin
  94       out " "; out name; out "=\""; out contents; out "\""
  95    end
  96
  97 let xml out version encoding =
  98    out "<?xml";
  99       attribute out ("version", version);
 100       attribute out ("encoding", encoding);
 101    out "?>\n\n"
 102
 103 let doctype out root system =
 104    out "<!DOCTYPE "; out root; out " SYSTEM \""; out system; out "\">\n\n"
 105
 106 let tag tag attrs ?contents out indent =
 107    let spc = String.make indent ' ' in
 108    out spc; out "<"; out tag; List.iter (attribute out) attrs;
 109    match contents with
 110       | None      -> out "/>\n"
 111       | Some cont ->
 112          out ">\n"; cont out (indent + 3); out spc;
 113          out "</"; out tag; out ">\n"
 114
 115 let sort = "Sort"
 116
 117 let lref = "LRef"
 118
 119 let gref = "GRef"
 120
 121 let cast = "Cast"
 122
 123 let appl = "Appl"
 124
 125 let proj = "Proj"
 126
 127 let abst = "Abst"
 128
 129 let abbr = "Abbr"
 130
 131 let void = "Void"
 132
 133 let position i =
 134    "position", string_of_int i
 135
 136 let offset j =
 137    let contents = if j > 0 then string_of_int j else "" in
 138    "offset", contents
 139
 140 let uri u =
 141    "uri", U.string_of_uri u
 142
 143 let arity n =
 144    let contents = if n > 1 then string_of_int n else "" in
 145    "arity", contents
 146
 147 let name a =
 148    let map f i n r s =
 149       let n = if r then n else "^" ^ n in
 150       let spc = if i then "" else " " in
 151       f (s ^ n ^ spc)
 152    in
 153    let f s = "name", s in
 154    Y.names f map a ""
 155
 156 let mark a =
 157    let err () = "mark", "" in
 158    let f i = "mark", string_of_int i in
 159    Y.mark err f a
 160
 161 let export_entity pp_term si g (a, u, b) =
 162    let path = path_of_uri u in
 163    let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in
 164    let och = open_out (path ^ obj_ext) in
 165    let out = output_string och in
 166    xml out "1.0" "UTF-8"; doctype out root system;
 167    let a = Y.Name (U.name_of_uri u, true) :: a in
 168    let attrs = [uri u; name a; mark a] in
 169    let contents = match b with
 170       | Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w)
 171       | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
 172    in
 173    let opts = if si then "si" else "" in
 174    let shp = H.string_of_graph C.start g in
 175    let attrs = ["hierarchy", shp; "options", opts] in
 176    tag root attrs ~contents out 0;
 177    close_out och