helm/ocaml/tactics/tacticals.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 open CicReduction
  27 open ProofEngineTypes
  28 open UriManager
  29
  30 (** DEBUGGING *)
  31
  32   (** perform debugging output? *)
  33 let debug = false
  34
  35   (** debugging print *)
  36 let warn s =
  37   if debug then
  38     prerr_endline ("TACTICALS WARNING: " ^ s)
  39
  40
  41 (** TACTIC{,AL}S *)
  42
  43   (* not a tactical, but it's used only here (?) *)
  44
  45 let id_tac =
  46  let tac (proof,goal) = (proof,[goal])
  47  in
  48   mk_tactic tac
  49
  50   (**
  51     naive implementation of ORELSE tactical, try a sequence of tactics in turn:
  52     if one fails pass to the next one and so on, eventually raises (failure "no
  53     tactics left")
  54     TODO warning: not tail recursive due to "try .. with" boxing
  55
  56     Galla: is this exactly Coq's "First"?
  57
  58   *)
  59 let try_tactics ~tactics =
  60  let rec try_tactics ~(tactics: (string * tactic) list) status =
  61   warn "in Tacticals.try_tactics";
  62   match tactics with
  63   | (descr, tac)::tactics ->
  64       warn ("Tacticals.try_tactics IS TRYING " ^ descr);
  65       (try
  66         let res = apply_tactic tac status in
  67         warn ("Tacticals.try_tactics: " ^ descr ^ " succedeed!!!");
  68         res
  69        with
  70         e ->
  71          match e with
  72             (Fail _)
  73           | (CicTypeChecker.TypeCheckerFailure _)
  74           | (CicUnification.UnificationFailure _) ->
  75               warn (
  76                 "Tacticals.try_tactics failed with exn: " ^
  77                 Printexc.to_string e);
  78               try_tactics ~tactics status
  79         | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
  80       )
  81   | [] -> raise (Fail "try_tactics: no tactics left")
  82  in
  83   mk_tactic (try_tactics ~tactics)
  84
  85
  86 let thens ~start ~continuations =
  87  let thens ~start ~continuations status =
  88  let (proof,new_goals) = apply_tactic start status in
  89   try
  90    List.fold_left2
  91     (fun (proof,goals) goal tactic ->
  92       let (proof',new_goals') = apply_tactic tactic (proof,goal) in
  93        (proof',goals@new_goals')
  94     ) (proof,[]) new_goals continuations
  95   with
  96    Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
  97  in
  98   mk_tactic (thens ~start ~continuations )
  99
 100
 101 let then_ ~start ~continuation =
 102  let then_ ~start ~continuation status =
 103  let (proof,new_goals) = apply_tactic start status in
 104   List.fold_left
 105    (fun (proof,goals) goal ->
 106      let (proof',new_goals') = apply_tactic continuation (proof,goal) in
 107       (proof',goals@new_goals')
 108    ) (proof,[]) new_goals
 109  in
 110   mk_tactic (then_ ~start ~continuation)
 111
 112 let rec seq ~tactics =
 113   match tactics with
 114   | [] -> assert false
 115   | [tac] -> tac
 116   | hd :: tl -> then_ ~start:hd ~continuation:(seq ~tactics:tl)
 117
 118 (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *)
 119
 120 (* This keep on appling tactic until it fails *)
 121 (* When <tactic> generates more than one goal, you have a tree of
 122    application on the tactic, repeat_tactic works in depth on this tree *)
 123
 124 let repeat_tactic ~tactic =
 125  let rec repeat_tactic ~tactic status =
 126   warn "in repeat_tactic";
 127   try let (proof, goallist) = apply_tactic tactic status in
 128    let rec step proof goallist =
 129     match goallist with
 130        [] -> (proof, [])
 131      | head::tail ->
 132         let (proof', goallist') = repeat_tactic ~tactic (proof, head) in
 133          let (proof'', goallist'') = step proof' tail in
 134           proof'', goallist'@goallist''
 135    in
 136     step proof goallist
 137   with
 138    (Fail _) as e ->
 139     warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
 140     apply_tactic id_tac status
 141  in
 142   mk_tactic (repeat_tactic ~tactic)
 143 ;;
 144
 145
 146
 147 (* This tries to apply tactic n times *)
 148 let do_tactic ~n ~tactic =
 149  let rec do_tactic ~n ~tactic status =
 150   warn "in do_tactic";
 151   try
 152    let (proof, goallist) =
 153     if (n>0) then apply_tactic tactic status
 154              else apply_tactic id_tac status in
 155 (*             else (proof, []) in *)
 156 (* perche' non va bene questo? stessa questione di ##### ? *)
 157    let rec step proof goallist =
 158     match goallist with
 159        [] -> (proof, [])
 160      | head::tail ->
 161         let (proof', goallist') =
 162          do_tactic ~n:(n-1) ~tactic (proof, head) in
 163         let (proof'', goallist'') = step proof' tail in
 164          proof'', goallist'@goallist''
 165    in
 166     step proof goallist
 167   with
 168    (Fail _) as e ->
 169     warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
 170     apply_tactic id_tac status
 171  in
 172   mk_tactic (do_tactic ~n ~tactic)
 173 ;;
 174
 175
 176
 177 (* This applies tactic and catches its possible failure *)
 178 let try_tactic ~tactic =
 179  let rec try_tactic ~tactic status =
 180   warn "in Tacticals.try_tactic";
 181   try
 182    apply_tactic tactic status
 183   with
 184    (Fail _) as e ->
 185     warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e);
 186     apply_tactic id_tac status
 187  in
 188   mk_tactic (try_tactic ~tactic)
 189 ;;
 190
 191 let fail = mk_tactic (fun _ -> raise (Fail "fail tactical"))
 192
 193 (* This tries tactics until one of them doesn't _solve_ the goal *)
 194 (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
 195 let solve_tactics ~tactics =
 196  let rec solve_tactics ~(tactics: (string * tactic) list) status =
 197   warn "in Tacticals.solve_tactics";
 198   match tactics with
 199   | (descr, currenttactic)::moretactics ->
 200       warn ("Tacticals.solve_tactics is trying " ^ descr);
 201       (try
 202         let (proof, goallist) = apply_tactic currenttactic status in
 203          match goallist with
 204             [] -> warn ("Tacticals.solve_tactics: " ^ descr ^
 205                    " solved the goal!!!");
 206 (* questo significa che non ci sono piu' goal, o che current_tactic non ne
 207    ha aperti di nuovi? (la 2a!) #####
 208    nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *)
 209                   (proof, goallist)
 210           | _ -> warn ("Tacticals.solve_tactics: try the next tactic");
 211                  solve_tactics ~tactics:(moretactics) status
 212        with
 213         (Fail _) as e ->
 214          warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^
 215           Printexc.to_string e);
 216          solve_tactics ~tactics status
 217       )
 218   | [] -> raise (Fail "solve_tactics cannot solve the goal");
 219           apply_tactic id_tac status
 220  in
 221   mk_tactic (solve_tactics ~tactics)
 222 ;;
 223
 224
 225
 226
 227
 228
 229
 230
 231
 232
 233   (** tattica di prova per debuggare i tatticali *)
 234 (*
 235 let thens' ~start ~continuations status =
 236  let (proof,new_goals) = start status in
 237   try
 238    List.fold_left2
 239     (fun (proof,goals) goal tactic ->
 240       let (proof',new_goals') = tactic (proof,goal) in
 241        (proof',goals@new_goals')
 242     ) (proof,[]) new_goals continuations
 243   with
 244    Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
 245
 246 let prova_tac =
 247  let apply_T_tac status =
 248   let (proof, goal) = status in
 249   let curi,metasenv,pbo,pty = proof in
 250   let metano,context,gty = CicUtil.lookup_meta goal metasenv in
 251    let rel =
 252     let rec find n =
 253      function
 254         [] -> assert false
 255       | (Some (Cic.Name name,_))::_ when name = "T" -> n
 256       | _::tl -> find (n+1) tl
 257     in
 258      prerr_endline ("eseguo find");
 259      find 1 context
 260    in
 261     prerr_endline ("eseguo apply");
 262     apply_tac ~term:(Cic.Rel rel) status
 263  in
 264 (*  do_tactic ~n:2 *)
 265   repeat_tactic
 266    ~tactic:
 267     (then_
 268       ~start:(intros_tac ~name:"pippo")
 269       ~continuation:(thens' ~start:apply_T_tac ~continuations:[id_tac ; apply_tac ~term:(Cic.Rel 1)]))
 270 (* id_tac *)
 271 ;;
 272 *)
 273
 274