]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_procedural/proceduralClassify.ml
fixed bug in coercion application, input/output swapped in unification
[helm.git] / helm / software / components / acic_procedural / proceduralClassify.ml
index 981acc969678302644d591be5bbe540702accd36..6da59eed1cf643ba4d68f4039b2b0d89dfb42642 100644 (file)
@@ -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