X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralClassify.ml;h=6da59eed1cf643ba4d68f4039b2b0d89dfb42642;hb=63b86fce8a75490b957e7301517b9006f58321b6;hp=981acc969678302644d591be5bbe540702accd36;hpb=790eccfa6b94dc82826d919691f8d4bfadb04573;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml
index 981acc969..6da59eed1 100644
--- a/helm/software/components/acic_procedural/proceduralClassify.ml
+++ b/helm/software/components/acic_procedural/proceduralClassify.ml
@@ -37,12 +37,14 @@ type conclusion = (int * int * UM.uri * int) option
 
 (* debugging ****************************************************************)
 
-let string_of_entry (inverse, b) =
-   if I.S.mem 0 inverse then begin if b then "CF" else "C" end else
+let string_of_entry synth (inverse, b) =
+   if I.overlaps synth inverse then begin if b then "CF" else "C" end else
    if I.S.is_empty inverse then "I" else "P"
 
-let to_string (classes, rc) =
-   let linearize = String.concat " " (List.map string_of_entry classes) in
+let to_string synth (classes, rc) =
+   let linearize = 
+      String.concat " " (List.map (string_of_entry synth) classes)
+   in
    match rc with
       | None              -> linearize
       | Some (i, j, _, _) -> Printf.sprintf "%s %u %u" linearize i j
@@ -56,6 +58,12 @@ let out_table b =
    Array.iteri map b;
    prerr_newline ()
 
+(* dummy dependences ********************************************************)
+
+let make l =
+   let map _ = I.S.empty, false in
+   List.rev_map map l
+
 (* classification ***********************************************************)
 
 let classify_conclusion vs = 
@@ -82,7 +90,7 @@ try
    let rc = classify_conclusion vs in
    let map (b, h) (c, v) = 
       let _, argsno = PEH.split_with_whd (c, v) in
-      let isf = argsno > 0 || H.is_sort v in
+      let isf = argsno > 0 (* || H.is_sort v *) in
       let iu = H.is_unsafe h (List.hd vs) in
       (I.get_rels_from_premise h v, I.S.empty, isf && iu) :: b, succ h
    in