From: Ferruccio Guidi Date: Mon, 10 Nov 2014 16:56:55 +0000 (+0000) Subject: we begin the commit of the validation procedure X-Git-Tag: make_still_working~804 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=52a8357823f16af9b3790178c9eb1b57daa1f199;p=helm.git we begin the commit of the validation procedure (this includes some changes in the xml format of exported entities) the procedure seems to introduce a delay, so this commit is partial ... --- diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index d1b9ca48d..8843aa957 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -130,9 +130,9 @@ src/basic_rg/brgOutput.cmx: src/xml/xmlCrg.cmx src/common/options.cmx \ src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brgCrg.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/brgEnvironment.cmo: src/common/entity.cmx \ src/basic_rg/brgEnvironment.cmi -src/basic_rg/brgEnvironment.cmx: src/common/entity.cmx src/basic_rg/brg.cmx \ +src/basic_rg/brgEnvironment.cmx: src/common/entity.cmx \ src/basic_rg/brgEnvironment.cmi src/basic_rg/brgSubstitution.cmi: src/basic_rg/brg.cmx src/basic_rg/brgSubstitution.cmo: src/common/options.cmx src/basic_rg/brg.cmx \ @@ -143,16 +143,26 @@ src/basic_rg/brgReduction.cmi: src/common/status.cmx src/lib/log.cmi \ src/common/entity.cmx src/basic_rg/brg.cmx src/basic_rg/brgReduction.cmo: src/common/status.cmx src/lib/share.cmx \ src/common/output.cmi src/lib/log.cmi src/common/level.cmi \ - src/common/entity.cmx src/lib/cps.cmx src/common/ccs.cmi \ - src/basic_rg/brgOutput.cmi src/basic_rg/brgEnvironment.cmi \ - src/basic_rg/brg.cmx src/basic_rg/brgReduction.cmi + src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \ + src/common/ccs.cmi src/basic_rg/brgOutput.cmi \ + src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \ + src/basic_rg/brgReduction.cmi src/basic_rg/brgReduction.cmx: src/common/status.cmx src/lib/share.cmx \ src/common/output.cmx src/lib/log.cmx src/common/level.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/common/ccs.cmx \ - src/basic_rg/brgOutput.cmx src/basic_rg/brgEnvironment.cmx \ - src/basic_rg/brg.cmx src/basic_rg/brgReduction.cmi -src/basic_rg/brgType.cmi: src/common/status.cmx src/lib/log.cmi \ + src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \ + src/common/ccs.cmx src/basic_rg/brgOutput.cmx \ + src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \ + src/basic_rg/brgReduction.cmi +src/basic_rg/brgValid.cmi: src/common/status.cmx \ src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx +src/basic_rg/brgValid.cmo: src/lib/log.cmi src/common/entity.cmx \ + src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \ + src/basic_rg/brg.cmx src/basic_rg/brgValid.cmi +src/basic_rg/brgValid.cmx: src/lib/log.cmx src/common/entity.cmx \ + src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \ + src/basic_rg/brg.cmx src/basic_rg/brgValid.cmi +src/basic_rg/brgType.cmi: src/common/status.cmx src/basic_rg/brgReduction.cmi \ + src/basic_rg/brg.cmx src/basic_rg/brgType.cmo: src/lib/share.cmx src/lib/log.cmi \ src/common/level.cmi src/common/hierarchy.cmi src/common/entity.cmx \ src/lib/cps.cmx src/basic_rg/brgSubstitution.cmi \ @@ -163,16 +173,16 @@ src/basic_rg/brgType.cmx: src/lib/share.cmx src/lib/log.cmx \ src/lib/cps.cmx src/basic_rg/brgSubstitution.cmx \ src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \ src/basic_rg/brg.cmx src/basic_rg/brgType.cmi -src/basic_rg/brgUntrusted.cmi: src/common/status.cmx src/basic_rg/brgType.cmi \ - src/basic_rg/brg.cmx +src/basic_rg/brgUntrusted.cmi: src/common/status.cmx \ + src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \ - src/basic_rg/brgType.cmi src/basic_rg/brgReduction.cmi \ - src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \ - src/basic_rg/brgUntrusted.cmi + src/basic_rg/brgValid.cmi src/basic_rg/brgType.cmi \ + src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \ + src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmi 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/basic_rg/brgValid.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/basic_ag/bag.cmo: src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bag.cmx: src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bagCrg.cmi: src/complete_rg/crg.cmx src/basic_ag/bag.cmx diff --git a/helm/software/helena/src/lib/log.ml b/helm/software/helena/src/lib/log.ml index 03e7b5b95..480e3c139 100644 --- a/helm/software/helena/src/lib/log.ml +++ b/helm/software/helena/src/lib/log.ml @@ -41,9 +41,9 @@ let err = F.err_formatter let pp_items frm st l items = let pp_item frm = function - | Term (c, t) -> F.fprintf frm "@,%a" (st.pp_term c) t - | LEnv c -> F.fprintf frm "%a" st.pp_lenv c - | Warn s -> F.fprintf frm "@,%s" s + | Term (c, t) -> F.fprintf frm "@ %a%!" (st.pp_term c) t + | LEnv c -> F.fprintf frm "%a%!" st.pp_lenv c + | Warn s -> F.fprintf frm "@ %s%!" s | String s -> F.fprintf frm "%s " s | Loc -> F.fprintf frm " <%s>" !loc in diff --git a/helm/software/helena/src/modules.ml b/helm/software/helena/src/modules.ml index 9fbb2cdf7..207fcccda 100644 --- a/helm/software/helena/src/modules.ml +++ b/helm/software/helena/src/modules.ml @@ -44,6 +44,7 @@ module BE = brgEnvironment module BS = brgSubstitution module BR = brgReduction module BT = brgType +module BV = brgValid module BU = brgUntrusted module Z = bag diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml index 45e33178a..c11614af5 100644 --- a/helm/software/helena/src/xml/xmlCrg.ml +++ b/helm/software/helena/src/xml/xmlCrg.ml @@ -66,7 +66,7 @@ let rec exp_term e t out tab = match t with XL.tag XL.lref attrs out tab | D.TGRef (a, n) -> let a = Y.Name (U.name_of_uri n, true) :: a in - let attrs = [XL.uri n; XL.name a] in + let attrs = [XL.uri n; XL.name a; XL.apix a] in XL.tag XL.gref attrs out tab | D.TCast (a, u, t) -> let attrs = [] in diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml index 91225c336..a7f5ae29a 100644 --- a/helm/software/helena/src/xml/xmlLibrary.ml +++ b/helm/software/helena/src/xml/xmlLibrary.ml @@ -116,6 +116,11 @@ let name a = let f s = "name", s in E.names f map a "" +let apix a = + let err () = "age", "" in + let f i = "age", string_of_int i in + E.apix err f a + let mark a = let err () = "mark", "" in let f i = "mark", string_of_int i in @@ -148,10 +153,10 @@ let export_entity pp_term (a, u, b) = 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 :: info a in + let attrs = uri u :: name a :: apix a :: meta a :: info 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.Abst (n, w) -> tag "GDec" (level n :: attrs) ~contents:(pp_term w) + | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v) | E.Void -> assert false in let opts = if !G.si then "si" else "" in diff --git a/helm/software/helena/src/xml/xmlLibrary.mli b/helm/software/helena/src/xml/xmlLibrary.mli index 5fd4dc38b..7b3a476c3 100644 --- a/helm/software/helena/src/xml/xmlLibrary.mli +++ b/helm/software/helena/src/xml/xmlLibrary.mli @@ -51,9 +51,10 @@ val level: Level.level -> attr val name: Entity.attrs -> attr +val apix: Entity.attrs -> attr + val mark: Entity.attrs -> attr val meta: Entity.attrs -> attr val info: Entity.attrs -> attr list -