]> matita.cs.unibo.it Git - helm.git/commitdiff
new toplevel: tentative implementation with more CPS
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 5 Oct 2009 20:55:46 +0000 (20:55 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 5 Oct 2009 20:55:46 +0000 (20:55 +0000)
helm/software/lambda-delta/.depend.opt
helm/software/lambda-delta/toplevel/top.ml

index 1dbe1c488022ea553f3e2c42c29b0e17e5bf0428..1bf429989588aec69f1d977b710328319f7b8be4 100644 (file)
@@ -163,18 +163,18 @@ toplevel/metaBrg.cmx: toplevel/meta.cmx common/entity.cmx lib/cps.cmx \
     basic_rg/brg.cmx toplevel/metaBrg.cmi 
 toplevel/top.cmo: lib/time.cmx common/output.cmi lib/nUri.cmi \
     toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \
-    toplevel/metaBag.cmi toplevel/metaAut.cmi lib/log.cmi common/library.cmi \
-    common/hierarchy.cmi common/entity.cmx lib/cps.cmx \
-    basic_rg/brgUntrusted.cmi basic_rg/brgReduction.cmi \
+    toplevel/metaBag.cmi toplevel/metaAut.cmi toplevel/meta.cmx lib/log.cmi \
+    common/library.cmi common/hierarchy.cmi common/entity.cmx dual_rg/drg.cmx \
+    lib/cps.cmx basic_rg/brgUntrusted.cmi basic_rg/brgReduction.cmi \
     basic_rg/brgOutput.cmi basic_rg/brg.cmx basic_ag/bagUntrusted.cmi \
     basic_ag/bagType.cmi basic_ag/bagOutput.cmi basic_ag/bag.cmx \
     automath/autProcess.cmi automath/autParser.cmi automath/autOutput.cmi \
     automath/autLexer.cmx 
 toplevel/top.cmx: lib/time.cmx common/output.cmx lib/nUri.cmx \
     toplevel/metaOutput.cmx toplevel/metaLibrary.cmx toplevel/metaBrg.cmx \
-    toplevel/metaBag.cmx toplevel/metaAut.cmx lib/log.cmx common/library.cmx \
-    common/hierarchy.cmx common/entity.cmx lib/cps.cmx \
-    basic_rg/brgUntrusted.cmx basic_rg/brgReduction.cmx \
+    toplevel/metaBag.cmx toplevel/metaAut.cmx toplevel/meta.cmx lib/log.cmx \
+    common/library.cmx common/hierarchy.cmx common/entity.cmx dual_rg/drg.cmx \
+    lib/cps.cmx basic_rg/brgUntrusted.cmx basic_rg/brgReduction.cmx \
     basic_rg/brgOutput.cmx basic_rg/brg.cmx basic_ag/bagUntrusted.cmx \
     basic_ag/bagType.cmx basic_ag/bagOutput.cmx basic_ag/bag.cmx \
     automath/autProcess.cmx automath/autParser.cmx automath/autOutput.cmx \
index 2509ffc845ef5cc7611aa793fe460e97395c2452..ff35879ffa6836f94ba1a06066d8fefafadbde64 100644 (file)
@@ -20,6 +20,7 @@ module Y    = Entity
 module X    = Library
 module AP   = AutProcess
 module AO   = AutOutput
+(* module DA   = DrgAut *)
 module MA   = MetaAut
 module MO   = MetaOutput
 module ML   = MetaLibrary
@@ -32,8 +33,9 @@ module BagO = BagOutput
 module BagT = BagType
 module BagU = BagUntrusted
 
-type status = {
+type 'a status = {
    ast : AP.status;
+(*   dst : 'a DA.status; *)
    mst : MA.status;
    ac  : AO.counters;
    mc  : MO.counters;
@@ -41,25 +43,26 @@ type status = {
    bagc: BagO.counters
 }
 
-let initial_status cover = {
+let initial_status mk_uri cover = {
    ac   = AO.initial_counters;
    mc   = MO.initial_counters;
    brgc = BrgO.initial_counters;
    bagc = BagO.initial_counters;
    mst  = MA.initial_status ~cover ();
+(*   dst  = DA.initial_status (mk_uri cover); *)
    ast  = AP.initial_status
 }
 
 let count count_fun c entity =
    if !L.level > 2 then count_fun C.start c entity else c
 
-let flush () = L.flush 0; L.flush_err ()
+let flush_all () = L.flush 0; L.flush_err ()
 
 let bag_error s msg =
-   L.error BagO.specs (L.Warn s :: L.Loc :: msg); flush () 
+   L.error BagO.specs (L.Warn s :: L.Loc :: msg); flush_all () 
 
 let brg_error s msg =
-   L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush () 
+   L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush_all () 
 
 let process_entity f st =
    let f ast = f {st with ast = ast} in
@@ -69,8 +72,10 @@ let process_entity f st =
 
 type kernel = Brg | Bag
 
-type kernel_entity = BrgEntity of Brg.entity
-                   | BagEntity of Bag.entity
+type kernel_entity = BrgEntity  of Brg.entity
+                   | BagEntity  of Bag.entity
+(*                | DrgEntity  of Drg.entity *)
+                  | MetaEntity of Meta.entity
 
 let kernel = ref Brg
 
@@ -78,44 +83,93 @@ let print_counters st = match !kernel with
    | Brg -> BrgO.print_counters C.start st.brgc
    | Bag -> BagO.print_counters C.start st.bagc
 
-let kernel_of_meta f st entity = match !kernel with
-   | Brg -> 
-      let f entity = f st (BrgEntity entity) in
-      Y.xlate f MBrg.brg_of_meta entity
-   | Bag -> 
-      let f entity = f st (BagEntity entity) in
-      Y.xlate f MBag.bag_of_meta entity
+let xlate f st entity = match !kernel, entity with
+   | Brg, MetaEntity e -> 
+      let f e = f st (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e
+   | Bag, MetaEntity e -> 
+      let f e = f st (BagEntity e) in Y.xlate f MBag.bag_of_meta e  
+   | _, entity         -> f st entity
 
 let count_entity st = function
-   | BrgEntity entity -> {st with brgc = count BrgO.count_entity st.brgc entity}
-   | BagEntity entity -> {st with bagc = count BagO.count_entity st.bagc entity}
+   | 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   *)
 
-let export_entity si g = function
-   | BrgEntity entity -> X.old_export_entity BrgO.export_term si g entity
-   | BagEntity _      -> ()
+let export_entity si g moch = function
+   | BrgEntity e  -> X.old_export_entity BrgO.export_term si g e
+   | MetaEntity e ->
+      begin match moch with
+         | None     -> ()
+         | Some och -> ML.write_entity C.start och e
+      end
+   | _            -> ()
 
 let type_check f st si g k =
    let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
-   let f _ (a, u, _) = f st a u in
+   let ok _ (a, u, _) = f st a u in
    match k with
-      | BrgEntity entity -> BrgU.type_check brg_err f ~si g entity
-      | BagEntity entity -> BagU.type_check f ~si g entity
+      | BrgEntity entity     -> BrgU.type_check brg_err ok ~si g entity
+      | BagEntity entity     -> BagU.type_check ok ~si g entity
+(*      | DrgEntity (a, u, _) *)
+      | MetaEntity (a, u, _) -> f st a u
+
+(****************************************************************************)
+
+let stage = ref 3
+let moch = ref None
+let meta = ref false
+let progress = ref false
+let process = 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 process_3 f st a u =
+   if !progress then 
+      let s = U.string_of_uri u in
+      let err () = L.warn (P.sprintf "%s" s); f st in
+      let f i = L.warn (P.sprintf "[%u] %s" i s); f st in
+      Y.mark err f a
+   else
+      f st
+
+let process_2 f st entity =
+   let st = count_entity st entity in
+   if !export then export_entity !si !graph !moch entity;
+   if !stage > 2 then type_check (process_3 f) st !si !graph entity else f st
+           
+let process_1 f st entity = 
+   let st = count_entity st entity in
+   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
+   | []           -> 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
 
 (****************************************************************************)
 
 let main =
 try 
    let version_string = "Helena 0.8.1 M - September 2009" in
-   let stage = ref 3 in
-   let moch = ref None in
-   let meta = ref false in
-   let progress = ref false in
-   let process = ref false in
-   let use_cover = ref true in
-   let si = ref false in
-   let cc = ref false in
-   let export = ref false in
-   let graph = ref (H.graph_of_string C.err C.start "Z2") in
    let set_hierarchy s = 
       let err () = L.warn (P.sprintf "Unknown type hierarchy: %s" s) in
       let f g = graph := g in
@@ -149,63 +203,22 @@ try
       let book = AutParser.book AutLexer.token lexbuf in
       close_in ich;
       if !L.level > 0 then T.utime_stamp "parsed";
-      let rec aux st = function
-         | []           -> st
-        | entity :: tl ->
-(* stage 3 *)
-           let f st a u = 
-               if !progress then 
-                  let s = U.string_of_uri u in
-                  let err () = L.warn (P.sprintf "%s" s); st in
-                  let f i = L.warn (P.sprintf "[%u] %s" i s); st in
-                  Y.mark err f a
-               else
-                  st
-           in
-(* stage 2 *)      
-           let f st entity =
-              let st = count_entity st entity in
-              if !export then export_entity !si !graph entity;
-              if !stage > 2 then type_check f st !si !graph entity else st
-           in
-(* stage 1 *)      
-           let f st mst entity = 
-              let st = {st with
-                 mst = mst; mc = count MO.count_entity st.mc entity
-              } in
-              begin match !moch with
-                 | None     -> ()
-                 | Some och -> ML.write_entity C.start och entity
-              end;
-              if !stage > 1 then kernel_of_meta f st entity else st 
-           in  
-(* stage 0 *)      
-            let st = {st with ac = count AO.count_entity st.ac entity} in
-           let err st mst = {st with mst = mst} in
-           let f st entity =
-              let st = 
-                 if !stage > 0 then
-                    MA.meta_of_aut (err st) (f st) st.mst entity
-                 else st
-              in
-              aux st tl
-           in
-           if !process then process_entity f st entity else f st entity
-      in
       O.clear_reductions ();
       let cover = if !use_cover then base_name else "" in
-      let st = aux (initial_status cover) book in
-      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 && !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 ()
+      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 && !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
    in
    let exit () =
       close !moch;
       if !L.level > 0 then T.utime_stamp "at exit";
-      flush ()
+      flush_all ()
    in
    let help = 
       "Usage: helena [ -Vcijmpux | -Ss <number> | -hk <string> ] <file> ...\n\n" ^
@@ -226,7 +239,7 @@ try
    let help_r = " disable initial segment of URI hierarchy" in
    let help_s = "<number>  set translation stage (see above)" in
    let help_u = " activate sort inclusion" in
-   let help_x = " export kernel objects (XML)" in
+   let help_x = " export kernel entities (XML)" in
    L.box 0; L.box_err ();
    H.set_sorts ignore ["Set"; "Prop"] 0;
    at_exit exit;