Hi,
I have a pretty printer function added by using temp_add_user_printer.
It looks like the following:
--------------------------------------------------------------
fun pp_lins Gs sys (ppsFun:ppstream_funs) gravs d pps t : unit = let
val (label, code) = (dest_pair) t
val ins = code |> term_to_string
|> cached_add_comment
val str = #add_string ppsFun
in
str "(";
sys (Top, Top, Top) (d - 1) label;
str ",";
sys (Top, Top, Top) (d - 1) code;
str ins;
str ")";
()
end handle _ => raise term_pp_types.UserPP_Failed;
--------------------------------------------------------------
It works well in svn r8815. I checked out the latest version of HOL:
r9029, and it doesn't work any more. The error message is:
--------------------------------------------------------------
Function: temp_add_user_printer :
string * term * term_grammar.userprinter -> unit
Argument:
("pp_lins", (Parse.Term [QUOTE " (*#loc 565 59*)(l,i)"]), pp_lins) :
string * term *
(type_grammar.grammar * grammar ->
(grav * grav * grav -> int -> term -> 'a) ->
ppstream_funs -> 'b -> int -> 'c -> term -> unit)
Reason:
Can't unify
{name: string,
add_break: ppstream -> int * int -> unit,
end_block: ppstream -> unit,
end_style: ppstream -> unit,
add_string: ppstream -> string -> unit,
add_newline: ppstream -> unit,
add_xstring: ppstream -> xstring -> unit,
begin_block: ppstream -> break_style -> int -> unit,
begin_style: ppstream -> pp_style list -> unit} to
grav * grav * grav -> int -> term -> 'a (Incompatible types)
--------------------------------------------------------------
What is the easiest way to migrate to using the term_grammar.userprinter?
Also, how to remove a user-added-printer correspondingly? My current
method is the following, which I don't know if still works in the latest
HOL:
--------------------------------------------------------------
fun remove_pp_ Gs sys ppsFun gravs d pps t = raise
term_pp_types.UserPP_Failed;
temp_add_user_printer("pp_lins", ``(l,i)``, remove_pp_);
--------------------------------------------------------------
Thanks.
Lu
------------------------------------------------------------------------------
WhatsUp Gold - Download Free Network Management Software
The most intuitive, comprehensive, and cost-effective network
management toolset available today. Delivers lowest initial
acquisition cost and overall TCO of any competing solution.
http://p.sf.net/sfu/whatsupgold-sd
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
