helm/ocaml/cic_transformations/cexpr2pres.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (**************************************************************************)
  27 (*                                                                        *)
  28 (*                           PROJECT HELM                                 *)
  29 (*                                                                        *)
  30 (*                Andrea Asperti <asperti@cs.unibo.it>                    *)
  31 (*                             28/6/2003                                   *)
  32 (*                                                                        *)
  33 (**************************************************************************)
  34
  35 module P = Mpresentation;;
  36
  37 let symbol_table = Hashtbl.create 503;;
  38 let symbol_table_charcount = Hashtbl.create 503;;
  39
  40 let maxsize = 25;;
  41
  42 let countterm current_size t =
  43   let module CE = Content_expressions in
  44   let rec aux current_size t =
  45     if current_size > maxsize then current_size
  46     else match t with
  47       CE.Symbol (_,name,None,_) -> current_size + (String.length name)
  48     | CE.Symbol (_,name,Some subst,_) ->
  49         let c1 = current_size + (String.length name) in
  50         countsubst subst c1
  51     | CE.LocalVar (_,name) -> current_size + (String.length name)
  52     | CE.Meta (_,name) -> current_size + (String.length name)
  53     | CE.Num (_,value) -> current_size + (String.length value)
  54     | CE.Appl (_,l) ->
  55         List.fold_left aux current_size l
  56     | CE.Binder (_, _,(n,s),body) ->
  57         let cs = aux (current_size + 2 + (String.length n)) s in
  58         aux cs body
  59     | CE.Letin (_,(n,s),body) ->
  60         let cs = aux (current_size + 3 + (String.length n)) s in
  61         aux cs body
  62     | CE.Letrec (_,defs,body) ->
  63         let cs =
  64           List.fold_left
  65             (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size defs in
  66         aux cs body
  67     | CE.Case (_,a,np) ->
  68         let cs = aux (current_size + 4) a in
  69         List.fold_left
  70           (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size np
  71   and
  72   countsubst subst current_size =
  73     List.fold_left
  74       (fun current_size (uri,expr) ->
  75          if (current_size > maxsize) then current_size
  76          else
  77            let c1 =
  78              (current_size + (String.length (UriManager.name_of_uri uri))) in
  79            (aux c1 expr)) current_size subst
  80   in
  81   (aux current_size t)
  82 ;;
  83
  84 let is_big t =
  85   ((countterm 0 t) > maxsize)
  86 ;;
  87
  88 let rec make_attributes l1 =
  89   function
  90       [] -> []
  91     | None::tl -> make_attributes (List.tl l1) tl
  92     | (Some s)::tl ->
  93        let p,n = List.hd l1 in
  94         (p,n,s)::(make_attributes (List.tl l1) tl)
  95 ;;
  96
  97 let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
  98   let module CE = Content_expressions in
  99   let module P = Mpresentation in
 100   let rec aux =
 101   function
 102       CE.Symbol (xref,name,None,uri) ->
 103         let attr =
 104          make_attributes
 105           [Some "helm","xref";Some "xlink","href"] [xref;uri] in
 106         if tail = [] then
 107           P.Mi (attr,name)
 108         else P.Mrow([],P.Mi (attr,name)::tail)
 109     | CE.Symbol (xref,name,Some subst,uri) ->
 110         let attr =
 111          make_attributes
 112           [Some "helm","xref";Some "xlink","href"] [xref;uri] in
 113         let rec make_subst =
 114           (function
 115                [] -> assert false
 116              | [(uri,a)] ->
 117                  [(aux a);
 118                   P.Mtext([],"/");
 119                   P.Mi([],UriManager.name_of_uri uri)]
 120              | (uri,a)::tl ->
 121                  (aux a)::
 122                  P.Mtext([],"/")::
 123                  P.Mi([],UriManager.name_of_uri uri)::
 124                  P.Mtext([],"; ")::
 125                  P.smallskip::
 126                  (make_subst tl)) in
 127         P.Mrow ([],
 128           P.Mi (attr,name)::
 129           P.Mtext([],"[")::
 130           (make_subst subst)@
 131           (P.Mtext([],"]")::tail))
 132     | CE.LocalVar (xref,name) ->
 133         let attr = make_attributes [Some "helm","xref"] [xref] in
 134         if tail = [] then
 135           P.Mi (attr,name)
 136         else P.Mrow([],P.Mi (attr,name)::tail)
 137     | CE.Meta (xref,name) ->
 138         let attr = make_attributes [Some "helm","xref"] [xref] in
 139         if tail = [] then
 140           P.Mi (attr,name)
 141         else P.Mrow([],P.Mi (attr,name)::tail)
 142     | CE.Num (xref,value) ->
 143         let attr = make_attributes [Some "helm","xref"] [xref] in
 144         if tail = [] then
 145           P.Mn (attr,value)
 146         else P.Mrow([],P.Mn (attr,value)::tail)
 147     | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
 148         let aattr = make_attributes [Some "helm","xref"] [axref] in
 149         let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
 150         (try
 151           (let f = Hashtbl.find symbol_table n in
 152            f tl ~priority ~assoc ~tail aattr sattr)
 153         with notfound ->
 154            P.Mrow(aattr,
 155            P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::tail)))
 156     | CE.Appl (xref,l) as t ->
 157         let attr = make_attributes [Some"helm","xref"] [xref] in
 158         P.Mrow(attr,
 159            P.Mo([],"(")::(make_args l)@(P.Mo([],")")::tail))
 160     | CE.Binder (xref, kind,(n,s),body) ->
 161         let attr = make_attributes [Some "helm","xref"] [xref] in
 162         let binder =
 163           if kind = "Lambda" then
 164              Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
 165           else if kind = "Prod" then
 166              Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
 167           else if kind = "Forall" then
 168              Netconversion.ustring_of_uchar `Enc_utf8 0x2200
 169           else if kind = "Exists" then
 170              Netconversion.ustring_of_uchar `Enc_utf8 0x2203
 171           else "unknown" in
 172         P.Mrow (attr,
 173            P.Mtext([None,"mathcolor","Blue"],binder)::
 174            P.Mtext([],n ^ ":")::
 175            (aux s)::
 176            P.Mo([],".")::
 177            (aux body)::tail)
 178     | CE.Letin (xref,(n,s),body) ->
 179         let attr = make_attributes [Some "helm","xref"] [xref] in
 180         P.Mrow (attr,
 181            P.Mtext([],("let "))::
 182            P.Mtext([],(n ^ "="))::
 183            (aux s)::
 184            P.Mtext([]," in ")::
 185            (aux body)::tail)
 186     | CE.Letrec (xref,defs,body) ->
 187         let attr = make_attributes [Some "helm","xref"] [xref] in
 188         let rec make_defs =
 189           (function
 190                [] -> assert false
 191              | [(n,bo)] ->
 192                  [P.Mtext([],(n ^ "="));(aux body)]
 193              | (n,bo)::tl ->
 194                  P.Mtext([],(n ^ "="))::
 195                  (aux body)::P.Mtext([]," and")::(make_defs tl)) in
 196         P.Mrow (attr,
 197           P.Mtext([],("let rec "))::
 198           (make_defs defs)@
 199            (P.Mtext([]," in ")::
 200            (aux body)::tail))
 201     | CE.Case (xref,a,np) ->
 202         let attr = make_attributes [Some "helm","xref"] [xref] in
 203         let rec make_patterns =
 204           (function
 205                [] -> []
 206              | [(n,p)] ->
 207                  [P.Mtext([],(n ^ " -> "));(aux p)]
 208              | (n,p)::tl ->
 209                  P.Mtext([],(n ^ " -> "))::
 210                  (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in
 211         P.Mrow (attr,
 212           P.Mtext([],("case "))::
 213           (aux a)::
 214           P.Mtext([],(" of "))::
 215           (make_patterns np)@tail) in
 216   aux t
 217
 218 and
 219
 220 make_args ?(priority = 0) ?(assoc = false) ?(tail = []) =
 221   let module P = Mpresentation in
 222   function
 223       [] -> tail
 224     | a::tl -> P.smallskip::(cexpr2pres a)::(make_args ~tail:tail tl)
 225 ;;
 226
 227 let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) =
 228   let module P = Mpresentation in
 229   function
 230     [] -> []
 231   | [a] ->
 232       [P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount ~tail:tail a))])]
 233   | (a::tl) as l ->
 234       let c = List.fold_left countterm 0 l in
 235       if c > maxsize then
 236         P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount a))])::
 237         (make_args_charcount ~tail:tail tl)
 238       else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([None,"width","0.2cm"]))::(make_args ~tail:tail l)))])]
 239
 240 (*
 241   function
 242       [] -> []
 243     | a::tl ->
 244         let tlpres =
 245           let c = List.fold_left countterm 0 tl in
 246           if c > maxsize then
 247             P.Mtable ([("align","baseline 1");("equalrows","false");
 248              ("columnalign","left")],
 249               (make_args_charcount tl))
 250           else
 251             P.Mrow([], make_args tl) in
 252         [P.Mtr([],[P.Mtd([],(cexpr2pres_charcount a))]);
 253          P.Mtr([],[P.Mtd([],P.indented tlpres)])] *)
 254 and
 255
 256 cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
 257   let module CE = Content_expressions in
 258   let module P = Mpresentation in
 259   let rec aux =
 260   function
 261       CE.Symbol (xref,name,None,uri) ->
 262         let attr =
 263          make_attributes
 264           [Some "helm","xref";Some "xlink","href"] [xref;uri] in
 265         if tail = [] then
 266           P.Mi (attr,name)
 267         else P.Mrow ([],P.Mi (attr,name)::tail)
 268     | CE.Symbol (xref,name,Some subst,uri) ->
 269         let attr =
 270          make_attributes
 271           [Some "helm","xref";Some "xlink","href"] [xref;uri] in
 272         let rec make_subst =
 273           (function
 274                [] -> assert false
 275              | [(uri,a)] ->
 276                  [(cexpr2pres a);
 277                   P.Mtext([],"/");
 278                   P.Mi([],UriManager.name_of_uri uri)]
 279              | (uri,a)::tl ->
 280                  (cexpr2pres a)::
 281                  P.Mtext([],"/")::
 282                  P.Mi([],UriManager.name_of_uri uri)::
 283                  P.Mtext([],"; ")::
 284                  P.smallskip::
 285                  (make_subst tl)) in
 286         P.Mrow ([],
 287           P.Mi (attr,name)::
 288           P.Mtext([],"[")::
 289           (make_subst subst)@
 290           (P.Mtext([],"]")::tail))
 291     | CE.LocalVar (xref,name) ->
 292         let attr = make_attributes [Some "helm","xref"] [xref] in
 293         if tail = [] then
 294           P.Mi (attr,name)
 295         else P.Mrow ([],P.Mi (attr,name)::tail)
 296     | CE.Meta (xref,name) ->
 297         let attr = make_attributes [Some "helm","xref"] [xref] in
 298         if tail = [] then
 299           P.Mi (attr,name)
 300         else P.Mrow ([],P.Mi (attr,name)::tail)
 301     | CE.Num (xref,value) ->
 302         let attr = make_attributes [Some "helm","xref"] [xref] in
 303         if tail = [] then
 304           P.Mn (attr,value)
 305         else P.Mrow ([],P.Mn (attr,value)::tail)
 306     | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
 307         let aattr = make_attributes [Some "helm","xref"] [axref] in
 308         let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
 309         if (is_big t) then
 310           (try
 311             (let f = Hashtbl.find symbol_table_charcount n in
 312              f tl ~priority ~assoc ~tail aattr sattr)
 313           with notfound ->
 314             P.Mtable (aattr@P.standard_tbl_attr,
 315               P.Mtr([],[P.Mtd([],P.Mrow([],
 316                 [P.Mtext([],"(");
 317                  cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))])::
 318               make_args_charcount ~tail:(P.Mtext([],")")::tail) tl))
 319         else cexpr2pres t
 320     | CE.Appl (xref,l) as t ->
 321         let attr = make_attributes [Some "helm","xref"] [xref] in
 322         if (is_big t) then
 323           P.Mtable (attr@P.standard_tbl_attr,
 324             P.Mtr([],[P.Mtd([],P.Mrow([],
 325               [P.Mtext([],"(");
 326                cexpr2pres_charcount (List.hd l)]))])::
 327             make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l))
 328         else cexpr2pres t
 329     | CE.Binder (xref, kind,(n,s),body) as t ->
 330         if (is_big t) then
 331           let attr = make_attributes [Some "helm","xref"] [xref] in
 332           let binder =
 333             if kind = "Lambda" then
 334               Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
 335             else if kind = "Prod" then
 336               Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
 337             else if kind = "Forall" then
 338               Netconversion.ustring_of_uchar `Enc_utf8 0x2200
 339             else if kind = "Exists" then
 340               Netconversion.ustring_of_uchar `Enc_utf8 0x2203
 341             else "unknown" in
 342           P.Mtable (attr@P.standard_tbl_attr,
 343              [P.Mtr ([],[P.Mtd ([],
 344                P.Mrow([],
 345                 [P.Mtext([None,"mathcolor","Blue"],binder);
 346                  P.Mtext([],n ^ ":");
 347                  cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]);
 348               P.Mtr ([],[P.Mtd ([],
 349                P.indented (cexpr2pres_charcount body ~tail:tail))])])
 350         else (cexpr2pres t ~tail:tail)
 351     | CE.Letin (xref,(n,s),body) as t ->
 352         if (is_big t) then
 353           let attr = make_attributes [Some "helm","xref"] [xref] in
 354           P.Mtable (attr@P.standard_tbl_attr,
 355              [P.Mtr ([],[P.Mtd ([],
 356                P.Mrow([],
 357                 [P.Mtext([None,"mathcolor","Blue"],"let");
 358                  P.smallskip;
 359                  P.Mtext([],n ^ "=");
 360                  cexpr2pres_charcount s;
 361                  P.smallskip;
 362                  P.Mtext([],"in");
 363                 ]))]);
 364               P.Mtr ([],[P.Mtd ([],
 365                P.indented (cexpr2pres_charcount body))])])
 366         else (cexpr2pres t)
 367     | CE.Letrec (xref,defs,body) ->
 368         let attr = make_attributes [Some "helm","xref"] [xref] in
 369         let rec make_defs =
 370           (function
 371                [] -> assert false
 372              | [(n,bo)] ->
 373                  [P.Mtext([],(n ^ "="));(aux body)]
 374              | (n,bo)::tl ->
 375                  P.Mtext([],(n ^ "="))::
 376                  (aux body)::P.Mtext([]," and")::(make_defs tl)) in
 377         P.Mrow (attr,
 378           P.Mtext([],("let rec "))::
 379           (make_defs defs)@
 380           [P.Mtext([]," in ");
 381            (aux body)])
 382     | CE.Case (xref,a,np) ->
 383         let attr = make_attributes [Some "helm","xref"] [xref] in
 384         let rec make_patterns =
 385           (function
 386                [] -> []
 387              | [(n,p)] ->
 388                  [P.Mtext([],(n ^ " -> "));(aux p)]
 389              | (n,p)::tl ->
 390                  P.Mtext([],(n ^ " -> "))::
 391                  (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in
 392         P.Mrow (attr,
 393           P.Mtext([],("case "))::
 394           (aux a)::
 395           P.Mtext([],(" of "))::
 396           (make_patterns np)) in
 397   aux t
 398 ;;