Mark, I now understand your  HOLZero/print_exn idea, and it works pretty well: 

exception Readable_fail of string;;
let PrintErrorFail s = raise(Readable_fail s);;
let print_exn e =
  match e with
  | Readable_fail s
       -> print_string s
  | _  -> print_string (Printexc.to_string e);;
#install_printer print_exn;;

Now PrintErrorFail gives me nice error messages, without double-quotes and with 
real newlines, e.g.

# Exception:
no matching right bracket operator \] to left bracket operator \[ in xyz
.
#                             Exception:
missing initial "proof" or final "qed;" in

  !m n. ~(n = 0)  ==>  ((m MOD n) MOD n = m MOD n)

  prooof
    intro_TAC !m n, H1;
    mp_TAC_specl [m; n; 1] MOD_MOD;
    fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC;
  qed;
.

So you were mostly right earlier:

   > and I thought the whole point of your post was that you weren't
   > happy with this pretty printing for Failure exceptions,

Yes!  But  I thought not, because I didn't understand that failwith just raises 
the exception Failure.  

   > and so I explained how to override it just for Failure exceptions

Yes, and that works great!  Thanks. 

   > and keep the pretty printer for all other exceptions exactly the
   > same.

But it's not exactly the same.  Run the eval code from 
http://caml.inria.fr/pub/docs/manual-ocaml/manual003.html#toc9 and you can then 
get

eval [("x", 1.0); ("y", 3.14)] (Prod(Sum(Var "z", Const 2.0), Var "y"));;

  Exception: Unbound_variable("z").

But normally this exception would be printed 

 Exception: Unbound_variable "z".

That's not a big difference, right?  But it's some change.  What really excites 
me is this: maybe you can generalize your print_exn to improve the 
pretty-printing of all HOL Light exception string error message.  

I looked through all your Tactician sources for uses of Toploop, Obj.magic and 
Lexing.  
Can you explain if this is a problem for Freek and I, from 
holzero-0.6.1/Bounty.txt:

    - circumventing the ML language proper or its type system (e.g. 
'Obj.magic');
      Carl Witty [16-09-2010]
         - for exposing how 'Obj.magic' can be used to create arbitrary theorems

It all looked interesting, such as this from termparser.ml, which looks like 
something that Freek posted he was interested in:

(* This file overwrites the existing HOL Light term parser with a version     *)
(* that stores the inputted quotation string in a dynamic lookup tree.  The   *)
(* idea is that this string can be looked up when the term gets pretty        *)
(* printed, so that it has all the type annotations of its original input.    *)
(* This gets around the fact that the HOL Light term pretty printer never     *)
(* annotates terms with their types, and so will often output ambiguous term  *)
(* quotations that do not get parsed back in correctly.                       *)

I saw you borrowed the update_database.ml `exec' in mlconcrete.ml, but I 
couldn't understand what you did with it.  Just take the first time you used 
`exec':

   exec
    ("type env_t = {
        values: (path_t * value_description) tbl;\n" ^
     (if (let v = String.sub Sys.ocaml_version 0 4 in v = "3.09" or v = "3.10")
        then ""
        else "  annotations: dummy;\n") ^
     "  constrs: dummy;
        labels: dummy;
        types: dummy;
        modules: (path_t * module_type) tbl;
        modtypes: dummy;
        components: dummy;
        classes: dummy;
        cltypes: dummy;
        summary: dummy};;");;

Can't you just evaluate this command yourself without `exec'?  At other times, 
it looked like you needed it, especially in autopromote.ml, where I think cmd 
is a string that you're getting from somewhere else:

   let rec promote_value0 verbose (name,t,vd) =
     match (promotion_command "" (name,vd)) with
       Some cmd -> if (t > !bulkpromoted_value_tstamp) &&
                      not (dltree_mem t !handpromoted_values)
                     then ((if verbose
                              then (print_string "Promoting value \"";
                                    print_string name;
                                    print_string "\"\n"));
                           exec cmd;
                           last_promoted_value := name)
     | _        -> ();;

-- 
Best,
Bill 

------------------------------------------------------------------------------
Get your SQL database under version control now!
Version control is standard for application code, but databases havent 
caught up. So what steps can you take to put your SQL databases under 
version control? Why should you start doing it? Read more to find out.
http://pubads.g.doubleclick.net/gampad/clk?id=49501711&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to