From 9ae997cc107e7cacfe3ee62c316361257f3832d4 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 28 May 2007 13:18:32 +0000
Subject: [PATCH] Added a new version of meta_convertibnility that returns the
 variant substitution.

---
 components/tactics/paramodulation/equality.ml | 27 ++++++++++++++++++-
 .../tactics/paramodulation/equality.mli       |  2 ++
 2 files changed, 28 insertions(+), 1 deletion(-)

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 30138b378..e35918c68 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -1026,7 +1026,6 @@ let meta_convertibility_eq eq1 eq2 =
         false
 ;;
 
-
 let meta_convertibility t1 t2 =
   if t1 = t2 then
     true
@@ -1038,6 +1037,32 @@ let meta_convertibility t1 t2 =
       false
 ;;
 
+let meta_convertibility_subst t1 t2 menv =
+  if t1 = t2 then
+    Some([])
+  else
+    try
+      let (l,_) = meta_convertibility_aux ([],[]) t1 t2 in
+      let subst =
+	List.map
+	  (fun (x,y) ->
+	     try 
+	       let (_,c,t) = CicUtil.lookup_meta x menv in
+	       let irl = 
+		 CicMkImplicit.identity_relocation_list_for_metavariable c in
+	       (x,(c,Cic.Meta(y,irl),t))
+	     with CicUtil.Meta_not_found _ ->
+	       try 
+		 let (_,c,t) = CicUtil.lookup_meta y menv in
+		 let irl =  
+		   CicMkImplicit.identity_relocation_list_for_metavariable c in
+		   (y,(c,Cic.Meta(x,irl),t))
+	       with CicUtil.Meta_not_found _ -> assert false) l in   
+	Some subst
+    with NotMetaConvertible ->
+      None
+;;
+
 exception TermIsNotAnEquality;;
 
 let term_is_equality term =
diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli
index a8dec96f9..6eb48a036 100644
--- a/components/tactics/paramodulation/equality.mli
+++ b/components/tactics/paramodulation/equality.mli
@@ -116,6 +116,8 @@ val meta_convertibility: Cic.term -> Cic.term -> bool
 
 (** meta convertibility between two equations *)
 val meta_convertibility_eq: equality -> equality -> bool
+val meta_convertibility_subst: 
+  Cic.term -> Cic.term -> Cic.metasenv -> Cic.substitution option
 
 val is_weak_identity: equality -> bool
 val is_identity: Utils.environment -> equality -> bool
-- 
2.39.2