(*
    ||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 system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"

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

(* TODO: the string s must be quoted *)
let meta a =
   let err () = "meta", "" in
   let f s = "meta", s in
   E.meta 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] 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 = ["hierarchy", shp; "options", opts] in
   tag obj_root attrs ~contents out 0;
   close_out och

let marks = function
   | [] -> "mark", ""
   | l  -> "mark", String.concat " " (List.rev_map string_of_int 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 = [uri s.Q.uri] in
   let contents = tag "ToInfinity" [arity s.Q.is; marks s.Q.is] in
   tag ccs_root attrs ~contents out 0;
   close_out och