From 78f2fb8fcf0bbd2521b67e4366b734ad88ebdc68 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 16 Apr 2007 21:15:44 +0000 Subject: [PATCH] simplify has a brand new semantics! replace_lifting passes a context to the comparison function (but in the case Fix/CoFix is incomplete) --- components/tactics/inversion.ml | 6 +- components/tactics/paramodulation/equality.ml | 7 +- components/tactics/primitiveTactics.ml | 3 +- components/tactics/proofEngineReduction.ml | 396 ++++++++++++------ components/tactics/proofEngineReduction.mli | 3 +- 5 files changed, 281 insertions(+), 134 deletions(-) diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml index 5f8a9a37f..5f90c45eb 100644 --- a/components/tactics/inversion.ml +++ b/components/tactics/inversion.ml @@ -123,7 +123,8 @@ let rec foo_prod nright right_param_tys rightparameters l2 base_rel goalty (CicSubstitution.lift 1 termty) isSetType (CicSubstitution.lift 1 term)) | [] -> ProofEngineReduction.replace_lifting - ~equality:(CicUtil.alpha_equivalence) + ~equality:(fun _ -> CicUtil.alpha_equivalence) + ~context:[] ~what: (if isSetType then (rightparameters_ @ [term] ) else (rightparameters_ ) ) @@ -151,7 +152,8 @@ let rec foo_lambda nright right_param_tys nright_ right_param_tys_ | [] when isSetType -> Cic.Lambda ( (Cic.Name ("lambda" ^ (string_of_int nright))), (ProofEngineReduction.replace_lifting - ~equality:(CicUtil.alpha_equivalence) + ~equality:(fun _ -> CicUtil.alpha_equivalence) + ~context:[] ~what: (rightparameters_ ) ~with_what: (List.map (CicSubstitution.lift (-1)) created_vars) ~where:termty), (* type of H with replaced right parameters *) diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index fcb4586cb..d9e16a255 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -371,12 +371,12 @@ prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI"); let compose_contexts ctx1 ctx2 = ProofEngineReduction.replace_lifting - ~equality:(=) ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1 + ~equality:(fun _ ->(=)) ~context:[] ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1 ;; let put_in_ctx ctx t = ProofEngineReduction.replace_lifting - ~equality:(=) ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx + ~equality:(fun _ -> (=)) ~context:[] ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx ;; let mk_eq uri ty l r = @@ -581,8 +581,9 @@ let parametrize_proof p l r = let p = CicSubstitution.lift (lift_no-1) p in let p = ProofEngineReduction.replace_lifting - ~equality:(fun t1 t2 -> + ~equality:(fun _ t1 t2 -> match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) + ~context:[] ~what ~with_what ~where:p in let ty_of_m _ = Cic.Implicit (Some `Type) in diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 50626aff0..cc16c2030 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -715,8 +715,9 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam in let replaced = ref false in let replace = ProofEngineReduction.replace_lifting - ~equality:(fun a b -> let rc = CicUtil.alpha_equivalence a b in + ~equality:(fun _ a b -> let rc = CicUtil.alpha_equivalence a b in if rc then replaced := true; rc) + ~context:[] in let captured = replace ~what:[CicSubstitution.lift n_lambdas term] diff --git a/components/tactics/proofEngineReduction.ml b/components/tactics/proofEngineReduction.ml index b55b92b93..ec6907436 100644 --- a/components/tactics/proofEngineReduction.ml +++ b/components/tactics/proofEngineReduction.ml @@ -49,6 +49,11 @@ exception RelToHiddenHypothesis;; module C = Cic module S = CicSubstitution +let debug = false +let prerr_endline = + if debug then prerr_endline else (fun x -> ()) +;; + exception WhatAndWithWhatDoNotHaveTheSameLength;; (* Replaces "textually" in "where" every term in "what" with the corresponding @@ -122,26 +127,28 @@ let replace ~equality ~what ~with_what ~where = Thus "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]" is the inverse of subst up to the fact that free variables in "where" are NOT lifted. *) -let replace_lifting ~equality ~what ~with_what ~where = - let find_image what t = +let replace_lifting ~equality ~context ~what ~with_what ~where = + let find_image ctx what t = let rec find_image_aux = function [],[] -> raise Not_found | what::tl1,with_what::tl2 -> - if equality what t then with_what else find_image_aux (tl1,tl2) + if equality ctx what t then with_what else find_image_aux (tl1,tl2) | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength in find_image_aux (what,with_what) in - let rec substaux k what t = + let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in + let add_ctx1 ctx n s = (Some (n, Cic.Def (s,None)))::ctx in + let rec substaux k ctx what t = try - S.lift (k-1) (find_image what t) + S.lift (k-1) (find_image ctx what t) with Not_found -> match t with C.Rel n as t -> t | C.Var (uri,exp_named_subst) -> let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst + List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst in C.Var (uri,exp_named_subst') | C.Meta (i, l) -> @@ -149,56 +156,56 @@ let replace_lifting ~equality ~what ~with_what ~where = List.map (function None -> None - | Some t -> Some (substaux k what t) + | Some t -> Some (substaux k ctx what t) ) l in C.Meta(i,l') | C.Sort _ as t -> t | C.Implicit _ as t -> t - | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty) + | C.Cast (te,ty) -> C.Cast (substaux k ctx what te, substaux k ctx what ty) | C.Prod (n,s,t) -> C.Prod - (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t) + (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t) | C.Lambda (n,s,t) -> C.Lambda - (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t) + (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t) | C.LetIn (n,s,t) -> C.LetIn - (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t) + (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (List.map (S.lift 1) what) t) | C.Appl (he::tl) -> (* Invariant: no Appl applied to another Appl *) - let tl' = List.map (substaux k what) tl in + let tl' = List.map (substaux k ctx what) tl in begin - match substaux k what he with + match substaux k ctx what he with C.Appl l -> C.Appl (l@tl') | _ as he' -> C.Appl (he'::tl') end | C.Appl _ -> assert false | C.Const (uri,exp_named_subst) -> let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst + List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst in C.Const (uri,exp_named_subst') | C.MutInd (uri,i,exp_named_subst) -> let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst + List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst in C.MutInd (uri,i,exp_named_subst') | C.MutConstruct (uri,i,j,exp_named_subst) -> let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst + List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst in C.MutConstruct (uri,i,j,exp_named_subst') | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,i,substaux k what outt, substaux k what t, - List.map (substaux k what) pl) + C.MutCase (sp,i,substaux k ctx what outt, substaux k ctx what t, + List.map (substaux k ctx what) pl) | C.Fix (i,fl) -> let len = List.length fl in let substitutedfl = List.map - (fun (name,i,ty,bo) -> - (name, i, substaux k what ty, - substaux (k+len) (List.map (S.lift len) what) bo) + (fun (name,i,ty,bo) -> (* WRONG CTX *) + (name, i, substaux k ctx what ty, + substaux (k+len) ctx (List.map (S.lift len) what) bo) ) fl in C.Fix (i, substitutedfl) @@ -206,14 +213,14 @@ let replace_lifting ~equality ~what ~with_what ~where = let len = List.length fl in let substitutedfl = List.map - (fun (name,ty,bo) -> - (name, substaux k what ty, - substaux (k+len) (List.map (S.lift len) what) bo) + (fun (name,ty,bo) -> (* WRONG CTX *) + (name, substaux k ctx what ty, + substaux (k+len) ctx (List.map (S.lift len) what) bo) ) fl in C.CoFix (i, substitutedfl) in - substaux 1 what where + substaux 1 context what where ;; (* Replaces in "where" every term in "what" with the corresponding @@ -228,7 +235,7 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where = function [],[] -> raise Not_found | what::tl1,with_what::tl2 -> - if equality what t then with_what else find_image_aux (tl1,tl2) + if equality what t then with_what else find_image_aux (tl1,tl2) | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength in find_image_aux (what,with_what) @@ -521,7 +528,7 @@ let reduce context = (fun (types,len) (n,_,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl in let t' () = let fl' = @@ -563,7 +570,7 @@ let reduce context = (fun (types,len) (n,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl in let t' = let fl' = @@ -581,6 +588,94 @@ let reduce context = reduceaux context [] ;; + +let unfold ?what context where = + let contextlen = List.length context in + let first_is_the_expandable_head_of_second context' t1 t2 = + match t1,t2 with + Cic.Const (uri,_), Cic.Const (uri',_) + | Cic.Var (uri,_), Cic.Var (uri',_) + | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_) + | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri' + | Cic.Const _, _ + | Cic.Var _, _ -> false + | Cic.Rel n, Cic.Rel m + | Cic.Rel n, Cic.Appl (Cic.Rel m::_) -> + n + (List.length context' - contextlen) = m + | Cic.Rel _, _ -> false + | _,_ -> + raise + (ProofEngineTypes.Fail + (lazy "The term to unfold is not a constant, a variable or a bound variable ")) + in + let appl he tl = + if tl = [] then he else Cic.Appl (he::tl) in + let cannot_delta_expand t = + raise + (ProofEngineTypes.Fail + (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in + let rec hd_delta_beta context tl = + function + Cic.Rel n as t -> + (try + match List.nth context (n-1) with + Some (_,Cic.Decl _) -> cannot_delta_expand t + | Some (_,Cic.Def (bo,_)) -> + CicReduction.head_beta_reduce + (appl (CicSubstitution.lift n bo) tl) + | None -> raise RelToHiddenHypothesis + with + Failure _ -> assert false) + | Cic.Const (uri,exp_named_subst) as t -> + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + (match o with + Cic.Constant (_,Some body,_,_,_) -> + CicReduction.head_beta_reduce + (appl (CicSubstitution.subst_vars exp_named_subst body) tl) + | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t + | Cic.Variable _ -> raise ReferenceToVariable + | Cic.CurrentProof _ -> raise ReferenceToCurrentProof + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + | Cic.Var (uri,exp_named_subst) as t -> + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + (match o with + Cic.Constant _ -> raise ReferenceToConstant + | Cic.CurrentProof _ -> raise ReferenceToCurrentProof + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + | Cic.Variable (_,Some body,_,_,_) -> + CicReduction.head_beta_reduce + (appl (CicSubstitution.subst_vars exp_named_subst body) tl) + | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t + ) + | Cic.Appl [] -> assert false + | Cic.Appl (he::tl) -> hd_delta_beta context tl he + | t -> cannot_delta_expand t + in + let context_and_matched_term_list = + match what with + None -> [context, where] + | Some what -> + let res = + ProofEngineHelpers.locate_in_term + ~equality:first_is_the_expandable_head_of_second + what ~where context + in + if res = [] then + raise + (ProofEngineTypes.Fail + (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))) + else + res + in + let reduced_terms = + List.map + (function (context,where) -> hd_delta_beta context [] where) + context_and_matched_term_list in + let whats = List.map snd context_and_matched_term_list in + replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where +;; + exception WrongShape;; exception AlreadySimplified;; @@ -761,7 +856,7 @@ let simpl context = (fun (types,len) (n,_,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl in let t' () = let fl' = @@ -803,7 +898,7 @@ let simpl context = (fun (types,len) (n,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl in let t' = let fl' = @@ -818,6 +913,15 @@ let simpl context = and reduceaux_exp_named_subst context l = List.map (function uri,t -> uri,reduceaux context [] t) (**** Step 2 ****) + and reduce_with_no_hope_to_fold_back t l = + prerr_endline "reduce_with_no_hope_to_fold_back"; + let simplified = reduceaux context l t in + let t' = if l = [] then t else C.Appl (t::l) in + if t' = simplified then + raise AlreadySimplified + else + simplified + and try_delta_expansion context l term body = try let res,constant_args = @@ -871,28 +975,153 @@ let simpl context = let simplified_term_to_fold = reduceaux context [] delta_expanded_term_to_fold in - replace_lifting (=) [simplified_term_to_fold] [term_to_fold] res + replace_lifting ~equality:(fun _ x y -> x = y) ~context + ~what:[simplified_term_to_fold] ~with_what:[term_to_fold] ~where:res with WrongShape -> + let rec skip_lambda n = function + | Cic.Lambda (_,_,t) -> skip_lambda (n+1) t | t -> t, n + in + let is_fix uri = + match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with + | Cic.Constant (_,Some bo, _, _,_) -> + (let t, _ = skip_lambda 0 bo in + match t with | Cic.Fix _ -> true | _ -> false) + | _ -> false + in + let guess_recno uri = + prerr_endline ("GUESS: " ^ UriManager.string_of_uri uri); + match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with + | Cic.Constant (_,Some bo, _, _,_ ) -> + let t, n = skip_lambda 0 bo in + (match t with + | Cic.Fix (i,fl) -> + let _,recno,_,_ = List.nth fl i in + prerr_endline ("GUESSED: " ^ string_of_int recno ^ " after " ^ + string_of_int n ^ " lambdas"); + recno + n + | _ -> assert false) + | _ -> assert false + in + let original_args = l in (**** Step 3.2 ****) let rec aux l = function - C.Lambda (name,s,t) -> + | C.Lambda (name,s,t) -> (match l with - [] -> raise AlreadySimplified + | [] -> raise AlreadySimplified | he::tl -> (* when name is Anonimous the substitution should *) (* be superfluous *) aux tl (S.subst he t)) | C.LetIn (_,s,t) -> aux l (S.subst s t) - | t -> - let simplified = reduceaux context l t in - let t' = if l = [] then t else C.Appl (t::l) in - if t' = simplified then - raise AlreadySimplified + | Cic.Appl (Cic.Const (uri,_) :: args) as t when is_fix uri -> + let recno = + prerr_endline ("cerco : " ^ string_of_int (guess_recno uri) + ^ " in: " ^ String.concat " " + (List.map (fun x -> CicPp.ppterm x) args)); + prerr_endline ("e piglio il rispettivo in :"^String.concat " " + (List.map (fun x -> CicPp.ppterm x) original_args)); + (* look for args[regno] in saved_args *) + let wanted = List.nth args (guess_recno uri) in (* args@l ? *) + let rec aux n = function + | [] -> n (* DA CAPIRE *) + | t::_ when t = wanted -> n + | _::tl -> aux (n+1) tl + in + aux 0 original_args + in + if recno = List.length original_args then + reduce_with_no_hope_to_fold_back t l else - simplified - in + let simplified = reduceaux context l t in + let rec mk_implicits = function + | n,_::tl when n = recno -> + Cic.Implicit None :: (mk_implicits (n+1,tl)) + | n,arg::tl -> arg :: (mk_implicits (n+1,tl)) + | _,[] -> [] + in + (* we try to fold back constant that do not expand to Fix *) + let _ = prerr_endline + ("INIZIO (" ^ string_of_int recno ^ ") : " ^ CicPp.ppterm + simplified) in + let term_to_fold = + Cic.Appl (term:: mk_implicits (0,original_args)) + in + (try + let term_to_fold, _, metasenv, _ = + CicRefine.type_of_aux' [] context term_to_fold + CicUniv.oblivion_ugraph + in + let _ = + prerr_endline ("RAFFINA: "^CicPp.ppterm term_to_fold) in + let _ = + prerr_endline + ("RAFFINA: "^CicMetaSubst.ppmetasenv [] metasenv) in + let simplified_term_to_fold = unfold context term_to_fold in + let _ = + prerr_endline ("SEMPLIFICA: " ^ + CicPp.ppterm simplified_term_to_fold) + in + let rec do_n f t = + let t1 = f t in + if t1 = t then t else do_n f t1 + in + do_n + (fun simplified -> + let subst = ref [] in + let myunif ctx t1 t2 = + if !subst <> [] then false + else + try + prerr_endline "MUNIF"; + prerr_endline (CicPp.ppterm t1); + prerr_endline "VS"; + prerr_endline (CicPp.ppterm t2 ^ "\n"); + let subst1, _, _ = + CicUnification.fo_unif metasenv ctx t1 t2 + CicUniv.empty_ugraph + in + prerr_endline "UNIFICANO\n\n\n"; + subst := subst1; + true + with + | CicUnification.UnificationFailure s + | CicUnification.Uncertain s + | CicUnification.AssertFailure s -> + prerr_endline (Lazy.force s); false + | CicUtil.Meta_not_found _ -> false + (* + | _ as exn -> + prerr_endline (Printexc.to_string exn); + false*) + in + let t = + replace_lifting myunif context + [simplified_term_to_fold] [term_to_fold] simplified + in + let _ = prerr_endline "UNIFICA" in + if List.length metasenv <> List.length !subst then + let _ = prerr_endline ("SUBST CORTA " ^ + CicMetaSubst.ppsubst !subst ~metasenv) + in + simplified + else + if t = simplified then + let _ = prerr_endline "NULLA DI FATTO" in + simplified + else + let t = CicMetaSubst.apply_subst !subst t in + prerr_endline ("ECCO: " ^ CicPp.ppterm t); t) + simplified + with + | CicRefine.RefineFailure s + | CicRefine.Uncertain s + | CicRefine.AssertFailure s -> + prerr_endline (Lazy.force s); simplified + (*| exn -> prerr_endline (Printexc.to_string exn); simplified*)) + | t -> reduce_with_no_hope_to_fold_back t l + in (try aux l body with AlreadySimplified -> @@ -905,90 +1134,3 @@ let simpl context = in reduceaux context [] ;; - -let unfold ?what context where = - let contextlen = List.length context in - let first_is_the_expandable_head_of_second context' t1 t2 = - match t1,t2 with - Cic.Const (uri,_), Cic.Const (uri',_) - | Cic.Var (uri,_), Cic.Var (uri',_) - | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_) - | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri' - | Cic.Const _, _ - | Cic.Var _, _ -> false - | Cic.Rel n, Cic.Rel m - | Cic.Rel n, Cic.Appl (Cic.Rel m::_) -> - n + (List.length context' - contextlen) = m - | Cic.Rel _, _ -> false - | _,_ -> - raise - (ProofEngineTypes.Fail - (lazy "The term to unfold is not a constant, a variable or a bound variable ")) - in - let appl he tl = - if tl = [] then he else Cic.Appl (he::tl) in - let cannot_delta_expand t = - raise - (ProofEngineTypes.Fail - (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in - let rec hd_delta_beta context tl = - function - Cic.Rel n as t -> - (try - match List.nth context (n-1) with - Some (_,Cic.Decl _) -> cannot_delta_expand t - | Some (_,Cic.Def (bo,_)) -> - CicReduction.head_beta_reduce - (appl (CicSubstitution.lift n bo) tl) - | None -> raise RelToHiddenHypothesis - with - Failure _ -> assert false) - | Cic.Const (uri,exp_named_subst) as t -> - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - (match o with - Cic.Constant (_,Some body,_,_,_) -> - CicReduction.head_beta_reduce - (appl (CicSubstitution.subst_vars exp_named_subst body) tl) - | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t - | Cic.Variable _ -> raise ReferenceToVariable - | Cic.CurrentProof _ -> raise ReferenceToCurrentProof - | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - ) - | Cic.Var (uri,exp_named_subst) as t -> - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - (match o with - Cic.Constant _ -> raise ReferenceToConstant - | Cic.CurrentProof _ -> raise ReferenceToCurrentProof - | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | Cic.Variable (_,Some body,_,_,_) -> - CicReduction.head_beta_reduce - (appl (CicSubstitution.subst_vars exp_named_subst body) tl) - | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t - ) - | Cic.Appl [] -> assert false - | Cic.Appl (he::tl) -> hd_delta_beta context tl he - | t -> cannot_delta_expand t - in - let context_and_matched_term_list = - match what with - None -> [context, where] - | Some what -> - let res = - ProofEngineHelpers.locate_in_term - ~equality:first_is_the_expandable_head_of_second - what ~where context - in - if res = [] then - raise - (ProofEngineTypes.Fail - (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))) - else - res - in - let reduced_terms = - List.map - (function (context,where) -> hd_delta_beta context [] where) - context_and_matched_term_list in - let whats = List.map snd context_and_matched_term_list in - replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where -;; diff --git a/components/tactics/proofEngineReduction.mli b/components/tactics/proofEngineReduction.mli index 2d04d3959..f8cdec89b 100644 --- a/components/tactics/proofEngineReduction.mli +++ b/components/tactics/proofEngineReduction.mli @@ -50,7 +50,8 @@ val replace : inverse of subst up to the fact that free variables in "where" are NOT lifted. *) val replace_lifting : - equality:(Cic.term -> Cic.term -> bool) -> + equality:(Cic.context -> Cic.term -> Cic.term -> bool) -> + context:Cic.context -> what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term (* Replaces in "where" every term in "what" with the corresponding -- 2.39.2