From ac0a12080b434bf0daafc08e9da240eb57f47280 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 13 Feb 2004 12:57:01 +0000 Subject: [PATCH 1/1] new (box based) pretty printer --- helm/ocaml/cic_transformations/.depend | 8 + helm/ocaml/cic_transformations/Makefile | 5 +- helm/ocaml/cic_transformations/ast2pres.ml | 302 ++++++++++++++++++++ helm/ocaml/cic_transformations/ast2pres.mli | 45 +++ helm/ocaml/cic_transformations/box.ml | 50 ++++ helm/ocaml/cic_transformations/box.mli | 51 ++++ helm/ocaml/cic_transformations/boxPp.ml | 21 ++ helm/ocaml/cic_transformations/boxPp.mli | 4 + 8 files changed, 484 insertions(+), 2 deletions(-) create mode 100644 helm/ocaml/cic_transformations/ast2pres.ml create mode 100644 helm/ocaml/cic_transformations/ast2pres.mli create mode 100644 helm/ocaml/cic_transformations/box.ml create mode 100644 helm/ocaml/cic_transformations/box.mli create mode 100644 helm/ocaml/cic_transformations/boxPp.ml create mode 100644 helm/ocaml/cic_transformations/boxPp.mli diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index c1a5eeb97..9a356a17b 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -1,10 +1,14 @@ contentTable.cmi: cicAst.cmo cexpr2pres.cmi: content_expressions.cmi mpresentation.cmi content2pres.cmi: mpresentation.cmi +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 +boxPp.cmi: box.cmi cicAst.cmo +box.cmo: box.cmi +box.cmx: box.cmi contentTable.cmo: cicAst.cmo contentTable.cmi contentTable.cmx: cicAst.cmx contentTable.cmi cic2Xml.cmo: cic2Xml.cmi @@ -19,6 +23,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 sequent2pres.cmo: cexpr2pres.cmi content_expressions.cmi mpresentation.cmi \ sequent2pres.cmi sequent2pres.cmx: cexpr2pres.cmx content_expressions.cmx mpresentation.cmx \ @@ -45,3 +51,5 @@ acic2Ast.cmo: cicAst.cmo acic2Ast.cmi acic2Ast.cmx: cicAst.cmx acic2Ast.cmi cicAstPp.cmo: cicAst.cmo cicAstPp.cmi cicAstPp.cmx: cicAst.cmx cicAstPp.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 05730df75..c16e7271e 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -6,13 +6,14 @@ PREDICATES = # modules which have both a .ml and a .mli INTERFACE_FILES = \ - contentTable.mli \ + box.mli contentTable.mli \ cic2Xml.mli content_expressions.mli \ mpresentation.mli cexpr2pres.mli content2pres.mli \ + ast2pres.mli \ sequent2pres.mli \ cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli sequentPp.mli \ applyStylesheets.mli applyTransformation.mli \ - acic2Ast.mli cicAstPp.mli + acic2Ast.mli cicAstPp.mli boxPp.mli IMPLEMENTATION_FILES = \ cicAst.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 new file mode 100644 index 000000000..934223e5c --- /dev/null +++ b/helm/ocaml/cic_transformations/ast2pres.ml @@ -0,0 +1,302 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + +(**************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 28/6/2003 *) +(* *) +(**************************************************************************) + +module P = Mpresentation;; +module A = CicAst;; + +let symbol_table = Hashtbl.create 503;; +let symbol_table_charcount = Hashtbl.create 503;; + +let maxsize = 25;; + +let rec countvar current_size = function + (Cic.Anonymous, None) -> current_size + 1 (* underscore *) + | (Cic.Anonymous, Some ty) -> countterm current_size ty + | (Cic.Name s, None) -> current_size + String.length s + | (Cic.Name s, Some ty) -> current_size + countterm current_size ty + +and countterm current_size t = + if current_size > maxsize then current_size + else match t with + A.AttributedTerm (_,t) -> countterm current_size t + | A.Appl l -> + List.fold_left countterm current_size l + | A.Binder (_,var,body) -> + let varsize = countvar current_size var in + countterm (varsize + 1) body (* binder *) + | A.Case (arg, _, ty, pl) -> + let size1 = countterm (current_size+10) arg in (* match with *) + let size2 = + match ty with + None -> size1 + | Some ty -> countterm size1 ty in + List.fold_left + (fun c ((constr,vars),action) -> + let size3 = + List.fold_left countvar (c+String.length constr) vars in + countterm size3 action) size2 pl + | A.LetIn (var,s,t) -> + let size1 = countvar current_size var in + let size2 = countterm size1 s in + countterm size2 t + | A.LetRec (_,l,t) -> + let size1 = + List.fold_left + (fun c (var,s,_) -> + let size1 = countvar c var in + countterm size1 s) current_size l in + countterm size1 t + | A.Ident(s,l) -> + List.fold_left + (fun c (v,t) -> countterm (c + (String.length v)) t) + (current_size + (String.length s)) l + | A.Implicit -> current_size + 1 (* underscore *) + | A.Meta (_,l) -> + List.fold_left + (fun c t -> + match t with + None -> c + 1 (* underscore *) + | Some t -> countterm c t) + (current_size + 1) l (* num *) + | A.Num (s, _) -> current_size + String.length s + | A.Sort _ -> current_size + 4 (* sort name *) + | A.Symbol (s,_) -> current_size + String.length s +;; + +let is_big t = + ((countterm 0 t) > maxsize) +;; + +let map_attribute = + function + `Loc (n,m) -> + (Some "helm","loc",(string_of_int n)^" "^(string_of_int m)) + | `IdRef s -> + (Some "helm","xref",s) +;; + +let map_attributes = List.map map_attribute +;; +let resolve_binder = function + `Lambda -> Box.Text([],"\\lambda") + | `Pi -> Box.Text([],"\\Pi") + | `Exists -> Box.Text([],"\\exists") + | `Forall -> Box.Text([],"\\forall") + +let rec ast2box ?(priority = 0) ?(assoc = false) ?(attr = []) t = + if is_big t then + bigast2box ~priority ~assoc ~attr t + else Box.Object (map_attributes attr, t) +and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) = + function + A.AttributedTerm (attr1, t) -> + (* attr should be empty, since AtrtributedTerm are not + supposed to be directly nested *) + bigast2box ~priority ~assoc ~attr:(attr1::~attr) t + | A.Appl l -> + Box.H + (map_attributes attr, + [Box.Text([],"("); + Box.V([],List.map ast2box l); + Box.Text([],")")]) + | A.Binder(kind, var, body) -> + Box.V(map_attributes attr, + [Box.H([],[resolve_binder kind; + Box.smallskip; + make_var var; + Box.Text([],".")]); + Box.indent (ast2box body)]) + | A.Case(arg, _, ty, pl) -> + let make_rule sep ((constr,vars),rhs) = + if (is_big rhs) then + Box.V([],[Box.H([],[Box.Text([],sep); + Box.smallskip; + make_pattern constr vars; + Box.smallskip; + Box.Text([],"->")]); + Box.indent (bigast2box rhs)]) + else + Box.H([],[Box.Text([],sep); + Box.smallskip; + make_pattern constr vars; + Box.smallskip; + Box.Text([],"->"); + Box.smallskip; + Box.Object([],rhs)]) in + let plbox = match pl with + [] -> Box.Text([],"[]") + | r::tl -> + Box.H([], + [Box.V([], + (make_rule "[" r)::(List.map (make_rule "|") tl)); + Box.Text([],"]")]) in + if is_big arg then + Box.V(map_attributes attr, + [Box.Text([],"match"); + Box.H([],[Box.skip; + bigast2box arg; + Box.smallskip; + Box.Text([],"with")]); + plbox]) + else + Box.V(map_attributes attr, + [Box.H(map_attributes attr, + [Box.Text([],"match"); + Box.smallskip; + ast2box arg; + Box.smallskip; + Box.Text([],"with")]); + plbox]) + | A.LetIn (var, s, t) -> + Box.V(map_attributes attr, + (make_def "let" var s "in")@[ast2box t]) + | A.LetRec (_, vars, body) -> + let definitions = + let rec make_defs let_txt = function + [] -> [] + | [(var,s,_)] -> + make_def let_txt var s "in" + | (var,s,_)::tl -> + (make_def let_txt var s "")@(make_defs "and" tl) in + make_defs "let rec" vars in + Box.V(map_attributes attr, + definitions@[ast2box body]) + | A.Ident (s, subst) -> + let subst = + let rec make_substs start_txt = + function + [] -> [] + | [(s,t)] -> + make_subst start_txt s t "]" + | (s,t)::tl -> + (make_subst start_txt s t ";")@(make_substs " " tl) in + make_substs "[" subst in + Box.V([], (* attr here or on Vbox? *) + [Box.Text(map_attributes attr,s); + Box.indent(Box.V([],subst))]) + | A.Implicit -> + Box.Text([],"_") (* big? *) + | A.Meta (n, l) -> + let local_context = + List.map + (function t -> + Box.H([],[aux_option t; Box.Text([],";")])) + l in + Box.V(map_attributes attr, + [Box.Text([],"?"^(string_of_int n)); + Box.H([],[Box.Text([],"["); + Box.V([],local_context); + Box.Text([],"]")])]) + | A.Num (s, _) -> + Box.Text([],s) + | A.Sort kind -> + (match kind with + `Prop -> Box.Text([],"Prop") + | `Set -> Box.Text([],"Set") + | `Type -> Box.Text([],"Type") + | `CProp -> Box.Text([],"CProp")) + | A.Symbol (s, _) -> + Box.Text([],s) + +and aux_option = function + None -> Box.Text([],"_") + | Some ast -> ast2box ast + +and make_var = function + (Cic.Anonymous, None) -> Box.Text([],"_:_") + | (Cic.Anonymous, Some t) -> + Box.H([],[Box.Text([],"_:");ast2box t]) + | (Cic.Name s, None) -> Box.Text([],s) + | (Cic.Name s, Some t) -> + if is_big t then + Box.V([],[Box.Text([],s^":"); + Box.indent(bigast2box t)]) + else + Box.H([],[Box.Text([],s^":");Box.Object([],t)]) + +and make_pattern constr = + function + [] -> Box.Text([],constr) + | vars -> + let bvars = + List.fold_right + (fun var acc -> + let bv = + match var with + (* ignoring the type *) + (Cic.Anonymous, _) -> Box.Text([],"_") + | (Cic.Name s, _) -> Box.Text([],s) in + Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in + Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars) + + +and make_def let_txt var def end_txt = + let name = + (match var with + (* ignoring the type *) + (Cic.Anonymous, _) -> Box.Text([],"_") + | (Cic.Name s, _) -> Box.Text([],s)) in + pretty_append + [Box.Text([],let_txt); + Box.smallskip; + name; + Box.smallskip; + Box.Text([],"=") + ] + def + [Box.smallskip;Box.Text([],end_txt)] + +and make_subst start_txt varname body end_txt = + pretty_append + [Box.Text([],start_txt); + Box.Text([],varname); + Box.smallskip; + Box.Text([],":=") + ] + body + [Box.Text([],end_txt)] + +and pretty_append l ast tail = + if is_big ast then + [Box.H([],l); + Box.H([],Box.skip::(bigast2box ast)::tail)] + else + [Box.H([],l@(Box.smallskip::(ast2box ast)::tail))] + +;; + + + + + diff --git a/helm/ocaml/cic_transformations/ast2pres.mli b/helm/ocaml/cic_transformations/ast2pres.mli new file mode 100644 index 000000000..dc370c2b9 --- /dev/null +++ b/helm/ocaml/cic_transformations/ast2pres.mli @@ -0,0 +1,45 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + +(**************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 28/6/2003 *) +(* *) +(**************************************************************************) + +val ast2box: + ?priority:int -> + ?assoc:bool -> + ?attr:CicAst.term_attribute list -> + CicAst.term -> CicAst.term Box.box + + + + + + diff --git a/helm/ocaml/cic_transformations/box.ml b/helm/ocaml/cic_transformations/box.ml new file mode 100644 index 000000000..41b7fb725 --- /dev/null +++ b/helm/ocaml/cic_transformations/box.ml @@ -0,0 +1,50 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + +(*************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 13/2/2004 *) +(* *) +(*************************************************************************) + +type + 'expr box = + Text of attr * string + | Space of attr + | H of attr * ('expr box) list + | V of attr * ('expr box) list + | Object of attr * 'expr + | Action of attr * ('expr box) list + +and attr = (string option * string * string) list + +let smallskip = Text([]," ");; +let skip = Text([]," ");; + +let indent t = H([],[skip;t]);; + diff --git a/helm/ocaml/cic_transformations/box.mli b/helm/ocaml/cic_transformations/box.mli new file mode 100644 index 000000000..2c98b2969 --- /dev/null +++ b/helm/ocaml/cic_transformations/box.mli @@ -0,0 +1,51 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + +(*************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 13/2/2004 *) +(* *) +(*************************************************************************) + +type + 'expr box = + Text of attr * string + | Space of attr + | H of attr * ('expr box) list + | V of attr * ('expr box) list + | Object of attr * 'expr + | Action of attr * ('expr box) list + +and attr = (string option * string * string) list + +val smallskip : 'expr box +val skip: 'expr box +val indent : 'expr box -> 'expr box + + + diff --git a/helm/ocaml/cic_transformations/boxPp.ml b/helm/ocaml/cic_transformations/boxPp.ml new file mode 100644 index 000000000..922d5c6a6 --- /dev/null +++ b/helm/ocaml/cic_transformations/boxPp.ml @@ -0,0 +1,21 @@ + +let to_string object_to_string b = + let layout = ref [] in + let rec aux_h current_s = + function + [] -> layout := current_s::!layout + | Box.Text (_,s)::tl -> aux_h (current_s ^ s) tl + | (Box.Space _)::_ -> assert false + | Box.H (_,bl)::tl -> aux_h current_s (bl@tl) + | Box.V (_,[])::tl -> aux_h current_s tl + | Box.V (_,[b])::tl -> aux_h current_s (b::tl) + | Box.V (_,b::bl')::tl -> + aux_h current_s [b] ; + aux_h (String.make (String.length current_s) ' ') (Box.V([],bl')::tl) + | Box.Object (_,obj)::tl -> aux_h (current_s ^ (object_to_string obj)) tl + | (Box.Action _)::tl -> assert false + in + aux_h "" [b] ; + List.rev !layout + +let pp_term t = String.concat "\n" (to_string CicAstPp.pp_term (Ast2pres.ast2box t)) diff --git a/helm/ocaml/cic_transformations/boxPp.mli b/helm/ocaml/cic_transformations/boxPp.mli new file mode 100644 index 000000000..4bbd64524 --- /dev/null +++ b/helm/ocaml/cic_transformations/boxPp.mli @@ -0,0 +1,4 @@ + +val to_string : ('expr -> string) -> 'expr Box.box -> string list + +val pp_term : CicAst.term -> string -- 2.39.2