You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
HOL Light with OCaml uses a char range of 0-255.
With F# based on .NET the char range is 0-65535.
This will cause problems with functions based on printer.ctable such as printer.isspace, printer.issymb, etc. because they will throw System.IndexOutOfRangeException for a char with a value of 256 or greater as ctable is an array with only 255 values.
For now we will limit the input values from 0-255 to be in agreement with the OCaml range, but latter may modify the functions to handle the fuller range of characters.
The text was updated successfully, but these errors were encountered:
ctable has 256 values by default, but it could be larger if any of the strings used to initialize it (e.g., alphas) contain characters with a larger value. We could just as easily initialize ctable to have 65536 entries (System.Char.MaxValue), as that's not much memory in the grand scheme of things.
We should probably leave the code as-is for now though, because the way the lexer/parser works it's going to be very slow if we use Checked.byte or manually check that value <= 255 and also because (eventually) it'd be nice to lift this ASCII restriction since it's a carry-over from OCaml and not a problem on .NET.
HOL Light with OCaml uses a char range of 0-255.
With F# based on .NET the char range is 0-65535.
This will cause problems with functions based on printer.ctable such as printer.isspace, printer.issymb, etc. because they will throw System.IndexOutOfRangeException for a char with a value of 256 or greater as ctable is an array with only 255 values.
For now we will limit the input values from 0-255 to be in agreement with the OCaml range, but latter may modify the functions to handle the fuller range of characters.
The text was updated successfully, but these errors were encountered: