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 d1b9ca48d72107bc3db553d19b11c43227c5aa71..8843aa957e85c50d7c8c22bd0c0a010a56ea7541 100644 (file)
--- 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 03e7b5b958a2b44dcca9a1571b7e12e948a60383..480e3c1399ebfddf4be13a33f4fc0b1de3bfca30 100644 (file)
--- 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 9fbb2cdf7008671373e3fedfd3834bad3a8d0832..207fcccda6b7e74649bdae00e08821afbf08b043 100644 (file)
--- 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 45e33178a4ffacc651b4f1eb897e80e6326d36b1..c11614af56c4268ad7c4bdf93df7f5a44b0ab27d 100644 (file)
--- 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 91225c336135384c73c48b60e492dfb0bb76714a..a7f5ae29a6e15bc94812514c7982e0b53af02ed8 100644 (file)
--- 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 5fd4dc38bbdd59cc350983144def2bcbac8e5ad8..7b3a476c3347728f931845cb28ee8d3c897b5e24 100644 (file)
--- 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
-