Vince, I figured out how to print error messages without double-quotes and with
actual newlines! This and a lot more is explained in the ocaml doc in "Module
Format", which I got the idea to use after looking at Freek's miz3.ml. I'd like
to get rid of a trailing message Exception: Failure "".
#load "str.cma";;
let StringRegexpEqual r s = Str.string_match r s 0 &&
s = Str.matched_string s;;
let rec FindMatch sleft sright s =
let test = Str.regexp ("\("^ sleft ^"\|"^ sright ^"\)") and
left = (Str.regexp sleft) in
let rec FindMatchPosition s count =
if count = 1 then 0 else
try
ignore(Str.search_forward test s 0);
let endpos = Str.match_end() in
let rest = Str.string_after s endpos and
increment =
if StringRegexpEqual left (Str.matched_group 1 s) then -1 else 1 in
endpos + (FindMatchPosition rest (count + increment))
with Not_found -> open_box 0; print_string
("\n no matching right bracket operator "^ sright ^
" to left bracket operator "^ sleft ^" in "^ s ^"\n");
close_box (); print_newline (); fail() in
FindMatchPosition s 0;;
let s = ";abc]edf" in Str.string_before s (FindMatch "\[" "\]" s);;
let s = ";1234[abc]]xyz" in Str.string_before s (FindMatch "\[" "\]" s);;
let s = ";12345[abc]lmnop]xyz" in Str.string_before s (FindMatch "\[" "\]" s);;
let s = ";123456[abc]lmnop[abc]pqrs]xyz" in Str.string_before s (FindMatch "\["
"\]" s);;
let s = ";123[45[abc]lm]nop!!!!!!!!!!]xyz" in Str.string_before s (FindMatch
"\[" "\]" s);;
let s = ";123456[abc]lmn[op[abc]pq]rs!!!!!!!!!!]xyz" in Str.string_before s
(FindMatch "\[" "\]" s);;
let s = ";123456[abc]lmn[op[abc]pq]rs!!!!!!!!!![]xyz" in Str.string_before s
(FindMatch "\[" "\]" s);;
Output:
val it : string = ";abc]"
# val it : string = ";1234[abc]]"
# val it : string = ";12345[abc]lmnop]"
# val it : string = ";123456[abc]lmnop[abc]pqrs]"
# val it : string = ";123[45[abc]lm]nop!!!!!!!!!!]"
# val it : string = ";123456[abc]lmn[op[abc]pq]rs!!!!!!!!!!]"
#
no matching right bracket operator \] to left bracket operator \[ in xyz
Exception: Failure "".
I'm responding to your post on Jul 2:
> 1) Can you pretty-print error messages in HOL Light? E.g. here:
>
> with Not_found -> failwith("missing initial \"proof\" or final \"qed;\" in
"^ s)
>
> It would be nice to at least have an actual newline before the string s.
Not to my knowledge.
Here's another example:
let rec FindSemicolon s =
try
let rec FindMatchPosition s pos =
let start = Str.search_forward (Str.regexp ";\|\[") s pos in
if Str.matched_string s = ";" then start
else
let rest = Str.string_after s (start + 1) in
let MatchingSquareBrace = FindMatch "\[" "\]" rest in
let newpos = start + 1 + MatchingSquareBrace in
FindMatchPosition s newpos in
FindMatchPosition s 0
with Not_found -> open_box 0; print_string
("\n no final semicolon in " ^ s ^"\n");
close_box (); print_newline (); fail();;
let s = "123456[abc]lmn[op[a; b; c]pq]rs!!!!!!!!!![];xyz" in Str.string_before
s (FindSemicolon s);;
let s = "123456[abc]lmn[op[a; b; c]pq]rs!!!!!!!!!![]xyz" in Str.string_before s
(FindSemicolon s);;
Output:
val it : string = "123456[abc]lmn[op[a; b; c]pq]rs!!!!!!!!!![]"
#
no final semicolon in 123456[abc]lmn[op[a; b; c]pq]rs!!!!!!!!!![]xyz
Exception: Failure "".
Thanks for writing you ZOL tutorial. I'll read it avidly.
--
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
