severe bug found in parallel zeta

[helm.git] / matita / components / binaries / probe / nCicScan.ml

diff --git a/matita/components/binaries/probe/nCicScan.ml b/matita/components/binaries/probe/nCicScan.ml
index a289af829936425b36dbef22e56bc95177696d8e..fc6957292645700ec33c5b340e09aad9f8df98c9 100644 (file)
--- a/matita/components/binaries/probe/nCicScan.ml
+++ b/matita/components/binaries/probe/nCicScan.ml
@@ -9,21 +9,26 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-module L = List
+module L  = List
 
-module U = NUri
-module R = NReference
-module C = NCic
-module P = NCicPp
-module E = NCicEnvironment
+module U  = NUri
+module US = U.UriSet
+module R  = NReference
+module C  = NCic
+module P  = NCicPp
+module E  = NCicEnvironment
 
-module O = Options
+module O  = Options
 
 let status = new P.status
 
 let malformed () =
    failwith "probe: malformed term"
 
+let add_attr n (_, xf, _) = O.add_xflavour n (xf:>O.def_xflavour)
+
+let add_ind n = O.add_xflavour n `Inductive
+
 let rec set_list c ts cts =
    let map cts t = (c, t) :: cts in
    L.fold_left map cts ts
@@ -50,7 +55,7 @@ let scan_gref a = function
    | R.Ref (u, R.Def _)
    | R.Ref (u, R.Fix _)
    | R.Ref (u, R.CoFix _) ->
-      if L.exists (U.eq u) !O.objs then a else succ a
+      if US.mem u !O.objs then a else succ a
 
 let rec scan_term a = function
    | []                                 -> a
@@ -70,16 +75,20 @@ let rec scan_term a = function
    | (c, C.LetIn (s, t0, t1, t2)) :: tl ->
       scan_term a ((c, t0) :: (c, t1) :: ((s, C.Def (t1, t0)) :: c, t2) :: tl)
 
-let scan_obj a u = 
+let scan_obj u a = 
    let _, _, _, _, obj = E.get_checked_obj status u in 
    match obj with
-      | C.Constant (_, _, None, t, _)     ->
+      | C.Constant (_, _, None, t, m)     ->
+         add_attr 1 m;
          scan_term (succ a) [[], t]
-      | C.Constant (_, _, Some t0, t1, _) ->
+      | C.Constant (_, _, Some t0, t1, m) ->
+         add_attr 1 m;
          scan_term (succ a) (set_list [] [t0; t1] [])
-      | C.Fixpoint (_, rfs, _)            ->
+      | C.Fixpoint (_, rfs, m)            ->
+         add_attr (L.length rfs) m;
          scan_term (a + L.length rfs) (set_funs [] rfs [])
       | C.Inductive (_, _, its, _)        ->
+         add_ind (L.length its);
         let cts = L.fold_left (set_type []) [] its in
          scan_term (a + L.length cts) cts
 
@@ -94,5 +103,5 @@ let accept_obj u =
 
 let scan () = 
    if !O.exclude <> [] then 
-      O.objs := L.filter accept_obj !O.objs;
-   O.net := L.fold_left scan_obj !O.net !O.objs
+      O.objs := US.filter accept_obj !O.objs;
+   O.net := US.fold scan_obj !O.objs !O.net