src/common/alpha.cmi: src/common/entity.cmx
src/common/alpha.cmo: src/common/entity.cmx src/common/alpha.cmi
src/common/alpha.cmx: src/common/entity.cmx src/common/alpha.cmi
-src/common/library.cmi: src/common/entity.cmx
-src/common/library.cmo: src/common/hierarchy.cmi src/common/entity.cmx \
- src/lib/cps.cmx src/common/library.cmi
-src/common/library.cmx: src/common/hierarchy.cmx src/common/entity.cmx \
- src/lib/cps.cmx src/common/library.cmi
src/text/txt.cmo:
src/text/txt.cmx:
src/text/txtParser.cmi: src/text/txt.cmx
src/basic_ag/bagUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \
src/basic_ag/bagType.cmx src/basic_ag/bagEnvironment.cmx \
src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi
+src/complete_rg/crg.cmo: src/common/entity.cmx
+src/complete_rg/crg.cmx: src/common/entity.cmx
+src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx
+src/complete_rg/crgOutput.cmo: src/common/hierarchy.cmi src/common/entity.cmx \
+ src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgOutput.cmi
+src/complete_rg/crgOutput.cmx: src/common/hierarchy.cmx src/common/entity.cmx \
+ src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgOutput.cmi
+src/complete_rg/crgTxt.cmi: src/text/txt.cmx src/complete_rg/crg.cmx
+src/complete_rg/crgTxt.cmo: src/text/txtTxt.cmi src/text/txt.cmx \
+ src/common/options.cmx src/common/hierarchy.cmi src/common/entity.cmx \
+ src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgTxt.cmi
+src/complete_rg/crgTxt.cmx: src/text/txtTxt.cmx src/text/txt.cmx \
+ src/common/options.cmx src/common/hierarchy.cmx src/common/entity.cmx \
+ src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgTxt.cmi
+src/complete_rg/crgAut.cmi: src/complete_rg/crg.cmx src/automath/aut.cmx
+src/complete_rg/crgAut.cmo: src/common/options.cmx src/common/entity.cmx \
+ src/complete_rg/crg.cmx src/lib/cps.cmx src/automath/aut.cmx \
+ src/complete_rg/crgAut.cmi
+src/complete_rg/crgAut.cmx: src/common/options.cmx src/common/entity.cmx \
+ src/complete_rg/crg.cmx src/lib/cps.cmx src/automath/aut.cmx \
+ src/complete_rg/crgAut.cmi
+src/xml/xmlLibrary.cmi: src/common/entity.cmx
+src/xml/xmlLibrary.cmo: src/common/hierarchy.cmi src/common/entity.cmx \
+ src/lib/cps.cmx src/xml/xmlLibrary.cmi
+src/xml/xmlLibrary.cmx: src/common/hierarchy.cmx src/common/entity.cmx \
+ src/lib/cps.cmx src/xml/xmlLibrary.cmi
+src/xml/xmlCrg.cmi: src/xml/xmlLibrary.cmi src/complete_rg/crg.cmx
+src/xml/xmlCrg.cmo: src/xml/xmlLibrary.cmi src/common/hierarchy.cmi \
+ src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+ src/common/alpha.cmi src/xml/xmlCrg.cmi
+src/xml/xmlCrg.cmx: src/xml/xmlLibrary.cmx src/common/hierarchy.cmx \
+ src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+ src/common/alpha.cmx src/xml/xmlCrg.cmi
src/basic_rg/brg.cmo: src/common/entity.cmx
src/basic_rg/brg.cmx: src/common/entity.cmx
-src/basic_rg/brgOutput.cmi: src/lib/log.cmi src/common/library.cmi \
+src/basic_rg/brgCrg.cmi: src/complete_rg/crg.cmx src/basic_rg/brg.cmx
+src/basic_rg/brgCrg.cmo: src/common/marks.cmx src/common/entity.cmx \
+ src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
+ src/basic_rg/brgCrg.cmi
+src/basic_rg/brgCrg.cmx: src/common/marks.cmx src/common/entity.cmx \
+ src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
+ src/basic_rg/brgCrg.cmi
+src/basic_rg/brgOutput.cmi: src/xml/xmlLibrary.cmi src/lib/log.cmi \
src/basic_rg/brg.cmx
-src/basic_rg/brgOutput.cmo: src/common/options.cmx src/lib/log.cmi \
- src/common/library.cmi src/common/hierarchy.cmi src/common/entity.cmx \
+src/basic_rg/brgOutput.cmo: src/xml/xmlLibrary.cmi src/common/options.cmx \
+ src/lib/log.cmi src/common/hierarchy.cmi src/common/entity.cmx \
src/lib/cps.cmx src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmi
-src/basic_rg/brgOutput.cmx: src/common/options.cmx src/lib/log.cmx \
- src/common/library.cmx src/common/hierarchy.cmx src/common/entity.cmx \
+src/basic_rg/brgOutput.cmx: src/xml/xmlLibrary.cmx src/common/options.cmx \
+ src/lib/log.cmx src/common/hierarchy.cmx src/common/entity.cmx \
src/lib/cps.cmx src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmi
src/basic_rg/brgEnvironment.cmi: src/basic_rg/brg.cmx
src/basic_rg/brgEnvironment.cmo: src/common/entity.cmx src/basic_rg/brg.cmx \
src/basic_rg/brgType.cmx src/basic_rg/brgReduction.cmx \
src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \
src/basic_rg/brgUntrusted.cmi
-src/complete_rg/crg.cmo: src/common/entity.cmx
-src/complete_rg/crg.cmx: src/common/entity.cmx
-src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx
-src/complete_rg/crgOutput.cmo: src/common/hierarchy.cmi src/common/entity.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgOutput.cmi
-src/complete_rg/crgOutput.cmx: src/common/hierarchy.cmx src/common/entity.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgOutput.cmi
-src/complete_rg/crgXml.cmi: src/common/library.cmi src/complete_rg/crg.cmx
-src/complete_rg/crgXml.cmo: src/common/library.cmi src/common/hierarchy.cmi \
- src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
- src/common/alpha.cmi src/complete_rg/crgXml.cmi
-src/complete_rg/crgXml.cmx: src/common/library.cmx src/common/hierarchy.cmx \
- src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
- src/common/alpha.cmx src/complete_rg/crgXml.cmi
-src/complete_rg/crgTxt.cmi: src/text/txt.cmx src/complete_rg/crg.cmx
-src/complete_rg/crgTxt.cmo: src/text/txtTxt.cmi src/text/txt.cmx \
- src/common/options.cmx src/common/hierarchy.cmi src/common/entity.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgTxt.cmi
-src/complete_rg/crgTxt.cmx: src/text/txtTxt.cmx src/text/txt.cmx \
- src/common/options.cmx src/common/hierarchy.cmx src/common/entity.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgTxt.cmi
-src/complete_rg/crgAut.cmi: src/complete_rg/crg.cmx src/automath/aut.cmx
-src/complete_rg/crgAut.cmo: src/common/options.cmx src/common/entity.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/automath/aut.cmx \
- src/complete_rg/crgAut.cmi
-src/complete_rg/crgAut.cmx: src/common/options.cmx src/common/entity.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/automath/aut.cmx \
- src/complete_rg/crgAut.cmi
-src/complete_rg/crgBrg.cmi: src/complete_rg/crg.cmx src/basic_rg/brg.cmx
-src/complete_rg/crgBrg.cmo: src/common/marks.cmx src/common/entity.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
- src/complete_rg/crgBrg.cmi
-src/complete_rg/crgBrg.cmx: src/common/marks.cmx src/common/entity.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
- src/complete_rg/crgBrg.cmi
src/toplevel/meta.cmo: src/common/entity.cmx
src/toplevel/meta.cmx: src/common/entity.cmx
src/toplevel/metaOutput.cmi: src/toplevel/meta.cmx
src/lib/cps.cmx src/basic_rg/brg.cmx src/toplevel/metaBrg.cmi
src/toplevel/metaBrg.cmx: src/toplevel/meta.cmx src/common/entity.cmx \
src/lib/cps.cmx src/basic_rg/brg.cmx src/toplevel/metaBrg.cmi
-src/toplevel/top.cmo: src/text/txtParser.cmi src/text/txtLexer.cmx \
- src/text/txt.cmx src/lib/time.cmx src/common/output.cmi \
- src/common/options.cmx src/toplevel/metaOutput.cmi \
- src/toplevel/metaLibrary.cmi src/toplevel/metaBrg.cmi \
- src/toplevel/metaBag.cmi src/toplevel/metaAut.cmi src/toplevel/meta.cmx \
- src/lib/log.cmi src/common/library.cmi src/common/hierarchy.cmi \
- src/common/entity.cmx src/complete_rg/crgXml.cmi \
- src/complete_rg/crgTxt.cmi src/complete_rg/crgBrg.cmi \
+src/toplevel/top.cmo: src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \
+ src/text/txtParser.cmi src/text/txtLexer.cmx src/text/txt.cmx \
+ src/lib/time.cmx src/common/output.cmi src/common/options.cmx \
+ src/toplevel/metaOutput.cmi src/toplevel/metaLibrary.cmi \
+ src/toplevel/metaBrg.cmi src/toplevel/metaBag.cmi \
+ src/toplevel/metaAut.cmi src/toplevel/meta.cmx src/lib/log.cmi \
+ src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crgTxt.cmi \
src/complete_rg/crgAut.cmi src/complete_rg/crg.cmx src/lib/cps.cmx \
src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \
- src/basic_rg/brgOutput.cmi src/basic_rg/brg.cmx \
+ src/basic_rg/brgOutput.cmi src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \
src/basic_ag/bagUntrusted.cmi src/basic_ag/bagType.cmi \
src/basic_ag/bagOutput.cmi src/basic_ag/bag.cmx \
src/automath/autProcess.cmi src/automath/autParser.cmi \
src/automath/autOutput.cmi src/automath/autLexer.cmx src/automath/aut.cmx
-src/toplevel/top.cmx: src/text/txtParser.cmx src/text/txtLexer.cmx \
- src/text/txt.cmx src/lib/time.cmx src/common/output.cmx \
- src/common/options.cmx src/toplevel/metaOutput.cmx \
- src/toplevel/metaLibrary.cmx src/toplevel/metaBrg.cmx \
- src/toplevel/metaBag.cmx src/toplevel/metaAut.cmx src/toplevel/meta.cmx \
- src/lib/log.cmx src/common/library.cmx src/common/hierarchy.cmx \
- src/common/entity.cmx src/complete_rg/crgXml.cmx \
- src/complete_rg/crgTxt.cmx src/complete_rg/crgBrg.cmx \
+src/toplevel/top.cmx: src/xml/xmlLibrary.cmx src/xml/xmlCrg.cmx \
+ src/text/txtParser.cmx src/text/txtLexer.cmx src/text/txt.cmx \
+ src/lib/time.cmx src/common/output.cmx src/common/options.cmx \
+ src/toplevel/metaOutput.cmx src/toplevel/metaLibrary.cmx \
+ src/toplevel/metaBrg.cmx src/toplevel/metaBag.cmx \
+ src/toplevel/metaAut.cmx src/toplevel/meta.cmx src/lib/log.cmx \
+ src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crgTxt.cmx \
src/complete_rg/crgAut.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \
- src/basic_rg/brgOutput.cmx src/basic_rg/brg.cmx \
+ src/basic_rg/brgOutput.cmx src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \
src/basic_ag/bagUntrusted.cmx src/basic_ag/bagType.cmx \
src/basic_ag/bagOutput.cmx src/basic_ag/bag.cmx \
src/automath/autProcess.cmx src/automath/autParser.cmx \
module L = Log
module O = Options
module Y = Entity
-module X = Library
+module X = XmlLibrary
module H = Hierarchy
module B = Brg
val specs: (Brg.lenv, Brg.term) Log.specs
-val export_term: Brg.term -> Library.pp
+val export_term: Brg.term -> XmlLibrary.pp
(*
val export_term: Format.formatter -> Brg.term -> unit
*)
-options hierarchy output entity marks alpha library
+options hierarchy output entity marks alpha
module H = Hierarchy
module Op = Output
module Y = Entity
-module X = Library
+module XL = XmlLibrary
+module XCrg = XmlCrg
module AL = AutLexer
module AP = AutProcess
module AO = AutOutput
module MA = MetaAut
module MO = MetaOutput
module ML = MetaLibrary
-module DX = CrgXml
-module DBrg = CrgBrg
module MBrg = MetaBrg
+module BrgC = BrgCrg
module BrgO = BrgOutput
module BrgR = BrgReduction
module BrgU = BrgUntrusted
let xlate_entity entity = match !kernel, entity with
| Brg, CrgEntity e ->
- let f e = (BrgEntity e) in Y.xlate f DBrg.brg_of_crg e
+ let f e = (BrgEntity e) in Y.xlate f BrgC.brg_of_crg e
| Brg, MetaEntity e ->
let f e = (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e
| Bag, MetaEntity e ->
| _ -> st
let export_entity si xdir moch = function
- | CrgEntity e -> X.export_entity DX.export_term si xdir e
- | BrgEntity e -> X.export_entity BrgO.export_term si xdir e
+ | CrgEntity e -> XL.export_entity XCrg.export_term si xdir e
+ | BrgEntity e -> XL.export_entity BrgO.export_term si xdir e
| MetaEntity e ->
begin match moch with
| None -> ()
--- /dev/null
+xmlLibrary xmlCrg
+++ /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 U = NUri
-module C = Cps
-module H = Hierarchy
-module Y = Entity
-module A = Alpha
-module X = Library
-module D = Crg
-
-(* internal functions *******************************************************)
-
-let rec list_iter map l out tab = match l with
- | [] -> ()
- | hd :: tl -> map hd out tab; list_iter map tl out tab
-
-let list_rev_iter map e ns l out tab =
- let rec aux err f e = function
- | [], [] -> f e
- | n :: ns, hd :: tl ->
- let f e =
-(*
- pp_lenv print_string e; print_string " |- ";
- pp_term print_string hd; print_newline ();
-*)
- map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ())
- in
- aux err f e (ns, tl)
- | _ -> err ()
- in
- ignore (aux C.err C.start e (ns, l))
-
-let lenv_iter map1 map2 l out tab =
- let rec aux f = function
- | D.ESort -> f ()
- | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
- | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
- in
- aux C.start l
-
-let rec exp_term e t out tab = match t with
- | D.TSort (a, l) ->
- let a =
- let err _ = a in
- let f s = Y.Name (s, true) :: a in
- H.string_of_sort err f l
- in
- let attrs = [X.position l; X.name a] in
- X.tag X.sort attrs out tab
- | D.TLRef (a, i, j) ->
- let a =
- let err _ = a in
- let f n r = Y.Name (n, r) :: a in
- D.get_name err f i j e
- in
- let attrs = [X.position i; X.offset j; X.name a] in
- X.tag X.lref attrs out tab
- | D.TGRef (a, n) ->
- let a = Y.Name (U.name_of_uri n, true) :: a in
- let attrs = [X.uri n; X.name a] in
- X.tag X.gref attrs out tab
- | D.TCast (a, u, t) ->
- let attrs = [] in
- X.tag X.cast attrs ~contents:(exp_term e u) out tab;
- exp_term e t out tab
- | D.TAppl (a, vs, t) ->
- let attrs = [X.arity (List.length vs)] in
- X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
- exp_term e t out tab
- | D.TProj (a, lenv, t) ->
- let attrs = [] in
- X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
- exp_term (D.push_proj C.start e a lenv) t out tab
- | D.TBind (a, b, t) ->
-(* NOTE: the inner binders are alpha-converted first *)
-(* so undesirable renamings might occur *)
-(* EX: we rename [x][x]x to [x][x_]x_ *)
-(* whereas [x_][x]x would be more desirable *)
- let a = A.alpha (D.names_of_lenv [] e) a in
- exp_bind e a b out tab;
- exp_term (D.push_bind C.start e a b) t out tab
-
-and exp_bind e a b out tab =
- let f a ns = a, ns in
- let a, ns = Y.get_names f a in
- match b with
- | D.Abst ws ->
- let e = D.push_bind C.start e a (D.Abst []) in
- let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
- X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
- | D.Abbr vs ->
- let e = D.push_bind C.start e a (D.Abbr []) in
- let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
- X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
- | D.Void n ->
- let attrs = [X.name a; X.mark a; X.arity n] in
- X.tag X.void attrs out tab
-
-and exp_eproj e a lenv out tab =
- let attrs = [] in
- X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
-
-(* interface functions ******************************************************)
-
-let export_term = exp_term D.empty_lenv
+++ /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_______________________________________________________________ *)
-
-val export_term: Crg.term -> Library.pp
+++ /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 Y = Entity
-
-(* internal functions *******************************************************)
-
-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 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 =
- 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
-
-(* TODO: the string s must be quoted *)
-let meta a =
- let err () = "meta", "" in
- let f s = "meta", s in
- Y.meta err f a
-
-let export_entity pp_term si xdir (a, u, b) =
- let path = path_of_uri xdir u in
- let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.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; meta 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)
- | Y.Void -> assert false
- in
- let opts = if si then "si" else "" in
- let shp = H.string_of_graph () in
- let attrs = ["hierarchy", shp; "options", opts] in
- tag root attrs ~contents out 0;
- close_out och
+++ /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_______________________________________________________________ *)
-
-type och = string -> unit
-
-type attr = string * string
-
-type pp = och -> int -> unit
-
-val export_entity:
- ('term -> pp) -> bool -> string -> 'term Entity.entity -> unit
-
-val tag: string -> attr list -> ?contents:pp -> pp
-
-val sort: string
-
-val lref: string
-
-val gref: string
-
-val cast: string
-
-val appl: string
-
-val proj: string
-
-val abst: string
-
-val abbr: string
-
-val void: string
-
-val position: int -> attr
-
-val offset: int -> attr
-
-val uri: Entity.uri -> attr
-
-val arity: int -> attr
-
-val name: Entity.attrs -> attr
-
-val mark: Entity.attrs -> attr
-
-val meta: Entity.attrs -> attr
--- /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 U = NUri
+module C = Cps
+module H = Hierarchy
+module Y = Entity
+module A = Alpha
+module X = XmlLibrary
+module D = Crg
+
+(* internal functions *******************************************************)
+
+let rec list_iter map l out tab = match l with
+ | [] -> ()
+ | hd :: tl -> map hd out tab; list_iter map tl out tab
+
+let list_rev_iter map e ns l out tab =
+ let rec aux err f e = function
+ | [], [] -> f e
+ | n :: ns, hd :: tl ->
+ let f e =
+(*
+ pp_lenv print_string e; print_string " |- ";
+ pp_term print_string hd; print_newline ();
+*)
+ map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ())
+ in
+ aux err f e (ns, tl)
+ | _ -> err ()
+ in
+ ignore (aux C.err C.start e (ns, l))
+
+let lenv_iter map1 map2 l out tab =
+ let rec aux f = function
+ | D.ESort -> f ()
+ | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
+ | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
+ in
+ aux C.start l
+
+let rec exp_term e t out tab = match t with
+ | D.TSort (a, l) ->
+ let a =
+ let err _ = a in
+ let f s = Y.Name (s, true) :: a in
+ H.string_of_sort err f l
+ in
+ let attrs = [X.position l; X.name a] in
+ X.tag X.sort attrs out tab
+ | D.TLRef (a, i, j) ->
+ let a =
+ let err _ = a in
+ let f n r = Y.Name (n, r) :: a in
+ D.get_name err f i j e
+ in
+ let attrs = [X.position i; X.offset j; X.name a] in
+ X.tag X.lref attrs out tab
+ | D.TGRef (a, n) ->
+ let a = Y.Name (U.name_of_uri n, true) :: a in
+ let attrs = [X.uri n; X.name a] in
+ X.tag X.gref attrs out tab
+ | D.TCast (a, u, t) ->
+ let attrs = [] in
+ X.tag X.cast attrs ~contents:(exp_term e u) out tab;
+ exp_term e t out tab
+ | D.TAppl (a, vs, t) ->
+ let attrs = [X.arity (List.length vs)] in
+ X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
+ exp_term e t out tab
+ | D.TProj (a, lenv, t) ->
+ let attrs = [] in
+ X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
+ exp_term (D.push_proj C.start e a lenv) t out tab
+ | D.TBind (a, b, t) ->
+(* NOTE: the inner binders are alpha-converted first *)
+(* so undesirable renamings might occur *)
+(* EX: we rename [x][x]x to [x][x_]x_ *)
+(* whereas [x_][x]x would be more desirable *)
+ let a = A.alpha (D.names_of_lenv [] e) a in
+ exp_bind e a b out tab;
+ exp_term (D.push_bind C.start e a b) t out tab
+
+and exp_bind e a b out tab =
+ let f a ns = a, ns in
+ let a, ns = Y.get_names f a in
+ match b with
+ | D.Abst ws ->
+ let e = D.push_bind C.start e a (D.Abst []) in
+ let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
+ X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
+ | D.Abbr vs ->
+ let e = D.push_bind C.start e a (D.Abbr []) in
+ let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
+ X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
+ | D.Void n ->
+ let attrs = [X.name a; X.mark a; X.arity n] in
+ X.tag X.void attrs out tab
+
+and exp_eproj e a lenv out tab =
+ let attrs = [] in
+ X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
+
+(* interface functions ******************************************************)
+
+let export_term = exp_term D.empty_lenv
--- /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_______________________________________________________________ *)
+
+val export_term: Crg.term -> XmlLibrary.pp
--- /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 Y = Entity
+
+(* internal functions *******************************************************)
+
+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 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 =
+ 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
+
+(* TODO: the string s must be quoted *)
+let meta a =
+ let err () = "meta", "" in
+ let f s = "meta", s in
+ Y.meta err f a
+
+let export_entity pp_term si xdir (a, u, b) =
+ let path = path_of_uri xdir u in
+ let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.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; meta 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)
+ | Y.Void -> assert false
+ in
+ let opts = if si then "si" else "" in
+ let shp = H.string_of_graph () in
+ let attrs = ["hierarchy", shp; "options", opts] in
+ tag root attrs ~contents out 0;
+ close_out och
--- /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_______________________________________________________________ *)
+
+type och = string -> unit
+
+type attr = string * string
+
+type pp = och -> int -> unit
+
+val export_entity:
+ ('term -> pp) -> bool -> string -> 'term Entity.entity -> unit
+
+val tag: string -> attr list -> ?contents:pp -> pp
+
+val sort: string
+
+val lref: string
+
+val gref: string
+
+val cast: string
+
+val appl: string
+
+val proj: string
+
+val abst: string
+
+val abbr: string
+
+val void: string
+
+val position: int -> attr
+
+val offset: int -> attr
+
+val uri: Entity.uri -> attr
+
+val arity: int -> attr
+
+val name: Entity.attrs -> attr
+
+val mark: Entity.attrs -> attr
+
+val meta: Entity.attrs -> attr
projects / helm.git / commitdiff