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