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