Thanks, Mark! That sounds like a good tip, but can you be more specific? I
produce error message with this function
let PrintErrorFail s =
open_box 0; print_string s; close_box (); print_newline (); fail();;
BTW I do not understand why this works, why I don't have to say
Format.open_box and Format.close_box,
which would follow Freek's miz3.ml usage. I know print_string and
print_newline are pervasive, so you didn't need to write Format.print_string.
I use PrintErrorFail in the following way:
let mp_TAC_specl stermlist sthm gl =
try
let termlist = map (fun s -> parse_env_string (make_env gl) s) stermlist in
(MP_TAC o SPECL termlist) (exec_thm sthm) gl
with _ -> PrintErrorFail ("This is not an mp_TAC_specl expression:
mp_TAC_specl [" ^ (String.concat "; " stermlist) ^ "] "^ sthm ^"\n");;
Then I get this error message
# This is not an mp_TAC_specl expression:
mp_TAC_specl [m; n; 1] mod_mod
Exception: Failure "".
#
from this intentionally busted proof (mod_mod should be MOD_MOD)
let MOD_MOD_REFL = theorem `;
∀m n. ¬(n = 0) ⇒ ((m MOD n) MOD n = m MOD n)
proof
intro_TAC !m n, H1;
mp_TAC_specl [m; n; 1] mod_mod;
fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC;
qed;
`;;
Now I'd be happy if my error message was instead
Exception:
This is not an mp_TAC_specl expression:
mp_TAC_specl [m; n; 1] mod_mod
But I only want to change the OCaml exception printer for my function
PrintErrorFail.
BTW do you understand either of the undocumented Ocaml features that Freek
uses, Toploop or Object.magic? Is there an Ocaml list I ought to posting
questions on instead of hol-info?
--
Best,
Bill
------------------------------------------------------------------------------
See everything from the browser to the database with AppDynamics
Get end-to-end visibility with application monitoring from AppDynamics
Isolate bottlenecks and diagnose root cause in seconds.
Start your free trial of AppDynamics Pro today!
http://pubads.g.doubleclick.net/gampad/clk?id=48808831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
