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