(*
    ||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 KF = Filename

module U  = NUri
module C  = Cps
module G  = Options
module H  = Hierarchy
module N  = Layer
module E  = Entity

(* internal functions *******************************************************)

let base = "xml"

let ext = ".xml"

let obj_root = "CONSTANT"

let home = "http://lambdadelta.info/"

let system = KF.concat (KF.concat home base) "ld.dtd"

let xmlns = "xmlns", home

let path_of_uri xdir uri =
   let base = KF.concat xdir base in 
   KF.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 x = if x then "Appx" else "Appr"

let proj = "Proj"

let abst = "Abst"

let abbr = "Abbr"

let void = "Void"

let position i =
   "position", string_of_int i

let uri u =
   "uri", U.string_of_uri u

let name a =
   let err () = "name", "" in
   let f n r = "name", if r then n else "-" ^ n in 
   E.name err f a

let apix a =
   "position", string_of_int a.E.n_apix

let layer st n =
   "layer", N.to_string st n

let kind a =
   "position", string_of_int a.E.n_sort

let meta a =
   let map = function
      | E.Main     -> "Main"
      | E.InProp   -> "InProp"
      | E.Progress -> "Progress"
      | E.Private  -> "Private"
   in
   "meta", String.concat " " (List.rev_map map a.E.r_meta)

(* 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 (ra, na, u, b) = 
   let path = path_of_uri !G.xdir u in
   let _ = Sys.command (Printf.sprintf "mkdir -p %s" (KF.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 na = {na with E.n_name = Some (U.name_of_uri u, true)} in
   let attrs = uri u :: name na :: apix na :: meta ra :: info ra in 
   let contents = match b with
      | E.Abst w -> tag "GDec" attrs ~contents:(pp_term w) 
      | E.Abbr v -> tag "GDef" 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