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.
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.
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.
--
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
