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