Thanks, Mark! I see your include Format;; in printer.ml. By grepping, I see
occurrences of Format.print_string and Format.print_newline commands in e.g.
make.ml, but isn't the Format prefix here unnecessary, because they're
pervasive? Isn't that explained in section
20.2 Module Pervasives : The initially opened module.
of the ocaml reference manual, and p 318 for print_string and print_newline?
Your failwith idea sounds great, but I didn't understand it. As printer.ml
begins
(* Simplistic HOL Light prettyprinter, using the OCaml "Format" library. *)
I wonder if there's not a simple well-understood way to pretty-print error
messages. For instance, should all error messages be pretty-printed? If not,
do I really want to override the standard printer?
The OCaml developers want to keep these modules (by the way, it's
Obj not Object) low key and don't publish any details about them.
OCaml is used in the implementation of OCaml (!), and as I
understand it, they exist for this purpose.
That's amazing, Mark! I don't understand "low key" at all. It seem to me that
Toploop & Obj.magic recover much of the quote feature in Scheme, and that's a
very valuable feature. I grepped through your Tactician sources and I see a
lot, so I bet you understand this quite well:
(poisson)Tactician> grep Toploop *; grep Obj.magic *
autopromote.ml: let env = Obj.magic !Toploop.toplevel_env in
autopromote.ml: let env = Obj.magic !Toploop.toplevel_env in
mlconcrete.ml: (ignore o Toploop.execute_phrase false Format.std_formatter o
mlconcrete.ml: !Toploop.parse_toplevel_phrase o Lexing.from_string) x;;
prooftreefns.ml:let original_prompt_fn = !Toploop.read_interactive_input in
prooftreefns.ml:Toploop.read_interactive_input :=
termparser.ml: let env = Obj.magic !Toploop.toplevel_env in
autopromote.ml: let env = Obj.magic !Toploop.toplevel_env in
autopromote.ml: let env = Obj.magic !Toploop.toplevel_env in
handpromote.ml: [] -> let (atac',xs') = Obj.magic (atac,xs) in
handpromote.ml: then let (atac',xs') = Obj.magic (atac,xs) in
handpromote.ml: then let (atac',xs') = Obj.magic (atac,xs) in
handpromote.ml: then let (atac',xs') = Obj.magic (atac,xs) in
handpromote.ml: then let (atac',xs') = Obj.magic (atac,xs) in
handpromote.ml: [] -> let (atac',xs') = Obj.magic (atac,xs) in
handpromote.ml: then let (atac',xs') = Obj.magic (atac,xs) in
handpromote.ml: then let (atac',xs') = Obj.magic (atac,xs) in
handpromote.ml: then let (atac',xs') = Obj.magic (atac,xs) in
handpromote.ml: then let (atac',xs') = Obj.magic (atac,xs) in
mltypeguess.ml: then let (x':'a*'b) = Obj.magic x in
mltypeguess.ml: then Mint (Obj.magic x)
mltypeguess.ml: then Mstring (Obj.magic x)
mltypeguess.ml: then Mterm (Obj.magic x)
mltypeguess.ml: then Mtype (Obj.magic x)
termparser.ml: let env = Obj.magic !Toploop.toplevel_env in
Mark, please explain to me what Freek's doing in the code of his I borrowed in
RichterHilbertAxiomGeometry/readable.ml:
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 exec_thm_out = ref TRUTH;;
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;;
I bet you understand Lexing as well:
(poisson)Tactician> grep Lexing *
mlconcrete.ml: !Toploop.parse_toplevel_phrase o Lexing.from_string) x;;
So is_thm is a predicate run on a string which tells if that string is the name
of a theorem. I get the impression that Freek is running a command somewhere
that fails if the string isn't a theorem. So this Toploop and Lexing stuff
does two things:
1) it takes a string and turns it into a command and runs it, and
2) if it fails, it doesn't print an error message.
Can you explain any actual details?
BTW I looked at your HOL Zero page
http://www.proof-technologies.com/holzero/index.html, and remind me of
something I should know: Does your HOL Zero do type quantification?
--
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
