From: Ferruccio Guidi Date: Thu, 29 Oct 2009 18:15:17 +0000 (+0000) Subject: new xml exportation procedure for basic_rg (10 times faster than previous). the stati... X-Git-Tag: make_still_working~3226 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=51beb717ea0a68ae899e73b09cb67ea90b260b27;p=helm.git new xml exportation procedure for basic_rg (10 times faster than previous). the static html pages were changed accordingly. Old exportation procedure removed --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 5335eac4f..1cf0b734e 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -72,7 +72,7 @@ basic_ag/bagUntrusted.cmx: lib/nUri.cmx lib/log.cmx common/entity.cmx \ basic_ag/bagUntrusted.cmi basic_rg/brg.cmo: common/entity.cmx basic_rg/brg.cmx: common/entity.cmx -basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brg.cmx +basic_rg/brgOutput.cmi: lib/log.cmi common/library.cmi basic_rg/brg.cmx basic_rg/brgOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \ common/library.cmi common/hierarchy.cmi common/entity.cmx lib/cps.cmx \ basic_rg/brg.cmx basic_rg/brgOutput.cmi diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index dacc62f6c..d2edae23b 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -8,9 +8,9 @@ CLEAN = etc/log.txt TAGS = test test-si test-si-fast hal xml-si-drg xml-si-old -XMLS = xml/grundlagen/l/not.ld.xml xml/grundlagen/l/et.ld.xml \ - xml/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ - xml/grundlagen/l/e/pairis1.ld.xml +XMLS = xml/brg/grundlagen/l/not.ld.xml xml/brg/grundlagen/l/et.ld.xml \ + xml/brg/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ + xml/brg/grundlagen/l/e/pairis1.ld.xml include Makefile.common @@ -42,7 +42,6 @@ xml-si-drg: $(MAIN).opt @echo " HELENA -u -x -s 1 $(INPUT)" $(H)./$(MAIN).opt -u -x -s 1 -S 1 $(INPUT) > etc/log.txt - %.ld: BASEURL = --stringparam baseurl $(LDDLURL) %.ld: diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index 7dfb2b937..58a407f04 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -222,44 +222,50 @@ let specs = { (* term xml printing ********************************************************) -let rec exp_term c frm = function +let rec exp_term e t out tab = match t with | B.Sort (a, l) -> let a = let err _ = a in let f s = Y.Name (s, true) :: a in H.get_sort err f l in - F.fprintf frm "" (string_of_int l) X.old_name a + let attrs = [X.position l; X.name a] in + X.tag X.sort attrs out tab | B.LRef (a, i) -> let a = let err _ = a in let f n r = Y.Name (n, r) :: a in let f _ b = attrs_of_binder (Y.name err f) b in - B.get err f c i + B.get err f e i in - F.fprintf frm "" (string_of_int i) X.old_name a - | B.GRef (a, u) -> - let a = Y.Name (U.name_of_uri u, true) :: a in - F.fprintf frm "" (U.string_of_uri u) X.old_name a - | B.Cast (a, w, t) -> - F.fprintf frm "%a@,%a" X.old_name a (exp_boxed c) w (exp_term c) t + let attrs = [X.position i; X.name a] in + X.tag X.lref attrs out tab + | B.GRef (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 + | B.Cast (a, u, t) -> + let attrs = [] in + X.tag X.cast attrs ~contents:(exp_term e u) out tab; + exp_term e t out tab | B.Appl (a, v, t) -> - F.fprintf frm "%a@,%a" X.old_name a (exp_boxed c) v (exp_term c) t - | B.Bind (b, t) -> - let f b cc = F.fprintf frm "%a@,%a" (exp_bind c) b (exp_term cc) t in - let f b = B.push (f b) c b in - rename_bind f c b + let attrs = [] in + X.tag X.appl attrs ~contents:(exp_term e v) out tab; + exp_term e t out tab + | B.Bind (b, t) -> + let b = rename_bind C.start e b in + exp_bind e b out tab; + exp_term (B.push C.start e b) t out tab -and exp_boxed c frm t = - F.fprintf frm "@,@[ %a@]@," (exp_term c) t - -and exp_bind c frm = function +and exp_bind e b out tab = match b with | B.Abst (a, w) -> - F.fprintf frm "%a" X.old_name a (exp_boxed c) w + let attrs = [X.name a; X.mark a] in + X.tag X.abst attrs ~contents:(exp_term e w) out tab | B.Abbr (a, v) -> - F.fprintf frm "%a" X.old_name a (exp_boxed c) v - | B.Void a -> - F.fprintf frm "" X.old_name a + let attrs = [X.name a; X.mark a] in + X.tag X.abbr attrs ~contents:(exp_term e v) out tab + | B.Void a -> + let attrs = [X.name a; X.mark a] in + X.tag X.void attrs out tab -let export_term frm t = - F.fprintf frm "%a" (exp_boxed B.empty_lenv) t +let export_term = exp_term B.empty_lenv diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.mli b/helm/software/lambda-delta/basic_rg/brgOutput.mli index 69700febd..772f43cad 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.mli +++ b/helm/software/lambda-delta/basic_rg/brgOutput.mli @@ -19,4 +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: Format.formatter -> Brg.term -> unit +*) diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml index ff4c54198..25bca63a9 100644 --- a/helm/software/lambda-delta/common/library.ml +++ b/helm/software/lambda-delta/common/library.ml @@ -29,60 +29,8 @@ let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd" let path_of_uri uri = N.concat base (Str.string_after (U.string_of_uri uri) 3) -let pp_head frm = - F.fprintf frm "@,@," "1.0" "UTF-8" - -let pp_doctype frm = - F.fprintf frm "@,@," system - -let open_entity si g frm = - let opts = if si then "si" else "" in - let f shp = - F.fprintf frm "" shp opts - in - H.string_of_graph f g - -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 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 diff --git a/helm/software/lambda-delta/common/library.mli b/helm/software/lambda-delta/common/library.mli index f364af329..3364175bd 100644 --- a/helm/software/lambda-delta/common/library.mli +++ b/helm/software/lambda-delta/common/library.mli @@ -50,9 +50,3 @@ val arity: int -> attr val name: Entity.attrs -> attr val mark: Entity.attrs -> attr - -val old_export_entity: - (Format.formatter -> 'term -> unit) -> - bool -> Hierarchy.graph -> 'term Entity.entity -> unit - -val old_name: Format.formatter -> Entity.attrs -> unit diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml index b20bdb3d3..87e973ca8 100644 --- a/helm/software/lambda-delta/dual_rg/drg.ml +++ b/helm/software/lambda-delta/dual_rg/drg.ml @@ -37,7 +37,7 @@ type entity = term Entity.entity (* helpers ******************************************************************) let mk_uri root s = - String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"] + String.concat "/" ["ld:"; "crg"; root; s ^ ".ld"] let empty_lenv = ESort diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 0c85bb0c5..6f7d60e9c 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -115,7 +115,7 @@ let count_entity st = function let export_entity si g moch = function | DrgEntity e -> X.export_entity DO.export_term si g e - | BrgEntity e -> X.old_export_entity BrgO.export_term si g e + | BrgEntity e -> X.export_entity BrgO.export_term si g e | MetaEntity e -> begin match moch with | None -> () diff --git a/helm/software/lambda-delta/xml/ld-html-entity.xsl b/helm/software/lambda-delta/xml/ld-html-entity.xsl new file mode 100644 index 000000000..ac30dacbf --- /dev/null +++ b/helm/software/lambda-delta/xml/ld-html-entity.xsl @@ -0,0 +1,34 @@ + + + + + + + + + +

+ Declaration: + +

+
+ + + +

+ Definition: + +

+
+ + + diff --git a/helm/software/lambda-delta/xml/ld-html-entry.xsl b/helm/software/lambda-delta/xml/ld-html-entry.xsl deleted file mode 100644 index c80119f79..000000000 --- a/helm/software/lambda-delta/xml/ld-html-entry.xsl +++ /dev/null @@ -1,42 +0,0 @@ - - - - - - - - - -

- Declaration: - -

-
- - - -

- Definition: - -

-
- - - -

- Exclusion: - -

-
- - - diff --git a/helm/software/lambda-delta/xml/ld-html-library.xsl b/helm/software/lambda-delta/xml/ld-html-library.xsl index 3479c3038..cf6857d65 100644 --- a/helm/software/lambda-delta/xml/ld-html-library.xsl +++ b/helm/software/lambda-delta/xml/ld-html-library.xsl @@ -101,8 +101,10 @@ - - + + + + @@ -137,7 +139,7 @@ - + diff --git a/helm/software/lambda-delta/xml/ld-html-root.xsl b/helm/software/lambda-delta/xml/ld-html-root.xsl index 8ee5ebcae..2b8edb470 100644 --- a/helm/software/lambda-delta/xml/ld-html-root.xsl +++ b/helm/software/lambda-delta/xml/ld-html-root.xsl @@ -13,7 +13,8 @@ - + + @@ -54,7 +55,7 @@ - +

Validation parameters: diff --git a/helm/software/lambda-delta/xml/ld-html.xsl b/helm/software/lambda-delta/xml/ld-html.xsl index f166025db..b5ed85342 100644 --- a/helm/software/lambda-delta/xml/ld-html.xsl +++ b/helm/software/lambda-delta/xml/ld-html.xsl @@ -17,7 +17,7 @@ - + - + - - - - - +