helm/software/components/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 (* $Id$ *)
  27
  28 (* open CicReduction
  29 open ProofEngineTypes
  30 open UriManager *)
  31
  32 (** DEBUGGING *)
  33
  34   (** perform debugging output? *)
  35 let debug = false
  36 let debug_print = fun _ -> ()
  37
  38   (** debugging print *)
  39 let info s = debug_print (lazy ("TACTICALS INFO: " ^ (Lazy.force s)))
  40
  41 let id_tac =
  42  let id_tac (proof,goal) =
  43   let _, metasenv, _, _ = proof in
  44   let _, _, _ = CicUtil.lookup_meta goal metasenv in
  45   (proof,[goal])
  46  in
  47   ProofEngineTypes.mk_tactic id_tac
  48
  49 let fail_tac =
  50  let fail_tac (proof,goal) =
  51   let _, metasenv, _, _ = proof in
  52   let _, _, _ = CicUtil.lookup_meta goal metasenv in
  53    raise (ProofEngineTypes.Fail (lazy "fail tactical"))
  54  in
  55   ProofEngineTypes.mk_tactic fail_tac
  56
  57 type goal = ProofEngineTypes.goal
  58
  59     (** TODO needed until tactics start returning both opened and closed goals
  60      * First part of the function performs a diff among goals ~before tactic
  61      * application and ~after it. Second part will add as both opened and closed
  62      * the goals which are returned as opened by the tactic *)
  63 let goals_diff ~before ~after ~opened =
  64   let sort_opened opened add =
  65     opened @ (List.filter (fun g -> not (List.mem g opened)) add)
  66   in
  67   let remove =
  68     List.fold_left
  69       (fun remove e -> if List.mem e after then remove else e :: remove)
  70       [] before
  71   in
  72   let add =
  73     List.fold_left
  74       (fun add e -> if List.mem e before then add else e :: add)
  75       []
  76       after
  77   in
  78   let add, remove = (* adds goals which have been both opened _and_ closed *)
  79     List.fold_left
  80       (fun (add, remove) opened_goal ->
  81         if List.mem opened_goal before
  82         then opened_goal :: add, opened_goal :: remove
  83         else add, remove)
  84       (add, remove)
  85       opened
  86   in
  87   sort_opened opened add, remove
  88
  89 module type T =
  90 sig
  91   type tactic
  92   val first: tactics: (string * tactic) list -> tactic
  93   val thens: start: tactic -> continuations: tactic list -> tactic
  94   val then_: start: tactic -> continuation: tactic -> tactic
  95   val seq: tactics: tactic list -> tactic
  96   val repeat_tactic: tactic: tactic -> tactic
  97   val do_tactic: n: int -> tactic: tactic -> tactic
  98   val try_tactic: tactic: tactic -> tactic
  99   val solve_tactics: tactics: (string * tactic) list -> tactic
 100
 101   val tactic: tactic -> tactic
 102   val skip: tactic
 103   val dot: tactic
 104   val semicolon: tactic
 105   val branch: tactic
 106   val shift: tactic
 107   val pos: int -> tactic
 108   val merge: tactic
 109   val focus: int list -> tactic
 110   val unfocus: tactic
 111 end
 112
 113 module Make (S: Continuationals.Status) : T with type tactic = S.tactic =
 114 struct
 115   module C = Continuationals.Make (S)
 116
 117   type tactic = S.tactic
 118
 119   let fold_eval status ts =
 120     let istatus =
 121       List.fold_left (fun istatus t -> S.focus ~-1 (C.eval t istatus)) status ts
 122     in
 123     S.inject istatus
 124
 125   (**
 126     naive implementation of ORELSE tactical, try a sequence of tactics in turn:
 127     if one fails pass to the next one and so on, eventually raises (failure "no
 128     tactics left")
 129   *)
 130   let first ~tactics =
 131     let rec first ~(tactics: (string * tactic) list) istatus =
 132       info (lazy "in Tacticals.first");
 133       match tactics with
 134       | (descr, tac)::tactics ->
 135           info (lazy ("Tacticals.first IS TRYING " ^ descr));
 136           (try
 137             let res = S.apply_tactic tac istatus in
 138             info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
 139             res
 140           with
 141           e ->
 142             match e with
 143             | (ProofEngineTypes.Fail _)
 144             | (CicTypeChecker.TypeCheckerFailure _)
 145             | (CicUnification.UnificationFailure _) ->
 146                 info (lazy (
 147                   "Tacticals.first failed with exn: " ^
 148                   Printexc.to_string e));
 149                   first ~tactics istatus
 150             | _ -> raise e) (* [e] must not be caught ; let's re-raise it *)
 151       | [] -> raise (ProofEngineTypes.Fail (lazy "first: no tactics left"))
 152     in
 153     S.mk_tactic (first ~tactics)
 154
 155   let thens ~start ~continuations =
 156     S.mk_tactic
 157       (fun istatus ->
 158         fold_eval istatus
 159           ([ C.Tactical (C.Tactic start); C.Branch ]
 160           @ (HExtlib.list_concat ~sep:[ C.Shift ]
 161               (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) continuations))
 162           @ [ C.Merge ]))
 163
 164   let then_ ~start ~continuation =
 165     S.mk_tactic
 166       (fun istatus ->
 167         let ostatus = C.eval (C.Tactical (C.Tactic start)) istatus in
 168         let opened,closed = S.goals ostatus in
 169          match opened with
 170             [] -> ostatus
 171           | _ ->
 172             fold_eval (S.focus ~-1 ostatus)
 173               [ C.Semicolon;
 174                 C.Tactical (C.Tactic continuation) ])
 175
 176   let seq ~tactics =
 177     S.mk_tactic
 178       (fun istatus ->
 179         fold_eval istatus
 180           (HExtlib.list_concat ~sep:[ C.Semicolon ]
 181             (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
 182
 183   (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno
 184    * applicato la tattica *)
 185
 186   let rec step f output_status opened closed =
 187     match opened with
 188     | [] -> output_status, [], closed
 189     | head :: tail ->
 190         let status = S.focus head output_status in
 191         let output_status' = f status in
 192         let opened', closed' = S.goals output_status' in
 193         let output_status'', opened'', closed'' =
 194           step f output_status' tail []
 195         in
 196         output_status'', opened' @ opened'', closed' @ closed''
 197
 198   (* This keep on appling tactic until it fails. When <tactic> generates more
 199    * than one goal, you have a tree of application on the tactic, repeat_tactic
 200    * works in depth on this tree *)
 201   let repeat_tactic ~tactic =
 202    let rec repeat_tactic ~tactic status =
 203     info (lazy "in repeat_tactic");
 204     try
 205      let output_status = S.apply_tactic tactic status in
 206      let opened, closed = S.goals output_status in
 207      let output_status, opened', closed' =
 208        step (repeat_tactic ~tactic) output_status opened closed
 209      in
 210      S.set_goals (opened', closed') output_status
 211     with
 212      (ProofEngineTypes.Fail _) as e ->
 213       info (lazy
 214         ("Tacticals.repeat_tactic failed after nth time with exception: "
 215          ^ Printexc.to_string e));
 216       S.apply_tactic S.id_tactic status
 217    in
 218     S.mk_tactic (repeat_tactic ~tactic)
 219
 220   (* This tries to apply tactic n times *)
 221   let do_tactic ~n ~tactic =
 222    let rec do_tactic ~n ~tactic status =
 223     if n = 0 then
 224      S.apply_tactic S.id_tactic status
 225     else
 226      try
 227       let output_status = S.apply_tactic tactic status in
 228       let opened, closed = S.goals output_status in
 229        let output_status, opened', closed' =
 230          step (do_tactic ~n:(n-1) ~tactic) output_status opened closed
 231        in
 232        S.set_goals (opened', closed') output_status
 233      with
 234       (ProofEngineTypes.Fail _) as e ->
 235        info (lazy
 236           ("Tacticals.do_tactic failed after nth time with exception: "
 237            ^ Printexc.to_string e)) ;
 238        S.apply_tactic S.id_tactic status
 239    in
 240     S.mk_tactic (do_tactic ~n ~tactic)
 241
 242   (* This applies tactic and catches its possible failure *)
 243   let try_tactic ~tactic =
 244    let rec try_tactic ~tactic status =
 245     info (lazy "in Tacticals.try_tactic");
 246     try
 247      S.apply_tactic tactic status
 248     with
 249      (ProofEngineTypes.Fail _) as e ->
 250       info (lazy (
 251         "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
 252       S.apply_tactic S.id_tactic status
 253    in
 254     S.mk_tactic (try_tactic ~tactic)
 255
 256   (* This tries tactics until one of them doesn't _solve_ the goal *)
 257   (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
 258   let solve_tactics ~tactics =
 259    let rec solve_tactics ~(tactics: (string * tactic) list) status =
 260     info (lazy "in Tacticals.solve_tactics");
 261     match tactics with
 262     | (descr, currenttactic)::moretactics ->
 263         info (lazy ("Tacticals.solve_tactics is trying " ^ descr));
 264         (try
 265           let output_status = S.apply_tactic currenttactic status in
 266           let opened, closed = S.goals output_status in
 267            match opened with
 268             | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^
 269                      " solved the goal!!!"));
 270   (* questo significa che non ci sono piu' goal, o che current_tactic non ne ha
 271    * aperti di nuovi? (la 2a!) ##### nel secondo caso basta per dire che
 272    * solve_tactics has solved the goal?  (si!) *)
 273                     output_status
 274             | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
 275                    solve_tactics ~tactics:(moretactics) status
 276          with
 277           (ProofEngineTypes.Fail _) as e ->
 278            info (lazy (
 279               "Tacticals.solve_tactics: current tactic failed with exn: "
 280               ^ Printexc.to_string e));
 281            solve_tactics ~tactics status
 282         )
 283     | [] ->
 284         raise (ProofEngineTypes.Fail
 285           (lazy "solve_tactics cannot solve the goal"))
 286    in
 287     S.mk_tactic (solve_tactics ~tactics)
 288
 289   let cont_proxy cont = S.mk_tactic (C.eval cont)
 290
 291   let tactic t = cont_proxy (C.Tactical (C.Tactic t))
 292   let skip = cont_proxy (C.Tactical C.Skip)
 293   let dot = cont_proxy C.Dot
 294   let semicolon = cont_proxy C.Semicolon
 295   let branch = cont_proxy C.Branch
 296   let shift = cont_proxy C.Shift
 297   let pos i = cont_proxy (C.Pos i)
 298   let merge = cont_proxy C.Merge
 299   let focus goals = cont_proxy (C.Focus goals)
 300   let unfocus = cont_proxy C.Unfocus
 301 end
 302
 303 module ProofEngineStatus =
 304 struct
 305   module Stack = Continuationals.Stack
 306
 307   type input_status =
 308     ProofEngineTypes.status (* (proof, goal) *) * Stack.t
 309
 310   type output_status =
 311     (ProofEngineTypes.proof * goal list * goal list) * Stack.t
 312
 313   type tactic = ProofEngineTypes.tactic
 314
 315   let id_tactic = id_tac
 316
 317   let mk_tactic f =
 318     ProofEngineTypes.mk_tactic
 319       (fun (proof, goal) as pstatus ->
 320         let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
 321         let istatus = pstatus, stack in
 322 (*         let ostatus = f istatus in
 323         let ((proof, opened, _), _) = ostatus in *)
 324         let (proof, _, _), stack = f istatus in
 325         let opened = Continuationals.Stack.open_goals stack in
 326         proof, opened)
 327
 328   let apply_tactic tac ((proof, _) as pstatus, stack) =
 329     let proof', opened = ProofEngineTypes.apply_tactic tac pstatus in
 330 (* let _ = prerr_endline ("goal aperti dalla tattica " ^ String.concat "," (List.map string_of_int opened)) in *)
 331     let before = ProofEngineTypes.goals_of_proof proof in
 332     let after = ProofEngineTypes.goals_of_proof proof' in
 333     let opened_goals, closed_goals = goals_diff ~before ~after ~opened in
 334 (* let _ = prerr_endline ("goal ritornati dalla tattica " ^ String.concat "," (List.map string_of_int opened_goals)) in *)
 335     (proof', opened_goals, closed_goals), stack
 336
 337   let goals ((_, opened, closed), _) = opened, closed
 338   let set_goals (opened, closed) ((proof, _, _), stack) =
 339     (proof, opened, closed), stack
 340
 341   let get_stack = snd
 342   let set_stack stack (opstatus, _) = opstatus, stack
 343
 344   let inject ((proof, _), stack) = ((proof, [], []), stack)
 345   let focus goal ((proof, _, _), stack) = (proof, goal), stack
 346 end
 347
 348 module ProofEngineTacticals = Make (ProofEngineStatus)
 349
 350 include ProofEngineTacticals
 351