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" <[email protected] on behalf of [email protected]> 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)" > <[email protected] on behalf of [email protected]> > 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)" > <[email protected] on behalf of [email protected]> > 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 > [email protected] > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > > _______________________________________________ > polyml mailing list > [email protected] > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > > _______________________________________________ > polyml mailing list > [email protected] > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
