Type check input

src/API/JSONData.hs

@@ -17,11 +17,10 @@ import Language.Types
 import GHC.Generics
 import Data.Aeson
 import Runtime.Values
-import Runtime.Eval
-import Parser.Parser
-import Runtime.Monad
 import Error.Error
 
+import Text.Parsec (errorPos, sourceLine, sourceColumn, ParseError)
+
 -- | Representation of a request to read a BoGL file
 data SpielRead = SpielRead {
   path :: String
@@ -56,31 +55,18 @@ instance FromJSON SpielFile where
   parseJSON (Object v) = SpielFile <$> v .: "fileName" <*> v .: "content"
   parseJSON _          = fail "Unable to parse File option" -- fallback
 
-instance FromJSON Val where
-  parseJSON (Object v) = do
-    t <- v .: "input"
-    case parseLine t of
-      Right x -> case runWithBuffer (emptyEnv (0,0)) ([], [], 1) x of
-        Right (_, v') -> return v'
-        Left _ -> fail "failed to parse..." -- FIXME
-      Left _ -> fail "failed to parse..."
-  parseJSON _ = fail "Unable to parse Val"
-
-
 -- | Representation of input to the repl, from the user
 data SpielCommand = SpielCommand {
     prelude     :: String,
     file        :: String,
     input       :: String,
-    buffer      :: [Val],
+    buffer      :: [String],
     programName :: String
   } deriving (Eq, Show, Generic)
 
-
 instance ToJSON SpielCommand
 instance FromJSON SpielCommand
 
-
 -- | Error message
 type Message = String
 -- | Error line number
@@ -125,6 +111,14 @@ data SpielResponse =
   Log String
   deriving(Eq, Generic)
 
+-- | Smart constructor for a SpielParseError
+spielParseError :: String -> ParseError -> SpielResponse
+spielParseError fn er = SpielParseError l c fn (show er)
+   where
+      pos = errorPos er
+      l   = sourceLine pos
+      c   = sourceColumn pos
+
 instance ToJSON SpielResponse where
 
 instance Show SpielResponse where
@@ -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
-
+  show (SpielTypeError e)               = show e
+  show _                                = "unused SpielResponse" -- todo: clean these out
 
 -- | List of spiel responses
 type SpielResponses = [SpielResponse]

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)
 import Parser.Parser
 import Language.Syntax
 import Language.Types
 import Text.Parsec.Pos
-import Text.Parsec (errorPos)
-import Text.Parsec.Error
 
 import Typechecker.Typechecker
-import Runtime.Eval
+import Typechecker.Monad (Env(types))
+import Runtime.Eval (runWithBuffer, bindings_)
 import Runtime.Values
-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
-_runCodeWithCommands :: SpielCommand -> IO SpielResponses
+_runCodeWithCommands :: SpielCommand -> SpielResponses
 _runCodeWithCommands sc@(SpielCommand _prelude gameFile _ _ filename) =
-  (_handleParsed sc $ parsePreludeAndGameText _prelude gameFile filename)
-
-
--- | Handles result of parsing a prelude and game
-_handleParsed :: SpielCommand -> IO (Either ParseError (Game SourcePos)) -> IO SpielResponses
-_handleParsed (SpielCommand _ gameFile inpt buf _) parsed = do
-  pparsed <- parsed
-  case pparsed of
-    Right game -> do
-      let checked = tc game
-      if success checked
-        then return $ [SpielTypes (rtypes checked), (serverRepl game gameFile inpt (buf, [], 1))]
-        else return $ SpielTypes (rtypes checked) : map (SpielTypeError . snd) (errors checked)
-    Left _err -> do
-      let position = errorPos _err
-          l = sourceLine position
-          c = sourceColumn position
-          in
-        return $ [SpielParseError l c gameFile (show _err)]
-
-
--- |Handles running a command in the repl from the server
+   case parsePreludeAndGameText _prelude gameFile filename of
+      Right game          -> _handleParsed sc game
+      Left progParseError -> [spielParseError gameFile progParseError]
+
+-- | Typechecks and evaluates a parsed prelude and game
+_handleParsed :: SpielCommand -> (Game SourcePos) -> SpielResponses
+_handleParsed (SpielCommand _ gameFile replExpr buf _) game =
+   if success progTCRes then
+      case handleInput inputEnv buf of
+         H (Left er)    -> [er]
+         H (Right buf') -> [progTypes, (serverRepl game gameFile replExpr (buf', [], 1))]
+   else
+      progTypes : map (SpielTypeError . snd) (errors progTCRes)
+   where
+      progTCRes = tc game
+      inputEnv  = (e progTCRes) { types = [] } -- keep the input type, discard other bindings
+      progTypes = SpielTypes (rtypes progTCRes)
+
+-- | Parses, typecheckes, and evaluates input strings so they can be used in evaluation
+--   as a 'Val' buffer
+--
+--   Note: if anything other than the first input string results in failure, then something is
+--   wrong on the front end. These have all been verified in previous calls to _runCodeWithCommands
+handleInput :: Env -> [String] -> SpielHandler [Val]
+handleInput inputEnv xs = do
+   exprs  <- mapM parseInput xs
+   exprs' <- mapM (tcInput inputEnv) exprs
+   mapM evalInput exprs'
+
+-- | Parses input strings so that they can be typechecked and evaluated
+parseInput :: String -> SpielHandler (Expr SourcePos)
+parseInput s = case parseFromText literal "user input" s of
+                  (Left er)  -> hFail $ spielParseError "user input" er
+                  (Right ex) -> return ex
+
+-- | Typechecks input expressions
+tcInput :: Env -> (Expr SourcePos) -> SpielHandler (Expr SourcePos)
+tcInput inputEnv x = case exprHasInputType inputEnv x of
+                        (Left er) -> hFail $ SpielTypeError er
+                        Right _ -> return x
+
+-- | Evaluates typechecker input expressions.
+--   If a literal fails to evaluate, then something is wrong with the evaluator,
+--   hence the internal error
+evalInput :: (Expr SourcePos) -> SpielHandler Val
+evalInput x = case run x of
+                  Left _ -> hFail $ SpielError "input evaluation internal error"
+                  Right (_, v') -> return v'
+   where
+      run = runWithBuffer (emptyEnv (0,0)) ([], [], 1)
+
+-- | Handles running a command in the repl from the server
 serverRepl :: (Game SourcePos) -> String -> String -> Buffer -> SpielResponse
-serverRepl (Game _ i@(BoardDef (szx,szy) _) b vs) fn inpt buf = do
-  case parseLine inpt of
+serverRepl (Game _ i@(BoardDef (szx,szy) _) b vs) fn replExpr buf = do
+  case parseLine replExpr of
     Right x -> do
       case tcexpr (environment i b vs) x of
         Right _ -> do -- Right t
@@ -66,15 +97,31 @@ serverRepl (Game _ i@(BoardDef (szx,szy) _) b vs) fn inpt buf = do
             -- boards and tape returned, returns the boards for displaying on the frontend
             Left (bs, _) -> (SpielPrompt bs)
 
-            -- runtime error encountered
-            -- TODO REMOVED Redundant clause?
-            --Left err -> (SpielRuntimeError (show err))
-
         -- typechecker encountered an error in the expression
         Left _err -> (SpielTypeError _err)
     -- bad parse
-    Left _err ->
-      let position = errorPos _err
-          l = sourceLine position
-          c = sourceColumn position in
-      (SpielParseError l c fn (show _err))
+    Left progParseError -> spielParseError fn progParseError
+
+newtype SpielHandler a = H (Either SpielResponse a)
+
+instance Show a => Show (SpielHandler a) where
+   show (H (Left s))  = show s
+   show (H (Right x)) = show x
+
+-- Monad for handling an operation in which failure is represented as an appropriate SpielResponse
+instance Monad SpielHandler where
+   return res = H $ Right res
+   (H h) >>= k = case h of
+                    Left er   -> hFail er
+                    Right res -> k res
+
+instance Functor SpielHandler where
+   fmap = liftM
+
+instance Applicative SpielHandler where
+   pure  = return
+   (<*>) = ap
+
+-- Smart constructor for a failure case in SpielHandler
+hFail :: SpielResponse -> SpielHandler a
+hFail = H . Left

src/API/RunCode.hs

@@ -13,13 +13,10 @@ import API.Run
 import API.JSONData
 import Servant
 
-import Control.Monad.IO.Class
-
-
 -- | Runs literal code, lifting it into Handler
 -- Runs the contents of the prelude and gamefile without writing them out into files
 -- Once these both succeed, the new temporary files are parsed
 -- , and the response is returned
 handleRunCode :: SpielCommand -> Handler SpielResponses
 -- calls API.Run._runCodeWithCommands to interpret this raw BoGL code
-handleRunCode sc = liftIO (_runCodeWithCommands sc)
+handleRunCode sc = return $ _runCodeWithCommands sc

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
    show (Error (TE e) _ p) = "Type error in " ++ srcname ++ show e
       where
          srcname = case sourceName p of
@@ -57,3 +58,4 @@ cterr terr = Error (TE terr) (assign terr)
                     (Dereff _ _)          -> 8
                     (Uninitialized _)     -> 10
                     (SigBadFeq _ _ _)     -> 11
+                    (InputMismatch _ _ _) -> 12

src/Error/TypeError.hs

@@ -21,6 +21,7 @@ data TypeError = Mismatch      {t1 :: Type,  t2 :: Type, expr :: Expr ()}
                | Dereff        {name :: String, typ :: Type}
                | Uninitialized {name :: String}
                | SigBadFeq     {name :: String, sigType :: Type, feq :: Equation ()}
+               | InputMismatch {actual :: Type, expected :: Type, expr :: Expr()}
                deriving (Eq)
 
 instance Show TypeError where
@@ -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 _)  = "Got type " ++ show act ++ ", but expected type " ++ show xp ++ " from input."

src/Language/Types.hs

@@ -94,9 +94,9 @@ boardt = Plain boardxt
 boardxt :: Xtype
 boardxt = bnestx Board
 
--- | Nest a Btype as a Type
-p :: Btype -> Type
-p b = Plain $ X b S.empty
+-- | Xtype smart constructor for Input
+inputxt :: Xtype
+inputxt = bnestx Input
 
 instance Show Xtype where
   show (X b xs) | S.null xs = show b

src/Parser/Parser.hs

@@ -6,8 +6,8 @@ License     : BSD-3
 -}
 
 module Parser.Parser (
-   parseLine, parsePreludeFromText, parseGameFromText, parseGameFile, parsePreludeAndGameText,
-   expr, isLeft, parseAll, valdef, ftype, xtype, boardeqn, equation, decl, parseGame, typesyn, Parser, lexer, reservedNames, enum)
+   parseLine, parseFromText, parsePreludeFromText, parseGameFromText, parseGameFile, parsePreludeAndGameText,
+   expr, isLeft, parseAll, valdef, ftype, xtype, boardeqn, equation, decl, parseGame, typesyn, Parser, lexer, reservedNames, enum, literal)
 where
 
 import Parser.Error
@@ -143,9 +143,6 @@ op s f assoc = Infix (reservedOp s *> pure f) assoc
 lexeme :: ParsecT String u Identity a -> ParsecT String u Identity a
 lexeme = P.lexeme lexer
 
--- TODO REMOVED UNUSED
---integer = P.integer lexer
-
 -- | Integer token recognizer
 int :: ParsecT String u Identity Int
 int = fromInteger <$> P.integer lexer
@@ -196,12 +193,16 @@ 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
+
 -- | Comma separated values, 1 or more
 commaSep1 :: ParsecT String u Identity a -> ParsecT String u Identity [a]
 commaSep1 = P.commaSep1 lexer
 
 -- | 0 or more comma separated values
--- unused
+-- unused, but possibly useful
 --commaSep :: ParsecT String u Identity a -> ParsecT String u Identity [a]
 --commaSep = P.commaSep lexer
 
@@ -217,6 +218,22 @@ reservedOp = P.reservedOp lexer
 comma :: ParsecT String u Identity String
 comma = P.comma lexer
 
+-- | A parser for a literal expression (to be used for input).
+--   Consumes all preceding whitespace since it is a top-level parser.
+literal :: Parser (Expr SourcePos)
+literal = spaces *> -- note: intentionally does not use whiteSpace, which allows comments
+  (I <$> int
+  <|>
+  B <$> (reserved "True" *> pure True)
+  <|>
+  B <$> (reserved "False" *> pure False)
+  <|>
+  S <$> capIdentifier
+  <|>
+  (try $ parens (literal <* notFollowedBy comma)) -- parenthesized literal
+  <|>
+  Tuple <$> parens (commaSep2 literal))
+
 -- | Atomic expression, under an annotation
 atom :: Parser (Expr SourcePos)
 atom =
@@ -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
-parsePreludeAndGameText :: String -> String -> String -> IO ParseResult
-parsePreludeAndGameText preludeContent gameFileContent fileName = do
-  prel <- return (parsePreludeFromText preludeContent)
-  case prel of
-    Right r -> return (parseGameFromText gameFileContent fileName r)
-    Left err              -> return $ Left err
+parsePreludeAndGameText :: String -> String -> String -> ParseResult
+parsePreludeAndGameText preludeContent gameFileContent fileName =
+  case parsePreludeFromText preludeContent of
+    Right r  -> (parseGameFromText gameFileContent fileName r)
+    Left err -> Left err

src/Typechecker/Monad.hs

@@ -55,7 +55,6 @@ data Stat = Stat {
 -- | Typechecking monad
 type Typechecked a = (StateT Stat (ReaderT Env (ExceptT Error Identity))) a
 
-
 -- | Run a computation inside of the typechecking monad
 typecheck :: Env -> Typechecked a -> Either Error (a, Stat)
 typecheck e a = runIdentity . runExceptT . (flip runReaderT e) $
@@ -154,6 +153,7 @@ unify (X y z) (X w k)
 unify a b = mismatch (Plain a) (Plain b)
 
 -- | Check if t1 has type t2 with subsumption (i.e. by subtyping)
+--   This is a wrapper around the Ord instance to produce the type error if there is a mismatch
 hasType :: Xtype -> Xtype -> Typechecked Xtype
 hasType (Tup xs) (Tup ys)
   | length xs == length ys = Tup <$> zipWithM hasType xs ys
@@ -173,6 +173,13 @@ getInfo = ((,) <$> getSrc <*> getPos)
 mismatch :: Type -> Type -> Typechecked a
 mismatch _t1 _t2 = getInfo >>= (\(e, x) -> throwError $ cterr (Mismatch _t1 _t2 e) x)
 
+-- | Input type mismatch error
+inputmismatch :: Type -> Typechecked a
+inputmismatch act = do
+                       (e, x) <- getInfo
+                       it     <- getInput
+                       throwError $ cterr (InputMismatch act (Plain it) e) x
+
 -- | Type mismatch error for function application
 appmismatch :: Name -> Type -> Type -> Typechecked a
 appmismatch n _t1 _t2 = getInfo >>= (\(e, x) -> throwError $ cterr (AppMismatch n _t1 _t2 e) x)