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 thens ~start ~continuations =
 163    let thens ~start ~continuations status =
 164    let output_status = S.apply_tactic start status in
 165    let new_goals = S.goals output_status in
 166     try
 167      let output_status,goals =
 168       List.fold_left2
 169        (fun (output_status,goals) goal tactic ->
 170          let status = S.focus goal output_status in
 171          let output_status' = S.apply_tactic tactic status in
 172          let new_goals' = S.goals output_status' in
 173           (output_status',goals@new_goals')
 174        ) (output_status,[]) new_goals continuations
 175      in
 176       S.set_goals output_status goals
 177     with
 178      Invalid_argument _ ->
 179       let debug = Printf.sprintf "thens: expected %i new goals, found %i"
 180        (List.length continuations) (List.length new_goals)
 181       in
 182       raise (Fail debug)
 183    in
 184     S.mk_tactic (thens ~start ~continuations ) *)
 185
 186   let then_ ~start ~continuation =
 187     S.mk_tactic
 188       (fun istatus ->
 189         fold_eval istatus
 190           [ C.Tactical (C.Tactic start);
 191             C.Semicolon;
 192             C.Tactical (C.Tactic continuation) ])
 193
 194 (*   let then_ ~start ~continuation =
 195    let then_ ~start ~continuation status =
 196    let output_status = S.apply_tactic start status in
 197    let new_goals = S.goals output_status in
 198     let output_status,goals =
 199      List.fold_left
 200       (fun (output_status,goals) goal ->
 201         let status = S.focus goal output_status in
 202         let output_status' = S.apply_tactic continuation status in
 203         let new_goals' = S.goals output_status' in
 204          (output_status',goals@new_goals')
 205       ) (output_status,[]) new_goals
 206     in
 207      S.set_goals output_status goals
 208    in
 209     S.mk_tactic (then_ ~start ~continuation) *)
 210
 211   let seq ~tactics =
 212     S.mk_tactic
 213       (fun istatus ->
 214         fold_eval istatus
 215           (HExtlib.list_concat ~sep:[ C.Semicolon ]
 216             (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
 217
 218 (*   let rec seq ~tactics =
 219     match tactics with
 220     | [] -> assert false
 221     | [tac] -> tac
 222     | hd :: tl -> then_ ~start:hd ~continuation:(seq ~tactics:tl) *)
 223
 224   (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno
 225    * applicato la tattica *)
 226
 227   let rec step f output_status opened closed =
 228     match opened with
 229     | [] -> output_status, [], closed
 230     | head :: tail ->
 231         let status = S.focus head output_status in
 232         let output_status' = f status in
 233         let opened', closed' = S.goals output_status' in
 234         let output_status'', opened'', closed'' =
 235           step f output_status' tail []
 236         in
 237         output_status'', opened' @ opened'', closed' @ closed''
 238
 239   (* This keep on appling tactic until it fails. When <tactic> generates more
 240    * than one goal, you have a tree of application on the tactic, repeat_tactic
 241    * works in depth on this tree *)
 242   let repeat_tactic ~tactic =
 243    let rec repeat_tactic ~tactic status =
 244     info (lazy "in repeat_tactic");
 245     try
 246 (*      let rec step output_status opened closed =
 247        match opened with
 248        | [] -> output_status, [], closed
 249        | head :: tail ->
 250            let status = S.focus head output_status in
 251            let output_status' = repeat_tactic ~tactic status in
 252            let opened', closed' = S.goals output_status' in
 253            let output_status'', opened'', closed'' =
 254              step output_status' tail []
 255            in
 256            output_status'', opened' @ opened'', closed' @ closed''
 257      in *)
 258      let output_status = S.apply_tactic tactic status in
 259      let opened, closed = S.goals output_status in
 260      let output_status, opened', closed' =
 261        step (repeat_tactic ~tactic) output_status opened closed
 262      in
 263      S.set_goals (opened', closed') output_status
 264     with
 265      (ProofEngineTypes.Fail _) as e ->
 266       info (lazy
 267         ("Tacticals.repeat_tactic failed after nth time with exception: "
 268          ^ Printexc.to_string e));
 269       S.apply_tactic S.id_tactic status
 270    in
 271     S.mk_tactic (repeat_tactic ~tactic)
 272
 273   (* This tries to apply tactic n times *)
 274   let do_tactic ~n ~tactic =
 275    let rec do_tactic ~n ~tactic status =
 276     if n = 0 then
 277      S.apply_tactic S.id_tactic status
 278     else
 279      try
 280       let output_status = S.apply_tactic tactic status in
 281       let opened, closed = S.goals output_status in
 282 (*       let rec step output_status goallist =
 283        match goallist with
 284           [] -> output_status, []
 285         | head::tail ->
 286            let status = S.focus head output_status in
 287            let output_status' = do_tactic ~n:(n-1) ~tactic status in
 288            let goallist' = S.goals output_status' in
 289            let (output_status'', goallist'') = step output_status' tail in
 290             output_status'', goallist'@goallist''
 291       in *)
 292        let output_status, opened', closed' =
 293          step (do_tactic ~n:(n-1) ~tactic) output_status opened closed
 294        in
 295        S.set_goals (opened', closed') output_status
 296      with
 297       (ProofEngineTypes.Fail _) as e ->
 298        info (lazy
 299           ("Tacticals.do_tactic failed after nth time with exception: "
 300            ^ Printexc.to_string e)) ;
 301        S.apply_tactic S.id_tactic status
 302    in
 303     S.mk_tactic (do_tactic ~n ~tactic)
 304
 305   (* This applies tactic and catches its possible failure *)
 306   let try_tactic ~tactic =
 307    let rec try_tactic ~tactic status =
 308     info (lazy "in Tacticals.try_tactic");
 309     try
 310      S.apply_tactic tactic status
 311     with
 312      (ProofEngineTypes.Fail _) as e ->
 313       info (lazy (
 314         "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
 315       S.apply_tactic S.id_tactic status
 316    in
 317     S.mk_tactic (try_tactic ~tactic)
 318
 319   (* This tries tactics until one of them doesn't _solve_ the goal *)
 320   (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
 321   let solve_tactics ~tactics =
 322    let rec solve_tactics ~(tactics: (string * tactic) list) status =
 323     info (lazy "in Tacticals.solve_tactics");
 324     match tactics with
 325     | (descr, currenttactic)::moretactics ->
 326         info (lazy ("Tacticals.solve_tactics is trying " ^ descr));
 327         (try
 328           let output_status = S.apply_tactic currenttactic status in
 329           let opened, closed = S.goals output_status in
 330            match opened with
 331             | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^
 332                      " solved the goal!!!"));
 333   (* questo significa che non ci sono piu' goal, o che current_tactic non ne ha
 334    * aperti di nuovi? (la 2a!) ##### nel secondo caso basta per dire che
 335    * solve_tactics has solved the goal?  (si!) *)
 336                     output_status
 337             | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
 338                    solve_tactics ~tactics:(moretactics) status
 339          with
 340           (ProofEngineTypes.Fail _) as e ->
 341            info (lazy (
 342               "Tacticals.solve_tactics: current tactic failed with exn: "
 343               ^ Printexc.to_string e));
 344            solve_tactics ~tactics status
 345         )
 346     | [] ->
 347         raise (ProofEngineTypes.Fail
 348           (lazy "solve_tactics cannot solve the goal"))
 349    in
 350     S.mk_tactic (solve_tactics ~tactics)
 351
 352   let cont_proxy cont = S.mk_tactic (C.eval cont)
 353
 354   let tactic t = cont_proxy (C.Tactical (C.Tactic t))
 355   let skip = cont_proxy (C.Tactical C.Skip)
 356   let dot = cont_proxy C.Dot
 357   let semicolon = cont_proxy C.Semicolon
 358   let branch = cont_proxy C.Branch
 359   let shift = cont_proxy C.Shift
 360   let pos i = cont_proxy (C.Pos i)
 361   let merge = cont_proxy C.Merge
 362   let focus goals = cont_proxy (C.Focus goals)
 363   let unfocus = cont_proxy C.Unfocus
 364 end
 365
 366 module ProofEngineStatus =
 367 struct
 368   module Stack = Continuationals.Stack
 369
 370   type input_status =
 371     ProofEngineTypes.status (* (proof, goal) *) * Stack.t
 372
 373   type output_status =
 374     (ProofEngineTypes.proof * goal list * goal list) * Stack.t
 375
 376   type tactic = ProofEngineTypes.tactic
 377
 378   let id_tactic = id_tac
 379
 380   let mk_tactic f =
 381     ProofEngineTypes.mk_tactic
 382       (fun (proof, goal) as pstatus ->
 383         let stack = [ [ 1, Stack.Open goal ], [], [], Stack.NoTag ] in
 384         let istatus = pstatus, stack in
 385 (*         let ostatus = f istatus in
 386         let ((proof, opened, _), _) = ostatus in *)
 387         let (proof, _, _), stack = f istatus in
 388         let opened = Continuationals.Stack.open_goals stack in
 389         proof, opened)
 390
 391   let apply_tactic tac ((proof, _) as pstatus, stack) =
 392     let proof', opened = ProofEngineTypes.apply_tactic tac pstatus in
 393 (* let _ = prerr_endline ("goal aperti dalla tattica " ^ String.concat "," (List.map string_of_int opened)) in *)
 394     let before = ProofEngineTypes.goals_of_proof proof in
 395     let after = ProofEngineTypes.goals_of_proof proof' in
 396     let opened_goals, closed_goals = goals_diff ~before ~after ~opened in
 397 (* let _ = prerr_endline ("goal ritornati dalla tattica " ^ String.concat "," (List.map string_of_int opened_goals)) in *)
 398     (proof', opened_goals, closed_goals), stack
 399
 400   let goals ((_, opened, closed), _) = opened, closed
 401   let set_goals (opened, closed) ((proof, _, _), stack) =
 402     (proof, opened, closed), stack
 403
 404   let get_stack = snd
 405   let set_stack stack (opstatus, _) = opstatus, stack
 406
 407   let inject ((proof, _), stack) = ((proof, [], []), stack)
 408   let focus goal ((proof, _, _), stack) = (proof, goal), stack
 409 end
 410
 411 module ProofEngineTacticals = Make (ProofEngineStatus)
 412
 413 include ProofEngineTacticals
 414