1 (* Copyright (C) 2004, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
26 type location = CicAst.location
28 (* TODO do we need this at the ast level? *)
29 (* in Coq these are all synonymous except definition which is transparent *)
40 | Theorem of location *
41 thm_flavour * string option * 'term * 'term option
42 (* flavour, name, type, body
43 * - name is absent when an unnamed theorem is being proved, tipically in
45 * - body is present when its given along with the command, otherwise it
46 * will be given in proof editing mode using the tactical language
52 * Name is needed when theorem was started without providing a name
59 (** body via tactic applications *)
60 | Tactics of location *
61 ('term, string) TacticAst.tactic TacticAst.tactical list
62 | Verbatim of location * 'term (** body via verbatim term *)
64 type 'term script_entry =
65 | Theorem of thm_flavour * string * 'term * 'term thm_body
66 (* flavour, name, type, body *)
68 type 'term script = 'term script_entry list
74 (** Just for debugging: not real pretty printers *)
78 let pp_flavour = function
79 | `Definition -> "Definition"
84 | `Theorem -> "Theorem"
86 let pp_command = function
87 | Theorem (_, flavour, name, typ, body) ->
88 sprintf "%s %s: %s %s."
90 (match name with None -> "" | Some name -> name)
91 (CicAstPp.pp_term typ)
94 | Some body -> "\\def " ^ CicAstPp.pp_term body)
97 (match name with None -> "Qed." | Some name -> sprintf "Save %s." name)
99 let pp_script_entry = function
100 | Script.Theorem (flavour, name, typ, body) ->
101 sprintf "%s %s: %s%s"
102 (pp_flavour flavour) name (CicAstPp.pp_term typ)
104 | Script.Tactics (_, tacs) ->
106 (String.concat "\n" (List.map TacticAstPp.pp_tactical tacs)) ^
108 | Script.Verbatim (_, body) ->
109 " \\def " ^ CicAstPp.pp_term body ^ ".\n")
111 let pp_script script = String.concat "\n\n" (List.map pp_script_entry script)