From 9ae997cc107e7cacfe3ee62c316361257f3832d4 Mon Sep 17 00:00:00 2001 From: Andrea Asperti 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