X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=2be5da0627d07d7c390ba622ea4d692ab6751c40;hb=e8f64678cc425f19336ff4f905f9b2f00acd6627;hp=3979c052985f76f542a68ad1c409ef8cf4274a44;hpb=9135f92fe15418abd2c2ae81ab155a2517bc72ea;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 3979c0529..2be5da062 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -223,7 +223,7 @@ let open_eq_ind args = let open_pred pred = match pred with - | Cic.Lambda (_,ty,(Cic.Appl [Cic.MutInd (uri, 0,_);_;l;r])) + | Cic.Lambda (_,_,(Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r])) when LibraryObjects.is_eq_URI uri -> ty,uri,l,r | _ -> prerr_endline (CicPp.ppterm pred); assert false ;; @@ -336,15 +336,16 @@ let contextualize uri ty left right t = * 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 *) - let rec aux uri ty left right ctx_d = function + let rec aux uri ty left right ctx_d ctx_ty = function | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) when LibraryObjects.is_sym_eq_URI uri_sym -> let ty,l,r,p = open_sym ens tl in - mk_sym uri_sym ty l r (aux uri ty l r ctx_d p) + 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 rest) + Cic.LetIn (name,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 -> @@ -355,12 +356,13 @@ let contextualize uri ty left right t = let is_not_fixed_lp = is_not_fixed lp in let avoid_eq_ind = LibraryObjects.is_eq_ind_URI uri_ind in (* extract the context and the fixed term from the predicate *) - let m, ctx_c = + let m, ctx_c, ty2 = let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in (* they were under a lambda *) - let m = CicSubstitution.subst (Cic.Implicit None) m in + let m = CicSubstitution.subst hole m in let ctx_c = CicSubstitution.subst hole ctx_c in - m, ctx_c + let ty2 = CicSubstitution.subst hole ty2 in + m, ctx_c, ty2 in (* create the compound context and put the terms under it *) let ctx_dc = compose_contexts ctx_d ctx_c in @@ -373,17 +375,17 @@ let contextualize uri ty left right t = (* now put the proofs in the compound context *) let p1 = (* p1: dc_what = d_m *) if is_not_fixed_lp then - aux uri ty1 c_what m ctx_d p1 + aux uri ty2 c_what m ctx_d ctx_ty p1 else - mk_sym uri_sym ty d_m dc_what - (aux uri ty1 m c_what ctx_d p1) + mk_sym uri_sym ctx_ty d_m dc_what + (aux uri ty2 m c_what ctx_d ctx_ty p1) in let p2 = (* p2: dc_other = dc_what *) if avoid_eq_ind then - mk_sym uri_sym ty dc_what dc_other - (aux uri ty1 what other ctx_dc p2) + mk_sym uri_sym ctx_ty dc_what dc_other + (aux uri ty1 what other ctx_dc ctx_ty p2) else - aux uri ty1 other what ctx_dc p2 + aux uri ty1 other what ctx_dc ctx_ty p2 in (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m if pred = \x.m=C[x] --> t : m=C[other] --> trans m what other *) @@ -392,10 +394,11 @@ let contextualize uri ty left right t = dc_other,dc_what,d_m,p2,p1 else d_m,dc_what,dc_other, - (mk_sym uri_sym ty dc_what d_m p1), - (mk_sym uri_sym ty dc_other dc_what p2) + (mk_sym uri_sym ctx_ty dc_what d_m p1), + (mk_sym uri_sym ctx_ty dc_other dc_what p2) in - mk_trans uri_trans ty a b c paeqb pbeqc + mk_trans uri_trans ctx_ty a b c paeqb pbeqc + | t when ctx_d = hole -> t | t -> let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in @@ -406,16 +409,16 @@ let contextualize uri ty left right t = let ctx_d = CicSubstitution.lift 1 ctx_d in put_in_ctx ctx_d (Cic.Rel 1) in - let lty = CicSubstitution.lift 1 ty in + let lty = CicSubstitution.lift 1 ctx_ty in Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r)) in let d_left = put_in_ctx ctx_d left in let d_right = put_in_ctx ctx_d right in - let refl_eq = mk_refl uri ty d_left in - mk_sym uri_sym ty d_right d_left + let refl_eq = mk_refl uri ctx_ty d_left in + mk_sym uri_sym ctx_ty d_right d_left (mk_eq_ind uri_ind ty left pred refl_eq right t) in - aux uri ty left right hole t + aux uri ty left right hole ty t ;; let contextualize_rewrites t ty = @@ -729,15 +732,14 @@ let build_goal_proof l initial ty se = cic, p)) lets (letsno-1,initial) in - (proof,se) - (* canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), - se *) + canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), + se ;; let refl_proof ty term = Cic.Appl [Cic.MutConstruct - (LibraryObjects.eq_URI (), 0, 1, []); + (Utils.eq_URI (), 0, 1, []); ty; term] ;; @@ -789,6 +791,7 @@ let meta_convertibility_aux table t1 t2 = let rec aux ((table_l, table_r) as table) t1 t2 = match t1, t2 with | C.Meta (m1, tl1), C.Meta (m2, tl2) -> + let tl1, tl2 = [],[] in let m1_binding, table_l = try List.assoc m1 table_l, table_l with Not_found -> m2, (m1, m2)::table_l @@ -912,14 +915,14 @@ let meta_convertibility t1 t2 = exception TermIsNotAnEquality;; let term_is_equality term = - let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in + let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in match term with | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true | _ -> false ;; let equality_of_term proof term = - let eq_uri = LibraryObjects.eq_URI () in + let eq_uri = Utils.eq_URI () in let iseq uri = UriManager.eq uri eq_uri in match term with | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri -> @@ -951,7 +954,7 @@ let term_of_equality equality = let argsno = List.length menv in let t = CicSubstitution.lift argsno - (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right]) + (Cic.Appl [Cic.MutInd (Utils.eq_URI (), 0, []); ty; left; right]) in snd ( List.fold_right