From 3b4c8315cd31b9ce3677335ccd7092aa4b87bc24 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 1 Jul 2005 14:18:51 +0000 Subject: [PATCH] Module TacticAst2Box unused! --- helm/ocaml/cic_transformations/.depend | 5 - helm/ocaml/cic_transformations/Makefile | 2 +- .../cic_transformations/tacticAst2Box.ml | 284 ------------------ .../cic_transformations/tacticAst2Box.mli | 41 --- 4 files changed, 1 insertion(+), 331 deletions(-) delete mode 100644 helm/ocaml/cic_transformations/tacticAst2Box.ml delete mode 100644 helm/ocaml/cic_transformations/tacticAst2Box.mli diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index f4c554908..2aff8f942 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -8,7 +8,6 @@ content2pres.cmi: mpresentation.cmi box.cmi sequent2pres.cmi: mpresentation.cmi box.cmi tacticAstPp.cmi: tacticAst.cmo cicAst.cmi boxPp.cmi: cicAst.cmi box.cmi -tacticAst2Box.cmi: tacticAst.cmo cicAst.cmi box.cmi tacticAst.cmo: cicAst.cmi tacticAst.cmx: cicAst.cmx cicAst.cmo: cicAst.cmi @@ -49,7 +48,3 @@ tacticAstPp.cmo: tacticAst.cmo cicAstPp.cmi tacticAstPp.cmi tacticAstPp.cmx: tacticAst.cmx cicAstPp.cmx tacticAstPp.cmi boxPp.cmo: cicAstPp.cmi box.cmi ast2pres.cmi boxPp.cmi boxPp.cmx: cicAstPp.cmx box.cmx ast2pres.cmx boxPp.cmi -tacticAst2Box.cmo: tacticAstPp.cmi tacticAst.cmo cicAstPp.cmi boxPp.cmi \ - box.cmi ast2pres.cmi tacticAst2Box.cmi -tacticAst2Box.cmx: tacticAstPp.cmx tacticAst.cmx cicAstPp.cmx boxPp.cmx \ - box.cmx ast2pres.cmx tacticAst2Box.cmi diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index 4675291d4..cde994c7b 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -16,7 +16,7 @@ INTERFACE_FILES = \ sequent2pres.mli \ domMisc.mli xml2Gdome.mli sequentPp.mli \ applyTransformation.mli \ - tacticAstPp.mli boxPp.mli tacticAst2Box.mli + tacticAstPp.mli boxPp.mli IMPLEMENTATION_FILES = \ tacticAst.ml \ $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml deleted file mode 100644 index 151ebfd7b..000000000 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ /dev/null @@ -1,284 +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/ - *) - -(**************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 18/2/2004 *) -(* *) -(**************************************************************************) - - -open Ast2pres -open TacticAst - -let count_pattern current_size (wanted,hyps_pat,concl_pat) = - if current_size > maxsize then current_size - else - let size = countterm (current_size + 3) concl_pat in - let size = - List.fold_left - (fun s (id,t) -> countterm (s + String.length id + 1) t) size hyps_pat in - match wanted with - None -> size + 3 - | Some t -> countterm (size + 9) t - -let count_kind = - function - `Reduce -> 6 - | `Simpl -> 8 - | `Whd -> 3 - | `Normalize -> 9 - -let rec count_tactic current_size tac = - if current_size > maxsize then current_size - else match tac with - | Absurd (_, term) -> countterm (current_size + 6) term - | Apply (_, term) -> countterm (current_size + 6) term - | Auto _ -> current_size + 4 - | Assumption _ -> current_size + 10 - | Change (_,p,term) -> - count_pattern (countterm (current_size + 13) term) p - | Clear (_,id) -> current_size + 6 + String.length id - | ClearBody (_,id) -> current_size + 10 + String.length id - | Compare (_, term) -> countterm (current_size + 7) term - | Constructor (_, n) -> current_size + 12 - | Contradiction _ -> current_size + 13 - | Cut (_, ident, term) -> - let id_size = - match ident with - None -> 0 - | Some id -> String.length id + 4 - in - countterm (current_size + 4 + id_size) term - | DecideEquality _ -> current_size + 15 - | Decompose (_, term) -> - countterm (current_size + 11) term - | Discriminate (_, term) -> countterm (current_size + 12) term - | 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 - | Fail _ -> current_size + 4 - | Fold (_,kind,term,p) -> - count_pattern (countterm (current_size + count_kind kind + 6) term) p - | Fourier _ -> current_size + 7 - | FwdSimpl (_,id,idl) -> - List.fold_left (fun s id -> s + String.length id) - (current_size + 4 + String.length id) idl - | Generalize (_,p,id) -> - let id_size = - match id with - None -> 0 - | Some id -> 4 + String.length id - in - count_pattern (current_size + 11 + id_size) p - | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n))) - | IdTac _ -> current_size + 2 - | Injection (_, term) -> - countterm (current_size + 10) term - | Intros (_, num, idents) -> - List.fold_left - (fun size s -> size + (String.length s)) - (current_size + 7) idents - | LApply (_,depth,terml,term,idopt) -> - let idopt_size = - match idopt with - None -> 0 - | Some id -> 6 + String.length id in - let terml_size = - if terml = [] then 0 - else - List.fold_left (fun s t -> countterm (s + 1) t) 3 terml in - let depth_size = - match depth with - None -> 0 - | Some n -> 8 + n / 10 - in - countterm (current_size + 7 + idopt_size + terml_size + depth_size) term - | Left _ -> current_size + 4 - | LetIn (_, term, ident) -> - countterm (current_size + 5 + String.length ident) term - | Reduce (_,kind,p) -> - count_pattern (current_size + count_kind kind + 1) p - | Reflexivity _ -> current_size + 11 - | Replace (_,p,term) -> - count_pattern (countterm (current_size + 11) term) p - | Rewrite (_,dir,term,p) -> - count_pattern (countterm (current_size + 10) term) p - | 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 tac = - Box.Text([], TacticAstPp.pp_tactic tac) - -let string_of_kind = function - | `Reduce -> "reduce" - | `Simpl -> "simplify" - | `Whd -> "whd" - | `Normalize -> "normalize" - -let dummy_tbl = Hashtbl.create 0 - -let ast2astBox ast = Ast2pres.ast2astBox (ast, dummy_tbl) - -let pretty_append l ast = - if is_big ast then - [Box.H([],l); - Box.H([],[Box.skip; ast2astBox ast])] - else - [Box.H([],l@[Box.smallskip; ast2astBox ast])] - -let rec tactic2box tac = - if (is_big_tac tac) then - big_tactic2box tac - else - small_tactic2box tac - -and big_tactic2box = function - | Absurd (_, term) -> - Box.V([],[Box.Text([],"absurd"); - ast2astBox term]) - | Apply (_, term) -> - Box.V([],[Box.Text([],"apply"); - ast2astBox term]) - | Assumption _ -> Box.Text([],"assumption") - | Auto _ -> Box.Text([],"auto") - | Compare (_, term) -> - Box.V([],[Box.Text([],"compare"); - Box.indent(ast2astBox term)]) - | Constructor (_,n) -> Box.Text ([],"constructor " ^ string_of_int n) - | Contradiction _ -> Box.Text([],"contradiction") - | DecideEquality _ -> Box.Text([],"decide equality") - | Decompose (_, term) -> - Box.V([],[Box.Text([],"decompose"); - Box.indent(ast2astBox term)]) - | Discriminate (_, term) -> - Box.V([],pretty_append [Box.Text([],"discriminate")] term) - | 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(ast2astBox term)]) - | Exact (_, term) -> - Box.V([],[Box.Text([],"exact"); - Box.indent(ast2astBox term)]) - | Exists _ -> Box.Text([],"exists") - | Fourier _ -> Box.Text([],"fourier") - | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n) - | 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 (ast2astBox term)]) - | Reflexivity _ -> Box.Text([],"reflexivity") - | 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 (ast2astBox term)]) -;; - -open TacticAst - -let rec tactical2box = function - | Tactic (_, tac) -> tactic2box tac - | Do (_, count, tac) -> - Box.V([],[Box.Text([],"do " ^ string_of_int count); - Box.indent (tactical2box tac)]) - | Repeat (_, tac) -> - Box.V([],[Box.Text([],"repeat"); - Box.indent (tactical2box tac)]) - | Seq (_, tacs) -> - Box.V([],tacticals2box tacs) - | 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 deleted file mode 100644 index f9daa4270..000000000 --- a/helm/ocaml/cic_transformations/tacticAst2Box.mli +++ /dev/null @@ -1,41 +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/ - *) - -(**************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 18/2/2004 *) -(* *) -(**************************************************************************) - - -val tactical2box: - (CicAst.term, string) TacticAst.tactical -> - CicAst.term Box.box - -val tacticalPp: (CicAst.term, string) TacticAst.tactical -> string - -- 2.39.2