drg: we added the "positive projection" in environments

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

diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index ff35879ffa6836f94ba1a06066d8fefafadbde64..3556db37aed72a1ec6f68e66cb4669755d6d7109 100644 (file)
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -20,7 +20,7 @@ module Y    = Entity
 module X    = Library
 module AP   = AutProcess
 module AO   = AutOutput
-(* module DA   = DrgAut *)
+module DA   = DrgAut
 module MA   = MetaAut
 module MO   = MetaOutput
 module ML   = MetaLibrary
@@ -33,9 +33,9 @@ module BagO = BagOutput
 module BagT = BagType
 module BagU = BagUntrusted
 
-type 'a status = {
+type status = {
    ast : AP.status;
-(*   dst : 'a DA.status; *)
+   dst : DA.status;
    mst : MA.status;
    ac  : AO.counters;
    mc  : MO.counters;
@@ -49,7 +49,7 @@ let initial_status mk_uri cover = {
    brgc = BrgO.initial_counters;
    bagc = BagO.initial_counters;
    mst  = MA.initial_status ~cover ();
-(*   dst  = DA.initial_status (mk_uri cover); *)
+   dst  = DA.initial_status (mk_uri cover);
    ast  = AP.initial_status
 }
 
@@ -74,7 +74,7 @@ type kernel = Brg | Bag
 
 type kernel_entity = BrgEntity  of Brg.entity
                    | BagEntity  of Bag.entity
-(*                | DrgEntity  of Drg.entity *)
+                  | DrgEntity  of Drg.entity
                   | MetaEntity of Meta.entity
 
 let kernel = ref Brg
@@ -94,7 +94,7 @@ let count_entity st = function
    | MetaEntity e -> {st with mc = count MO.count_entity st.mc e} 
    | BrgEntity e  -> {st with brgc = count BrgO.count_entity st.brgc e}
    | BagEntity e  -> {st with bagc = count BagO.count_entity st.bagc e}
-(*   | _            -> st   *)
+   | _            -> st
 
 let export_entity si g moch = function
    | BrgEntity e  -> X.old_export_entity BrgO.export_term si g e
@@ -111,7 +111,7 @@ let type_check f st si g k =
    match k with
       | BrgEntity entity     -> BrgU.type_check brg_err ok ~si g entity
       | BagEntity entity     -> BagU.type_check ok ~si g entity
-(*      | DrgEntity (a, u, _) *)
+      | DrgEntity (a, u, _)
       | MetaEntity (a, u, _) -> f st a u
 
 (****************************************************************************)
@@ -120,13 +120,13 @@ let stage = ref 3
 let moch = ref None
 let meta = ref false
 let progress = ref false
-let process = ref false
+let preprocess = ref false
 let use_cover = ref true
 let si = ref false
 let cc = ref false
 let export = ref false
 let graph = ref (H.graph_of_string C.err C.start "Z2")
-let old = ref true
+let old = ref false
 
 let process_3 f st a u =
    if !progress then 
@@ -147,29 +147,30 @@ let process_1 f st entity =
    export_entity !si !graph !moch entity;
    if !stage > 1 then xlate (process_2 f) st entity else f st 
 
-let rec process_0 f st = function
+let process_0 f st entity = 
+   let f st entity =
+      if !stage = 0 then f st else
+      let frr mst = f {st with mst = mst} in
+      let h mst e = process_1 f {st with mst = mst} (MetaEntity e) in
+      let err dst = f {st with dst = dst} in
+      let g dst e = process_1 f {st with dst = dst} (DrgEntity e) in
+      if !old then MA.meta_of_aut frr h st.mst entity else 
+      DA.drg_of_aut err g st.dst entity
+   in
+   let st = {st with ac = count AO.count_entity st.ac entity} in 
+   if !preprocess then process_entity f st entity else f st entity
+
+let rec process f book st = match book with
    | []           -> f st
-   | entity :: tl ->
-      let f st = process_0 f st tl in   
-      let frr st mst = {st with mst = mst} in
-      let h st mst e = 
-           process_1 C.start {st with mst = mst} (MetaEntity e)
-      in
-      let f st entity =
-        if !stage = 0 then f st else
-(*       let err st dst = f {st with dst = dst} in
-         let g st dst e = process_1 f {st with dst = dst} (DrgEntity e) in
-        if !old then *) f (MA.meta_of_aut (frr st) (h st) st.mst entity) (* else 
-        DA.drg_of_aut (err st) (g st) st.dst entity *)
-      in
-      let st = {st with ac = count AO.count_entity st.ac entity} in 
-      if !process then process_entity f st entity else f st entity
+   | entity :: tl -> 
+      process f tl (process_0 C.start st entity) 
+(*      process_0 (process f tl) st entity *) (* CPS variant of the above *)
 
 (****************************************************************************)
 
 let main =
 try 
-   let version_string = "Helena 0.8.1 M - September 2009" in
+   let version_string = "Helena 0.8.1 M - October 2009" in
    let set_hierarchy s = 
       let err () = L.warn (P.sprintf "Unknown type hierarchy: %s" s) in
       let f g = graph := g in
@@ -208,12 +209,12 @@ try
       let f st = 
          if !L.level > 0 then T.utime_stamp "processed";
          if !L.level > 2 then AO.print_counters C.start st.ac;
-         if !L.level > 2 && !process then AO.print_process_counters C.start st.ast;
+         if !L.level > 2 && !preprocess then AO.print_process_counters C.start st.ast;
          if !L.level > 2 && !stage > 0 then MO.print_counters C.start st.mc;
          if !L.level > 2 && !stage > 1 then print_counters st;
          if !L.level > 2 && !stage > 1 then O.print_reductions ()
       in
-      process_0 f (initial_status Drg.mk_uri cover) book
+      process f book (initial_status Drg.mk_uri cover)
    in
    let exit () =
       close !moch;
@@ -221,7 +222,7 @@ try
       flush_all ()
    in
    let help = 
-      "Usage: helena [ -Vcijmpux | -Ss <number> | -hk <string> ] <file> ...\n\n" ^
+      "Usage: helena [ -Vcijmopux | -Ss <number> | -hk <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"
@@ -235,6 +236,7 @@ try
    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 drg" in   
    let help_p = " preprocess Automath source" in
    let help_r = " disable initial segment of URI hierarchy" in
    let help_s = "<number>  set translation stage (see above)" in
@@ -252,7 +254,8 @@ try
       ("-j", Arg.Set progress, help_j);      
       ("-k", Arg.String set_kernel, help_k);
       ("-m", Arg.Set meta, help_m); 
-      ("-p", Arg.Set process, help_p);      
+      ("-o", Arg.Set old, help_o);      
+      ("-p", Arg.Set preprocess, help_p);      
       ("-r", Arg.Clear use_cover, help_r);
       ("-s", Arg.Int set_stage, help_s);
       ("-u", Arg.Set si, help_u);