+++ /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 CE = Content_expressions;;
-
-let symbol_table = Hashtbl.create 503;;
-let symbol_table_charcount = Hashtbl.create 503;;
-
-let maxsize = 25;;
-
-let rec countterm current_size t =
- if current_size > maxsize then current_size
- else match t with
- CE.Symbol (_,name,None,_) -> current_size + (String.length name)
- | CE.Symbol (_,name,Some subst,_) ->
- let c1 = current_size + (String.length name) in
- countsubst subst c1
- | CE.LocalVar (_,name) -> current_size + (String.length name)
- | CE.Meta (_,name,l) ->
- List.fold_left
- (fun i t ->
- match t with
- None -> i
- | Some t' -> countterm i t'
- ) (current_size + String.length name) l
- | CE.Num (_,value) -> current_size + (String.length value)
- | CE.Appl (_,l) ->
- List.fold_left countterm current_size l
- | CE.Binder (_, _,(n,s),body) ->
- let cs = countterm (current_size + 2 + (String.length n)) s in
- countterm cs body
- | CE.Letin (_,(n,s),body) ->
- let cs = countterm (current_size + 3 + (String.length n)) s in
- countterm cs body
- | CE.Letrec (_,defs,body) ->
- let cs =
- List.fold_left
- (fun c (n,bo) -> countterm (c+(String.length n)) bo) current_size defs in
- countterm cs body
- | CE.Case (_,a,np) ->
- let cs = countterm (current_size + 4) a in
- List.fold_left
- (fun c (n,bo) -> countterm (c+(String.length n)) bo) current_size np
-
-and
-countsubst subst current_size =
- List.fold_left
- (fun current_size (uri,expr) ->
- if (current_size > maxsize) then current_size
- else
- let c1 =
- (current_size + (String.length (UriManager.name_of_uri uri))) in
- (countterm c1 expr)) current_size subst
-;;
-
-let is_big t =
- ((countterm 0 t) > maxsize)
-;;
-
-let rec make_attributes l1 =
- function
- [] -> []
- | None::tl -> make_attributes (List.tl l1) tl
- | (Some s)::tl ->
- let p,n = List.hd l1 in
- (p,n,s)::(make_attributes (List.tl l1) tl)
-;;
-
-let make_math_tail = List.map (fun s -> P.Mtext ([], s))
-
-let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
- let module CE = Content_expressions in
- let module P = Mpresentation in
- let rec aux =
- function
- CE.Symbol (xref,name,None,uri) ->
- let attr =
- make_attributes
- [Some "helm","xref";Some "xlink","href"] [xref;uri] in
- if tail = [] then
- P.Mi (attr,name)
- else P.Mrow([],P.Mi (attr,name)::(make_math_tail tail))
- | CE.Symbol (xref,name,Some subst,uri) ->
- let attr =
- make_attributes
- [Some "helm","xref";Some "xlink","href"] [xref;uri] in
- let rec make_subst =
- (function
- [] -> assert false
- | [(uri,a)] ->
- [(aux a);
- P.Mtext([],"/");
- P.Mi([],UriManager.name_of_uri uri)]
- | (uri,a)::tl ->
- (aux a)::
- P.Mtext([],"/")::
- P.Mi([],UriManager.name_of_uri uri)::
- P.Mtext([],"; ")::
- P.smallskip::
- (make_subst tl)) in
- P.Mrow ([],
- P.Mi (attr,name)::
- P.Mtext([],"[")::
- (make_subst subst)@
- (P.Mtext([],"]")::(make_math_tail tail)))
- | CE.LocalVar (xref,name) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- if tail = [] then
- P.Mi (attr,name)
- else P.Mrow([],P.Mi (attr,name)::(make_math_tail tail))
- | CE.Meta (xref,name,l) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let l' =
- List.map
- (function
- None -> P.Mo([],"_")
- | Some t -> cexpr2pres t
- ) l
- in
- if tail = [] then
- P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
- else
- P.Mrow
- ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ (make_math_tail tail))
- | CE.Num (xref,value) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- if tail = [] then
- P.Mn (attr,value)
- else P.Mrow([],P.Mn (attr,value)::(make_math_tail tail))
- | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
- let aattr = make_attributes [Some "helm","xref"] [axref] in
- let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
- (try
- (let f = Hashtbl.find symbol_table n in
- f tl ~priority ~assoc ~tail aattr sattr)
- with notfound ->
- P.Mrow(aattr,
- P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::(make_math_tail tail))))
- | CE.Appl (xref,l) as t ->
- let attr = make_attributes [Some"helm","xref"] [xref] in
- P.Mrow(attr,
- P.Mo([],"(")::(make_args l)@(P.Mo([],")")::(make_math_tail tail)))
- | CE.Binder (xref, kind,(n,s),body) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let binder =
- if kind = "Lambda" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
- else if kind = "Prod" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
- else if kind = "Forall" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x2200
- else if kind = "Exists" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x2203
- else "unknown" in
- P.Mrow (attr,
- P.Mtext([None,"mathcolor","blue"],binder)::
- P.Mtext([],n ^ ":")::
- (aux s)::
- P.Mo([],".")::
- (aux body)::(make_math_tail tail))
- | CE.Letin (xref,(n,s),body) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- P.Mrow (attr,
- P.Mtext([],("let "))::
- P.Mtext([],(n ^ "="))::
- (aux s)::
- P.Mtext([]," in ")::
- (aux body)::(make_math_tail tail))
- | CE.Letrec (xref,defs,body) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let rec make_defs =
- (function
- [] -> assert false
- | [(n,bo)] ->
- [P.Mtext([],(n ^ "="));(aux body)]
- | (n,bo)::tl ->
- P.Mtext([],(n ^ "="))::
- (aux body)::P.Mtext([]," and")::(make_defs tl)) in
- P.Mrow (attr,
- P.Mtext([],("let rec "))::
- (make_defs defs)@
- (P.Mtext([]," in ")::
- (aux body)::(make_math_tail tail)))
- | CE.Case (xref,a,np) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let rec make_patterns =
- (function
- [] -> []
- | [(n,p)] -> make_pattern n p
- | (n,p)::tl ->
- (make_pattern n p)@(P.smallskip::
- P.Mtext([],"|")::P.smallskip::(make_patterns tl)))
- and make_pattern n p =
- let rec get_vars_and_body =
- (function
- CE.Binder (_, "Lambda",(n,_),body) ->
- let v,b = get_vars_and_body body in
- n::v,b
- | t -> [],t) in
- let vars,body = get_vars_and_body p in
- let lhs =
- match vars with
- [] -> n ^ " -> "
- | l -> "(" ^ n ^" "^(String.concat " " l) ^ ")" ^ " -> " in
- [P.Mtext([],lhs);P.smallskip;aux body] in
- P.Mrow (attr,
- P.Mtext([],"match")::P.smallskip::
- (aux a)::P.smallskip::
- P.Mtext([],"with")::P.smallskip::
- P.Mtext([],"[")::P.smallskip::
- (make_patterns np)@(P.smallskip::P.Mtext([],("]"))::(make_math_tail tail))) in
- aux t
-
-and
-
-make_args ?(priority = 0) ?(assoc = false) ?(tail = []) =
- function
- [] -> List.map (fun s -> P.Mtext ([], s)) tail
- | a::tl -> P.smallskip::(cexpr2pres a)::(make_args ~tail:tail tl)
-;;
-
-let make_box_tail = List.map (Box.b_text [])
-;;
-
-let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) =
- function
- [] -> []
- | [a] -> [Box.indent (cexpr2pres_charcount ~tail:tail a)]
- | (a::tl) as l ->
- let c = List.fold_left countterm 0 l in
- if c > maxsize then
- (Box.indent (cexpr2pres_charcount a))::
- (make_args_charcount ~tail:tail tl)
- else
- [Box.indent (Box.b_object (P.Mrow ([], (make_args ~tail:tail l))))]
-
-(*
- function
- [] -> []
- | a::tl ->
- let tlpres =
- let c = List.fold_left countterm 0 tl in
- if c > maxsize then
- P.Mtable ([("align","baseline 1");("equalrows","false");
- ("columnalign","left")],
- (make_args_charcount tl))
- else
- P.Mrow([], make_args tl) in
- [P.Mtr([],[P.Mtd([],(cexpr2pres_charcount a))]);
- P.Mtr([],[P.Mtd([],P.indented tlpres)])] *)
-and
-
-cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
- if not (is_big t) then
- Box.b_object (cexpr2pres ~priority ~assoc ~tail t)
- else let aux = cexpr2pres_charcount in
- match t with
- CE.Symbol (xref,name,None,uri) ->
- let attr =
- make_attributes
- [Some "helm","xref";Some "xlink","href"] [xref;uri] in
- if tail = [] then
- Box.b_object (P.Mi (attr,name))
- else
- Box.b_h [] (Box.b_object (P.Mi (attr,name)) :: (make_box_tail tail))
- | CE.Symbol (xref,name,Some subst,uri) ->
- let attr =
- make_attributes
- [Some "helm","xref";Some "xlink","href"] [xref;uri] in
- let rec make_subst =
- (function
- [] -> assert false
- | [(uri,a)] ->
- [Box.b_object (cexpr2pres a);
- Box.b_text [] "/";
- Box.b_object (P.Mi([],UriManager.name_of_uri uri))]
- | (uri,a)::tl ->
- Box.b_object (cexpr2pres a) ::
- Box.b_text [] "/" ::
- Box.b_object (P.Mi([],UriManager.name_of_uri uri)) ::
- Box.b_text [] "; " ::
- Box.smallskip ::
- (make_subst tl)) in
- Box.b_h [] (
- Box.b_object (P.Mi (attr,name))::
- Box.b_text [] "["::
- (make_subst subst)@
- (Box.b_text [] "]")::(make_box_tail tail) )
- | CE.LocalVar (xref,name) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- if tail = [] then
- Box.b_object (P.Mi (attr,name))
- else
- Box.b_object (P.Mrow ([], P.Mi (attr,name)::(make_math_tail tail)))
- | CE.Meta (xref,name,l) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let l' =
- List.map
- (function
- None -> P.Mo([],"_")
- | Some t -> cexpr2pres t
- ) l
- in
- Box.b_object (P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ (make_math_tail tail)))
- | CE.Num (xref,value) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- if tail = [] then
- Box.b_object (P.Mn (attr,value))
- else
- Box.b_object (P.Mrow ([], P.Mn (attr,value)::(make_math_tail tail)))
- | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
- let aattr = make_attributes [Some "helm","xref"] [axref] in
- let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
- (try
- (let f = Hashtbl.find symbol_table_charcount n in
- f tl ~priority ~assoc ~tail aattr sattr)
- with notfound ->
- Box.b_v aattr (
- Box.b_h [] [
- Box.b_text [] "(";
- Box.b_object (cexpr2pres (CE.Symbol(sxref,n,subst,uri)))
- ] ::
- make_args_charcount ~tail:(")"::tail) tl
- ))
- | CE.Appl (xref,l) as t ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- Box.b_v attr (
- Box.b_h [] [
- Box.b_text [] "(";
- cexpr2pres_charcount (List.hd l)
- ] ::
- make_args_charcount ~tail:(")"::tail) (List.tl l)
- )
- | CE.Binder (xref, kind,(n,s),body) as t ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let binder =
- if kind = "Lambda" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
- else if kind = "Prod" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
- else if kind = "Forall" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x2200
- else if kind = "Exists" then
- Netconversion.ustring_of_uchar `Enc_utf8 0x2203
- else "unknown" in
- Box.b_v attr [
- Box.b_h [] [
- Box.b_text [None,"color","blue"] binder;
- Box.b_text [] (n ^ ":");
- cexpr2pres_charcount s ~tail:["."]
- ];
- Box.b_h [] [ Box.indent (cexpr2pres_charcount body ~tail:tail) ]
- ]
- | CE.Letin (xref,(n,s),body) as t ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- Box.b_v attr [
- Box.b_h [] [
- Box.b_kw "let";
- Box.smallskip;
- Box.b_text [] (n ^ "=");
- cexpr2pres_charcount s;
- Box.smallskip;
- Box.b_kw "in"
- ];
- Box.indent (cexpr2pres_charcount body)
- ]
- | CE.Letrec (xref,defs,body) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let rec make_defs =
- (function
- [] -> assert false
- | [(n,bo)] ->
- [Box.b_text [] (n ^ "="); (aux body)]
- | (n,bo)::tl ->
- Box.b_text [] (n ^ "=")::
- (aux body)::
- Box.smallskip::
- Box.b_kw "and"::
- (make_defs tl)) in
- Box.b_h attr (
- Box.b_kw "let" ::
- Box.smallskip ::
- Box.b_kw "rec" ::
- Box.smallskip ::
- make_defs defs @
- [ Box.smallskip; Box.b_kw "in"; Box.smallskip; aux body ]
- )
- | CE.Case (xref,a,np) ->
- let attr = make_attributes [Some "helm","xref"] [xref] in
- let arg =
- if (is_big a) then
- let tail = " with"::tail in (* LUCA: porcheria all'ennesima potenza, TODO ripensare il meccanismo del tail *)
- [ Box.b_h [] [ Box.b_kw "match"; Box.smallskip ];
- aux a ~tail
- ]
- else
- [ Box.b_h [] [
- Box.b_kw "match";
- Box.smallskip;
- aux a ~tail;
- Box.smallskip;
- Box.b_kw "with"
- ]
- ] in
- let rec make_patterns is_first ~tail =
- function
- [] -> []
- | [(n,p)] ->
- let sep = if is_first then "[ " else "| " in
- [ Box.b_h [] [make_pattern sep ~tail n p] ]
- | (n,p)::tl ->
- let sep =
- if is_first then "[ " else "| " in
- [ Box.b_h [] ((make_pattern sep [] n p) :: (make_patterns false ~tail tl)) ]
- and make_pattern sep ~tail n p =
- let rec get_vars_and_body =
- function
- CE.Binder (_, "Lambda",(n,_),body) ->
- let v,b = get_vars_and_body body in
- n::v,b
- | t -> [],t in
- let vars,body = get_vars_and_body p in
- let lhs =
- match vars with
- [] -> sep ^ n ^ " -> "
- | l -> sep ^"(" ^n^" "^(String.concat " " l) ^ ")" ^ " -> " in
- if (is_big body) then
- Box.b_v [] [
- Box.b_text [] lhs;
- Box.indent (aux ~tail body)
- ]
- else
- Box.b_h [] [ Box.b_text [] lhs; aux ~tail body ]
- in
- let patterns =
- make_patterns true np ~tail:("]"::tail) in
- Box.b_v attr (arg@patterns)
-;;
-
-
-
projects / helm.git / blobdiff