From 7eb9140b9347edefbe859c4736187a9f5809c322 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 26 Feb 2004 14:52:16 +0000 Subject: [PATCH] added command and script ASTs with _debugging_only_ pretty printers --- helm/ocaml/cic_transformations/.depend | 8 +- helm/ocaml/cic_transformations/Makefile | 5 +- helm/ocaml/cic_transformations/commandAst.ml | 112 +++++++++++++++++++ helm/ocaml/cic_transformations/tacticAst.ml | 6 +- 4 files changed, 124 insertions(+), 7 deletions(-) create mode 100644 helm/ocaml/cic_transformations/commandAst.ml diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index 7b0cced55..7506b4d52 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -9,6 +9,10 @@ acic2Ast.cmi: cicAst.cmo 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 @@ -57,7 +61,7 @@ tacticAstPp.cmo: cicAstPp.cmi tacticAst.cmo tacticAstPp.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 diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index 576861290..41517807a 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -15,7 +15,10 @@ INTERFACE_FILES = \ applyStylesheets.mli applyTransformation.mli \ acic2Ast.mli tacticAstPp.mli boxPp.mli tacticAst2Box.mli IMPLEMENTATION_FILES = \ - cicAst.ml tacticAst.ml $(INTERFACE_FILES:%.mli=%.ml) + cicAst.ml \ + tacticAst.ml \ + $(INTERFACE_FILES:%.mli=%.ml) \ + commandAst.ml EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = diff --git a/helm/ocaml/cic_transformations/commandAst.ml b/helm/ocaml/cic_transformations/commandAst.ml new file mode 100644 index 000000000..cab4c2a2e --- /dev/null +++ b/helm/ocaml/cic_transformations/commandAst.ml @@ -0,0 +1,112 @@ +(* 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) + diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 833e1b1c4..fbb281c49 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -23,8 +23,6 @@ * http://helm.cs.unibo.it/ *) -type location = int * int - type direction = [ `Left | `Right ] type reduction_kind = [ `Reduce | `Simpl | `Whd ] type 'term pattern = Pattern of 'term @@ -33,7 +31,7 @@ type 'term pattern = Pattern of 'term to the current goal *) type ('term, 'ident) tactic = - | LocatedTactic of location * ('term, 'ident) tactic + | LocatedTactic of CicAst.location * ('term, 'ident) tactic | Absurd | Apply of 'term @@ -68,7 +66,7 @@ type ('term, 'ident) tactic = | Transitivity of 'term type 'tactic tactical = - | LocatedTactical of location * 'tactic tactical + | LocatedTactical of CicAst.location * 'tactic tactical | Fail | Do of int * 'tactic tactical -- 2.39.2