(* Copyright (C) 2002, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

open CicReduction
open PrimitiveTactics
open ProofEngineTypes
open UriManager

(** DEBUGGING *)

  (** perform debugging output? *)
let debug = false

  (** debugging print *)
let warn s =
  if debug then
    prerr_endline ("TACTICALS WARNING: " ^ s)

(** AUX TACTIC{,AL}S *)

  (**
    naive implementation of ORELSE tactical, try a sequence of tactics in turn:
    if one fails pass to the next one and so on, eventually raises (failure "no
    tactics left")
    TODO warning: not tail recursive due to "try .. with" boxing
  *)
let rec try_tactics ~(tactics: (string * tactic) list) ~status =
  warn "in Ring.try_tactics";
  match tactics with
  | (descr, tac)::tactics ->
      warn ("Ring.try_tactics IS TRYING " ^ descr);
      (try
        let res = tac ~status in
        warn ("Ring.try_tactics: " ^ descr ^ " succedeed!!!");
        res
       with
        e ->
         match e with
            (Fail _)
          | (CicTypeChecker.NotWellTyped _)
          | (CicUnification.UnificationFailed) ->
              warn (
                "Ring.try_tactics failed with exn: " ^
                Printexc.to_string e);
              try_tactics ~tactics ~status
        | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
      )
  | [] -> raise (Fail "try_tactics: no tactics left")

let thens ~start ~continuations ~status =
 let (proof,new_goals) = start ~status in
  try
   List.fold_left2
    (fun (proof,goals) goal tactic ->
      let (proof',new_goals') = tactic ~status:(proof,goal) in
       (proof',goals@new_goals')
    ) (proof,[]) new_goals continuations
  with
   Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")

let then_ ~start ~continuation ~status =
 let (proof,new_goals) = start ~status in
  List.fold_left
   (fun (proof,goals) goal ->
     let (proof',new_goals') = continuation ~status:(proof,goal) in
      (proof',goals@new_goals')
   ) (proof,[]) new_goals