components/tactics/substTactic.ml

   1 (* Copyright (C) 2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 module C    = Cic
  27 module DTI  = DoubleTypeInference
  28 module ET   = EqualityTactics
  29 module HEL  = HExtlib
  30 module LO   = LibraryObjects
  31 module PEH  = ProofEngineHelpers
  32 module PESR = ProofEngineStructuralRules
  33 module PET  = ProofEngineTypes
  34 module S    = CicSubstitution
  35 module T    = Tacticals
  36 module TC   = CicTypeChecker
  37
  38 (* FG: This should be replaced by T.try_tactic *)
  39 let try_tactic ~tactic =
  40    let try_tactic status =
  41       try PET.apply_tactic tactic status with
  42          | PET.Fail _ -> PET.apply_tactic T.id_tac status
  43    in
  44    PET.mk_tactic try_tactic
  45
  46 let rec lift_rewrite_tac ~context ~direction ~pattern equality =
  47    let lift_rewrite_tac status =
  48       let (proof, goal) = status in
  49       let (_, metasenv, _, _, _) = proof in
  50       let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
  51       let n = List.length new_context - List.length context in
  52       let equality = if n > 0 then S.lift n equality else equality in
  53       PET.apply_tactic (ET.rewrite_tac ~direction ~pattern equality []) status
  54    in
  55    PET.mk_tactic lift_rewrite_tac
  56
  57
  58 let msg0 = lazy "Subst: not found in context"
  59 let msg1 = lazy "Subst: not a simple equality"
  60 let msg2 = lazy "Subst: recursive equation"
  61
  62 let subst_tac ~hyp =
  63    let hole = C.Implicit (Some `Hole) in
  64    let subst_tac status =
  65       let (proof, goal) = status in
  66       let (_, metasenv, _, _, _) = proof in
  67       let _, context, _ = CicUtil.lookup_meta goal metasenv in
  68       let what = match PEH.get_rel context hyp with
  69          | Some t -> t
  70          | None   -> raise (PET.Fail msg0)
  71       in
  72       let ty, _ = TC.type_of_aux' metasenv context what CicUniv.empty_ugraph in
  73       let direction, i, t = match ty with
  74          | (C.Appl [(C.MutInd (uri, 0, [])); _; C.Rel i; t])
  75             when LO.is_eq_URI uri -> `LeftToRight, i, t
  76          | (C.Appl [(C.MutInd (uri, 0, [])); _; t; C.Rel i])
  77             when LO.is_eq_URI uri -> `RightToLeft, i, t
  78          | _ -> raise (PET.Fail msg1)
  79       in
  80       let rewrite pattern =
  81          let tactic = lift_rewrite_tac ~context ~direction ~pattern what in
  82          try_tactic ~tactic
  83       in
  84       let var = match PEH.get_name context i with
  85          | Some name -> name
  86          | None      -> raise (PET.Fail msg0)
  87       in
  88       if DTI.does_not_occur i t then () else raise (PET.Fail msg2);
  89       let map self = function
  90          | Some (C.Name s, _) when s <> self ->
  91             Some (rewrite (None, [(s, hole)], None))
  92          | _                                 -> None
  93       in
  94       let rew_hips = HEL.list_rev_map_filter (map hyp) context in
  95       let rew_concl = rewrite (None, [], Some hole) in
  96       let clear = PESR.clear ~hyps:[hyp; var] in
  97       let tactics = List.rev_append (rew_concl :: rew_hips) [clear] in
  98       PET.apply_tactic (T.seq ~tactics) status
  99    in
 100    PET.mk_tactic subst_tac
 101
 102 let subst_tac =
 103    let subst hyp = try_tactic ~tactic:(subst_tac hyp) in
 104    let map = function
 105       | Some (C.Name s, _) -> Some (subst s)
 106       | _                  -> None
 107    in
 108    let subst_tac status =
 109       let (proof, goal) = status in
 110       let (_, metasenv, _, _, _) = proof in
 111       let _, context, _ = CicUtil.lookup_meta goal metasenv in
 112       let tactics = HEL.list_rev_map_filter map context in
 113       PET.apply_tactic (T.seq ~tactics) status
 114    in
 115    PET.mk_tactic subst_tac