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
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
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
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
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
I managed to produce a smallish example fairly quickly as the code causing it didn't have many dependencies. I have raised https://github.com/polyml/polyml/issues/136
Phil
On 30/06/20 00:14, Norrish, Michael (Data61, Acton) wrote:
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 ... endit 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
Thanks for producing this example. I've investigated it and the current master ( fb10196 ) includes a fix.
This turned out to be more complicated than expected. Earlier in the year Makarius reported a segfault in some generated code and produced a cut down example. Reverting a change (19d82db) seemed to fix the problem but the reversion appears to have introduced the Option exception that you found. I've now looked again and both the segfault bug and the Option exception bug are unrelated to the changes. It's just that these changes either revealed or masked the underlying bugs by altering the intermediate code.
The current master should have proper fixes for both the bugs. Makarius: Could you check that you don't get the segfault in the generated code with the current master. It works correctly with my cut down version of your cut down version.
David
On 30/06/2020 18:01, Phil Clayton wrote:
I managed to produce a smallish example fairly quickly as the code causing it didn't have many dependencies.? I have raised https://github.com/polyml/polyml/issues/136
Phil
On 30/06/20 00:14, Norrish, Michael (Data61, Acton) wrote:
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
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On 07/07/2020 08:41, David Matthews wrote:
Thanks for producing this example.? I've investigated it and the current master ( fb10196 ) includes a fix.
The current master should have proper fixes for both the bugs. Makarius: Could you check that you don't get the segfault in the generated code with the current master.? It works correctly with my cut down version of your cut down version.
It looks fine so far with Isabelle + AFP. The example causing the crash also works.
That Poly/ML version is officially used/tested here https://isabelle-dev.sketis.net/rISABELLEa7e6ac2dfa58
BTW, we should move on towards an official Poly/ML release eventually, without a few months.
I would also like to see extended monitoring included (branch GCPercent), but I still need to try it out with Isabelle in the first place.
Makarius
Thanks for your work on this! The HOL4 code that was causing the Option exception previously now compiles fine.
Michael
?On 7/7/20, 16:43, "polyml on behalf of David Matthews" <polyml-bounces at inf.ed.ac.uk on behalf of David.Matthews at prolingua.co.uk> wrote:
Thanks for producing this example. I've investigated it and the current master ( fb10196 ) includes a fix.
This turned out to be more complicated than expected. Earlier in the year Makarius reported a segfault in some generated code and produced a cut down example. Reverting a change (19d82db) seemed to fix the problem but the reversion appears to have introduced the Option exception that you found. I've now looked again and both the segfault bug and the Option exception bug are unrelated to the changes. It's just that these changes either revealed or masked the underlying bugs by altering the intermediate code.
The current master should have proper fixes for both the bugs. Makarius: Could you check that you don't get the segfault in the generated code with the current master. It works correctly with my cut down version of your cut down version.
David
On 30/06/2020 18:01, Phil Clayton wrote:
I managed to produce a smallish example fairly quickly as the code causing it didn't have many dependencies. I have raised https://github.com/polyml/polyml/issues/136
Phil
On 30/06/20 00:14, Norrish, Michael (Data61, Acton) wrote:
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 ... endit 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
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
-
David.Matthews＠prolingua.co.uk -
makarius＠sketis.net -
Michael.Norrish＠data61.csiro.au -
phil.clayton＠veonix.com