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 EA073820A1 for ; Wed, 21 Aug 2013 05:30:38 +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: AswAAM8zFFKBaVFEjWdsb2JhbABagzqDa7xCgSkWDgEBAQEJFgcYJIIlAQUjBAsBCjwQCQIaAgUhAgIPSAYOiBWHR5tIiTWBKYEpjnkzB4JogSwDiS2PZZNj X-IPAS-Result: AswAAM8zFFKBaVFEjWdsb2JhbABagzqDa7xCgSkWDgEBAQEJFgcYJIIlAQUjBAsBCjwQCQIaAgUhAgIPSAYOiBWHR5tIiTWBKYEpjnkzB4JogSwDiS2PZZNj X-IronPort-AV: E=Sophos;i="4.89,924,1367964000"; d="scan'208";a="24370875" Received: from levi.math.northwestern.edu ([129.105.81.68]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 21 Aug 2013 05:30:36 +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 r7L3UYsR029461 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Tue, 20 Aug 2013 22:30:34 -0500 Received: (from richter@localhost) by poisson.math.northwestern.edu (8.14.4/8.14.4/Submit) id r7L3UYxM006819; Tue, 20 Aug 2013 22:30:34 -0500 Date: Tue, 20 Aug 2013 22:30:34 -0500 Message-Id: <201308210330.r7L3UYxM006819@poisson.math.northwestern.edu> From: Bill Richter To: Goswin von Brederlow CC: caml-list@inria.fr In-reply-to: <20130820091631.GD3302@frosties> (message from Goswin von Brederlow on Tue, 20 Aug 2013 11:16:31 +0200) References: <201308120312.r7C3Cn35015470@poisson.math.northwestern.edu> <20130819155116.GA3104@frosties> <201308200318.r7K3Iw5t000609@poisson.math.northwestern.edu> <20130820091631.GD3302@frosties> MIME-version: 1.0 Content-type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] Obj.magic, Toploop, HOL Light & pretty-printing exceptions Thanks, Gerd! My `only remaining problem is' that I don't understand my own code, and I'm wondering if there's not a preferred ocaml way to accomplish the same thing. Allow me to explain what I'm trying to do, which is something like: 1) take a string which looks sort of like ocaml code, 2) use the Str module to rewrite the string into better ocaml code (actually HOL Light code) 3) execute the new string (incrementally in fact). Let me just show an example. First I'll show normal HOL Light code, and then a version that runs when I load my file readable.ml that uses the Toploop code I don't understand let exec = ignore o Toploop.execute_phrase false Format.std_formatter o !Toploop.parse_toplevel_phrase o Lexing.from_string;; The second version is basically the same proof, but it looks a lot more readable to me. let FourMovesToCorrectTwo = prove (`!A B C A' B' C'. ~collinear {A,B,C} /\ ~collinear {A',B',C'} ==> ? n. n < 5 /\ ? Y. reachableN (A,B,C) (A',B',Y) n \/ reachableN (A,B,C) (A',Y,C') n \/ reachableN (A,B,C) (Y,B',C') n`, INTRO_TAC "!A B C A' B' C'; H1" THEN SUBGOAL_TAC "H1'" `~collinear {B,C,(A:real^2)} /\ ~collinear{B',C',(A':real^2)} /\ ~collinear {C,A,B} /\ ~collinear {C',A',B'}` [HYP MESON_TAC "H1" [collinearSymmetry]] THEN SUBGOAL_TAC "easy_arith" `0 < 5 /\ 2 < 5 /\ 3 < 5 /\ 4 < 5` [ARITH_TAC] THEN cases "case01 | case2 | case3" `((A:real^2) = A' /\ (B:real^2) = B' /\ (C:real^2) = C' \/ A = A' /\ B = B' /\ ~(C = C') \/ A = A' /\ ~(B = B') /\ C = C' \/ ~(A = A') /\ B = B' /\ C = C') \/ (A = A' /\ ~(B = B') /\ ~(C = C') \/ ~(A = A') /\ B = B' /\ ~(C = C') \/ ~(A = A') /\ ~(B = B') /\ C = C') \/ ~(A = A') /\ ~(B = B') /\ ~(C = C')` [MESON_TAC []] THENL [so (HYP MESON_TAC "easy_arith" [reachableN_CLAUSES]); so (HYP MESON_TAC "H1 H1' easy_arith" [SameCdiffAB; reachableNSymmetry]); EXISTS_TAC `4` THEN HYP SIMP_TAC "easy_arith" [] THEN so (HYP MESON_TAC "H1 H1'" [DistinctImplies2moveable; FourStepMoveABBAreach; reachableNSymmetry; reachableN_Four])]);; let FourMovesToCorrectTwo = theorem `; ∀A B C A' B' C'. ¬collinear {A,B,C} ∧ ¬collinear {A',B',C'} ⇒ ∃ n. n < 5 ∧ ∃ Y. reachableN (A,B,C) (A',B',Y) n ∨ reachableN (A,B,C) (A',Y,C') n ∨ reachableN (A,B,C) (Y,B',C') n proof intro_TAC ∀A B C A' B' C', H1; ¬collinear {B,C,A} ∧ ¬collinear{B',C',A'} ∧ ¬collinear {C,A,B} ∧ ¬collinear {C',A',B'} [H1'] by fol H1 collinearSymmetry; 0 < 5 ∧ 2 < 5 ∧ 3 < 5 ∧ 4 < 5 [easy_arith] by ARITH_TAC; case_split case01 | case2 | case3 by fol; suppose A = A' ∧ B = B' ∧ C = C' ∨ A = A' ∧ B = B' ∧ ¬(C = C') ∨ A = A' ∧ ¬(B = B') ∧ C = C' ∨ ¬(A = A') ∧ B = B' ∧ C = C'; fol - easy_arith reachableN_CLAUSES; end; suppose A = A' ∧ ¬(B = B') ∧ ¬(C = C') ∨ ¬(A = A') ∧ B = B' ∧ ¬(C = C') ∨ ¬(A = A') ∧ ¬(B = B') ∧ C = C'; fol - H1 H1' easy_arith SameCdiffAB reachableNSymmetry; end; suppose ¬(A = A') ∧ ¬(B = B') ∧ ¬(C = C'); exists_TAC 4; SIMP_TAC easy_arith reachableN_CLAUSES; fol - H1 H1' DistinctImplies2moveable FourStepMoveABBAreach reachableNSymmetry reachableN_Four; end; qed; `;; Back to you: Am I right in that the executing itself works fine. So your only remaining problem is returning the result? Sorry, I didn't understand the question. I think that just doesn't work like you want. A function can only ever return exactly one type (or throw an exception). But the return type of eval would have to depend on the input. So I think you can't return the result. You can only pretty print it. Interesting. I don't use the function eval myself. But I might be wrong. I never used Toploop. Maybe it has something to return the result including some type encoding. Something like (but more complex): type result = Int of int | String of string That's interesting, I think you're explaining how the eval code works. Let me give you the entire fragment, from hol_light/update_database.ml (part of the HOL Light distribution, and not my code). Maybe you can tell me if a result is returned or just pretty printed: (* 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. *) (* ========================================================================= *) (* 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__");; (* Register all theorems added since the last update. *) exec ( "let update_database = let lastStamp = ref 0 and currentStamp = ref 0 and thms = Hashtbl.create 5000 in let ifNew f i x = if i.stamp > !lastStamp then ((if i.stamp > !currentStamp then currentStamp := i.stamp); f i x) in let rec regVal pfx = ifNew (fun i vd -> let n = pfx ^ i.name in if n <> \"buf__\" then (if get_simple_type vd.val_type.desc = Some \"thm\" then Hashtbl.replace thms n (eval n) else Hashtbl.remove thms n)) and regMod pfx = ifNew (fun i mt -> match mt with | Tmty_signature sg -> let pfx' = pfx ^ i.name ^ \".\" in List.iter (function | Tsig_value (i',vd) -> regVal pfx' i' vd | Tsig_module (i',mt',_) -> regMod pfx' i' mt' | _ -> ()) sg | _ -> ()) in fun () -> let env = Obj.magic !Toploop.toplevel_env in " ^ (if String.sub Sys.ocaml_version 0 1 = "4" then "iterTbl (fun i ((_,vd),_) -> regVal \"\" i vd) env.values; iterTbl (fun i ((_,mt),_) -> regMod \"\" i mt) env.modules; " else "iterTbl (fun i (_,vd) -> regVal \"\" i vd) env.values; iterTbl (fun i (_,mt) -> regMod \"\" i mt) env.modules; ") ^ " lastStamp := !currentStamp; theorems := Hashtbl.fold (fun s t l -> (s,t)::l) thms [];; ");;