From: Ferruccio Guidi Date: Fri, 6 Aug 2010 12:13:49 +0000 (+0000) Subject: the refactoring continues ... X-Git-Tag: make_still_working~2847 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bb2a0b22a2c38b59ca664b550f34e5e40e6f04c7;p=helm.git the refactoring continues ... --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index c6e6ac189..bc920f171 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -24,11 +24,6 @@ src/common/marks.cmx: src/common/entity.cmx 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 @@ -110,15 +105,55 @@ src/basic_ag/bagUntrusted.cmo: src/lib/log.cmi src/common/entity.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 \ @@ -162,41 +197,6 @@ src/basic_rg/brgUntrusted.cmx: src/lib/log.cmx src/common/entity.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 @@ -226,32 +226,30 @@ src/toplevel/metaBrg.cmo: src/toplevel/meta.cmx src/common/entity.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 \ diff --git a/helm/software/lambda-delta/src/basic_rg/brgOutput.ml b/helm/software/lambda-delta/src/basic_rg/brgOutput.ml index 186349a1c..c70bbfec7 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgOutput.ml @@ -16,7 +16,7 @@ module U = NUri module L = Log module O = Options module Y = Entity -module X = Library +module X = XmlLibrary module H = Hierarchy module B = Brg diff --git a/helm/software/lambda-delta/src/basic_rg/brgOutput.mli b/helm/software/lambda-delta/src/basic_rg/brgOutput.mli index 772f43cad..556439a99 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgOutput.mli +++ b/helm/software/lambda-delta/src/basic_rg/brgOutput.mli @@ -19,7 +19,7 @@ val print_counters: (unit -> 'a) -> counters -> 'a 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 *) diff --git a/helm/software/lambda-delta/src/common/Make b/helm/software/lambda-delta/src/common/Make index de13dd4c9..09f15792b 100644 --- a/helm/software/lambda-delta/src/common/Make +++ b/helm/software/lambda-delta/src/common/Make @@ -1 +1 @@ -options hierarchy output entity marks alpha library +options hierarchy output entity marks alpha diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml index 40fcda5e1..d45bcf98e 100644 --- a/helm/software/lambda-delta/src/toplevel/top.ml +++ b/helm/software/lambda-delta/src/toplevel/top.ml @@ -19,7 +19,8 @@ module O = Options 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 @@ -28,9 +29,8 @@ module DA = CrgAut 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 @@ -95,7 +95,7 @@ let print_counters st = match !kernel with 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 -> @@ -122,8 +122,8 @@ let count_entity st = function | _ -> 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 -> () diff --git a/helm/software/lambda-delta/src/xml/Make b/helm/software/lambda-delta/src/xml/Make new file mode 100644 index 000000000..3a626cece --- /dev/null +++ b/helm/software/lambda-delta/src/xml/Make @@ -0,0 +1 @@ +xmlLibrary xmlCrg diff --git a/helm/software/lambda-delta/src/xml/XmlCrg.ml b/helm/software/lambda-delta/src/xml/XmlCrg.ml deleted file mode 100644 index 111cfed06..000000000 --- a/helm/software/lambda-delta/src/xml/XmlCrg.ml +++ /dev/null @@ -1,114 +0,0 @@ -(* - ||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 diff --git a/helm/software/lambda-delta/src/xml/XmlCrg.mli b/helm/software/lambda-delta/src/xml/XmlCrg.mli deleted file mode 100644 index c326a9822..000000000 --- a/helm/software/lambda-delta/src/xml/XmlCrg.mli +++ /dev/null @@ -1,12 +0,0 @@ -(* - ||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 diff --git a/helm/software/lambda-delta/src/xml/XmlLibrary.ml b/helm/software/lambda-delta/src/xml/XmlLibrary.ml deleted file mode 100644 index 8a6801159..000000000 --- a/helm/software/lambda-delta/src/xml/XmlLibrary.ml +++ /dev/null @@ -1,132 +0,0 @@ -(* - ||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 "\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 "\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 diff --git a/helm/software/lambda-delta/src/xml/XmlLibrary.mli b/helm/software/lambda-delta/src/xml/XmlLibrary.mli deleted file mode 100644 index ed3f7bb8f..000000000 --- a/helm/software/lambda-delta/src/xml/XmlLibrary.mli +++ /dev/null @@ -1,53 +0,0 @@ -(* - ||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 diff --git a/helm/software/lambda-delta/src/xml/xmlCrg.ml b/helm/software/lambda-delta/src/xml/xmlCrg.ml new file mode 100644 index 000000000..62f0654bd --- /dev/null +++ b/helm/software/lambda-delta/src/xml/xmlCrg.ml @@ -0,0 +1,114 @@ +(* + ||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 diff --git a/helm/software/lambda-delta/src/xml/xmlCrg.mli b/helm/software/lambda-delta/src/xml/xmlCrg.mli new file mode 100644 index 000000000..7e63c5c4a --- /dev/null +++ b/helm/software/lambda-delta/src/xml/xmlCrg.mli @@ -0,0 +1,12 @@ +(* + ||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 diff --git a/helm/software/lambda-delta/src/xml/xmlLibrary.ml b/helm/software/lambda-delta/src/xml/xmlLibrary.ml new file mode 100644 index 000000000..8a6801159 --- /dev/null +++ b/helm/software/lambda-delta/src/xml/xmlLibrary.ml @@ -0,0 +1,132 @@ +(* + ||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 "\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 "\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 diff --git a/helm/software/lambda-delta/src/xml/xmlLibrary.mli b/helm/software/lambda-delta/src/xml/xmlLibrary.mli new file mode 100644 index 000000000..ed3f7bb8f --- /dev/null +++ b/helm/software/lambda-delta/src/xml/xmlLibrary.mli @@ -0,0 +1,53 @@ +(* + ||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