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
  88
  89
  90
  91
  92
  93
  94
  95 (*
  96    let count_dependent_prods context t =
  97       let rec aux context p = function
  98          | Cic.Prod (name, t1, t2) ->
  99             if TC.does_not_occur context 0 1 t2 then p else
 100             let e = Some (name, Cic.Decl t1) in
 101             aux (e :: context) (succ p) t2
 102          | t                       -> p
 103       in
 104       aux context 0 t
 105    in
 106    let rec pad_context p context add_context =
 107       if List.length add_context >= p then add_context @ context
 108       else pad_context p context (None :: add_context)
 109    in
 110    let strip_dependent_prods metasenv context p t =
 111       let rec aux metasenv add_context q = function
 112          | Cic.Prod (name, t1, t2) when q > 0 ->
 113             let context_for_meta = pad_context p context add_context in
 114             let metasenv, index = MI.mk_implicit metasenv [] context_for_meta in
 115             let rs = MI.identity_relocation_list_for_metavariable context_for_meta in
 116             let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, rs) in
 117             aux metasenv (e :: add_context) (pred q) (S.subst s t2)
 118          | t                                  -> metasenv, add_context, t
 119       in
 120       aux metasenv [] p t
 121    in
 122    let mk_body bo = function
 123       | Some (name, Cic.Decl t1) -> Cic.Lambda (name, t1, bo)
 124       | _                        -> failwith "mk_body"
 125    in
 126    let lapply_tac (proof, goal) =
 127       let xuri, metasenv, u, t = proof in
 128 (* preliminaries *)
 129       let metano, context, ty = CicUtil.lookup_meta goal metasenv in
 130       let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
 131       let p = count_dependent_prods context lemma in
 132 (* stripping *)
 133       let metasenv, add_context, holed_lemma = strip_dependent_prods metasenv context p lemma in
 134       let proof = xuri, metasenv, u, t in
 135       let newmeta = MI.new_meta metasenv [] in
 136       let context = add_context @ context in
 137       let irl = MI.identity_relocation_list_for_metavariable context in
 138       let bo = List.fold_left mk_body (Cic.Meta (newmeta, irl)) add_context in
 139       let ty = S.lift p ty in
 140       let (xuri, metasenv, u, t), _ =
 141          PEH.subst_meta_in_proof proof metano bo [newmeta, context, ty]
 142       in
 143       prerr_endline (CicPp.ppterm holed_lemma);
 144 (* cut *)
 145       let status = (xuri, metasenv, u, t), newmeta in
 146       PET.apply_tactic (PT.cut_tac ~mk_fresh_name_callback holed_lemma) status
 147    in
 148    PET.mk_tactic lapply_tac
 149 *)
 150 (* fwd **********************************************************************)
 151
 152 let fwd_simpl_tac ~what ~dbd =
 153    let fwd_simpl_tac status =
 154       let (proof, goal) = status in
 155       let _, metasenv, _, _ = proof in
 156       let _, context, ty = CicUtil.lookup_meta goal metasenv in
 157       let major, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
 158       match MetadataQuery.fwd_simpl ~dbd major with
 159          | []       -> error fail_msg1
 160          | uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, [])
 161    in
 162    PET.mk_tactic fwd_simpl_tac