From 9e3eb63a93acaca0b4ad59c213e9ea430524d3ae Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 13 Sep 2005 11:56:42 +0000 Subject: [PATCH] Two bugs fixed in the apply tactic: 1. an application of a term of type t where t reduces to a product does not fail any longer: t is unfolded as required to produce enough products. E.g. apply (t: ~A) when the goal is False 2. the apply tactic does not fail any longer when the goal is a product. When the head of the type of the term is flexible, the type is a product and the goal is a product (e.g. t: A -> ? vs A' -> B) the less instantiated term (i.e. t) is tried first; in case of failure (e.g. A not unifiable with A') t is instantiated adding one metavariable after another. --- helm/ocaml/paramodulation/inference.ml | 4 +- helm/ocaml/tactics/equalityTactics.ml | 2 +- helm/ocaml/tactics/primitiveTactics.ml | 30 ++++++++------ helm/ocaml/tactics/proofEngineHelpers.ml | 48 ++++++++++++++--------- helm/ocaml/tactics/proofEngineHelpers.mli | 13 +++--- 5 files changed, 56 insertions(+), 41 deletions(-) diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index e92117334..969d412ce 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1055,7 +1055,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = (* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *) let (head, newmetas, args, newmeta) = ProofEngineHelpers.saturate_term newmeta [] - context (S.lift index term) + context (S.lift index term) 0 in let p = if List.length args = 0 then @@ -1161,7 +1161,7 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = match termty with | C.Prod (name, s, t) -> let head, newmetas, args, newmeta = - ProofEngineHelpers.saturate_term newmeta [] context termty + ProofEngineHelpers.saturate_term newmeta [] context termty 0 in let p = if List.length args = 0 then diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 94cb0624b..c56d3de2d 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -47,7 +47,7 @@ let rewrite_tac ~direction ~pattern equality = 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 + (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in let equality = if List.length arguments = 0 then equality diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index c43034f93..97f402052 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -223,9 +223,9 @@ let new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff ;; -let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty = +let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity = let (consthead,newmetasenv,arguments,_) = - saturate_term newmeta' metasenv' context termty in + saturate_term newmeta' metasenv' context termty goal_arity in let subst,newmetasenv',_ = CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph in @@ -234,6 +234,11 @@ let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty = in subst,newmetasenv',t +let rec count_prods context ty = + match CicReduction.whd context ty with + Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t + | _ -> 0 + let apply_tac_verbose ~term (proof, goal) = (* Assumption: The term "term" must be closed in the current context *) let module T = CicTypeChecker in @@ -278,18 +283,17 @@ let apply_tac_verbose ~term (proof, goal) = let termty,_ = CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph in 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. *) + CicSubstitution.subst_vars exp_named_subst_diff termty in + let goal_arity = count_prods context ty in let subst,newmetasenv',t = - try + let rec add_one_argument n = + 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) + termty n + with CicUnification.UnificationFailure _ when n > 0 -> + add_one_argument (n - 1) + in + add_one_argument goal_arity in let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in let apply_subst = CicMetaSubst.apply_subst subst in @@ -457,7 +461,7 @@ let elim_tac ~term = let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in let (termty,metasenv',arguments,fresh_meta) = ProofEngineHelpers.saturate_term - (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty in + (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in let term = if arguments = [] then term else Cic.Appl (term::arguments) in let uri,exp_named_subst,typeno,args = match termty with diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index a7c1d39bd..23aa20bfb 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -608,17 +608,18 @@ let locate_in_conjecture ?(equality=fun _ -> (==)) what (_,context,ty) = in res @ locate_in_term what ~where:ty context -(* 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 = +(* saturate_term newmeta metasenv context ty goal_arity *) +(* Given a type [ty] (a backbone), it returns its suffix of length *) +(* [goal_arity] 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 goal_arity = let module C = Cic in let module S = CicSubstitution in + assert (goal_arity >= 0); let rec aux newmeta ty = - let ty' = ty in - match ty' with + 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 ==> @@ -643,22 +644,31 @@ let saturate_term newmeta metasenv context ty = CicMkImplicit.identity_relocation_list_for_metavariable context in let newargument = C.Meta (newmeta,irl) in - let (res,newmetasenv,arguments,lastmeta) = + let res,newmetasenv,arguments,lastmeta,prod_no = 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 + if prod_no + 1 = goal_arity then + let head = CicReduction.normalize ~delta:false context ty in + head,[],[],newmeta,goal_arity + 1 + else + (** 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 **) + let s' = CicReduction.normalize ~delta:false context s in + res,(newmeta,context,s')::newmetasenv,newargument::arguments, + lastmeta,prod_no + 1 + | t -> + let head = CicReduction.normalize ~delta:false context t in + match CicReduction.whd context head with + C.Prod _ as head' -> aux newmeta head' + | _ -> head,[],[],newmeta,0 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 + let res,newmetasenv,arguments,lastmeta,_ = aux newmeta ty in res,metasenv @ newmetasenv,arguments,lastmeta let lookup_type metasenv context hyp = diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index 6d1c7ffaa..a7603d3a5 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -103,13 +103,14 @@ val locate_in_conjecture: ?equality:(Cic.context -> Cic.term -> Cic.term -> bool) -> Cic.term -> Cic.conjecture -> (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. *) +(* saturate_term newmeta metasenv context ty goal_arity *) +(* Given a type [ty] (a backbone), it returns its suffix of length *) +(* [goal_arity] 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 -> + int -> Cic.metasenv -> Cic.context -> Cic.term -> int -> Cic.term * Cic.metasenv * Cic.term list * int (* returns the index and the type of a premise in a context *) -- 2.39.2