the commit continues with the support for validation (inactive for now)

[helm.git] / helm / software / helena / src / basic_rg / brgUntrusted.ml

diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.ml b/helm/software/helena/src/basic_rg/brgUntrusted.ml
index 27f471f9a81eb8899f05f6cf9ed0492f049ab66c..373f9497399622582a6267c54411ff59fed53fde 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgUntrusted.ml
+++ b/helm/software/helena/src/basic_rg/brgUntrusted.ml
@@ -16,6 +16,7 @@ module B  = Brg
 module BE = BrgEnvironment
 module BR = BrgReduction
 module BT = BrgType
+module BV = BrgValidity
 
 (* Interface functions ******************************************************)
 
@@ -36,3 +37,12 @@ let type_check err f st = function
       in
       L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t
    | _, _, E.Void          -> assert false
+
+let validate err f st e =
+   let uri, t = match e with
+      | _, uri, E.Abst (_, t) -> uri, t
+      | _, uri, E.Abbr t      -> uri, t
+      | _, _,   E.Void        -> assert false
+   in
+   let f () = let _ = BE.set_entity e in f () in
+   L.loc := U.string_of_uri uri; BV.validate err f st BR.empty_kam t