a module was missing .........

[helm.git] / helm / software / lambda-delta / src / toplevel / top.ml

diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml
index f69c4b8df7375c9d12951f8ccd9c6dedd2d0a4c4..95ff41df34783cfc79a5d060927c57e7a6b4776e 100644 (file)
--- a/helm/software/lambda-delta/src/toplevel/top.ml
+++ b/helm/software/lambda-delta/src/toplevel/top.ml
@@ -27,7 +27,6 @@ module TD = CrgTxt
 module AD = CrgAut
 module MA = MetaAut
 module MO = MetaOutput
-module ML = MetaLibrary
 module MB = MetaBrg
 module BD = BrgCrg
 module BO = BrgOutput
@@ -120,14 +119,10 @@ let count_entity st = function
    | BagEntity e  -> {st with bagc = ZO.count_entity C.start st.bagc e}
    | _            -> st
 
-let export_entity si xdir moch = function
+let export_entity si xdir = function
    | CrgEntity e  -> XL.export_entity XD.export_term si xdir e
    | BrgEntity e  -> XL.export_entity BO.export_term si xdir e
-   | MetaEntity e ->
-      begin match moch with
-         | None     -> ()
-         | Some och -> ML.write_entity C.start och e
-      end
+   | MetaEntity _
    | BagEntity _  -> ()
 
 let type_check st k =
@@ -212,8 +207,6 @@ let count_input st = function
 (****************************************************************************)
 
 let stage = ref 3
-let moch = ref None
-let meta = ref false
 let progress = ref false
 let preprocess = ref false
 let root = ref ""
@@ -225,13 +218,13 @@ 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 !G.si !export !moch entity;
+   if !export <> "" then export_entity !G.si !export entity;
    if !stage > 2 then type_check st entity else st
            
 let process_1 st entity = 
    if !progress then pp_progress entity;
    let st = if !L.level > 2 then count_entity st entity else st in
-   if !export <> "" && !stage = 1 then export_entity !G.si !export !moch entity;
+   if !export <> "" && !stage = 1 then export_entity !G.si !export entity;
    if !stage > 1 then process_2 st (xlate_entity entity) else st 
 
 let process_0 st entity = 
@@ -256,9 +249,10 @@ let process_0 st entity =
    if !preprocess then process_input f st entity else f st entity
 
 let process_nostreaming st lexbuf input =
+   let id x = x in
    let rec aux1 book = match entity_of_input lexbuf input with
       | NoEntity -> List.rev book
-      | e        -> aux1 (e :: book)   
+      | e        -> aux1 (id e :: book)   
    in
    let rec aux2 st = function
       | []           -> st
@@ -266,9 +260,12 @@ let process_nostreaming st lexbuf input =
    in
    aux2 st (aux1 [])
 
-let rec process_streaming st lexbuf input = match entity_of_input lexbuf input with
-   | NoEntity -> st
-   | e        -> process_streaming (process_0 st e) lexbuf input   
+let process_streaming st lexbuf input =
+   let rec aux st = match entity_of_input lexbuf input with
+      | NoEntity -> st
+      | e        -> aux (process_0 st e)
+   in
+   aux st
 
 (****************************************************************************)
 
@@ -282,7 +279,7 @@ let process st name =
 
 let main =
 try 
-   let version_string = "Helena 0.8.1 M - August 2010" in
+   let version_string = "Helena 0.8.1 M - October 2010" in
    let print_version () = L.warn (version_string ^ "\n"); exit 0 in
    let set_hierarchy s = 
       if H.set_graph s then () else 
@@ -295,20 +292,12 @@ try
    in
    let set_summary i = L.level := i in
    let set_stage i = stage := i in
-   let set_meta_file name =
-      let f och = moch := Some och in
-      ML.open_out f name
-   in
    let set_xdir s = export := s in
    let set_root s = root := s in
-   let close = function
-      | None     -> ()
-      | Some och -> ML.close_out C.start och
-   in
    let clear_options () =
-      stage := 3; moch := None; meta := false; progress := false;
+      stage := 3; progress := false; old := false; 
       preprocess := false; root := ""; cc := false; export := "";
-      old := false; kernel := Brg; st := initial_status ();
+      kernel := Brg; st := initial_status ();
       L.clear (); G.clear (); H.clear (); O.clear_reductions ();
       streaming := false;
    in
@@ -318,7 +307,6 @@ try
          L.warn (P.sprintf "Processing file: %s" name);
       if !L.level > 0 then Y.utime_stamp "started";
       let base_name = Filename.chop_extension (Filename.basename name) in
-      if !meta then set_meta_file base_name;
       let mk_uri =
          if !stage < 2 then Crg.mk_uri else
         match !kernel with
@@ -339,12 +327,11 @@ try
       end
    in
    let exit () =
-      close !moch;
       if !L.level > 0 then Y.utime_stamp "at exit";
       flush_all ()
    in
    let help = 
-      "Usage: helena [ -LPVXcgijmopqu1 | -Ss <number> | -x <dir> | -hkr <string> ]* [ <file> ]*\n\n" ^
+      "Usage: helena [ -LPVXcgijopqu1 | -Ss <number> | -x <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"
@@ -361,7 +348,6 @@ try
    let help_i = " show local references by index" in
    let help_j = " show URI of processed kernel objects" in
    let help_k = "<string>  set kernel version (default: brg)" in
-   let help_m = " output intermediate representation (HAL)" in
    let help_o = " use old abstract language instead of crg" in   
    let help_p = " preprocess source" in
    let help_q = " disable quotation of identifiers" in
@@ -385,7 +371,6 @@ try
       ("-i", Arg.Set G.indexes, help_i);
       ("-j", Arg.Set progress, help_j);      
       ("-k", Arg.String set_kernel, help_k);
-      ("-m", Arg.Set meta, help_m); 
       ("-o", Arg.Set old, help_o);      
       ("-p", Arg.Set preprocess, help_p);
       ("-q", Arg.Set G.unquote, help_q);