X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralClassify.ml;h=a607bf60d039fd3fc2ec6af7287d04bdaee42801;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=e69b471ca265400e5057f99c5870529c85072e3f;hpb=9ece6e414b255f519426d5643782af4f7dfc584f;p=helm.git diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml index e69b471ca..a607bf60d 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 = @@ -78,7 +86,7 @@ let classify_conclusion vs = let classify c t = try - let vs, h = PEH.split_with_normalize (c, t) in + let vs, h = PEH.split_with_whd (c, t) in let rc = classify_conclusion vs in let map (b, h) (c, v) = let _, argsno = PEH.split_with_whd (c, v) in