helm/ocaml/tactics/fwdSimplTactic.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 MI = CicMkImplicit
  27 module TC = CicTypeChecker
  28 module PET = ProofEngineTypes
  29 module PEH = ProofEngineHelpers
  30 module U  = CicUniv
  31 module S = CicSubstitution
  32 module PT = PrimitiveTactics
  33 module T = Tacticals
  34
  35 let fail_msg1 = "no applicable simplification"
  36
  37 let error msg = raise (PET.Fail msg)
  38
  39 (* lapply *******************************************************************)
  40
  41 let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
  42                (* ?(substs = []) *) ?to_what what =
  43    let cut_tac term = PT.cut_tac ~mk_fresh_name_callback term in
  44    let apply_tac term = PT.apply_tac term in
  45    let strip_dependent_prods metasenv context t =
  46       let irl = MI.identity_relocation_list_for_metavariable context in
  47       let rec aux metasenv p xcontext = function
  48          | Cic.Prod (name, t1, t2) when not (TC.does_not_occur xcontext 0 1 t2) ->
  49             let index = MI.new_meta metasenv [] in
  50             let metasenv = [index, context, t1] @ metasenv in
  51             let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, irl) in
  52             aux metasenv (succ p) (e :: xcontext) (S.subst s t2)
  53          | Cic.Prod (name, t1, t2) -> metasenv, p, Some t1, t2
  54          | t                       -> metasenv, p, None, t
  55       in
  56       aux metasenv 0 context t
  57    in
  58    let rec mk_continuations p l =
  59       if p <= 0 then l else mk_continuations (pred p) (T.id_tac :: l)
  60    in
  61    let lapply_tac (proof, goal) =
  62       let xuri, metasenv, u, t = proof in
  63       let _, context, _ = CicUtil.lookup_meta goal metasenv in
  64       let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
  65       match strip_dependent_prods metasenv context lemma with
  66          | metasenv, p, Some premise, conclusion ->
  67             let premise_tac =
  68                match to_what with
  69                   | None      -> T.id_tac
  70                   | Some term -> PT.apply_tac term
  71             in
  72             let status = (xuri, metasenv, u, t), goal in
  73             let tac = T.thens ~start:(cut_tac premise)
  74                               ~continuations:[
  75                       T.thens ~start:(cut_tac conclusion)
  76                               ~continuations:[ T.id_tac;
  77                       T.thens ~start:(PT.apply_tac what)
  78                               ~continuations:(mk_continuations p [PT.apply_tac ~term:(Cic.Rel 1)])
  79                                              ]; premise_tac ]
  80             in
  81             PET.apply_tactic tac status
  82          | metasenv, p, None, conclusion         ->
  83             failwith "lapply_tac: not implemented"
  84    in
  85    PET.mk_tactic lapply_tac
  86
  87 (* fwd **********************************************************************)
  88
  89 let fwd_simpl_tac ~what ~dbd =
  90    let fwd_simpl_tac status =
  91       let (proof, goal) = status in
  92       let _, metasenv, _, _ = proof in
  93       let _, context, ty = CicUtil.lookup_meta goal metasenv in
  94       let major, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
  95       match MetadataQuery.fwd_simpl ~dbd major with
  96          | []       -> error fail_msg1
  97          | uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, [])
  98    in
  99    PET.mk_tactic fwd_simpl_tac