helm/ocaml/tactics/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
  28 chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
  29 funzione di callback che restituisce la (sola) hyp da applicare *)
  30
  31 let assumption_tac ~status:((proof,goal) as status) =
  32   let module C = Cic in
  33   let module R = CicReduction in
  34   let module S = CicSubstitution in
  35    let _,metasenv,_,_ = proof in
  36     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
  37      let rec find n = function
  38         hd::tl ->
  39          (match hd with
  40              (Some (_, C.Decl t)) when
  41                (R.are_convertible context (S.lift n t) ty) -> n
  42            | (Some (_, C.Def t)) when
  43                (R.are_convertible context
  44                 (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n
  45            | _ -> find (n+1) tl
  46          )
  47       | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption")
  48      in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
  49 ;;
  50
  51 (* Questa invece era in fourierR.ml
  52 let assumption_tac ~status:(proof,goal)=
  53   let curi,metasenv,pbo,pty = proof in
  54   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
  55   let num = ref 0 in
  56   let tac_list = List.map
  57         ( fun x -> num := !num + 1;
  58                 match x with
  59                   Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
  60                   | _ -> ("fake",tcl_fail 1)
  61         )
  62         context
  63   in
  64   Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
  65 ;;
  66 *)
  67
  68
  69 (* ANCORA DA DEBUGGARE *)
  70
  71 (* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda
  72 e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
  73 contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
  74
  75 let generalize_tac ~term ~status:((proof,goal) as status) =
  76   let module C = Cic in
  77   let module P = PrimitiveTactics in
  78   let module T = Tacticals in
  79    let _,metasenv,_,_ = proof in
  80     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
  81 (*
  82      let found = false in
  83      let rec new_context context ty =
  84       if ty == term then let found = true in context
  85        else match ty with
  86              C.Rel _
  87            | C.Var _
  88            | C.Meta _ (* ???? *)
  89            | C.Sort s
  90            | C.Implicit -> context
  91            | C.Cast (val,typ) ->
  92               let tmp_context = new_context context val in
  93                tmp_context @ (new_context tmp_context typ)
  94            | C.Prod (binder, source, target) ->
  95            | C.Lambda (binder, source, target) ->
  96               let tmp_context = new_context context source in
  97                tmp_context @ (new_context tmp_context binder)
  98            | C.LetIn (binder, term, target) ->
  99            | C.Appl applist ->
 100               let rec aux context =
 101                match applist with
 102                   [] -> context
 103                 | hd::tl ->
 104                    let tmp_context = (new_context context hd)
 105                    in aux tmp_context tl
 106               in aux context applist
 107            | C.Const (uri, exp_named_subst)
 108            | C.MutInd (uri, typeno, exp_named_subst)
 109            | C.MutConstruct (uri, typeno, consno, exp_named_subst) ->
 110               match exp_named_subst with
 111                  [] -> context
 112                | (uri,t)::_ -> new_context context (type_of_aux' context t)
 113                | _ -> assert false
 114            | C.MutCase (uri, typeno, outtype, iterm, patterns)
 115            | C.Fix (funno, funlist)
 116            | C.CoFix (funno, funlist) ->
 117               match funlist with
 118                  [] -> context (* caso possibile? *)
 119                | (name, index, type, body)::_ ->
 120                   let tmp_context = ~
 121      in
 122 *)
 123      T.thens
 124       ~start:(P.cut_tac
 125        ~term:(
 126          C.Prod(
 127           (C.Name "dummy_for_gen"),
 128           (CicTypeChecker.type_of_aux' metasenv context term),
 129           (ProofEngineReduction.replace_lifting_csc 1
 130             ~equality:(==)
 131             ~what:term
 132             ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)
 133             ~where:ty)
 134         )))
 135       ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
 136       ~status
 137 ;;
 138
 139
 140 (* IN FASE DI IMPLEMENTAZIONE *)
 141
 142 let decide_equality_tac =
 143 (* il goal e' un termine della forma t1=t2\/~t1=t2; la tattica decide se l'uguaglianza
 144 e' vera o no e lo risolve *)
 145   Tacticals.id_tac
 146 ;;
 147
 148
 149 let compare_tac ~term ~status:((proof, goal) as status) =
 150 (* term is in the form t1=t2; the tactic leaves two goals: in the first you have to          *)
 151 (* demonstrate the goal with the additional hyp that t1=t2, in the second the hyp is ~t1=t2  *)
 152   let module C = Cic in
 153   let module U = UriManager in
 154   let module P = PrimitiveTactics in
 155   let module T = Tacticals in
 156    let _,metasenv,_,_ = proof in
 157     let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
 158      let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
 159       match termty with
 160          (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
 161
 162           let term' = (* (t1=t2)\/~(t1=t2) *)
 163            C.Appl [
 164             (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ;
 165             term ;
 166             C.Appl [
 167              (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 1, [])) ;
 168              t1 ;
 169              C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2]
 170             ]
 171            ]
 172           in
 173             T.thens
 174                ~start:(P.cut_tac ~term:term')
 175                ~continuations:[
 176                  T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ;
 177                  decide_equality_tac]
 178       | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
 179           let term' = (* (t1=t2) \/ ~(t1=t2) *)
 180            C.Appl [
 181             (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ;
 182             term ;
 183             C.Appl [
 184              (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind"), 1, [])) ;
 185              t1 ;
 186              C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2]
 187             ]
 188            ]
 189           in
 190             T.thens
 191                ~start:(P.cut_tac ~term:term')
 192                ~continuations:[
 193                  T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ;
 194                  decide_equality_tac]
 195       | _ -> raise (ProofEngineTypes.Fail "Compare: Not an equality")
 196 ;;
 197
 198
 199 let discriminate_tac ~term ~status:((proof, goal) as status) =
 200   let module C = Cic in
 201   let module U = UriManager in
 202   let module P = PrimitiveTactics in
 203   let module T = Tacticals in
 204    T.id_tac
 205 ;;
 206