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 let generalize_tac ~term ~status:((proof,goal) as status) =
  69   let module C = Cic in
  70   let module P = PrimitiveTactics in
  71   let module T = Tacticals in
  72    let _,metasenv,_,_ = proof in
  73     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
  74      T.thens
  75       ~start:(P.cut_tac
  76        ~term:(
  77          C.Prod (
  78           (C.Name "dummy_for_gen")),
  79           (CicTypeChecker.type_of_aux' metasenv context term)),
  80           (ProofEngineReduction.replace_lifting_csc 1
  81             ~equality:(==)
  82             ~what:term
  83             ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)
  84             ~where:ty)
  85           )
  86       ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
  87       ~status
  88 ;;
  89
  90
  91 (* IN FASE DI IMPLEMENTAZIONE *)
  92
  93 let decide_equality_tac =
  94   Tacticals.id_tac
  95 ;;
  96
  97 (*
  98 let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
  99   let module C = Cic in
 100   let module U = UriManager in
 101   let module P = PrimitiveTactics in
 102   let module T = Tacticals in
 103    let _,metasenv,_,_ = proof in
 104     let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
 105      if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2))
 106        (* controllo che i due termini siano comparabili *)
 107       then
 108        T.thens
 109          ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *)
 110          ~continuations:[split_tac ; P.intros_tac ~name:"FOO"]
 111       else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types")
 112 ;;
 113 *)
 114
 115
 116
 117 (*** DOMANDE ***
 118
 119 - field, omega... come ring?
 120
 121 *)