From bf40c378bd2c624405be2118a478a0734eb8d3aa Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 8 Jul 2005 09:15:19 +0000 Subject: [PATCH] 1. PrimitiveTactics.new_metasenv_for_apply changed a little bit, moved to ProofEngineHelpers and renamed to saturate_term. It can be used to fully apply a term to metavariables until its type becomes different from a product. 2. the tactic rewrite now saturates the user provided term 3. the select function (to map a pattern to a set of physical pointers) now work up to unification WARNING: replace and generalize will not be working for a few hours --- helm/matita/library/Z.ma | 79 ++++---- helm/matita/library/nat.ma | 6 +- helm/matita/matita.txt | 6 + helm/ocaml/paramodulation/inference.ml | 12 +- helm/ocaml/tactics/equalityTactics.ml | 25 ++- helm/ocaml/tactics/primitiveTactics.ml | 80 ++------ helm/ocaml/tactics/primitiveTactics.mli | 5 - helm/ocaml/tactics/proofEngineHelpers.ml | 215 +++++++++++++++++----- helm/ocaml/tactics/proofEngineHelpers.mli | 11 ++ helm/ocaml/tactics/reductionTactics.ml | 42 +++-- helm/ocaml/tactics/variousTactics.ml | 2 + 11 files changed, 290 insertions(+), 193 deletions(-) diff --git a/helm/matita/library/Z.ma b/helm/matita/library/Z.ma index da6bbadb2..ba1084720 100644 --- a/helm/matita/library/Z.ma +++ b/helm/matita/library/Z.ma @@ -126,21 +126,21 @@ simplify.reflexivity. qed. theorem sym_Zplus : \forall x,y:Z. eq Z (Zplus x y) (Zplus y x). -intros.elim x.simplify.rewrite > Zplus_z_O y.reflexivity. +intros.elim x.simplify.rewrite > Zplus_z_O.reflexivity. elim y.simplify.reflexivity. simplify. -rewrite < (sym_plus e e1).reflexivity. +rewrite < sym_plus.reflexivity. simplify. -rewrite > nat_compare_invert e1 e2. -simplify.elim nat_compare e2 e1.simplify.reflexivity. +rewrite > nat_compare_invert. +simplify.elim nat_compare ? ?.simplify.reflexivity. simplify. reflexivity. simplify. reflexivity. elim y.simplify.reflexivity. -simplify.rewrite > nat_compare_invert e1 e2. -simplify.elim nat_compare e2 e1.simplify.reflexivity. +simplify.rewrite > nat_compare_invert. +simplify.elim nat_compare ? ?.simplify.reflexivity. simplify. reflexivity. simplify. reflexivity. -simplify.elim (sym_plus e2 e).reflexivity. +simplify.elim (sym_plus ? ?).reflexivity. qed. theorem Zpred_neg : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z). @@ -167,9 +167,9 @@ simplify.reflexivity. simplify.reflexivity. elim m. simplify. -rewrite < plus_n_O e1.reflexivity. +rewrite < plus_n_O.reflexivity. simplify. -rewrite < plus_n_Sm e1 e.reflexivity. +rewrite < plus_n_Sm.reflexivity. qed. theorem Zplus_succ_pred_pn : @@ -195,23 +195,21 @@ elim n.elim m. simplify.reflexivity. simplify.reflexivity. elim m. -simplify.rewrite < plus_n_Sm e1 O.reflexivity. -simplify.rewrite > plus_n_Sm e1 (S e).reflexivity. +simplify.rewrite < plus_n_Sm.reflexivity. +simplify.rewrite > plus_n_Sm.reflexivity. qed. -(* da qui in avanti rewrite ancora non utilizzata *) - theorem Zplus_succ_pred: \forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)). intros. elim x. elim y. simplify.reflexivity. simplify.reflexivity. -elim (Zsucc_pos ?).elim (sym_eq ? ? ? (Zsucc_pred ?)).reflexivity. -elim y.elim sym_Zplus ? ?.elim sym_Zplus (Zpred OZ) ?. -elim (Zpred_neg ?).elim (sym_eq ? ? ? (Zpred_succ ?)). +rewrite < Zsucc_pos.rewrite > Zsucc_pred.reflexivity. +elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ). +rewrite < Zpred_neg.rewrite > Zpred_succ. simplify.reflexivity. -apply Zplus_succ_pred_nn. +rewrite < Zplus_succ_pred_nn.reflexivity. apply Zplus_succ_pred_np. elim y.simplify.reflexivity. apply Zplus_succ_pred_pn. @@ -236,7 +234,7 @@ intros. elim n1. simplify. reflexivity. simplify.reflexivity. intros. -elim (Zplus_succ_pred_pn ? m1). +rewrite < (Zplus_succ_pred_pn ? m1). elim H.reflexivity. qed. @@ -253,7 +251,7 @@ intros. elim n1. simplify. reflexivity. simplify.reflexivity. intros. -elim (Zplus_succ_pred_nn ? m1). +rewrite < (Zplus_succ_pred_nn ? m1). reflexivity. qed. @@ -270,8 +268,8 @@ intros. elim n1. simplify. reflexivity. simplify.reflexivity. intros. -elim H. -elim (Zplus_succ_pred_np ? (S m1)). +rewrite < H. +rewrite < (Zplus_succ_pred_np ? (S m1)). reflexivity. qed. @@ -279,13 +277,13 @@ qed. theorem Zsucc_plus : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)). intros.elim x.elim y. simplify. reflexivity. -elim (Zsucc_pos ?).reflexivity. +rewrite < Zsucc_pos.reflexivity. simplify.reflexivity. -elim y.elim sym_Zplus ? ?.elim sym_Zplus OZ ?.simplify.reflexivity. +elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity. apply Zsucc_plus_nn. apply Zsucc_plus_np. elim y. -elim (sym_Zplus OZ ?).reflexivity. +rewrite < sym_Zplus OZ.reflexivity. apply Zsucc_plus_pn. apply Zsucc_plus_pp. qed. @@ -293,30 +291,31 @@ qed. theorem Zpred_plus : \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)). intros. cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)). -elim (sym_eq ? ? ? Hcut). -elim (sym_eq ? ? ? (Zsucc_plus ? ?)). -elim (sym_eq ? ? ? (Zpred_succ ?)). +rewrite > Hcut. +rewrite > Zsucc_plus. +rewrite > Zpred_succ. reflexivity. -elim (sym_eq ? ? ? (Zsucc_pred ?)). +rewrite > Zsucc_pred. reflexivity. qed. theorem assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus x (Zplus y z)) (Zplus (Zplus x y) z). intros.elim x.simplify.reflexivity. -elim e1.elim (Zpred_neg (Zplus y z)). -elim (Zpred_neg y). -elim (Zpred_plus ? ?). +elim e1.rewrite < (Zpred_neg (Zplus y z)). +rewrite < (Zpred_neg y). +rewrite < Zpred_plus. reflexivity. -elim (sym_eq ? ? ? (Zpred_plus (neg e) ?)). -elim (sym_eq ? ? ? (Zpred_plus (neg e) ?)). -elim (sym_eq ? ? ? (Zpred_plus (Zplus (neg e) y) ?)). +rewrite > Zpred_plus (neg e). +rewrite > Zpred_plus (neg e). +rewrite > Zpred_plus (Zplus (neg e) y). apply f_equal.assumption. -elim e2.elim (Zsucc_pos ?). -elim (Zsucc_pos ?). -apply (sym_eq ? ? ? (Zsucc_plus ? ?)) . -elim (sym_eq ? ? ? (Zsucc_plus (pos e1) ?)). -elim (sym_eq ? ? ? (Zsucc_plus (pos e1) ?)). -elim (sym_eq ? ? ? (Zsucc_plus (Zplus (pos e1) y) ?)). +elim e2.rewrite < Zsucc_pos. +rewrite < Zsucc_pos. +rewrite > Zsucc_plus. +reflexivity. +rewrite > Zsucc_plus (pos e1). +rewrite > Zsucc_plus (pos e1). +rewrite > Zsucc_plus (Zplus (pos e1) y). apply f_equal.assumption. qed. diff --git a/helm/matita/library/nat.ma b/helm/matita/library/nat.ma index 4ab1feb2b..c125e6775 100644 --- a/helm/matita/library/nat.ma +++ b/helm/matita/library/nat.ma @@ -36,8 +36,8 @@ qed. theorem injective_S : \forall n,m:nat. (eq nat (S n) (S m)) \to (eq nat n m). intros; -rewrite > pred_Sn n; -rewrite > pred_Sn m; +rewrite > pred_Sn; +rewrite > pred_Sn m. apply f_equal; assumption. qed. @@ -112,7 +112,7 @@ qed. theorem sym_times : \forall n,m:nat. eq nat (times n m) (times m n). intros.elim n.simplify.apply times_n_O. -simplify.rewrite < sym_eq ? ? ? H.apply times_n_Sm. +simplify.rewrite > H.apply times_n_Sm. qed. let rec minus n m \def diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 1bcb2a342..6310a8f71 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -2,6 +2,12 @@ (**********************************************************************) TODO +- Guardare il commento + (*CSC: this code is suspect and/or bugged: we try first without reduction + and then using whd. However, the saturate_term always tries with full + reduction without delta. *) + in primitiveTactics.ml. Potrebbe essere causa di rallentamento della apply + oltre che di bug! - Bug di cut&paste: se si fa cut&paste di testo lockato si ottiene testo lockato! - Dare errore significativo al posto di NotWellTypedInterpreation diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index fad86a854..62308896f 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -996,18 +996,10 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = match term with | C.Prod (name, s, t) -> (* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *) - let (head, newmetas, args, _) = - PrimitiveTactics.new_metasenv_for_apply newmeta proof + let (head, newmetas, args, newmeta) = + ProofEngineHelpers.saturate_term newmeta [] context (S.lift index term) in - let newmeta = - List.fold_left - (fun maxm arg -> - match arg with - | C.Meta (i, _) -> (max maxm i) - | _ -> assert false) - newmeta args - in let p = if List.length args = 0 then C.Rel index diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index e4520292d..4a6c445e6 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -42,10 +42,17 @@ let rewrite_tac ~direction ~pattern equality = in let curi, metasenv, pbo, pty = proof in let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in - let ty_eq,_ = + let ty_eq,ugraph = CicTypeChecker.type_of_aux' metasenv context equality - CicUniv.empty_ugraph - in + CicUniv.empty_ugraph in + let (ty_eq,metasenv,arguments,fresh_meta) = + ProofEngineHelpers.saturate_term + (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq in + let equality = + if List.length arguments = 0 then + equality + else + C.Appl (equality :: arguments) in let eq_ind, ty, t1, t2 = match ty_eq with | C.Appl [C.MutInd (uri, 0, []); ty; t1; t2] @@ -65,9 +72,10 @@ let rewrite_tac ~direction ~pattern equality = let lifted_conjecture = metano,(Some (fresh_name,Cic.Decl ty))::context,lifted_gty in let lifted_pattern = Some lifted_t1,[],CicSubstitution.lift 1 concl_pat in - let _,selected_terms_with_context = + let subst,metasenv,ugraph,_,selected_terms_with_context = ProofEngineHelpers.select - ~metasenv ~conjecture:lifted_conjecture ~pattern:lifted_pattern in + ~metasenv ~ugraph ~conjecture:lifted_conjecture ~pattern:lifted_pattern in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in let what,with_what = (* Note: Rel 1 does not live in the context context_of_t *) (* The replace_lifting_csc_0 function will take care of lifting it *) @@ -78,8 +86,11 @@ let rewrite_tac ~direction ~pattern equality = let abstr_gty = ProofEngineReduction.replace_lifting_csc 0 ~equality:(==) ~what ~with_what:with_what ~where:lifted_gty in + let abstr_gty = CicMetaSubst.apply_subst subst abstr_gty in + let t1 = CicMetaSubst.apply_subst subst t1 in + let t2 = CicMetaSubst.apply_subst subst t2 in + let equality = CicMetaSubst.apply_subst subst equality in let gty' = CicSubstitution.subst t2 abstr_gty in - let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let metasenv' = (fresh_meta,context,gty')::metasenv in let pred = C.Lambda (fresh_name, ty, abstr_gty) in @@ -110,6 +121,7 @@ let rewrite_simpl_tac ~direction ~pattern equality = ;; let replace_tac ~pattern ~with_what = +(* let replace_tac ~pattern:(wanted,hyps_pat,concl_pat) ~with_what status = let (proof, goal) = status in let module C = Cic in @@ -206,6 +218,7 @@ let replace_tac ~pattern ~with_what = aux 0 whats status in ProofEngineTypes.mk_tactic (replace_tac ~pattern ~with_what) +*) assert false ;; diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 00b6dac7e..2b67b521f 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -163,59 +163,6 @@ let classify_metas newmeta in_subst_domain subst_in metasenv = old_uninst,((i,canonical_context',ty')::new_uninst) ) metasenv ([],[]) -(* Auxiliary function for apply: given a type (a backbone), it returns its *) -(* head, a META environment in which there is new a META for each hypothesis,*) -(* a list of arguments for the new applications and the indexes of the first *) -(* and last new METAs introduced. The nth argument in the list of arguments *) -(* is just the nth new META. *) -let new_metasenv_for_apply newmeta proof context ty = - let module C = Cic in - let module S = CicSubstitution in - let rec aux newmeta ty = - let ty' = ty in - match ty' with - C.Cast (he,_) -> aux newmeta he -(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type - (* If the expected type is a Type, then also Set is OK ==> - * we accept any term of type Type *) - (*CSC: BUG HERE: in this way it is possible for the term of - * type Type to be different from a Sort!!! *) - | C.Prod (name,(C.Sort (C.Type _) as s),t) -> - (* TASSI: ask CSC if BUG HERE refers to the C.Cast or C.Propd case *) - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - let newargument = C.Meta (newmeta+1,irl) in - let (res,newmetasenv,arguments,lastmeta) = - aux (newmeta + 2) (S.subst newargument t) - in - res, - (newmeta,[],s)::(newmeta+1,context,C.Meta (newmeta,[]))::newmetasenv, - newargument::arguments,lastmeta -*) - | C.Prod (name,s,t) -> - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - let newargument = C.Meta (newmeta,irl) in - let (res,newmetasenv,arguments,lastmeta) = - aux (newmeta + 1) (S.subst newargument t) - in - let s' = CicReduction.normalize ~delta:false context s in - res,(newmeta,context,s')::newmetasenv,newargument::arguments,lastmeta - (** NORMALIZE RATIONALE - * we normalize the target only NOW since we may be in this case: - * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k - * and we want a mesasenv with ?1:A1 and ?2:A2 and not - * ?1, ?2, ?3 (that is the one we whould get if we start from the - * beta-normalized A1 -> A2 -> A3 -> P **) - | t -> (CicReduction.normalize ~delta:false context t),[],[],newmeta - in - (* WARNING: here we are using the invariant that above the most *) - (* recente new_meta() there are no used metas. *) - let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in - res,newmetasenv,arguments,lastmeta - (* Useful only inside apply_tac *) let generalize_exp_named_subst_with_fresh_metas context newmeta uri exp_named_subst @@ -276,16 +223,14 @@ let new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff ;; -let new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty termty = - let (consthead,newmetas,arguments,_) = - new_metasenv_for_apply newmeta' proof context termty - in - let newmetasenv = metasenv'@newmetas in +let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty = + let (consthead,newmetasenv,arguments,_) = + saturate_term newmeta' metasenv' context termty in let subst,newmetasenv',_ = - CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph + CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph in let t = - if List.length newmetas = 0 then term' else Cic.Appl (term'::arguments) + if List.length arguments = 0 then term' else Cic.Appl (term'::arguments) in subst,newmetasenv',t @@ -335,13 +280,16 @@ let apply_tac_verbose ~term (proof, goal) = let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in +(*CSC: this code is suspect and/or bugged: we try first without reduction + and then using whd. However, the saturate_term always tries with full + reduction without delta. *) let subst,newmetasenv',t = - try - new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty - termty - with CicUnification.UnificationFailure _ -> - new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty - (CicReduction.whd context termty) + try + new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty + termty + with CicUnification.UnificationFailure _ -> + new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty + (CicReduction.whd context termty) in let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in let apply_subst = CicMetaSubst.apply_subst subst in diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli index 6dac98724..5f608beb9 100644 --- a/helm/ocaml/tactics/primitiveTactics.mli +++ b/helm/ocaml/tactics/primitiveTactics.mli @@ -23,11 +23,6 @@ * http://cs.unibo.it/helm/. *) -(* ALB needed for paramodulation... *) -val new_metasenv_for_apply: - int -> ProofEngineTypes.proof -> Cic.context -> Cic.term -> - Cic.term * Cic.metasenv * Cic.term list * int - (* not a real tactic *) val apply_tac_verbose : term:Cic.term -> diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index ea797481c..f390b0e42 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -111,42 +111,92 @@ let compare_metasenvs ~oldmetasenv ~newmetasenv = ;; (** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *) -let find_subterms ~wanted ~context t = - let rec find context w t = - if ProofEngineReduction.alpha_equivalence w t then - [context,t] - else +let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t = + let rec find subst metasenv ugraph context w t = + try + let subst,metasenv,ugraph = + CicUnification.fo_unif_subst subst context metasenv w t ugraph + in + subst,metasenv,ugraph,[context,t] + with + CicUnification.UnificationFailure _ + | CicUnification.Uncertain _ -> match t with | Cic.Sort _ - | Cic.Rel _ -> [] + | Cic.Rel _ -> subst,metasenv,ugraph,[] | Cic.Meta (_, ctx) -> List.fold_left ( - fun acc e -> + fun (subst,metasenv,ugraph,acc) e -> match e with - | None -> acc - | Some t -> find context w t @ acc - ) [] ctx + | None -> subst,metasenv,ugraph,acc + | Some t -> + let subst,metasenv,ugraph,res = + find subst metasenv ugraph context w t + in + subst,metasenv,ugraph, res @ acc + ) (subst,metasenv,ugraph,[]) ctx | Cic.Lambda (name, t1, t2) | Cic.Prod (name, t1, t2) -> - find context w t1 @ - find (Some (name, Cic.Decl t1)::context) + let subst,metasenv,ugraph,rest1 = + find subst metasenv ugraph context w t1 in + let subst,metasenv,ugraph,rest2 = + find subst metasenv ugraph (Some (name, Cic.Decl t1)::context) (CicSubstitution.lift 1 w) t2 + in + subst,metasenv,ugraph,rest1 @ rest2 | Cic.LetIn (name, t1, t2) -> - find context w t1 @ - find (Some (name, Cic.Def (t1,None))::context) + let subst,metasenv,ugraph,rest1 = + find subst metasenv ugraph context w t1 in + let subst,metasenv,ugraph,rest2 = + find subst metasenv ugraph (Some (name, Cic.Def (t1,None))::context) (CicSubstitution.lift 1 w) t2 + in + subst,metasenv,ugraph,rest1 @ rest2 | Cic.Appl l -> - List.fold_left (fun acc t -> find context w t @ acc) [] l - | Cic.Cast (t, ty) -> find context w t @ find context w ty + List.fold_left + (fun (subst,metasenv,ugraph,acc) t -> + let subst,metasenv,ugraph,res = + find subst metasenv ugraph context w t + in + subst,metasenv,ugraph,res @ acc) + (subst,metasenv,ugraph,[]) l + | Cic.Cast (t, ty) -> + let subst,metasenv,ugraph,rest = + find subst metasenv ugraph context w t in + let subst,metasenv,ugraph,resty = + find subst metasenv ugraph context w ty + in + subst,metasenv,ugraph,rest @ resty | Cic.Implicit _ -> assert false | Cic.Const (_, esubst) | Cic.Var (_, esubst) | Cic.MutInd (_, _, esubst) | Cic.MutConstruct (_, _, _, esubst) -> - List.fold_left (fun acc (_, t) -> find context w t @ acc) [] esubst + List.fold_left + (fun (subst,metasenv,ugraph,acc) (_, t) -> + let subst,metasenv,ugraph,res = + find subst metasenv ugraph context w t + in + subst,metasenv,ugraph,res @ acc) + (subst,metasenv,ugraph,[]) esubst | Cic.MutCase (_, _, outty, indterm, patterns) -> - find context w outty @ find context w indterm @ - List.fold_left (fun acc p -> find context w p @ acc) [] patterns + let subst,metasenv,ugraph,resoutty = + find subst metasenv ugraph context w outty in + let subst,metasenv,ugraph,resindterm = + find subst metasenv ugraph context w indterm in + let subst,metasenv,ugraph,respatterns = + List.fold_left + (fun (subst,metasenv,ugraph,acc) p -> + let subst,metaseng,ugraph,res = + find subst metasenv ugraph context w p + in + subst,metasenv,ugraph,res @ acc + ) (subst,metasenv,ugraph,[]) patterns + in + subst,metasenv,ugraph,resoutty @ resindterm @ respatterns +(*CSC: c'e' ancora un problema: il caso vs Meta puo' alterare il goal ==> + bisogna ricominciare da capo sul nuovo goal per preservare i puntatori + fisici | Cic.Fix (_, funl) -> let tys = List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl @@ -163,10 +213,11 @@ let find_subterms ~wanted ~context t = fun acc (_, ty, bo) -> find context w ty @ find (tys @ context) w bo @ acc ) [] funl +*) in - find context wanted t + find subst metasenv ugraph context wanted t -let select_in_term ~context ~term ~pattern:(wanted,where) = +let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = let add_ctx context name entry = (Some (name, entry)) :: context in @@ -238,21 +289,21 @@ let select_in_term ~context ~term ~pattern:(wanted,where) = let context_len = List.length context in let roots = aux context where term in match wanted with - None -> roots + None -> [],metasenv,ugraph,roots | Some wanted -> let rec find_in_roots = function - [] -> [] + [] -> [],metasenv,ugraph,[] | (context',where)::tl -> - let tl' = find_in_roots tl in + let subst,metasenv,ugraph,tl' = find_in_roots tl in let context'_len = List.length context' in - let found = + let subst,metasenv,ugraph,found = let wanted = CicSubstitution.lift (context'_len - context_len) wanted in - find_subterms ~wanted ~context where + find_subterms ~subst ~metasenv ~ugraph ~wanted ~context where in - found @ tl' + subst,metasenv,ugraph,found @ tl' in find_in_roots roots @@ -406,21 +457,26 @@ exception Fail of string * has an entry for each entry in the context and in the same order. * Of course the list of terms (with their context) associated to the * hypothesis name may be empty. *) - let select ~metasenv ~conjecture:(_,context,ty) ~pattern:(what,hyp_patterns,goal_pattern) = + let select ~metasenv ~ugraph ~conjecture:(_,context,ty) + ~pattern:(what,hyp_patterns,goal_pattern) + = let find_pattern_for name = try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns)) with Not_found -> None in - let ty_terms = select_in_term ~context ~term:ty ~pattern:(what,goal_pattern) in + let subst,metasenv,ugraph,ty_terms = + select_in_term ~metasenv ~context ~ugraph ~term:ty + ~pattern:(what,goal_pattern) in let context_len = List.length context in - let context_terms = - fst + let subst,metasenv,ugraph,context_terms = + let subst,metasenv,ugraph,res,_ = (List.fold_right - (fun entry (res,context) -> + (fun entry (subst,metasenv,ugraph,res,context) -> match entry with - None -> (None::res),(None::context) + None -> subst,metasenv,ugraph,(None::res),(None::context) | Some (name,Cic.Decl term) -> (match find_pattern_for name with - | None -> ((Some (`Decl []))::res),(entry::context) + | None -> + subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context) | Some pat -> try let what = @@ -434,8 +490,12 @@ exception Fail of string assert (subst' = []); assert (metasenv' = metasenv); Some what in - let terms = select_in_term ~context ~term ~pattern:(what,pat) in - ((Some (`Decl terms))::res),(entry::context) + let subst,metasenv,ugraph,terms = + select_in_term ~metasenv ~context ~ugraph ~term + ~pattern:(what,pat) + in + subst,metasenv,ugraph,((Some (`Decl terms))::res), + (entry::context) with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> raise @@ -445,8 +505,9 @@ exception Fail of string | Some (name,Cic.Def (bo, ty)) -> (match find_pattern_for name with | None -> - let selected_ty= match ty with None -> None | Some _ -> Some [] in - ((Some (`Def ([],selected_ty)))::res),(entry::context) + let selected_ty=match ty with None -> None | Some _ -> Some [] in + subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res), + (entry::context) | Some pat -> try let what = @@ -460,21 +521,83 @@ exception Fail of string assert (subst' = []); assert (metasenv' = metasenv); Some what in - let terms_bo = - select_in_term ~context ~term:bo ~pattern:(what,pat) in - let terms_ty = + let subst,metasenv,ugraph,terms_bo = + select_in_term ~metasenv ~context ~ugraph ~term:bo + ~pattern:(what,pat) in + let subst,metasenv,ugraph,terms_ty = match ty with - None -> None + None -> subst,metasenv,ugraph,None | Some ty -> - Some (select_in_term ~context ~term:ty ~pattern:(what,pat)) + let subst,metasenv,ugraph,res = + select_in_term ~metasenv ~context ~ugraph ~term:ty + ~pattern:(what,pat) + in + subst,metasenv,ugraph,Some res in - ((Some (`Def (terms_bo,terms_ty)))::res),(entry::context) + subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res), + (entry::context) with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> raise (Fail ("The term the user wants to convert is not closed " ^ "in the context of the position of the substitution."))) - ) context ([],[])) + ) context (subst,metasenv,ugraph,[],[])) + in + subst,metasenv,ugraph,res in - context_terms, ty_terms + subst,metasenv,ugraph,context_terms, ty_terms + +(* saturate_term newmeta metasenv context ty *) +(* Given a type [ty] (a backbone), it returns its head and a new metasenv in *) +(* which there is new a META for each hypothesis, a list of arguments for the *) +(* new applications and the index of the last new META introduced. The nth *) +(* argument in the list of arguments is just the nth new META. *) +let saturate_term newmeta metasenv context ty = + let module C = Cic in + let module S = CicSubstitution in + let rec aux newmeta ty = + let ty' = ty in + match ty' with + C.Cast (he,_) -> aux newmeta he +(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type + (* If the expected type is a Type, then also Set is OK ==> + * we accept any term of type Type *) + (*CSC: BUG HERE: in this way it is possible for the term of + * type Type to be different from a Sort!!! *) + | C.Prod (name,(C.Sort (C.Type _) as s),t) -> + (* TASSI: ask CSC if BUG HERE refers to the C.Cast or C.Propd case *) + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + let newargument = C.Meta (newmeta+1,irl) in + let (res,newmetasenv,arguments,lastmeta) = + aux (newmeta + 2) (S.subst newargument t) + in + res, + (newmeta,[],s)::(newmeta+1,context,C.Meta (newmeta,[]))::newmetasenv, + newargument::arguments,lastmeta +*) + | C.Prod (name,s,t) -> + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + let newargument = C.Meta (newmeta,irl) in + let (res,newmetasenv,arguments,lastmeta) = + aux (newmeta + 1) (S.subst newargument t) + in + let s' = CicReduction.normalize ~delta:false context s in + res,(newmeta,context,s')::newmetasenv,newargument::arguments,lastmeta + (** NORMALIZE RATIONALE + * we normalize the target only NOW since we may be in this case: + * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k + * and we want a mesasenv with ?1:A1 and ?2:A2 and not + * ?1, ?2, ?3 (that is the one we whould get if we start from the + * beta-normalized A1 -> A2 -> A3 -> P **) + | t -> (CicReduction.normalize ~delta:false context t),[],[],newmeta + in + (* WARNING: here we are using the invariant that above the most *) + (* recente new_meta() there are no used metas. *) + let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in + res,metasenv @ newmetasenv,arguments,lastmeta + diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index 219d426e4..b77fd88ac 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -71,9 +71,20 @@ val pattern_of: * hypothesis may be empty. *) val select: metasenv:Cic.metasenv -> + ugraph:CicUniv.universe_graph -> conjecture:Cic.conjecture -> pattern:ProofEngineTypes.pattern -> + Cic.substitution * Cic.metasenv * CicUniv.universe_graph * [ `Decl of (Cic.context * Cic.term) list | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list option ] option list * (Cic.context * Cic.term) list + +(* saturate_term newmeta metasenv context ty *) +(* Given a type [ty] (a backbone), it returns its head and a new metasenv in *) +(* which there is new a META for each hypothesis, a list of arguments for the *) +(* new applications and the index of the last new META introduced. The nth *) +(* argument in the list of arguments is just the nth new META. *) +val saturate_term: + int -> Cic.metasenv -> Cic.context -> Cic.term -> + Cic.term * Cic.metasenv * Cic.term list * int diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index d34678e52..1885e956c 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -30,31 +30,35 @@ open ProofEngineTypes let reduction_tac ~reduction ~pattern (proof,goal) = let curi,metasenv,pbo,pty = proof in let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in - let change where terms = + let change subst where terms = if terms = [] then where else let terms, terms' = List.split (List.map (fun (context, t) -> t, reduction context t) terms) in + let where' = ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' - ~where:where in - let (selected_context,selected_ty) = - ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in - let ty' = change ty selected_ty in + ~where:where + in + CicMetaSubst.apply_subst subst where' in + let (subst,metasenv,ugraph,selected_context,selected_ty) = + ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph + ~conjecture ~pattern in + let ty' = change subst ty selected_ty in let context' = List.fold_right2 (fun entry selected_entry context' -> match entry,selected_entry with None,None -> None::context' | Some (name,Cic.Decl ty),Some (`Decl selected_ty) -> - let ty' = change ty selected_ty in + let ty' = change subst ty selected_ty in Some (name,Cic.Decl ty')::context' | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) -> - let bo' = change bo selected_bo in + let bo' = change subst bo selected_bo in let ty' = match ty,selected_ty with None,None -> None - | Some ty,Some selected_ty -> Some (change ty selected_ty) + | Some ty,Some selected_ty -> Some (change subst ty selected_ty) | _,_ -> assert false in Some (name,Cic.Def (bo',ty'))::context' @@ -97,7 +101,7 @@ let change_tac ~pattern with_what = let curi,metasenv,pbo,pty = proof in let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in let context_len = List.length context in - let change context'_len where terms = + let change subst context'_len where terms = if terms = [] then where else let terms, terms' = @@ -134,11 +138,15 @@ let change_tac ~pattern with_what = else raise NotConvertible) terms) in - ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' - ~where:where in - let (selected_context,selected_ty) = - ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in - let ty' = change context_len ty selected_ty in + let where' = + ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' + ~where:where + in + CicMetaSubst.apply_subst subst where' in + let (subst,metasenv,ugraph,selected_context,selected_ty) = + ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture + ~pattern in + let ty' = change subst context_len ty selected_ty in let context' = List.fold_right2 (fun entry selected_entry context' -> @@ -146,15 +154,15 @@ let change_tac ~pattern with_what = match entry,selected_entry with None,None -> None::context' | Some (name,Cic.Decl ty),Some (`Decl selected_ty) -> - let ty' = change context'_len ty selected_ty in + let ty' = change subst context'_len ty selected_ty in Some (name,Cic.Decl ty')::context' | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) -> - let bo' = change context'_len bo selected_bo in + let bo' = change subst context'_len bo selected_bo in let ty' = match ty,selected_ty with None,None -> None | Some ty,Some selected_ty -> - Some (change context'_len ty selected_ty) + Some (change subst context'_len ty selected_ty) | _,_ -> assert false in Some (name,Cic.Def (bo',ty'))::context' diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index e2003f48d..8bbe05dcb 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -72,6 +72,7 @@ let generalize_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) pattern = +(* let module PET = ProofEngineTypes in let generalize_tac mk_fresh_name_callback ~pattern:(term,hyps_pat,concl_pat) status @@ -142,4 +143,5 @@ let generalize_tac status in PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern) +*) assert false ;; -- 2.39.2