caledon
caledon copied to clipboard
Parser stalls on some bad inputs.
For whatever reason, the Caledon program will stall, eating up an arbitrarily large amount of memory when encountering certain code which should instead produce syntax errors. Here are some examples of code which, if encountered, will trigger what I'm talking about;
defn unit : prop
as
defn unit : prop
as \(P : prop) P . P
defn unit : prop
as [P : prop] P -> P
defn tt : unit
as \0 p . p
defn unit : prop
| tt =
defn unit : prop
| tt = \(P : prop) . unit
defn unit : prop
| one = unit
a(