From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 4BCDC820A1 for ; Mon, 19 Aug 2013 17:51:18 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=pra; client-ip=212.227.17.12; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=mailfrom; client-ip=212.227.17.12; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.web.de) identity=helo; client-ip=212.227.17.12; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="postmaster@mout.web.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AusBAL89ElLU4xEMm2dsb2JhbABaFoMmukaFO4EhFg4BAQEBAQYLCwkUKIIkAQEFJxMxHgsYCSUPBSiIMQEWCKx/H4kWkGcWgwV3A5djgS6EaY5d X-IPAS-Result: AusBAL89ElLU4xEMm2dsb2JhbABaFoMmukaFO4EhFg4BAQEBAQYLCwkUKIIkAQEFJxMxHgsYCSUPBSiIMQEWCKx/H4kWkGcWgwV3A5djgS6EaY5d X-IronPort-AV: E=Sophos;i="4.89,913,1367964000"; d="scan'208";a="29763502" Received: from mout.web.de ([212.227.17.12]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 19 Aug 2013 17:51:17 +0200 Received: from frosties.localnet ([95.208.119.3]) by smtp.web.de (mrweb001) with ESMTPSA (Nemesis) id 0MNLAn-1V9UrM0y4n-006sXv for ; Mon, 19 Aug 2013 17:51:17 +0200 Received: from mrvn by frosties.localnet with local (Exim 4.80) (envelope-from ) id 1VBRjg-0002Ae-G0 for caml-list@inria.fr; Mon, 19 Aug 2013 17:51:16 +0200 Date: Mon, 19 Aug 2013 17:51:16 +0200 From: Goswin von Brederlow To: caml-list@inria.fr Message-ID: <20130819155116.GA3104@frosties> References: <201308120312.r7C3Cn35015470@poisson.math.northwestern.edu> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <201308120312.r7C3Cn35015470@poisson.math.northwestern.edu> User-Agent: Mutt/1.5.21 (2010-09-15) X-Provags-ID: V03:K0:SPPzFwE46AF9DYkvqOP43aG+JHO5S5k6qLTAnx2mdC/P6X9gObt xVPnqv9mn4IEnaQNDjif2jwn3BJ20MDzH8kBFt9htpFUKuJPlLwY9Avp78XqZ0/8MysKHfT +5MivSEDMzoBchVl/0wf6ail/l2PdS48EOk88pxq8/sO9uzn0bemSnoL4jM4r2l166QpcAR 3rdXnZ8Hm56rqoByPIhQw== Subject: Re: [Caml-list] Obj.magic, Toploop, HOL Light & pretty-printing exceptions 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