(* Copyright (C) 2004, 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://helm.cs.unibo.it/
 *)

  (** exceptions whose content should be presented to the user *)
exception Not_implemented of string
exception Failure of string

val not_implemented : string -> 'a
val error : string -> 'a
val warning : string -> unit
val debug_print : string -> unit

exception No_proof  (** no current proof is available *)
exception Cancel
exception Unbound_identifier of string

  (** @param exn an exception
  * @return a string which is meant to be a textual explaination of the
   exception understandable by a user *)
val explain: exn -> string

val unopt_uri : 'a option -> 'a

  (** {3 disambiguator callbacks} *)

type choose_uris_callback =
  selection_mode:[ `MULTIPLE | `SINGLE ] ->
  ?title:string ->
  ?msg:string -> ?nonvars_button:bool -> string list -> string list

type choose_interp_callback = (string * string) list list -> int list

  (** @raise Failure if called, use if unambiguous input is required *)
val mono_uris_callback: choose_uris_callback
  (** @raise Failure if called, use if unambiguous input is required *)
val mono_interp_callback: choose_interp_callback

(** {2 major matita objects} *)

class type parserr =
  object
    method parseTactical : char Stream.t -> DisambiguateTypes.tactical
    method parseTerm : char Stream.t -> DisambiguateTypes.term
  end

  (* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
class type console =
  object
    method clear : unit -> unit
    method echo_error : string -> unit
    method echo_message : string -> unit
    method wrap_exn : 'a. (unit -> 'a) -> 'a option
  end

class type disambiguator =
  object
    method env : DisambiguateTypes.environment
    method setEnv : DisambiguateTypes.environment -> unit

    method chooseUris: choose_uris_callback
    method setChooseUris: choose_uris_callback -> unit

    method chooseInterp: choose_interp_callback
    method setChooseInterp: choose_interp_callback -> unit

    method parserr: parserr

      (* TODO Zack: as long as matita doesn't support MDI inteface,
      * disambiguateTerm will return a single term *)
      (** @param env disambiguation environment. If this parameter is given the
      * disambiguator act statelessly, that is internal disambiguation status
      * want be changed but only returned. If this parameter is not given the
      * internal one will be used and updated with the disambiguation status
      * resulting from the disambiguation *)
    method disambiguateTerm :
      ?context:Cic.context ->
      ?metasenv:Cic.metasenv ->
      ?env:DisambiguateTypes.environment ->
      char Stream.t ->
      DisambiguateTypes.environment * Cic.metasenv * Cic.term *
      CicUniv.universe_graph

      (** @param env @see disambiguateTerm above *)
    method disambiguateTermAst :
      ?context:Cic.context ->
      ?metasenv:Cic.metasenv ->
      ?env:DisambiguateTypes.environment ->
      DisambiguateTypes.term ->
      DisambiguateTypes.environment * Cic.metasenv * Cic.term *
      CicUniv.universe_graph

      (** as disambiguateTermAst, but disambiguate a list of ASTs at once. All
      * AST should be closed hence no context param is permitted on this method
      *)
    method disambiguateTermAsts :
      ?metasenv:Cic.metasenv ->
      ?env:DisambiguateTypes.environment ->
      DisambiguateTypes.term list ->
      DisambiguateTypes.environment * Cic.metasenv * Cic.term list *
      CicUniv.universe_graph
  end

class type proof =
  object
    inherit [unit] StatefulProofEngine.status

    (** return a pair of "xml" (as defined in Xml module) representing the *
     * current proof type and body, respectively *)
    method toXml : Xml.token Stream.t * Xml.token Stream.t

    method toString : string
  end

class type currentProof =
  object
    method onGoing: unit -> bool  (** true if a proof is on going *)
    method proof: proof           (** @raise Failure "No current proof" *)
    method start: proof -> unit   (** starts a new proof *)
    method abort: unit -> unit    (** abort the on going proof *)
    method quit: unit -> unit     (** quit matita *)
  end

  (** first component represents success: true = success, false = failure
  * second component represents console action: true = hide, false = keep *)
type command_outcome = bool * bool

  (** schematic representation of items scripts are made of *)
type script_item =
  [ `Tactic                       (** action on proof status *)
  | `Theorem                      (** start of proof, to be proved *)
  | `Qed of UriManager.uri        (** end of proof, successfull *)
  | `Def of UriManager.uri        (** constant with body *)
  | `Inductive of UriManager.uri  (** inductive definition *)
  ]

  (** interpreter for toplevel phrases given via console *)
class type interpreter =
  object
      (** parse a single phrase contained in the input string. Additional
      * garbage at the end of the phrase is ignored
      * @return true if no exception has been raised by the evaluation, false
      * otherwise
      *)
    method evalPhrase: string -> command_outcome

      (** as evalPhrase above, but parses a character stream. Only characters
      * composing next phrases are consumed *)
(*     method evalStream: char Stream.t -> command_outcome *)

      (** as above, evaluating a command/tactics AST *)
    method evalAst: DisambiguateTypes.tactical -> command_outcome

    (** {3 callbacks} *)

    method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit

    (** {3 stateful methods}
     * bookkeeping of last interpreted phrase *)

      (** offset from the starting of the last string parser by evalPhrase where
      * parsing stop.
      * @raise Failure when no offset has been recorded *)
    method endOffset: int

      (** last item parsed *)
    method lastItem: script_item option

      (** change internal interpreter state *)
    method setState: [`Proof | `Command] -> unit

  end

(** {2 MathML widgets} *)

type term_source =
  [ `Ast of DisambiguateTypes.term
  | `Cic of Cic.term
  | `String of string
  ]

class type mathViewer =
  object
    method checkTerm: term_source -> unit
  end

class type cicBrowser =
  object
    method loadUri: string -> unit
    method loadTerm: term_source -> unit
  end

type mml_of_cic_sequent =
  Cic.metasenv ->
  Cic.conjecture ->
  Gdome.document *
  ((Cic.id, Cic.term) Hashtbl.t * (Cic.id, Cic.id option) Hashtbl.t *
   (string, Cic.hypothesis) Hashtbl.t)

type mml_of_cic_object =
  explode_all:bool ->
  UriManager.uri ->
  Cic.annobj ->
  (string, string) Hashtbl.t ->
  (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document

(** {2 shorthands} *)

type namer = ProofEngineTypes.mk_fresh_name_type