tacticAstPp.cmi: cicAst.cmo tacticAst.cmo
boxPp.cmi: box.cmi cicAst.cmo
tacticAst2Box.cmi: box.cmi cicAst.cmo tacticAst.cmo
+tacticAst.cmo: cicAst.cmo
+tacticAst.cmx: cicAst.cmx
+commandAst.cmo: cicAst.cmo cicAstPp.cmi tacticAst.cmo tacticAstPp.cmi
+commandAst.cmx: cicAst.cmx cicAstPp.cmx tacticAst.cmx tacticAstPp.cmx
box.cmo: box.cmi
box.cmx: box.cmi
contentTable.cmo: cicAst.cmo contentTable.cmi
tacticAstPp.cmx: cicAstPp.cmx tacticAst.cmx tacticAstPp.cmi
boxPp.cmo: ast2pres.cmi box.cmi cicAstPp.cmi boxPp.cmi
boxPp.cmx: ast2pres.cmx box.cmx cicAstPp.cmx boxPp.cmi
-tacticAst2Box.cmo: ast2pres.cmi box.cmi boxPp.cmi tacticAst.cmo \
+tacticAst2Box.cmo: ast2pres.cmi box.cmi boxPp.cmi cicAstPp.cmi tacticAst.cmo \
tacticAstPp.cmi tacticAst2Box.cmi
-tacticAst2Box.cmx: ast2pres.cmx box.cmx boxPp.cmx tacticAst.cmx \
+tacticAst2Box.cmx: ast2pres.cmx box.cmx boxPp.cmx cicAstPp.cmx tacticAst.cmx \
tacticAstPp.cmx tacticAst2Box.cmi
--- /dev/null
+(* 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)
+
projects / helm.git / commitdiff