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 make_math_tail = List.map (fun s -> P.Mtext ([], s))
 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)::(make_math_tail 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([],"]")::(make_math_tail 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)::(make_math_tail 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 ([],"]")] @ (make_math_tail 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)::(make_math_tail 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([],")")::(make_math_tail 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([],")")::(make_math_tail 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)::(make_math_tail 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)::(make_math_tail 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)::(make_math_tail 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)] -> make_pattern n p
 222              | (n,p)::tl ->
 223                  (make_pattern n p)@(P.smallskip::
 224                  P.Mtext([],"|")::P.smallskip::(make_patterns tl)))
 225         and make_pattern n p =
 226           let rec get_vars_and_body =
 227             (function
 228                 CE.Binder (_, "Lambda",(n,_),body) ->
 229                   let v,b = get_vars_and_body body in
 230                   n::v,b
 231               | t -> [],t) in
 232           let vars,body = get_vars_and_body p in
 233           let lhs =
 234             match vars with
 235                 [] -> n ^ " -> "
 236               | l -> "(" ^ n ^" "^(String.concat " " l) ^ ")" ^ " -> " in
 237           [P.Mtext([],lhs);P.smallskip;aux body] in
 238         P.Mrow (attr,
 239           P.Mtext([],"match")::P.smallskip::
 240           (aux a)::P.smallskip::
 241           P.Mtext([],"with")::P.smallskip::
 242           P.Mtext([],"[")::P.smallskip::
 243           (make_patterns np)@(P.smallskip::P.Mtext([],("]"))::(make_math_tail tail)))  in
 244   aux t
 245
 246 and
 247
 248 make_args ?(priority = 0) ?(assoc = false) ?(tail = []) =
 249   function
 250       [] -> List.map (fun s -> P.Mtext ([], s)) tail
 251     | a::tl -> P.smallskip::(cexpr2pres a)::(make_args ~tail:tail tl)
 252 ;;
 253
 254 let make_box_tail = List.map (Box.b_text [])
 255 ;;
 256
 257 let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) =
 258   function
 259     [] -> []
 260   | [a] -> [Box.indent (cexpr2pres_charcount ~tail:tail a)]
 261   | (a::tl) as l ->
 262       let c = List.fold_left countterm 0 l in
 263       if c > maxsize then
 264         (Box.indent (cexpr2pres_charcount a))::
 265         (make_args_charcount ~tail:tail tl)
 266       else
 267         [Box.indent (Box.b_object (P.Mrow ([], (make_args ~tail:tail l))))]
 268
 269 (*
 270   function
 271       [] -> []
 272     | a::tl ->
 273         let tlpres =
 274           let c = List.fold_left countterm 0 tl in
 275           if c > maxsize then
 276             P.Mtable ([("align","baseline 1");("equalrows","false");
 277              ("columnalign","left")],
 278               (make_args_charcount tl))
 279           else
 280             P.Mrow([], make_args tl) in
 281         [P.Mtr([],[P.Mtd([],(cexpr2pres_charcount a))]);
 282          P.Mtr([],[P.Mtd([],P.indented tlpres)])] *)
 283 and
 284
 285 cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
 286   if not (is_big t) then
 287     Box.b_object (cexpr2pres ~priority ~assoc ~tail t)
 288   else let aux = cexpr2pres_charcount in
 289   match t with
 290       CE.Symbol (xref,name,None,uri) ->
 291         let attr =
 292          make_attributes
 293           [Some "helm","xref";Some "xlink","href"] [xref;uri] in
 294         if tail = [] then
 295           Box.b_object (P.Mi (attr,name))
 296         else
 297           Box.b_h [] (Box.b_object (P.Mi (attr,name)) :: (make_box_tail tail))
 298     | CE.Symbol (xref,name,Some subst,uri) ->
 299         let attr =
 300          make_attributes
 301           [Some "helm","xref";Some "xlink","href"] [xref;uri] in
 302         let rec make_subst =
 303           (function
 304                [] -> assert false
 305              | [(uri,a)] ->
 306                  [Box.b_object (cexpr2pres a);
 307                   Box.b_text [] "/";
 308                   Box.b_object (P.Mi([],UriManager.name_of_uri uri))]
 309              | (uri,a)::tl ->
 310                  Box.b_object (cexpr2pres a) ::
 311                  Box.b_text [] "/" ::
 312                  Box.b_object (P.Mi([],UriManager.name_of_uri uri)) ::
 313                  Box.b_text [] "; " ::
 314                  Box.smallskip ::
 315                  (make_subst tl)) in
 316         Box.b_h [] (
 317           Box.b_object (P.Mi (attr,name))::
 318           Box.b_text [] "["::
 319           (make_subst subst)@
 320           (Box.b_text [] "]")::(make_box_tail tail) )
 321     | CE.LocalVar (xref,name) ->
 322         let attr = make_attributes [Some "helm","xref"] [xref] in
 323         if tail = [] then
 324           Box.b_object (P.Mi (attr,name))
 325         else
 326           Box.b_object (P.Mrow ([], P.Mi (attr,name)::(make_math_tail tail)))
 327     | CE.Meta (xref,name,l) ->
 328         let attr = make_attributes [Some "helm","xref"] [xref] in
 329         let l' =
 330          List.map
 331           (function
 332               None -> P.Mo([],"_")
 333             | Some t -> cexpr2pres t
 334           ) l
 335         in
 336         Box.b_object (P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ (make_math_tail tail)))
 337     | CE.Num (xref,value) ->
 338         let attr = make_attributes [Some "helm","xref"] [xref] in
 339         if tail = [] then
 340           Box.b_object (P.Mn (attr,value))
 341         else
 342           Box.b_object (P.Mrow ([], P.Mn (attr,value)::(make_math_tail tail)))
 343     | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
 344         let aattr = make_attributes [Some "helm","xref"] [axref] in
 345         let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
 346         (try
 347           (let f = Hashtbl.find symbol_table_charcount n in
 348            f tl ~priority ~assoc ~tail aattr sattr)
 349          with notfound ->
 350           Box.b_v aattr (
 351             Box.b_h [] [
 352               Box.b_text [] "(";
 353               Box.b_object (cexpr2pres (CE.Symbol(sxref,n,subst,uri)))
 354             ] ::
 355             make_args_charcount ~tail:(")"::tail) tl
 356           ))
 357     | CE.Appl (xref,l) as t ->
 358         let attr = make_attributes [Some "helm","xref"] [xref] in
 359         Box.b_v attr (
 360           Box.b_h [] [
 361             Box.b_text [] "(";
 362             cexpr2pres_charcount (List.hd l)
 363           ] ::
 364           make_args_charcount ~tail:(")"::tail) (List.tl l)
 365         )
 366     | CE.Binder (xref, kind,(n,s),body) as t ->
 367         let attr = make_attributes [Some "helm","xref"] [xref] in
 368         let binder =
 369           if kind = "Lambda" then
 370             Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
 371           else if kind = "Prod" then
 372             Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
 373           else if kind = "Forall" then
 374             Netconversion.ustring_of_uchar `Enc_utf8 0x2200
 375           else if kind = "Exists" then
 376             Netconversion.ustring_of_uchar `Enc_utf8 0x2203
 377           else "unknown" in
 378         Box.b_v attr [
 379           Box.b_h [] [
 380             Box.b_text [None,"color","blue"] binder;
 381             Box.b_text [] (n ^ ":");
 382             cexpr2pres_charcount s ~tail:["."]
 383           ];
 384           Box.b_h [] [ Box.indent (cexpr2pres_charcount body ~tail:tail) ]
 385         ]
 386     | CE.Letin (xref,(n,s),body) as t ->
 387         let attr = make_attributes [Some "helm","xref"] [xref] in
 388         Box.b_v attr [
 389           Box.b_h [] [
 390             Box.b_kw "let";
 391             Box.smallskip;
 392             Box.b_text [] (n ^ "=");
 393             cexpr2pres_charcount s;
 394             Box.smallskip;
 395             Box.b_kw "in"
 396           ];
 397           Box.indent (cexpr2pres_charcount body)
 398         ]
 399     | CE.Letrec (xref,defs,body) ->
 400         let attr = make_attributes [Some "helm","xref"] [xref] in
 401         let rec make_defs =
 402           (function
 403                [] -> assert false
 404              | [(n,bo)] ->
 405                  [Box.b_text [] (n ^ "="); (aux body)]
 406              | (n,bo)::tl ->
 407                  Box.b_text [] (n ^ "=")::
 408                  (aux body)::
 409                  Box.smallskip::
 410                  Box.b_kw "and"::
 411                  (make_defs tl)) in
 412         Box.b_h attr (
 413           Box.b_kw "let" ::
 414           Box.smallskip ::
 415           Box.b_kw "rec" ::
 416           Box.smallskip ::
 417           make_defs defs @
 418           [ Box.smallskip; Box.b_kw "in"; Box.smallskip; aux body ]
 419         )
 420     | CE.Case (xref,a,np) ->
 421         let attr = make_attributes [Some "helm","xref"] [xref] in
 422         let arg =
 423           if (is_big a) then
 424             let tail = " with"::tail in (* LUCA: porcheria all'ennesima potenza, TODO ripensare il meccanismo del tail *)
 425             [ Box.b_h [] [ Box.b_kw "match"; Box.smallskip ];
 426               aux a ~tail
 427             ]
 428           else
 429             [ Box.b_h [] [
 430                 Box.b_kw "match";
 431                 Box.smallskip;
 432                 aux a ~tail;
 433                 Box.smallskip;
 434                 Box.b_kw "with"
 435               ]
 436             ] in
 437         let rec make_patterns is_first ~tail =
 438           function
 439               [] -> []
 440             | [(n,p)] ->
 441                 let sep = if is_first then "[ " else "| " in
 442                 [ Box.b_h [] [make_pattern sep ~tail n p] ]
 443             | (n,p)::tl ->
 444                 let sep =
 445                   if is_first then "[ " else "| " in
 446                 [ Box.b_h [] ((make_pattern sep [] n p) :: (make_patterns false ~tail  tl)) ]
 447         and make_pattern sep ~tail n p =
 448           let rec get_vars_and_body =
 449             function
 450                 CE.Binder (_, "Lambda",(n,_),body) ->
 451                   let v,b = get_vars_and_body body in
 452                   n::v,b
 453               | t -> [],t in
 454           let vars,body = get_vars_and_body p in
 455           let lhs =
 456             match vars with
 457                 [] -> sep ^ n ^ " -> "
 458               | l -> sep ^"(" ^n^" "^(String.concat " " l) ^ ")" ^ " -> " in
 459           if (is_big body) then
 460             Box.b_v [] [
 461               Box.b_text [] lhs;
 462               Box.indent (aux ~tail body)
 463             ]
 464           else
 465             Box.b_h [] [ Box.b_text [] lhs; aux ~tail body ]
 466           in
 467         let patterns =
 468           make_patterns true np ~tail:("]"::tail) in
 469         Box.b_v attr (arg@patterns)
 470 ;;
 471
 472
 473