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 (* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda
  69 e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
  70 contesto e si lifta *)
  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      T.thens
  78       ~start:(P.cut_tac
  79        ~term:(
  80          C.Prod(
  81           (C.Name "dummy_for_gen"),
  82           (CicTypeChecker.type_of_aux' metasenv context term),
  83           (ProofEngineReduction.replace_lifting_csc 1
  84             ~equality:(==)
  85             ~what:term
  86             ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)
  87             ~where:ty)
  88         )))
  89       ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
  90       ~status
  91 ;;
  92
  93
  94 (* IN FASE DI IMPLEMENTAZIONE *)
  95
  96 let decide_equality_tac =
  97   Tacticals.id_tac
  98 ;;
  99
 100 (*
 101 let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
 102   let module C = Cic in
 103   let module U = UriManager in
 104   let module P = PrimitiveTactics in
 105   let module T = Tacticals in
 106    let _,metasenv,_,_ = proof in
 107     let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
 108      if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2))
 109        (* controllo che i due termini siano comparabili *)
 110       then
 111        T.thens
 112          ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *)
 113          ~continuations:[split_tac ; P.intros_tac ~name:"FOO"]
 114       else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types")
 115 ;;
 116 *)
 117