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,None) -> current_size + (String.length s)
  80     | A.Ident(s,Some 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([],"\Rightarrow")]);
 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([],"\Rightarrow");
 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)
 223           in
 224           match subst with
 225           | Some subst -> make_substs "\\subst [" subst
 226           | None -> []
 227         in
 228         Box.V([], (* attr here or on Vbox? *)
 229               [Box.Text(map_attributes attr,s);
 230                Box.indent(Box.V([],subst))])
 231     | A.Implicit ->
 232         Box.Text([],"_") (* big? *)
 233     | A.Meta (n, l) ->
 234         let local_context =
 235           List.map
 236             (function t ->
 237                Box.H([],[aux_option t; Box.Text([],";")]))
 238             l in
 239         Box.V(map_attributes attr,
 240               [Box.Text([],"?"^(string_of_int n));
 241                Box.H([],[Box.Text([],"[");
 242                          Box.V([],local_context);
 243                          Box.Text([],"]")])])
 244     | A.Num (s, _) ->
 245          Box.Text([],s)
 246     | A.Sort kind ->
 247         (match kind with
 248              `Prop -> Box.Text([],"Prop")
 249            | `Set -> Box.Text([],"Set")
 250            | `Type -> Box.Text([],"Type")
 251            | `CProp -> Box.Text([],"CProp"))
 252     | A.Symbol (s, _) ->
 253         Box.Text([],s)
 254
 255 and aux_option = function
 256     None  -> Box.Text([],"_")
 257   | Some ast -> ast2box ast
 258
 259 and make_var = function
 260     (Cic.Anonymous, None) -> Box.Text([],"_:_")
 261   | (Cic.Anonymous, Some t) ->
 262       Box.H([],[Box.Text([],"_:");ast2box t])
 263   | (Cic.Name s, None) -> Box.Text([],s)
 264   | (Cic.Name s, Some t) ->
 265       if is_big t then
 266         Box.V([],[Box.Text([],s^":");
 267                   Box.indent(bigast2box t)])
 268       else
 269         Box.H([],[Box.Text([],s^":");Box.Object([],t)])
 270
 271 and make_pattern constr =
 272   function
 273       [] -> Box.Text([],constr)
 274     | vars ->
 275         let bvars =
 276           List.fold_right
 277             (fun var acc ->
 278                let bv =
 279                  match var with
 280                      (* ignoring the type *)
 281                      (Cic.Anonymous, _) -> Box.Text([],"_")
 282                    | (Cic.Name s, _) -> Box.Text([],s) in
 283                  Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
 284           Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
 285
 286
 287 and make_def let_txt var def end_txt =
 288   let name =
 289     (match var with
 290          (* ignoring the type *)
 291          (Cic.Anonymous, _) -> Box.Text([],"_")
 292        | (Cic.Name s, _) -> Box.Text([],s)) in
 293   pretty_append
 294     [Box.Text([],let_txt);
 295      Box.smallskip;
 296      name;
 297      Box.smallskip;
 298      Box.Text([],"=")
 299     ]
 300     def
 301     [Box.smallskip;Box.Text([],end_txt)]
 302
 303 and make_subst start_txt varname body end_txt =
 304   pretty_append
 305     [Box.Text([],start_txt);
 306      Box.Text([],varname);
 307      Box.smallskip;
 308      Box.Text([],"\Assign")
 309     ]
 310     body
 311     [Box.Text([],end_txt)]
 312
 313 and pretty_append l ast tail =
 314   prerr_endline("pretty riceve: " ^ (CicAstPp.pp_term ast));
 315   if is_big ast then
 316     [Box.H([],l);
 317      Box.H([],Box.skip::(bigast2box ast)::tail)]
 318   else
 319     [Box.H([],l@(Box.smallskip::(ast2box ast)::tail))]
 320
 321 ;;
 322
 323
 324
 325
 326