From f36b907612b05a95aba0f9e96030def1609bdadb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 31 May 2006 13:54:36 +0000 Subject: [PATCH] fixed proofs, contextualization should now work. the empty context is not a term with an open (Rel 1), but a a term with a (Cic.Implicit(Some `Hole)) so that it can't bw confused with a Rel to the last Hypothesis. --- components/tactics/autoTactic.ml | 4 +++- components/tactics/paramodulation/equality.ml | 20 ++++++++++--------- 2 files changed, 14 insertions(+), 10 deletions(-) diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index 7aabf9f33..a9505d739 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -340,7 +340,9 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation debug_print (lazy "USO PARAMODULATION..."); (* try *) try - Saturation.saturate dbd ~depth ~width ~full (proof, goal) + let rc = Saturation.saturate dbd ~depth ~width ~full (proof, goal) in + prerr_endline (Saturation.get_stats ()); + rc with exn -> prerr_endline (Saturation.get_stats ()); raise exn diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index bceb3ebc2..2561ea56f 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -305,12 +305,12 @@ let ty_of_lambda = function let compose_contexts ctx1 ctx2 = ProofEngineReduction.replace_lifting - ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[ctx2] ~where:ctx1 + ~equality:(=) ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1 ;; let put_in_ctx ctx t = ProofEngineReduction.replace_lifting - ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[t] ~where:ctx + ~equality:(=) ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx ;; let mk_eq uri ty l r = @@ -328,13 +328,14 @@ let open_eq = function ;; let contextualize uri ty left right t = + let hole = Cic.Implicit (Some `Hole) in (* aux [uri] [ty] [left] [right] [ctx] [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 open (Rel 1). (Rel 1) is the empty context + * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context *) let rec aux uri ty left right ctx_d = function | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) @@ -358,7 +359,7 @@ let contextualize uri ty left right t = 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 ctx_c = CicSubstitution.subst (Cic.Rel 1) ctx_c in + let ctx_c = CicSubstitution.subst hole ctx_c in m, ctx_c in (* create the compound context and put the terms under it *) @@ -400,9 +401,11 @@ let contextualize uri ty left right t = let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in let pred = (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *) - let ctx_d = CicSubstitution.lift_from 2 1 ctx_d in (* bleah *) - let r = put_in_ctx ctx_d (CicSubstitution.lift 1 left) in - let l = ctx_d in + let r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) in + let l = + 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 Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r)) in @@ -412,8 +415,7 @@ let contextualize uri ty left right t = mk_sym uri_sym ty d_right d_left (mk_eq_ind uri_ind ty left pred refl_eq right t) in - let empty_context = Cic.Rel 1 in - aux uri ty left right empty_context t + aux uri ty left right hole t ;; let contextualize_rewrites t ty = -- 2.39.2