X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fcommon%2Flibrary.ml;h=ff4c54198832220c4154e44d7a62ef3da1a50318;hb=c69505678c1746083a9a01ec4367cea67d888aa1;hp=8dec0dd5d122614ca10ddfc61c04644b8fa9d61d;hpb=cca5f6b7431b846b7bdcbf813632cb79580d5874;p=helm.git
diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml
index 8dec0dd5d..ff4c54198 100644
--- a/helm/software/lambda-delta/common/library.ml
+++ b/helm/software/lambda-delta/common/library.ml
@@ -9,9 +9,12 @@
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module F = Filename
+module F = Format
+module N = Filename
module U = NUri
+module C = Cps
module H = Hierarchy
+module Y = Entity
(* internal functions *******************************************************)
@@ -19,38 +22,156 @@ let base = "xml"
let obj_ext = ".xml"
+let root = "ENTITY"
+
let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
let path_of_uri uri =
- F.concat base (Str.string_after (U.string_of_uri uri) 3)
+ N.concat base (Str.string_after (U.string_of_uri uri) 3)
let pp_head frm =
- Format.fprintf frm "@,@," "1.0" "UTF-8"
+ F.fprintf frm "@,@," "1.0" "UTF-8"
let pp_doctype frm =
- Format.fprintf frm "@,@," system
+ F.fprintf frm "@,@," system
-let open_entry si g frm =
+let open_entity si g frm =
let opts = if si then "si" else "" in
let f shp =
- Format.fprintf frm "" shp opts
+ F.fprintf frm "" shp opts
in
H.string_of_graph f g
-let close_entry frm =
- Format.fprintf frm ""
+let close_entity frm =
+ F.fprintf frm ""
+
+let name frm a =
+ let f s = function
+ | true -> F.fprintf frm " name=%S" s
+ | false -> F.fprintf frm " name=%S" ("^" ^ s)
+ in
+ Y.name C.start f a
+
+let pp_entity pp_term frm = function
+ | a, u, Y.Abst w ->
+ let str = U.string_of_uri u in
+ let a = Y.Name (U.name_of_uri u, true) :: a in
+ F.fprintf frm "%a" str name a pp_term w
+ | a, u, Y.Abbr v ->
+ let str = U.string_of_uri u in
+ let a = Y.Name (U.name_of_uri u, true) :: a in
+ F.fprintf frm "%a" str name a pp_term v
+
+let pp_boxed pp_term frm entity =
+ F.fprintf frm "@,@[ %a@]@," (pp_entity pp_term) entity
(* interface functions ******************************************************)
-let export_item export_obj si g = function
- | Some obj ->
- let _, uri, bind = obj in
- let path = path_of_uri uri in
- let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
- let och = open_out (path ^ obj_ext) in
- let frm = Format.formatter_of_out_channel och in
- Format.pp_set_margin frm max_int;
- Format.fprintf frm "@[%t%t%t%a%t@]@."
- pp_head pp_doctype (open_entry si g) export_obj obj close_entry;
- close_out och
- | None -> ()
+let old_export_entity pp_term si g entity =
+ let _, uri, _ = entity in
+ let path = path_of_uri uri in
+ let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in
+ let och = open_out (path ^ obj_ext) in
+ let frm = F.formatter_of_out_channel och in
+ F.pp_set_margin frm max_int;
+ F.fprintf frm "@[%t%t%t%a%t@]@."
+ pp_head pp_doctype
+ (open_entity si g) (pp_boxed pp_term) entity close_entity;
+ close_out och
+
+let old_name = name
+
+(****************************************************************************)
+
+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 "\n\n"
+
+let doctype out root 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 =
+ 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
+ Y.names f map a ""
+
+let mark a =
+ let err () = "mark", "" in
+ let f i = "mark", string_of_int i in
+ Y.mark err f a
+
+let export_entity pp_term si g (a, u, b) =
+ let path = path_of_uri u in
+ let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in
+ let och = open_out (path ^ obj_ext) in
+ let out = output_string och in
+ xml out "1.0" "UTF-8"; doctype out root system;
+ let a = Y.Name (U.name_of_uri u, true) :: a in
+ let attrs = [uri u; name a; mark a] in
+ let contents = match b with
+ | Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w)
+ | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
+ in
+ let opts = if si then "si" else "" in
+ let shp = H.string_of_graph C.start g in
+ let attrs = ["hierarchy", shp; "options", opts] in
+ tag root attrs ~contents out 0;
+ close_out och