applyStylesheets.cmi
applyStylesheets.cmx: cic2Xml.cmx misc.cmx sequentPp.cmx xml2Gdome.cmx \
applyStylesheets.cmi
-applyTransformation.cmo: content2pres.cmi misc.cmi mpresentation.cmi \
- sequent2pres.cmi xml2Gdome.cmi applyTransformation.cmi
-applyTransformation.cmx: content2pres.cmx misc.cmx mpresentation.cmx \
- sequent2pres.cmx xml2Gdome.cmx applyTransformation.cmi
+applyTransformation.cmo: cexpr2pres.cmi cexpr2pres_hashtbl.cmi \
+ content2pres.cmi misc.cmi mpresentation.cmi sequent2pres.cmi \
+ xml2Gdome.cmi applyTransformation.cmi
+applyTransformation.cmx: cexpr2pres.cmx cexpr2pres_hashtbl.cmx \
+ content2pres.cmx misc.cmx mpresentation.cmx sequent2pres.cmx \
+ xml2Gdome.cmx applyTransformation.cmi
acic2Ast.cmo: cicAst.cmo acic2Ast.cmi
acic2Ast.cmx: cicAst.cmx acic2Ast.cmi
tacticAstPp.cmo: cicAstPp.cmi tacticAst.cmo tacticAstPp.cmi
tacticAstPp.cmi tacticAst2Box.cmi
tacticAst2Box.cmx: ast2pres.cmx box.cmx boxPp.cmx cicAstPp.cmx tacticAst.cmx \
tacticAstPp.cmx tacticAst2Box.cmi
-commandAst.cmo: cicAst.cmo cicAstPp.cmi tacticAst.cmo tacticAstPp.cmi
-commandAst.cmx: cicAst.cmx cicAstPp.cmx tacticAst.cmx tacticAstPp.cmx
IMPLEMENTATION_FILES = \
cicAst.ml \
tacticAst.ml \
- $(INTERFACE_FILES:%.mli=%.ml) \
- commandAst.ml
+ $(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL =
EXTRA_OBJECTS_TO_CLEAN =
+++ /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)
-
| Symmetry
| Transitivity of 'term
-type 'tactic tactical =
- | LocatedTactical of CicAst.location * 'tactic tactical
+type thm_flavour =
+ [ `Definition
+ | `Fact
+ | `Goal
+ | `Lemma
+ | `Remark
+ | `Theorem
+ ]
+
+type 'term command =
+ | Proof
+ | Theorem of 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
+ *)
+ | Qed of string option
+ (* name.
+ * Name is needed when theorem was started without providing a name
+ *)
+ | Quit
+
+type ('term, 'ident) tactical =
+ | LocatedTactical of CicAst.location * ('term, 'ident) tactical
+
+ | Tactic of ('term, 'ident) tactic
+ | Command of 'term command
| Fail
- | Do of int * 'tactic tactical
+ | Do of int * ('term, 'ident) tactical
| IdTac
- | Repeat of 'tactic tactical
- | Seq of 'tactic tactical list (* sequential composition *)
- | Tactic of 'tactic
- | Then of 'tactic tactical * 'tactic tactical list
- | Tries of 'tactic tactical list
+ | Repeat of ('term, 'ident) tactical
+ | Seq of ('term, 'ident) tactical list (* sequential composition *)
+ | Then of ('term, 'ident) tactical * ('term, 'ident) tactical list
+ | Tries of ('term, 'ident) tactical list
(* try a sequence of tacticals until one succeeds, fail otherwise *)
- | Try of 'tactic tactical (* try a tactical and mask failures *)
+ | Try of ('term, 'ident) tactical (* try a tactical and mask failures *)
open TacticAst
let rec tactical2box ?(attr = []) = function
- LocatedTactical (loc, tac) -> tactical2box tac
+ | LocatedTactical (loc, tac) -> tactical2box tac
+
+ | Tactic tac -> tactic2box tac
+ | Command cmd -> (* TODO dummy implementation *)
+ Box.Text([], TacticAstPp.pp_tactical (Command cmd))
+
| Fail -> Box.Text([],"fail")
| Do (count, tac) ->
Box.V([],[Box.Text([],"do " ^ string_of_int count);
Box.indent (tactical2box tac)])
| Seq tacs ->
Box.V([],tacticals2box tacs)
- | Tactic tac -> tactic2box tac
| Then (tac, tacs) ->
Box.V([],[tactical2box tac;
Box.H([],[Box.skip;
val tactical2box:
- ?attr:'a list
- -> (CicAst.term, string) TacticAst.tactic TacticAst.tactical
- -> CicAst.term Box.box
+ ?attr:'a list -> (CicAst.term, string) TacticAst.tactical ->
+ CicAst.term Box.box
+
+val tacticalPp: (CicAst.term, string) TacticAst.tactical -> string
-val tacticalPp:
- (CicAst.term, string) TacticAst.tactic TacticAst.tactical -> string
| Symmetry -> "symmetry"
| Transitivity term -> "transitivity " ^ pp_term term
+let pp_flavour = function
+ | `Definition -> "Definition"
+ | `Fact -> "Fact"
+ | `Goal -> "Goal"
+ | `Lemma -> "Lemma"
+ | `Remark -> "Remark"
+ | `Theorem -> "Theorem"
+
+let pp_command = function
+ | Proof -> "Proof."
+ | 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)
+ | Qed name ->
+ (match name with None -> "Qed." | Some name -> sprintf "Save %s." name)
+ | Quit -> "Quit."
+
let rec pp_tactical = function
| LocatedTactical (loc, tac) -> pp_tactical tac
+
+ | Tactic tac -> pp_tactic tac
+ | Command cmd -> pp_command cmd
+
| Fail -> "fail"
| Do (count, tac) -> sprintf "do %d %s" count (pp_tactical tac)
| IdTac -> "id"
| Repeat tac -> "repeat " ^ pp_tactical tac
| Seq tacs -> pp_tacticals tacs
- | Tactic tac -> pp_tactic tac
| Then (tac, tacs) -> sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs)
| Tries tacs -> sprintf "tries [%s]" (pp_tacticals tacs)
| Try tac -> "try " ^ pp_tactical tac
val pp_tactic: (CicAst.term, string) TacticAst.tactic -> string
-val pp_tactical:
- (CicAst.term, string) TacticAst.tactic TacticAst.tactical ->
- string
+val pp_tactical: (CicAst.term, string) TacticAst.tactical -> string
projects / helm.git / commitdiff