Thanks for the great response, John! I'm sorry it took me so long to respond,
and I still don't have a good response, but:
l think I see what you're saying about MP_TAC, MESON_TAC and FREEZE_THEN, and
I'll have to do more experiments.
I ought to learn how parse_preterm works, and I would if I really stared at
parser.ml. But I'm missing the point, I think. Let me explain my problem
thinking about my readable.ml. Here's more or less the BNF syntax for the
tactics proofs I'm accepting, modelled on Freek's miz3:
Proof := Tactic | Thm_Tactic Thm | Thm List -> Tactic listof {label | Thm} |
"intro_TAC" string |
"consider" listof {Var} "such that" statement [label] Proof |
"raa" statement [label] Proof | "assume" statement [label] Proof |
"proof" listof {Proof} "qed" |
"case_split DESTRUCT listof {statement} Proof
listof {"suppose" statement Proof "end"}
Now the syntax of the actual proofs (which are strings) are modelled on Freek's
miz3 syntax. So I have recursive functions which turn a long string proof into
a Proof as above. Well, I figure it would be simpler to have an intermediate
step which is a tree. In Scheme, which is untyped, I think I could easily do
that. But these trees I'd want to build are so un-homogeneous, that I think it
would be hard for me to define such trees or write a string_proof -> tree
function. Somehow I think that's the point of your parser suite, which Freek's
miz3 uses heavily, but I'm not getting it yet.
--
Best,
Bill
------------------------------------------------------------------------------
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
