let get_candidates ?env mode tree term =
let s =
match mode with
- | Matching -> Index.retrieve_generalizations tree term
- | Unification -> Index.retrieve_unifiables tree term
+ | Matching ->
+ let _ = <:start<retrieve_generalizations>> in
+ <:stop<retrieve_generalizations
+ Index.retrieve_generalizations tree term
+ >>
+ | Unification ->
+ let _ = <:start<retrieve_unifiables>> in
+ <:stop<retrieve_unifiables
+ Index.retrieve_unifiables tree term
+ >>
+
in
Index.PosEqSet.elements s
;;
let name = C.Name "x" in
let bo' =
let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
- C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+ C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
S.lift 1 eq_ty; l; r]
in
if sign = Utils.Positive then
let res, lifted_term =
match term with
| C.Meta (i, l) ->
+ let l = [] in
let l', lifted_l =
List.fold_right
(fun arg (res, lifted_tl) ->
let bo'' =
let l, r =
if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
- C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+ C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
S.lift 1 eq_ty; l; r]
in
bo',
Utils.compare_weights ~normalize:true
(Utils.weight_of_term l) (Utils.weight_of_term r)
in
- let big,small,possmall =
- match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
- in
- let expansions, _ = betaexpand_term menv context ugraph table 0 big in
- List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
+
+ if c = Utils.Incomparable then
+ let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
+ let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
+ prerr_endline "ZZZ";
+ prerr_endline (string_of_int (List.length expansionsl));
+ prerr_endline (string_of_int (List.length expansionsr));
+ List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+ @
+ List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+
+ else
+ let big,small,possmall =
+ match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
+ in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
;;
(** demodulation, when the target is a goal *)