allow loading and parsing of source files

Author: Jonas Betzendahl

goedelT.cabal

@@ -22,6 +22,7 @@ executable goedelT
   -- other-extensions:    
   build-depends:       base >=4.8,
                        attoparsec >=0.13,
-                       bytestring >=0.10
+                       bytestring >=0.10,
+                       directory >=1.2.6
   hs-source-dirs:      src
   default-language:    Haskell2010

src/Evaluator.hs

@@ -1,4 +1,4 @@
-module Evaluator where
+module Evaluator (eval, replace) where
 
 import Types
 

src/Main.hs

@@ -1,11 +1,13 @@
 module Main where
 
-import Data.List (deleteBy, find, intersect, nub, permutations, union)
+import Data.List  (deleteBy, find, foldl', intercalate, intersect, nub, permutations, union)
+
 import System.IO
+import System.Directory (doesFileExist, makeAbsolute)
 
 import Types
-import Typechecker
-import Evaluator
+import Typechecker (typecheck)
+import Evaluator   (eval, replace)
 import Parser
 
 -- Entry point of program
@@ -23,9 +25,6 @@ repl ts = do
   inp <- getLine
   case parseInput inp of
     Quit      -> pure ()
-    Run       -> case find (\(a,_) -> a == "main") ts of
-      (Just (a,e)) -> print (eval e) >> repl ts
-      Nothing      -> putStrLn "~> No expression \"main\" currently in context." >> repl ts
     Context   -> case ts of 
       [] -> putStrLn "~> Context currently empty!" >> repl ts
       _  -> do putStrLn "\n~> Current Context:"
@@ -44,7 +43,7 @@ repl ts = do
                  ":clear         Clear current context\n"] >> repl ts
     (Expr e)  -> case typecheck ts e of
                    (Left  r) -> putStrLn ("Error: Typecheck failed!\n" ++  r) >> repl ts
-                   (Right _) -> let f = foldl (\k (n,s) -> (replace (make_disjoint k s) (Placeholder n)) k)
+                   (Right _) -> let f = foldl' (\k (n,s) -> (replace (make_disjoint k s) (Placeholder n)) k)
                                     d (x:y:zs) = if x == y then x else d (y:zs)
                                     o = d $ iterate ((flip f) ts) e 
                                  in (print (eval o)) >> repl ts
@@ -59,12 +58,26 @@ repl ts = do
                       (Right tau) -> putStrLn $ "This expression has type "  ++ show tau 
                     repl ts
     Clear     -> putStrLn "~> Context cleared!"              >> repl []
-    (Load fl) -> do inh <- readFile fl
-                    case parseFile inh of
-                      (Left err)  -> putStrLn err >> repl ts
-                      (Right con) -> putStrLn "~> File loaded!" >> repl (ts ++ con)
+    (Load fl) -> do afl <- makeAbsolute fl
+                    ex  <- doesFileExist afl
+                    if ex then do inh <- readFile afl
+                                  case parseFile inh of
+                                    (Left err)  -> putStrLn err >> repl ts
+                                    (Right res) -> do let (foo,bar) = foldl' embed ([],[]) res
+                                                      case bar of 
+                                                        [] -> pure ()
+                                                        xs -> do putStrLn "~> The following expressions had incorrect types:"
+                                                                 putStrLn ("   " ++ (intercalate ", " xs))
+                                                      putStrLn "~> File loaded!"
+                                                      repl (ts ++ foo)
+                          else putStrLn "~> That file does not exist!" >> repl ts
     NoParse   -> putStrLn "~> Error: Could not parse input!" >> repl ts
 
+embed :: (Context, [String]) -> (String, Exp, Typ) -> (Context, [String])
+embed (con,fs) (nm, ex, tp) = case typecheck con ex of 
+  (Left _)   -> (con, fs ++ [nm])
+  (Right sg) -> if sg == tp then (con ++ [(nm, ex)],fs) else (con, fs ++ [nm])
+
 -- Returns a version of the second expression, that has no shared
 -- variables with the first expression. This is to avoid capture.
 make_disjoint :: Exp -> Exp -> Exp

src/Parser.hs

@@ -16,18 +16,19 @@ parseInput str = case ((parseOnly inputParser) . pack) str of
   (Left  e) -> NoParse
   where
     inputParser :: Parser Input
-    inputParser = ((string ":quit")    >> pure Quit)
+    inputParser = ((string ":q")       >> pure Quit)
+              <|> ((string ":quit")    >> pure Quit)
               <|> ((string ":context") >> pure Context)
               <|> ((string ":clear")   >> pure Clear)
               <|> ((string ":help")    >> pure Help)
-              <|> ((string ":run")     >> pure Run)
               <|> letParser
               <|> typecheckParser
               <|> evalParser
+              <|> loadParser
 
     loadParser :: Parser Input
     loadParser = do string ":load "
-                    filepth <- manyTill letter_ascii endOfLine
+                    filepth <- (many1 anyChar)
                     pure $ Load filepth
 
     letParser :: Parser Input
@@ -96,8 +97,8 @@ typParser = pNat <|> pVoid <|> pUnit <|> pBool <|> pOption <|> pSum <|> pProduct
               sigma <- typParser ; char ')' ; pure $ Sum tau sigma
 
 expParser :: Parser Exp
-expParser = pBools <|> pIf  <|> pEmpty <|> pFull <|> pWhich <|> pTuple <|> pProject <|> 
-            pVoid <|> pSum <|> pCase <|> pAp  <|> pLambda <|> pRec <|> pZ <|> pSucc 
+expParser = pBools <|> pIf <|> pEmpty <|> pFull <|> pWhich <|> pTuple <|> pProject <|> 
+            pVoid <|> pSum <|> pCase <|> pAp <|> pLambda <|> pRec <|> pZ <|> pSucc 
             <|> pVar <|> pPlaceholder
   where
     pPlaceholder :: Parser Exp
@@ -214,12 +215,26 @@ expParser = pBools <|> pIf  <|> pEmpty <|> pFull <|> pWhich <|> pTuple <|> pProj
 -- File Parsing --
 ------------------
 
-parseFile :: String -> Either String Context
-parseFile = undefined 
-
-fileParser :: Parser Context
-fileParser = many1 defParser
+parseFile :: String -> Either String [(String, Exp, Typ)]
+parseFile = (parseOnly fileParser) . pack . init . clearLines
   where
-    defParser :: Parser (String, Exp)
-    defParser = undefined
+    commentOrEmpty :: String -> Bool
+    commentOrEmpty []    = True
+    commentOrEmpty (x:_) = x == '#'  
+
+    clearLines :: String -> String
+    clearLines = unlines . (filter (not . commentOrEmpty)) . lines
+
+fileParser :: Parser [(String, Exp, Typ)]
+fileParser = many1 (defParser <* endOfLine)
+
+defParser :: Parser (String, Exp, Typ)
+defParser = do nm <- manyTill anyChar space
+               string ": " 
+               tau <- typParser
+               endOfLine
+               string (pack nm)
+               string " = "
+               e <- expParser
+               pure $ (nm, e, tau)
 

src/Types.hs

@@ -48,8 +48,7 @@ data Exp = Placeholder String        -- Placeholder
          deriving (Eq, Ord)
 
 -- Inputs expected on REPL
-data Input = Run
-           | Quit
+data Input = Quit
            | Help
            | Context
            | Clear