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

[Bill Richter <richter@math.northwestern.edu>]

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