+++ /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 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,None) -> current_size + (String.length s)
- | A.Ident(s,Some 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 (`Forall, (Cic.Anonymous, typ), body)
- | A.Binder (`Pi, (Cic.Anonymous, typ), body) ->
- Box.V(map_attributes attr,
- [Box.H([],[(match typ with
- | None -> Box.Text([], "?")
- | Some typ -> ast2box typ);
- Box.smallskip;
- Box.Text([], "\\to")]);
- Box.indent(ast2box body)])
- | 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([],"\Rightarrow")]);
- Box.indent (bigast2box rhs)])
- else
- Box.H([],[Box.Text([],sep);
- Box.smallskip;
- make_pattern constr vars;
- Box.smallskip;
- Box.Text([],"\Rightarrow");
- 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
- let ty_box =
- match ty with
- | Some ty ->
- [ Box.H([],[Box.Text([],"[");
- ast2box ty;
- Box.Text([],"]")]) ]
- | None -> []
- in
- if is_big arg then
- Box.V(map_attributes attr,
- ty_box @
- [Box.Text([],"match");
- Box.H([],[Box.skip;
- bigast2box arg;
- Box.smallskip;
- Box.Text([],"with")]);
- plbox])
- else
- Box.V(map_attributes attr,
- ty_box @
- [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
- match subst with
- | Some subst -> make_substs "\\subst [" subst
- | None -> []
- 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([],"\Assign")
- ]
- body
- [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)]
- else
- [Box.H([],l@(Box.smallskip::(ast2box ast)::tail))]
-
-;;
-
-
-
-
-
projects / helm.git / blobdiff