]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/paramodulation/inference.ml
various optimizations (to paramodulation and passive clause selection)
[helm.git] / helm / ocaml / paramodulation / inference.ml
index c4b0a842f26c163c513dfc25089736a860f872ea..999666bca4652602566c3043c2cf4d967c8b4933 100644 (file)
@@ -1,19 +1,87 @@
 open Utils;;
 
 
+let string_of_equality ?env =
+  match env with
+  | None -> (
+      function
+        | _, (ty, left, right), _, _ ->
+            Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty)
+              (CicPp.ppterm left) (CicPp.ppterm right)
+    )
+  | Some (_, context, _) -> (
+      let names = names_of_context context in
+      function
+        | _, (ty, left, right), _, _ ->
+            Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names)
+              (CicPp.pp left names) (CicPp.pp right names)
+    )
+;;
+
+
+let rec metas_of_term = function
+  | Cic.Meta (i, c) -> [i]
+  | Cic.Var (_, ens) 
+  | Cic.Const (_, ens) 
+  | Cic.MutInd (_, _, ens) 
+  | Cic.MutConstruct (_, _, _, ens) ->
+      List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
+  | Cic.Cast (s, t)
+  | Cic.Prod (_, s, t)
+  | Cic.Lambda (_, s, t)
+  | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
+  | Cic.Appl l -> List.flatten (List.map metas_of_term l)
+  | Cic.MutCase (uri, i, s, t, l) ->
+      (metas_of_term s) @ (metas_of_term t) @
+        (List.flatten (List.map metas_of_term l))
+  | Cic.Fix (i, il) ->
+      List.flatten
+        (List.map (fun (s, i, t1, t2) ->
+                     (metas_of_term t1) @ (metas_of_term t2)) il)
+  | Cic.CoFix (i, il) ->
+      List.flatten
+        (List.map (fun (s, t1, t2) ->
+                     (metas_of_term t1) @ (metas_of_term t2)) il)
+  | _ -> []
+;;      
+
+
 exception NotMetaConvertible;;
 
 let meta_convertibility_aux table t1 t2 =
   let module C = Cic in
-  let rec aux table t1 t2 =
+  let print_table t =
+    String.concat ", "
+      (List.map
+         (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
+  in
+  let rec aux ((table_l, table_r) as table) t1 t2 =
+(*     Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *)
+(*       (CicPp.ppterm t1) (CicPp.ppterm t2) *)
+(*       (print_table table_l) (print_table table_r); *)
     match t1, t2 with
-    | t1, t2 when t1 = t2 -> table
     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
-        let m1_binding, table =
-          try List.assoc m1 table, table
-          with Not_found -> m2, (m1, m2)::table
+        let m1_binding, table_l =
+          try List.assoc m1 table_l, table_l
+          with Not_found -> m2, (m1, m2)::table_l
+        and m2_binding, table_r =
+          try List.assoc m2 table_r, table_r
+          with Not_found -> m1, (m2, m1)::table_r
         in
-        if m1_binding <> m2 then
+(*         let m1_binding, m2_binding, table = *)
+(*           let m1b, table =  *)
+(*             try List.assoc m1 table, table *)
+(*             with Not_found -> m2, (m1, m2)::table *)
+(*           in *)
+(*           let m2b, table =  *)
+(*             try List.assoc m2 table, table *)
+(*             with Not_found -> m1, (m2, m1)::table *)
+(*           in *)
+(*           m1b, m2b, table *)
+(*         in *)
+(*         Printf.printf "table_l: %s\ntable_r: %s\n\n" *)
+(*           (print_table table_l) (print_table table_r); *)
+        if (m1_binding <> m2) || (m2_binding <> m1) then
           raise NotMetaConvertible
         else (
           try
@@ -23,7 +91,7 @@ let meta_convertibility_aux table t1 t2 =
                  | None, Some _ | Some _, None -> raise NotMetaConvertible
                  | None, None -> res
                  | Some t1, Some t2 -> (aux res t1 t2))
-              table tl1 tl2
+              (table_l, table_r) tl1 tl2
           with Invalid_argument _ ->
             raise NotMetaConvertible
         )
@@ -70,6 +138,7 @@ let meta_convertibility_aux table t1 t2 =
             table il1 il2
         with Invalid_argument _ -> raise NotMetaConvertible
       )
+    | t1, t2 when t1 = t2 -> table
     | _, _ -> raise NotMetaConvertible
         
   and aux_ens table ens1 ens2 =
@@ -95,26 +164,18 @@ let meta_convertibility_eq eq1 eq2 =
   and _, (ty', left', right'), _, _ = eq2 in
   if ty <> ty' then
     false
+  else if (left = left') && (right = right') then
+    true
+  else if (left = right') && (right = left') then
+    true
   else
-    let print_table t w =
-      Printf.printf "table %s is:\n" w;
-      List.iter
-        (fun (k, v) -> Printf.printf "?%d: ?%d\n" k v)
-        t;
-      print_newline ();
-    in
     try
-      let table = meta_convertibility_aux [] left left' in
-(*       print_table table "before"; *)
+      let table = meta_convertibility_aux ([], []) left left' in
       let _ = meta_convertibility_aux table right right' in
-(*       print_table table "after"; *)
       true
     with NotMetaConvertible ->
-(*       Printf.printf "NotMetaConvertible:\n%s = %s\n%s = %s\n\n" *)
-(*         (CicPp.ppterm left) (CicPp.ppterm right) *)
-(*         (CicPp.ppterm left') (CicPp.ppterm right'); *)
       try
-        let table = meta_convertibility_aux [] left right' in
+        let table = meta_convertibility_aux ([], []) left right' in
         let _ = meta_convertibility_aux table right left' in
         true
       with NotMetaConvertible ->
@@ -123,18 +184,129 @@ let meta_convertibility_eq eq1 eq2 =
 
 
 let meta_convertibility t1 t2 =
-  try
-    let _ = meta_convertibility_aux [] t1 t2 in
+  let f t =
+    String.concat ", "
+      (List.map
+         (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
+  in
+  if t1 = t2 then
     true
-  with NotMetaConvertible ->
-    false
+  else
+    try
+      let l, r = meta_convertibility_aux ([], []) t1 t2 in
+      (*     Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
+      true
+    with NotMetaConvertible ->
+      false
+;;
+
+
+let replace_metas (* context *) term =
+  let module C = Cic in
+  let rec aux = function
+    | C.Meta (i, c) ->
+(*         let irl = *)
+(*           CicMkImplicit.identity_relocation_list_for_metavariable context *)
+(*         in *)
+(*         if c = irl then *)
+(*           C.Implicit (Some (`MetaIndex i)) *)
+(*         else ( *)
+(*           Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
+(*             (String.concat "\n" *)
+(*                (List.map *)
+(*                   (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
+(*           C.Meta (i, c) *)
+(*         ) *)
+        C.Implicit (Some (`MetaInfo (i, c)))
+    | C.Var (u, ens) -> C.Var (u, aux_ens ens)
+    | C.Const (u, ens) -> C.Const (u, aux_ens ens)
+    | C.Cast (s, t) -> C.Cast (aux s, aux t)
+    | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
+    | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
+    | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
+    | C.Appl l -> C.Appl (List.map aux l)
+    | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
+    | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
+    | C.MutCase (uri, i, s, t, l) ->
+        C.MutCase (uri, i, aux s, aux t, List.map aux l)
+    | C.Fix (i, il) ->
+        let il' =
+          List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
+        C.Fix (i, il')
+    | C.CoFix (i, il) ->
+        let il' =
+          List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
+        C.CoFix (i, il')
+    | t -> t
+  and aux_ens ens =
+    List.map (fun (u, t) -> (u, aux t)) ens
+  in
+  aux term
 ;;
 
 
+let restore_metas (* context *) term =
+  let module C = Cic in
+  let rec aux = function
+    | C.Implicit (Some (`MetaInfo (i, c))) ->
+(*         let c = *)
+(*           CicMkImplicit.identity_relocation_list_for_metavariable context *)
+(*         in *)
+(*         C.Meta (i, c) *)
+(*         let local_context:(C.term option) list = *)
+(*           Marshal.from_string mc 0 *)
+(*         in *)
+(*         C.Meta (i, local_context) *)
+        C.Meta (i, c)
+    | C.Var (u, ens) -> C.Var (u, aux_ens ens)
+    | C.Const (u, ens) -> C.Const (u, aux_ens ens)
+    | C.Cast (s, t) -> C.Cast (aux s, aux t)
+    | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
+    | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
+    | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
+    | C.Appl l -> C.Appl (List.map aux l)
+    | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
+    | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
+    | C.MutCase (uri, i, s, t, l) ->
+        C.MutCase (uri, i, aux s, aux t, List.map aux l)
+    | C.Fix (i, il) ->
+        let il' =
+          List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
+        C.Fix (i, il')
+    | C.CoFix (i, il) ->
+        let il' =
+          List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
+        C.CoFix (i, il')
+    | t -> t
+  and aux_ens ens =
+    List.map (fun (u, t) -> (u, aux t)) ens
+  in
+  aux term
+;;
+
+
+let rec restore_subst (* context *) subst =
+  List.map
+    (fun (i, (c, t, ty)) ->
+       i, (c, restore_metas (* context *) t, ty))
+    subst
+;;
+
+      
 let beta_expand ?(metas_ok=true) ?(match_only=false)
     what type_of_what where context metasenv ugraph = 
   let module S = CicSubstitution in
   let module C = Cic in
+
+  let print_info = false in
+  
+(*   let _ = *)
+(*     let names = names_of_context context in *)
+(*     Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
+(*       (CicPp.pp what names) (CicPp.ppterm what) *)
+(*       (CicPp.pp where names) (CicPp.ppterm where); *)
+(*     print_newline (); *)
+(*   in *)
   (*
     return value:
     ((list of all possible beta expansions, subst, metasenv, ugraph),
@@ -379,8 +551,14 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
       | C.Meta _ when (not metas_ok) ->
           res, lifted_term
       | _ ->
+(*           let term' = *)
+(*             if match_only then replace_metas context term *)
+(*             else term *)
+(*           in *)
           try
             let subst', metasenv', ugraph' =
+(*               Printf.printf "provo a unificare %s e %s\n" *)
+(*                 (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
               CicUnification.fo_unif metasenv context
                 (S.lift lift_amount what) term ugraph
             in
@@ -390,20 +568,44 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
 (*           Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
             (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
             if match_only then
-              let term' = CicMetaSubst.apply_subst subst' term in
-              if not (meta_convertibility term term') then (
-(*                 let names = names_of_context context in *)
-(*                 Printf.printf "\nterm e term' sono diversi!:\n%s\n%s\n\n" *)
-(*                   (CicPp.pp term names) (CicPp.pp term' names); *)
+              let t' = CicMetaSubst.apply_subst subst' term in
+              if not (meta_convertibility term t') then (
+(*                 if print_info then ( *)
+(*                   let names = names_of_context context in *)
+(*                   Printf.printf *)
+(*                     "\nbeta_expand: term e t' sono diversi!:\n%s\n%s\n\n" *)
+(*                     (CicPp.pp term names) (CicPp.pp t' names) *)
+(*                 ); *)
                 res, lifted_term
-              )
-              else
+              ) else (
+                let metas = metas_of_term term in
+(*                 let ok = ref false in *)
+                let fix_subst = function
+                  | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas ->
+(*                       Printf.printf "fix_subst: scambio ?%d e ?%d\n" i j; *)
+(*                       ok := true; *)
+                      (j, (c, C.Meta (i, lc), ty))
+                  | s -> s
+                in
+                let subst' = List.map fix_subst subst' in
+(*                 if !ok then ( *)
+(*                   Printf.printf "aaa:\nterm: %s\nt'%s\n term subst': %s\n" *)
+(*                     (CicPp.ppterm term) *)
+(*                     (CicPp.ppterm t') *)
+(*                     (CicPp.ppterm (CicMetaSubst.apply_subst subst' term)) *)
+(*                 ); *)
                 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
                  lifted_term)
+              )
+(*               ((C.Rel (1 + lift_amount), restore_subst context subst', *)
+(*                 metasenv', ugraph')::res, lifted_term) *)
             else
               ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
                lifted_term)
-          with _ ->
+          with e ->
+            if print_info then (
+              print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
+            );
             res, lifted_term
     in
 (*     Printf.printf "exit aux\n"; *)
@@ -437,14 +639,30 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
       ) exp_named_subst ([], [])
 
   in
-  let expansions, _ = aux 0 where context metasenv [] ugraph in
-  List.map
-    (fun (term, subst, metasenv, ugraph) ->
-       let term' = C.Lambda (C.Anonymous, type_of_what, term) in
-(*        Printf.printf "term is: %s\nsubst is:\n%s\n\n" *)
-(*          (CicPp.ppterm term') (print_subst subst); *)
-       (term', subst, metasenv, ugraph))
-    expansions
+  let expansions, _ =
+(*     let where = *)
+(*       if match_only then replace_metas (\* context *\) where *)
+(*       else where *)
+(*     in *)
+    if print_info then (
+      Printf.printf "searching %s inside %s\n"
+        (CicPp.ppterm what) (CicPp.ppterm where);
+    );
+    aux 0 where context metasenv [] ugraph
+  in
+  let mapfun =
+(*     if match_only then *)
+(*       (fun (term, subst, metasenv, ugraph) -> *)
+(*          let term' = *)
+(*            C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
+(*          and subst = restore_subst subst in *)
+(*          (term', subst, metasenv, ugraph)) *)
+(*     else *)
+      (fun (term, subst, metasenv, ugraph) ->
+         let term' = C.Lambda (C.Anonymous, type_of_what, term) in
+         (term', subst, metasenv, ugraph))
+  in
+  List.map mapfun expansions
 ;;
 
 
@@ -514,11 +732,14 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
 
 
 let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
+  let table = Hashtbl.create (List.length args) in
   let newargs, _ =
     List.fold_right
       (fun t (newargs, index) ->
          match t with
-         | Cic.Meta (i, l) -> ((Cic.Meta (index, l))::newargs, index+1)
+         | Cic.Meta (i, l) ->
+             Hashtbl.add table i index;
+             ((Cic.Meta (index, l))::newargs, index+1)
          | _ -> assert false)
       args ([], newmeta)
   in
@@ -526,14 +747,27 @@ let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
       ~where
   in
-  let menv', _ =
+  let menv' =
     List.fold_right
-      (fun (i, context, term) (menv, index) ->
-         ((index, context, term)::menv, index+1))
-      menv ([], newmeta)
+      (fun (i, context, term) menv ->
+         try
+           let index = Hashtbl.find table i in
+           (index, context, term)::menv
+         with Not_found ->
+           (i, context, term)::menv)
+      menv []
+  in
+  let ty = repl ty
+  and left = repl left
+  and right = repl right in
+  let metas = (metas_of_term left) @ (metas_of_term right) in
+  let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv'
+  and newargs =
+    List.filter
+      (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
   in
   (newmeta + (List.length newargs) + 1,
-   (repl proof, (repl ty, repl left, repl right), menv', newargs))
+   (repl proof, (ty, left, right), menv', newargs))
 ;;
 
 
@@ -561,63 +795,74 @@ let superposition_left (metasenv, context, ugraph) target source =
   let proof, (eq_ty, left, right), _, _ = target in
   let eqproof, (ty, t1, t2), newmetas, args = source in
 
-  (* ALB: TODO check that ty and eq_ty are indeed equal... *)
-  assert (eq_ty = ty);
-  
-  let where, is_left =
-    match nonrec_kbo left right with
-    | Lt -> right, false
-    | Gt -> left, true
-    | _ -> (
-        Printf.printf "????????? %s = %s" (CicPp.ppterm left)
-          (CicPp.ppterm right);
-        print_newline ();
-        assert false (* again, for ground terms this shouldn't happen... *)
-      )
-  in
-  let metasenv' = newmetas @ metasenv in
-  let res1 =
-    List.filter
-      (fun (t, s, m, ug) ->
-         nonrec_kbo (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
-      (beta_expand t1 ty where context metasenv' ugraph)
-  and res2 =
-    List.filter
-      (fun (t, s, m, ug) ->
-         nonrec_kbo (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
-      (beta_expand t2 ty where context metasenv' ugraph)
-  in
-(*   let what, other = *)
-(*     if is_left then left, right *)
-(*     else right, left *)
-(*   in *)
-  let build_new what other eq_URI (t, s, m, ug) =
-    let newgoal, newgoalproof =
-      match t with
-      | C.Lambda (nn, ty, bo) ->
-          let bo' = S.subst (M.apply_subst s other) bo in
-          let bo'' =
-            C.Appl (
-              [C.MutInd (HL.Logic.eq_URI, 0, []);
-               S.lift 1 eq_ty] @
-                if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo'])
+  let compare_terms = !Utils.compare_terms in
+
+  if eq_ty <> ty then
+    []
+  else    
+    let where, is_left =
+      match compare_terms left right with
+      | Lt -> right, false
+      | Gt -> left, true
+      | _ -> (
+          Printf.printf "????????? %s = %s" (CicPp.ppterm left)
+            (CicPp.ppterm right);
+          print_newline ();
+          assert false (* again, for ground terms this shouldn't happen... *)
+        )
+    in
+    let metasenv' = newmetas @ metasenv in
+    let result = compare_terms t1 t2 in
+    let res1, res2 = 
+      match result with
+      | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
+      | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
+      | _ ->
+          let res1 =
+            List.filter
+              (fun (t, s, m, ug) ->
+                 compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
+              (beta_expand t1 ty where context metasenv' ugraph)
+          and res2 =
+            List.filter
+              (fun (t, s, m, ug) ->
+                 compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
+              (beta_expand t2 ty where context metasenv' ugraph)
           in
-          let t' = C.Lambda (nn, ty, bo'') in
-          S.subst (M.apply_subst s other) bo,
-          M.apply_subst s
-            (C.Appl [C.Const (eq_URI, []); ty; what; t';
-                     proof; other; eqproof])
-      | _ -> assert false
+          res1, res2
     in
-    let equation =
-      if is_left then (eq_ty, newgoal, right)
-      else (eq_ty, left, newgoal)
+    (*   let what, other = *)
+    (*     if is_left then left, right *)
+    (*     else right, left *)
+    (*   in *)
+    let build_new what other eq_URI (t, s, m, ug) =
+      let newgoal, newgoalproof =
+        match t with
+        | C.Lambda (nn, ty, bo) ->
+            let bo' = S.subst (M.apply_subst s other) bo in
+            let bo'' =
+              C.Appl (
+                [C.MutInd (HL.Logic.eq_URI, 0, []);
+                 S.lift 1 eq_ty] @
+                  if is_left then [bo'; S.lift 1 right]
+                  else [S.lift 1 left; bo'])
+            in
+            let t' = C.Lambda (nn, ty, bo'') in
+            S.subst (M.apply_subst s other) bo,
+            M.apply_subst s
+              (C.Appl [C.Const (eq_URI, []); ty; what; t';
+                       proof; other; eqproof])
+        | _ -> assert false
+      in
+      let equation =
+        if is_left then (eq_ty, newgoal, right)
+        else (eq_ty, left, newgoal)
+      in
+      (eqproof, equation, [], [])
     in
-    (eqproof, equation, [], [])
-  in
-  let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
-  and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
-  new1 @ new2
+    let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
+    and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
+    new1 @ new2
 ;;
 
 
@@ -631,85 +876,126 @@ let superposition_right newmeta (metasenv, context, ugraph) target source =
   let eqp', (ty', t1, t2), newm', args' = source in
   let maxmeta = ref newmeta in
 
-  (* TODO check if ty and ty' are equal... *)
-  assert (eq_ty = ty');
-  
-(*   let ok term subst other other_eq_side ugraph = *)
-(*     match term with *)
-(*     | C.Lambda (nn, ty, bo) -> *)
-(*         let bo' = S.subst (M.apply_subst subst other) bo in *)
-(*         let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
-(*         not res *)
-(*     |  _ -> assert false *)
-(*   in *)
-  let condition left right what other (t, s, m, ug) =
-    let subst = M.apply_subst s in
-    let cmp1 = nonrec_kbo (subst what) (subst other) in
-    let cmp2 = nonrec_kbo (subst left) (subst right) in
-(*     cmp1 = Gt && cmp2 = Gt *)
-    cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
-(*     && (ok t s other right ug) *)
-  in
-  let metasenv' = metasenv @ newmetas @ newm' in
-  let beta_expand = beta_expand ~metas_ok:false in
-  let res1 =
-    List.filter
-      (condition left right t1 t2)
-      (beta_expand t1 eq_ty left context metasenv' ugraph)
-  and res2 =
-    List.filter
-      (condition left right t2 t1)
-      (beta_expand t2 eq_ty left context metasenv' ugraph)
-  and res3 =
-    List.filter
-      (condition right left t1 t2)
-      (beta_expand t1 eq_ty right context metasenv' ugraph)
-  and res4 =
-    List.filter
-      (condition right left t2 t1)
-      (beta_expand t2 eq_ty right context metasenv' ugraph)
-  in
-  let newmetas = newmetas @ newm' in
-  let newargs = args @ args' in
-  let build_new what other is_left eq_URI (t, s, m, ug) =
-(*     let what, other = *)
-(*       if is_left then left, right *)
-(*       else right, left *)
-(*     in *)
-    let newterm, neweqproof =
-      match t with
-      | C.Lambda (nn, ty, bo) ->
-          let bo' = M.apply_subst s (S.subst other bo) in
-          let bo'' =
-            C.Appl (
-              [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
-                if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo'])
-          in
-          let t' = C.Lambda (nn, ty, bo'') in
-          bo',
-          M.apply_subst s
-            (C.Appl [C.Const (eq_URI, []); ty; what; t'; eqproof; other; eqp'])
-      | _ -> assert false
+  let compare_terms = !Utils.compare_terms in
+
+  if eq_ty <> ty' then
+    newmeta, []
+  else
+    (*   let ok term subst other other_eq_side ugraph = *)
+    (*     match term with *)
+    (*     | C.Lambda (nn, ty, bo) -> *)
+    (*         let bo' = S.subst (M.apply_subst subst other) bo in *)
+    (*         let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
+    (*         not res *)
+    (*     |  _ -> assert false *)
+    (*   in *)
+    let condition left right what other (t, s, m, ug) =
+      let subst = M.apply_subst s in
+      let cmp1 = compare_terms (subst what) (subst other) in
+      let cmp2 = compare_terms (subst left) (subst right) in
+      (*     cmp1 = Gt && cmp2 = Gt *)
+      cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
+        (*     && (ok t s other right ug) *)
     in
-    let newmeta, newequality =
-      let left, right =
-        if is_left then (newterm, M.apply_subst s right)
-        else (M.apply_subst s left, newterm) in
-      fix_metas !maxmeta
-        (neweqproof, (eq_ty, left, right), newmetas, newargs)
+    let metasenv' = metasenv @ newmetas @ newm' in
+    let beta_expand = beta_expand ~metas_ok:false in
+    let cmp1 = compare_terms left right
+    and cmp2 = compare_terms t1 t2 in
+    let res1, res2, res3, res4 =
+      let res l r s t =
+        List.filter
+          (condition l r s t)
+          (beta_expand s eq_ty l context metasenv' ugraph)
+      in
+      match cmp1, cmp2 with
+      | Gt, Gt ->
+          (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
+      | Gt, Lt ->
+          [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
+      | Lt, Gt ->
+          [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
+      | Lt, Lt ->
+          [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
+      | Gt, _ ->
+          let res1 = res left right t1 t2
+          and res2 = res left right t2 t1 in
+          res1, res2, [], []
+      | Lt, _ ->
+          let res3 = res right left t1 t2
+          and res4 = res right left t2 t1 in
+          [], [], res3, res4
+      | _, Gt ->
+          let res1 = res left right t1 t2
+          and res3 = res right left t1 t2 in
+          res1, [], res3, []
+      | _, Lt ->
+          let res2 = res left right t2 t1
+          and res4 = res right left t2 t1 in
+          [], res2, [], res4
+      | _, _ ->
+          let res1 = res left right t1 t2
+          and res2 = res left right t2 t1
+          and res3 = res right left t1 t2
+          and res4 = res right left t2 t1 in
+          res1, res2, res3, res4
     in
-    maxmeta := newmeta;
-    newequality
-  in
-  let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
-  and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
-  and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
-  and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
-  let ok = function
-    | _, (_, left, right), _, _ ->
-        not (fst (CR.are_convertible context left right ugraph))
-  in
-  !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))
+    let newmetas = newmetas @ newm' in
+    let newargs = args @ args' in
+    let build_new what other is_left eq_URI (t, s, m, ug) =
+      (*     let what, other = *)
+      (*       if is_left then left, right *)
+      (*       else right, left *)
+      (*     in *)
+      let newterm, neweqproof =
+        match t with
+        | C.Lambda (nn, ty, bo) ->
+            let bo' = M.apply_subst s (S.subst other bo) in
+            let bo'' =
+              C.Appl (
+                [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
+                  if is_left then [bo'; S.lift 1 right]
+                  else [S.lift 1 left; bo'])
+            in
+            let t' = C.Lambda (nn, ty, bo'') in
+            bo',
+            M.apply_subst s
+              (C.Appl [C.Const (eq_URI, []); ty; what; t';
+                       eqproof; other; eqp'])
+        | _ -> assert false
+      in
+      let newmeta, newequality =
+        let left, right =
+          if is_left then (newterm, M.apply_subst s right)
+          else (M.apply_subst s left, newterm) in
+        fix_metas !maxmeta
+          (neweqproof, (eq_ty, left, right), newmetas, newargs)
+      in
+      maxmeta := newmeta;
+      newequality
+    in
+    let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
+    and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
+    and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
+    and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
+    let ok = function
+      | _, (_, left, right), _, _ ->
+          not (fst (CR.are_convertible context left right ugraph))
+    in
+    !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))
+;;
+
+
+let is_identity ((_, context, ugraph) as env) = function
+  | ((_, (ty, left, right), _, _) as equality) ->
+      let res =
+        (left = right ||
+            (fst (CicReduction.are_convertible context left right ugraph)))
+      in
+(*       if res then ( *)
+(*         Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
+(*         print_newline (); *)
+(*       ); *)
+      res
 ;;
 
 
@@ -722,16 +1008,33 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
 
   let proof, (eq_ty, left, right), metas, args = target
   and proof', (ty, t1, t2), metas', args' = source in
+
+  let compare_terms = !Utils.compare_terms in
+  
   if eq_ty <> ty then
     newmeta, target
   else
-    let get_params step =
-      match step with
-      | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
-      | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
-      | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
-      | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
-      | _ -> assert false
+    let first_step, get_params = 
+      match compare_terms t1 t2 with
+      | Gt -> 1, (function
+                    | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
+                    | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
+                    | _ -> assert false)
+      | Lt -> 1, (function
+                    | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
+                    | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
+                    | _ -> assert false)
+      | _ ->
+          let first_step = 3 in
+          let get_params step =
+            match step with
+            | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
+            | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
+            | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
+            | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
+            | _ -> assert false
+          in
+          first_step, get_params
     in
     let rec demodulate newmeta step metasenv target =
       let proof, (eq_ty, left, right), metas, args = target in
@@ -743,19 +1046,32 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
 (*         "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
 (*         (string_of_equality ~env target) (CicPp.pp what names) *)
 (*         (CicPp.pp other names) (string_of_bool is_left); *)
-(*       Printf.printf "step: %d\n" step; *)
+(*       Printf.printf "step: %d" step; *)
 (*       print_newline (); *)
 
       let ok (t, s, m, ug) =
-        nonrec_kbo (M.apply_subst s what) (M.apply_subst s other) = Gt
+        compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
       in
       let res =
         let r = (beta_expand ~metas_ok:false ~match_only:true
                    what ty (if is_left then left else right)
                    context (metasenv @ metas) ugraph) 
         in
-(*         print_endline "res:"; *)
-(*         List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
+(*         let m' = metas_of_term what *)
+(*         and m'' = metas_of_term (if is_left then left else right) in *)
+(*         if (List.mem 527 m'') && (List.mem 6 m') then ( *)
+(*           Printf.printf *)
+(*             "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
+(*             (string_of_equality ~env target) (CicPp.pp what names) *)
+(*             (CicPp.pp other names) (string_of_bool is_left); *)
+(*           Printf.printf "step: %d" step; *)
+(*           print_newline (); *)
+(*           print_endline "res:"; *)
+(*           List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
+(*           print_newline (); *)
+(*           Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
+(*           print_newline (); *)
+(*         ); *)
         List.filter ok r
       in
       match res with
@@ -766,7 +1082,8 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
           let newterm, newproof =
             match t with
             | C.Lambda (nn, ty, bo) ->
-                let bo' = M.apply_subst s (S.subst other bo) in
+(*                 let bo' = M.apply_subst s (S.subst other bo) in *)
+                let bo' = S.subst (M.apply_subst s other) bo in
                 let bo'' =
                   C.Appl (
                     [C.MutInd (HL.Logic.eq_URI, 0, []);
@@ -775,7 +1092,8 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
                       else [S.lift 1 left; bo'])
                 in
                 let t' = C.Lambda (nn, ty, bo'') in
-                M.apply_subst s (S.subst other bo),
+(*                 M.apply_subst s (S.subst other bo), *)
+                bo', 
                 M.apply_subst s
                   (C.Appl [C.Const (eq_URI, []); ty; what; t';
                            proof; other; proof'])
@@ -783,21 +1101,39 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
           in
           let newmeta, newtarget =
             let left, right =
-              if is_left then (newterm, M.apply_subst s right)
-              else (M.apply_subst s left, newterm) in
-            let newmetasenv = metasenv @ metas in
-            let newargs = args @ args' in
-            fix_metas newmeta
-              (newproof, (eq_ty, left, right), newmetasenv, newargs)
+(*               if is_left then (newterm, M.apply_subst s right) *)
+(*               else (M.apply_subst s left, newterm) in *)
+              if is_left then newterm, right
+              else left, newterm
+            in
+(*             let newmetasenv = metasenv @ metas in *)
+(*             let newargs = args @ args' in *)
+(*             fix_metas newmeta *)
+(*               (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
+            let m = (metas_of_term left) @ (metas_of_term right) in
+            let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
+            and newargs =
+              List.filter
+                (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
+                args
+            in
+            newmeta, (newproof, (eq_ty, left, right), newmetasenv, newargs)
           in
 (*           Printf.printf *)
 (*             "demodulate, newtarget: %s\ntarget was: %s\n" *)
 (*             (string_of_equality ~env newtarget) *)
 (*             (string_of_equality ~env target); *)
+(* (\*           let _, _, newm, newa = newtarget in *\) *)
+(* (\*           Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
+(* (\*             (print_metasenv newm) *\) *)
+(* (\*             (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
 (*           print_newline (); *)
-          demodulate newmeta step metasenv newtarget
+          if is_identity env newtarget then
+            newmeta, newtarget
+          else
+            demodulate newmeta first_step metasenv newtarget
     in
-    demodulate newmeta 3 (metasenv @ metas') target
+    demodulate newmeta first_step (metasenv @ metas') target
 ;;