From f065a68682b23976d185370d85869c196da3f20b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 17 Feb 2004 23:57:44 +0000 Subject: [PATCH] added tactics and tacticals (heavily bugged) --- helm/ocaml/cic_transformations/.depend | 7 +- helm/ocaml/cic_transformations/Makefile | 4 +- helm/ocaml/cic_transformations/tacticAst.ml | 83 +++++++++++++++++ helm/ocaml/cic_transformations/tacticAstPp.ml | 93 +++++++++++++++++++ .../ocaml/cic_transformations/tacticAstPp.mli | 31 +++++++ 5 files changed, 214 insertions(+), 4 deletions(-) create mode 100644 helm/ocaml/cic_transformations/tacticAst.ml create mode 100644 helm/ocaml/cic_transformations/tacticAstPp.ml create mode 100644 helm/ocaml/cic_transformations/tacticAstPp.mli diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index 9a356a17b..ceed54c22 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -6,6 +6,7 @@ sequent2pres.cmi: mpresentation.cmi cexpr2pres_hashtbl.cmi: content_expressions.cmi mpresentation.cmi acic2Ast.cmi: cicAst.cmo cicAstPp.cmi: cicAst.cmo +tacticAstPp.cmi: cicAst.cmo tacticAst.cmo boxPp.cmi: box.cmi cicAst.cmo box.cmo: box.cmi box.cmx: box.cmi @@ -23,8 +24,8 @@ content2pres.cmo: cexpr2pres.cmi content_expressions.cmi mpresentation.cmi \ content2pres.cmi content2pres.cmx: cexpr2pres.cmx content_expressions.cmx mpresentation.cmx \ content2pres.cmi -ast2pres.cmo: box.cmi cicAst.cmo mpresentation.cmi ast2pres.cmi -ast2pres.cmx: box.cmx cicAst.cmx mpresentation.cmx ast2pres.cmi +ast2pres.cmo: box.cmi cicAst.cmo ast2pres.cmi +ast2pres.cmx: box.cmx cicAst.cmx ast2pres.cmi sequent2pres.cmo: cexpr2pres.cmi content_expressions.cmi mpresentation.cmi \ sequent2pres.cmi sequent2pres.cmx: cexpr2pres.cmx content_expressions.cmx mpresentation.cmx \ @@ -51,5 +52,7 @@ acic2Ast.cmo: cicAst.cmo acic2Ast.cmi acic2Ast.cmx: cicAst.cmx acic2Ast.cmi cicAstPp.cmo: cicAst.cmo cicAstPp.cmi cicAstPp.cmx: cicAst.cmx cicAstPp.cmi +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 diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index c16e7271e..615ff9ff3 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -13,9 +13,9 @@ INTERFACE_FILES = \ sequent2pres.mli \ cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli sequentPp.mli \ applyStylesheets.mli applyTransformation.mli \ - acic2Ast.mli cicAstPp.mli boxPp.mli + acic2Ast.mli cicAstPp.mli tacticAstPp.mli boxPp.mli IMPLEMENTATION_FILES = \ - cicAst.ml $(INTERFACE_FILES:%.mli=%.ml) + cicAst.ml tacticAst.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml new file mode 100644 index 000000000..833e1b1c4 --- /dev/null +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -0,0 +1,83 @@ +(* 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 = int * int + +type direction = [ `Left | `Right ] +type reduction_kind = [ `Reduce | `Simpl | `Whd ] +type 'term pattern = Pattern of 'term + + (* when an 'ident option is None, the default is to apply the tactic + to the current goal *) + +type ('term, 'ident) tactic = + | LocatedTactic of location * ('term, 'ident) tactic + + | Absurd + | Apply of 'term + | Assumption + | Change of 'term * 'term * 'ident option (* what, with what, where *) + | Change_pattern of 'term pattern * 'term * 'ident option + (* what, with what, where *) + | Contradiction + | Cut of 'term + | Decompose of 'ident * 'ident list (* where, which principles *) + | Discriminate of 'ident + | Elim of 'term * 'term option (* what to elim, which principle to use *) + | ElimType of 'term + | Exact of 'term + | Exists + | Fold of reduction_kind * 'term + | Fourier + | Injection of 'ident + | Intros of int option * 'ident list + | Left + | LetIn of 'term * 'ident +(* | Named_intros of 'ident list (* joined with Intros above *) *) + | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *) + | Reflexivity + | Replace of 'term * 'term (* what, with what *) + | Replace_pattern of 'term pattern * 'term + | Rewrite of direction * 'term * 'ident option + | Right + | Ring + | Split + | Symmetry + | Transitivity of 'term + +type 'tactic tactical = + | LocatedTactical of location * 'tactic tactical + + | Fail + | Do of int * 'tactic 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 + (* try a sequence of tacticals until one succeeds, fail otherwise *) + | Try of 'tactic tactical (* try a tactical and mask failures *) + diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml new file mode 100644 index 000000000..50ef218f8 --- /dev/null +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -0,0 +1,93 @@ +(* 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/ + *) + +open Printf + +open TacticAst + +let pp_term term = CicAstPp.pp_term term + +let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" + +let pp_reduction_kind = function + | `Reduce -> "reduce" + | `Simpl -> "simpl" + | `Whd -> "whd" + +let rec pp_tactic = function + | LocatedTactic (loc, tac) -> pp_tactic tac + | Absurd -> "absurd" + | Apply term -> "apply " ^ pp_term term + | Assumption -> "assumption" + | Change (t1, t2, where) -> + sprintf "change %s with %s%s" (pp_term t1) (pp_term t2) + (match where with None -> "" | Some ident -> "in " ^ ident) + | Change_pattern (_, _, _) -> assert false (* TODO *) + | Contradiction -> "contradiction" + | Cut term -> "cut " ^ pp_term term + | Decompose (ident, principles) -> + sprintf "decompose %s %s" (pp_idents principles) ident + | Discriminate ident -> "discriminate " ^ ident + | Elim (term, using) -> + sprintf "elim " ^ pp_term term ^ + (match using with None -> "" | Some term -> "using " ^ pp_term term) + | ElimType term -> "elim type " ^ pp_term term + | Exact term -> "exact " ^ pp_term term + | Exists -> "exists" + | Fold (kind, term) -> + sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term term) + | Fourier -> "fourier" + | Injection ident -> "injection " ^ ident + | Intros (num, idents) -> + sprintf "intros%s%s" + (match num with None -> "" | Some num -> " " ^ string_of_int num) + (match idents with [] -> "" | idents -> pp_idents idents) + | Left -> "left" + | LetIn (term, ident) -> sprintf "let %s in %s" (pp_term term) ident + | Reduce (_, _, _) -> assert false (* TODO *) + | Reflexivity -> "reflexivity" + | Replace (t1, t2) -> sprintf "replace %s with %s" (pp_term t1) (pp_term t2) + | Replace_pattern (_, _) -> assert false (* TODO *) + | Rewrite (_, _, _) -> assert false (* TODO *) + | Right -> "right" + | Ring -> "ring" + | Split -> "split" + | Symmetry -> "symmetry" + | Transitivity term -> "transitivity " ^ pp_term term + +let rec pp_tactical = function + | LocatedTactical (loc, tac) -> pp_tactical tac + | 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 + +and pp_tacticals tacs = String.concat "; " (List.map pp_tactical tacs) + diff --git a/helm/ocaml/cic_transformations/tacticAstPp.mli b/helm/ocaml/cic_transformations/tacticAstPp.mli new file mode 100644 index 000000000..f75e3f317 --- /dev/null +++ b/helm/ocaml/cic_transformations/tacticAstPp.mli @@ -0,0 +1,31 @@ +(* 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/ + *) + +val pp_tactic: (CicAst.term, string) TacticAst.tactic -> string + +val pp_tactical: + (CicAst.term, string) TacticAst.tactic TacticAst.tactical -> + string + -- 2.39.2