No, I'm afraid not. I will try to find some time to find a MWE this week.
Michael
?On 30/6/20, 02:54, "polyml on behalf of Phil Clayton" <polyml-bounces at inf.ed.ac.uk on behalf of phil.clayton at veonix.com> wrote:
I, too, am seeing this error message with the latest master (ef44a8b).
Michael - did you make any progress with this issue?
Phil
On 22/06/20 02:18, Norrish, Michael (Data61, Acton) wrote:
Sorry to spam (will take this elsewhere after this).
The "workaround" below doesn't help in the wider context. If I select all of the code without the enclosing
structure helperLib :> helperLib = struct ... end
it compiles without error, but if I have the enclosure, I again get the same Option error.
Michael
On 22/6/20, 11:08, "polyml on behalf of Norrish, Michael (Data61, Acton)" <polyml-bounces at inf.ed.ac.uk on behalf of Michael.Norrish at data61.csiro.au> wrote:
I get a workaround by lifting the definition of find_term_and_apply out to the top-level.
Michael
On 22/6/20, 10:54, "polyml on behalf of Norrish, Michael (Data61, Acton)" <polyml-bounces at inf.ed.ac.uk on behalf of Michael.Norrish at data61.csiro.au> wrote:
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
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml