Mark, I now understand your HOLZero/print_exn idea, and it works pretty well:
exception Readable_fail of string;;
let PrintErrorFail s = raise(Readable_fail s);;
let print_exn e =
match e with
| Readable_fail s
-> print_string s
| _ -> print_string (Printexc.to_string e);;
#install_printer print_exn;;
Now PrintErrorFail gives me nice error messages, without double-quotes and with
real newlines, e.g.
# Exception:
no matching right bracket operator \] to left bracket operator \[ in xyz
.
# Exception:
missing initial "proof" or final "qed;" in
!m n. ~(n = 0) ==> ((m MOD n) MOD n = m MOD n)
prooof
intro_TAC !m n, H1;
mp_TAC_specl [m; n; 1] MOD_MOD;
fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC;
qed;
.
So you were mostly right earlier:
> and I thought the whole point of your post was that you weren't
> happy with this pretty printing for Failure exceptions,
Yes! But I thought not, because I didn't understand that failwith just raises
the exception Failure.
> and so I explained how to override it just for Failure exceptions
Yes, and that works great! Thanks.
> and keep the pretty printer for all other exceptions exactly the
> same.
But it's not exactly the same. Run the eval code from
http://caml.inria.fr/pub/docs/manual-ocaml/manual003.html#toc9 and you can then
get
eval [("x", 1.0); ("y", 3.14)] (Prod(Sum(Var "z", Const 2.0), Var "y"));;
Exception: Unbound_variable("z").
But normally this exception would be printed
Exception: Unbound_variable "z".
That's not a big difference, right? But it's some change. What really excites
me is this: maybe you can generalize your print_exn to improve the
pretty-printing of all HOL Light exception string error message.
I looked through all your Tactician sources for uses of Toploop, Obj.magic and
Lexing.
Can you explain if this is a problem for Freek and I, from
holzero-0.6.1/Bounty.txt:
- circumventing the ML language proper or its type system (e.g.
'Obj.magic');
Carl Witty [16-09-2010]
- for exposing how 'Obj.magic' can be used to create arbitrary theorems
It all looked interesting, such as this from termparser.ml, which looks like
something that Freek posted he was interested in:
(* This file overwrites the existing HOL Light term parser with a version *)
(* that stores the inputted quotation string in a dynamic lookup tree. The *)
(* idea is that this string can be looked up when the term gets pretty *)
(* printed, so that it has all the type annotations of its original input. *)
(* This gets around the fact that the HOL Light term pretty printer never *)
(* annotates terms with their types, and so will often output ambiguous term *)
(* quotations that do not get parsed back in correctly. *)
I saw you borrowed the update_database.ml `exec' in mlconcrete.ml, but I
couldn't understand what you did with it. Just take the first time you used
`exec':
exec
("type env_t = {
values: (path_t * value_description) tbl;\n" ^
(if (let v = String.sub Sys.ocaml_version 0 4 in v = "3.09" or v = "3.10")
then ""
else " annotations: dummy;\n") ^
" constrs: dummy;
labels: dummy;
types: dummy;
modules: (path_t * module_type) tbl;
modtypes: dummy;
components: dummy;
classes: dummy;
cltypes: dummy;
summary: dummy};;");;
Can't you just evaluate this command yourself without `exec'? At other times,
it looked like you needed it, especially in autopromote.ml, where I think cmd
is a string that you're getting from somewhere else:
let rec promote_value0 verbose (name,t,vd) =
match (promotion_command "" (name,vd)) with
Some cmd -> if (t > !bulkpromoted_value_tstamp) &&
not (dltree_mem t !handpromoted_values)
then ((if verbose
then (print_string "Promoting value \"";
print_string name;
print_string "\"\n"));
exec cmd;
last_promoted_value := name)
| _ -> ();;
--
Best,
Bill
------------------------------------------------------------------------------
Get your SQL database under version control now!
Version control is standard for application code, but databases havent
caught up. So what steps can you take to put your SQL databases under
version control? Why should you start doing it? Read more to find out.
http://pubads.g.doubleclick.net/gampad/clk?id=49501711&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
