From 0e6ba9d1134a3bfe9fd4d5b4495faf0811a216df Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 30 May 2006 08:59:27 +0000
Subject: [PATCH] the function to create on the fly a symmetry step has been
 moved to equality

---
 .../tactics/paramodulation/equality.ml        | 21 ++++++++++++++++
 .../tactics/paramodulation/equality.mli       | 13 ++++++++++
 .../tactics/paramodulation/saturation.ml      | 25 ++-----------------
 3 files changed, 36 insertions(+), 23 deletions(-)

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index b5fc4543b..1708ed5b8 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -913,3 +913,24 @@ let term_of_equality equality =
       menv (argsno, t))
 ;;
 
+let symmetric eq_ty l id uri m =
+  let eq = Cic.MutInd(uri,0,[]) in
+  let pred = 
+    Cic.Lambda (Cic.Name "Sym",eq_ty,
+     Cic.Appl [CicSubstitution.lift 1 eq ;
+               CicSubstitution.lift 1 eq_ty;
+               Cic.Rel 1;CicSubstitution.lift 1 l]) 
+  in
+  let prefl = 
+    Exact (Cic.Appl
+      [Cic.MutConstruct(uri,0,1,[]);eq_ty;l]) 
+  in
+  let id1 = 
+    let eq = mk_equality (0,prefl,(eq_ty,l,l,Utils.Eq),m) in
+    let (_,_,_,_,id) = open_equality eq in
+    id
+  in
+  Step(Subst.empty_subst,
+    (Demodulation,id1,(Utils.Left,id),pred))
+;;
+
diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli
index ee90d7b6e..8c55516a9 100644
--- a/helm/software/components/tactics/paramodulation/equality.mli
+++ b/helm/software/components/tactics/paramodulation/equality.mli
@@ -93,3 +93,16 @@ val meta_convertibility_eq: equality -> equality -> bool
 
 val is_weak_identity: equality -> bool
 val is_identity: Utils.environment -> equality -> bool
+
+(* symmetric [eq_ty] [l] [id] [uri] [m] 
+ *
+ * given an equality (_,p,(_,[l],r,_),[m],[id]) of 'type' l=r
+ * returns the proof of the symmetric (r=l).
+ *
+ * [uri] is the uri of eq
+ * [eq_ty] the ty of the equality sides
+ *)
+val symmetric:
+  Cic.term -> Cic.term -> int -> UriManager.uri ->
+    Cic.metasenv -> proof
+
diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index faae7b15f..02b080147 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -882,34 +882,13 @@ let print_goals goals =
            Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
 ;;
               
-(* adds a symmetry step *)
-let symmetric pred eq eq_ty l id uri m =
-  let pred = 
-    Cic.Lambda (Cic.Name "Sym",eq_ty,
-     Cic.Appl [CicSubstitution.lift 1 eq ;
-               CicSubstitution.lift 1 eq_ty;
-               Cic.Rel 1;CicSubstitution.lift 1 l]) 
-  in
-  let prefl = 
-    Equality.Exact (Cic.Appl
-      [Cic.MutConstruct(uri,0,1,[]);eq_ty;l]) 
-  in
-  let id1 = 
-    let eq = Equality.mk_equality (0,prefl,(eq_ty,l,l,Eq),m) in
-    let (_,_,_,_,id) = Equality.open_equality eq in
-    id
-  in
-  Equality.Step(Subst.empty_subst,
-    (Equality.Demodulation,id1,(Utils.Left,id),pred))
-;;
-
 let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
 (*
   let names = names_of_context ctx in
   Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
 *)
   match ty with
-  | Cic.Appl[Cic.MutInd(uri,_,_) as eq;eq_ty;left;right] 
+  | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
     when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
       (let goal_equation = 
          Equality.mk_equality
@@ -925,7 +904,7 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
             let p =
               if pos = Utils.Left then
-                symmetric pred eq eq_ty l id uri m
+                Equality.symmetric eq_ty l id uri m
               else
                 p
             in
-- 
2.39.2