components/tactics/declarative.ml

   1 (* Copyright (C) 2006, 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 let assume id t =
  27   Tacticals.then_
  28      ~start:
  29        (Tactics.intros ~howmany:1
  30         ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
  31      ~continuation:
  32        (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
  33          (fun _ metasenv ugraph -> t,metasenv,ugraph))
  34 ;;
  35
  36 let suppose t id ty =
  37 (*BUG: check on t missing *)
  38  let ty = match ty with None -> t | Some ty -> ty in
  39  Tacticals.then_
  40    ~start:
  41      (Tactics.intros ~howmany:1
  42        ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
  43    ~continuation:
  44      (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
  45       (fun _ metasenv ugraph -> ty,metasenv,ugraph))
  46 ;;
  47
  48 let by_term_we_proved t ty id ty' =
  49  match t with
  50     None -> assert false
  51   | Some t ->
  52      let continuation =
  53       match ty' with
  54          None -> Tacticals.id_tac
  55        | Some ty' ->
  56           Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
  57            (fun _ metasenv ugraph -> ty,metasenv,ugraph)
  58      in
  59       Tacticals.thens
  60       ~start:
  61         (Tactics.cut ty
  62           ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
  63       ~continuations:
  64         [ continuation ; Tactics.apply t ]
  65 ;;
  66
  67 let bydone t =
  68    match t with
  69     None -> assert false
  70   | Some t ->
  71     (Tactics.apply ~term:t)
  72 ;;
  73
  74 let we_need_to_prove t id ty =
  75  let aux status =
  76   let cont,cutted =
  77    match ty with
  78       None -> Tacticals.id_tac,t
  79     | Some ty ->
  80        Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
  81          (fun _ metasenv ugraph -> t,metasenv,ugraph), ty in
  82   let proof,goals =
  83    ProofEngineTypes.apply_tactic
  84     (Tacticals.thens
  85       ~start:
  86        (Tactics.cut cutted
  87          ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
  88       ~continuations:[cont])
  89     status
  90   in
  91    let goals' =
  92     match goals with
  93        [fst; snd] -> [snd; fst]
  94      | _ -> assert false
  95    in
  96     proof,goals'
  97  in
  98   ProofEngineTypes.mk_tactic aux
  99 ;;
 100
 101 let existselim t id1 t1 id2 t2 =
 102 (*BUG: t1 and t2 not used *)
 103 (*PARSING BUG: t2 is parsed in the current context, but it may
 104   have occurrences of id1 in it *)
 105  Tactics.elim_intros t
 106   ~mk_fresh_name_callback:
 107     (let i = ref 0 in
 108       fun _ _ _  ~typ ->
 109        incr i;
 110        if !i = 1 then Cic.Name id1 else Cic.Name id2)
 111
 112 let andelim = existselim;;
 113
 114 let rewritingstep lhs rhs just conclude =
 115  let aux ((proof,goal) as status) =
 116   let (curi,metasenv,proofbo,proofty) = proof in
 117   let _,context,_ = CicUtil.lookup_meta goal metasenv in
 118   let eq,trans =
 119    match LibraryObjects.eq_URI () with
 120       None -> assert false (*TODO*)
 121     | Some uri ->
 122       Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
 123   in
 124   let ty,_ =
 125    CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
 126   let just =
 127    match just with
 128       None -> assert false (*TOOD*)
 129     | Some just -> just
 130   in
 131    match lhs with
 132       None ->
 133        let plhs,prhs =
 134         match
 135          fst
 136           (CicTypeChecker.type_of_aux' metasenv context (Cic.Rel 1)
 137             CicUniv.empty_ugraph)
 138         with
 139            Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
 140          | _ -> assert false in
 141        let last_hyp_name =
 142         match context with
 143            (Some (Cic.Name id,_))::_ -> id
 144          | _ -> assert false
 145        in
 146         (match conclude with
 147             None ->
 148              ProofEngineTypes.apply_tactic
 149               (Tacticals.thens
 150                 ~start:(Tactics.apply ~term:trans)
 151                 ~continuations:
 152                   [ Tactics.apply prhs ;
 153                     Tactics.apply (Cic.Rel 1) ;
 154                     Tactics.apply just]) status
 155           | Some name ->
 156              let mk_fresh_name_callback =
 157               fun metasenv context _ ~typ ->
 158                 FreshNamesGenerator.mk_fresh_name ~subst:[]
 159                  metasenv context name ~typ
 160              in
 161               ProofEngineTypes.apply_tactic
 162                (Tacticals.thens
 163                  ~start:(Tactics.cut ~mk_fresh_name_callback
 164                   (Cic.Appl [eq ; ty ; plhs ; rhs]))
 165                  ~continuations:
 166                    [ Tactics.clear ~hyps:[last_hyp_name] ;
 167                      Tacticals.thens
 168                       ~start:(Tactics.apply ~term:trans)
 169                       ~continuations:
 170                         [ Tactics.apply prhs ;
 171                           Tactics.apply (Cic.Rel 1) ;
 172                           Tactics.apply just]
 173                    ]) status)
 174     | Some lhs ->
 175        match conclude with
 176           None -> ProofEngineTypes.apply_tactic (Tactics.apply just) status
 177         | Some name ->
 178             let mk_fresh_name_callback =
 179              fun metasenv context _ ~typ ->
 180                FreshNamesGenerator.mk_fresh_name ~subst:[]
 181                 metasenv context name ~typ
 182             in
 183              ProofEngineTypes.apply_tactic
 184               (Tacticals.thens
 185                 ~start:
 186                   (Tactics.cut ~mk_fresh_name_callback
 187                     (Cic.Appl [eq ; ty ; lhs ; rhs]))
 188                 ~continuations:[ Tacticals.id_tac ; Tactics.apply just ]) status
 189  in
 190   ProofEngineTypes.mk_tactic aux
 191 ;;
 192
 193 let we_proceed_by_induction_on t pat =
 194  (*BUG here: pat unused *)
 195  Tactics.elim_intros ~depth:0 t
 196 ;;
 197
 198 let case id ~params =
 199  (*BUG here: id unused*)
 200  (*BUG here: it does not verify that the previous branch is closed *)
 201  (*BUG here: the params should be parsed telescopically*)
 202  (*BUG here: the tactic_terms should be terms*)
 203  let rec aux ~params ((proof,goal) as status) =
 204   match params with
 205      [] -> proof,[goal]
 206    | (id,t)::tl ->
 207       match ProofEngineTypes.apply_tactic (assume id t) status with
 208          proof,[goal] -> aux tl (proof,goal)
 209        | _ -> assert false
 210  in
 211   ProofEngineTypes.mk_tactic (aux ~params)
 212 ;;
 213
 214 let thesisbecomes t =
 215 let ty = None in
 216  (*BUG here: missing check on t *)
 217  match ty with
 218     None -> Tacticals.id_tac
 219   | Some ty ->
 220      Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
 221       (fun _ metasenv ugraph -> ty,metasenv,ugraph)
 222 ;;
 223
 224 let byinduction t id  = suppose t id None;;