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

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

[Bill Richter]

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 

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

[Goswin von Brederlow]

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

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

[Bill Richter]

Goswin, thanks for the reply!  I'm not sure if I'm using Obj.magic (I'll study this question), and I couldn't tell if your prohibition of Obj.magic extends to Toploop.getvalue, which I definitely am using:

>    let exec = ignore o Toploop.execute_phrase false Format.std_formatter
>      o !Toploop.parse_toplevel_phrase o Lexing.from_string;;

Thanks for explaining why `eval' crashes the GC because of advanced pointers by 2. Perhaps I can draw you into what I think is the real discussion.  How does one complete the standard Scheme-type exercise of building an ocaml meta-interpreter inside ocaml?  You can do this easily in Scheme because of the quote feature.  What I and my teachers Freek, Mark and Vince are doing is, I think, trying to emulate the Scheme quote feature with Toploop & Obj.magic.  

-- 
Best,
Bill 

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

[Goswin von Brederlow]

On Mon, Aug 19, 2013 at 10:18:58PM -0500, Bill Richter wrote:
> Goswin, thanks for the reply!  I'm not sure if I'm using Obj.magic
> (I'll study this question), and I couldn't tell if your prohibition of
> Obj.magic extends to Toploop.getvalue, which I definitely am using:
> 
> >    let exec = ignore o Toploop.execute_phrase false Format.std_formatter
> >      o !Toploop.parse_toplevel_phrase o Lexing.from_string;;
> 
> Thanks for explaining why `eval' crashes the GC because of advanced
> pointers by 2. Perhaps I can draw you into what I think is the real
> discussion.  How does one complete the standard Scheme-type exercise
> of building an ocaml meta-interpreter inside ocaml?  You can do this
> easily in Scheme because of the quote feature.  What I and my teachers
> Freek, Mark and Vince are doing is, I think, trying to emulate the
> Scheme quote feature with Toploop & Obj.magic.  

Am I right in that the executing itself works fine. So your only remaining
problem is returning the result?

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.

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

MfG
	Goswin

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

[Bill Richter]

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 [];;
");;