helm/software/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 type just = [ `Term of Cic.term | `Auto of Auto.auto_params ]
  27
  28 let mk_just ~dbd ~universe =
  29  function
  30     `Auto (l,params) ->
  31        Tactics.auto ~dbd
  32        ~params:(l,("skip_trie_filtering","1")::("skip_context","1")::params) ~universe
  33   | `Term t -> Tactics.apply t
  34 ;;
  35
  36 let assume id t =
  37   Tacticals.then_
  38      ~start:
  39        (Tactics.intros ~howmany:1
  40         ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
  41      ~continuation:
  42        (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
  43          (fun _ metasenv ugraph -> t,metasenv,ugraph))
  44 ;;
  45
  46 let suppose t id ty =
  47 (*BUG: check on t missing *)
  48  let ty = match ty with None -> t | Some ty -> ty in
  49  Tacticals.then_
  50    ~start:
  51      (Tactics.intros ~howmany:1
  52        ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
  53    ~continuation:
  54      (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
  55       (fun _ metasenv ugraph -> ty,metasenv,ugraph))
  56 ;;
  57
  58 let by_just_we_proved ~dbd ~universe just ty id ty' =
  59  let just = mk_just ~dbd ~universe just in
  60   match id with
  61      None ->
  62       (match ty' with
  63           None -> assert false
  64         | Some ty' ->
  65            Tacticals.then_
  66             ~start:(Tactics.change
  67               ~pattern:(ProofEngineTypes.conclusion_pattern None)
  68               (fun _ metasenv ugraph -> ty,metasenv,ugraph))
  69             ~continuation:just
  70       )
  71    | Some id ->
  72        let ty',continuation =
  73         match ty' with
  74            None -> ty,just
  75          | Some ty' ->
  76             ty',
  77             Tacticals.then_
  78              ~start:
  79                (Tactics.change
  80                  ~with_cast:true
  81                  ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
  82                  (fun _ metasenv ugraph -> ty,metasenv,ugraph))
  83              ~continuation:just
  84        in
  85         Tacticals.thens
  86         ~start:
  87           (Tactics.cut ty'
  88             ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
  89         ~continuations:[ Tacticals.id_tac ; continuation ]
  90 ;;
  91
  92 let bydone ~dbd ~universe just =
  93  mk_just ~dbd ~universe just
  94 ;;
  95
  96 let we_need_to_prove t id ty =
  97  match id with
  98     None ->
  99      (match ty with
 100          None -> Tacticals.id_tac (*BUG: check missing here *)
 101        | Some ty ->
 102           Tactics.change ~pattern:(ProofEngineTypes.conclusion_pattern None)
 103            (fun _ metasenv ugraph -> ty,metasenv,ugraph))
 104   | Some id ->
 105      let aux status =
 106       let cont,cutted =
 107        match ty with
 108           None -> Tacticals.id_tac,t
 109         | Some ty ->
 110            Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
 111              (fun _ metasenv ugraph -> t,metasenv,ugraph), ty in
 112       let proof,goals =
 113        ProofEngineTypes.apply_tactic
 114         (Tacticals.thens
 115           ~start:
 116            (Tactics.cut cutted
 117              ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
 118           ~continuations:[cont])
 119         status
 120       in
 121        let goals' =
 122         match goals with
 123            [fst; snd] -> [snd; fst]
 124          | _ -> assert false
 125        in
 126         proof,goals'
 127      in
 128       ProofEngineTypes.mk_tactic aux
 129 ;;
 130
 131 let existselim ~dbd ~universe just id1 t1 id2 t2 =
 132  let aux (proof, goal) =
 133   let (n,metasenv,_subst,bo,ty,attrs) = proof in
 134   let metano,context,_ = CicUtil.lookup_meta goal metasenv in
 135   let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
 136   let proof' = (n,metasenv,_subst,bo,ty,attrs) in
 137    ProofEngineTypes.apply_tactic (
 138    Tacticals.thens
 139     ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)]))
 140     ~continuations:
 141      [ Tactics.elim_intros (Cic.Rel 1)
 142         ~mk_fresh_name_callback:
 143           (let i = ref 0 in
 144             fun _ _ _  ~typ ->
 145              incr i;
 146              if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
 147        (mk_just ~dbd ~universe just)
 148      ]) (proof', goal)
 149  in
 150   ProofEngineTypes.mk_tactic aux
 151 ;;
 152
 153 let andelim ~dbd ~universe just id1 t1 id2 t2 =
 154    Tacticals.thens
 155     ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/And.ind", 0, []); t1 ; t2]))
 156     ~continuations:
 157      [ Tactics.elim_intros (Cic.Rel 1)
 158         ~mk_fresh_name_callback:
 159           (let i = ref 0 in
 160             fun _ _ _  ~typ ->
 161              incr i;
 162              if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
 163        (mk_just ~dbd ~universe just) ]
 164 ;;
 165
 166 let rewritingstep ~dbd ~universe lhs rhs just last_step =
 167  let aux ((proof,goal) as status) =
 168   let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in
 169   let _,context,gty = CicUtil.lookup_meta goal metasenv in
 170   let eq,trans =
 171    match LibraryObjects.eq_URI () with
 172       None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
 173     | Some uri ->
 174       Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
 175   in
 176   let ty,_ =
 177    CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.oblivion_ugraph in
 178   let just' =
 179    match just with
 180       `Auto (univ, params) ->
 181         let params =
 182          if not (List.exists (fun (k,_) -> k = "timeout") params) then
 183           ("timeout","3")::params
 184          else params
 185         in
 186         let params' =
 187          if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
 188           ("paramodulation","1")::params
 189          else params
 190         in
 191          if params = params' then
 192           Tactics.auto ~dbd ~params:(univ, params) ~universe
 193          else
 194           Tacticals.first
 195            [Tactics.auto ~dbd ~params:(univ, params) ~universe ;
 196             Tactics.auto ~dbd ~params:(univ, params') ~universe]
 197     | `Term just -> Tactics.apply just
 198     | `SolveWith term ->
 199          Tactics.solve_rewrite ~universe ~params:([term],["steps","1"]) ()
 200     | `Proof ->
 201         Tacticals.id_tac
 202   in
 203    let plhs,prhs,prepare =
 204     match lhs with
 205        None ->
 206         let plhs,prhs =
 207          match gty with
 208             Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
 209           | _ -> assert false
 210         in
 211          plhs,prhs,
 212           (fun continuation ->
 213             ProofEngineTypes.apply_tactic continuation status)
 214      | Some (None,lhs) ->
 215         let plhs,prhs =
 216          match gty with
 217             Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
 218           | _ -> assert false
 219         in
 220          (*CSC: manca check plhs convertibile con lhs *)
 221          plhs,prhs,
 222           (fun continuation ->
 223             ProofEngineTypes.apply_tactic continuation status)
 224      | Some (Some name,lhs) ->
 225         let newmeta = CicMkImplicit.new_meta metasenv [] in
 226         let irl =
 227          CicMkImplicit.identity_relocation_list_for_metavariable context in
 228         let plhs = lhs in
 229         let prhs = Cic.Meta(newmeta,irl) in
 230          plhs,prhs,
 231           (fun continuation ->
 232             let metasenv = (newmeta, context, ty)::metasenv in
 233             let mk_fresh_name_callback =
 234              fun metasenv context _ ~typ ->
 235               FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context
 236                (Cic.Name name) ~typ
 237             in
 238             let proof = curi,metasenv,_subst,proofbo,proofty, attrs in
 239             let proof,goals =
 240              ProofEngineTypes.apply_tactic
 241               (Tacticals.thens
 242                 ~start:(Tactics.cut ~mk_fresh_name_callback
 243                  (Cic.Appl [eq ; ty ; lhs ; prhs]))
 244                 ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal)
 245             in
 246              let goals =
 247               match just,goals with
 248                  `Proof, [g1;g2;g3] -> [g2;g3;newmeta;g1]
 249                | _, [g1;g2] -> [g2;newmeta;g1]
 250                | _, l ->
 251                  prerr_endline (String.concat "," (List.map string_of_int l));
 252                  prerr_endline (CicMetaSubst.ppmetasenv [] metasenv);
 253                  assert false
 254              in
 255               proof,goals)
 256    in
 257     let continuation =
 258      if last_step then
 259       (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
 260       just'
 261      else
 262       Tacticals.thens
 263        ~start:(Tactics.apply ~term:(Cic.Appl [trans;ty;plhs;rhs;prhs]))
 264        ~continuations:[just' ; Tacticals.id_tac]
 265     in
 266      prepare continuation
 267  in
 268   ProofEngineTypes.mk_tactic aux
 269 ;;
 270
 271 let we_proceed_by_cases_on t pat =
 272  (*BUG here: pat unused *)
 273  Tactics.cases_intros t
 274 ;;
 275
 276 let we_proceed_by_induction_on t pat =
 277  let pattern = None, [], Some pat in
 278  Tactics.elim_intros ~depth:0 (*~pattern*) t
 279 ;;
 280
 281 let case id ~params =
 282  (*BUG here: id unused*)
 283  (*BUG here: it does not verify that the previous branch is closed *)
 284  (*BUG here: the params should be parsed telescopically*)
 285  (*BUG here: the tactic_terms should be terms*)
 286  let rec aux ~params ((proof,goal) as status) =
 287   match params with
 288      [] -> proof,[goal]
 289    | (id,t)::tl ->
 290       match ProofEngineTypes.apply_tactic (assume id t) status with
 291          proof,[goal] -> aux tl (proof,goal)
 292        | _ -> assert false
 293  in
 294   ProofEngineTypes.mk_tactic (aux ~params)
 295 ;;
 296
 297 let thesisbecomes t =
 298 let ty = None in
 299  match ty with
 300     None ->
 301      Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
 302       (fun _ metasenv ugraph -> t,metasenv,ugraph)
 303   | Some ty ->
 304      (*BUG here: missing check on t *)
 305      Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
 306       (fun _ metasenv ugraph -> ty,metasenv,ugraph)
 307 ;;
 308
 309 let byinduction t id  = suppose t id None;;