Hi Bill,
Le 2013-07-02 à 00:00, Bill Richter <rich...@math.northwestern.edu> a écrit :
> I hope folks can help me improve my code readable.ml, which in the new
> subversion 166 is in
> hol_light/RichterHilbertAxiomGeometry/
>
> 1) Can you pretty-print error messages in HOL Light? E.g. here:
>
> with Not_found -> failwith("missing initial \"proof\" or final \"qed;\" in "^
> s)
>
> It would be nice to at least have an actual newline before the string s.
Not to my knowledge.
>
> 2) Can I rewrite this function
> let is_thm s =
> try let thm = exec_thm s in true
> with _ -> false;;
>
> to not generate the error message "Warning 26: unused variable thm:" Of
> course, it's true, thm is never used. Maybe my real question is can someone
> explain the Toploop code for exec_thm I borrowed from miz3/miz3.ml.
How about:
let is_thm s =
try ignore (exec_thm s); true
with _ -> false;;
> 3) I wonder if I shouldn't be using the parser suite, as in parser.ml or
> miz3/miz3.ml. John gave me a very interesting response to this question
> earlier which I still haven't understood, but maybe I can ask the question
> more precisely now, using comment lines from the file (uncommented here
> below), which explains the BNF of both the tactics and string proofs allowed.
> The function StringToTactic is 105 lines long, using many helping functions,
> and violates the standard Ocaml indenting conventions, for otherwise the
> if/then/else/if/then/else.... would run off page. The question is whether I
> shouldn't be using the parser suite to have an intermediate data type between
> string proofs and tactics. Anyway, thanks to everyone for helping me,
> especially Vince and Freek.
I don't have the time to look at the details, but having an intermediate
datatype is very often a good idea in this context.
V.
>
> --
> Best,
> Bill
>
> StringToTactic uses regexp functions from the Str library to transform a
> string into a tactic. The allowable tactics can be written in BNF form
> as
> Tactic := ALL_TAC | Tactic THEN Tactic |
> one-word-tactic (e.g. ARITH_TAC) |
> one-word-thm_tactic one-word-thm (e.g. MATCH_MP_TAC num_WF) |
> one-word-thmlist_tactic listof(thm | label | - | --) |
> intro_TAC string | exists_TAC string | X_gen_TAC term |
> case_split string listof(statement) Tactic THENL listof(Tactic) |
> consider listof(variable) such that statement [label] Tactic |
> raa label statement Tactic | assume label statement Tactic |
> subgoal_TAC label statement Tactic
>
> The allowable string proofs which StringToTactic transforms into tactics
> can be written in BNF form as
>
> OneStepProof := one-word-tactic ";" (e.g. "ARITH_TAC;") |
> one-word-thm_tactic one-word-thm ";" (e.g. "MATCH_MP_TAC num_WF;") |
> one-word-thmlist_tactic concatenationof(thm | label | - | --) ";" |
> "intro_TAC" string ";" | "exists_TAC" term ";" | "X_gen_TAC" var ";"
>
> ByProofQed := "by" OneStepProof | "proof" Proof Proof ... Proof "qed;"
>
> Proof := "" | OneStepProof | Proof Proof |
> "consider" variable-list "such that" term [label] ByProofQed |
> "raa" statement [label] ByProofQed |
> "assume" statement [label] ByProofQed | statement [label] ByProofQed |
> "case_split" destruct ByProofQed
> "suppose" statement ";" Proof "end;" ...
> "suppose" statement ";" Proof "end;"
>
> ------------------------------------------------------------------------------
> This SF.net email is sponsored by Windows:
>
> Build for Windows Store.
>
> http://p.sf.net/sfu/windows-dev2dev
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
This SF.net email is sponsored by Windows:
Build for Windows Store.
http://p.sf.net/sfu/windows-dev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
