(*
    Copyright (C) 2003-19 Richard Bornat & Bernard Sufrin
     
        richard@bornat.me.uk
        sufrin@comlab.ox.ac.uk

    This file is part of the jape proof engine, which is part of jape.

    Jape 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.

    Jape 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 jape; if not, write to the Free Software
    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
    (or look at http://www.gnu.org).

*)

open Termtype
open Sequent
open Cxttype
open Tactictype
open Prooftree.Tree.Fmttree
 
type prooftree = Prooftree.Tree.Fmttree.prooftree
 and path = Prooftree.Tree.Fmttree.path
 
(* should this be public? RB *)
(* sometimes -- currently only in doCUTIN -- the tree is not the whole tree, so
   tree provisos -- currently only DischargeProviso -- can't be reliably checked.
   RB 2023/07/03
 *)
type proofstate = Proofstate of staterec
 and staterec = { cxt : cxt; tree : prooftree; wholetree : bool;
                  goal : path option; target : path option;
                  root : (prooftree * path) option;
                  givens : seq list
                }

val addautorule : bool * tactic -> unit
val autorules : unit -> (bool * tactic) list
val clearautorules : unit -> unit
val isproven : proofstate -> bool
val nextGoal : bool -> proofstate -> proofstate
val proofstate_cxt : proofstate -> cxt
val proofstate_givens : proofstate -> seq list
val proofstate_goal : proofstate -> path option
val proofstate_root : proofstate -> (prooftree * path) option
val proofstate_target : proofstate -> path option
val proofstate_tree : proofstate -> prooftree

val proofstep : cxt -> prooftree -> proofstate -> proofstate option
val prunestate : path -> proofstate -> proofstate
val rewriteproofstate : proofstate -> proofstate
val withcxt : proofstate -> cxt -> proofstate
val withgivens : proofstate -> seq list -> proofstate
val withgoal : proofstate -> path option -> proofstate
val withroot : proofstate -> (prooftree * path) option -> proofstate
val withtarget : proofstate -> path option -> proofstate
val withtree : proofstate -> prooftree -> proofstate
val withwhole : proofstate -> bool -> proofstate

val string_of_proofstate : bool -> proofstate -> string
val string_of_subtree : path option -> prooftree -> string
