X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=7ff0dfd2cc6560dd0b7cfefbb8d088122875283c;hb=ba5f2cc720dd8fbb74214cfd99d63fb7330ffce3;hp=7cdbf43d38a2242938c5f83c710f08f3cfe08761;hpb=d990d5c64d0b9c07baef4257e7931321a42ae695;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 7cdbf43d3..7ff0dfd2c 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -145,7 +145,7 @@ let not_unit_eq ctx eq =
   List.exists 
     (fun (_,_,ty) ->
        try 
-	 let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.empty_ugraph
+	 let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.oblivion_ugraph
 	 in s = Cic.Sort(Cic.Prop)
        with _ -> 
 	 prerr_endline ("ERROR typing " ^ CicPp.ppterm ty); assert false) metas
@@ -164,8 +164,8 @@ let check_demod_res res metasenv msg =
 	in
 	  if (not b) then
 	    begin
-	      prerr_endline ("extended context " ^ msg);
-	      prerr_endline (CicMetaSubst.ppmetasenv [] menv);
+	      debug_print (lazy ("extended context " ^ msg));
+	      debug_print (lazy (CicMetaSubst.ppmetasenv [] menv));
 	    end;
 	b
     | None -> false
@@ -313,7 +313,8 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty =
               Founif.matching 
                 metasenv metas context term (S.lift lift_amount c) ugraph
             in
-	    check_metasenv "founif :" metasenv';
+            if Utils.debug_metas then
+    	      check_metasenv "founif :" metasenv';
             Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
           in
           let c, other =
@@ -360,7 +361,7 @@ let find_matches metasenv context ugraph lift_amount term termty =
   can be either Founif.matching or Inference.unification
 *)
 (* XXX termty unused *)
-let rec find_all_matches ?(unif_fun=Founif.unification)
+let rec find_all_matches ?(unif_fun=Founif.unification) ?(demod=false)
     metasenv context ugraph lift_amount term termty =
   let module C = Cic in
   let module U = Utils in
@@ -368,7 +369,16 @@ let rec find_all_matches ?(unif_fun=Founif.unification)
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   (* prerr_endline ("matching " ^  CicPp.ppterm term); *)
-  let cmp = !Utils.compare_terms in
+  let cmp x y = 
+          let r = !Utils.compare_terms x y in
+(*
+          prerr_endline (
+                  CicPp.ppterm x ^ "   " ^
+                  Utils.string_of_comparison r ^ "   " ^ 
+                       CicPp.ppterm y ); 
+*)
+          r
+  in
   let check = match termty with C.Implicit None -> false | _ -> true in
   function
     | [] -> []
@@ -409,12 +419,14 @@ let rec find_all_matches ?(unif_fun=Founif.unification)
                 let c' = apply_subst s c
                 and other' = apply_subst s other in
                 let order = cmp c' other' in
-                if order <> U.Lt && order <> U.Le then
+                if (demod && order = U.Gt) ||
+                   (not demod && (order <> U.Lt && order <> U.Le)) 
+                then
                   res::(find_all_matches ~unif_fun metasenv context ugraph
                           lift_amount term termty tl)
                 else
                   find_all_matches ~unif_fun metasenv context ugraph
-                    lift_amount term termty tl
+                     lift_amount term termty tl
           with
           | Founif.MatchingFailure
           | CicUnification.UnificationFailure _
@@ -424,10 +436,10 @@ let rec find_all_matches ?(unif_fun=Founif.unification)
 ;;
 
 let find_all_matches 
-  ?unif_fun metasenv context ugraph lift_amount term termty l 
+  ?unif_fun ?demod metasenv context ugraph lift_amount term termty l 
 =
     find_all_matches 
-      ?unif_fun metasenv context ugraph lift_amount term termty l 
+      ?unif_fun ?demod metasenv context ugraph lift_amount term termty l 
   (*prerr_endline "CANDIDATES:";
   List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
   prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
@@ -506,7 +518,8 @@ let subsumption_aux_all use_unification env table target =
   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
   let _, context, ugraph = env in
   let metasenv = tmetas in
-  check_for_duplicates metasenv "subsumption_aux_all";
+  if Utils.debug_metas then
+    check_for_duplicates metasenv "subsumption_aux_all";
   let predicate, unif_fun = 
     if use_unification then
       Unification, Founif.unification
@@ -556,7 +569,7 @@ let subsumption_all x y z =
 ;;
 
 let unification_all x y z = 
-  prerr_endline "unification_all"; subsumption_aux_all true x y z
+  subsumption_aux_all true x y z
 ;;
 
 let rec demodulation_aux bag ?from ?(typecheck=false) 
@@ -565,13 +578,13 @@ let rec demodulation_aux bag ?from ?(typecheck=false)
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
-  (* prerr_endline ("demodulating " ^ CicPp.ppterm term); *)
-  check_for_duplicates metasenv "in input a demodulation aux";
+  if Utils.debug_metas then
+    check_for_duplicates metasenv "in input a demodulation aux";
   let candidates = 
     get_candidates 
       ~env:(metasenv,context,ugraph) (* Unification *) Matching table term 
-  in let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates 
-  in
+  in 
+(*   let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates in *)
   let res =
     match term with
       | C.Meta _ -> None
@@ -677,17 +690,7 @@ let rec demodulation_aux bag ?from ?(typecheck=false)
 exception Foo
 
 (** demodulation, when target is an equality *)
-let rec demodulation_equality bag ?from eq_uri newmeta env table target =
-        (*
-          prerr_endline ("demodulation_eq:\n");
-        Index.iter table (fun l -> 
-          let l = Index.PosEqSet.elements l in
-          let l = 
-            List.map (fun (p,e) -> 
-              Utils.string_of_pos p ^ Equality.string_of_equality e) l in
-          prerr_endline (String.concat "\n" l)
-          );
-          *)
+let rec demodulation_equality bag ?from eq_uri env table target =
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
@@ -707,9 +710,8 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
   if Utils.debug_metas then 
     ignore(check_target bag context target "demod equalities input");
   let metasenv' = (* metasenv @ *) metas in
-  let maxmeta = ref newmeta in
   
-  let build_newtarget is_left (t, subst, menv, ug, eq_found) =
+  let build_newtarget bag is_left (t, subst, menv, ug, eq_found) =
     
     if Utils.debug_metas then
       begin
@@ -721,10 +723,11 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
     let pos, equality = eq_found in
     let (_, proof', 
         (ty, what, other, _), menv',id') = Equality.open_equality equality in
+    (*
     let ty =
-      try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
-      with CicUtil.Meta_not_found _ -> ty
-    in
+      try fst (CicTypeChecker.type_of_aux' menv' context what ugraph)
+      with CicUtil.Meta_not_found _ -> ty 
+    in *)
     let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newproof =
@@ -743,45 +746,44 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
     let left, right = if is_left then newterm, right else left, newterm in
     let ordering = !Utils.compare_terms left right in
     let stat = (eq_ty, left, right, ordering) in
-    let res =
+    let bag, res =
       let w = Utils.compute_equality_weight stat in
-          (Equality.mk_equality bag (w, newproof, stat,newmenv))
+      Equality.mk_equality bag (w, newproof, stat,newmenv)
     in
     if Utils.debug_metas then 
       ignore(check_target bag context res "buildnew_target output");
-    !maxmeta, res 
+    bag, res 
   in
-
   let res = 
     demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left 
   in
   if Utils.debug_res then check_res res "demod result";
-  let newmeta, newtarget = 
+  let bag, newtarget = 
     match res with
     | Some t ->
-        let newmeta, newtarget = build_newtarget true t in
+        let bag, newtarget = build_newtarget bag true t in
           (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
           if (Equality.is_weak_identity newtarget) (* || *)
             (*Equality.meta_convertibility_eq target newtarget*) then
-              newmeta, newtarget
+              bag, newtarget
           else 
-            demodulation_equality bag ?from eq_uri newmeta env table newtarget
+            demodulation_equality bag ?from eq_uri env table newtarget
     | None ->
         let res = demodulation_aux bag metasenv' context ugraph table 0 right in
         if Utils.debug_res then check_res res "demod result 1"; 
           match res with
           | Some t ->
-              let newmeta, newtarget = build_newtarget false t in
+              let bag, newtarget = build_newtarget bag false t in
                 if (Equality.is_weak_identity newtarget) ||
                   (Equality.meta_convertibility_eq target newtarget) then
-                    newmeta, newtarget
+                    bag, newtarget
                 else
-                   demodulation_equality bag ?from eq_uri newmeta env table newtarget
+                   demodulation_equality bag ?from eq_uri env table newtarget
           | None ->
-              newmeta, target
+              bag, target
   in
   (* newmeta, newtarget *)
-  newmeta,newtarget 
+  bag, newtarget 
 ;;
 
 (**
@@ -901,10 +903,11 @@ let rec betaexpand_term
   | C.Meta (i, l) -> res, lifted_term
   | term ->
       let termty, ugraph =
-(*        C.Implicit None, ugraph *)
-         CicTypeChecker.type_of_aux' metasenv context term ugraph 
+       C.Implicit None, ugraph
+(*          CicTypeChecker.type_of_aux' metasenv context term ugraph  *)
       in
       let candidates = get_candidates Unification table term in
+      (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
       let r = 
         if subterms_only then 
           [] 
@@ -923,7 +926,7 @@ let rec betaexpand_term
    index: its updated value is also returned
 *)
 let superposition_right bag
-  ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
+  ?(subterms_only=false) eq_uri (metasenv, context, ugraph) table target=
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
@@ -936,7 +939,6 @@ let superposition_right bag
   if Utils.debug_metas then 
     ignore (check_target bag context target "superpositionright");
   let metasenv' = newmetas in
-  let maxmeta = ref newmeta in
   let res1, res2 =
     match ordering with
     | U.Gt -> 
@@ -954,7 +956,7 @@ let superposition_right bag
         in
         (res left right), (res right left)
   in
-  let build_new ordering (bo, s, m, ug, eq_found) =
+  let build_new bag ordering (bo, s, m, ug, eq_found) =
     if Utils.debug_metas then 
       ignore (check_target bag context (snd eq_found) "buildnew1" );
     
@@ -980,33 +982,41 @@ let superposition_right bag
           (s,(Equality.SuperpositionRight,
                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
     in
-    let newmeta, newequality = 
+    let bag, newequality = 
       let left, right =
         if ordering = U.Gt then newgoal, apply_subst s right
         else apply_subst s left, newgoal in
       let neworder = !Utils.compare_terms left right in
       let newmenv = (* Founif.filter s *) m in
       let stat = (eq_ty, left, right, neworder) in
-      let eq' =
+      let bag, eq' =
         let w = Utils.compute_equality_weight stat in
         Equality.mk_equality bag (w, newproof, stat, newmenv) in
       if Utils.debug_metas then 
         ignore (check_target bag context eq' "buildnew3");
-      let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
+      let bag, eq' = Equality.fix_metas bag eq' in
       if Utils.debug_metas then 
         ignore (check_target bag context eq' "buildnew4");
-      newm, eq'
+      bag, eq'
     in
-    maxmeta := newmeta;
     if Utils.debug_metas then 
       ignore(check_target bag context newequality "buildnew2"); 
-    newequality
+    bag, newequality
+  in
+  let bag, new1 = 
+    List.fold_right 
+      (fun x (bag,acc) -> 
+        let bag, e = build_new bag U.Gt x in
+        bag, e::acc) res1 (bag,[]) 
+  in
+  let bag, new2 = 
+    List.fold_right 
+      (fun x (bag,acc) -> 
+        let bag, e = build_new bag U.Lt x in
+        bag, e::acc) res2 (bag,[]) 
   in
-  let new1 = List.map (build_new U.Gt) res1
-  and new2 = List.map (build_new U.Lt) res2 in
   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
-  (!maxmeta,
-   (List.filter ok (new1 @ new2)))
+  bag, List.filter ok (new1 @ new2)
 ;;
 
 (** demodulation, when the target is a theorem *)
@@ -1085,9 +1095,9 @@ let build_newg bag context goal rule expansion =
 ;;
 
 let rec demod bag env table goal =
-  let goalproof,menv,t = goal in
+  let _,menv,t = goal in
   let _, context, ugraph = env in
-  let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in
+  let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:false)in
   match res with
     | Some newt ->
 	let newg = 
@@ -1163,7 +1173,7 @@ let build_newgoal bag context goal posu rule expansion =
    returns a list of new clauses inferred with a left superposition step
    the negative equation "target" and one of the positive equations in "table"
 *)
-let superposition_left bag (metasenv, context, ugraph) table goal maxmeta = 
+let superposition_left bag (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
@@ -1176,15 +1186,13 @@ let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
       prerr_endline (string_of_int (List.length expansionsl));
       prerr_endline (string_of_int (List.length expansionsr));
       *)
-      if expansionsl <> [] then prerr_endline "expansionl";
-      if expansionsr <> [] then prerr_endline "expansionr";
       List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
       @
       List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
       end
     else
         match c with 
-        | Utils.Gt -> (* prerr_endline "GT"; *) 
+        | Utils.Gt -> 
             let big,small,possmall = l,r,Utils.Right in
             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
             List.map 
@@ -1204,9 +1212,10 @@ let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
   in
   (* rinfresco le meta *)
   List.fold_right
-    (fun g (max,acc) -> 
-       let max,g = Equality.fix_metas_goal max g in max,g::acc) 
-    newgoals (maxmeta,[])
+    (fun g (b,acc) -> 
+       let b,g = Equality.fix_metas_goal b g in 
+       b,g::acc) 
+    newgoals (bag,[])
 ;;
 
 (** demodulation, when the target is a goal *)
@@ -1238,12 +1247,10 @@ let rec demodulation_goal bag env table goal =
   | None -> do_right ()
 ;;
 
-type next = L | R 
-type solved = Yes of Equality.goal | No of Equality.goal list
-
 (* returns all the 1 step demodulations *)
 module C = Cic;; 
 module S = CicSubstitution;;
+
 let rec demodulation_all_aux 
   metasenv context ugraph table lift_amount term 
 =
@@ -1256,100 +1263,178 @@ let rec demodulation_all_aux
       let termty, ugraph = C.Implicit None, ugraph in
       let res =
         find_all_matches 
-          metasenv context ugraph lift_amount term termty candidates
+          ~unif_fun:Founif.matching ~demod:true
+            metasenv context ugraph lift_amount term termty candidates
       in
       match term with
       | C.Appl l ->
-         let res, _, _ = 
+         let res, _, _, _ = 
            List.fold_left
-            (fun (res,l,r) t ->
-               res @ 
-               List.map 
-                 (fun (rel, s, m, ug, c) -> 
-                   (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
-                 (demodulation_all_aux 
-                   metasenv context ugraph table lift_amount t),
-               l@[List.hd r], List.tl r)
-            (res, [], List.map (S.lift 1) l) l
+            (fun (res,b,l,r) t ->
+               if not b then res,b,l,r
+               else
+                 let demods_for_t = 
+                   demodulation_all_aux 
+                     metasenv context ugraph table lift_amount t
+                 in
+                 let b = demods_for_t = [] in
+                 res @  
+                   List.map 
+                    (fun (rel, s, m, ug, c) -> 
+                      (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
+                   demods_for_t, b, l@[List.hd r], List.tl r)
+            (res, true, [], List.map (S.lift 1) l) l
          in
          res
-      | C.Prod (nn, s, t) 
-      | C.Lambda (nn, s, t) ->
-          let context = (Some (nn, C.Decl s))::context in
-          let mk s t = 
-            match term with 
-            | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t)
-          in
-          res @ 
-          List.map
-            (fun (rel, subst, m, ug, c) -> 
-               mk (S.lift 1 s) rel, subst, m, ug, c)
-            (demodulation_all_aux
-              metasenv context ugraph table (lift_amount+1) t)
-              (* we could demodulate also in s, but then t may be badly
-               * typed... *)
       | t -> res
 ;;
 
-let solve_demodulating bag env table initgoal steps =
+let demod_all steps bag env table goal =
   let _, context, ugraph = env in
-  let solved goal res side = 
-    let newg = build_newgoal bag context goal side Equality.Demodulation res in
-    match newg with
-    | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right]) 
-      when LibraryObjects.is_eq_URI uri ->
-        (try 
-          let _ = 
-            Founif.unification m m context left right CicUniv.empty_ugraph 
-          in
-          Yes newg
-        with CicUnification.UnificationFailure _ -> No [newg])
-    | _ -> No [newg]
+  let is_visited l (_,_,t) = 
+    List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l 
   in
-  let solved goal res_list side = 
-    let newg = List.map (fun x -> solved goal x side) res_list in
-    try
-      List.find (function Yes _ -> true | _ -> false) newg
-    with Not_found -> 
-      No (List.flatten (List.map (function No s -> s | _-> assert false) newg))
+  let rec aux steps visited nf bag = function
+    | _ when steps = 0 -> visited, bag, nf
+    | [] -> visited, bag, nf
+    | goal :: rest when is_visited visited goal-> aux steps visited nf bag rest
+    | goal :: rest ->
+        let visited = goal :: visited in
+        let _,menv,t = goal in
+        let res = demodulation_all_aux menv context ugraph table 0 t in
+        let steps = if res = [] then steps-1 else steps in
+        let new_goals = 
+          List.map (build_newg bag context goal Equality.Demodulation) res 
+        in
+        let nf = if new_goals = [] then goal :: nf else nf in
+        aux steps visited nf bag (new_goals @ rest)
   in
-  let rec first f l =
-    match l with
-    | [] -> None
-    | x::tl -> 
-       match f x with
-       | None -> first f tl
-       | Some x as ok -> ok
+  aux steps [] [] bag [goal] 
+;;
+
+let combine_demodulation_proofs bag env goal (pl,ml,l) (pr,mr,r) =
+  let proof,m,eq,ty,left,right = open_goal goal in
+  let pl = 
+    List.map 
+      (fun (rule,pos,id,subst,pred) -> 
+        let pred = 
+          match pred with
+          | Cic.Lambda (name,src,tgt) ->
+              Cic.Lambda (name,src, 
+                Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
+          | _ -> assert false                 
+        in
+        rule,pos,id,subst,pred)
+      pl
+  in
+  let pr = 
+    List.map 
+      (fun (rule,pos,id,subst,pred) -> 
+        let pred = 
+          match pred with
+          | Cic.Lambda (name,src,tgt) ->
+              Cic.Lambda (name,src, 
+                Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
+          | _ -> assert false                 
+        in
+        rule,pos,id,subst,pred)
+      pr
+  in
+  (pr@pl@proof, m, Cic.Appl [eq;ty;l;r])
+;;
+
+let demodulation_all_goal bag env table goal maxnf =
+  let proof,menv,eq,ty,left,right = open_goal goal in
+  let v1, bag, l_demod = demod_all maxnf bag env table ([],menv,left) in
+  let v2, bag, r_demod = demod_all maxnf bag env table ([],menv,right) in
+  let l_demod = if l_demod = [] then [ [], menv, left ] else l_demod in
+  let r_demod = if r_demod = [] then [ [], menv, right ] else r_demod in
+  List.fold_left
+    (fun acc (_,_,l as ld) -> 
+       List.fold_left 
+           (fun acc (_,_,r as rd) ->
+                combine_demodulation_proofs bag env goal ld rd :: acc)
+         acc r_demod)
+    [] l_demod
+;;
+
+let solve_demodulating bag env table initgoal steps =
+  let proof,menv,eq,ty,left,right = open_goal initgoal in
+  let uri = 
+    match eq with
+    | Cic.MutInd (u,_,_) -> u
+    | _ -> assert false
   in
-  let rec aux steps next goal = 
-    if steps = 0 then None else
-    let goalproof,menv,_,_,left,right = open_goal goal in
-    let do_step t = 
-      demodulation_all_aux menv context ugraph table 0 t
+  let _, context, ugraph = env in
+  let v1, bag, l_demod = demod_all steps bag env table ([],menv,left) in
+  let v2, bag, r_demod = demod_all steps bag env table ([],menv,right) in
+  let is_solved left right ml mr =
+    let m = ml @ (List.filter 
+      (fun (x,_,_) -> not (List.exists (fun (y,_,_) -> x=y)ml)) mr) 
     in
-    match next with
-    | L -> 
-        (match do_step left with
-        | _::_ as res -> 
-            (match solved goal res Utils.Right with
-            | No newgoals -> 
-                 (match first (aux (steps - 1) L) newgoals with
-                 | Some g as success -> success
-                 | None -> aux steps R goal)
-            | Yes newgoal -> Some newgoal)
-        | [] -> aux steps R goal)
-    | R -> 
-        (match do_step right with
-        | _::_ as res -> 
-            (match solved goal res Utils.Left with
-            | No newgoals -> 
-                 (match first (aux (steps - 1) L) newgoals with
-                 | Some g as success -> success
-                 | None -> None)
-            | Yes newgoal -> Some newgoal)
-        | [] -> None) 
+    try 
+      let s,_,_ =
+        Founif.unification [] m context left right CicUniv.empty_ugraph in
+      Some (bag, m,s,Equality.Exact (Equality.refl_proof uri ty left))
+    with CicUnification.UnificationFailure _ -> 
+      let solutions = 
+       unification_all env table (Equality.mk_tmp_equality 
+          (0,(Cic.Implicit None,left,right,Utils.Incomparable),m))
+      in
+      if solutions = [] then None
+      else
+        let s, e, swapped = List.hd solutions in
+        let _,p,(ty,l,r,_),me,id = Equality.open_equality e in 
+        let bag, p = 
+          if swapped then Equality.symmetric bag ty l id uri me else bag, p
+        in
+        Some (bag, m,s, p) 
   in
-  aux steps L initgoal
+  let newgoal =  
+   HExtlib.list_findopt
+     (fun (pr,mr,r) _ ->
+         try
+           let pl,ml,l,bag,m,s,p = 
+             match 
+             HExtlib.list_findopt (fun (pl,ml,l) _ -> 
+               match is_solved l r ml mr with
+               | None -> None
+               | Some (bag,m,s,p) -> Some (pl,ml,l,bag,m,s,p)
+             ) l_demod
+             with Some x -> x | _ -> raise Not_found
+           in
+           let pl = 
+             List.map 
+               (fun (rule,pos,id,subst,pred) -> 
+                 let pred = 
+                   match pred with
+                   | Cic.Lambda (name,src,tgt) ->
+                       Cic.Lambda (name,src, 
+                         Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
+                   | _ -> assert false                 
+                 in
+                 rule,pos,id,subst,pred)
+               pl
+           in
+           let pr = 
+             List.map 
+               (fun (rule,pos,id,subst,pred) -> 
+                 let pred = 
+                   match pred with
+                   | Cic.Lambda (name,src,tgt) ->
+                       Cic.Lambda (name,src, 
+                         Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
+                   | _ -> assert false                 
+                 in
+                 rule,pos,id,subst,pred)
+               pr
+           in
+           Some (bag,pr@pl@proof,m,s,p)
+         with Not_found -> None)
+     r_demod
+  in
+  newgoal
 ;;
 
-let get_stats () = "" ;;
+
+