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 ProofEngineStatus =
  92 struct
  93   module Stack = Continuationals.Stack
  94
  95   (* The stack is used and saved only at the very end of the eval function;
  96      it is read only at the beginning of the eval;
  97      we need it just to apply several times in a row this machine to an
  98      initial stack, i.e. to chain several applications of the machine together,
  99      i.e. to dump and restore the state of the machine.
 100      The stack is never used by the tactics: each tactic of type
 101      PET.tactic ignore the stack. To make a tactic from the eval function
 102      of a machine we apply the eval on a fresh stack (via the mk_tactic). *)
 103   type input_status =
 104     PET.status (* (proof, goal) *) * Stack.t
 105
 106   type output_status =
 107     (PET.proof * goal list * goal list) * Stack.t
 108
 109   type tactic = PET.tactic
 110
 111   let id_tactic = id_tac
 112
 113   (* f is an eval function of a machine;
 114      the machine is applied to a fresh stack and the final stack is read
 115      back to obtain the result of the tactic *)
 116   let mk_tactic f =
 117     PET.mk_tactic
 118       (fun (proof, goal) as pstatus ->
 119         let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
 120         let istatus = pstatus, stack in
 121         let (proof, _, _), stack = f istatus in
 122         let opened = Continuationals.Stack.open_goals stack in
 123         proof, opened)
 124
 125   (* it applies a tactic ignoring (and preserving) the stack *)
 126   let apply_tactic tac ((proof, _) as pstatus, stack) =
 127     let proof', opened = PET.apply_tactic tac pstatus in
 128     let before = PET.goals_of_proof proof in
 129     let after = PET.goals_of_proof proof' in
 130     let opened_goals, closed_goals = goals_diff ~before ~after ~opened in
 131     (proof', opened_goals, closed_goals), stack
 132
 133   let get_status (status, _) = status
 134   let get_proof ((proof, _, _), _) = proof
 135
 136   let goals ((_, opened, closed), _) = opened, closed
 137   let set_goals (opened, closed) ((proof, _, _), stack) =
 138     (proof, opened, closed), stack
 139
 140   (* Done only at the beginning of the eval of the machine *)
 141   let get_stack = snd
 142   (* Done only at the end of the eval of the machine *)
 143   let set_stack stack (opstatus, _) = opstatus, stack
 144
 145   let inject ((proof, _), stack) = ((proof, [], []), stack)
 146   let focus goal ((proof, _, _), stack) = (proof, goal), stack
 147 end
 148
 149 module S = ProofEngineStatus
 150 module C = Continuationals.Make (S)
 151
 152 type tactic = S.tactic
 153
 154 let fold_eval status ts =
 155   let istatus =
 156     List.fold_left (fun istatus t -> S.focus ~-1 (C.eval t istatus)) status ts
 157   in
 158   S.inject istatus
 159
 160 (* Tacticals implemented on top of tynycals *)
 161
 162 let thens ~start ~continuations =
 163   S.mk_tactic
 164     (fun istatus ->
 165       fold_eval istatus
 166         ([ C.Tactical (C.Tactic start); C.Branch ]
 167         @ (HExtlib.list_concat ~sep:[ C.Shift ]
 168             (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) continuations))
 169         @ [ C.Merge ]))
 170
 171 let then_ ~start ~continuation =
 172   S.mk_tactic
 173     (fun istatus ->
 174       let ostatus = C.eval (C.Tactical (C.Tactic start)) istatus in
 175       let opened,closed = S.goals ostatus in
 176        match opened with
 177           [] -> ostatus
 178         | _ ->
 179           fold_eval (S.focus ~-1 ostatus)
 180             [ C.Semicolon;
 181               C.Tactical (C.Tactic continuation) ])
 182
 183 let seq ~tactics =
 184   S.mk_tactic
 185     (fun istatus ->
 186       fold_eval istatus
 187         (HExtlib.list_concat ~sep:[ C.Semicolon ]
 188           (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
 189
 190 (* Tacticals that cannot be implemented on top of tynycals *)
 191
 192 let first ~tactics =
 193   let rec first ~(tactics: (string * tactic) list) status =
 194     info (lazy "in Tacticals.first");
 195     match tactics with
 196       [] -> raise (PET.Fail (lazy "first: no tactics left"))
 197     | (descr, tac)::tactics ->
 198         info (lazy ("Tacticals.first IS TRYING " ^ descr));
 199         try
 200          let res = PET.apply_tactic tac status in
 201           info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
 202           res
 203         with
 204          PET.Fail _ -> first ~tactics status
 205   in
 206   PET.mk_tactic (first ~tactics)
 207
 208
 209 let rec do_tactic ~n ~tactic =
 210  PET.mk_tactic
 211   (function status ->
 212     if n = 0 then
 213      PET.apply_tactic id_tac status
 214     else
 215      PET.apply_tactic
 216       (then_ ~start:tactic ~continuation:(do_tactic ~n:(n-1) ~tactic))
 217       status)
 218
 219 (* This applies tactic and catches its possible failure *)
 220 let try_tactic ~tactic =
 221  let try_tactic status =
 222   try
 223     PET.apply_tactic tactic status
 224   with (PET.Fail _) as e ->
 225     info (lazy (
 226       "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
 227     PET.apply_tactic id_tac status
 228  in
 229   PET.mk_tactic try_tactic
 230
 231 let rec repeat_tactic ~tactic =
 232  ProofEngineTypes.mk_tactic
 233   (fun status ->
 234     ProofEngineTypes.apply_tactic
 235      (then_ ~start:tactic
 236        ~continuation:(try_tactic (repeat_tactic ~tactic))) status)
 237
 238 (* This tries tactics until one of them solves the goal *)
 239 let solve_tactics ~tactics =
 240  let rec solve_tactics ~(tactics: (string * tactic) list) status =
 241   info (lazy "in Tacticals.solve_tactics");
 242   match tactics with
 243   | (descr, currenttactic)::moretactics ->
 244       info (lazy ("Tacticals.solve_tactics is trying " ^ descr));
 245       (try
 246         let (proof, opened) as output_status =
 247          PET.apply_tactic currenttactic status
 248         in
 249         match opened with
 250           | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^
 251                    " solved the goal!!!"));
 252                   output_status
 253           | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
 254                  raise (PET.Fail (lazy "Goal not solved"))
 255        with (PET.Fail _) as e ->
 256          info (lazy (
 257             "Tacticals.solve_tactics: current tactic failed with exn: "
 258             ^ Printexc.to_string e));
 259          solve_tactics ~tactics:moretactics status)
 260   | [] ->
 261       raise (PET.Fail
 262         (lazy "solve_tactics cannot solve the goal"))
 263  in
 264   PET.mk_tactic (solve_tactics ~tactics)
 265
 266 let progress_tactic ~tactic =
 267   let msg = lazy "Failed to progress" in
 268   let progress_tactic (((_,metasenv,_,_,_),_) as istatus) =
 269     let ((_,metasenv',_,_,_),_) as ostatus =
 270      PET.apply_tactic tactic istatus
 271     in
 272      (*CSC: Warning
 273        If just the index of some metas changes the tactic is recognized
 274        as a progressing one. This is wrong. *)
 275      if metasenv' = metasenv then
 276       raise (PET.Fail msg)
 277      else
 278       ostatus
 279   in
 280   PET.mk_tactic progress_tactic