Start adding tests for TypeDD book

Also detailing any changes needed to the code. Added primitives for
Doubles, and repl/replWith to get Chapter 2 code to work.

CONTRIBUTING.md

@@ -7,6 +7,7 @@ beyond work on the language core, are (in no particular order):
 * CI integration.
 * Documentation string support (at the REPL and IDE mode).
 * A better REPL, including:
+  - `it` and `:let`
   - readline and tab completion
   - :search and :apropos
   - help commands

TypeDD.md

@@ -0,0 +1,92 @@
+Type Driven Development with Idris
+==================================
+
+The code in the book "Type Driven Development with Idris" by Edwin Brady,
+published by Manning, will mostly work in Idris 2, with some small changes
+as detailed in this document. The updated code is also [going to be] part
+of the test suite (see tests/typedd).
+
+Chaoter 1
+---------
+
+No changes necessary
+
+Chaoter 2
+---------
+
+The Prelude is smaller than Idris 1, and many functions have been moved to
+the base libraries instead. So: 
+
+In `Average.idr`, add:
+
+import Data.Strings -- for `words`
+import Data.List -- for `length` on lists
+
+In `AveMain.idr` and `Reverse.idr` add:
+
+import System.REPL -- for 'repl'
+
+Chaoter 3
+---------
+
+TODO
+
+Chaoter 4
+---------
+
+TODO
+
+Chaoter 5
+---------
+
+TODO
+
+Chaoter 6
+---------
+
+TODO
+
+Chaoter 7
+---------
+
+TODO
+
+Chaoter 8
+---------
+
+TODO
+
+Chaoter 9
+---------
+
+TODO
+
+Chaoter 10
+----------
+
+TODO
+
+Chaoter 11
+----------
+
+TODO
+
+Chaoter 12
+----------
+
+TODO
+
+Chaoter 13
+----------
+
+TODO
+
+Chaoter 14
+----------
+
+TODO
+
+Chaoter 15
+----------
+
+TODO

libs/base/System/File.idr

@@ -16,6 +16,10 @@ data FilePtr : Type where
 %extern prim__writeLine : FilePtr -> String -> (1 x : %World) -> IORes (Either Int ())
 %extern prim__eof : FilePtr -> (1 x : %World) -> IORes Int
 
+%extern prim__stdin : FilePtr
+%extern prim__stdout : FilePtr
+%extern prim__stderr : FilePtr
+
 modeStr : Mode -> String
 modeStr Read              = "r"
 modeStr WriteTruncate     = "w"
@@ -62,6 +66,18 @@ public export
 BinaryFile : Type
 BinaryFile = FileT True
 
+export
+stdin : File
+stdin = FHandle prim__stdin
+
+export
+stdout : File
+stdout = FHandle prim__stdout
+
+export
+stderr : File
+stderr = FHandle prim__stderr
+
 export
 openFile : String -> Mode -> IO (Either FileError File)
 openFile f m 

libs/base/System/REPL.idr

@@ -0,0 +1,35 @@
+module System.REPL
+
+import System.File
+
+||| A basic read-eval-print loop, maintaining a state
+||| @ state the input state
+||| @ prompt the prompt to show
+||| @ onInput the function to run on reading input, returning a String to
+||| output and a new state. Returns Nothing if the repl should exit
+export
+replWith : (state : a) -> (prompt : String) ->
+           (onInput : a -> String -> Maybe (String, a)) -> IO ()
+replWith acc prompt fn
+   = do putStr prompt
+        eof <- fEOF stdin
+        if eof
+          then pure ()
+          else do x <- getLine
+                  case fn acc x of
+                       Just (out, acc') => 
+                           do putStr out
+                              replWith acc' prompt fn
+                       Nothing => pure ()
+
+||| A basic read-eval-print loop
+||| @ prompt the prompt to show
+||| @ onInput the function to run on reading input, returning a String to
+||| output
+export
+repl : (prompt : String) ->
+       (onInput : String -> String) -> IO ()
+repl prompt fn
+   = replWith () prompt (\x, s => Just (fn s, ()))
+
+

libs/base/base.ipkg

@@ -10,5 +10,6 @@ modules = Control.WellFounded,
 
           System,
           System.Concurrency.Raw,
-          System.File
+          System.File,
+          System.REPL
 

libs/prelude/Prelude.idr

@@ -1082,6 +1082,78 @@ export
 printLn : Show a => a -> IO ()
 printLn x = putStrLn $ show x
 
+-----------------------
+-- DOUBLE PRIMITIVES --
+-----------------------
+
+public export
+pi : Double
+pi = 3.14159265358979323846
+
+public export
+euler : Double
+euler = 2.7182818284590452354
+
+public export
+exp : Double -> Double
+exp x = prim__doubleExp x
+
+public export
+log : Double -> Double
+log x = prim__doubleLog x
+
+public export
+pow : Double -> Double -> Double
+pow x y = exp (y * log x) 
+
+public export
+sin : Double -> Double
+sin x = prim__doubleSin x
+
+public export
+cos : Double -> Double
+cos x = prim__doubleCos x
+
+public export
+tan : Double -> Double
+tan x = prim__doubleTan x
+
+public export
+asin : Double -> Double
+asin x = prim__doubleASin x
+
+public export
+acos : Double -> Double
+acos x = prim__doubleACos x
+
+public export
+atan : Double -> Double
+atan x = prim__doubleATan x
+
+public export
+sinh : Double -> Double
+sinh x = (exp x - exp (-x)) / 2
+
+public export
+cosh : Double -> Double
+cosh x = (exp x + exp (-x)) / 2
+
+public export
+tanh : Double -> Double
+tanh x = sinh x / cosh x
+
+public export
+sqrt : Double -> Double
+sqrt x = prim__doubleSqrt x
+
+public export
+floor : Double -> Double
+floor x = prim__doubleFloor x
+
+public export
+ceiling : Double -> Double
+ceiling x = prim__doubleCeiling x
+
 -----------
 -- CASTS --
 -----------
@@ -1128,6 +1200,10 @@ export
 Cast String Integer where
   cast = prim__cast_StringInteger
 
+export
+Cast Nat Integer where
+  cast = natToInteger
+
 -- To Int
 
 export
@@ -1146,6 +1222,10 @@ export
 Cast String Int where
   cast = prim__cast_StringInt
 
+export
+Cast Nat Int where
+  cast = fromInteger . natToInteger
+
 -- To Char
 
 export
@@ -1165,3 +1245,8 @@ Cast Integer Double where
 export
 Cast String Double where
   cast = prim__cast_StringDouble
+
+export
+Cast Nat Double where
+  cast = prim__cast_IntegerDouble . natToInteger
+

src/Compiler/Scheme/Common.idr

@@ -103,6 +103,18 @@ schOp StrAppend [x, y] = op "string-append" [x, y]
 schOp StrReverse [x] = op "string-reverse" [x]
 schOp StrSubstr [x, y, z] = op "string-substr" [x, y, z]
 
+schOp DoubleExp [x] = op "exp" [x]
+schOp DoubleLog [x] = op "log" [x]
+schOp DoubleSin [x] = op "sin" [x]
+schOp DoubleCos [x] = op "cos" [x]
+schOp DoubleTan [x] = op "tan" [x]
+schOp DoubleASin [x] = op "asin" [x]
+schOp DoubleACos [x] = op "asin" [x]
+schOp DoubleATan [x] = op "atan" [x]
+schOp DoubleSqrt [x] = op "sqrt" [x]
+schOp DoubleFloor [x] = op "floor" [x]
+schOp DoubleCeiling [x] = op "ceiling" [x]
+
 schOp (Cast IntType StringType) [x] = op "number->string" [x]
 schOp (Cast IntegerType StringType) [x] = op "number->string" [x]
 schOp (Cast DoubleType StringType) [x] = op "number->string" [x]
@@ -133,6 +145,7 @@ public export
 data ExtPrim = CCall | SchemeCall | PutStr | GetStr 
              | FileOpen | FileClose | FileReadLine | FileWriteLine | FileEOF
              | NewIORef | ReadIORef | WriteIORef
+             | Stdin | Stdout | Stderr
              | Unknown Name
 
 export
@@ -149,6 +162,9 @@ Show ExtPrim where
   show NewIORef = "NewIORef"
   show ReadIORef = "ReadIORef"
   show WriteIORef = "WriteIORef"
+  show Stdin = "Stdin"
+  show Stdout = "Stdout"
+  show Stderr = "Stderr"
   show (Unknown n) = "Unknown " ++ show n
 
 ||| Match on a user given name to get the scheme primitive
@@ -165,7 +181,10 @@ toPrim pn@(NS _ n)
             (n == UN "prim__eof", FileEOF),
             (n == UN "prim__newIORef", NewIORef),
             (n == UN "prim__readIORef", ReadIORef),
-            (n == UN "prim__writeIORef", WriteIORef)
+            (n == UN "prim__writeIORef", WriteIORef),
+            (n == UN "prim__stdin", Stdin),
+            (n == UN "prim__stdout", Stdout),
+            (n == UN "prim__stderr", Stderr)
             ]
            (Unknown pn)
 toPrim pn = Unknown pn
@@ -305,6 +324,9 @@ parameters (schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CEx
                            ++ !(schExp i vs val) ++ ")"
   schExtCommon i vs (Unknown n) args 
       = throw (InternalError ("Can't compile unknown external primitive " ++ show n))
+  schExtCommon i vs Stdin [] = pure "(current-input-port)"
+  schExtCommon i vs Stdout [] = pure "(current-output-port)"
+  schExtCommon i vs Stderr [] = pure "(current-error-port)"
   schExtCommon i vs prim args 
       = throw (InternalError ("Badly formed external primitive " ++ show prim
                                 ++ " " ++ show args))

src/Core/Primitives.idr

@@ -187,6 +187,43 @@ gt (Ch x) (Ch y) = pure $ toInt (x > y)
 gt (Db x) (Db y) = pure $ toInt (x > y)
 gt _ _ = Nothing
 
+doubleOp : (Double -> Double) -> Vect 1 (NF vars) -> Maybe (NF vars)
+doubleOp f [NPrimVal fc (Db x)] = Just (NPrimVal fc (Db (f x)))
+doubleOp f _ = Nothing
+
+doubleExp : Vect 1 (NF vars) -> Maybe (NF vars)
+doubleExp = doubleOp exp
+
+doubleLog : Vect 1 (NF vars) -> Maybe (NF vars)
+doubleLog = doubleOp log
+
+doubleSin : Vect 1 (NF vars) -> Maybe (NF vars)
+doubleSin = doubleOp sin
+
+doubleCos : Vect 1 (NF vars) -> Maybe (NF vars)
+doubleCos = doubleOp cos
+
+doubleTan : Vect 1 (NF vars) -> Maybe (NF vars)
+doubleTan = doubleOp tan
+
+doubleASin : Vect 1 (NF vars) -> Maybe (NF vars)
+doubleASin = doubleOp asin
+
+doubleACos : Vect 1 (NF vars) -> Maybe (NF vars)
+doubleACos = doubleOp acos
+
+doubleATan : Vect 1 (NF vars) -> Maybe (NF vars)
+doubleATan = doubleOp atan
+
+doubleSqrt : Vect 1 (NF vars) -> Maybe (NF vars)
+doubleSqrt = doubleOp sqrt
+
+doubleFloor : Vect 1 (NF vars) -> Maybe (NF vars)
+doubleFloor = doubleOp floor
+
+doubleCeiling : Vect 1 (NF vars) -> Maybe (NF vars)
+doubleCeiling = doubleOp ceiling
+
 -- Only reduce for concrete values
 believeMe : Vect 3 (NF vars) -> Maybe (NF vars)
 believeMe [_, _, val@(NDCon _ _ _ _ _)] = Just val
@@ -215,6 +252,9 @@ arithTy t = constTy t t t
 cmpTy : Constant -> ClosedTerm
 cmpTy t = constTy t t IntType
 
+doubleTy : ClosedTerm
+doubleTy = predTy DoubleType DoubleType
+
 believeMeTy : ClosedTerm
 believeMeTy 
     = Bind emptyFC (UN "a") (Pi Rig0 Explicit (TType emptyFC)) $
@@ -255,6 +295,18 @@ getOp StrAppend = strAppend
 getOp StrReverse = strReverse
 getOp StrSubstr = strSubstr
 
+getOp DoubleExp = doubleExp
+getOp DoubleLog = doubleLog
+getOp DoubleSin = doubleSin
+getOp DoubleCos = doubleCos
+getOp DoubleTan = doubleTan
+getOp DoubleASin = doubleASin
+getOp DoubleACos = doubleACos
+getOp DoubleATan = doubleATan
+getOp DoubleSqrt = doubleSqrt
+getOp DoubleFloor = doubleFloor
+getOp DoubleCeiling = doubleCeiling
+
 getOp (Cast _ y) = castTo y
 getOp BelieveMe = believeMe
 
@@ -284,6 +336,17 @@ opName StrCons = prim "strCons"
 opName StrAppend = prim "strAppend"
 opName StrReverse = prim "strReverse"
 opName StrSubstr = prim "strSubstr"
+opName DoubleExp = prim "doubleExp"
+opName DoubleLog = prim "doubleLog"
+opName DoubleSin = prim "doubleSin"
+opName DoubleCos = prim "doubleCos"
+opName DoubleTan = prim "doubleTan"
+opName DoubleASin = prim "doubleASin"
+opName DoubleACos = prim "doubleACos"
+opName DoubleATan = prim "doubleATan"
+opName DoubleSqrt = prim "doubleSqrt"
+opName DoubleFloor = prim "doubleFloor"
+opName DoubleCeiling = prim "doubleCeiling"
 opName (Cast x y) = prim $ "cast_" ++ show x ++ show y
 opName BelieveMe = prim $ "believe_me"
 
@@ -313,6 +376,18 @@ allPrimitives =
      MkPrim StrSubstr (constTy3 IntType IntType StringType StringType) isTotal,
      MkPrim BelieveMe believeMeTy isTotal] ++
 
+    [MkPrim DoubleExp doubleTy isTotal,
+     MkPrim DoubleLog doubleTy isTotal,
+     MkPrim DoubleSin doubleTy isTotal,
+     MkPrim DoubleCos doubleTy isTotal,
+     MkPrim DoubleTan doubleTy isTotal,
+     MkPrim DoubleASin doubleTy isTotal,
+     MkPrim DoubleACos doubleTy isTotal,
+     MkPrim DoubleATan doubleTy isTotal,
+     MkPrim DoubleSqrt doubleTy isTotal,
+     MkPrim DoubleFloor doubleTy isTotal,
+     MkPrim DoubleCeiling doubleTy isTotal] ++
+
     map (\t => MkPrim (Cast t StringType) (predTy t StringType) isTotal) [IntType, IntegerType, CharType, DoubleType] ++
     map (\t => MkPrim (Cast t IntegerType) (predTy t IntegerType) isTotal) [StringType, IntType, CharType, DoubleType] ++
     map (\t => MkPrim (Cast t IntType) (predTy t IntType) isTotal) [StringType, IntegerType, CharType, DoubleType] ++

src/Core/TT.idr

@@ -126,6 +126,18 @@ data PrimFn : Nat -> Type where
      StrReverse : PrimFn 1
      StrSubstr : PrimFn 3
 
+     DoubleExp : PrimFn 1
+     DoubleLog : PrimFn 1
+     DoubleSin : PrimFn 1
+     DoubleCos : PrimFn 1
+     DoubleTan : PrimFn 1
+     DoubleASin : PrimFn 1
+     DoubleACos : PrimFn 1
+     DoubleATan : PrimFn 1
+     DoubleSqrt : PrimFn 1
+     DoubleFloor : PrimFn 1
+     DoubleCeiling : PrimFn 1
+
      Cast : Constant -> Constant -> PrimFn 1
      BelieveMe : PrimFn 3
 
@@ -150,6 +162,17 @@ Show (PrimFn arity) where
   show StrAppend = "++"
   show StrReverse = "op_strrev"
   show StrSubstr = "op_strsubstr"
+  show DoubleExp = "op_doubleExp"
+  show DoubleLog = "op_doubleLog"
+  show DoubleSin = "op_doubleSin"
+  show DoubleCos = "op_doubleCos"
+  show DoubleTan = "op_doubleTan"
+  show DoubleASin = "op_doubleASin"
+  show DoubleACos = "op_doubleACos"
+  show DoubleATan = "op_doubleATan"
+  show DoubleSqrt = "op_doubleSqrt"
+  show DoubleFloor = "op_doubleFloor"
+  show DoubleCeiling = "op_doubleCeiling"
   show (Cast x y) = "cast-" ++ show x ++ "-" ++ show y
   show BelieveMe = "believe_me"
 

src/Core/TTC.idr

@@ -475,8 +475,21 @@ TTC (PrimFn n) where
   toBuf b StrAppend = tag 16
   toBuf b StrReverse = tag 17
   toBuf b StrSubstr = tag 18
-  toBuf b (Cast x y) = do tag 19; toBuf b x; toBuf b y
+
-  toBuf b BelieveMe = tag 20
+  toBuf b DoubleExp = tag 19
+  toBuf b DoubleLog = tag 20
+  toBuf b DoubleSin = tag 22
+  toBuf b DoubleCos = tag 23
+  toBuf b DoubleTan = tag 24
+  toBuf b DoubleASin = tag 25
+  toBuf b DoubleACos = tag 26
+  toBuf b DoubleATan = tag 27
+  toBuf b DoubleSqrt = tag 32
+  toBuf b DoubleFloor = tag 33
+  toBuf b DoubleCeiling = tag 34
+
+  toBuf b (Cast x y) = do tag 99; toBuf b x; toBuf b y
+  toBuf b BelieveMe = tag 100
 
   fromBuf {n} b
       = case n of
@@ -494,7 +507,19 @@ TTC (PrimFn n) where
                  12 => pure StrHead
                  13 => pure StrTail
                  17 => pure StrReverse
-                 19 => do x <- fromBuf b; y <- fromBuf b; pure (Cast x y)
+                 19 => pure DoubleExp
+                 20 => pure DoubleLog
+                 22 => pure DoubleSin
+                 23 => pure DoubleCos
+                 24 => pure DoubleTan
+                 25 => pure DoubleASin
+                 26 => pure DoubleACos
+                 27 => pure DoubleATan
+                 32 => pure DoubleSqrt
+                 33 => pure DoubleFloor
+                 34 => pure DoubleCeiling
+
+                 99 => do x <- fromBuf b; y <- fromBuf b; pure (Cast x y)
                  _ => corrupt "PrimFn 1"
 
       fromBuf2 : Ref Bin Binary ->
@@ -521,7 +546,7 @@ TTC (PrimFn n) where
       fromBuf3 b
           = case !getTag of
                  18 => pure StrSubstr
-                 20 => pure BelieveMe
+                 100 => pure BelieveMe
                  _ => corrupt "PrimFn 3"
              
 mutual

tests/Main.idr

@@ -45,6 +45,10 @@ idrisTests
        "total001", "total002", "total003", "total004", "total005",
        "total006"]
 
+typeddTests : List String
+typeddTests
+   = ["chapter001", "chapter002"]
+
 chezTests : List String
 chezTests
    = ["chez001", "chez002", "chez003", "chez004", 
@@ -99,16 +103,17 @@ main
               | _ => do putStrLn "Usage: runtests [ttimp path]"
          ttimps <- traverse (runTest "ttimp" idris2) ttimpTests
          idrs <- traverse (runTest "idris2" idris2) idrisTests
+         typedds <- traverse (runTest "typedd" idris2) typeddTests
          chexec <- findChez
          chezs <- maybe (do putStrLn "Chez Scheme not found"
                             pure [])
                         (\c => do putStrLn $ "Found Chez Scheme at " ++ c
                                   traverse (runTest "chez" idris2) chezTests)
                         chexec
-         let res = ttimps ++ idrs ++ chezs
+         let res = ttimps ++ typedds ++ idrs ++ chezs
          putStrLn (show (length (filter id res)) ++ "/" ++ show (length res) 
                        ++ " tests successful")
-         if (any not (ttimps ++ idrs ++ chezs))
+         if (any not res)
             then exitWith (ExitFailure 1)
             else exitWith ExitSuccess
 

tests/chez/chez001/Total.idr

@@ -19,9 +19,6 @@ badProcess : SP a b -> Stream a -> Stream b
 badProcess (Get f) (x :: xs) = badProcess (f x) xs
 badProcess (Put b sp) xs = badProcess sp xs
 
-Cast Nat Integer where
-  cast = natToInteger
-
 doubleInt : SP Nat Integer
 doubleInt = Get (\x => Put (the Integer (cast x))
                         (Put (the Integer (cast x) * 2) doubleInt))

tests/idris2/total006/Total.idr

@@ -19,9 +19,6 @@ badProcess : SP a b -> Stream a -> Stream b
 badProcess (Get f) (x :: xs) = badProcess (f x) xs
 badProcess (Put b sp) xs = badProcess sp xs
 
-Cast Nat Integer where
-  cast = natToInteger
-
 doubleInt : SP Nat Integer
 doubleInt = Get (\x => Put (the Integer (cast x))
                         (Put (the Integer (cast x) * 2) doubleInt))

tests/ttimp/basic006/expected

@@ -2,5 +2,5 @@ Processing as TTImp
 Written TTC
 Yaffle> ((Main.Just [Just a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [Just k = Main.Z]) [Just a = Integer]) 1) (Main.Vect.Nil [Just a = Integer])))
 Yaffle> ((Main.MkInfer [Just a = (Main.List.List Integer)]) (((Main.List.Cons [Just a = Integer]) 1) (Main.List.Nil [Just a = Integer])))
-Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved96 ?Main.{a:54}_[]), ($resolved78 ?Main.{a:54}_[])]
+Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved107 ?Main.{a:54}_[]), ($resolved89 ?Main.{a:54}_[])]
 Yaffle> Bye for now!

tests/ttimp/coverage001/expected

@@ -2,9 +2,9 @@ Processing as TTImp
 Written TTC
 Yaffle> Bye for now!
 Processing as TTImp
-Vect2.yaff:25:1--26:1:pat 0 {b:27} : Type => pat 0 {a:26} : Type => ($resolved95 {b:27}[1] {a:26}[0] $resolved77 ($resolved86 {a:26}[0]) ($resolved86 {b:27}[1])) is not a valid impossible pattern because it typechecks
+Vect2.yaff:25:1--26:1:pat 0 {b:27} : Type => pat 0 {a:26} : Type => ($resolved106 {b:27}[1] {a:26}[0] $resolved88 ($resolved97 {a:26}[0]) ($resolved97 {b:27}[1])) is not a valid impossible pattern because it typechecks
 Yaffle> Bye for now!
 Processing as TTImp
 Vect3.yaff:25:1--26:1:Not a valid impossible pattern:
-	Vect3.yaff:25:9--25:11:Type mismatch: $resolved76 and ($resolved84 ?Main.{n:21}_[] ?Main.{b:19}_[])
+	Vect3.yaff:25:9--25:11:Type mismatch: $resolved87 and ($resolved95 ?Main.{n:21}_[] ?Main.{b:19}_[])
 Yaffle> Bye for now!

tests/ttimp/coverage002/expected

@@ -2,6 +2,6 @@ Processing as TTImp
 Written TTC
 Yaffle> Main.lookup: All cases covered
 Yaffle> Main.lookup':
-($resolved122 {arg:0} {arg:1} (Main.FZ {m:0}) {arg:3})
+($resolved133 {arg:0} {arg:1} (Main.FZ {m:0}) {arg:3})
 Yaffle> Main.lookup'': Calls non covering function Main.lookup'
 Yaffle> Bye for now!

tests/ttimp/dot001/expected

@@ -3,13 +3,13 @@ Written TTC
 Yaffle> Bye for now!
 Processing as TTImp
 Dot2.yaff:15:1--16:1:When elaborating left hand side of Main.half:
-Dot2.yaff:15:10--15:15:Can't match on ($resolved73 ?{P:n:81}_[] ?{P:m:81}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?{P:n:81}_[] ?{P:n:81}_[])
+Dot2.yaff:15:10--15:15:Can't match on ($resolved84 ?{P:n:92}_[] ?{P:m:92}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved84 ?{P:n:92}_[] ?{P:n:92}_[])
 Yaffle> Bye for now!
 Processing as TTImp
 Dot3.yaff:18:1--20:1:When elaborating left hand side of Main.addBaz3:
-Dot3.yaff:18:10--18:15:Can't match on ($resolved73 ?{P:x:86}_[] ?{P:y:86}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?Main.{_:13}_[] ?Main.{_:14}_[])
+Dot3.yaff:18:10--18:15:Can't match on ($resolved84 ?{P:x:97}_[] ?{P:y:97}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved84 ?Main.{_:13}_[] ?Main.{_:14}_[])
 Yaffle> Bye for now!
 Processing as TTImp
 Dot4.yaff:17:1--19:1:When elaborating left hand side of Main.addBaz4:
-Dot4.yaff:17:10--17:15:Can't match on ($resolved73 ?Main.{_:13}_[] ?Main.{_:14}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?{P:x:86}_[] ?{P:y:86}_[])
+Dot4.yaff:17:10--17:15:Can't match on ($resolved84 ?Main.{_:13}_[] ?Main.{_:14}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved84 ?{P:x:97}_[] ?{P:y:97}_[])
 Yaffle> Bye for now!

tests/ttimp/eta002/expected

@@ -1,5 +1,5 @@
 Processing as TTImp
 Eta.yaff:16:1--17:1:When elaborating right hand side of Main.etaBad:
-Eta.yaff:16:10--17:1:When unifying: ($resolved78 ((x : Char) -> ((y : ?Main.{_:14}_[x[0]]) -> $resolved86)) ((x : Char) -> ((y : ?Main.{_:14}_[x[0]]) -> $resolved86)) ?Main.{x:18}_[] ?Main.{x:18}_[]) and ($resolved78 ((x : Char) -> ((y : ?Main.{_:14}_[x[0]]) -> $resolved86)) (({arg:10} : Integer) -> (({arg:11} : Integer) -> $resolved86)) $resolved87 \x : Char => \y : ?Main.{_:14}_[x[0]] => ($resolved87 ?Main.{_:15}_[x[1], y[0]] ?Main.{_:16}_[x[1], y[0]]))
+Eta.yaff:16:10--17:1:When unifying: ($resolved89 ((x : Char) -> ((y : ?Main.{_:14}_[x[0]]) -> $resolved97)) ((x : Char) -> ((y : ?Main.{_:14}_[x[0]]) -> $resolved97)) ?Main.{x:18}_[] ?Main.{x:18}_[]) and ($resolved89 ((x : Char) -> ((y : ?Main.{_:14}_[x[0]]) -> $resolved97)) (({arg:10} : Integer) -> (({arg:11} : Integer) -> $resolved97)) $resolved98 \x : Char => \y : ?Main.{_:14}_[x[0]] => ($resolved98 ?Main.{_:15}_[x[1], y[0]] ?Main.{_:16}_[x[1], y[0]]))
 	Eta.yaff:16:10--17:1:Type mismatch: Char and Integer
 Yaffle> Bye for now!

tests/typedd/chapter001/FCTypes.idr

@@ -0,0 +1,14 @@
+StringOrInt : Bool -> Type
+StringOrInt x = case x of
+                     True => Int
+                     False => String
+
+getStringOrInt : (x : Bool) -> StringOrInt x
+getStringOrInt x = case x of
+                        True => 94
+                        False => "Ninety four"
+
+valToString : (x : Bool) -> StringOrInt x -> String
+valToString x val = case x of
+                         True => cast val
+                         False => val

tests/typedd/chapter001/Hello.idr

@@ -0,0 +1,4 @@
+module Main
+
+main : IO ()
+main = putStrLn "Hello, Idris world!"

tests/typedd/chapter001/HelloHole.idr

@@ -0,0 +1,6 @@
+module Main
+
+main : IO ()
+main = putStrLn ?greeting
+
+

tests/typedd/chapter001/HoleFix.idr

@@ -0,0 +1,4 @@
+module Main
+
+main : IO ()
+main = putStrLn (?convert 'x')

tests/typedd/chapter001/expected

@@ -0,0 +1,8 @@
+1/1: Building FCTypes (FCTypes.idr)
+1/1: Building HelloHole (HelloHole.idr)
+1/1: Building Hello (Hello.idr)
+1/1: Building HoleFix (HoleFix.idr)
+Welcome to Idris 2 version 0.0. Enjoy yourself!
+Main> -------------------------------------
+convert : Char -> String
+Main> Bye for now!

tests/typedd/chapter001/input

@@ -0,0 +1,2 @@
+:t convert
+:q

tests/typedd/chapter001/run

@@ -0,0 +1,6 @@
+$1 FCTypes.idr --check
+$1 HelloHole.idr --check
+$1 Hello.idr --check
+$1 HoleFix.idr < input
+
+rm -rf build

tests/typedd/chapter002/AveMain.idr

@@ -0,0 +1,11 @@
+module Main
+
+import System.REPL
+import Average
+
+showAverage : String -> String
+showAverage str = "The average word length is: " ++
+                  show (average str) ++ "\n"
+
+main : IO ()
+main = repl "Enter a string: " showAverage

tests/typedd/chapter002/Average.idr

@@ -0,0 +1,18 @@
+module Average
+
+import Data.Strings
+import Data.List
+
+||| Calculate the average length of words in a string.
+||| @str a string containing words separated by whitespace.
+export
+average : (str : String) -> Double
+average str = let numWords = wordCount str
+                  totalLength = sum (allLengths (words str)) in
+                  cast totalLength / cast numWords
+  where
+    wordCount : String -> Nat
+    wordCount str = length (words str)
+
+    allLengths : List String -> List Nat
+    allLengths strs = map length strs

tests/typedd/chapter002/Double.idr

@@ -0,0 +1,2 @@
+double : Int -> Int
+double x = x + x

tests/typedd/chapter002/Generic.idr

@@ -0,0 +1,20 @@
+identityInt : Int -> Int
+identityInt x = x
+
+identityString : String -> String
+identityString x = x
+
+identityBool : Bool -> Bool
+identityBool x = x
+
+identity : ty -> ty
+identity x = x
+
+doubleNat : Nat -> Nat
+doubleNat x = x * x
+
+doubleInteger : Integer -> Integer
+doubleInteger x = x * x
+
+double : Num ty => ty -> ty
+double x = x * x

tests/typedd/chapter002/HOF.idr

@@ -0,0 +1,14 @@
+double : Num a => a -> a
+double x = x * x
+
+twice : (a -> a) -> a -> a
+twice f x = f (f x)
+
+Shape : Type
+rotate : Shape -> Shape
+
+quadruple : Num a => a -> a
+quadruple = twice double
+
+turn_around : Shape -> Shape
+turn_around = twice rotate

tests/typedd/chapter002/Let_Where.idr

@@ -0,0 +1,11 @@
+longer : String -> String -> Nat
+longer word1 word2
+    = let len1 = length word1
+          len2 = length word2 in
+          if len1 > len2 then len1 else len2
+
+pythagoras : Double -> Double -> Double
+pythagoras x y = sqrt (square x + square y)
+    where
+      square : Double -> Double
+      square x = x * x

tests/typedd/chapter002/Partial.idr

@@ -0,0 +1,2 @@
+add : Int -> Int -> Int
+add x y = x + y

tests/typedd/chapter002/Reverse.idr

@@ -0,0 +1,6 @@
+module Main
+
+import System.REPL
+
+main : IO ()
+main = repl "> " reverse

tests/typedd/chapter002/expected

@@ -0,0 +1,8 @@
+1/1: Building Double (Double.idr)
+1/1: Building Generic (Generic.idr)
+1/1: Building HOF (HOF.idr)
+1/1: Building Partial (Partial.idr)
+1/1: Building Reverse (Reverse.idr)
+1/2: Building Average (Average.idr)
+2/2: Building AveMain (AveMain.idr)
+1/1: Building Let_Where (Let_Where.idr)

tests/typedd/chapter002/run

@@ -0,0 +1,9 @@
+$1 Double.idr --check
+$1 Generic.idr --check
+$1 HOF.idr --check
+$1 Partial.idr --check
+$1 Reverse.idr --check
+$1 AveMain.idr --check
+$1 Let_Where.idr --check
+
+rm -rf build