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 floc ->
 104         let (n, m) = CicAst.loc_of_floc floc in
 105         (Some "helm","loc",(string_of_int n)^" "^(string_of_int m))
 106     | `IdRef s ->
 107         (Some "helm","xref",s)
 108 ;;
 109
 110 let map_attributes = List.map map_attribute
 111 ;;
 112 let resolve_binder = function
 113     `Lambda -> Box.Text([],"\\lambda")
 114   | `Pi -> Box.Text([],"\\Pi")
 115   | `Exists -> Box.Text([],"\\exists")
 116   | `Forall -> Box.Text([],"\\forall")
 117
 118 let rec ast2box ?(priority = 0) ?(assoc = false) ?(attr = []) t =
 119   if is_big t then
 120     bigast2box ~priority ~assoc ~attr t
 121   else Box.Object (map_attributes attr, t)
 122 and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
 123   function
 124       A.AttributedTerm (attr1, t) ->
 125         (* attr should be empty, since AtrtributedTerm are not
 126            supposed to be directly nested *)
 127         bigast2box ~priority ~assoc ~attr:(attr1::~attr) t
 128     | A.Appl l ->
 129         Box.H
 130           (map_attributes attr,
 131            [Box.Text([],"(");
 132             Box.V([],List.map ast2box l);
 133             Box.Text([],")")])
 134     | A.Binder (`Forall, (Cic.Anonymous, typ), body)
 135     | A.Binder (`Pi, (Cic.Anonymous, typ), body) ->
 136         Box.V(map_attributes attr,
 137               [Box.H([],[(match typ with
 138                          | None -> Box.Text([], "?")
 139                          | Some typ -> ast2box typ);
 140                          Box.smallskip;
 141                          Box.Text([], "\\to")]);
 142                Box.indent(ast2box body)])
 143     | A.Binder(kind, var, body) ->
 144         Box.V(map_attributes attr,
 145               [Box.H([],[resolve_binder kind;
 146                          Box.smallskip;
 147                          make_var var;
 148                          Box.Text([],".")]);
 149                Box.indent (ast2box body)])
 150     | A.Case(arg, _, ty, pl) ->
 151         let make_rule sep ((constr,vars),rhs) =
 152           if (is_big rhs) then
 153             Box.V([],[Box.H([],[Box.Text([],sep);
 154                                 Box.smallskip;
 155                                  make_pattern constr vars;
 156                                 Box.smallskip;
 157                                 Box.Text([],"\\Rightarrow")]);
 158                       Box.indent (bigast2box rhs)])
 159           else
 160             Box.H([],[Box.Text([],sep);
 161                       Box.smallskip;
 162                       make_pattern constr vars;
 163                       Box.smallskip;
 164                       Box.Text([],"\\Rightarrow");
 165                       Box.smallskip;
 166                       Box.Object([],rhs)]) in
 167         let plbox = match pl with
 168             [] -> Box.Text([],"[]")
 169           | r::tl ->
 170               Box.H([],
 171                     [Box.V([],
 172                            (make_rule "[" r)::(List.map (make_rule "|") tl));
 173                      Box.Text([],"]")]) in
 174         let ty_box =
 175           match ty with
 176           | Some ty ->
 177               [ Box.H([],[Box.Text([],"[");
 178                          ast2box ty;
 179                          Box.Text([],"]")]) ]
 180           | None -> []
 181         in
 182         if is_big arg then
 183           Box.V(map_attributes attr,
 184                  ty_box @
 185                  [Box.Text([],"match");
 186                  Box.H([],[Box.skip;
 187                            bigast2box arg;
 188                            Box.smallskip;
 189                            Box.Text([],"with")]);
 190                  plbox])
 191         else
 192           Box.V(map_attributes attr,
 193                 ty_box @
 194                 [Box.H(map_attributes attr,
 195                        [Box.Text([],"match");
 196                         Box.smallskip;
 197                         ast2box arg;
 198                         Box.smallskip;
 199                         Box.Text([],"with")]);
 200                  plbox])
 201     | A.LetIn (var, s, t) ->
 202         Box.V(map_attributes attr,
 203               (make_def "let" var s "in")@[ast2box t])
 204     | A.LetRec (_, vars, body) ->
 205         let definitions =
 206           let rec make_defs let_txt = function
 207               [] -> []
 208             | [(var,s,_)] ->
 209                 make_def let_txt var s "in"
 210             | (var,s,_)::tl ->
 211                 (make_def let_txt var s "")@(make_defs "and" tl) in
 212           make_defs "let rec" vars in
 213         Box.V(map_attributes attr,
 214               definitions@[ast2box body])
 215     | A.Ident (s, subst) ->
 216         let subst =
 217           let rec make_substs start_txt =
 218             function
 219               [] -> []
 220             | [(s,t)] ->
 221                 make_subst start_txt s t "]"
 222             | (s,t)::tl ->
 223                 (make_subst start_txt s t ";")@(make_substs " " tl)
 224           in
 225           match subst with
 226           | Some subst -> make_substs "\\subst [" subst
 227           | None -> []
 228         in
 229         Box.V([], (* attr here or on Vbox? *)
 230               [Box.Text(map_attributes attr,s);
 231                Box.indent(Box.V([],subst))])
 232     | A.Implicit ->
 233         Box.Text([],"_") (* big? *)
 234     | A.Meta (n, l) ->
 235         let local_context =
 236           List.map
 237             (function t ->
 238                Box.H([],[aux_option t; Box.Text([],";")]))
 239             l in
 240         Box.V(map_attributes attr,
 241               [Box.Text([],"?"^(string_of_int n));
 242                Box.H([],[Box.Text([],"[");
 243                          Box.V([],local_context);
 244                          Box.Text([],"]")])])
 245     | A.Num (s, _) ->
 246          Box.Text([],s)
 247     | A.Sort kind ->
 248         (match kind with
 249              `Prop -> Box.Text([],"Prop")
 250            | `Set -> Box.Text([],"Set")
 251            | `Type -> Box.Text([],"Type")
 252            | `CProp -> Box.Text([],"CProp"))
 253     | A.Symbol (s, _) ->
 254         Box.Text([],s)
 255
 256 and aux_option = function
 257     None  -> Box.Text([],"_")
 258   | Some ast -> ast2box ast
 259
 260 and make_var = function
 261     (Cic.Anonymous, None) -> Box.Text([],"_:_")
 262   | (Cic.Anonymous, Some t) ->
 263       Box.H([],[Box.Text([],"_:");ast2box t])
 264   | (Cic.Name s, None) -> Box.Text([],s)
 265   | (Cic.Name s, Some t) ->
 266       if is_big t then
 267         Box.V([],[Box.Text([],s^":");
 268                   Box.indent(bigast2box t)])
 269       else
 270         Box.H([],[Box.Text([],s^":");Box.Object([],t)])
 271
 272 and make_pattern constr =
 273   function
 274       [] -> Box.Text([],constr)
 275     | vars ->
 276         let bvars =
 277           List.fold_right
 278             (fun var acc ->
 279                let bv =
 280                  match var with
 281                      (* ignoring the type *)
 282                      (Cic.Anonymous, _) -> Box.Text([],"_")
 283                    | (Cic.Name s, _) -> Box.Text([],s) in
 284                  Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
 285           Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
 286
 287
 288 and make_def let_txt var def end_txt =
 289   let name =
 290     (match var with
 291          (* ignoring the type *)
 292          (Cic.Anonymous, _) -> Box.Text([],"_")
 293        | (Cic.Name s, _) -> Box.Text([],s)) in
 294   pretty_append
 295     [Box.Text([],let_txt);
 296      Box.smallskip;
 297      name;
 298      Box.smallskip;
 299      Box.Text([],"=")
 300     ]
 301     def
 302     [Box.smallskip;Box.Text([],end_txt)]
 303
 304 and make_subst start_txt varname body end_txt =
 305   pretty_append
 306     [Box.Text([],start_txt);
 307      Box.Text([],varname);
 308      Box.smallskip;
 309      Box.Text([],"\\Assign")
 310     ]
 311     body
 312     [Box.Text([],end_txt)]
 313
 314 and pretty_append l ast tail =
 315   prerr_endline("pretty riceve: " ^ (CicAstPp.pp_term ast));
 316   if is_big ast then
 317     [Box.H([],l);
 318      Box.H([],Box.skip::(bigast2box ast)::tail)]
 319   else
 320     [Box.H([],l@(Box.smallskip::(ast2box ast)::tail))]
 321
 322 ;;
 323
 324
 325
 326
 327