--- /dev/null
+(* 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 <asperti@cs.unibo.it> *)
+(* 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))]
+
+;;
+
+
+
+
+
projects / helm.git / commitdiff