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

[helm.git] / helm / software / helena / src / toplevel / top.ml

diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml
index d0476f78ac85e9d2cf7144a0112dfe932ec5ff17..52d2b0be2e2c548289d426eb2e3dbce69ee4165e 100644 (file)
--- a/helm/software/helena/src/toplevel/top.ml
+++ b/helm/software/helena/src/toplevel/top.ml
@@ -95,7 +95,7 @@ let pp_progress e =
       let s = U.string_of_uri u in
       let err () = L.warn (P.sprintf "%s" s) in
       let f i = L.warn (P.sprintf "[%u] %s" i s) in
-      E.mark err f a
+      E.apix err f a
    in
    match e with
       | CrgEntity e -> E.common f e
@@ -120,6 +120,14 @@ let type_check st k =
       | BagEntity entity -> ZU.type_check ok st.kst entity
       | CrgEntity _      -> st
 
+let validate st k =
+   let brg_err msg = brg_error "Validation Error" msg; failwith "Interrupted" in
+   let ok _ = st in
+   match k with
+      | BrgEntity entity -> BU.validate brg_err ok st.kst entity
+      | BagEntity _      -> st
+      | CrgEntity _      -> st
+
 (* extended lexer ***********************************************************)
 
 type 'token lexer = {
@@ -192,6 +200,7 @@ let count_input st = function
 
 (****************************************************************************)
 
+let version = ref true
 let stage = ref 3
 let progress = ref false
 let preprocess = ref false
@@ -203,7 +212,10 @@ let streaming = ref false (* parsing style (temporary) *)
 let process_2 st entity =
    let st = if !L.level > 2 then count_entity st entity else st in
    if !export then export_entity entity;
-   if !stage > 2 then type_check st entity else st
+   if !stage > 2 then 
+      let f = if !version then validate else type_check in 
+      f st entity
+   else st
            
 let process_1 st entity = 
    if !progress then pp_progress entity;
@@ -261,7 +273,7 @@ let process st name =
 
 let main =
 try 
-   let version_string = "Helena 0.8.2 M - January 2011" in
+   let version_string = "Helena 0.8.2 M - November 2014" in
    let print_version () = L.warn (version_string ^ "\n"); exit 0 in
    let set_hierarchy s = 
       if H.set_graph s then () else 
@@ -282,6 +294,7 @@ try
       st := initial_status ();
       L.clear (); G.clear (); H.clear (); O.clear_reductions ();
       streaming := false;
+      version := true
    in
    let process_file name =
       if !L.level > 0 then Y.gmtime version_string;      
@@ -308,7 +321,7 @@ try
       flush_all ()
    in
    let help = 
-      "Usage: helena [ -LPVXcgijopqx1 | -Ss <number> | -O <dir> | -hkr <string> ]* [ <file> ]*\n\n" ^
+      "Usage: helena [ -LPVXcgijopqtx1 | -Ss <number> | -O <dir> | -hkr <string> ]* [ <file> ]*\n\n" ^
       "Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \
        3 data information, 4 typing information, 5 reduction information\n\n" ^
        "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
@@ -331,6 +344,7 @@ try
    let help_q = " disable quotation of identifiers" in
    let help_r = "<string>  set initial segment of URI hierarchy (default: empty)" in
    let help_s = "<number>  set translation stage (see above)" in
+   let help_t = " type check [version 1]" in
    let help_x = " export kernel entities (XML)" in
    
    let help_1 = " parse files with streaming policy" in
@@ -354,6 +368,7 @@ try
       ("-q", Arg.Set G.unquote, help_q);      
       ("-r", Arg.String set_root, help_r);
       ("-s", Arg.Int set_stage, help_s);
+      ("-t", Arg.Clear version, help_t);      
       ("-x", Arg.Set export, help_x);
       ("-1", Arg.Set streaming, help_1);      
    ] process_file help;