X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;fp=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=4b79607f52b0384951baba7fe9921c00c8ed0967;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml deleted file mode 100644 index 4b79607f5..000000000 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ /dev/null @@ -1,271 +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 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 - - | 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); - 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) - | 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));; - -