Re: [Caml-list] Obj.magic, Toploop, HOL Light & pretty-printing exceptions

[Goswin von Brederlow <goswin-v-b@web.de>]

On Sun, Aug 11, 2013 at 10:12:49PM -0500, Bill Richter wrote:
> I'm an HOL Light programmer, and I'd like to understand Obj.magic and Toploop, which aren't explained in the ocaml doc http://caml.inria.fr/pub/docs/manual-ocaml-4.00/index.html.  I think Obj.magic and Toploop should be well explained, as they seem similar to the Scheme quote feature which allows one to write a Scheme->Scheme meta-interpreter.  That's the sort of thing I'm trying to do in
> hol_light/RichterHilbertAxiomGeometry/readable.ml
> included in the latest HOL Light subversion (see http://www.cl.cam.ac.uk/~jrh13/hol-light), which crucially use `exec' from 
> hol_light/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;;
> 
>    (* Evaluate any OCaml expression given as a string. *)
> 
>    let eval n =
>      exec ("let buf__ = ( " ^ n ^ " );;");
>      Obj.magic (Toploop.getvalue "buf__");;
> 
> BTW I got segfaults when I used `eval'.  I'd like to thank the expert HOL Light programmers who taught me, John Harrison, Freek Wiedijk (who wrote my model meta-interpreter hol_light/miz3/miz3.ml), Vince Aravantinos and Mark Adams, but I'd like to understand my own code better.  Mark explained everything I know about `exec', with:
> 
>    Roughly speaking it takes a string, turns it into lexical tokens,
>    turns this into abstract syntax and then executes it.

First: Obj.magic should not be used. It's not documented so you don't
get tempted to use it. Don't use it. [Well, unless you know what you
are doing and must.]

Obj.magic is a function 'a -> 'b that does absolutely nothing. It
simply makes the type inference belive that the type was converted
from 'a to 'b by some magic means. So unless you know what you are
doing this will cause a segfault the next time you use the 'b value.

In your case Toploop.getvalue will return 'a and the runtime will
blindly assume that has type 'b and use it as such. What 'b is depends
on what you do with the result of eval, e.g.:

# 1 + (eval "2 + 3");;

Here 'b is infered as int. That looks about right (which doesn't mean
it is).

But what about:

# 1 + (eval "2.0 +. 3.0");;

If Toploop.getvalue doesn't return an int (or other non-pointer type)
you suddenly add an integer and a pointer. Or in other words you
advanced the pointer by 2, which is right in the middle of a word and
will crash the GC.

The Obj.magic totaly breaks the type inference and only makes sense in
verry specific cases where you annotate the types carefully.

MfG
	Goswin