]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/toplevel/top.ml
- lambda-delta: some fixes: now the grundlagen type-checkes through dual_rg
[helm.git] / helm / software / lambda-delta / toplevel / top.ml
index 6e6ccfc288e34b0838232020c82574c32babe7f4..0c85bb0c5dab51560344bdc7b5189f578860a460 100644 (file)
@@ -94,6 +94,19 @@ let xlate f st entity = match !kernel, entity with
       let f e = f st (BagEntity e) in Y.xlate f MBag.bag_of_meta e  
    | _, entity         -> f st entity
 
+let pp_progress e =
+   let f a u =
+      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
+      Y.mark err f a
+   in
+   match e with
+      | DrgEntity e -> Y.common f e
+      | BrgEntity e -> Y.common f e
+      | BagEntity e -> Y.common f 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}
@@ -134,13 +147,7 @@ let graph = ref (H.graph_of_string C.err C.start "Z2")
 let old = ref false
 
 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
+   f st
 
 let process_2 f st entity =
    let st = count_entity st entity in
@@ -148,6 +155,7 @@ let process_2 f st entity =
    if !stage > 2 then type_check (process_3 f) st !si !graph entity else f st
            
 let process_1 f st entity = 
+   if !progress then pp_progress entity;
    let st = count_entity st entity 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