I don't expect this in isolation will help, but the following HOL function causes the compiler to emit a
Fail "Exception- Option unexpectedly raised while compiling"
message.
?- - -
fun EXISTS_SEP_REWRITE_RULE rw th = let (* possibly fragile *)
val (p,q) = dest_eq (concl (SPEC_ALL rw))
val frame = genvar(type_of p)
val vs = list_dest dest_sep_exists p
val lhs = mk_star(last vs,frame)
val vs = butlast vs
fun find_exists_match lhs tm = let
val (v,t) = dest_sep_exists tm
val vs = list_dest dest_sep_exists tm
in (butlast vs,last vs,generic_star_match [] lhs (last vs)) end
fun find_term_and_apply f tm = f (find_term (can f) tm)
fun foo th = let
val (ws,tm,s) = find_term_and_apply (find_exists_match lhs) (concl th)
val (t,t2) = (dest_eq (concl (SPEC_ALL rw)))
val zs = list_dest dest_sep_exists t
val (zs,z) = (butlast zs,list_dest dest_star (last zs))
val xs = list_dest dest_star tm
val ys = filter (fn y => not (tmem y (map (subst s) z))) xs
val t3 = foldr mk_sep_exists (subst s (list_mk_star z (type_of frame))) (map (subst s) zs)
val goal = foldr mk_sep_exists (list_mk_star (t3::ys) (type_of frame)) ws
val goal = mk_eq(foldr mk_sep_exists tm ws,goal)
val lemma = auto_prove "EXISTS_SEP_REWRITE_RULE" (goal,
SIMP_TAC std_ss [GSYM rw]
THEN SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES]
THEN CONV_TAC (BINOP_CONV SEP_EXISTS_AC_CONV)
THEN SIMP_TAC (std_ss++star_ss) [AC CONJ_ASSOC CONJ_COMM])
val lemma = CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV [rw]
THENC SIMP_CONV std_ss [SEP_CLAUSES])) lemma
in foo (RW1 [lemma] th) end handle HOL_ERR _ => th
in foo th end;
- - -
This comes from HOL4's examples/machine-code/hoare-triple/helperLib.sml (line 667 onwards).
I will try to reduce it to a smaller instance.
Michael
