]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/toplevel/top.ml
basic_rg: reduction was not tail recursive by mistake
[helm.git] / helm / software / lambda-delta / toplevel / top.ml
index 12e639c5636da1e1fa389544a3ff91f1d44bf17b..1bab9136be2a569e51fd84ddb4e2f6cee8115a57 100644 (file)
@@ -55,9 +55,6 @@ let 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_all () = L.flush 0; L.flush_err ()
 
 let bag_error s msg =
@@ -66,9 +63,9 @@ let bag_error s msg =
 let brg_error s msg =
    L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush_all () 
 
-let process_entity f st =
+let process_entity f st entity =
    let f ast = f {st with ast = ast} in
-   AP.process_entity f st.ast
+   AP.process_entity f st.ast entity
 
 (* kernel related ***********************************************************)
 
@@ -85,14 +82,14 @@ let print_counters st = match !kernel with
    | Brg -> BrgO.print_counters C.start st.brgc
    | Bag -> BagO.print_counters C.start st.bagc
 
-let xlate f st entity = match !kernel, entity with
+let xlate_entity entity = match !kernel, entity with
    | Brg, CrgEntity e  -> 
-      let f e = f st (BrgEntity e) in Y.xlate f DBrg.brg_of_crg e
+      let f e = (BrgEntity e) in Y.xlate f DBrg.brg_of_crg e
    | Brg, MetaEntity e -> 
-      let f e = f st (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e
+      let f e = (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 f e = (BagEntity e) in Y.xlate f MBag.bag_of_meta e  
+   | _, entity         -> entity
 
 let pp_progress e =
    let f a u =
@@ -108,9 +105,9 @@ let pp_progress e =
       | MetaEntity e -> Y.common f e
 
 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}
+   | MetaEntity e -> {st with mc = MO.count_entity C.start st.mc e} 
+   | BrgEntity e  -> {st with brgc = BrgO.count_entity C.start st.brgc e}
+   | BagEntity e  -> {st with bagc = BagO.count_entity C.start st.bagc e}
    | _            -> st
 
 let export_entity si g moch = function
@@ -123,14 +120,14 @@ let export_entity si g moch = function
       end
    | BagEntity _  -> ()
 
-let type_check st si g k =
+let type_check st si g k =
    let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
-   let ok _ _ = st in
+   let ok _ _ = st in
    match k with
       | BrgEntity entity -> BrgU.type_check brg_err ok ~si g entity
       | BagEntity entity -> BagU.type_check ok ~si g entity
       | CrgEntity _
-      | MetaEntity _     -> st
+      | MetaEntity _     -> st
 
 (****************************************************************************)
 
@@ -146,38 +143,36 @@ let export = ref false
 let graph = ref (H.graph_of_string C.err C.start "Z2")
 let old = ref false
 
-let process_3 f st =
-   f st
-
-let process_2 f st entity =
-   let st = count_entity st entity in
+let process_2 st entity =
+   let st = if !L.level > 2 then count_entity st entity else st 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
+   if !stage > 2 then type_check st !si !graph entity else st
            
-let process_1 st entity = 
+let process_1 st entity = 
    if !progress then pp_progress entity;
-   let st = count_entity st entity in
+   let st = if !L.level > 2 then count_entity st entity else st in
    if !export && !stage = 1 then export_entity !si !graph !moch entity;
-   if !stage > 1 then xlate (process_2 f) st entity else f st 
+   if !stage > 1 then process_2 st (xlate_entity entity) else st 
 
-let process_0 st entity = 
+let process_0 st entity = 
    let f st entity =
-      if !stage = 0 then st else
-      let frr mst = {st with mst = mst} in
-      let h mst e = process_1 {st with mst = mst} (MetaEntity e) in
-      let err dst = {st with dst = dst} in
-      let g dst e = process_1 {st with dst = dst} (CrgEntity e) in
+      if !stage = 0 then st else
+      let frr mst = {st with mst = mst} in
+      let h mst e = process_1 {st with mst = mst} (MetaEntity e) in
+      let err dst = {st with dst = dst} in
+      let g dst e = process_1 {st with dst = dst} (CrgEntity e) in
       if !old then MA.meta_of_aut frr h st.mst entity else 
       DA.crg_of_aut err g st.dst entity
    in
-   let st = {st with ac = count AO.count_entity st.ac entity} in 
+   let st = 
+      if !L.level > 2 then {st with ac = AO.count_entity C.start st.ac entity}
+      else st
+   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 -> 
-(* we exploit tail recursion rather than CPS *)
-      process f tl (process_0 C.start st entity)
+let rec process st = function
+   | []           -> st
+   | entity :: tl -> process (process_0 st entity) tl
 
 (****************************************************************************)
 
@@ -225,15 +220,15 @@ try
            | Bag -> Bag.mk_uri
       in
       let cover = if !use_cover then base_name else "" in
-      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 && !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 f book (initial_status mk_uri cover)
+      let st = process (initial_status mk_uri cover) book in
+      if !L.level > 0 then T.utime_stamp "processed";
+      if !L.level > 2 then begin
+         AO.print_counters C.start st.ac;
+         if !preprocess then AO.print_process_counters C.start st.ast;
+         if !stage > 0 then MO.print_counters C.start st.mc;
+         if !stage > 1 then print_counters st;
+         if !stage > 2 then O.print_reductions ()
+      end
    in
    let exit () =
       close !moch;