From 8ab96f137cdd78abea388ca7f58a24ba1bce61e2 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 19 Jun 2006 13:01:52 +0000 Subject: [PATCH] Utils.compare_terms instead of compare_weights fold_right -> fold_right --- components/tactics/paramodulation/indexing.ml | 24 +++++++++++-------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index 7aafcbcd6..e7166324d 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -798,8 +798,8 @@ let rec betaexpand_term | C.Appl l -> let l', lifted_l = - List.fold_right - (fun arg (res, lifted_tl) -> + List.fold_left + (fun (res, lifted_tl) arg -> let arg_res, lifted_arg = betaexpand_term metasenv context ugraph table lift_amount arg in @@ -815,7 +815,7 @@ let rec betaexpand_term lifted_arg::r, s, m, ug, eq_found) res), lifted_arg::lifted_tl) - ) l ([], []) + ) ([], []) (List.rev l) in (List.map (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l', @@ -1050,21 +1050,25 @@ let build_newgoal context goal posu rule expansion = *) let superposition_left (metasenv, context, ugraph) table goal = let proof,menv,eq,ty,l,r = open_goal goal in - let c = - Utils.compare_weights ~normalize:true - (Utils.weight_of_term l) (Utils.weight_of_term r) - in - + let c = !Utils.compare_terms l r in 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 let big,small,possmall = - match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left + 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 -- 2.39.2