+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-module F = Filename
-module U = NUri
-module C = Cps
-module H = Hierarchy
-module G = Options
-module E = Entity
-module N = Level
-module Q = Ccs
-
-(* internal functions *******************************************************)
-
-let base = "xml"
-
-let ext = ".xml"
-
-let obj_root = "ENTITY"
-
-let ccs_name = "ccs.ldc"
-
-let ccs_root = "CCS"
-
-let home = "http://lambda-delta.info"
-
-let system = home ^ "/" ^ base ^ "/ld.dtd"
-
-let xmlns = "xmlns", home
-
-let path_of_uri xdir uri =
- let base = F.concat xdir base in
- F.concat base (Str.string_after (U.string_of_uri uri) 3)
-
-(* interface functions ******************************************************)
-
-type och = string -> unit
-
-type attr = string * string
-
-type pp = och -> int -> unit
-
-let attribute out (name, contents) =
- if contents <> "" then begin
- out " "; out name; out "=\""; out contents; out "\""
- end
-
-let xml out version encoding =
- out "<?xml";
- attribute out ("version", version);
- attribute out ("encoding", encoding);
- out "?>\n\n"
-
-let doctype out root system =
- out "<!DOCTYPE "; out root; out " SYSTEM \""; out system; out "\">\n\n"
-
-let tag tag attrs ?contents out indent =
- let spc = String.make indent ' ' in
- out spc; out "<"; out tag; List.iter (attribute out) attrs;
- match contents with
- | None -> out "/>\n"
- | Some cont ->
- out ">\n"; cont out (indent + 3); out spc;
- out "</"; out tag; out ">\n"
-
-let sort = "Sort"
-
-let lref = "LRef"
-
-let gref = "GRef"
-
-let cast = "Cast"
-
-let appl = "Appl"
-
-let proj = "Proj"
-
-let abst = "Abst"
-
-let abbr = "Abbr"
-
-let void = "Void"
-
-let position i =
- "position", string_of_int i
-
-let offset j =
- let contents = if j > 0 then string_of_int j else "" in
- "offset", contents
-
-let uri u =
- "uri", U.string_of_uri u
-
-let arity ?n l =
- let n = match n with
- | None -> List.length l
- | Some n -> n
- in
- let contents = if n > 1 then string_of_int n else "" in
- "arity", contents
-
-let name a =
- let map f i n r s =
- let n = if r then n else "-" ^ n in
- let spc = if i then "" else " " in
- f (s ^ n ^ spc)
- in
- let f s = "name", s in
- E.names f map a ""
-
-let mark a =
- let err () = "mark", "" in
- let f i = "mark", string_of_int i in
- E.mark err f a
-
-let level n =
- "level", N.to_string n
-
-let meta a =
- let map = function
- | E.Main -> "Main"
- | E.InProp -> "InProp"
- | E.Progress -> "Progress"
- | E.Private -> "Private"
- in
- let err () = "meta", "" in
- let f ms = "meta", String.concat " " (List.rev_map map ms) in
- E.meta err f a
-
-(* TODO: the string tx must be quoted *)
-let info a =
- let err () = ["lang", ""; "info", ""] in
- let f lg tx = ["lang", lg; "info", tx] in
- E.info err f a
-
-let export_entity pp_term (a, u, b) =
- let path = path_of_uri !G.xdir u in
- let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
- let och = open_out (path ^ ext) in
- let out = output_string och in
- xml out "1.0" "UTF-8"; doctype out obj_root system;
- let a = E.Name (U.name_of_uri u, true) :: a in
- let attrs = uri u :: name a :: mark a :: meta a :: info a in
- let contents = match b with
- | E.Abst (n, w) -> tag "ABST" (level n :: attrs) ~contents:(pp_term w)
- | E.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
- | E.Void -> assert false
- in
- let opts = if !G.si then "si" else "" in
- let shp = H.string_of_graph () in
- let attrs = [xmlns; "hierarchy", shp; "options", opts] in
- tag obj_root attrs ~contents out 0;
- close_out och
-
-let prec_map (i, _) = string_of_int i
-
-let next_map (_, i) = string_of_int i
-
-let marks = function
- | [] -> "mark", ""
- | l -> "mark", String.concat " " (List.rev_map string_of_int l)
-
-let precs = function
- | [] -> "prec", ""
- | l -> "prec", String.concat " " (List.rev_map prec_map l)
-
-let nexts = function
- | [] -> "next", ""
- | l -> "next", String.concat " " (List.rev_map next_map l)
-
-let export_csys s =
- let path = path_of_uri !G.xdir s.Q.uri in
- let _ = Sys.command (Printf.sprintf "mkdir -p %s" path) in
- let name = F.concat path (ccs_name ^ ext) in
- let och = open_out name in
- let out = output_string och in
- xml out "1.0" "UTF-8"; doctype out ccs_root system;
- let attrs = [xmlns; uri s.Q.uri] in
- let contents out tab =
- tag "ToPositive" [arity s.Q.tp; marks s.Q.tp] out tab;
- tag "ToOne" [arity s.Q.t1; marks s.Q.t1] out tab;
- tag "ToNext" [arity s.Q.tn; precs s.Q.tn; nexts s.Q.tn] out tab
- in
- tag ccs_root attrs ~contents out 0;
- close_out och
projects / helm.git / blobdiff