module H = ProceduralHelpers
-type dependence = I.S.t * bool
+type dependences = (I.S.t * bool) list
type conclusion = (int * int * UM.uri * int) option
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
let extract (x, y, z) = y, z in
List.rev_map extract (List.tl (Array.to_list b)), rc
with Invalid_argument _ -> failwith "Classify.classify"
+
+(* adjusting the inferrable arguments that do not occur in the goal *********)
+
+let adjust c vs ?goal classes =
+ let list_xmap2 map l1 l2 =
+ let rec aux a = function
+ | hd1 :: tl1, hd2 :: tl2 -> aux (map hd1 hd2 :: a) (tl1,tl2)
+ | _, l2 -> List.rev_append l2 a
+ in
+ List.rev (aux [] (l1, l2))
+ in
+ let map where what (i, b) =
+ let what = H.cic what in
+ (i, b || not (H.occurs c ~what ~where))
+ in
+ match goal with
+ | None -> classes
+ | Some goal -> list_xmap2 (map goal) vs classes