Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@cs.uidaho.edu, reetz@ira.uka.de
In-Reply-To: <4627.9405111736@frogland.inmos.co.uk> (message from David Shepherd on Wed, 11 May 1994 19:36:50 +0200)
Subject: Re: RE: does there exists a hol-lex?
Message-Id: <94May12.171206met_dst.8067@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 12 May 1994 17:12:04 +0200


David Shepherd writes

> I'm fairly certain that I talked to Konrad about this a few months ago
> and he said that there is a hook into the hol term pretty printer.  In
> this way you just write a pretty printer for terms of type :vhdl and
> add a function into this hook that calls this printer whenever it
> meets something of that type

Recently, Richard Boulton wrote and installed an extensible
prettyprinter for hol90. This is going to be included in the next
release; if there is enough interest in a patch for version 6, I can
emit one. The following is an edited version of the change log entry:

&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&
55. Richard Boulton has modified the prettyprinter so that it is extensible.

   The structure Extend_hol_pp in hol90 contains functions for incrementally
   extending the system pretty-printers for HOL types and terms, and for
   resetting them to their original state. 

   Considering terms (and by analogy, types), there are two functions: one to
   extend the printer; the other to reset it to the start-up state. Users can
   provide a pretty-printing function for whatever special features they 
   require. Such a function will be tried first on each call (top-level and 
   recursive) to the pretty-printer. If it fails for any reason, the original 
   printer is called (or the previously extended version of it).

   ...
  
   To extend the term prettyprinter, one would call 

      val extend_pp_term 
          : ((term_context -> Term.term -> PP.ppstream -> unit)
              -> (term_context -> Term.term -> PP.ppstream -> unit))
            -> unit

   where "term_context" is a type abbreviation:

       term_context = {boundvars: term list, depth:int, gravity:gravity}

   where, when the prettyprinter is at a subterm M, "boundvars" gives
   the scope of M, "depth" gives how far M is from the root of the
   original term (this is used for implementing ellipsis for large terms),
   and "gravity" gives the binding force of the context (this is used
   for minimizing brackets) 

  Example:

  The use of the extensibility functions is illustrated in the session
  below in which a function to print conditional expressions as "if
  ... then ... else ..."  instead of as "... => ... | ..." is
  installed. Note that the call to dest_cond fails if the term is not a
  conditional expression and so forces the original printer to be used.


   (* Define a new prettyprinter, just for conditionals *)
   - local
   =    open PP Extend_HOL_PP
   = in
   = fun pp_ite pp_tm {boundvars:term list,depth,gravity} tm ppstrm =
   =    if (depth = 0)
   =    then raise Fail "pp_ite"
   =    else let val {cond,larm,rarm} = dest_cond tm
   =             val parenth = gravity_geq gravity WEAK
   =             val params = {boundvars=boundvars,depth=depth-1,gravity=TOP}
   =         in  (if parenth then add_string ppstrm "(" else ();
   =              begin_block ppstrm CONSISTENT 0;
   =              add_string ppstrm "if ";
   =              (pp_tm params cond ppstrm : unit);
   =              add_break ppstrm (1,0);
   =              add_string ppstrm "then ";
   =              pp_tm params larm ppstrm;
   =              add_break ppstrm (1,0);
   =              add_string ppstrm "else ";
   =              pp_tm params rarm ppstrm;
   =              end_block ppstrm;
   =              if parenth then add_string ppstrm ")" else ())
   =         end
   = end;

   val pp_ite = fn : (term_context -> term -> ppstream -> unit)
                     -> (term_context -> term -> ppstream -> unit)

   (* Show original prettyprinter in action *)
   - val tm = (--`APPEND ((n = 0) => [] | [n]) [1;2;3]`--);
   val tm = (--`APPEND ((n = 0) => [] | [n]) [1; 2; 3]`--) : term

   (* Add the new prettyprinter *)
   - Extend_HOL_PP.extend_pp_term pp_ite;
   val it = () : unit

   (* Show the new prettyprinter *)
   - tm;
   val it = (--`APPEND (if (n = 0) then [] else [n]) [1; 2; 3]`--) : term

   (* Drop back *)
   - Extend_HOL_PP.reset_pp_term ();
   val it = () : unit

   - tm;
   val it = (--`APPEND ((n = 0) => [] | [n]) [1; 2; 3]`--) : term
   -