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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id F324C820A1 for ; Mon, 12 Aug 2013 05:12:53 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of richter@math.northwestern.edu) identity=pra; client-ip=129.105.81.68; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="richter@math.northwestern.edu"; x-sender="richter@math.northwestern.edu"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of richter@math.northwestern.edu designates 129.105.81.68 as permitted sender) identity=mailfrom; client-ip=129.105.81.68; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="richter@math.northwestern.edu"; x-sender="richter@math.northwestern.edu"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of postmaster@levi.math.northwestern.edu designates 129.105.81.68 as permitted sender) identity=helo; client-ip=129.105.81.68; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="richter@math.northwestern.edu"; x-sender="postmaster@levi.math.northwestern.edu"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhcBAFVSCFKBaVFEjWdsb2JhbABaFoMlrS4BkxEWDgEBAQEJFgcYJIJSREo0iHEMlWeXYogHkFiDewOJLY9jk14 X-IPAS-Result: AhcBAFVSCFKBaVFEjWdsb2JhbABaFoMlrS4BkxEWDgEBAQEJFgcYJIJSREo0iHEMlWeXYogHkFiDewOJLY9jk14 X-IronPort-AV: E=Sophos;i="4.89,859,1367964000"; d="scan'208";a="23736089" Received: from levi.math.northwestern.edu ([129.105.81.68]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 12 Aug 2013 05:12:52 +0200 Received: from poisson.math.northwestern.edu (poisson.math.northwestern.edu [129.105.81.230]) by levi.math.northwestern.edu (8.14.4/8.14.4) with ESMTP id r7C3CnYl014810 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Sun, 11 Aug 2013 22:12:50 -0500 Received: (from richter@localhost) by poisson.math.northwestern.edu (8.14.4/8.14.4/Submit) id r7C3Cn35015470; Sun, 11 Aug 2013 22:12:49 -0500 Date: Sun, 11 Aug 2013 22:12:49 -0500 Message-Id: <201308120312.r7C3Cn35015470@poisson.math.northwestern.edu> From: Bill Richter To: caml-list@inria.fr Subject: [Caml-list] Obj.magic, Toploop, HOL Light & pretty-printing exceptions 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. The file hol_light/update_database.ml begins (* ========================================================================= *) (* Create search database from OCaml / modify search database dynamically. *) (* *) (* This file assigns to "theorems", which is a list of name-theorem pairs. *) (* The core system already has such a database set up. Use this file if you *) (* want to update the database beyond the core, so you can search it. *) (* *) (* The trickery to get at the OCaml environment is due to Roland Zumkeller. *) (* It works by copying some internal data structures and casting into the *) (* copy using Obj.magic. *) (* ========================================================================= *) Here's another question about pretty-printing exception messages. This code from readable.ml, essentially due to Mark Adams, does a pretty good job printing my error messages: exception Readable_fail of string;; let printReadExn e = match e with | Readable_fail s -> print_string s | _ -> print_string (Printexc.to_string e);; #install_printer printReadExn;; But I know that with other exceptions, the behavior isn't quite identical to normal exception printing, as I would have preferred. A last question: I'm not sure I understood the indentation rules for multiple if/then/else explained in http://caml.inria.fr/resources/doc/guides/guidelines.en.html Maybe someone can look at the 97 lines of code in my readable.ml beginning with let rec StringToTactic s = -- Best, Bill