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