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