(* 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/
 *)

type location = CicAst.location

  (* TODO do we need this at the ast level? *)
  (* in Coq these are all synonymous except definition which is transparent *)
type thm_flavour =
  [ `Definition
  | `Fact
  | `Goal
  | `Lemma
  | `Remark
  | `Theorem
  ]

type 'term command =
  | Theorem of location *
      thm_flavour * string option * 'term * 'term option
      (* flavour, name, type, body
       * - name is absent when an unnamed theorem is being proved, tipically in
       *   interactive usage
       * - body is present when its given along with the command, otherwise it
       *   will be given in proof editing mode using the tactical language
       *)
  | Proof of location
  | Qed of location *
      string option
      (* name.
       * Name is needed when theorem was started without providing a name
       *)

module Script =
  struct

    type 'term thm_body =
        (** body via tactic applications *)
      | Tactics of location *
          ('term, string) TacticAst.tactic TacticAst.tactical list
      | Verbatim of location * 'term  (** body via verbatim term *)

    type 'term script_entry =
      | Theorem of thm_flavour * string * 'term * 'term thm_body
          (* flavour, name, type, body *)

    type 'term script = 'term script_entry list

  end

(**/**)

(** Just for debugging: not real pretty printers *)

open Printf

let pp_flavour = function
  | `Definition -> "Definition"
  | `Fact -> "Fact"
  | `Goal -> "Goal"
  | `Lemma -> "Lemma"
  | `Remark -> "Remark"
  | `Theorem -> "Theorem"

let pp_command = function
  | Theorem (_, flavour, name, typ, body) ->
      sprintf "%s %s: %s %s."
        (pp_flavour flavour)
        (match name with None -> "" | Some name -> name)
        (CicAstPp.pp_term typ)
        (match body with
        | None -> ""
        | Some body -> "\\def " ^ CicAstPp.pp_term body)
  | Proof _ -> "Proof."
  | Qed (_, name) ->
      (match name with None -> "Qed." | Some name -> sprintf "Save %s." name)

let pp_script_entry = function
  | Script.Theorem (flavour, name, typ, body) ->
      sprintf "%s %s: %s%s"
        (pp_flavour flavour) name (CicAstPp.pp_term typ)
        (match body with
        | Script.Tactics (_, tacs) ->
            ".\n" ^
            (String.concat "\n" (List.map TacticAstPp.pp_tactical tacs)) ^
            "\nQed.\n"
        | Script.Verbatim (_, body) ->
            " \\def " ^ CicAstPp.pp_term body ^ ".\n")

let pp_script script = String.concat "\n\n" (List.map pp_script_entry script)