]> matita.cs.unibo.it Git - helm.git/blob - helm/software/helena/src/xml/xmlLibrary.ml
new intermediate language complete_rg,
[helm.git] / 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 uri u =
96    "uri", U.string_of_uri u
97
98 let name a =
99    let map f i n r s =
100       let n = if r then n else "-" ^ n in 
101       let spc = if i then "" else " " in
102       f (s ^ n ^ spc)
103    in
104    let f s = "name", s in
105    E.names f map a ""
106
107 let apix a =
108    let err () = "age", "" in
109    let f i = "age", string_of_int i in
110    E.apix err f a
111
112 let mark a =
113    let err () = "mark", "" in
114    let f i = "mark", string_of_int i in
115    E.mark err f a
116
117 let level n =
118    "level", N.to_string n
119
120 let meta a =
121    let map = function
122       | E.Main     -> "Main"
123       | E.InProp   -> "InProp"
124       | E.Progress -> "Progress"
125       | E.Private  -> "Private"
126    in
127    let err () = "meta", "" in
128    let f ms = "meta", String.concat " " (List.rev_map map ms) in
129    E.meta err f a
130
131 let arity l =
132    "arity", string_of_int (List.length l)
133
134 (* TODO: the string tx must be quoted *)
135 let info a =
136    let err () = ["lang", ""; "info", ""] in
137    let f lg tx = ["lang", lg; "info", tx] in
138    E.info err f a
139
140 let export_entity pp_term (a, u, b) = 
141    let path = path_of_uri !G.xdir u in
142    let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
143    let och = open_out (path ^ ext) in
144    let out = output_string och in
145    xml out "1.0" "UTF-8"; doctype out obj_root system;
146    let a = E.Name (U.name_of_uri u, true) :: a in
147    let attrs = uri u :: name a :: apix a :: meta a :: info a in 
148    let contents = match b with
149       | E.Abst (n, w) -> tag "GDec" (level n :: attrs) ~contents:(pp_term w) 
150       | E.Abbr v      -> tag "GDef" attrs ~contents:(pp_term v)
151       | E.Void        -> assert false
152    in
153    let opts = if !G.si then "si" else "" in
154    let shp = H.string_of_graph () in
155    let attrs = [xmlns; "hierarchy", shp; "options", opts] in
156    tag obj_root attrs ~contents out 0;
157    close_out och
158
159 let prec_map (i, _) = string_of_int i
160
161 let next_map (_, i) = string_of_int i
162
163 let marks = function
164    | [] -> "mark", ""
165    | l  -> "mark", String.concat " " (List.rev_map string_of_int l)
166
167 let precs = function
168    | [] -> "prec", ""
169    | l  -> "prec", String.concat " " (List.rev_map prec_map l)
170
171 let nexts = function
172    | [] -> "next", ""
173    | l  -> "next", String.concat " " (List.rev_map next_map l)
174
175 let export_csys s = 
176    let path = path_of_uri !G.xdir s.Q.buri in
177    let _ = Sys.command (Printf.sprintf "mkdir -p %s" path) in
178    let name = F.concat path (ccs_name ^ ext) in
179    let och = open_out name in
180    let out = output_string och in
181    xml out "1.0" "UTF-8"; doctype out ccs_root system;
182    let attrs = [xmlns; uri s.Q.buri] in
183    let contents out tab =
184       tag "ToPositive" [arity s.Q.tp; marks s.Q.tp] out tab;
185       tag "ToOne" [arity s.Q.t1; marks s.Q.t1] out tab;
186       tag "ToNext" [arity s.Q.tn; precs s.Q.tn; nexts s.Q.tn] out tab
187    in
188    tag ccs_root attrs ~contents out 0;
189    close_out och