the negative equation "target" and one of the positive equations in "table"
*)
let superposition_left (metasenv, context, ugraph) table goal =
+ let names = Utils.names_of_context context in
let proof,menv,eq,ty,l,r = open_goal goal in
let c = !Utils.compare_terms l r in
if c = Utils.Incomparable then
List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
end
else
- let big,small,possmall =
match c with
- Utils.Gt -> (* prerr_endline "GT"; *) l,r,Utils.Right
- | Utils.Lt -> (* prerr_endline "LT"; *) r,l,Utils.Left
- | _ -> assert false
- in
- let expansions, _ = betaexpand_term menv context ugraph table 0 big in
- List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
+ | 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
;;
(** demodulation, when the target is a goal *)