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