Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Candle REPL fixes #904

Merged
merged 3 commits into from Aug 20, 2022
Merged

Candle REPL fixes #904

merged 3 commits into from Aug 20, 2022

Conversation

oskarabrahamsson
Copy link
Contributor

Fixes the following issues with the Candle REPL:

  • The lexer now leaves type variables untouched. Previously, writing a type variable could get the lexer stuck scanning an infinitely long character literal. (The Caml syntax uses '-ticks for character literals.)
  • Change the syntax of the loading directives to match exactly that used in the HOL Light sources. The new directives are:
    • loads "file";; to load 'file' and add it to a list of loaded files;
    • needs "file";; to load 'file' if it wasn't previously loaded, and add it to a list of loaded files;
    • #use "file";; to load a file without adding it to the list of loaded files.
  • Add a stub for pointer equality ((==): 'a -> 'a -> bool) that always evaluates to false.

- Pointer equality definition (==) defaulting to false
- Define rat_minus
- Define a printer for rationals
- Set userInput when recovering from error
- Add comment about exception printer
This makes the REPL pick up on the words 'needs' and 'loads' when
they sit at the top level. If they are followed by a string literal
and a double semicolon token, the REPL loads a file (like previously
with #load and #need).

The motivation behind this change is to make sure Candle accepts HOL
Light source files with as minor changes as possible.
@oskarabrahamsson oskarabrahamsson changed the title Candle boot fixes Candle REPL fixes Aug 16, 2022
@myreen myreen merged commit cf77a10 into master Aug 20, 2022
@myreen myreen deleted the candle_boot-fixes branch August 20, 2022 05:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants