I learned a number of basic facts thinking about Vince and Freek's ideas, and
now I have no "unused variable" warnings in
RichterHilbertAxiomGeometry/readable.ml. I have some questions.
I reworked Freek's code to get eliminate the "unused variable" warning I was
getting with `is_thm':
let is_thm s =
try
let ok,rst = exec_phrase ("exec_thm_out := (("^s^") : thm);;") in
if not ok or rst <> "" then raise Noparse
else true
with _ -> false;;
let exec_thm s =
try if not (is_thm s) then raise Noparse else !exec_thm_out
with _ -> raise Noparse;;
Vince's ignore idea eliminates a different "unused variable" warning, in a
function with the line
let start = Str.search_forward test s 0 in
where start was never used. Here's the new code:
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 -> failwith("no matching right bracket operator "^ sright
^" to left bracket operator "^ sleft ^" in "^ s) in
FindMatchPosition s 0;;
I don't understand why this works. I thought all expressions in a sequence
(delimited by semicolons) must return values of the same type, and the `ignore'
expression returns (). However, I think the 2nd (long) expression in the
sequence returns a value of type num.
By studying Freek's code, I finally understood how to combine an if-test with
an exception-test. I had these lines in `StringToTactic':
if StringRegexpEqual (Str.regexp (ws0^ "\([^ \t\n]+\)" ^ws0)) step &&
is_tactic (Str.matched_group 1 step)
then
exec_tactic (Str.matched_group 1 step), rest
I eliminated the predicate `is_tactic', using Freek's trick:
try
if not (StringRegexpEqual (Str.regexp (ws0^ "\([^ \t\n]+\)" ^ws0)) step)
then raise Not_found
else exec_tactic (Str.matched_group 1 step), rest
with _ ->
And now I have no "unused variable" warnings!
Folks have posted here that there is no Ocaml function which returns the type
of an Ocaml object, even though `type_of' returns the type of an HOL Light
term, e.g.
type_of `\n. n + 1`;;
type_of `&1`;;
val it : hol_type = `:num->num`
# val it : hol_type = `:real`
But Freek's `exec_phrase' allows us to come reasonably close to this, defining
an Ocaml function is_type that detects if an Ocaml object, written as a string,
has a given type:
let exec_phrase s =
let lexbuf = Lexing.from_string s in
let ok = Toploop.execute_phrase false Format.std_formatter
(!Toploop.parse_toplevel_phrase lexbuf) in
Format.pp_print_flush Format.std_formatter ();
(ok,
let i = lexbuf.Lexing.lex_curr_pos in
String.sub lexbuf.Lexing.lex_buffer
i (lexbuf.Lexing.lex_buffer_len - i));;
let is_type s ty =
try
let ok,rst = exec_phrase ("(("^s^") : "^ ty ^");;") in
if not ok or rst <> "" then raise Noparse
else true
with _ -> false;;
is_type "LE_MULT2" "thm";;
is_type "SIMP_TAC" "thm";;
is_type "ARITH_TAC" "thm";;
is_type "MP_TAC" "thm";;
is_type "SIMP_TAC" "thm list -> tactic";;
is_type "ARITH_TAC" "tactic";;
is_type "MP_TAC" "thm_tactic";;
is_type correctly returns
val it : bool = true
# val it : bool = false
# val it : bool = false
# val it : bool = false
# val it : bool = true
# val it : bool = true
# val it : bool = true
I think I have to read
Chapter 12 of the Ocaml ref manual,
Lexer and parser generators
(ocamllex, ocamlyacc)
to understand of Freek's code. I don't see how to use is_type on HOL Light
terms, but maybe that's OK, because type_of, defined in term.ml, looks like it
uses a lot.
--
Best,
Bill
------------------------------------------------------------------------------
This SF.net email is sponsored by Windows:
Build for Windows Store.
http://p.sf.net/sfu/windows-dev2dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
