From 8dfe64de7854c787c1f226a11e7ed540b0e67d9f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Jul 2006 15:10:24 +0000 Subject: [PATCH] trans chains even inside letins body --- components/tactics/paramodulation/equality.ml | 20 +++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 2634752e7..368a80f5d 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -422,16 +422,29 @@ let mk_feq uri_feq ty ty1 left pred right t = Cic.Appl [Cic.Const(uri_feq,[]);ty;ty1;pred;left;right;t] ;; +let rec look_ahead aux = function + | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) as t + when LibraryObjects.is_eq_ind_URI uri_ind || + LibraryObjects.is_eq_ind_r_URI uri_ind -> + let ty1,what,pred,p1,other,p2 = open_eq_ind tl in + let ty2,eq,lp,rp = open_pred pred in + let hole = Cic.Implicit (Some `Hole) in + let ty2 = CicSubstitution.subst hole ty2 in + aux ty1 (CicSubstitution.subst other lp) (CicSubstitution.subst other rp) hole ty2 t + | Cic.Lambda (n,s,t) -> Cic.Lambda (n,s,look_ahead aux t) + | t -> t +;; + let contextualize uri ty left right t = let hole = Cic.Implicit (Some `Hole) in - (* aux [uri] [ty] [left] [right] [ctx] [t] + (* aux [uri] [ty] [left] [right] [ctx] [ctx_ty] [t] * * the parameters validate this invariant * t: eq(uri) ty left right * that is used only by the base case * * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context - * ty_ctx is the type of ctx_d + * ctx_ty is the type of ctx *) let rec aux uri ty left right ctx_d ctx_ty = function | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) @@ -439,8 +452,7 @@ let contextualize uri ty left right t = let ty,l,r,p = open_sym ens tl in mk_sym uri_sym ty l r (aux uri ty l r ctx_d ctx_ty p) | Cic.LetIn (name,body,rest) -> - (* we should go in body *) - Cic.LetIn (name,body,aux uri ty left right ctx_d ctx_ty rest) + Cic.LetIn (name,look_ahead (aux uri) body, aux uri ty left right ctx_d ctx_ty rest) | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) when LibraryObjects.is_eq_ind_URI uri_ind || LibraryObjects.is_eq_ind_r_URI uri_ind -> -- 2.39.2