- "linear" flag added to lapply (automatic clearing)

[helm.git] / helm / software / components / tactics / paramodulation / indexing.ml

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 7aafcbcd627927c66ced9577151dd61f2ef985ab..c74abe27d4605b8cf7b2638b826b8181d2bf77ca 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/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',
@@ -1049,25 +1049,40 @@ let build_newgoal context goal posu rule expansion =
    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_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
-    in
-    let expansions, _ = betaexpand_term menv context ugraph table 0 big in
-    List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
+      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
 ;;
 
 (** demodulation, when the target is a goal *)