(**************************************************************************)
module P = Mpresentation;;
+module CE = Content_expressions;;
let symbol_table = Hashtbl.create 503;;
let symbol_table_charcount = Hashtbl.create 503;;
let maxsize = 25;;
-let countterm current_size t =
- let module CE = Content_expressions in
- let rec aux 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) -> current_size + (String.length name)
- | CE.Num (_,value) -> current_size + (String.length value)
- | CE.Appl (_,l) ->
- List.fold_left aux current_size l
- | CE.Binder (_, _,(n,s),body) ->
- let cs = aux (current_size + 2 + (String.length n)) s in
- aux cs body
- | CE.Letin (_,(n,s),body) ->
- let cs = aux (current_size + 3 + (String.length n)) s in
- aux cs body
- | CE.Letrec (_,defs,body) ->
- let cs =
- List.fold_left
- (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size defs in
- aux cs body
- | CE.Case (_,a,np) ->
- let cs = aux (current_size + 4) a in
+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) -> aux (c+(String.length n)) bo) current_size np
- and
- countsubst subst current_size =
+ (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
- (aux c1 expr)) current_size subst
- in
- (aux current_size t)
+ (countterm c1 expr)) current_size subst
;;
let is_big t =
function
[] -> []
| None::tl -> make_attributes (List.tl l1) tl
- | (Some s)::tl -> (List.hd l1,s)::(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 rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
CE.Symbol (xref,name,None,uri) ->
let attr =
make_attributes
- ["helm:xref";"xlink:href"] [xref;uri] in
+ [Some "helm","xref";Some "xlink","href"] [xref;uri] in
if tail = [] then
P.Mi (attr,name)
else P.Mrow([],P.Mi (attr,name)::tail)
| CE.Symbol (xref,name,Some subst,uri) ->
let attr =
make_attributes
- ["helm:xref";"xlink:href"] [xref;uri] in
+ [Some "helm","xref";Some "xlink","href"] [xref;uri] in
let rec make_subst =
(function
[] -> assert false
(make_subst subst)@
(P.Mtext([],"]")::tail))
| CE.LocalVar (xref,name) ->
- let attr = make_attributes ["helm:xref"] [xref] in
- if tail = [] then
- P.Mi (attr,name)
- else P.Mrow([],P.Mi (attr,name)::tail)
- | CE.Meta (xref,name) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
if tail = [] then
P.Mi (attr,name)
else P.Mrow([],P.Mi (attr,name)::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 ([],"]")] @ tail)
| CE.Num (xref,value) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
if tail = [] then
P.Mn (attr,value)
else P.Mrow([],P.Mn (attr,value)::tail)
| CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
- let aattr = make_attributes ["helm:xref"] [axref] in
- let sattr = make_attributes ["helm:xref";"xlink:href"] [sxref;uri] in
+ 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)
P.Mrow(aattr,
P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::tail)))
| CE.Appl (xref,l) as t ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some"helm","xref"] [xref] in
P.Mrow(attr,
P.Mo([],"(")::(make_args l)@(P.Mo([],")")::tail))
| CE.Binder (xref, kind,(n,s),body) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
let binder =
if kind = "Lambda" then
Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
Netconversion.ustring_of_uchar `Enc_utf8 0x2203
else "unknown" in
P.Mrow (attr,
- P.Mtext([("mathcolor","Blue")],binder)::
+ P.Mtext([None,"mathcolor","Blue"],binder)::
P.Mtext([],n ^ ":")::
(aux s)::
P.Mo([],".")::
(aux body)::tail)
| CE.Letin (xref,(n,s),body) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
P.Mrow (attr,
P.Mtext([],("let "))::
P.Mtext([],(n ^ "="))::
P.Mtext([]," in ")::
(aux body)::tail)
| CE.Letrec (xref,defs,body) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
let rec make_defs =
(function
[] -> assert false
(P.Mtext([]," in ")::
(aux body)::tail))
| CE.Case (xref,a,np) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
let rec make_patterns =
(function
[] -> []
- | [(n,p)] ->
- [P.Mtext([],(n ^ " -> "));(aux p)]
+ | [(n,p)] -> make_pattern n p
| (n,p)::tl ->
- P.Mtext([],(n ^ " -> "))::
- (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in
+ (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([],("case "))::
- (aux a)::
- P.Mtext([],(" of "))::
- (make_patterns np)@tail) in
+ 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([],("]"))::tail)) in
aux t
and
if c > maxsize then
P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount a))])::
(make_args_charcount ~tail:tail tl)
- else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([("width","0.2cm")]))::(make_args ~tail:tail l)))])]
+ else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([None,"width","0.2cm"]))::(make_args ~tail:tail l)))])]
(*
function
and
cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
- let module CE = Content_expressions in
- let module P = Mpresentation in
- let rec aux =
- function
+ if not(is_big t) then (cexpr2pres ~priority ~assoc ~tail t)
+ else let aux = cexpr2pres_charcount in
+ match t with
CE.Symbol (xref,name,None,uri) ->
let attr =
make_attributes
- ["helm:xref";"xlink:href"] [xref;uri] in
+ [Some "helm","xref";Some "xlink","href"] [xref;uri] in
if tail = [] then
P.Mi (attr,name)
else P.Mrow ([],P.Mi (attr,name)::tail)
| CE.Symbol (xref,name,Some subst,uri) ->
let attr =
make_attributes
- ["helm:xref";"xlink:href"] [xref;uri] in
+ [Some "helm","xref";Some "xlink","href"] [xref;uri] in
let rec make_subst =
(function
[] -> assert false
(make_subst subst)@
(P.Mtext([],"]")::tail))
| CE.LocalVar (xref,name) ->
- let attr = make_attributes ["helm:xref"] [xref] in
- if tail = [] then
- P.Mi (attr,name)
- else P.Mrow ([],P.Mi (attr,name)::tail)
- | CE.Meta (xref,name) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
if tail = [] then
P.Mi (attr,name)
else P.Mrow ([],P.Mi (attr,name)::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 ([],"]")] @ tail)
| CE.Num (xref,value) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
if tail = [] then
P.Mn (attr,value)
else P.Mrow ([],P.Mn (attr,value)::tail)
| CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
- let aattr = make_attributes ["helm:xref"] [axref] in
- let sattr = make_attributes ["helm:xref";"xlink:href"] [sxref;uri] in
- if (is_big t) then
- (try
- (let f = Hashtbl.find symbol_table_charcount n in
- f tl ~priority ~assoc ~tail aattr sattr)
- with notfound ->
- P.Mtable (aattr@P.standard_tbl_attr,
- P.Mtr([],[P.Mtd([],P.Mrow([],
- [P.Mtext([],"(");
- cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))])::
- make_args_charcount ~tail:(P.Mtext([],")")::tail) tl))
- else cexpr2pres t
- | CE.Appl (xref,l) as t ->
- let attr = make_attributes ["helm:xref"] [xref] in
- if (is_big t) then
- P.Mtable (attr@P.standard_tbl_attr,
+ 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 ->
+ P.Mtable (aattr@P.standard_tbl_attr,
P.Mtr([],[P.Mtd([],P.Mrow([],
[P.Mtext([],"(");
- cexpr2pres_charcount (List.hd l)]))])::
- make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l))
- else cexpr2pres t
+ cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))])::
+ make_args_charcount ~tail:(P.Mtext([],")")::tail) tl))
+ | CE.Appl (xref,l) as t ->
+ let attr = make_attributes [Some "helm","xref"] [xref] in
+ P.Mtable (attr@P.standard_tbl_attr,
+ P.Mtr([],[P.Mtd([],P.Mrow([],
+ [P.Mtext([],"(");
+ cexpr2pres_charcount (List.hd l)]))])::
+ make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l))
| CE.Binder (xref, kind,(n,s),body) as t ->
- if (is_big t) then
- let attr = make_attributes ["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.Mtable (attr@P.standard_tbl_attr,
- [P.Mtr ([],[P.Mtd ([],
- P.Mrow([],
- [P.Mtext([("mathcolor","Blue")],binder);
- P.Mtext([],n ^ ":");
- cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]);
- P.Mtr ([],[P.Mtd ([],
- P.indented (cexpr2pres_charcount body ~tail:tail))])])
- else (cexpr2pres t ~tail:tail)
+ 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.Mtable (attr@P.standard_tbl_attr,
+ [P.Mtr ([],[P.Mtd ([],
+ P.Mrow([],
+ [P.Mtext([None,"mathcolor","Blue"],binder);
+ P.Mtext([],n ^ ":");
+ cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]);
+ P.Mtr ([],[P.Mtd ([],
+ P.indented (cexpr2pres_charcount body ~tail:tail))])])
| CE.Letin (xref,(n,s),body) as t ->
- if (is_big t) then
- let attr = make_attributes ["helm:xref"] [xref] in
- P.Mtable (attr@P.standard_tbl_attr,
- [P.Mtr ([],[P.Mtd ([],
- P.Mrow([],
- [P.Mtext([("mathcolor","Blue")],"let");
- P.smallskip;
- P.Mtext([],n ^ "=");
- cexpr2pres_charcount s;
- P.smallskip;
- P.Mtext([],"in");
- ]))]);
- P.Mtr ([],[P.Mtd ([],
- P.indented (cexpr2pres_charcount body))])])
- else (cexpr2pres t)
+ let attr = make_attributes [Some "helm","xref"] [xref] in
+ P.Mtable (attr@P.standard_tbl_attr,
+ [P.Mtr ([],[P.Mtd ([],
+ P.Mrow([],
+ [P.Mtext([None,"mathcolor","Blue"],"let");
+ P.smallskip;
+ P.Mtext([],n ^ "=");
+ cexpr2pres_charcount s;
+ P.smallskip;
+ P.Mtext([],"in");
+ ]))]);
+ P.Mtr ([],[P.Mtd ([],
+ P.indented (cexpr2pres_charcount body))])])
| CE.Letrec (xref,defs,body) ->
- let attr = make_attributes ["helm:xref"] [xref] in
+ let attr = make_attributes [Some "helm","xref"] [xref] in
let rec make_defs =
(function
[] -> assert false
[P.Mtext([]," in ");
(aux body)])
| CE.Case (xref,a,np) ->
- let attr = make_attributes ["helm:xref"] [xref] in
- let rec make_patterns =
- (function
- [] -> []
- | [(n,p)] ->
- [P.Mtext([],(n ^ " -> "));(aux p)]
- | (n,p)::tl ->
- P.Mtext([],(n ^ " -> "))::
- (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in
- P.Mrow (attr,
- P.Mtext([],("case "))::
- (aux a)::
- P.Mtext([],(" of "))::
- (make_patterns np)) in
- aux t
+ let attr = make_attributes [Some "helm","xref"] [xref] in
+ let arg =
+ if (is_big a) then
+ let tail = P.Mtext([],(" with"))::tail in
+ [P.Mtr ([],[P.Mtd ([],P.Mtext([],("match ")))]);
+ P.Mtr ([],[P.Mtd ([],aux a ~tail:tail)])]
+ else
+ [P.Mtr ([],[P.Mtd ([],P.Mrow([],[P.Mtext([],("match"));P.smallskip;aux a ~tail:tail; P.smallskip;P.Mtext([],("with"))]))])] in
+ let rec make_patterns is_first ~tail =
+ function
+ [] -> []
+ | [(n,p)] ->
+ let sep =
+ if is_first then "[ " else "| " in
+ [P.Mtr ([],
+ [P.Mtd ([],
+ make_pattern sep ~tail n p)])]
+ | (n,p)::tl ->
+ let sep =
+ if is_first then "[ " else "| " in
+ P.Mtr ([],
+ [P.Mtd ([],
+ 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
+ P.Mtable (P.standard_tbl_attr,
+ [P.Mtr ([],
+ [P.Mtd ([],P.Mtext([],lhs))]);
+ P.Mtr ([],
+ [P.Mtd ([],P.indented (aux ~tail body ))])])
+ else
+ P.Mrow([],[P.Mtext([],lhs);aux ~tail body]) in
+ let patterns =
+ make_patterns true np ~tail:(P.Mtext([],"]")::tail) in
+ P.Mtable (attr@P.standard_tbl_attr,
+ arg@patterns)
;;
+
+
+
projects / helm.git / blobdiff