Mark, your update_database.ml idea worked great! My code simplified to
(* From update_database.ml: Execute any OCaml expression given as a string. *)
let exec = ignore o Toploop.execute_phrase false Format.std_formatter
o !Toploop.parse_toplevel_phrase o Lexing.from_string;;
(* exec and a reference idea from miz3.ml yield is_thm, a predicate asking *)
(* if a string represents a theorem, and exec_thm, which returns the thm. *)
let thm_ref = ref TRUTH;;
let is_thm s =
try exec ("thm_ref := ((" ^ s ^ "): thm);;"); true
with _ -> false;;
let exec_thm s =
try if (is_thm s) then !thm_ref else raise Noparse
with _ -> raise Noparse;;
I understand this much better than my old code, but I'd like to understand it
even better. I have many questions, and my most serious one is if you do
anything in your code like this from update_database.ml
(* Evaluate any OCaml expression given as a string. *)
let eval n =
exec ("let buf__ = ( " ^ n ^ " );;");
Obj.magic (Toploop.getvalue "buf__");;
I'd really like to understand this code in order to believe in exec. Following
some suggestions of Vince, I tried
((eval "EVEN"): thm);;
val it : thm = |- (EVEN 0 <=> T) /\ (!n. EVEN (SUC n) <=> ~EVEN n)
((eval "ARITH_TAC"): tactic);;
val it : tactic = <fun>
So that's fine, but now I get a segfault:
((eval "ARITH_TAC"): thm);;
Segmentation fault
You have mail in /var/spool/mail/richter
(poisson)hol_light>
John said he'd like to get eval to make a more graceful exit, but I think he
said I wasn't using eval as intended. Do you ever do anything like eval or
Freek's clever reference stunt above? Do you do something else to either check
the type of a string or to evaluate it?
Maybe you can help me with Freek's
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));;
The first part, as you say, is basically exec, but we see from his usage is
that the 2nd argument is a string that's supposed to be the empty string. Can
you say why that would be a useful check against errors?
You wrote about the update_database.ml function exec, which I'm now borrowing:
Roughly speaking it takes a string, turns it into lexical tokens,
turns this into abstract syntax and then executes it.
Lexing.from_string is a function of type
string -> lexbuf that's explained in the ocaml ref manual:
Create a lexer buffer which reads from the given string. Reading
starts from the first character in the string. An end-of-input
condition is generated when the end of the string is reached.
I'm not too clear on lexer buffers or even ocamllex. Is each character in my
string one of your tokens? Ocaml tells me that !Toploop.parse_toplevel_phrase
is a function of type
Lexing.lexbuf -> Parsetree.toplevel_phrase
That must be the undocumented function that "turns this into abstract syntax".
Ocaml also tells me that
Toploop.execute_phrase false Format.std_formatter is a function of type
Parsetree.toplevel_phrase -> bool
That be the undocumented function that "executes it." I get the impression
from Freek's miz3 code that we'll get True if the execution goes smoothly. Do
we get False if the execution raises an exception?
HOL Light's [...] got a snappy little lexer, implemented towards
the start of parser.ml.
Thanks! I didn't even realize that lexing and parsing were related. Vince
advised me to read parser.ml anyway.
Part of the point of HOL Zero is to have more explanation in the
source code, so that non-experts stand a chance of understanding
what's going on. Another is that quotation syntax is carefully
designed to avoid issues related to parser/printer
completeness/soundness, so that any valid HOL name can be parsed in
and unambiguously pretty printed. So the lexer, implemented in
lexer.ml, is more lengthy but is well commented.
This sounds fantastic! I will try to read it.
What about instead of printing out your failure message followed by
using fail(), just using failwith applied to a string argument that
is your failure message?
That's what the current version of RichterHilbertAxiomGeometry/readable.ml
does, and the error messages look terrible, like this one (with the misspelled
"proof"):
let MOD_MOD_REFL = theorem `;
∀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;
`;;
Exception:
Failure
"missing initial \"proof\" or final \"qed;\" in \n !m n. ~(n = 0) ==> ((m
MOD n) MOD n = m MOD n)\n\n prooof\n intro_TAC !m n, H1;\n mp_TAC_specl
[m; n; 1] MOD_MOD;\n fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC;\n qed;\n".
#
Here's the new beautiful error message:
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;
Exception: Failure "".
Yes, but 'print_string' and 'print_newline' are in *both* modules:
Pervasives and Format. All the other formatting stuff is not in
Pervasives.
But doesn't that mean there's no reason to write
'Format.print_string'? That 'print_string' is exactly the same function?
--
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
