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) ->
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 *)