Dear Alice experts,
I've just managed to make Alice crash due to a pattern match that mentions
a variable redudantly, see the example below.
Makarius
-----------------------------------------------------------------------------
datatype pgipdoc =
Openblock of { metavarid: string option, name: string option }
| Closeblock of { }
| Opentheory of { thyname: string, parentnames: string list , text: string}
| Theoryitem of { name: string option, text: string }
| Closetheory of { text: string }
| Opengoal of { thmname: string option, text: string }
| Proofstep of { text: string }
| Closegoal of { text: string }
| Giveupgoal of { text: string }
| Postponegoal of { text: string }
| Comment of { text: string }
| Doccomment of { text: string }
| Whitespace of { text: string }
| Spuriouscmd of { text: string }
| Badcmd of { text: string }
| Unparseable of { text: string }
| Metainfo of { name: string option, text: string }
| Litcomment of { format: string option, content: string }
| Showcode of { show: bool }
| Setformat of { format: string };
fun ok (Closeblock _) = false;
fun crash (Closeblock x) = false;
(*vpdebug.txt:
val rec
$642768[crash] =
fn $642776 : 1 =>
label 642780:
case $642776 of
(tag Closeblock/1) () =>
label 642778:
val $642771[x] = $642774
label 642777:
indirect
return (tag false/0) ()
else
label 642779:
raise prim "General.Match"
export {crash=$642768[crash], ...}
*)
-----------------------------------------------------------------------------
_______________________________________________
alice-users mailing list
[email protected]
http://www.ps.uni-sb.de/mailman/listinfo/alice-users
