Thanks, Vince! Your is_thm works fine, but I get a warning when I try to
extend your idea:
let is_thm s =
try ignore (exec_thm s); true
with _ -> false;;
let is_tactic s =
try ignore (exec_tactic s); true
with _ -> false;;
let is_thmtactic s =
try ignore (exec_thmtactic s); true
with _ -> false;;
let is_thmlist_tactic s =
try ignore (exec_thmlist_tactic s); true
with _ -> false;;
val is_thm : string -> bool = <fun>
Characters 33-48:
try ignore (exec_tactic s); true
^^^^^^^^^^^^^^^
Warning 5: this function application is partial,
maybe some arguments are missing.
val is_tactic : string -> bool = <fun>
# Characters 35-53:
try ignore (exec_thmtactic s); true
^^^^^^^^^^^^^^^^^^
Warning 5: this function application is partial,
maybe some arguments are missing.
val is_thmtactic : string -> bool = <fun>
# Characters 40-63:
try ignore (exec_thmlist_tactic s); true
^^^^^^^^^^^^^^^^^^^^^^^
Warning 5: this function application is partial,
maybe some arguments are missing.
val is_thmlist_tactic : string -> bool = <fun>
The code works fine, though.
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.
Sure, but can you just look at my tactic and string-proof BNFs and make a
general suggestion about intermediate datatypes? I'm just not getting the
whole parser suite concept. And I think you understand parser.ml quite well.
Perhaps you can also make a suggestion about this code up top:
(* make_env and parse_env_string, following Mizarlight/miz2a.ml and Vince *)
(* Aravantinos's https://github.com/aravantv/HOL-Light-Q, turn a string to a *)
(* term with types inferred by the goal and assumption list. *)
let (make_env: goal -> (string * pretype) list) =
fun (asl,w) -> map ((fun (s,ty) -> s,pretype_of_type ty) o dest_var)
(freesl (w::(map (concl o snd) asl)));;
let parse_env_string env s = (term_of_preterm o retypecheck env)
((fst o parse_preterm o lex o explode) s);;
--
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
