From: Stefano Zacchiroli Date: Fri, 30 Apr 2004 09:25:36 +0000 (+0000) Subject: embedded commands ast into tacticals ast X-Git-Tag: V_0_0_9~62 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=511f0c1672e0db4cf577afc9b79f12dea39469ad embedded commands ast into tacticals ast --- diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index 7f03ceb1a..c35209cdb 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -49,10 +49,12 @@ applyStylesheets.cmo: cic2Xml.cmi misc.cmi sequentPp.cmi xml2Gdome.cmi \ 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 @@ -63,5 +65,3 @@ tacticAst2Box.cmo: ast2pres.cmi box.cmi boxPp.cmi cicAstPp.cmi tacticAst.cmo \ 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 diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index 41517807a..9b16740b3 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -17,8 +17,7 @@ INTERFACE_FILES = \ IMPLEMENTATION_FILES = \ cicAst.ml \ tacticAst.ml \ - $(INTERFACE_FILES:%.mli=%.ml) \ - commandAst.ml + $(INTERFACE_FILES:%.mli=%.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 deleted file mode 100644 index cab4c2a2e..000000000 --- a/helm/ocaml/cic_transformations/commandAst.ml +++ /dev/null @@ -1,112 +0,0 @@ -(* 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 fbb281c49..f0dad83e2 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -65,17 +65,43 @@ type ('term, 'ident) tactic = | 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 *) diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index 5d8fae1b6..4b79607f5 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -227,7 +227,12 @@ and big_tactic2box ?(attr = []) = function 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); @@ -238,7 +243,6 @@ let rec tactical2box ?(attr = []) = function 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; diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.mli b/helm/ocaml/cic_transformations/tacticAst2Box.mli index 36eeb3e73..0eeef6c53 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.mli +++ b/helm/ocaml/cic_transformations/tacticAst2Box.mli @@ -34,9 +34,8 @@ 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 diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 6627c4613..4380dd5df 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -77,14 +77,39 @@ let rec pp_tactic = function | 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 diff --git a/helm/ocaml/cic_transformations/tacticAstPp.mli b/helm/ocaml/cic_transformations/tacticAstPp.mli index f75e3f317..356b07e76 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.mli +++ b/helm/ocaml/cic_transformations/tacticAstPp.mli @@ -25,7 +25,5 @@ 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