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 -> (List.hd l1,s)::(make_attributes (List.tl l1) tl)
  93 ;;
  94
  95 let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
  96   let module CE = Content_expressions in
  97   let module P = Mpresentation in
  98   let rec aux =
  99   function
 100       CE.Symbol (xref,name,None,uri) ->
 101         let attr =
 102          make_attributes
 103           ["helm:xref";"xlink:href"] [xref;uri] in
 104         if tail = [] then
 105           P.Mi (attr,name)
 106         else P.Mrow([],P.Mi (attr,name)::tail)
 107     | CE.Symbol (xref,name,Some subst,uri) ->
 108         let attr =
 109          make_attributes
 110           ["helm:xref";"xlink:href"] [xref;uri] in
 111         let rec make_subst =
 112           (function
 113                [] -> assert false
 114              | [(uri,a)] ->
 115                  [(aux a);
 116                   P.Mtext([],"/");
 117                   P.Mi([],UriManager.name_of_uri uri)]
 118              | (uri,a)::tl ->
 119                  (aux a)::
 120                  P.Mtext([],"/")::
 121                  P.Mi([],UriManager.name_of_uri uri)::
 122                  P.Mtext([],"; ")::
 123                  P.smallskip::
 124                  (make_subst tl)) in
 125         P.Mrow ([],
 126           P.Mi (attr,name)::
 127           P.Mtext([],"[")::
 128           (make_subst subst)@
 129           (P.Mtext([],"]")::tail))
 130     | CE.LocalVar (xref,name) ->
 131         let attr = make_attributes ["helm:xref"] [xref] in
 132         if tail = [] then
 133           P.Mi (attr,name)
 134         else P.Mrow([],P.Mi (attr,name)::tail)
 135     | CE.Meta (xref,name) ->
 136         let attr = make_attributes ["helm:xref"] [xref] in
 137         if tail = [] then
 138           P.Mi (attr,name)
 139         else P.Mrow([],P.Mi (attr,name)::tail)
 140     | CE.Num (xref,value) ->
 141         let attr = make_attributes ["helm:xref"] [xref] in
 142         if tail = [] then
 143           P.Mn (attr,value)
 144         else P.Mrow([],P.Mn (attr,value)::tail)
 145     | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
 146         let aattr = make_attributes ["helm:xref"] [axref] in
 147         let sattr = make_attributes ["helm:xref";"xlink:href"] [sxref;uri] in
 148         (try
 149           (let f = Hashtbl.find symbol_table n in
 150            f tl ~priority ~assoc ~tail aattr sattr)
 151         with notfound ->
 152            P.Mrow(aattr,
 153            P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::tail)))
 154     | CE.Appl (xref,l) as t ->
 155         let attr = make_attributes ["helm:xref"] [xref] in
 156         P.Mrow(attr,
 157            P.Mo([],"(")::(make_args l)@(P.Mo([],")")::tail))
 158     | CE.Binder (xref, kind,(n,s),body) ->
 159         let attr = make_attributes ["helm:xref"] [xref] in
 160         let binder =
 161           if kind = "Lambda" then
 162              Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
 163           else if kind = "Prod" then
 164              Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
 165           else if kind = "Forall" then
 166              Netconversion.ustring_of_uchar `Enc_utf8 0x2200
 167           else if kind = "Exists" then
 168              Netconversion.ustring_of_uchar `Enc_utf8 0x2203
 169           else "unknown" in
 170         P.Mrow (attr,
 171            P.Mtext([("mathcolor","Blue")],binder)::
 172            P.Mtext([],n ^ ":")::
 173            (aux s)::
 174            P.Mo([],".")::
 175            (aux body)::tail)
 176     | CE.Letin (xref,(n,s),body) ->
 177         let attr = make_attributes ["helm:xref"] [xref] in
 178         P.Mrow (attr,
 179            P.Mtext([],("let "))::
 180            P.Mtext([],(n ^ "="))::
 181            (aux s)::
 182            P.Mtext([]," in ")::
 183            (aux body)::tail)
 184     | CE.Letrec (xref,defs,body) ->
 185         let attr = make_attributes ["helm:xref"] [xref] in
 186         let rec make_defs =
 187           (function
 188                [] -> assert false
 189              | [(n,bo)] ->
 190                  [P.Mtext([],(n ^ "="));(aux body)]
 191              | (n,bo)::tl ->
 192                  P.Mtext([],(n ^ "="))::
 193                  (aux body)::P.Mtext([]," and")::(make_defs tl)) in
 194         P.Mrow (attr,
 195           P.Mtext([],("let rec "))::
 196           (make_defs defs)@
 197            (P.Mtext([]," in ")::
 198            (aux body)::tail))
 199     | CE.Case (xref,a,np) ->
 200         let attr = make_attributes ["helm:xref"] [xref] in
 201         let rec make_patterns =
 202           (function
 203                [] -> []
 204              | [(n,p)] ->
 205                  [P.Mtext([],(n ^ " -> "));(aux p)]
 206              | (n,p)::tl ->
 207                  P.Mtext([],(n ^ " -> "))::
 208                  (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in
 209         P.Mrow (attr,
 210           P.Mtext([],("case "))::
 211           (aux a)::
 212           P.Mtext([],(" of "))::
 213           (make_patterns np)@tail) in
 214   aux t
 215
 216 and
 217
 218 make_args ?(priority = 0) ?(assoc = false) ?(tail = []) =
 219   let module P = Mpresentation in
 220   function
 221       [] -> tail
 222     | a::tl -> P.smallskip::(cexpr2pres a)::(make_args ~tail:tail tl)
 223 ;;
 224
 225 let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) =
 226   let module P = Mpresentation in
 227   function
 228     [] -> []
 229   | [a] ->
 230       [P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount ~tail:tail a))])]
 231   | (a::tl) as l ->
 232       let c = List.fold_left countterm 0 l in
 233       if c > maxsize then
 234         P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount a))])::
 235         (make_args_charcount ~tail:tail tl)
 236       else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([("width","0.2cm")]))::(make_args ~tail:tail l)))])]
 237
 238 (*
 239   function
 240       [] -> []
 241     | a::tl ->
 242         let tlpres =
 243           let c = List.fold_left countterm 0 tl in
 244           if c > maxsize then
 245             P.Mtable ([("align","baseline 1");("equalrows","false");
 246              ("columnalign","left")],
 247               (make_args_charcount tl))
 248           else
 249             P.Mrow([], make_args tl) in
 250         [P.Mtr([],[P.Mtd([],(cexpr2pres_charcount a))]);
 251          P.Mtr([],[P.Mtd([],P.indented tlpres)])] *)
 252 and
 253
 254 cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
 255   let module CE = Content_expressions in
 256   let module P = Mpresentation in
 257   let rec aux =
 258   function
 259       CE.Symbol (xref,name,None,uri) ->
 260         let attr =
 261          make_attributes
 262           ["helm:xref";"xlink:href"] [xref;uri] in
 263         if tail = [] then
 264           P.Mi (attr,name)
 265         else P.Mrow ([],P.Mi (attr,name)::tail)
 266     | CE.Symbol (xref,name,Some subst,uri) ->
 267         let attr =
 268          make_attributes
 269           ["helm:xref";"xlink:href"] [xref;uri] in
 270         let rec make_subst =
 271           (function
 272                [] -> assert false
 273              | [(uri,a)] ->
 274                  [(cexpr2pres a);
 275                   P.Mtext([],"/");
 276                   P.Mi([],UriManager.name_of_uri uri)]
 277              | (uri,a)::tl ->
 278                  (cexpr2pres a)::
 279                  P.Mtext([],"/")::
 280                  P.Mi([],UriManager.name_of_uri uri)::
 281                  P.Mtext([],"; ")::
 282                  P.smallskip::
 283                  (make_subst tl)) in
 284         P.Mrow ([],
 285           P.Mi (attr,name)::
 286           P.Mtext([],"[")::
 287           (make_subst subst)@
 288           (P.Mtext([],"]")::tail))
 289     | CE.LocalVar (xref,name) ->
 290         let attr = make_attributes ["helm:xref"] [xref] in
 291         if tail = [] then
 292           P.Mi (attr,name)
 293         else P.Mrow ([],P.Mi (attr,name)::tail)
 294     | CE.Meta (xref,name) ->
 295         let attr = make_attributes ["helm:xref"] [xref] in
 296         if tail = [] then
 297           P.Mi (attr,name)
 298         else P.Mrow ([],P.Mi (attr,name)::tail)
 299     | CE.Num (xref,value) ->
 300         let attr = make_attributes ["helm:xref"] [xref] in
 301         if tail = [] then
 302           P.Mn (attr,value)
 303         else P.Mrow ([],P.Mn (attr,value)::tail)
 304     | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
 305         let aattr = make_attributes ["helm:xref"] [axref] in
 306         let sattr = make_attributes ["helm:xref";"xlink:href"] [sxref;uri] in
 307         if (is_big t) then
 308           (try
 309             (let f = Hashtbl.find symbol_table_charcount n in
 310              f tl ~priority ~assoc ~tail aattr sattr)
 311           with notfound ->
 312             P.Mtable (aattr@P.standard_tbl_attr,
 313               P.Mtr([],[P.Mtd([],P.Mrow([],
 314                 [P.Mtext([],"(");
 315                  cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))])::
 316               make_args_charcount ~tail:(P.Mtext([],")")::tail) tl))
 317         else cexpr2pres t
 318     | CE.Appl (xref,l) as t ->
 319         let attr = make_attributes ["helm:xref"] [xref] in
 320         if (is_big t) then
 321           P.Mtable (attr@P.standard_tbl_attr,
 322             P.Mtr([],[P.Mtd([],P.Mrow([],
 323               [P.Mtext([],"(");
 324                cexpr2pres_charcount (List.hd l)]))])::
 325             make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l))
 326         else cexpr2pres t
 327     | CE.Binder (xref, kind,(n,s),body) as t ->
 328         if (is_big t) then
 329           let attr = make_attributes ["helm:xref"] [xref] in
 330           let binder =
 331             if kind = "Lambda" then
 332               Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
 333             else if kind = "Prod" then
 334               Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
 335             else if kind = "Forall" then
 336               Netconversion.ustring_of_uchar `Enc_utf8 0x2200
 337             else if kind = "Exists" then
 338               Netconversion.ustring_of_uchar `Enc_utf8 0x2203
 339             else "unknown" in
 340           P.Mtable (attr@P.standard_tbl_attr,
 341              [P.Mtr ([],[P.Mtd ([],
 342                P.Mrow([],
 343                 [P.Mtext([("mathcolor","Blue")],binder);
 344                  P.Mtext([],n ^ ":");
 345                  cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]);
 346               P.Mtr ([],[P.Mtd ([],
 347                P.indented (cexpr2pres_charcount body ~tail:tail))])])
 348         else (cexpr2pres t ~tail:tail)
 349     | CE.Letin (xref,(n,s),body) as t ->
 350         if (is_big t) then
 351           let attr = make_attributes ["helm:xref"] [xref] in
 352           P.Mtable (attr@P.standard_tbl_attr,
 353              [P.Mtr ([],[P.Mtd ([],
 354                P.Mrow([],
 355                 [P.Mtext([("mathcolor","Blue")],"let");
 356                  P.smallskip;
 357                  P.Mtext([],n ^ "=");
 358                  cexpr2pres_charcount s;
 359                  P.smallskip;
 360                  P.Mtext([],"in");
 361                 ]))]);
 362               P.Mtr ([],[P.Mtd ([],
 363                P.indented (cexpr2pres_charcount body))])])
 364         else (cexpr2pres t)
 365     | CE.Letrec (xref,defs,body) ->
 366         let attr = make_attributes ["helm:xref"] [xref] in
 367         let rec make_defs =
 368           (function
 369                [] -> assert false
 370              | [(n,bo)] ->
 371                  [P.Mtext([],(n ^ "="));(aux body)]
 372              | (n,bo)::tl ->
 373                  P.Mtext([],(n ^ "="))::
 374                  (aux body)::P.Mtext([]," and")::(make_defs tl)) in
 375         P.Mrow (attr,
 376           P.Mtext([],("let rec "))::
 377           (make_defs defs)@
 378           [P.Mtext([]," in ");
 379            (aux body)])
 380     | CE.Case (xref,a,np) ->
 381         let attr = make_attributes ["helm:xref"] [xref] in
 382         let rec make_patterns =
 383           (function
 384                [] -> []
 385              | [(n,p)] ->
 386                  [P.Mtext([],(n ^ " -> "));(aux p)]
 387              | (n,p)::tl ->
 388                  P.Mtext([],(n ^ " -> "))::
 389                  (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in
 390         P.Mrow (attr,
 391           P.Mtext([],("case "))::
 392           (aux a)::
 393           P.Mtext([],(" of "))::
 394           (make_patterns np)) in
 395   aux t
 396 ;;