From 2b01133527077e8dd554f0fbcc51368903dd3b8c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Jun 2005 12:25:19 +0000 Subject: [PATCH] 1. rewrite_* and rewrite_back_* merged into one function 2. signature of rewrite_* improved 3. concrete syntax for the rewrite direction fixed to ">" and "<" NOTE: rewrite_* is still no longer working. --- .../cic_disambiguation/cicTextualParser2.ml | 6 +-- helm/ocaml/cic_transformations/tacticAst.ml | 2 +- helm/ocaml/cic_transformations/tacticAstPp.ml | 3 +- helm/ocaml/tactics/discriminationTactics.ml | 13 ++++-- helm/ocaml/tactics/equalityTactics.ml | 41 +++++-------------- helm/ocaml/tactics/equalityTactics.mli | 14 ++----- helm/ocaml/tactics/fourierR.ml | 5 ++- helm/ocaml/tactics/tactics.ml | 2 - helm/ocaml/tactics/tactics.mli | 14 ++----- 9 files changed, 37 insertions(+), 63 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index fc46cc725..9f6476d28 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -351,10 +351,8 @@ EXTEND wanted, hyp_paths, goal_path ] ]; direction: [ - [ IDENT "left" -> `Left - | SYMBOL ">" -> `Left - | IDENT "right" -> `Right - | SYMBOL "<" -> `Right ] + [ SYMBOL ">" -> `LeftToRight + | SYMBOL "<" -> `RightToLeft ] ]; tactic: [ [ IDENT "absurd"; t = tactic_term -> diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 15961702d..d9f909a5f 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -type direction = [ `Left | `Right ] +type direction = [ `LeftToRight | `RightToLeft ] type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ] type loc = CicAst.location diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 33b5e8ade..83fdaf082 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -104,7 +104,8 @@ let rec pp_tactic = function sprintf "replace %s with %s" (pp_pattern pattern) (pp_term_ast t) | Rewrite (_, pos, t, pattern) -> sprintf "rewrite %s %s %s" - (if pos = `Left then "left" else "right") (pp_term_ast t) + (if pos = `LeftToRight then ">" else "<") + (pp_term_ast t) (pp_pattern pattern) | Right _ -> "right" | Ring _ -> "ring" diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 05344e0ab..ffc6a9e81 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -183,7 +183,11 @@ and injection1_tac ~term ~i = )) ~continuation: (T.then_ - ~start:(EqualityTactics.rewrite_simpl_tac ~term ()) + ~start: + (EqualityTactics.rewrite_simpl_tac + ~direction:`LeftToRight + ~pattern:(ProofEngineTypes.conclusion_pattern None) + term) ~continuation:EqualityTactics.reflexivity_tac ) ]) @@ -314,8 +318,11 @@ let discriminate'_tac ~term = ~continuation: ( T.then_ - ~start:(EqualityTactics.rewrite_back_simpl_tac - ~term ()) + ~start: + (EqualityTactics.rewrite_simpl_tac + ~direction:`RightToLeft + ~pattern:(ProofEngineTypes.conclusion_pattern None) + term) ~continuation:(IntroductionTactics.constructor_tac ~n:1) )) (proof',goal') diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 94f62a955..5bbfa33a6 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -24,7 +24,8 @@ *) -let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) = +let rewrite_tac ~direction ~pattern equality = + let rewrite_tac ~direction ~pattern equality status = (* let module C = Cic in let module U = UriManager in @@ -33,6 +34,7 @@ let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) = let module PEH = ProofEngineHelpers in let module PT = PrimitiveTactics in let module HLO = HelmLibraryObjects in + let proof,goal = status in let if_left a b = match direction with | `Right -> b @@ -106,45 +108,22 @@ let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) = in assert (List.length goals = 0) ; (proof',[fresh_meta]) -*) assert false + ProofEngineTypes.mk_tactic (rewrite_tac ?where ~term) +*) assert false in + ProofEngineTypes.mk_tactic (rewrite_tac ~direction ~pattern equality) -let rewrite_tac ?where ~term () = - let rewrite_tac ?where ~term status = - rewrite ?where ~term ~direction:`Right status - in - ProofEngineTypes.mk_tactic (rewrite_tac ?where ~term) - -let rewrite_simpl_tac ?where ~term () = - let rewrite_simpl_tac ?where ~term status = +let rewrite_simpl_tac ~direction ~pattern equality = + let rewrite_simpl_tac ~direction ~pattern equality status = ProofEngineTypes.apply_tactic (Tacticals.then_ - ~start:(rewrite_tac ?where ~term ()) + ~start:(rewrite_tac ~direction:`LeftToRight ~pattern equality) ~continuation: (ReductionTactics.simpl_tac ~pattern:(ProofEngineTypes.conclusion_pattern None))) status in - ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term) -;; - -let rewrite_back_tac ?where ~term () = - let rewrite_back_tac ?where ~term status = - rewrite ?where ~term ~direction:`Left status - in - ProofEngineTypes.mk_tactic (rewrite_back_tac ?where ~term) - -let rewrite_back_simpl_tac ?where ~term () = - let rewrite_back_simpl_tac ?where ~term status = - ProofEngineTypes.apply_tactic - (Tacticals.then_ - ~start:(rewrite_back_tac ?where ~term ()) - ~continuation: - (ReductionTactics.simpl_tac - ~pattern:(ProofEngineTypes.conclusion_pattern None))) - status - in - ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term) + ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~direction ~pattern equality) ;; let replace_tac ~pattern ~with_what = diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli index d156ae440..a9b4d1d0b 100644 --- a/helm/ocaml/tactics/equalityTactics.mli +++ b/helm/ocaml/tactics/equalityTactics.mli @@ -24,17 +24,11 @@ *) val rewrite_tac: - ?where:ProofEngineTypes.pattern -> - term:Cic.term -> unit -> ProofEngineTypes.tactic + direction:[`LeftToRight | `RightToLeft] -> + pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic val rewrite_simpl_tac: - ?where:ProofEngineTypes.pattern -> - term:Cic.term -> unit -> ProofEngineTypes.tactic -val rewrite_back_tac: - ?where:ProofEngineTypes.pattern -> - term:Cic.term -> unit -> ProofEngineTypes.tactic -val rewrite_back_simpl_tac: - ?where:ProofEngineTypes.pattern -> - term:Cic.term -> unit -> ProofEngineTypes.tactic + direction:[`LeftToRight | `RightToLeft] -> + pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic val replace_tac: pattern:ProofEngineTypes.pattern -> diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index e6fa4edcd..2fbba97ad 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -886,7 +886,10 @@ let equality_replace a b = let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl))); let (proof,goals) = apply_tactic - (EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) ()) + (EqualityTactics.rewrite_simpl_tac + ~direction:`LeftToRight + ~pattern:(ProofEngineTypes.conclusion_pattern None) + (C.Meta (fresh_meta,irl))) ((curi,metasenv',pbo,pty),goal) in let new_goals = fresh_meta::goals in diff --git a/helm/ocaml/tactics/tactics.ml b/helm/ocaml/tactics/tactics.ml index fc2c1c75d..055c00528 100644 --- a/helm/ocaml/tactics/tactics.ml +++ b/helm/ocaml/tactics/tactics.ml @@ -58,8 +58,6 @@ let reduce = ReductionTactics.reduce_tac let reflexivity = EqualityTactics.reflexivity_tac let replace = EqualityTactics.replace_tac let rewrite = EqualityTactics.rewrite_tac -let rewrite_back = EqualityTactics.rewrite_back_tac -let rewrite_back_simpl = EqualityTactics.rewrite_back_simpl_tac let rewrite_simpl = EqualityTactics.rewrite_simpl_tac let right = IntroductionTactics.right_tac let ring = Ring.ring_tac diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index a8730287e..f78624c97 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -59,17 +59,11 @@ val replace : pattern:ProofEngineTypes.pattern -> with_what:Cic.term -> ProofEngineTypes.tactic val rewrite : - ?where:ProofEngineTypes.pattern -> - term:Cic.term -> unit -> ProofEngineTypes.tactic -val rewrite_back : - ?where:ProofEngineTypes.pattern -> - term:Cic.term -> unit -> ProofEngineTypes.tactic -val rewrite_back_simpl : - ?where:ProofEngineTypes.pattern -> - term:Cic.term -> unit -> ProofEngineTypes.tactic + direction:[ `LeftToRight | `RightToLeft ] -> + pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic val rewrite_simpl : - ?where:ProofEngineTypes.pattern -> - term:Cic.term -> unit -> ProofEngineTypes.tactic + direction:[ `LeftToRight | `RightToLeft ] -> + pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic val right : ProofEngineTypes.tactic val ring : ProofEngineTypes.tactic val set_goal : int -> ProofEngineTypes.tactic -- 2.39.2