- let c =
- 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
+ let c = !Utils.compare_terms l r in
+ let newgoals =
+ if c = Utils.Incomparable then
+ begin
+ let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
+ let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
+ (* prerr_endline "incomparable";
+ 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
+ end
+ else
+ match c with
+ | Utils.Gt -> (* prerr_endline "GT"; *)
+ let big,small,possmall = l,r,Utils.Right in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map
+ (build_newgoal context goal possmall Equality.SuperpositionLeft)
+ expansions
+ | Utils.Lt -> (* prerr_endline "LT"; *)
+ let big,small,possmall = 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
+ | Utils.Eq -> []
+ | _ ->
+ prerr_endline
+ ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
+ assert false