From 9766d606b71ec69594919ca34b067e268afeabf0 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 19 Feb 2004 08:32:56 +0000 Subject: [PATCH] Adding tacticAst2Box (pretty printer for tactical, preliminary version). --- helm/ocaml/cic_transformations/.depend | 15 +- helm/ocaml/cic_transformations/Makefile | 4 +- helm/ocaml/cic_transformations/ast2pres.ml | 1 + helm/ocaml/cic_transformations/ast2pres.mli | 10 + .../cic_transformations/tacticAst2Box.ml | 267 ++++++++++++++++++ .../cic_transformations/tacticAst2Box.mli | 42 +++ 6 files changed, 332 insertions(+), 7 deletions(-) create mode 100644 helm/ocaml/cic_transformations/tacticAst2Box.ml create mode 100644 helm/ocaml/cic_transformations/tacticAst2Box.mli diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index ceed54c22..7b0cced55 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -1,13 +1,14 @@ contentTable.cmi: cicAst.cmo cexpr2pres.cmi: content_expressions.cmi mpresentation.cmi content2pres.cmi: mpresentation.cmi +cicAstPp.cmi: cicAst.cmo ast2pres.cmi: box.cmi cicAst.cmo 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 +tacticAst2Box.cmi: box.cmi cicAst.cmo tacticAst.cmo box.cmo: box.cmi box.cmx: box.cmi contentTable.cmo: cicAst.cmo contentTable.cmi @@ -24,8 +25,10 @@ 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 ast2pres.cmi -ast2pres.cmx: box.cmx cicAst.cmx ast2pres.cmi +cicAstPp.cmo: cicAst.cmo cicAstPp.cmi +cicAstPp.cmx: cicAst.cmx cicAstPp.cmi +ast2pres.cmo: box.cmi cicAst.cmo cicAstPp.cmi ast2pres.cmi +ast2pres.cmx: box.cmx cicAst.cmx cicAstPp.cmx ast2pres.cmi sequent2pres.cmo: cexpr2pres.cmi content_expressions.cmi mpresentation.cmi \ sequent2pres.cmi sequent2pres.cmx: cexpr2pres.cmx content_expressions.cmx mpresentation.cmx \ @@ -50,9 +53,11 @@ applyTransformation.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 -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 +tacticAst2Box.cmo: ast2pres.cmi box.cmi boxPp.cmi tacticAst.cmo \ + tacticAstPp.cmi tacticAst2Box.cmi +tacticAst2Box.cmx: ast2pres.cmx box.cmx boxPp.cmx tacticAst.cmx \ + tacticAstPp.cmx tacticAst2Box.cmi diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index 615ff9ff3..576861290 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -9,11 +9,11 @@ INTERFACE_FILES = \ box.mli contentTable.mli \ cic2Xml.mli content_expressions.mli \ mpresentation.mli cexpr2pres.mli content2pres.mli \ - ast2pres.mli \ + cicAstPp.mli ast2pres.mli \ sequent2pres.mli \ cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli sequentPp.mli \ applyStylesheets.mli applyTransformation.mli \ - acic2Ast.mli cicAstPp.mli tacticAstPp.mli boxPp.mli + acic2Ast.mli tacticAstPp.mli boxPp.mli tacticAst2Box.mli IMPLEMENTATION_FILES = \ cicAst.ml tacticAst.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml index c5d59029d..9679501ab 100644 --- a/helm/ocaml/cic_transformations/ast2pres.ml +++ b/helm/ocaml/cic_transformations/ast2pres.ml @@ -306,6 +306,7 @@ and make_subst start_txt varname body end_txt = [Box.Text([],end_txt)] and pretty_append l ast tail = + prerr_endline("pretty riceve: " ^ (CicAstPp.pp_term ast)); if is_big ast then [Box.H([],l); Box.H([],Box.skip::(bigast2box ast)::tail)] diff --git a/helm/ocaml/cic_transformations/ast2pres.mli b/helm/ocaml/cic_transformations/ast2pres.mli index dc370c2b9..32531a232 100644 --- a/helm/ocaml/cic_transformations/ast2pres.mli +++ b/helm/ocaml/cic_transformations/ast2pres.mli @@ -32,6 +32,16 @@ (* *) (**************************************************************************) +val maxsize : int + +val countterm : int -> CicAst.term -> int + +val pretty_append : + (CicAst.term Box.box) list -> + CicAst.term -> + (CicAst.term Box.box) list -> + (CicAst.term Box.box) list + val ast2box: ?priority:int -> ?assoc:bool -> diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml new file mode 100644 index 000000000..3c4026f95 --- /dev/null +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -0,0 +1,267 @@ +(* 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/ + *) + +(**************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 18/2/2004 *) +(* *) +(**************************************************************************) + + +open Ast2pres +open TacticAst + +let rec count_tactic current_size tac = + if current_size > maxsize then current_size + else match tac with + LocatedTactic (_, tac) -> count_tactic current_size tac + | Absurd -> current_size + 6 + | Apply term -> countterm (current_size+6) term + | Assumption -> current_size + 10 + | Change (t1, t2, where) -> + let size1 = countterm (current_size + 12) t1 in (* change, with *) + let size2 = countterm size1 t2 in + (match where with + None -> size2 + | Some ident -> size2 + 3 + String.length ident) + | Change_pattern (_, _, _) -> assert false (* TODO *) + | Contradiction -> current_size + 13 + | Cut term -> countterm (current_size + 4) term + | Decompose (ident, principles) -> + List.fold_left + (fun size s -> size + (String.length s)) + (current_size + 11 + String.length ident) principles + | Discriminate ident -> current_size + 12 + (String.length ident) + | Elim (term, using) -> + let size1 = countterm (current_size + 5) term in + (match using with + None -> size1 + | Some term -> countterm (size1 + 7) term) + | ElimType term -> countterm (current_size + 10) term + | Exact term -> countterm (current_size + 6) term + | Exists -> current_size + 6 + | Fold (kind, term) -> + countterm (current_size + 5) term + | Fourier -> current_size + 7 + | Injection ident -> current_size + 10 + (String.length ident) + | Intros (num, idents) -> + List.fold_left + (fun size s -> size + (String.length s)) + (current_size + 7) idents + | Left -> current_size + 4 + | LetIn (term, ident) -> + countterm (current_size + 5 + String.length ident) term + | Reduce (_, _, _) -> assert false (* TODO *) + | Reflexivity -> current_size + 11 + | Replace (t1, t2) -> + let size1 = countterm (current_size + 14) t1 in (* replace, with *) + countterm size1 t2 + | Replace_pattern (_, _) -> assert false (* TODO *) + | Rewrite (_, _, _) -> assert false (* TODO *) + | Right -> current_size + 5 + | Ring -> current_size + 4 + | Split -> current_size + 5 + | Symmetry -> current_size + 8 + | Transitivity term -> + countterm (current_size + 13) term +;; + +let is_big_tac tac = + let n = (count_tactic 0 tac) in + prerr_endline ("Lunghezza: " ^ (string_of_int n)); + n > maxsize +;; + +(* prova *) +let rec small_tactic2box ?(attr = []) tac = + Box.Text([], TacticAstPp.pp_tactic tac) + +let string_of_kind = function + | `Reduce -> "reduce" + | `Simpl -> "simpl" + | `Whd -> "whd" + +let rec tactic2box ?(attr = []) tac = + if (is_big_tac tac) then + big_tactic2box ~attr tac + else + small_tactic2box ~attr tac + +and big_tactic2box ?(attr = []) = function + LocatedTactic (loc, tac) -> + big_tactic2box ~attr tac + | Absurd -> Box.Text([],"absurd") + | Apply term -> + Box.V([],[Box.Text([],"apply"); + ast2box ~attr term]) + | Assumption -> Box.Text([],"assumption") + | Change (t1, t2, where) -> + let where = + (match where with + None -> [] + | Some ident -> + [Box.Text([],"in"); + Box.smallskip; + Box.Text([],ident)]) in + Box.V([], + (pretty_append + [Box.Text([],"change")] + t1 + [])@ + (pretty_append + [Box.Text([],"with")] + t2 + [])@where) + | Change_pattern (_, _, _) -> assert false (* TODO *) + | Contradiction -> Box.Text([],"contradiction") + | Cut term -> + Box.V([],[Box.Text([],"cut"); + Box.indent(ast2box term)]) + | Decompose (ident, principles) -> + let principles = + List.map (fun x -> Box.Text([],x)) principles in + Box.V([],[Box.Text([],"decompose"); + Box.H([],[Box.Text([],"["); + Box.V([],principles); + Box.Text([],"]")]); + Box.Text([],ident)]) + | Discriminate ident -> + Box.V([],[Box.Text([],"discriminate"); + Box.Text([],ident)]) + | Elim (term, using) -> + let using = + (match using with + None -> [] + | Some term -> + (pretty_append + [Box.Text([],"using")] + term + [])) in + Box.V([], + (pretty_append + [Box.Text([],"elim")] + term + [])@using) + | ElimType term -> + Box.V([],[Box.Text([],"elim type"); + Box.indent(ast2box term)]) + | Exact term -> + Box.V([],[Box.Text([],"exact"); + Box.indent(ast2box term)]) + | Exists -> Box.Text([],"exists") + | Fold (kind, term) -> + Box.V([],[Box.H([],[Box.Text([],"fold"); + Box.smallskip; + Box.Text([],string_of_kind kind)]); + Box.indent(ast2box term)]) + | Fourier -> Box.Text([],"fourier") + | Injection ident -> + Box.V([],[Box.Text([],"transitivity"); + Box.indent (Box.Text([],ident))]) + | Intros (num, idents) -> + let num = + (match num with + None -> [] + | Some num -> [Box.Text([],string_of_int num)]) in + let idents = + List.map (fun x -> Box.Text([],x)) idents in + Box.V([],[Box.Text([],"decompose"); + Box.H([],[Box.smallskip; + Box.V([],idents)])]) + | Left -> Box.Text([],"left") + | LetIn (term, ident) -> + Box.V([],[Box.H([],[Box.Text([],"let"); + Box.smallskip; + Box.Text([],ident); + Box.smallskip; + Box.Text([],"=")]); + Box.indent (ast2box term)]) + | Reduce (_, _, _) -> assert false (* TODO *) + | Reflexivity -> Box.Text([],"reflexivity") + | Replace (t1, t2) -> + Box.V([], + (pretty_append + [Box.Text([],"replace")] + t1 + [])@ + (pretty_append + [Box.Text([],"with")] + t2 + [])) + | Replace_pattern (_, _) -> assert false (* TODO *) + | Rewrite (_, _, _) -> assert false (* TODO *) + | Right -> Box.Text([],"right") + | Ring -> Box.Text([],"ring") + | Split -> Box.Text([],"split") + | Symmetry -> Box.Text([],"symmetry") + | Transitivity term -> + Box.V([],[Box.Text([],"transitivity"); + Box.indent (ast2box term)]) +;; + +open TacticAst + +let rec tactical2box ?(attr = []) = function + LocatedTactical (loc, tac) -> tactical2box tac + | Fail -> Box.Text([],"fail") + | Do (count, tac) -> + Box.V([],[Box.Text([],"do " ^ string_of_int count); + Box.indent (tactical2box tac)]) + | IdTac -> Box.Text([],"id") + | Repeat tac -> + Box.V([],[Box.Text([],"repeat"); + 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; + Box.Text([],"["); + Box.V([],tacticals2box tacs); + Box.Text([],"]");])]) + | Tries tacs -> + Box.V([],[Box.Text([],"try"); + Box.H([],[Box.skip; + Box.Text([],"["); + Box.V([],tacticals2box tacs); + Box.Text([],"]");])]) + | Try tac -> + Box.V([],[Box.Text([],"try"); + Box.indent (tactical2box tac)]) + +and tacticals2box tacs = + List.map + (function tac -> Box.H([],[tactical2box tac; Box.Text([],";")])) tacs +;; + +let tacticalPp tac = + String.concat "\n" + (BoxPp.to_string CicAstPp.pp_term (tactical2box tac));; + + diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.mli b/helm/ocaml/cic_transformations/tacticAst2Box.mli new file mode 100644 index 000000000..36eeb3e73 --- /dev/null +++ b/helm/ocaml/cic_transformations/tacticAst2Box.mli @@ -0,0 +1,42 @@ +(* 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/ + *) + +(**************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 18/2/2004 *) +(* *) +(**************************************************************************) + + +val tactical2box: + ?attr:'a list + -> (CicAst.term, string) TacticAst.tactic TacticAst.tactical + -> CicAst.term Box.box + +val tacticalPp: + (CicAst.term, string) TacticAst.tactic TacticAst.tactical -> string -- 2.39.2