From 9352c5815be42fadc2c1f0241c0449a56273fd12 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 28 Jul 2005 15:09:53 +0000 Subject: [PATCH] Bug fixed: unfold used to work iff the term to unfold was in head position in the term. --- helm/ocaml/tactics/proofEngineReduction.ml | 15 ++++++++++----- helm/ocaml/tactics/proofEngineReduction.mli | 2 +- 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index a9b8b5500..8d4245068 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -127,7 +127,7 @@ let replace ~equality ~what ~with_what ~where = function [],[] -> raise Not_found | what::tl1,with_what::tl2 -> - if equality t what 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) @@ -190,7 +190,7 @@ let replace_lifting ~equality ~what ~with_what ~where = function [],[] -> raise Not_found | what::tl1,with_what::tl2 -> - if equality t what 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) @@ -288,7 +288,7 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where = function [],[] -> raise Not_found | what::tl1,with_what::tl2 -> - if equality t what 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) @@ -933,7 +933,7 @@ let unfold ?what context where = | Cic.Appl (he::tl) -> hd_delta_beta context tl he | t -> cannot_delta_expand t in - let context, where = + let context, where' = match what with None -> context, where | Some what -> @@ -947,5 +947,10 @@ let unfold ?what context where = (ProofEngineTypes.Fail ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)) in - hd_delta_beta context [] where + let reduced_term = hd_delta_beta context [] where' in + match what with + None -> reduced_term + | Some what -> + replace ~equality:first_is_the_expandable_head_of_second + ~what:[what] ~with_what:[reduced_term] ~where ;; diff --git a/helm/ocaml/tactics/proofEngineReduction.mli b/helm/ocaml/tactics/proofEngineReduction.mli index ebb61a7c8..67247876a 100644 --- a/helm/ocaml/tactics/proofEngineReduction.mli +++ b/helm/ocaml/tactics/proofEngineReduction.mli @@ -36,7 +36,7 @@ exception WhatAndWithWhatDoNotHaveTheSameLength;; val alpha_equivalence: Cic.term -> Cic.term -> bool val replace : - equality:(Cic.term -> 'a -> bool) -> + equality:('a -> Cic.term -> bool) -> what:'a list -> with_what:Cic.term list -> where:Cic.term -> Cic.term val replace_lifting : equality:(Cic.term -> Cic.term -> bool) -> -- 2.39.2