X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=999666bca4652602566c3043c2cf4d967c8b4933;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=987c17cc83950fb00baeaff2b7825861b5081e20;hpb=d8c8060ad0cfc9b93ce919b6662383a230192840;p=helm.git

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 987c17cc8..999666bca 100644
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1,26 +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, 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
+        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 || m2_binding <> m1 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
@@ -30,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
         )
@@ -77,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 =
@@ -102,28 +164,19 @@ 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
+      let table = meta_convertibility_aux ([], []) left left' in
       let _ = meta_convertibility_aux table right right' in
-(*       Printf.printf "meta_convertibility_eq, ok:\n%s\n%s\n" *)
-(*         (string_of_equality eq1) (string_of_equality eq2); *)
-(*       print_newline (); *)
       true
     with NotMetaConvertible ->
       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
-(*         Printf.printf "meta_convertibility_eq, ok:\n%s\n%s\n" *)
-(*           (string_of_equality eq1) (string_of_equality eq2); *)
-(*         print_newline (); *)
         true
       with NotMetaConvertible ->
         false
@@ -131,18 +184,122 @@ 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" *)
@@ -394,6 +551,10 @@ 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" *)
@@ -409,19 +570,42 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
             if match_only then
               let t' = CicMetaSubst.apply_subst subst' term in
               if not (meta_convertibility term t') 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); *)
+(*                 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 e ->
-(*             print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e)); *)
+            if print_info then (
+              print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
+            );
             res, lifted_term
     in
 (*     Printf.printf "exit aux\n"; *)
@@ -455,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
 ;;
 
 
@@ -557,8 +757,17 @@ let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
            (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))
 ;;
 
 
@@ -586,14 +795,13 @@ 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 compare_terms = !Utils.compare_terms in
 
   if eq_ty <> ty then
     []
   else    
     let where, is_left =
-      match nonrec_kbo left right with
+      match compare_terms left right with
       | Lt -> right, false
       | Gt -> left, true
       | _ -> (
@@ -604,16 +812,24 @@ let superposition_left (metasenv, context, ugraph) target source =
         )
     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)
+    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
+          res1, res2
     in
     (*   let what, other = *)
     (*     if is_left then left, right *)
@@ -660,8 +876,7 @@ 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 compare_terms = !Utils.compare_terms in
 
   if eq_ty <> ty' then
     newmeta, []
@@ -676,30 +891,53 @@ let superposition_right newmeta (metasenv, context, ugraph) target source =
     (*   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
+      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 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)
+    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
     let newmetas = newmetas @ newm' in
     let newargs = args @ args' in
@@ -770,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
@@ -795,18 +1050,28 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
 (*       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; *)
-(*         print_newline (); *)
-(*         Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
-(*         print_newline (); *)
+(*         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
@@ -817,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, []);
@@ -826,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'])
@@ -834,24 +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);
-          print_newline ();
+(*           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 (); *)
           if is_identity env newtarget then
             newmeta, newtarget
           else
-            demodulate newmeta step metasenv newtarget
+            demodulate newmeta first_step metasenv newtarget
     in
-    demodulate newmeta 3 (metasenv @ metas') target
+    demodulate newmeta first_step (metasenv @ metas') target
 ;;