helm/software/components/tactics/eliminationTactics.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 (* $Id$ *)
  27
  28 module C    = Cic
  29 module I    = CicInspect
  30 module S    = CicSubstitution
  31 module TC   = CicTypeChecker
  32 module P    = PrimitiveTactics
  33 module T    = Tacticals
  34 module PESR = ProofEngineStructuralRules
  35 module F    = FreshNamesGenerator
  36 module PET  = ProofEngineTypes
  37 module RT   = ReductionTactics
  38 module E    = CicEnvironment
  39 module R    = CicReduction
  40 module Un   = CicUniv
  41 module PEH  = ProofEngineHelpers
  42
  43 let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None
  44
  45 let get_inductive_def uri =
  46    match E.get_obj Un.oblivion_ugraph uri with
  47       | C.InductiveDefinition (tys, _, lpsno, _), _ ->
  48          lpsno, tys
  49       | _                                           -> assert false
  50
  51 let is_not_recursive uri tyno tys =
  52    let map mutinds (_, ty) =
  53 (* FG: we can do much better here *)
  54       let map mutinds (_, t) = I.S.union mutinds (I.get_mutinds_of_uri uri t) in
  55 (**********************************)
  56       let premises, _ = PEH.split_with_whd ([], ty) in
  57       List.fold_left map mutinds (List.tl premises)
  58    in
  59    let msg = "recursiveness check non implemented for mutually inductive types" in
  60    if List.length tys > 1 then raise (PET.Fail (lazy msg)) else
  61    let _, _, _, constructors = List.nth tys tyno in
  62    let mutinds = List.fold_left map I.S.empty constructors in
  63    I.S.is_empty mutinds
  64
  65 let rec check_type sorts metasenv context t =
  66    match R.whd ~delta:true context t with
  67       | C.MutInd (uri, tyno, _) as t ->
  68          let lpsno, tys = get_inductive_def uri in
  69          let _, inductive, arity, _ = List.nth tys tyno in
  70          let _, psno = PEH.split_with_whd ([], arity) in
  71          let not_relation = (lpsno = psno) in
  72          let not_recursive = is_not_recursive uri tyno tys in
  73          let ty_ty, _ = TC.type_of_aux' metasenv context t Un.oblivion_ugraph in
  74          let sort = match PEH.split_with_whd (context, ty_ty) with
  75             | (_, C.Sort sort) ::_ , _ -> CicPp.ppsort sort
  76             | (_, C.Meta _) :: _, _    -> CicPp.ppsort (C.Type (Un.fresh ()))
  77             | _                        -> assert false
  78          in
  79          let right_sort = List.mem sort sorts in
  80          if not_relation && inductive && not_recursive && right_sort then
  81          begin
  82             HLog.warn (Printf.sprintf "Decomposing %s %u" (UriManager.string_of_uri uri) (succ tyno));
  83             true
  84          end
  85          else false
  86       | C.Appl (hd :: tl)         -> check_type sorts metasenv context hd
  87       | _                         -> false
  88
  89 (* unexported tactics *******************************************************)
  90
  91 let rec scan_tac ~old_context_length ~index ~tactic =
  92    let scan_tac status =
  93       let (proof, goal) = status in
  94       let _, metasenv, _subst, _, _, _ = proof in
  95       let _, context, _ = CicUtil.lookup_meta goal metasenv in
  96       let context_length = List.length context in
  97       let rec aux index =
  98          match PEH.get_name context index with
  99             | _ when index <= 0 -> (proof, [goal])
 100             | None              -> aux (pred index)
 101             | Some what         ->
 102                let tac = T.then_ ~start:(tactic ~what)
 103                                  ~continuation:(scan_tac ~old_context_length:context_length ~index ~tactic)
 104                in
 105                try PET.apply_tactic tac status
 106                with PET.Fail _ -> aux (pred index)
 107       in aux (index + context_length - old_context_length)
 108    in
 109    PET.mk_tactic scan_tac
 110
 111 let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
 112    let elim_clear_unfold_tac status =
 113       let (proof, goal) = status in
 114       let _, metasenv, _subst, _, _, _ = proof in
 115       let _, context, _ = CicUtil.lookup_meta goal metasenv in
 116       let index, ty = PEH.lookup_type metasenv context what in
 117       let tac =
 118          if check_type sorts metasenv context (S.lift index ty) then
 119             T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
 120                     ~continuation:(PESR.clear [what])
 121          else
 122             let msg = "unexported elim_clear: not an decomposable type" in
 123             raise (PET.Fail (lazy msg))
 124       in
 125       PET.apply_tactic tac status
 126    in
 127    PET.mk_tactic elim_clear_unfold_tac
 128
 129 (* elim type ****************************************************************)
 130
 131 let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth
 132   ?using what
 133 =
 134   let elim =
 135     P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback
 136   in
 137   let elim_type_tac status =
 138     let tac =
 139       T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac]
 140     in
 141     PET.apply_tactic tac status
 142   in
 143   PET.mk_tactic elim_type_tac
 144
 145 (* decompose ****************************************************************)
 146
 147 (* robaglia --------------------------------------------------------------- *)
 148
 149   (** perform debugging output? *)
 150 let debug = false
 151 let debug_print = fun _ -> ()
 152
 153   (** debugging print *)
 154 let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s)))
 155
 156 (* roba seria ------------------------------------------------------------- *)
 157
 158 let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort (C.CProp (CicUniv.fresh ()))])
 159                   ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
 160    let decompose_tac status =
 161       let (proof, goal) = status in
 162       let _, metasenv, _subst, _,_, _ = proof in
 163       let _, context, _ = CicUtil.lookup_meta goal metasenv in
 164       let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in
 165       let old_context_length = List.length context in
 166       let tac = scan_tac ~old_context_length ~index:old_context_length ~tactic
 167       in
 168       PET.apply_tactic tac status
 169    in
 170    PET.mk_tactic decompose_tac