ct-gradual-typing/Papers

Issue with loading file

Closed this issue · 1 comments

Can you take a look at the latest loadfile branch? I've tried figuring these two issues out over the last two days but I'm still stuck. Here are the issues. If you could just help point me in the right direction, that would be helpful.

  1. For some reason, the file loading only parses out the first definition and expression. This is especially confounding as the code has parseFile = many parseDef which should use the parseTypeDef and parseExpDef parsers multiple times. I also had to add the separator \\ between the end of one expression and the next definition. Without this, the parser was mixing an expression with the following definition. It didn't stop parsing one expression at the white space separating that expression from the next definition.

  2. I've also found another issue revolving around variables starting with 't'. For example:
    let true = \(p:?).\(q:?).p
    works just fine. But if you try to typecheck this, you get the error:

unexpected 't'
expecting "triv" or end of input

I first thought this was coming from the REPL parser but then we should have the same issues any variables starting with 'd', or 'u'. So I'm not really sure where this is coming from. Any thoughts?

First:

  1. For some reason, the file loading only parses out the first definition and expression. This is
    especially confounding as the code has parseFile = many parseDef which should use the
    parseTypeDef and parseExpDef parsers multiple times.

Okay, I will take a look at this.

I also had to add the separator \
between the end of one expression and the next definition. Without this, the parser was
mixing an expression with the following definition. It didn't stop parsing one expression at the
white space separating that expression from the next definition.

We defiantly do not want this separator. This just means that we have something wrong with our parser. So we should fix it.