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