X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2FnCicScan.ml;h=736baafbcc4e67546d7ab09deab874a5473fa487;hb=ea99a55173ebdcfe60f3b3d6f6c979f5d7785d48;hp=f1c2772ec14665a40d213bfeec495423150c51ff;hpb=2f19651bcec24abfb1bf15ff7e1387daad1f6638;p=helm.git

diff --git a/matita/components/binaries/probe/nCicScan.ml b/matita/components/binaries/probe/nCicScan.ml
index f1c2772ec..736baafbc 100644
--- a/matita/components/binaries/probe/nCicScan.ml
+++ b/matita/components/binaries/probe/nCicScan.ml
@@ -1,12 +1,12 @@
 (*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.      
-     \ /   This software is distributed as is, NO WARRANTY.     
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department, University of Bologna, Italy.
+    ||I||
+    ||T||  HELM is free software; you can redistribute it and/or
+    ||A||  modify it under the terms of the GNU General Public License
+    \   /  version 2 or (at your option) any later version.
+     \ /   This software is distributed as is, NO WARRANTY.
       V_______________________________________________________________ *)
 
 module L  = List
@@ -19,6 +19,7 @@ module P  = NCicPp
 module E  = NCicEnvironment
 
 module O  = Options
+module X  = Error
 
 type status = {
 (* current complexity *)
@@ -29,8 +30,10 @@ type status = {
 
 let status = new P.status
 
-let malformed () =
-  failwith "probe: malformed term"
+let add_name str =
+  let u = U.uri_of_string str in
+  if US.mem u !O.names then Printf.eprintf "probe: name clash: %S\n" str;
+  O.names := US.add u !O.names
 
 let add_attr n (_, xf, _) = O.add_xflavour n (xf:>O.def_xflavour)
 
@@ -41,12 +44,15 @@ let rec set_list c ts cts =
   L.fold_left map cts ts
 
 let set_funs c rfs cts =
-  let map cts (_, _, _, t0, t1) = set_list c [t0; t1] cts in
+  let map cts (_, s, _, t0, t1) =
+    add_name s;
+    set_list c [t0; t1] cts
+  in
   L.fold_left map cts rfs
 
-let set_type c cts (_, _, t, css) =
-  let map cts (_, _, t) = (c, t) :: cts in
-  (c, t) :: L.fold_left map cts css
+let set_type c cts (_, s, t, css) =
+  let map cts (_, s, t) = add_name s; (c, t) :: cts in
+  add_name s; (c, t) :: L.fold_left map cts css
 
 let inc st = {st with c = succ st.c}
 
@@ -78,7 +84,7 @@ let rec scan_term st = function
   | (_, C.Sort _)                :: tl -> scan_term (inc st) tl
   | (c, C.Rel i)                 :: tl -> scan_term (scan_lref st c i) tl
   | (_, C.Const p)               :: tl -> scan_term (scan_gref st p) tl
-  | (_, C.Appl [])               :: tl -> malformed ()
+  | (_, C.Appl [])               :: tl -> X.malformed ()
   | (c, C.Appl ts)               :: tl ->
     scan_term (add st (pred (L.length ts))) (set_list c ts tl)
   | (c, C.Match (_, t0, t1, ts)) :: tl ->
@@ -93,11 +99,11 @@ let scan_obj u c =
   let st = {c; u} in
   let _, _, _, _, obj = E.get_checked_obj status u in
   let st = match obj with
-    | C.Constant (_, _, None, t, m)     ->
-      add_attr 1 m;
+    | C.Constant (_, s, None, t, m)     ->
+      add_name s; add_attr 1 m;
       scan_term (inc st) [[], t]
-    | C.Constant (_, _, Some t0, t1, m) ->
-      add_attr 1 m;
+    | C.Constant (_, s, Some t0, t1, m) ->
+      add_name s; add_attr 1 m;
       scan_term (inc st) (set_list [] [t0; t1] [])
     | C.Fixpoint (_, rfs, m)            ->
       add_attr (L.length rfs) m;