+++ /dev/null
-(* 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 DT = DiscriminationTactics
-module DTI = DoubleTypeInference
-module ET = EqualityTactics
-module HEL = HExtlib
-module LO = LibraryObjects
-module PEH = ProofEngineHelpers
-module PESR = ProofEngineStructuralRules
-module PET = ProofEngineTypes
-module RT = ReductionTactics
-module S = CicSubstitution
-module T = Tacticals
-module TC = CicTypeChecker
-
-let lift_rewrite_tac ~context ~direction ~pattern equality =
- let lift_rewrite_tac status =
- let (proof, goal) = status in
- let (_, metasenv, _subst, _, _, _) = proof in
- let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
- let n = List.length new_context - List.length context in
- let equality = S.lift n equality in
- PET.apply_tactic (ET.rewrite_tac ~direction ~pattern equality []) status
- in
- PET.mk_tactic lift_rewrite_tac
-
-let lift_destruct_tac ~context ~what =
- let lift_destruct_tac status =
- let (proof, goal) = status in
- let (_, metasenv, _subst, _, _, _) = proof in
- let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
- let n = List.length new_context - List.length context in
- let what = S.lift n what in
- PET.apply_tactic (DT.destruct_tac ~term:what) status
- in
- PET.mk_tactic lift_destruct_tac
-
-let msg0 = lazy "Subst: not found in context"
-let msg1 = lazy "Subst: not an erasable equation"
-let msg2 = lazy "Subst: recursive equation"
-let msg3 = lazy "Subst: no progress"
-
-let rec subst_tac ~try_tactic ~hyp =
- let hole = C.Implicit (Some `Hole) in
- let meta = C.Implicit None in
- let rec ind = function
- | C.MutInd _ -> true
- | C.Appl (t :: tl) -> ind t
- | _ -> false
- in
- let rec constr = function
- | C.MutConstruct _ -> true
- | C.Appl (t :: tl) -> constr t
- | _ -> false
- in
- let subst_tac status =
- let (proof, goal) = status in
- let (_, metasenv, _subst, _, _, _) = 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 subst_g direction i t =
- 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
- List.rev_append (rew_concl :: rew_hips) [clear]
- in
- let destruct_g () =
- [lift_destruct_tac ~context ~what; PESR.clear ~hyps:[hyp]]
- in
- let whd_g () =
- let whd_pattern = C.Appl [meta; hole; hole; hole] in
- let pattern = None, [hyp, whd_pattern], None in
- [RT.whd_tac ~pattern; subst_tac ~try_tactic ~hyp]
- in
- let tactics = match ty with
- | (C.Appl [(C.MutInd (uri, 0, [])); _; C.Rel i; t])
- when LO.is_eq_URI uri -> subst_g `LeftToRight i t
- | (C.Appl [(C.MutInd (uri, 0, [])); _; t; C.Rel i])
- when LO.is_eq_URI uri -> subst_g `RightToLeft i t
- | (C.Appl [(C.MutInd (uri, 0, [])); t; t1; t2])
- when LO.is_eq_URI uri && ind t && constr t1 && constr t2 -> destruct_g ()
- | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2])
- when LO.is_eq_URI uri -> whd_g ()
- | _ -> raise (PET.Fail msg1)
- in
- PET.apply_tactic (T.seq ~tactics) status
- in
- PET.mk_tactic subst_tac
-
-let subst_tac =
- let subst_tac status =
- let progress = ref false in
- let try_tactic ~tactic =
- let try_tactic status =
- try
- let result = PET.apply_tactic tactic status in
- progress := true; result
- with
- | PET.Fail _ -> PET.apply_tactic T.id_tac status
- in
- PET.mk_tactic try_tactic
- in
- let subst hyp = try_tactic ~tactic:(subst_tac ~try_tactic ~hyp) in
- let map = function
- | Some (C.Name s, _) -> Some (subst s)
- | _ -> None
- in
- let (proof, goal) = status in
- let (_, metasenv, _subst, _, _, _) = proof in
- let _, context, _ = CicUtil.lookup_meta goal metasenv in
- let tactics = HEL.list_rev_map_filter map context in
- let result = PET.apply_tactic (T.seq ~tactics) status in
- if !progress then result else raise (PET.Fail msg3)
- in
- PET.mk_tactic subst_tac
-
- let try_tac tactic = T.try_tactic ~tactic
- let then_tac start continuation = T.then_ ~start ~continuation
-
-let subst_tac =
- let tactic = T.repeat_tactic ~tactic:subst_tac in
- T.try_tactic ~tactic
projects / helm.git / blobdiff