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(kind, var, body) ->
 134         Box.V(map_attributes attr,
 135               [Box.H([],[resolve_binder kind;
 136                          Box.smallskip;
 137                          make_var var;
 138                          Box.Text([],".")]);
 139                Box.indent (ast2box body)])
 140     | A.Case(arg, _, ty, pl) ->
 141         let make_rule sep ((constr,vars),rhs) =
 142           if (is_big rhs) then
 143             Box.V([],[Box.H([],[Box.Text([],sep);
 144                                 Box.smallskip;
 145                                 make_pattern constr vars;
 146                                 Box.smallskip;
 147                                 Box.Text([],"->")]);
 148                       Box.indent (bigast2box rhs)])
 149           else
 150             Box.H([],[Box.Text([],sep);
 151                       Box.smallskip;
 152                       make_pattern constr vars;
 153                       Box.smallskip;
 154                       Box.Text([],"->");
 155                       Box.smallskip;
 156                       Box.Object([],rhs)]) in
 157         let plbox = match pl with
 158             [] -> Box.Text([],"[]")
 159           | r::tl ->
 160               Box.H([],
 161                     [Box.V([],
 162                            (make_rule "[" r)::(List.map (make_rule "|") tl));
 163                      Box.Text([],"]")]) in
 164         if is_big arg then
 165           Box.V(map_attributes attr,
 166                 [Box.Text([],"match");
 167                  Box.H([],[Box.skip;
 168                            bigast2box arg;
 169                            Box.smallskip;
 170                            Box.Text([],"with")]);
 171                  plbox])
 172         else
 173           Box.V(map_attributes attr,
 174                 [Box.H(map_attributes attr,
 175                        [Box.Text([],"match");
 176                         Box.smallskip;
 177                         ast2box arg;
 178                         Box.smallskip;
 179                         Box.Text([],"with")]);
 180                  plbox])
 181     | A.LetIn (var, s, t) ->
 182         Box.V(map_attributes attr,
 183               (make_def "let" var s "in")@[ast2box t])
 184     | A.LetRec (_, vars, body) ->
 185         let definitions =
 186           let rec make_defs let_txt = function
 187               [] -> []
 188             | [(var,s,_)] ->
 189                 make_def let_txt var s "in"
 190             | (var,s,_)::tl ->
 191                 (make_def let_txt var s "")@(make_defs "and" tl) in
 192           make_defs "let rec" vars in
 193         Box.V(map_attributes attr,
 194               definitions@[ast2box body])
 195     | A.Ident (s, subst) ->
 196         let subst =
 197           let rec make_substs start_txt =
 198             function
 199               [] -> []
 200             | [(s,t)] ->
 201                 make_subst start_txt s t "]"
 202             | (s,t)::tl ->
 203                 (make_subst start_txt s t ";")@(make_substs " " tl) in
 204           make_substs "[" subst in
 205         Box.V([], (* attr here or on Vbox? *)
 206               [Box.Text(map_attributes attr,s);
 207                Box.indent(Box.V([],subst))])
 208     | A.Implicit ->
 209         Box.Text([],"_") (* big? *)
 210     | A.Meta (n, l) ->
 211         let local_context =
 212           List.map
 213             (function t ->
 214                Box.H([],[aux_option t; Box.Text([],";")]))
 215             l in
 216         Box.V(map_attributes attr,
 217               [Box.Text([],"?"^(string_of_int n));
 218                Box.H([],[Box.Text([],"[");
 219                          Box.V([],local_context);
 220                          Box.Text([],"]")])])
 221     | A.Num (s, _) ->
 222          Box.Text([],s)
 223     | A.Sort kind ->
 224         (match kind with
 225              `Prop -> Box.Text([],"Prop")
 226            | `Set -> Box.Text([],"Set")
 227            | `Type -> Box.Text([],"Type")
 228            | `CProp -> Box.Text([],"CProp"))
 229     | A.Symbol (s, _) ->
 230         Box.Text([],s)
 231
 232 and aux_option = function
 233     None  -> Box.Text([],"_")
 234   | Some ast -> ast2box ast
 235
 236 and make_var = function
 237     (Cic.Anonymous, None) -> Box.Text([],"_:_")
 238   | (Cic.Anonymous, Some t) ->
 239       Box.H([],[Box.Text([],"_:");ast2box t])
 240   | (Cic.Name s, None) -> Box.Text([],s)
 241   | (Cic.Name s, Some t) ->
 242       if is_big t then
 243         Box.V([],[Box.Text([],s^":");
 244                   Box.indent(bigast2box t)])
 245       else
 246         Box.H([],[Box.Text([],s^":");Box.Object([],t)])
 247
 248 and make_pattern constr =
 249   function
 250       [] -> Box.Text([],constr)
 251     | vars ->
 252         let bvars =
 253           List.fold_right
 254             (fun var acc ->
 255                let bv =
 256                  match var with
 257                      (* ignoring the type *)
 258                      (Cic.Anonymous, _) -> Box.Text([],"_")
 259                    | (Cic.Name s, _) -> Box.Text([],s) in
 260                  Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
 261           Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
 262
 263
 264 and make_def let_txt var def end_txt =
 265   let name =
 266     (match var with
 267          (* ignoring the type *)
 268          (Cic.Anonymous, _) -> Box.Text([],"_")
 269        | (Cic.Name s, _) -> Box.Text([],s)) in
 270   pretty_append
 271     [Box.Text([],let_txt);
 272      Box.smallskip;
 273      name;
 274      Box.smallskip;
 275      Box.Text([],"=")
 276     ]
 277     def
 278     [Box.smallskip;Box.Text([],end_txt)]
 279
 280 and make_subst start_txt varname body end_txt =
 281   pretty_append
 282     [Box.Text([],start_txt);
 283      Box.Text([],varname);
 284      Box.smallskip;
 285      Box.Text([],":=")
 286     ]
 287     body
 288     [Box.Text([],end_txt)]
 289
 290 and pretty_append l ast tail =
 291   if is_big ast then
 292     [Box.H([],l);
 293      Box.H([],Box.skip::(bigast2box ast)::tail)]
 294   else
 295     [Box.H([],l@(Box.smallskip::(ast2box ast)::tail))]
 296
 297 ;;
 298
 299
 300
 301
 302