helm/gTopLevel/variousTactics.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
  27 (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *)
  28 let assumption_tac ~status:((proof,goal) as status) =
  29   let module C = Cic in
  30   let module R = CicReduction in
  31   let module S = CicSubstitution in
  32    let _,metasenv,_,_ = proof in
  33     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
  34      let rec find n = function
  35         hd::tl ->
  36          (match hd with
  37              (Some (_, C.Decl t)) when
  38                (R.are_convertible context (S.lift n t) ty) -> n
  39            | (Some (_, C.Def t)) when
  40                (R.are_convertible context
  41                 (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n
  42            | _ -> find (n+1) tl
  43          )
  44       | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption")
  45      in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
  46 ;;
  47
  48 (* Questa invece era in fourierR.ml
  49 let assumption_tac ~status:(proof,goal)=
  50   let curi,metasenv,pbo,pty = proof in
  51   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
  52   let num = ref 0 in
  53   let tac_list = List.map
  54         ( fun x -> num := !num + 1;
  55                 match x with
  56                   Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
  57                   | _ -> ("fake",tcl_fail 1)
  58         )
  59         context
  60   in
  61   Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
  62 ;;
  63 *)
  64
  65
  66 (* ANCORA DA DEBUGGARE *)
  67
  68
  69 (* IN FASE DI IMPLEMENTAZIONE *)
  70
  71 let generalize_tac ~term ~status:((proof,goal) as status) =
  72   let module C = Cic in
  73   let module P = PrimitiveTactics in
  74   let module T = Tacticals in
  75    let _,metasenv,_,_ = proof in
  76     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
  77
  78 (*
  79 let uno = (C.Appl [
  80              C.MutConstruct (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", 0, 2, []) ;
  81              C.MutConstruct (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", 0, 1, [])])  in
  82  let tuno = CicTypeChecker.type_of_aux' metasenv context uno in
  83 prerr_endline ("#### uno: " ^ CicPp.ppterm uno);
  84 prerr_endline ("#### tuno: " ^ CicPp.ppterm tuno);
  85 *)
  86 prerr_endline ("#### dummy: " ^ (CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv context term)));
  87 prerr_endline ("#### with_what: " ^ CicPp.ppterm (C.Rel 1));
  88 prerr_endline ("#### term: " ^ CicPp.ppterm term);
  89 prerr_endline ("#### ty: " ^ CicPp.ppterm ty);
  90
  91
  92      T.thens
  93       ~start:(P.cut_tac
  94        ~term:(
  95          C.Prod (
  96           (C.Name "dummy_for_gen"),
  97           (CicTypeChecker.type_of_aux' metasenv context term),
  98           (ProofEngineReduction.replace_lifting
  99             ~equality:(==)
 100             ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)
 101             ~what:term
 102             ~where:ty))))
 103       ~continuations:
 104        [T.id_tac ; (P.apply_tac ~term:(C.Appl [(C.Rel 1); term]))]      (* in quest'ordine o viceversa? provare *)
 105 (*       [(P.apply_tac ~term:(C.Appl [(C.Rel 1); term])) ; T.id_tac]    (* in quest'ordine o viceversa? provare *)*)
 106       ~status
 107 ;;
 108
 109 (*
 110 let generalize_tac ~term ~status:((proof,goal) as status) =
 111   let module C = Cic in
 112   let module H = ProofEngineHelpers in
 113   let module P = PrimitiveTactics in
 114   let module T = Tacticals in
 115    let _,metasenv,_,_ = proof in
 116     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 117
 118      let add_decl_tac ~term ~status:(proof, goal) =
 119       let module C = Cic in
 120       let curi,metasenv,pbo,pty = proof in
 121       let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 122        let _ = CicTypeChecker.type_of_aux' metasenv context term in
 123         let newmeta = H.new_meta ~proof in
 124         let context_for_newmeta = (Some (C.Name "dummy_for_gen",C.Decl term))::context in
 125         let irl = H.identity_relocation_list_for_metavariable context_for_newmeta in
 126          let newmetaty = CicSubstitution.lift 1 ty in
 127          let bo' = C.LetIn (C.Name "dummy_for_gen" , term , C.Meta (newmeta,irl)) in
 128           let (newproof, _) = H.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty]
 129          in
 130           (newproof, [newmeta])
 131
 132      in
 133       T.then_
 134        ~start:(add_decl_tac ~term:(CicTypeChecker.type_of_aux' metasenv context term))
 135        ~continuation:(
 136 T.id_tac) (*         T.thens
 137           ~start:(P.cut_tac ~term:(ProofEngineReduction.replace
 138             ~equality:(==)
 139             ~with_what:(C.Rel 1) (* dummy_for_gen *)
 140             ~what:term
 141             ~where:ty))
 142           ~continuations:
 143             [T.id_tac ; (P.apply_tac ~term:(C.Appl [term ; (C.Rel 1)]))])       (* in quest'ordine o viceversa? provare *)
 144 (*            [(P.apply_tac ~term:(C.Appl [term ; (C.Rel 1)])) ; T.id_tac])     in quest'ordine o viceversa? provare *)
 145 *)      ~status
 146 ;;
 147 *)
 148
 149
 150
 151 let decide_equality_tac =
 152   Tacticals.id_tac
 153 ;;
 154
 155 (*
 156 let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
 157   let module C = Cic in
 158   let module U = UriManager in
 159   let module P = PrimitiveTactics in
 160   let module T = Tacticals in
 161    let _,metasenv,_,_ = proof in
 162     let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
 163      if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2))
 164        (* controllo che i due termini siano comparabili *)
 165       then
 166        T.thens
 167          ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *)
 168          ~continuations:[split_tac ; P.intros_tac ~name:"FOO"]
 169       else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types")
 170 ;;
 171 *)
 172
 173
 174
 175 (*** DOMANDE ***
 176
 177 - come faccio clear di un ipotesi di cui non so il nome?
 178 - differenza tra elim e induction ...e inversion?
 179 - come passo a decompose la lista di termini?
 180 - ma la rewrite funzionava?
 181 - come implemento la generalize?
 182
 183 *)