Type check input #165

alexgrejuc · 2020-11-05T02:54:46Z

This, in combination with your editor changes, is good to merge so that we have better handling of input for users. Fixes #165.

alexgrejuc · 2020-11-05T02:57:58Z

src/API/Run.hs

+
+          -- this is bad. We grab the last Val off the buffer, which has not been typechecked
+          -- then we do: Val => String => Expr so that we can type check it
+          -- it would be much better to receive it as a Maybe Expr separate from the buffer


What we have now works, but is sketchy. We can discuss my proposed change for a further change in the near future.

Sketchy how so?

The comment above is the short version. It would be much easier to explain in full detail over a Discord chat, which we should do soon!

alexgrejuc · 2020-11-05T03:01:26Z

src/Parser/Parser.hs

@@ -217,6 +216,19 @@ reservedOp = P.reservedOp lexer
 comma :: ParsecT String u Identity String
 comma = P.comma lexer

+-- | A parser for a literal expression
+literal :: Parser (Expr SourcePos)


If we decide that only literals should be allowed, we can use this

alexgrejuc · 2020-11-05T03:02:23Z

src/Typechecker/Typechecker.hs

@@ -192,10 +193,21 @@ tc g = case tc' g of
  (_e, ls) -> let l = lefts ls in
    Tc (length l == 0) _e l (rights ls ++ types _e)

-- | Typecheck a game, and produce a tuple of an environment, with a list of errors and/or successfully typechecked names


Shortened a long line

montymxb

I'm a bit concerned that the parsing for literals will allow malformed tuples. If you could add a test to verify this is not the case that would be good. Also I had a punctuation thing, and a question, beyond that the rest seems okay for an initial work.

I understand we'll be making additional changes from this point onwards, so some of this may be irrelevant, so the addition of some lit tests would be the minimum to add here.

montymxb · 2020-11-05T19:14:19Z

src/API/Run.hs

+
+          -- this is bad. We grab the last Val off the buffer, which has not been typechecked
+          -- then we do: Val => String => Expr so that we can type check it
+          -- it would be much better to receive it as a Maybe Expr separate from the buffer


Sketchy how so?

montymxb · 2020-11-05T19:18:55Z

src/Error/Error.hs

@@ -21,6 +21,7 @@ data Error = Error {

 -- Note: the error code functionality works, but only for type errors so they are not displayed
 instance Show Error where
+   show (Error (TE e@(InputMismatch _ _ _)) _ _) = show e


montymxb · 2020-11-05T19:20:32Z

src/Error/TypeError.hs

@@ -34,4 +35,5 @@ instance Show TypeError where
  show (BadApp n e)              = "Could not apply " ++ n ++ " to " ++ show e ++ "; it is not a function."
  show (Dereff n _t)             = "Could not dereference the function " ++ n ++ " with type " ++ show _t ++ ". Maybe you forgot to give it arguments."
  show (Uninitialized n)         = "Incomplete initialization of Board " ++ quote n
-  show (SigBadFeq n sig f)    = quote (n ++ " : " ++ show sig) ++ " cannot be defined with the function equation\n\t" ++ show f
+  show (SigBadFeq n sig f)       = quote (n ++ " : " ++ show sig) ++ " cannot be defined with the function equation\n\t" ++ show f
+  show (InputMismatch act xp e)  = "Got type " ++ show act ++ " but expected type " ++ show xp ++ " from input:\n\t" ++ show e


A small punctuation nit, can add a comma between got & expected. Got type Int, but expected...

Good catch; I will fix it.

montymxb · 2020-11-05T19:23:31Z

src/Parser/Parser.hs

@@ -217,6 +216,19 @@ reservedOp = P.reservedOp lexer
 comma :: ParsecT String u Identity String
 comma = P.comma lexer

+-- | A parser for a literal expression
+literal :: Parser (Expr SourcePos)


montymxb · 2020-11-05T19:27:23Z

src/Parser/Parser.hs

+  <|>
+  S <$> capIdentifier
+  <|>
+  Tuple <$> parens ((:) <$> (lexeme literal <* lexeme comma) <*> commaSep literal)


This has the capacity to match (1,) if I am reading this correctly. Maybe it will be caught elsewhere, but by definition our tuples are a pair or more in BoGL. We could add

... (lexeme literal <* lexeme comma <* lexeme literal) <*> try $ lexeme comma *> commaSep literal

Or something of that form, basically guarantee a tuple to parse only if it has minimum two elements, and potentially look for others preceded by an additional comma.

A test against this would be revealing if this is a problem in the first place actually.

You're right. Good catch.

montymxb · 2020-11-05T19:29:26Z

src/Typechecker/Typechecker.hs

+isInputType ie = do
+   et <- exprtypeE ie
+   it <- getInput
+   if et <= it then return () else inputmismatch $ Plain et


montymxb

The changes currently up are good and look mergable, but I'll leave this as a comment if you choose to add on the extra changes for a buffer of [String] instead of [Val], whenever you have some time later this weekend or during next week.

montymxb · 2020-11-07T02:42:54Z

src/Parser/Parser.hs

@@ -196,13 +196,18 @@ gameIdentifier = capIdentifier
 capIdentifier :: ParsecT String u Identity [Char]
 capIdentifier = lookAhead upper *> identifier

+-- | Comma separated values, 2 or more
+commaSep2 :: ParsecT String u Identity a -> ParsecT String u Identity [a]
+commaSep2 p = (:) <$> (lexeme p <* lexeme comma) <*> commaSep1 p


Awesome 👍

montymxb · 2020-11-07T02:43:16Z

test/ParserTests.hs

+  True $
+  checkAllParsePass literal lits)
+     where
+        lits = ["1", "True", "False", "-1", "+1", "A", "(((40, 2), Nested, Tuple), 0)",


tests look good

alexgrejuc · 2020-11-09T03:31:02Z

The one problem is that the API tests are not comprehensive, however, I have already done quite a bit in this PR. In my opinion, fine-tuning the API and testing it is a significant amount of work and a totally separate issue. I did add some preliminary tests and I made it easier to test by making the handler functions pure.

alexgrejuc · 2020-11-09T03:31:53Z

src/API/JSONData.hs

@@ -144,8 +138,8 @@ instance Show SpielResponse where
  show (SpielTypeHole m _ _)            = show m
  -- show a fallback error, such as reading a bad-file
  show (SpielError m)                   = show m
-  show x                                = show x


Grrrrrr, I lost more time than I would like to admit due to this line.

alexgrejuc · 2020-11-09T03:33:04Z

src/API/JSONData.hs

-  show x                                = show x
-
+  show (SpielTypeError e)               = show e
+  show _                                = "unused SpielResponse" -- todo: clean these out


I did not want to write cases for unused responses, but I also did not want to remove them in this change set for fear of changing too much at once.

That's a good call. This is a certain unspoken limit before the PR should just be split into another PR haha

alexgrejuc · 2020-11-09T03:35:07Z

src/API/Run.hs

-import Runtime.Monad
+import Runtime.Monad (Buffer, emptyEnv)
+
+import Control.Monad(liftM, ap)

 -- | Runs BoGL code from raw text with the given commands
 -- utilizes parsePreludeAndGameText to parse the code directly,
 -- without reading it from a file first


this function was unnecessarily in the IO monad! I pulled it out so that it is easier to test.

alexgrejuc · 2020-11-09T03:36:07Z

src/API/Run.hs

@@ -10,49 +10,80 @@ Holds the routines for parsing and interpreting a BoGL Prelude and Game file.

 module API.Run (_runCodeWithCommands) where

-import API.JSONData
+import API.JSONData (SpielResponse(..), SpielCommand(..), SpielResponses, spielParseError)


This file still needs quite a bit of cleaning up, but I had to let it go eventually. We can do some more work to polish the API later and do it then.

It would be good to clean things up once we've taken care of whatever comes up at this upcoming meeting. In addition, it would probably be good to make several smaller changes in separate PRs. Everything that is changed there will go live, and the more we change the more likely we are to introduce a bug. Small changes will make that easier to track down when they occur.

alexgrejuc · 2020-11-09T03:37:04Z

src/Language/Types.hs

@@ -94,9 +94,9 @@ boardt = Plain boardxt
 boardxt :: Xtype
 boardxt = bnestx Board

-- | Nest a Btype as a Type


Unused and it caused a lot of issues with shadowing

alexgrejuc · 2020-11-09T03:37:47Z

src/Parser/Parser.hs

@@ -540,9 +557,8 @@ parseGameFromText :: String -> String -> ([Maybe (ValDef SourcePos)], ParState)
 parseGameFromText prog fileName pr = parseWithState (snd pr) (parseGame (catMaybes (fst pr))) fileName prog

 -- | Parse a prelude and game from text directly, without a file


There was no reason for this to be in IO.

I know I added the IO stuff in when we were first writing these out. I believe that was because we were still reading & writing from files instead of parsing the responses directly. Seems it was never re-addressed when we phased that out.

alexgrejuc · 2020-11-09T03:41:09Z

test/ParserTests.hs

+  True $
+  checkAllParsePass literal lits)
+     where
+        lits = ["1", " 1", "1 ", "True", "False", "-1", "+1", "A", "(((40, 2), Nested, Tuple), 0)",


+1 is a unary plus, just like -1 is a unary minus. Did you know that 1 + + 1 ==> 1 + (+1) is a valid BoGL program? Perhaps it could be removed, but that requires messing around with the lexer.

Honestly I had no clue, a little bit surprised actually. We can bring this up with Martin, but this seems like a very small concern for the moment.

alexgrejuc · 2020-11-09T03:43:06Z

One final note: don't squash these commits if you merge the PR! They are isolated units and it can be helpful to have them in the history for bug-tracking.

montymxb

Alright, merging this in.

montymxb · 2020-11-09T07:04:03Z

src/API/Run.hs

@@ -10,49 +10,80 @@ Holds the routines for parsing and interpreting a BoGL Prelude and Game file.

 module API.Run (_runCodeWithCommands) where

-import API.JSONData
+import API.JSONData (SpielResponse(..), SpielCommand(..), SpielResponses, spielParseError)


It would be good to clean things up once we've taken care of whatever comes up at this upcoming meeting. In addition, it would probably be good to make several smaller changes in separate PRs. Everything that is changed there will go live, and the more we change the more likely we are to introduce a bug. Small changes will make that easier to track down when they occur.

montymxb · 2020-11-09T07:07:17Z

src/Parser/Parser.hs

@@ -540,9 +557,8 @@ parseGameFromText :: String -> String -> ([Maybe (ValDef SourcePos)], ParState)
 parseGameFromText prog fileName pr = parseWithState (snd pr) (parseGame (catMaybes (fst pr))) fileName prog

 -- | Parse a prelude and game from text directly, without a file


I know I added the IO stuff in when we were first writing these out. I believe that was because we were still reading & writing from files instead of parsing the responses directly. Seems it was never re-addressed when we phased that out.

montymxb · 2020-11-09T07:08:16Z

src/Utils/General.hs

+-- unused
+--safeLast :: [a] -> Maybe a
+--safeLast [] = Nothing
+--safeLast xs = Just $ last xs


This PR is already way too big so I won't ask for it here, but this is an empty file now. In the next PR we should remove this.

I actually think it is worth keeping. I am certain we will have (if we do not already have) functions that are generally useful and should not be contained to a specific module. Keeping this file makes it more likely that a function like that will end up in the proper location rather than tucked away in another module. That is exactly the situation we had with the string utility functions, whose functionality was often being duplicated.

montymxb · 2020-11-09T07:09:35Z

test/ParserTests.hs

+  True $
+  checkAllParsePass literal lits)
+     where
+        lits = ["1", " 1", "1 ", "True", "False", "-1", "+1", "A", "(((40, 2), Nested, Tuple), 0)",


Honestly I had no clue, a little bit surprised actually. We can bring this up with Martin, but this seems like a very small concern for the moment.

alexgrejuc added 2 commits November 4, 2020 18:37

add literal parser

bbfea5e

typecheck input

ffdbdc9

alexgrejuc commented Nov 5, 2020

View reviewed changes

alexgrejuc mentioned this pull request Nov 5, 2020

Input typecheck #152

Closed

alexgrejuc requested a review from montymxb November 5, 2020 03:07

montymxb requested changes Nov 5, 2020

View reviewed changes

alexgrejuc force-pushed the type-check-input branch from a2466ee to 184d07b Compare November 6, 2020 23:50

fix literal parser and add tests

09d8938

alexgrejuc force-pushed the type-check-input branch from 184d07b to 09d8938 Compare November 7, 2020 00:20

montymxb reviewed Nov 7, 2020

View reviewed changes

reject bad input as a SpielResponse

979230f

alexgrejuc requested a review from montymxb November 9, 2020 03:28

alexgrejuc commented Nov 9, 2020

View reviewed changes

montymxb approved these changes Nov 9, 2020

View reviewed changes

montymxb merged commit 560c952 into master Nov 9, 2020

montymxb mentioned this pull request Nov 9, 2020

Input Expressions need Verification #149

Closed

alexgrejuc deleted the type-check-input branch November 11, 2020 06:52

		@@ -540,9 +557,8 @@ parseGameFromText :: String -> String -> ([Maybe (ValDef SourcePos)], ParState)
		parseGameFromText prog fileName pr = parseWithState (snd pr) (parseGame (catMaybes (fst pr))) fileName prog

		-- \| Parse a prelude and game from text directly, without a file

Navigation Menu

Type check input #165

Type check input #165

Conversation

alexgrejuc commented Nov 5, 2020 • edited

alexgrejuc Nov 5, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

montymxb left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

montymxb left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

alexgrejuc commented Nov 9, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

alexgrejuc commented Nov 9, 2020

montymxb left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

alexgrejuc commented Nov 5, 2020 •

edited

alexgrejuc Nov 5, 2020 •

edited