helm/ocaml/cic_transformations/ast2pres.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 A = CicAst;;
  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 countvar current_size = function
  44     (Cic.Anonymous, None) -> current_size + 1 (* underscore *)
  45   | (Cic.Anonymous, Some ty) -> countterm current_size ty
  46   | (Cic.Name s, None) -> current_size + String.length s
  47   | (Cic.Name s, Some ty) -> current_size + countterm current_size ty
  48
  49 and countterm current_size t =
  50   if current_size > maxsize then current_size
  51   else match t with
  52       A.AttributedTerm (_,t) -> countterm current_size t
  53     | A.Appl l ->
  54         List.fold_left countterm current_size l
  55     | A.Binder (_,var,body) ->
  56         let varsize = countvar current_size var in
  57         countterm (varsize + 1) body (* binder *)
  58     | A.Case (arg, _, ty, pl) ->
  59         let size1 = countterm (current_size+10) arg in (* match with *)
  60         let size2 =
  61           match ty with
  62               None -> size1
  63             | Some ty -> countterm size1 ty in
  64         List.fold_left
  65           (fun c ((constr,vars),action) ->
  66              let size3 =
  67                List.fold_left countvar (c+String.length constr) vars in
  68              countterm size3 action) size2 pl
  69     | A.LetIn (var,s,t) ->
  70         let size1 = countvar current_size var in
  71         let size2 = countterm size1 s in
  72         countterm size2 t
  73     | A.LetRec (_,l,t) ->
  74         let size1 =
  75           List.fold_left
  76             (fun c (var,s,_) ->
  77                let size1 = countvar c var in
  78                countterm size1 s) current_size l in
  79           countterm size1 t
  80     | A.Ident(s,l) ->
  81         List.fold_left
  82           (fun c (v,t) -> countterm (c + (String.length v)) t)
  83           (current_size + (String.length s)) l
  84     | A.Implicit -> current_size + 1 (* underscore *)
  85     | A.Meta (_,l) ->
  86         List.fold_left
  87           (fun c t ->
  88              match t with
  89                  None -> c + 1 (* underscore *)
  90                | Some t -> countterm c t)
  91           (current_size + 1) l (* num *)
  92     | A.Num (s, _) -> current_size + String.length s
  93     | A.Sort _ -> current_size + 4 (* sort name *)
  94     | A.Symbol (s,_) -> current_size + String.length s
  95 ;;
  96
  97 let is_big t =
  98   ((countterm 0 t) > maxsize)
  99 ;;
 100
 101 let map_attribute =
 102   function
 103       `Loc (n,m) ->
 104         (Some "helm","loc",(string_of_int n)^" "^(string_of_int m))
 105     | `IdRef s ->
 106         (Some "helm","xref",s)
 107 ;;
 108
 109 let map_attributes = List.map map_attribute
 110 ;;
 111 let resolve_binder = function
 112     `Lambda -> Box.Text([],"\\lambda")
 113   | `Pi -> Box.Text([],"\\Pi")
 114   | `Exists -> Box.Text([],"\\exists")
 115   | `Forall -> Box.Text([],"\\forall")
 116
 117 let rec ast2box ?(priority = 0) ?(assoc = false) ?(attr = []) t =
 118   if is_big t then
 119     bigast2box ~priority ~assoc ~attr t
 120   else Box.Object (map_attributes attr, t)
 121 and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
 122   function
 123       A.AttributedTerm (attr1, t) ->
 124         (* attr should be empty, since AtrtributedTerm are not
 125            supposed to be directly nested *)
 126         bigast2box ~priority ~assoc ~attr:(attr1::~attr) t
 127     | A.Appl l ->
 128         Box.H
 129           (map_attributes attr,
 130            [Box.Text([],"(");
 131             Box.V([],List.map ast2box l);
 132             Box.Text([],")")])
 133     | A.Binder (`Forall, (Cic.Anonymous, typ), body)
 134     | A.Binder (`Pi, (Cic.Anonymous, typ), body) ->
 135         Box.V(map_attributes attr,
 136               [Box.H([],[(match typ with
 137                          | None -> Box.Text([], "?")
 138                          | Some typ -> ast2box typ);
 139                          Box.smallskip;
 140                          Box.Text([], "\\to")]);
 141                Box.indent(ast2box body)])
 142     | A.Binder(kind, var, body) ->
 143         Box.V(map_attributes attr,
 144               [Box.H([],[resolve_binder kind;
 145                          Box.smallskip;
 146                          make_var var;
 147                          Box.Text([],".")]);
 148                Box.indent (ast2box body)])
 149     | A.Case(arg, _, ty, pl) ->
 150         let make_rule sep ((constr,vars),rhs) =
 151           if (is_big rhs) then
 152             Box.V([],[Box.H([],[Box.Text([],sep);
 153                                 Box.smallskip;
 154                                 make_pattern constr vars;
 155                                 Box.smallskip;
 156                                 Box.Text([],"->")]);
 157                       Box.indent (bigast2box rhs)])
 158           else
 159             Box.H([],[Box.Text([],sep);
 160                       Box.smallskip;
 161                       make_pattern constr vars;
 162                       Box.smallskip;
 163                       Box.Text([],"->");
 164                       Box.smallskip;
 165                       Box.Object([],rhs)]) in
 166         let plbox = match pl with
 167             [] -> Box.Text([],"[]")
 168           | r::tl ->
 169               Box.H([],
 170                     [Box.V([],
 171                            (make_rule "[" r)::(List.map (make_rule "|") tl));
 172                      Box.Text([],"]")]) in
 173         let ty_box =
 174           match ty with
 175           | Some ty ->
 176               [ Box.H([],[Box.Text([],"[");
 177                          ast2box ty;
 178                          Box.Text([],"]")]) ]
 179           | None -> []
 180         in
 181         if is_big arg then
 182           Box.V(map_attributes attr,
 183                  ty_box @
 184                  [Box.Text([],"match");
 185                  Box.H([],[Box.skip;
 186                            bigast2box arg;
 187                            Box.smallskip;
 188                            Box.Text([],"with")]);
 189                  plbox])
 190         else
 191           Box.V(map_attributes attr,
 192                 ty_box @
 193                 [Box.H(map_attributes attr,
 194                        [Box.Text([],"match");
 195                         Box.smallskip;
 196                         ast2box arg;
 197                         Box.smallskip;
 198                         Box.Text([],"with")]);
 199                  plbox])
 200     | A.LetIn (var, s, t) ->
 201         Box.V(map_attributes attr,
 202               (make_def "let" var s "in")@[ast2box t])
 203     | A.LetRec (_, vars, body) ->
 204         let definitions =
 205           let rec make_defs let_txt = function
 206               [] -> []
 207             | [(var,s,_)] ->
 208                 make_def let_txt var s "in"
 209             | (var,s,_)::tl ->
 210                 (make_def let_txt var s "")@(make_defs "and" tl) in
 211           make_defs "let rec" vars in
 212         Box.V(map_attributes attr,
 213               definitions@[ast2box body])
 214     | A.Ident (s, subst) ->
 215         let subst =
 216           let rec make_substs start_txt =
 217             function
 218               [] -> []
 219             | [(s,t)] ->
 220                 make_subst start_txt s t "]"
 221             | (s,t)::tl ->
 222                 (make_subst start_txt s t ";")@(make_substs " " tl) in
 223           make_substs "[" subst in
 224         Box.V([], (* attr here or on Vbox? *)
 225               [Box.Text(map_attributes attr,s);
 226                Box.indent(Box.V([],subst))])
 227     | A.Implicit ->
 228         Box.Text([],"_") (* big? *)
 229     | A.Meta (n, l) ->
 230         let local_context =
 231           List.map
 232             (function t ->
 233                Box.H([],[aux_option t; Box.Text([],";")]))
 234             l in
 235         Box.V(map_attributes attr,
 236               [Box.Text([],"?"^(string_of_int n));
 237                Box.H([],[Box.Text([],"[");
 238                          Box.V([],local_context);
 239                          Box.Text([],"]")])])
 240     | A.Num (s, _) ->
 241          Box.Text([],s)
 242     | A.Sort kind ->
 243         (match kind with
 244              `Prop -> Box.Text([],"Prop")
 245            | `Set -> Box.Text([],"Set")
 246            | `Type -> Box.Text([],"Type")
 247            | `CProp -> Box.Text([],"CProp"))
 248     | A.Symbol (s, _) ->
 249         Box.Text([],s)
 250
 251 and aux_option = function
 252     None  -> Box.Text([],"_")
 253   | Some ast -> ast2box ast
 254
 255 and make_var = function
 256     (Cic.Anonymous, None) -> Box.Text([],"_:_")
 257   | (Cic.Anonymous, Some t) ->
 258       Box.H([],[Box.Text([],"_:");ast2box t])
 259   | (Cic.Name s, None) -> Box.Text([],s)
 260   | (Cic.Name s, Some t) ->
 261       if is_big t then
 262         Box.V([],[Box.Text([],s^":");
 263                   Box.indent(bigast2box t)])
 264       else
 265         Box.H([],[Box.Text([],s^":");Box.Object([],t)])
 266
 267 and make_pattern constr =
 268   function
 269       [] -> Box.Text([],constr)
 270     | vars ->
 271         let bvars =
 272           List.fold_right
 273             (fun var acc ->
 274                let bv =
 275                  match var with
 276                      (* ignoring the type *)
 277                      (Cic.Anonymous, _) -> Box.Text([],"_")
 278                    | (Cic.Name s, _) -> Box.Text([],s) in
 279                  Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
 280           Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
 281
 282
 283 and make_def let_txt var def end_txt =
 284   let name =
 285     (match var with
 286          (* ignoring the type *)
 287          (Cic.Anonymous, _) -> Box.Text([],"_")
 288        | (Cic.Name s, _) -> Box.Text([],s)) in
 289   pretty_append
 290     [Box.Text([],let_txt);
 291      Box.smallskip;
 292      name;
 293      Box.smallskip;
 294      Box.Text([],"=")
 295     ]
 296     def
 297     [Box.smallskip;Box.Text([],end_txt)]
 298
 299 and make_subst start_txt varname body end_txt =
 300   pretty_append
 301     [Box.Text([],start_txt);
 302      Box.Text([],varname);
 303      Box.smallskip;
 304      Box.Text([],":=")
 305     ]
 306     body
 307     [Box.Text([],end_txt)]
 308
 309 and pretty_append l ast tail =
 310   if is_big ast then
 311     [Box.H([],l);
 312      Box.H([],Box.skip::(bigast2box ast)::tail)]
 313   else
 314     [Box.H([],l@(Box.smallskip::(ast2box ast)::tail))]
 315
 316 ;;
 317
 318
 319
 320
 321