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 list -> tactic
 108   val wildcard: tactic
 109   val merge: tactic
 110   val focus: int list -> tactic
 111   val unfocus: tactic
 112 end
 113
 114 module Make (S: Continuationals.Status) : T with type tactic = S.tactic =
 115 struct
 116   module C = Continuationals.Make (S)
 117
 118   type tactic = S.tactic
 119
 120   let fold_eval status ts =
 121     let istatus =
 122       List.fold_left (fun istatus t -> S.focus ~-1 (C.eval t istatus)) status ts
 123     in
 124     S.inject istatus
 125
 126   (**
 127     naive implementation of ORELSE tactical, try a sequence of tactics in turn:
 128     if one fails pass to the next one and so on, eventually raises (failure "no
 129     tactics left")
 130   *)
 131   let first ~tactics =
 132     let rec first ~(tactics: (string * tactic) list) istatus =
 133       info (lazy "in Tacticals.first");
 134       match tactics with
 135       | (descr, tac)::tactics ->
 136           info (lazy ("Tacticals.first IS TRYING " ^ descr));
 137           (try
 138             let res = S.apply_tactic tac istatus in
 139             info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
 140             res
 141           with
 142           e ->
 143             match e with
 144             | (ProofEngineTypes.Fail _)
 145             | (CicTypeChecker.TypeCheckerFailure _)
 146             | (CicUnification.UnificationFailure _) ->
 147                 info (lazy (
 148                   "Tacticals.first failed with exn: " ^
 149                   Printexc.to_string e));
 150                   first ~tactics istatus
 151             | _ -> raise e) (* [e] must not be caught ; let's re-raise it *)
 152       | [] -> raise (ProofEngineTypes.Fail (lazy "first: no tactics left"))
 153     in
 154     S.mk_tactic (first ~tactics)
 155
 156   let thens ~start ~continuations =
 157     S.mk_tactic
 158       (fun istatus ->
 159         fold_eval istatus
 160           ([ C.Tactical (C.Tactic start); C.Branch ]
 161           @ (HExtlib.list_concat ~sep:[ C.Shift ]
 162               (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) continuations))
 163           @ [ C.Merge ]))
 164
 165   let then_ ~start ~continuation =
 166     S.mk_tactic
 167       (fun istatus ->
 168         let ostatus = C.eval (C.Tactical (C.Tactic start)) istatus in
 169         let opened,closed = S.goals ostatus in
 170          match opened with
 171             [] -> ostatus
 172           | _ ->
 173             fold_eval (S.focus ~-1 ostatus)
 174               [ C.Semicolon;
 175                 C.Tactical (C.Tactic continuation) ])
 176
 177   let seq ~tactics =
 178     S.mk_tactic
 179       (fun istatus ->
 180         fold_eval istatus
 181           (HExtlib.list_concat ~sep:[ C.Semicolon ]
 182             (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
 183
 184   (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno
 185    * applicato la tattica *)
 186
 187   let rec step f output_status opened closed =
 188     match opened with
 189     | [] -> output_status, [], closed
 190     | head :: tail ->
 191         let status = S.focus head output_status in
 192         let output_status' = f status in
 193         let opened', closed' = S.goals output_status' in
 194         let output_status'', opened'', closed'' =
 195           step f output_status' tail []
 196         in
 197         output_status'', opened' @ opened'', closed' @ closed''
 198
 199   (* This keep on appling tactic until it fails. When <tactic> generates more
 200    * than one goal, you have a tree of application on the tactic, repeat_tactic
 201    * works in depth on this tree *)
 202   let repeat_tactic ~tactic =
 203    let rec repeat_tactic ~tactic status =
 204     info (lazy "in repeat_tactic");
 205     try
 206      let output_status = S.apply_tactic tactic status in
 207      let opened, closed = S.goals output_status in
 208      let output_status, opened', closed' =
 209        step (repeat_tactic ~tactic) output_status opened closed
 210      in
 211      S.set_goals (opened', closed') output_status
 212     with
 213      (ProofEngineTypes.Fail _) as e ->
 214       info (lazy
 215         ("Tacticals.repeat_tactic failed after nth time with exception: "
 216          ^ Printexc.to_string e));
 217       S.apply_tactic S.id_tactic status
 218    in
 219     S.mk_tactic (repeat_tactic ~tactic)
 220
 221   (* This tries to apply tactic n times *)
 222   let do_tactic ~n ~tactic =
 223    let rec do_tactic ~n ~tactic status =
 224     if n = 0 then
 225      S.apply_tactic S.id_tactic status
 226     else
 227      try
 228       let output_status = S.apply_tactic tactic status in
 229       let opened, closed = S.goals output_status in
 230        let output_status, opened', closed' =
 231          step (do_tactic ~n:(n-1) ~tactic) output_status opened closed
 232        in
 233        S.set_goals (opened', closed') output_status
 234      with
 235       (ProofEngineTypes.Fail _) as e ->
 236        info (lazy
 237           ("Tacticals.do_tactic failed after nth time with exception: "
 238            ^ Printexc.to_string e)) ;
 239        S.apply_tactic S.id_tactic status
 240    in
 241     S.mk_tactic (do_tactic ~n ~tactic)
 242
 243   (* This applies tactic and catches its possible failure *)
 244   let try_tactic ~tactic =
 245    let rec try_tactic ~tactic status =
 246     info (lazy "in Tacticals.try_tactic");
 247     try
 248      S.apply_tactic tactic status
 249     with
 250      (ProofEngineTypes.Fail _) as e ->
 251       info (lazy (
 252         "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
 253       S.apply_tactic S.id_tactic status
 254    in
 255     S.mk_tactic (try_tactic ~tactic)
 256
 257   (* This tries tactics until one of them doesn't _solve_ the goal *)
 258   (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
 259   let solve_tactics ~tactics =
 260    let rec solve_tactics ~(tactics: (string * tactic) list) status =
 261     info (lazy "in Tacticals.solve_tactics");
 262     match tactics with
 263     | (descr, currenttactic)::moretactics ->
 264         info (lazy ("Tacticals.solve_tactics is trying " ^ descr));
 265         (try
 266           let output_status = S.apply_tactic currenttactic status in
 267           let opened, closed = S.goals output_status in
 268            match opened with
 269             | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^
 270                      " solved the goal!!!"));
 271   (* questo significa che non ci sono piu' goal, o che current_tactic non ne ha
 272    * aperti di nuovi? (la 2a!) ##### nel secondo caso basta per dire che
 273    * solve_tactics has solved the goal?  (si!) *)
 274                     output_status
 275             | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
 276                    solve_tactics ~tactics:(moretactics) status
 277          with
 278           (ProofEngineTypes.Fail _) as e ->
 279            info (lazy (
 280               "Tacticals.solve_tactics: current tactic failed with exn: "
 281               ^ Printexc.to_string e));
 282            solve_tactics ~tactics status
 283         )
 284     | [] ->
 285         raise (ProofEngineTypes.Fail
 286           (lazy "solve_tactics cannot solve the goal"))
 287    in
 288     S.mk_tactic (solve_tactics ~tactics)
 289
 290   let cont_proxy cont = S.mk_tactic (C.eval cont)
 291
 292   let tactic t = cont_proxy (C.Tactical (C.Tactic t))
 293   let skip = cont_proxy (C.Tactical C.Skip)
 294   let dot = cont_proxy C.Dot
 295   let semicolon = cont_proxy C.Semicolon
 296   let branch = cont_proxy C.Branch
 297   let shift = cont_proxy C.Shift
 298   let pos i = cont_proxy (C.Pos i)
 299   let wildcard =  cont_proxy C.Wildcard
 300   let merge = cont_proxy C.Merge
 301   let focus goals = cont_proxy (C.Focus goals)
 302   let unfocus = cont_proxy C.Unfocus
 303 end
 304
 305 module ProofEngineStatus =
 306 struct
 307   module Stack = Continuationals.Stack
 308
 309   type input_status =
 310     ProofEngineTypes.status (* (proof, goal) *) * Stack.t
 311
 312   type output_status =
 313     (ProofEngineTypes.proof * goal list * goal list) * Stack.t
 314
 315   type tactic = ProofEngineTypes.tactic
 316
 317   let id_tactic = id_tac
 318
 319   let mk_tactic f =
 320     ProofEngineTypes.mk_tactic
 321       (fun (proof, goal) as pstatus ->
 322         let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
 323         let istatus = pstatus, stack in
 324 (*         let ostatus = f istatus in
 325         let ((proof, opened, _), _) = ostatus in *)
 326         let (proof, _, _), stack = f istatus in
 327         let opened = Continuationals.Stack.open_goals stack in
 328         proof, opened)
 329
 330   let apply_tactic tac ((proof, _) as pstatus, stack) =
 331     let proof', opened = ProofEngineTypes.apply_tactic tac pstatus in
 332 (* let _ = prerr_endline ("goal aperti dalla tattica " ^ String.concat "," (List.map string_of_int opened)) in *)
 333     let before = ProofEngineTypes.goals_of_proof proof in
 334     let after = ProofEngineTypes.goals_of_proof proof' in
 335     let opened_goals, closed_goals = goals_diff ~before ~after ~opened in
 336 (* let _ = prerr_endline ("goal ritornati dalla tattica " ^ String.concat "," (List.map string_of_int opened_goals)) in *)
 337     (proof', opened_goals, closed_goals), stack
 338
 339   let goals ((_, opened, closed), _) = opened, closed
 340   let set_goals (opened, closed) ((proof, _, _), stack) =
 341     (proof, opened, closed), stack
 342
 343   let get_stack = snd
 344   let set_stack stack (opstatus, _) = opstatus, stack
 345
 346   let inject ((proof, _), stack) = ((proof, [], []), stack)
 347   let focus goal ((proof, _, _), stack) = (proof, goal), stack
 348 end
 349
 350 module ProofEngineTacticals = Make (ProofEngineStatus)
 351
 352 include ProofEngineTacticals
 353