From e436c170ce2b9154d3e090c2140e8a0172f4a016 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 16 Apr 2007 15:28:27 +0000 Subject: [PATCH] subst tactic put in a file on its own --- helm/software/components/tactics/.depend | 19 ++- helm/software/components/tactics/.depend.opt | 19 ++- helm/software/components/tactics/Makefile | 5 +- .../components/tactics/equalityTactics.ml | 80 ------------ .../components/tactics/equalityTactics.mli | 5 - .../components/tactics/substTactic.ml | 115 ++++++++++++++++++ .../components/tactics/substTactic.mli | 27 ++++ helm/software/components/tactics/tactics.ml | 2 +- helm/software/components/tactics/tactics.mli | 2 +- 9 files changed, 172 insertions(+), 102 deletions(-) create mode 100644 helm/software/components/tactics/substTactic.ml create mode 100644 helm/software/components/tactics/substTactic.mli diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index 6c23fc909..bac580671 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -24,6 +24,7 @@ equalityTactics.cmi: proofEngineTypes.cmi auto.cmi: universe.cmi proofEngineTypes.cmi autoTactic.cmi: universe.cmi proofEngineTypes.cmi discriminationTactics.cmi: proofEngineTypes.cmi +substTactic.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi ring.cmi: proofEngineTypes.cmi setoids.cmi: proofEngineTypes.cmi @@ -147,13 +148,19 @@ autoTactic.cmx: proofEngineTypes.cmx proofEngineHelpers.cmx \ primitiveTactics.cmx metadataQuery.cmx paramodulation/equality.cmx \ autoTypes.cmx auto.cmx autoTactic.cmi discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \ - proofEngineTypes.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \ - introductionTactics.cmi equalityTactics.cmi eliminationTactics.cmi \ - discriminationTactics.cmi + proofEngineTypes.cmi proofEngineStructuralRules.cmi \ + proofEngineHelpers.cmi primitiveTactics.cmi introductionTactics.cmi \ + equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \ - proofEngineTypes.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \ - introductionTactics.cmx equalityTactics.cmx eliminationTactics.cmx \ - discriminationTactics.cmi + proofEngineTypes.cmx proofEngineStructuralRules.cmx \ + proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \ + equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi +substTactic.cmo: tacticals.cmi proofEngineTypes.cmi \ + proofEngineStructuralRules.cmi proofEngineHelpers.cmi equalityTactics.cmi \ + substTactic.cmi +substTactic.cmx: tacticals.cmx proofEngineTypes.cmx \ + proofEngineStructuralRules.cmx proofEngineHelpers.cmx equalityTactics.cmx \ + substTactic.cmi inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ equalityTactics.cmi inversion.cmi diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt index 6c23fc909..bac580671 100644 --- a/helm/software/components/tactics/.depend.opt +++ b/helm/software/components/tactics/.depend.opt @@ -24,6 +24,7 @@ equalityTactics.cmi: proofEngineTypes.cmi auto.cmi: universe.cmi proofEngineTypes.cmi autoTactic.cmi: universe.cmi proofEngineTypes.cmi discriminationTactics.cmi: proofEngineTypes.cmi +substTactic.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi ring.cmi: proofEngineTypes.cmi setoids.cmi: proofEngineTypes.cmi @@ -147,13 +148,19 @@ autoTactic.cmx: proofEngineTypes.cmx proofEngineHelpers.cmx \ primitiveTactics.cmx metadataQuery.cmx paramodulation/equality.cmx \ autoTypes.cmx auto.cmx autoTactic.cmi discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \ - proofEngineTypes.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \ - introductionTactics.cmi equalityTactics.cmi eliminationTactics.cmi \ - discriminationTactics.cmi + proofEngineTypes.cmi proofEngineStructuralRules.cmi \ + proofEngineHelpers.cmi primitiveTactics.cmi introductionTactics.cmi \ + equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \ - proofEngineTypes.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \ - introductionTactics.cmx equalityTactics.cmx eliminationTactics.cmx \ - discriminationTactics.cmi + proofEngineTypes.cmx proofEngineStructuralRules.cmx \ + proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \ + equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi +substTactic.cmo: tacticals.cmi proofEngineTypes.cmi \ + proofEngineStructuralRules.cmi proofEngineHelpers.cmi equalityTactics.cmi \ + substTactic.cmi +substTactic.cmx: tacticals.cmx proofEngineTypes.cmx \ + proofEngineStructuralRules.cmx proofEngineHelpers.cmx equalityTactics.cmx \ + substTactic.cmi inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ equalityTactics.cmi inversion.cmi diff --git a/helm/software/components/tactics/Makefile b/helm/software/components/tactics/Makefile index cdb16efe4..a0b1b1cea 100644 --- a/helm/software/components/tactics/Makefile +++ b/helm/software/components/tactics/Makefile @@ -19,9 +19,8 @@ INTERFACE_FILES = \ variousTactics.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ equalityTactics.mli \ - auto.mli \ - autoTactic.mli \ - discriminationTactics.mli \ + auto.mli autoTactic.mli \ + discriminationTactics.mli substTactic.mli \ inversion.mli inversion_principle.mli ring.mli setoids.mli \ fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \ statefulProofEngine.mli tactics.mli declarative.mli diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml index a31b0f052..f284a2d1d 100644 --- a/helm/software/components/tactics/equalityTactics.ml +++ b/helm/software/components/tactics/equalityTactics.ml @@ -378,83 +378,3 @@ let transitivity_tac ~term = ProofEngineTypes.mk_tactic (transitivity_tac ~term) ;; -(* FG: subst tactic *********************************************************) - -(* FG: This should be replaced by T.try_tactic *) -let try_tactic ~tactic = - let try_tactic status = - try PET.apply_tactic tactic status with - | PET.Fail _ -> PET.apply_tactic T.id_tac status - in - PET.mk_tactic try_tactic - -let rec lift_rewrite_tac ~context ~direction ~pattern equality = - let lift_rewrite_tac status = - let (proof, goal) = status in - let (_, metasenv, _, _, _) = proof in - let _, new_context, _ = CicUtil.lookup_meta goal metasenv in - let n = List.length new_context - List.length context in - let equality = if n > 0 then S.lift n equality else equality in - PET.apply_tactic (rewrite_tac ~direction ~pattern equality []) status - in - PET.mk_tactic lift_rewrite_tac - - -let msg0 = lazy "Subst: not found in context" -let msg1 = lazy "Subst: not a simple equality" -let msg2 = lazy "Subst: recursive equation" - -let subst_tac ~hyp = - let hole = C.Implicit (Some `Hole) in - let subst_tac status = - let (proof, goal) = status in - let (_, metasenv, _, _, _) = proof in - let _, context, _ = CicUtil.lookup_meta goal metasenv in - let what = match PEH.get_rel context hyp with - | Some t -> t - | None -> raise (PET.Fail msg0) - in - let ty, _ = TC.type_of_aux' metasenv context what CicUniv.empty_ugraph in - let direction, i, t = match ty with - | (C.Appl [(C.MutInd (uri, 0, [])); _; C.Rel i; t]) - when LO.is_eq_URI uri -> `LeftToRight, i, t - | (C.Appl [(C.MutInd (uri, 0, [])); _; t; C.Rel i]) - when LO.is_eq_URI uri -> `RightToLeft, i, t - | _ -> raise (PET.Fail msg1) - in - let rewrite pattern = - let tactic = lift_rewrite_tac ~context ~direction ~pattern what in - try_tactic ~tactic - in - let var = match PEH.get_name context i with - | Some name -> name - | None -> raise (PET.Fail msg0) - in - if DTI.does_not_occur i t then () else raise (PET.Fail msg2); - let map self = function - | Some (C.Name s, _) when s <> self -> - Some (rewrite (None, [(s, hole)], None)) - | _ -> None - in - let rew_hips = HEL.list_rev_map_filter (map hyp) context in - let rew_concl = rewrite (None, [], Some hole) in - let clear = PESR.clear ~hyps:[hyp; var] in - let tactics = List.rev_append (rew_concl :: rew_hips) [clear] in - PET.apply_tactic (T.seq ~tactics) status - in - PET.mk_tactic subst_tac - -let subst_tac = - let subst hyp = try_tactic ~tactic:(subst_tac hyp) in - let map = function - | Some (C.Name s, _) -> Some (subst s) - | _ -> None - in - let subst_tac status = - let (proof, goal) = status in - let (_, metasenv, _, _, _) = proof in - let _, context, _ = CicUtil.lookup_meta goal metasenv in - let tactics = HEL.list_rev_map_filter map context in - PET.apply_tactic (T.seq ~tactics) status - in - PET.mk_tactic subst_tac diff --git a/helm/software/components/tactics/equalityTactics.mli b/helm/software/components/tactics/equalityTactics.mli index 52f2f2043..1aa48173c 100644 --- a/helm/software/components/tactics/equalityTactics.mli +++ b/helm/software/components/tactics/equalityTactics.mli @@ -40,8 +40,3 @@ val replace_tac: val reflexivity_tac: ProofEngineTypes.tactic val symmetry_tac: ProofEngineTypes.tactic val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic - -(* FG *) - -(* rewrites and clears all simple equalities in the context *) -val subst_tac: ProofEngineTypes.tactic diff --git a/helm/software/components/tactics/substTactic.ml b/helm/software/components/tactics/substTactic.ml new file mode 100644 index 000000000..1c0124648 --- /dev/null +++ b/helm/software/components/tactics/substTactic.ml @@ -0,0 +1,115 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module C = Cic +module DTI = DoubleTypeInference +module ET = EqualityTactics +module HEL = HExtlib +module LO = LibraryObjects +module PEH = ProofEngineHelpers +module PESR = ProofEngineStructuralRules +module PET = ProofEngineTypes +module S = CicSubstitution +module T = Tacticals +module TC = CicTypeChecker + +(* FG: This should be replaced by T.try_tactic *) +let try_tactic ~tactic = + let try_tactic status = + try PET.apply_tactic tactic status with + | PET.Fail _ -> PET.apply_tactic T.id_tac status + in + PET.mk_tactic try_tactic + +let rec lift_rewrite_tac ~context ~direction ~pattern equality = + let lift_rewrite_tac status = + let (proof, goal) = status in + let (_, metasenv, _, _, _) = proof in + let _, new_context, _ = CicUtil.lookup_meta goal metasenv in + let n = List.length new_context - List.length context in + let equality = if n > 0 then S.lift n equality else equality in + PET.apply_tactic (ET.rewrite_tac ~direction ~pattern equality []) status + in + PET.mk_tactic lift_rewrite_tac + + +let msg0 = lazy "Subst: not found in context" +let msg1 = lazy "Subst: not a simple equality" +let msg2 = lazy "Subst: recursive equation" + +let subst_tac ~hyp = + let hole = C.Implicit (Some `Hole) in + let subst_tac status = + let (proof, goal) = status in + let (_, metasenv, _, _, _) = proof in + let _, context, _ = CicUtil.lookup_meta goal metasenv in + let what = match PEH.get_rel context hyp with + | Some t -> t + | None -> raise (PET.Fail msg0) + in + let ty, _ = TC.type_of_aux' metasenv context what CicUniv.empty_ugraph in + let direction, i, t = match ty with + | (C.Appl [(C.MutInd (uri, 0, [])); _; C.Rel i; t]) + when LO.is_eq_URI uri -> `LeftToRight, i, t + | (C.Appl [(C.MutInd (uri, 0, [])); _; t; C.Rel i]) + when LO.is_eq_URI uri -> `RightToLeft, i, t + | _ -> raise (PET.Fail msg1) + in + let rewrite pattern = + let tactic = lift_rewrite_tac ~context ~direction ~pattern what in + try_tactic ~tactic + in + let var = match PEH.get_name context i with + | Some name -> name + | None -> raise (PET.Fail msg0) + in + if DTI.does_not_occur i t then () else raise (PET.Fail msg2); + let map self = function + | Some (C.Name s, _) when s <> self -> + Some (rewrite (None, [(s, hole)], None)) + | _ -> None + in + let rew_hips = HEL.list_rev_map_filter (map hyp) context in + let rew_concl = rewrite (None, [], Some hole) in + let clear = PESR.clear ~hyps:[hyp; var] in + let tactics = List.rev_append (rew_concl :: rew_hips) [clear] in + PET.apply_tactic (T.seq ~tactics) status + in + PET.mk_tactic subst_tac + +let subst_tac = + let subst hyp = try_tactic ~tactic:(subst_tac hyp) in + let map = function + | Some (C.Name s, _) -> Some (subst s) + | _ -> None + in + let subst_tac status = + let (proof, goal) = status in + let (_, metasenv, _, _, _) = proof in + let _, context, _ = CicUtil.lookup_meta goal metasenv in + let tactics = HEL.list_rev_map_filter map context in + PET.apply_tactic (T.seq ~tactics) status + in + PET.mk_tactic subst_tac diff --git a/helm/software/components/tactics/substTactic.mli b/helm/software/components/tactics/substTactic.mli new file mode 100644 index 000000000..cce9d0fe9 --- /dev/null +++ b/helm/software/components/tactics/substTactic.mli @@ -0,0 +1,27 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* rewrites and clears all simple equalities in the context *) +val subst_tac: ProofEngineTypes.tactic diff --git a/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml index 82c343085..358de1303 100644 --- a/helm/software/components/tactics/tactics.ml +++ b/helm/software/components/tactics/tactics.ml @@ -67,7 +67,7 @@ let ring = Ring.ring_tac let set_goal = ProofEngineStructuralRules.set_goal let simpl = ReductionTactics.simpl_tac let split = IntroductionTactics.split_tac -let subst = EqualityTactics.subst_tac +let subst = SubstTactic.subst_tac let symmetry = EqualityTactics.symmetry_tac let transitivity = EqualityTactics.transitivity_tac let unfold = ReductionTactics.unfold_tac diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index 4f2908706..f95c736bb 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Mar 16 19:03:48 CET 2007 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Apr 16 17:26:20 CEST 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : -- 2.39.2