Improve examples and fix more bugs.

app/Main.hs

@@ -1,9 +1,9 @@
 module Main (main) where
 
 import Parser.Parser (ParserError, parseProgram, composeASTs)
-import Parser.TypeDefs (fnName, AST(AST), typeDecls, mapFromDeclList)
+import Parser.TypeDefs (fnName, mapFromDeclList, AST(..))
 import TypeSystem.PatternChecker (PatternError, runCoverageCheck, checkPatterns)
-import TypeSystem.TypeDefs
+import TypeSystem.TypeDefs (TypeSystemError, IAST, iTypeDecls)
 import System.Environment (getArgs)
 import Data.Bifunctor (first)
 import Semantics.Builtins (makePrelude)
@@ -14,7 +14,7 @@ import Semantics.TypeDefs
 import Debug.Trace (traceM)
 import System.IO
 import Data.Either (isLeft, isRight)
-import Control.Monad (when, unless)
+import Control.Monad (when, unless, zipWithM)
 import System.Exit (exitFailure)
 import System.Directory
 
@@ -51,11 +51,11 @@ getRight _ = error "getRight called with a Left"
 doInterpret :: Either ProgramError IAST -> IO Value
 doInterpret res = if isRight res then interpretAST (getRight res) else return (VAlg "Error occured, exiting!" [])
 
-doChecks :: String -> String -> String -> Either ProgramError IAST
+doChecks :: [String] -> [String] -> String -> Either ProgramError IAST
 doChecks fname contents preludeContents = do
   prelude <- mapPrelude <$> parseRealProgram preludeFileName preludeContents
-  ast <- parseRealProgram fname contents
-  let full = composeASTs prelude ast
+  ast <- zipWithM parseRealProgram fname contents
+  let full = foldl1 composeASTs (prelude : ast)
   iast <- first PreprocessingError $ preprocess full
   let typeEnv = mapFromDeclList $ iTypeDecls iast
   traceM $ "Full AST is: " ++ show full
@@ -74,19 +74,16 @@ assertFileExists name = do
   exists <- doesFileExist name
   unless exists . printAndExit $ "Cannot find file \"" ++ name ++ "\"."
 
-{- | Parses one file, typechecks it and prints the AST. -}
-oneFileParser :: IO ()
-oneFileParser = do
-  fname:_ <- getArgs
+
+main :: IO ()
+main = do
+  fileNames <- getArgs
   assertFileExists preludeFileName
-  assertFileExists fname
-  contents <- readFile fname
+  mapM_ assertFileExists fileNames
+  contents <- mapM readFile fileNames
   preludeContents <- readFile preludeFileName
-  let res = doChecks fname contents preludeContents
+  let res = doChecks fileNames contents preludeContents
   when (isLeft res) . printAndExit $ showResult res
   v <- doInterpret res
   print v
-  hFlush stderr
-
-main :: IO ()
-main = oneFileParser
+  hFlush stderr

bad/bad13.cont

@@ -0,0 +1,3 @@
+# wrong use of continuation notation
+@{Int}(Int) ::
+a = 1;

bad/bad3.cont

@@ -1,3 +1,3 @@
-# this function is well typed in System F, not in Hindley-Milner
+# this function requires unrestricted quantification on types.
 Int ::
 one = (fn f. f succ (f 0)) (fn x. x);

bad/bad5.cont

@@ -1,9 +1,6 @@
 # this will fail due to non-exhaustive patterns: the case where list has only one element is missing.
-# furthermore, even if we add the "h : _" case, it will cause a type error because
-# the "a" type variable cannot be unified with type "Maybe a" due to the occurs check.
 
 [a] -> Maybe a ::
 safeHead xs c = match xs with
-  | h : (Just x) : _ => c (Just h)
-  | h : _ => c (Just h)
-  | [] => c Nothing;
+| h : (Just x) : _ => c (Just h)
+| [] => c Nothing;

badout/bad13.out

@@ -0,0 +1 @@
+Cannot add continuation to non-function type Int

badout/bad5.out

@@ -1,2 +1 @@
-Type error occured:
-Cannot unify type [a103] with Maybe a104
+Pattern group for expression EVar "xs" is non-exhaustive.

badout/bad6.out

@@ -1,2 +1,2 @@
 Type error occured:
-Cannot unify type Int with (Int -> a107) -> a107
+Cannot unify type Int with (Int -> a104) -> a104

good/conttest.cont

@@ -1,18 +1,19 @@
+{#
+  Demonstration of basic contination function usage.
+}#
+
 Int -> Int ::
 fac n c =
   if n == 0
     then c 1
-    else fac (n - 1) (λf . c (n * f));
+    else fac (n - 1) (\f. c (n * f));
 
 Int -> Int ::
 fib n c =
   if n <= 1
     then c 1
     else fib (n - 1) (λres . fib (n - 2) (λres2 . c (res + res2)));
 
-Int -> Int -> Int ::
-sum a b c = c (a + b);
-
 Int -> Int -> Int ::
 max2 a b c = c (if a <= b then b else a);
 
@@ -22,5 +23,21 @@ max3 x y z =
     then max2 y z
     else max2 x y;
 
-Int ::
-main = max3 1 2 3;
+# Example of throwing an exception.
+Int -> Int -> Int ::
+div x y c =
+  if y == 0
+    then Nothing
+    else safeDiv x y c;
+
+# safe means it assumes it's safe and won't be called with a zero value
+Int -> Int -> Int ::
+safeDiv x y c =
+  if x < y
+    then c 0
+    else safeDiv (x - y) y (\rest. c (rest + 1));
+
+# if we replace 'fa' by 0 we get Nothing instead of Just 3628800
+res = fib 10 (\fi. fac 10 (\fa. div fi fa (\d. max3 fi fa (1000 * d) Just)));
+
+main = const res;

good/library.cont

@@ -0,0 +1,34 @@
+{#
+  This is a library, it cannot be interpreted on its own.
+}#
+
+c :
+@{c}(a -> b) -> [a] -> [b] ::
+contMap f xs c = match xs with
+| [] => c []
+| h:t => f h (\x . contMap f t (\rest . c (x : rest)));
+
+[a] -> Maybe a ::
+safeHead xs c = match xs with
+  | h : _ => c (Just h)
+  | [] => c Nothing;
+
+d :
+@{d}(a -> b -> c) -> [a] -> [b] -> [c] ::
+zipWith f xs ys c = match Pair xs ys with
+| Pair (x:tx) (y:ty) => f x y (\n . zipWith f tx ty (\rest . c (n : rest)))
+| _ => c [];
+
+c :
+[@{c}(a -> b)] -> [a] -> [b] ::
+apply fs xs c = match Pair fs xs with
+| Pair (f:frest) (x:xrest) => f x (\res . apply frest xrest (\l . c (res : l)))
+| _ => c [];
+
+[[a]] -> [a] ::
+contcat xs c = match xs with
+| l:ls => contcat ls (\res . c (l ++ res))
+| [] => c [];
+
+[[[[[[a]]]]]] -> [a] ::
+superFlatten xs c = contcat xs (flip contcat (flip contcat (flip contcat (flip contcat c))));

good/listTest.cont

@@ -1,22 +1,12 @@
-type TwoLists a b = TwoLists [a] [b];
-
-c :
-@{c}(a -> b) -> [a] -> [b] ::
-contMap f xs c = match xs with
-  | [] => c []
-  | h:t => f h (\x . contMap f t (\rest . c (x : rest)));
-
-
-[a] -> Maybe a ::
-safeHead xs c = match xs with
-  | h : _ => c (Just h)
-  | [] => c Nothing;
+{#
+  To run this, import library.cont as well.
+}#
 
 d :
 @{d}(a -> b -> c) -> [a] -> [b] -> Maybe c ::
-joinSafeHeads f xs ys c = match TwoLists xs ys with
-  | TwoLists (h1:_) (h2:_) => f h1 h2 (\x.c (Just x))
-  | TwoLists _ _ => c Nothing;
+joinSafeHeads f xs ys c = match Pair xs ys with
+  | Pair (h1:_) (h2:_) => f h1 h2 (\x.c (Just x))
+  | Pair _ _ => c Nothing;
 
 
 plusThree x c = c (x + 3);
@@ -26,5 +16,5 @@ add x y c = c (x + y);
 Maybe Int ::
 main = \c .
   contMap plusThree [3, 1, 3, 7] \l .
-  joinSafeHeads add l [4, 2, 12] c;
+  joinSafeHeads add l (4 : 2 : 12 : []) c;
 

good/staticBinding.cont

@@ -0,0 +1,12 @@
+x = 1;
+
+y = x;
+
+f z c = c (z + x);
+
+test =
+  let g = \_ . x in
+  let x = 0      in
+  f 0 (\res . res + y + g 20);
+
+main = const test;

good/tiny.cont

@@ -25,10 +25,10 @@ type Stmt =
   | SIfte BExpr Stmt Stmt
   | SWhile BExpr Stmt;
 
-{# {- | Due to the limitations of the type system
+{# Due to the limitations of the type system
    the statement denotation function
    differs from the one presented on the lecture
-   Semantics and verification of computer programs. -} }#
+   Semantics and verification of computer programs. }#
 
 alias Cont = Store -> Store;
 
@@ -64,15 +64,6 @@ evalBExpr b env c = match b with
 | BAnd b1 b2 => evalBExpr b1 env (\l . evalBExpr b2 env (\r . c (l and r)))
 | BNot b => evalBExpr b env (\res . c (not res));
 
-#evalStmt stmt env store :: (Return Store -> Store) -> Store
-
-#comp const unReturn :: Return Store -> Store
-
-#unReturn :: Return a -> a
-#const :: a -> b -> a
-#comp :: (a -> b -> a) -> (Return a -> a) -> Return a -> b -> a
-
-
 power =
 let emptyEnv   = const (Loc (-1)) in
 let emptyState = const (-1)       in

goodout/conttest.out

@@ -1 +1 @@
-3
+Just 3628800

goodout/staticBinding.out

@@ -0,0 +1 @@
+3