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 = debug_print (lazy ("TACTICALS WARNING: " ^ (Lazy.force s)))
  38
  39 let id_tac =
  40  let id_tac (proof,goal) =
  41   let _, metasenv, _, _ = proof in
  42   let _, _, _ = CicUtil.lookup_meta goal metasenv in
  43   (proof,[goal])
  44  in
  45   mk_tactic id_tac
  46
  47 let fail_tac =
  48  let fail_tac (proof,goal) =
  49   let _, metasenv, _, _ = proof in
  50   let _, _, _ = CicUtil.lookup_meta goal metasenv in
  51    raise (Fail "fail tactical")
  52  in
  53   mk_tactic fail_tac
  54
  55 module type Status =
  56  sig
  57    type input_status
  58    type output_status
  59    type tactic
  60    val id_tac : tactic
  61    val mk_tactic : (input_status -> output_status) -> tactic
  62    val apply_tactic : tactic -> input_status -> output_status
  63    val goals : output_status -> ProofEngineTypes.goal list
  64    val set_goals: output_status -> ProofEngineTypes.goal list -> output_status
  65    val focus : output_status -> ProofEngineTypes.goal -> input_status
  66  end
  67
  68 module type T =
  69  sig
  70   type tactic
  71
  72   val first: tactics: (string * tactic) list -> tactic
  73
  74   val thens: start: tactic -> continuations: tactic list -> tactic
  75
  76   val then_: start: tactic -> continuation: tactic -> tactic
  77
  78    (** "folding" of then_ *)
  79   val seq: tactics: tactic list -> tactic
  80
  81   val repeat_tactic: tactic: tactic -> tactic
  82
  83   val do_tactic: n: int -> tactic: tactic -> tactic
  84
  85   val try_tactic: tactic: tactic -> tactic
  86
  87   val solve_tactics: tactics: (string * tactic) list -> tactic
  88  end
  89
  90 module Make (S:Status) : T with type tactic = S.tactic =
  91 struct
  92 type tactic = S.tactic
  93
  94   (**
  95     naive implementation of ORELSE tactical, try a sequence of tactics in turn:
  96     if one fails pass to the next one and so on, eventually raises (failure "no
  97     tactics left")
  98   *)
  99 let first ~tactics =
 100  let rec first ~(tactics: (string * tactic) list) status =
 101   warn (lazy "in Tacticals.first");
 102   match tactics with
 103   | (descr, tac)::tactics ->
 104       warn (lazy ("Tacticals.first IS TRYING " ^ descr));
 105       (try
 106         let res = S.apply_tactic tac status in
 107         warn (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
 108         res
 109        with
 110         e ->
 111          match e with
 112             (Fail _)
 113           | (CicTypeChecker.TypeCheckerFailure _)
 114           | (CicUnification.UnificationFailure _) ->
 115               warn (lazy (
 116                 "Tacticals.first failed with exn: " ^
 117                 Printexc.to_string e));
 118               first ~tactics status
 119         | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
 120       )
 121   | [] -> raise (Fail "first: no tactics left")
 122  in
 123   S.mk_tactic (first ~tactics)
 124
 125
 126 let thens ~start ~continuations =
 127  let thens ~start ~continuations status =
 128  let output_status = S.apply_tactic start status in
 129  let new_goals = S.goals output_status in
 130   try
 131    let output_status,goals =
 132     List.fold_left2
 133      (fun (output_status,goals) goal tactic ->
 134        let status = S.focus output_status goal in
 135        let output_status' = S.apply_tactic tactic status in
 136        let new_goals' = S.goals output_status' in
 137         (output_status',goals@new_goals')
 138      ) (output_status,[]) new_goals continuations
 139    in
 140     S.set_goals output_status goals
 141   with
 142    Invalid_argument _ ->
 143     let debug = Printf.sprintf "thens: expected %i new goals, found %i"
 144      (List.length continuations) (List.length new_goals)
 145     in
 146     raise (Fail debug)
 147  in
 148   S.mk_tactic (thens ~start ~continuations )
 149
 150
 151 let then_ ~start ~continuation =
 152  let then_ ~start ~continuation status =
 153  let output_status = S.apply_tactic start status in
 154  let new_goals = S.goals output_status in
 155   let output_status,goals =
 156    List.fold_left
 157     (fun (output_status,goals) goal ->
 158       let status = S.focus output_status goal in
 159       let output_status' = S.apply_tactic continuation status in
 160       let new_goals' = S.goals output_status' in
 161        (output_status',goals@new_goals')
 162     ) (output_status,[]) new_goals
 163   in
 164    S.set_goals output_status goals
 165  in
 166   S.mk_tactic (then_ ~start ~continuation)
 167
 168 let rec seq ~tactics =
 169   match tactics with
 170   | [] -> assert false
 171   | [tac] -> tac
 172   | hd :: tl -> then_ ~start:hd ~continuation:(seq ~tactics:tl)
 173
 174 (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *)
 175
 176 (* This keep on appling tactic until it fails *)
 177 (* When <tactic> generates more than one goal, you have a tree of
 178    application on the tactic, repeat_tactic works in depth on this tree *)
 179
 180 let repeat_tactic ~tactic =
 181  let rec repeat_tactic ~tactic status =
 182   warn (lazy "in repeat_tactic");
 183   try
 184    let output_status = S.apply_tactic tactic status in
 185    let goallist = S.goals output_status in
 186    let rec step output_status goallist =
 187     match goallist with
 188        [] -> output_status,[]
 189      | head::tail ->
 190         let status = S.focus output_status head in
 191         let output_status' = repeat_tactic ~tactic status in
 192         let goallist' = S.goals output_status' in
 193          let output_status'',goallist'' = step output_status' tail in
 194           output_status'',goallist'@goallist''
 195    in
 196     let output_status,goallist = step output_status goallist in
 197      S.set_goals output_status goallist
 198   with
 199    (Fail _) as e ->
 200     warn (lazy ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e)) ;
 201     S.apply_tactic S.id_tac status
 202  in
 203   S.mk_tactic (repeat_tactic ~tactic)
 204
 205
 206 (* This tries to apply tactic n times *)
 207 let do_tactic ~n ~tactic =
 208  let rec do_tactic ~n ~tactic status =
 209   if n = 0 then
 210    S.apply_tactic S.id_tac status
 211   else
 212    try
 213     let output_status = S.apply_tactic tactic status in
 214     let goallist = S.goals output_status in
 215     let rec step output_status goallist =
 216      match goallist with
 217         [] -> output_status, []
 218       | head::tail ->
 219          let status = S.focus output_status head in
 220          let output_status' = do_tactic ~n:(n-1) ~tactic status in
 221          let goallist' = S.goals output_status' in
 222          let (output_status'', goallist'') = step output_status' tail in
 223           output_status'', goallist'@goallist''
 224     in
 225      let output_status,goals = step output_status goallist in
 226       S.set_goals output_status goals
 227    with
 228     (Fail _) as e ->
 229      warn (lazy ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e)) ;
 230      S.apply_tactic S.id_tac status
 231  in
 232   S.mk_tactic (do_tactic ~n ~tactic)
 233
 234
 235
 236 (* This applies tactic and catches its possible failure *)
 237 let try_tactic ~tactic =
 238  let rec try_tactic ~tactic status =
 239   warn (lazy "in Tacticals.try_tactic");
 240   try
 241    S.apply_tactic tactic status
 242   with
 243    (Fail _) as e ->
 244     warn (lazy ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
 245     S.apply_tactic S.id_tac status
 246  in
 247   S.mk_tactic (try_tactic ~tactic)
 248
 249 (* This tries tactics until one of them doesn't _solve_ the goal *)
 250 (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
 251 let solve_tactics ~tactics =
 252  let rec solve_tactics ~(tactics: (string * tactic) list) status =
 253   warn (lazy "in Tacticals.solve_tactics");
 254   match tactics with
 255   | (descr, currenttactic)::moretactics ->
 256       warn (lazy ("Tacticals.solve_tactics is trying " ^ descr));
 257       (try
 258         let output_status = S.apply_tactic currenttactic status in
 259         let goallist = S.goals output_status in
 260          match goallist with
 261             [] -> warn (lazy ("Tacticals.solve_tactics: " ^ descr ^
 262                    " solved the goal!!!"));
 263 (* questo significa che non ci sono piu' goal, o che current_tactic non ne
 264    ha aperti di nuovi? (la 2a!) #####
 265    nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *)
 266                   output_status
 267           | _ -> warn (lazy ("Tacticals.solve_tactics: try the next tactic"));
 268                  solve_tactics ~tactics:(moretactics) status
 269        with
 270         (Fail _) as e ->
 271          warn (lazy ("Tacticals.solve_tactics: current tactic failed with exn: " ^
 272           Printexc.to_string e));
 273          solve_tactics ~tactics status
 274       )
 275   | [] -> raise (Fail "solve_tactics cannot solve the goal");
 276           S.apply_tactic S.id_tac status
 277  in
 278   S.mk_tactic (solve_tactics ~tactics)
 279 end
 280
 281 module ProofEngineStatus =
 282  struct
 283    type input_status = ProofEngineTypes.status
 284    type output_status = ProofEngineTypes.proof * ProofEngineTypes.goal list
 285    type tactic = ProofEngineTypes.tactic
 286    let id_tac = id_tac
 287    let mk_tactic = ProofEngineTypes.mk_tactic
 288    let apply_tactic = ProofEngineTypes.apply_tactic
 289    let goals (_,goals) = goals
 290    let set_goals (proof,_) goals = proof,goals
 291    let focus (proof,_) goal = proof,goal
 292  end
 293
 294 module ProofEngineTacticals = Make(ProofEngineStatus)
 295
 296 include ProofEngineTacticals