diff --git a/src/Compiler/ES/ES.idr b/src/Compiler/ES/ES.idr index e9f88acd6..397de5648 100644 --- a/src/Compiler/ES/ES.idr +++ b/src/Compiler/ES/ES.idr @@ -20,14 +20,14 @@ addConstToPreamble : {auto c : Ref ESs ESSt} -> String -> String -> Core String addConstToPreamble name def = do s <- get ESs + let v = "const " ++ esName name ++ " = (" ++ def ++ ")" case lookup name (preamble s) of Nothing => do - let v = "const " ++ esName name ++ " = (" ++ def ++ ")" put ESs (record { preamble = insert name v (preamble s) } s) pure $ esName name Just x => - if x /= def then throw $ InternalError $ "two incompatible definitions for " ++ name + if x /= v then throw $ InternalError $ "two incompatible definitions for " ++ name ++ "<|" ++ x ++"|> <|"++ v ++ "|>" else pure $ esName name @@ -104,7 +104,7 @@ boundedIntOp bits o lhs rhs = boundedInt 63 (binOp o lhs rhs) boolOp : String -> String -> String -> String -boolOp o lhs rhs = "(" ++ binOp o lhs rhs ++ " ? 1 : 0)" +boolOp o lhs rhs = "(" ++ binOp o lhs rhs ++ " ? BigInt(1) : BigInt(0))" jsConstant : {auto c : Ref ESs ESSt} -> Constant -> Core String jsConstant (I i) = pure $ toBigInt $ show i diff --git a/src/Compiler/ES/Imperative.idr b/src/Compiler/ES/Imperative.idr index bfbb1fc03..a75ab7c7e 100644 --- a/src/Compiler/ES/Imperative.idr +++ b/src/Compiler/ES/Imperative.idr @@ -9,6 +9,10 @@ import Compiler.CompileExpr import public Core.Context import public Core.TT +import Compiler.ES.RemoveUnused + +import Debug.Trace + mutual public export data ImperativeExp = IEVar Name @@ -272,6 +276,6 @@ compileToImperative c tm = let ndefs = namedDefs cdata let ctm = forget (mainExpr cdata) s <- newRef Imps (MkImpSt 0) - compdefs <- traverse getImp ndefs + compdefs <- traverse getImp (defsUsedByNamedCExp ctm ndefs) (s, main) <- impExp ctm pure $ concat compdefs <+> s <+> EvalExpStatement main diff --git a/src/Compiler/ES/Node.idr b/src/Compiler/ES/Node.idr index ef9864253..9508bdb93 100644 --- a/src/Compiler/ES/Node.idr +++ b/src/Compiler/ES/Node.idr @@ -30,7 +30,8 @@ compileExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> (outfile : String) -> Core (Maybe String) compileExpr c execDir tm outfile = do es <- compileToNode c tm - coreLift (writeFile outfile es) + Right () <- coreLift (writeFile outfile es) + | Left err => throw (FileErr outfile err) pure (Just outfile) ||| Node implementation of the `executeExpr` interface. diff --git a/src/Compiler/ES/RemoveUnused.idr b/src/Compiler/ES/RemoveUnused.idr new file mode 100644 index 000000000..2bca28abc --- /dev/null +++ b/src/Compiler/ES/RemoveUnused.idr @@ -0,0 +1,66 @@ +module Compiler.ES.RemoveUnused + +import Data.SortedSet +import Data.SortedMap +import Data.Vect +import Data.List + +import Core.CompileExpr +import Core.Name +import Core.FC + +import Debug.Trace + +mutual + usedNames : NamedCExp -> SortedSet Name + usedNames (NmLocal fc n) = empty + usedNames (NmRef fc n) = insert n empty + usedNames (NmLam fc n e) = usedNames e + usedNames (NmApp fc x args) = usedNames x `union` concat (usedNames <$> args) + usedNames (NmPrimVal fc c) = empty + usedNames (NmOp fc op args) = concat $ usedNames <$> args + usedNames (NmConCase fc sc alts def) = (usedNames sc `union` concat (usedNamesConAlt <$> alts)) `union` maybe empty usedNames def + usedNames (NmConstCase fc sc alts def) = (usedNames sc `union` concat (usedNamesConstAlt <$> alts)) `union` maybe empty usedNames def + usedNames (NmExtPrim fc p args) = concat $ usedNames <$> args + usedNames (NmCon fc x t args) = concat $ usedNames <$> args + usedNames (NmDelay fc t) = usedNames t + usedNames (NmForce fc t) = usedNames t + usedNames (NmLet fc x val sc) = usedNames val `union` usedNames sc + usedNames (NmErased fc) = empty + usedNames (NmCrash fc msg) = empty + + usedNamesConAlt : NamedConAlt -> SortedSet Name + usedNamesConAlt (MkNConAlt n t args exp) = usedNames exp + + usedNamesConstAlt : NamedConstAlt -> SortedSet Name + usedNamesConstAlt (MkNConstAlt c exp) = usedNames exp + +usedNamesDef : NamedDef -> SortedSet Name +usedNamesDef (MkNmFun args exp) = usedNames exp +usedNamesDef (MkNmError exp) = usedNames exp +usedNamesDef (MkNmForeign cs args ret) = empty +usedNamesDef (MkNmCon _ _ _) = empty + +defsToUsedMap : List (Name, FC, NamedDef) -> SortedMap Name (SortedSet Name) +defsToUsedMap defs = + fromList $ (\(n,_,d)=> (n, usedNamesDef d)) <$> defs + +calcUsed : SortedSet Name -> SortedMap Name (SortedSet Name) -> List Name -> SortedSet Name +calcUsed done d [] = done +calcUsed done d xs = + let used_in_xs = foldl f empty $ (\z => lookup z d) <$> xs + new_done = union done (fromList xs) + in calcUsed (new_done) d (SortedSet.toList $ difference used_in_xs new_done) + where + f : SortedSet Name -> Maybe (SortedSet Name) -> SortedSet Name + f x Nothing = x + f x (Just y) = union x y + +calcUsedDefs : List Name -> List (Name, FC, NamedDef) -> List (Name, FC, NamedDef) +calcUsedDefs names defs = + let usedNames = calcUsed empty (defsToUsedMap defs) names + in List.filter (\(n, fc, d) => contains n usedNames) defs + +export +defsUsedByNamedCExp : NamedCExp -> List (Name, FC, NamedDef) -> List (Name, FC, NamedDef) +defsUsedByNamedCExp exp defs = calcUsedDefs (SortedSet.toList $ usedNames exp) defs diff --git a/tests/Main.idr b/tests/Main.idr index 7c3040046..083c92f95 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -117,7 +117,11 @@ chezTests nodeTests : List String nodeTests - = ["node001"] + = [ "node001", "node002", "node003", "node004", "node005", "node006", "node007", "node008", "node009" + , "node011", "node012", "node013", "node014", "node015", "node017", "node018", "node019" + , "node020", "node021" + , "reg001" + ] ideModeTests : List String ideModeTests diff --git a/tests/node/node002/Pythag.idr b/tests/node/node002/Pythag.idr new file mode 100644 index 000000000..ac1b61484 --- /dev/null +++ b/tests/node/node002/Pythag.idr @@ -0,0 +1,9 @@ +range : Integer -> Integer -> List Integer +range bottom top + = if bottom > top then [] + else bottom :: range (bottom + 1) top + +pythag : Integer -> List (Integer, Integer, Integer) +pythag top + = [(x, y, z) | z <- range 1 top, y <- range 1 z, x <- range 1 y, + x * x + y * y == z * z] diff --git a/tests/node/node002/expected b/tests/node/node002/expected new file mode 100644 index 000000000..92a55d8cb --- /dev/null +++ b/tests/node/node002/expected @@ -0,0 +1,3 @@ +[(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))] +1/1: Building Pythag (Pythag.idr) +Main> Main> Bye for now! diff --git a/tests/node/node002/input b/tests/node/node002/input new file mode 100644 index 000000000..236990f22 --- /dev/null +++ b/tests/node/node002/input @@ -0,0 +1,2 @@ +:exec printLn (pythag 200) +:q diff --git a/tests/node/node002/run b/tests/node/node002/run new file mode 100755 index 000000000..4b2d4cc5a --- /dev/null +++ b/tests/node/node002/run @@ -0,0 +1,2 @@ +$1 --cg node --no-banner Pythag.idr < input +rm -rf build diff --git a/tests/node/node003/IORef.idr b/tests/node/node003/IORef.idr new file mode 100644 index 000000000..d44964a57 --- /dev/null +++ b/tests/node/node003/IORef.idr @@ -0,0 +1,16 @@ +import Data.IORef + +main : IO () +main + = do x <- newIORef 42 + let y = x + writeIORef y 94 + val <- readIORef x + printLn val + val <- readIORef y + printLn val + modifyIORef x (* 2) + val <- readIORef x + printLn val + val <- readIORef y + printLn val diff --git a/tests/node/node003/expected b/tests/node/node003/expected new file mode 100644 index 000000000..22097cf85 --- /dev/null +++ b/tests/node/node003/expected @@ -0,0 +1,6 @@ +94 +94 +188 +188 +1/1: Building IORef (IORef.idr) +Main> Main> Bye for now! diff --git a/tests/node/node003/input b/tests/node/node003/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/node/node003/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/node/node003/run b/tests/node/node003/run new file mode 100755 index 000000000..1917cdfb5 --- /dev/null +++ b/tests/node/node003/run @@ -0,0 +1,2 @@ +$1 --cg node --no-banner IORef.idr < input +rm -rf build diff --git a/tests/node/node004/Buffer.idr b/tests/node/node004/Buffer.idr new file mode 100644 index 000000000..57365495a --- /dev/null +++ b/tests/node/node004/Buffer.idr @@ -0,0 +1,54 @@ +import Data.Buffer +import System.File + +main : IO () +main + = do Just buf <- newBuffer 100 + | Nothing => putStrLn "Buffer creation failed" + s <- rawSize buf + printLn s + + setInt32 buf 1 94 + setString buf 5 "AAAA" + val <- getInt32 buf 1 + printLn val + + setDouble buf 10 94.42 + val <- getDouble buf 10 + printLn val + + setString buf 20 "Hello there!" + val <- getString buf 20 5 + printLn val + + val <- getString buf 26 6 + printLn val + + setBits16 buf 32 65535 + val <- getBits16 buf 32 + printLn val + + ds <- bufferData buf + printLn ds + + Right _ <- writeBufferToFile "test.buf" buf 100 + | Left err => putStrLn "Buffer write fail" + Right buf2 <- createBufferFromFile "test.buf" + | Left err => putStrLn "Buffer read fail" + + ds <- bufferData buf2 + printLn ds + + freeBuffer buf + freeBuffer buf2 + +-- Put back when the File API is moved to C and these can work again +-- Right f <- openBinaryFile "test.buf" Read +-- | Left err => putStrLn "File error on read" +-- Just buf3 <- newBuffer 99 +-- | Nothing => putStrLn "Buffer creation failed" +-- Right _ <- readBufferFromFile f buf3 100 +-- | Left err => do putStrLn "Buffer read fail" +-- closeFile f +-- closeFile f + diff --git a/tests/node/node004/expected b/tests/node/node004/expected new file mode 100644 index 000000000..fb6f8bffe --- /dev/null +++ b/tests/node/node004/expected @@ -0,0 +1,10 @@ +100 +94 +94.42 +"Hello" +"there!" +65535 +[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] +[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] +1/1: Building Buffer (Buffer.idr) +Main> Main> Bye for now! diff --git a/tests/node/node004/input b/tests/node/node004/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/node/node004/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/node/node004/run b/tests/node/node004/run new file mode 100755 index 000000000..de18df5c0 --- /dev/null +++ b/tests/node/node004/run @@ -0,0 +1,2 @@ +$1 --cg node --no-banner Buffer.idr < input +rm -rf build test.buf diff --git a/tests/node/node005/Filter.idr b/tests/node/node005/Filter.idr new file mode 100644 index 000000000..1c726d2c8 --- /dev/null +++ b/tests/node/node005/Filter.idr @@ -0,0 +1,29 @@ +data Vect : Nat -> Type -> Type where + Nil : Vect Z a + (::) : a -> Vect k a -> Vect (S k) a + +Show a => Show (Vect n a) where + show xs = "[" ++ showV xs ++ "]" + where + showV : forall n . Vect n a -> String + showV [] = "" + showV [x] = show x + showV (x :: xs) = show x ++ ", " ++ showV xs + +filter : (a -> Bool) -> Vect n a -> (p ** Vect p a) +filter pred [] = (_ ** []) +filter pred (x :: xs) + = let (n ** xs') = filter pred xs in + if pred x + then (_ ** x :: xs') + else (_ ** xs') + +test : (x ** Vect x Nat) +test = (_ ** [1,2]) + +foo : String +foo = show test + +even : Nat -> Bool +even Z = True +even (S k) = not (even k) diff --git a/tests/node/node005/expected b/tests/node/node005/expected new file mode 100644 index 000000000..3458b122d --- /dev/null +++ b/tests/node/node005/expected @@ -0,0 +1,3 @@ +(3 ** [2, 4, 6]) +1/1: Building Filter (Filter.idr) +Main> Main> Bye for now! diff --git a/tests/node/node005/input b/tests/node/node005/input new file mode 100644 index 000000000..eb9e0b8d6 --- /dev/null +++ b/tests/node/node005/input @@ -0,0 +1,2 @@ +:exec printLn (filter even [S Z,2,3,4,5,6]) +:q diff --git a/tests/node/node005/run b/tests/node/node005/run new file mode 100755 index 000000000..9bf1f7f18 --- /dev/null +++ b/tests/node/node005/run @@ -0,0 +1,3 @@ +$1 --cg node --no-banner Filter.idr < input + +rm -rf build diff --git a/tests/node/node006/TypeCase.idr b/tests/node/node006/TypeCase.idr new file mode 100644 index 000000000..b28d64229 --- /dev/null +++ b/tests/node/node006/TypeCase.idr @@ -0,0 +1,32 @@ +data Bar = MkBar +data Baz = MkBaz + +foo : (x : Type) -> String +foo Nat = "Nat" +foo Bool = "Bool" +foo (List x) = "List of " ++ foo x +foo Int = "Int" +foo Type = "Type" +foo _ = "Something else" + +strangeId : {a : Type} -> a -> a +strangeId {a=Integer} x = x+1 +strangeId x = x + +partial +strangeId' : {a : Type} -> a -> a +strangeId' {a=Integer} x = x+1 + +main : IO () +main = do printLn (foo Nat) + printLn (foo (List Nat)) + printLn (foo (List Bar)) + printLn (foo (List Baz)) + printLn (foo (List Bool)) + printLn (foo Int) + printLn (foo String) + printLn (foo (List Type)) + printLn (foo (List Int)) + printLn (strangeId 42) + printLn (strangeId (the Int 42)) + diff --git a/tests/node/node006/TypeCase2.idr b/tests/node/node006/TypeCase2.idr new file mode 100644 index 000000000..d647b5c69 --- /dev/null +++ b/tests/node/node006/TypeCase2.idr @@ -0,0 +1,14 @@ +data Bar = MkBar +data Baz = MkBaz + +strangeId : a -> a +strangeId {a=Nat} x = x+1 +strangeId x = x + +foo : (0 x : Type) -> String +foo Nat = "Nat" +foo Bool = "Bool" +foo (List x) = "List of " ++ foo x +foo Int = "Int" +foo Type = "Type" +foo _ = "Something else" diff --git a/tests/node/node006/expected b/tests/node/node006/expected new file mode 100644 index 000000000..e3982e0c4 --- /dev/null +++ b/tests/node/node006/expected @@ -0,0 +1,21 @@ +"Nat" +"List of Nat" +"List of Something else" +"List of Something else" +"List of Bool" +"Int" +"Something else" +"List of Type" +"List of Int" +43 +42 +1/1: Building TypeCase (TypeCase.idr) +Main> Main> Main.strangeId is total +Main> Main.strangeId': +strangeId' _ +Main> Bye for now! +1/1: Building TypeCase2 (TypeCase2.idr) +TypeCase2.idr:5:14--5:17:While processing left hand side of strangeId at TypeCase2.idr:5:1--6:1: +Can't match on Nat (Erased argument) +TypeCase2.idr:9:5--9:9:While processing left hand side of foo at TypeCase2.idr:9:1--10:1: +Can't match on Nat (Erased argument) diff --git a/tests/node/node006/input b/tests/node/node006/input new file mode 100644 index 000000000..7be5b94cc --- /dev/null +++ b/tests/node/node006/input @@ -0,0 +1,4 @@ +:exec main +:total strangeId +:missing strangeId' +:q diff --git a/tests/node/node006/run b/tests/node/node006/run new file mode 100755 index 000000000..63a3817bc --- /dev/null +++ b/tests/node/node006/run @@ -0,0 +1,4 @@ +$1 --cg node --no-banner TypeCase.idr < input +$1 --cg node --no-banner TypeCase2.idr --check + +rm -rf build diff --git a/tests/node/node007/TypeCase.idr b/tests/node/node007/TypeCase.idr new file mode 100644 index 000000000..026199d97 --- /dev/null +++ b/tests/node/node007/TypeCase.idr @@ -0,0 +1,26 @@ +data Bar = MkBar +data Baz = MkBaz + +data Vect : Nat -> Type -> Type where + Nil : Vect Z a + (::) : a -> Vect k a -> Vect (S k) a + +desc : Type -> String +desc Int = "Int" +desc Nat = "Nat" +desc (Vect n a) = "Vector of " ++ show n ++ " " ++ desc a +desc Type = "Type" +desc _ = "Something else" + +descNat : Type -> String +descNat t = "Function from Nat to " ++ desc t + +descFn : (x : Type) -> String +descFn ((x : Nat) -> b) = descNat (b Z) +descFn (a -> b) = "Function on " ++ desc a +descFn x = desc x + +main : IO () +main = do printLn (descFn (Nat -> Nat)) + printLn (descFn ((x : Nat) -> Vect x Int)) + printLn (descFn (Type -> Int)) diff --git a/tests/node/node007/expected b/tests/node/node007/expected new file mode 100644 index 000000000..34a2bbdb3 --- /dev/null +++ b/tests/node/node007/expected @@ -0,0 +1,5 @@ +"Function from Nat to Nat" +"Function from Nat to Vector of 0 Int" +"Function on Type" +1/1: Building TypeCase (TypeCase.idr) +Main> Main> Bye for now! diff --git a/tests/node/node007/input b/tests/node/node007/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/node/node007/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/node/node007/run b/tests/node/node007/run new file mode 100755 index 000000000..adc812558 --- /dev/null +++ b/tests/node/node007/run @@ -0,0 +1,3 @@ +$1 --cg node --no-banner TypeCase.idr < input + +rm -rf build diff --git a/tests/node/node008/Nat.idr b/tests/node/node008/Nat.idr new file mode 100644 index 000000000..664f20bca --- /dev/null +++ b/tests/node/node008/Nat.idr @@ -0,0 +1,11 @@ +myS : Nat -> Nat +myS n = S n + +myS_crash : Nat -> Nat +myS_crash = S + +main : IO () +main = do + printLn (S Z) + printLn (myS Z) + printLn (myS_crash Z) diff --git a/tests/node/node008/expected b/tests/node/node008/expected new file mode 100644 index 000000000..b01365535 --- /dev/null +++ b/tests/node/node008/expected @@ -0,0 +1,5 @@ +1 +1 +1 +1/1: Building Nat (Nat.idr) +Main> Main> Bye for now! diff --git a/tests/node/node008/input b/tests/node/node008/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/node/node008/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/node/node008/run b/tests/node/node008/run new file mode 100755 index 000000000..36d4a1139 --- /dev/null +++ b/tests/node/node008/run @@ -0,0 +1,3 @@ +$1 --cg node --no-banner Nat.idr < input + +rm -rf build diff --git a/tests/node/node009/expected b/tests/node/node009/expected new file mode 100644 index 000000000..e1e52cfb6 --- /dev/null +++ b/tests/node/node009/expected @@ -0,0 +1,4 @@ +42 +ällo +1/1: Building uni (uni.idr) +Main> Main> Bye for now! diff --git a/tests/node/node009/input b/tests/node/node009/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/node/node009/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/node/node009/run b/tests/node/node009/run new file mode 100755 index 000000000..b1a33028d --- /dev/null +++ b/tests/node/node009/run @@ -0,0 +1,3 @@ +$1 --cg node --no-banner uni.idr < input + +rm -rf build diff --git a/tests/node/node009/uni.idr b/tests/node/node009/uni.idr new file mode 100644 index 000000000..e5b0b5e2c --- /dev/null +++ b/tests/node/node009/uni.idr @@ -0,0 +1,9 @@ +foo : String +foo = "ällo" + +ällo : Int +ällo = 42 + +main : IO () +main = do printLn ällo + putStrLn "ällo" diff --git a/tests/node/node011/bangs.idr b/tests/node/node011/bangs.idr new file mode 100644 index 000000000..6cbc67dd6 --- /dev/null +++ b/tests/node/node011/bangs.idr @@ -0,0 +1,32 @@ + +add : Int -> Int -> Int +add = (+) + +-- lift to nearest binder +addm1 : Maybe Int -> Maybe Int -> Maybe Int +addm1 x y = let z = x in pure (add !z !y) + +-- lift to nearest binder +addm2 : Maybe Int -> Maybe Int -> Maybe Int +addm2 = \x, y => pure (!x + !y) + +getLen : String -> IO Nat +getLen str = pure (length str) + +fakeGetLine : String -> IO String +fakeGetLine str = pure str + +-- lift out innermost first +printThing1 : IO () +printThing1 = printLn !(getLen !(fakeGetLine "line1")) + +-- lift out leftmost first +printThing2 : IO () +printThing2 = printLn (!(fakeGetLine "1") ++ !(fakeGetLine "2")) + +-- don't lift out of if +printBool : Bool -> IO () +printBool x + = if x + then putStrLn !(fakeGetLine "True") + else putStrLn !(fakeGetLine "False") diff --git a/tests/node/node011/expected b/tests/node/node011/expected new file mode 100644 index 000000000..b9fef7313 --- /dev/null +++ b/tests/node/node011/expected @@ -0,0 +1,8 @@ +5 +"12" +True +False +1/1: Building bangs (bangs.idr) +Main> Just 7 +Main> Just 7 +Main> Main> Main> Main> Main> Bye for now! diff --git a/tests/node/node011/input b/tests/node/node011/input new file mode 100644 index 000000000..a18e9ba45 --- /dev/null +++ b/tests/node/node011/input @@ -0,0 +1,7 @@ +addm1 (Just 3) (Just 4) +addm2 (Just 3) (Just 4) +:exec printThing1 +:exec printThing2 +:exec printBool True +:exec printBool False +:q diff --git a/tests/node/node011/run b/tests/node/node011/run new file mode 100644 index 000000000..d46ee7e63 --- /dev/null +++ b/tests/node/node011/run @@ -0,0 +1,3 @@ +$1 --cg node --no-banner bangs.idr < input + +rm -rf build diff --git a/tests/node/node012/array.idr b/tests/node/node012/array.idr new file mode 100644 index 000000000..209677fa2 --- /dev/null +++ b/tests/node/node012/array.idr @@ -0,0 +1,11 @@ +import Data.IOArray + +main : IO () +main + = do x <- newArray 20 + writeArray x 10 "Hello" + writeArray x 11 "World" + printLn !(toList x) + + y <- fromList (map Just [1,2,3,4,5]) + printLn !(toList y) diff --git a/tests/node/node012/expected b/tests/node/node012/expected new file mode 100644 index 000000000..364c6cd0e --- /dev/null +++ b/tests/node/node012/expected @@ -0,0 +1,4 @@ +[Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just "Hello", Just "World", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing] +[Just 1, Just 2, Just 3, Just 4, Just 5] +1/1: Building array (array.idr) +Main> Main> Bye for now! diff --git a/tests/node/node012/input b/tests/node/node012/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/node/node012/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/node/node012/run b/tests/node/node012/run new file mode 100755 index 000000000..0d88d47c9 --- /dev/null +++ b/tests/node/node012/run @@ -0,0 +1,2 @@ +$1 --cg node --no-banner array.idr < input +rm -rf build diff --git a/tests/node/node014/Echo.idr b/tests/node/node014/Echo.idr new file mode 100644 index 000000000..bc3e6af93 --- /dev/null +++ b/tests/node/node014/Echo.idr @@ -0,0 +1,57 @@ +module Main + +import System +import System.Info +import Network.Socket +import Network.Socket.Data +import Network.Socket.Raw + +runServer : IO (Either String (Port, ThreadID)) +runServer = do + Right sock <- socket AF_INET Stream 0 + | Left fail => pure (Left $ "Failed to open socket: " ++ show fail) + res <- bind sock (Just (Hostname "localhost")) 0 + if res /= 0 + then pure (Left $ "Failed to bind socket with error: " ++ show res) + else do + port <- getSockPort sock + res <- listen sock + if res /= 0 + then pure (Left $ "Failed to listen on socket with error: " ++ show res) + else do + forked <- fork (serve port sock) + pure $ Right (port, forked) + + where + serve : Port -> Socket -> IO () + serve port sock = do + Right (s, _) <- accept sock + | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err) + Right (str, _) <- recv s 1024 + | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err) + putStrLn ("Received: " ++ str) + Right n <- send s ("echo: " ++ str) + | Left err => putStrLn ("Server failed to send data with error: " ++ show err) + pure () + +runClient : Port -> IO () +runClient serverPort = do + Right sock <- socket AF_INET Stream 0 + | Left fail => putStrLn ("Failed to open socket: " ++ show fail) + res <- connect sock (Hostname "localhost") serverPort + if res /= 0 + then putStrLn ("Failed to connect client to port " ++ show serverPort ++ ": " ++ show res) + else do + Right n <- send sock ("hello world!") + | Left err => putStrLn ("Client failed to send data with error: " ++ show err) + Right (str, _) <- recv sock 1024 + | Left err => putStrLn ("Client failed to receive on socket with error: " ++ show err) + -- assuming that stdout buffers get flushed in between system calls, this is "guaranteed" + -- to be printed after the server prints its own message + putStrLn ("Received: " ++ str) + +main : IO () +main = do + Right (serverPort, tid) <- runServer + | Left err => putStrLn $ "[server] " ++ err + runClient serverPort diff --git a/tests/node/node014/expected b/tests/node/node014/expected new file mode 100644 index 000000000..4d6c212bb --- /dev/null +++ b/tests/node/node014/expected @@ -0,0 +1,4 @@ +Received: hello world! +Received: echo: hello world! +1/1: Building Echo (Echo.idr) +Main> Main> Bye for now! diff --git a/tests/node/node014/input b/tests/node/node014/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/node/node014/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/node/node014/run b/tests/node/node014/run new file mode 100755 index 000000000..e7505f39a --- /dev/null +++ b/tests/node/node014/run @@ -0,0 +1,3 @@ +$1 --cg node --no-banner -p network Echo.idr < input + +rm -rf build diff --git a/tests/node/node015/Numbers.idr b/tests/node/node015/Numbers.idr new file mode 100644 index 000000000..dddc8010a --- /dev/null +++ b/tests/node/node015/Numbers.idr @@ -0,0 +1,36 @@ +module Main + +import Data.List + +%default partial + +large : (a: Type) -> a +-- integer larger than 64 bits +large Integer = 3518437212345678901234567890123 +-- int close to 2ˆ63 +-- we expect some operations will overflow +large Int = 3518437212345678901234567890 + +small : (a: Type) -> a +small Integer = 437 +small Int = 377 + +numOps : (Num a) => List ( a -> a -> a ) +numOps = [ (+), (*) ] + +negOps : (Neg a) => List (a -> a -> a) +negOps = [ (-) ] + +integralOps : (Integral a) => List (a -> a -> a) +integralOps = [ div, mod ] + +binOps : (Num a, Neg a, Integral a) => List (a -> a -> a) +binOps = numOps ++ negOps ++ integralOps + +main : IO () +main = do + putStrLn $ show (results Integer) + putStrLn $ show (results Int) + where + results : (a:Type) -> (Num a, Neg a, Integral a) => List a + results a = map (\ op => large a `op` small a) binOps diff --git a/tests/node/node015/expected b/tests/node/node015/expected new file mode 100644 index 000000000..4808bb6af --- /dev/null +++ b/tests/node/node015/expected @@ -0,0 +1,4 @@ +[3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339] +[8650625671965379659, 5435549321212129090, 8650625671965378905, 365458446121836181, 357] +1/1: Building Numbers (Numbers.idr) +Main> Main> Bye for now! diff --git a/tests/node/node015/input b/tests/node/node015/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/node/node015/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/node/node015/run b/tests/node/node015/run new file mode 100755 index 000000000..c9bfe42cc --- /dev/null +++ b/tests/node/node015/run @@ -0,0 +1,3 @@ +$1 --cg node --no-banner Numbers.idr < input + +rm -rf build diff --git a/tests/node/node017/.gitignore b/tests/node/node017/.gitignore new file mode 100644 index 000000000..062cbdb0b --- /dev/null +++ b/tests/node/node017/.gitignore @@ -0,0 +1,2 @@ +/expected + diff --git a/tests/node/node017/dir.idr b/tests/node/node017/dir.idr new file mode 100644 index 000000000..27b385b91 --- /dev/null +++ b/tests/node/node017/dir.idr @@ -0,0 +1,15 @@ +import System.Directory + +main : IO () +main = do Right () <- createDir "testdir" + | Left err => printLn err + Left err <- createDir "testdir" + | _ => printLn "That wasn't supposed to work" + printLn err + ok <- changeDir "nosuchdir" + printLn ok + ok <- changeDir "testdir" + printLn ok + writeFile "test.txt" "hello\n" + printLn !currentDir + diff --git a/tests/node/node017/expected.in b/tests/node/node017/expected.in new file mode 100644 index 000000000..394038a25 --- /dev/null +++ b/tests/node/node017/expected.in @@ -0,0 +1,7 @@ +File Exists +False +True +Just "__PWD__testdir" +1/1: Building dir (dir.idr) +Main> Main> Bye for now! +hello diff --git a/tests/node/node017/gen_expected.sh b/tests/node/node017/gen_expected.sh new file mode 100755 index 000000000..45f5cb08d --- /dev/null +++ b/tests/node/node017/gen_expected.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env sh +if [ $OS = "windows" ]; then + MY_PWD="$(cygpath -m $(pwd))\\\\" +else + MY_PWD=$(pwd)/ +fi + +sed -e "s|__PWD__|${MY_PWD}|g" expected.in > expected diff --git a/tests/node/node017/input b/tests/node/node017/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/node/node017/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/node/node017/run b/tests/node/node017/run new file mode 100755 index 000000000..c32e6ec92 --- /dev/null +++ b/tests/node/node017/run @@ -0,0 +1,4 @@ +./gen_expected.sh +$1 --cg node --no-banner dir.idr < input +cat testdir/test.txt +rm -rf build testdir diff --git a/tests/node/node018/File.idr b/tests/node/node018/File.idr new file mode 100644 index 000000000..ee1715506 --- /dev/null +++ b/tests/node/node018/File.idr @@ -0,0 +1,14 @@ +import System.File + +main : IO () +main + = do Right ok <- readFile "test.txt" + | Left err => printLn err + putStr ok + writeFile "testout.txt" "abc\ndef\n" + Right ok <- readFile "testout.txt" + | Left err => printLn err + putStr ok + Right ok <- readFile "notfound" + | Left err => printLn err + putStr ok diff --git a/tests/node/node018/expected b/tests/node/node018/expected new file mode 100644 index 000000000..06b8a8939 --- /dev/null +++ b/tests/node/node018/expected @@ -0,0 +1,6 @@ +test test +unfinished lineabc +def +File Not Found +1/1: Building File (File.idr) +Main> Main> Bye for now! diff --git a/tests/node/node018/input b/tests/node/node018/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/node/node018/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/node/node018/run b/tests/node/node018/run new file mode 100755 index 000000000..13cb0aab8 --- /dev/null +++ b/tests/node/node018/run @@ -0,0 +1,3 @@ +$1 --cg node --no-banner File.idr < input + +rm -rf build testout.txt diff --git a/tests/node/node018/test.txt b/tests/node/node018/test.txt new file mode 100644 index 000000000..7b95d3350 --- /dev/null +++ b/tests/node/node018/test.txt @@ -0,0 +1,2 @@ +test test +unfinished line \ No newline at end of file diff --git a/tests/node/node019/expected b/tests/node/node019/expected new file mode 100644 index 000000000..cf8687d4d --- /dev/null +++ b/tests/node/node019/expected @@ -0,0 +1,6 @@ +ERROR: Unhandled input for Main.foo at partial.idr:4:1--6:1 +2 +ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--21:1 +ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--21:1 +1/1: Building partial (partial.idr) +Main> Main> Main> Main> Main> Bye for now! diff --git a/tests/node/node019/input b/tests/node/node019/input new file mode 100644 index 000000000..28f8cb5a7 --- /dev/null +++ b/tests/node/node019/input @@ -0,0 +1,5 @@ +:exec main +:exec printLn $ lookup (FS FZ) [1,2,3,4] +:exec printLn $ lookup' (FS FZ) [1,2,3,4] +:exec printLn $ lookup'' (FS FZ) [1,2,3,4] +:q diff --git a/tests/node/node019/partial.idr b/tests/node/node019/partial.idr new file mode 100644 index 000000000..11a7ac0bf --- /dev/null +++ b/tests/node/node019/partial.idr @@ -0,0 +1,26 @@ +%default partial + +foo : Maybe a -> a +foo (Just x) = x + +data Vect : ? -> Type -> Type where + Nil : Vect Z a + (::) : a -> Vect k a -> Vect (S k) a + +data Fin : Nat -> Type where + FZ : Fin (S k) + FS : Fin k -> Fin (S k) + +lookup : Fin n -> Vect n a -> a +lookup FZ (x :: xs) = x +lookup (FS k) (x :: xs) = lookup k xs + +lookup' : Fin n -> Vect n a -> a +lookup' (FS k) (x :: xs) = lookup' k xs + +lookup'' : Fin n -> Vect n a -> a +lookup'' n xs = lookup' n xs + +main : IO () +main = do let x = foo Nothing + printLn (the Int x) diff --git a/tests/node/node019/run b/tests/node/node019/run new file mode 100755 index 000000000..e201cff28 --- /dev/null +++ b/tests/node/node019/run @@ -0,0 +1,3 @@ +$1 --cg node --no-banner partial.idr < input + +rm -rf build testout.txt diff --git a/tests/node/node020/Popen.idr b/tests/node/node020/Popen.idr new file mode 100644 index 000000000..5dcbddf9d --- /dev/null +++ b/tests/node/node020/Popen.idr @@ -0,0 +1,29 @@ +import System +import System.File +import System.Info +import Data.Strings + +windowsPath : String -> String +windowsPath path = + let replaceSlashes : List Char -> List Char + replaceSlashes [] = [] + replaceSlashes ('/' :: cs) = '\\' :: replaceSlashes cs + replaceSlashes (c :: cs) = c :: replaceSlashes cs + in + pack $ replaceSlashes (unpack path) + +main : IO () +main = do + Just cmd <- getEnv "POPEN_CMD" + | Nothing => putStrLn "POPEN_CMD env var not set" + let cmd = if isWindows then windowsPath cmd else cmd + Right fh <- popen cmd Read + | Left err => printLn err + putStrLn "opened" + Right output <- fGetLine fh + | Left err => printLn err + pclose fh + putStrLn "closed" + let [idris2, _] = split ((==) ',') output + | _ => printLn "Unexpected result" + putStrLn idris2 diff --git a/tests/node/node020/expected b/tests/node/node020/expected new file mode 100644 index 000000000..3f645a591 --- /dev/null +++ b/tests/node/node020/expected @@ -0,0 +1,5 @@ +opened +closed +Idris 2 +1/1: Building Popen (Popen.idr) +Main> Main> Bye for now! diff --git a/tests/node/node020/input b/tests/node/node020/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/node/node020/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/node/node020/run b/tests/node/node020/run new file mode 100644 index 000000000..cc2b6663e --- /dev/null +++ b/tests/node/node020/run @@ -0,0 +1,3 @@ +POPEN_CMD="$1 --version" $1 --cg node --no-banner Popen.idr < input + +rm -rf build diff --git a/tests/node/node021/Bits.idr b/tests/node/node021/Bits.idr new file mode 100644 index 000000000..66f9e98fa --- /dev/null +++ b/tests/node/node021/Bits.idr @@ -0,0 +1,43 @@ +t1 : Bits8 +t1 = 2 + +t2 : Bits8 +t2 = 255 + +t3 : Bits8 +t3 = 100 + +tests8 : List String +tests8 = map show [t1 + t2, + t1 * t3, + the Bits8 (fromInteger (-8)), + the Bits8 257, + the Bits8 (fromInteger (-1)), + prim__shl_Bits8 t3 1, + prim__shl_Bits8 t2 1] + +testsCmp : List String +testsCmp = map show [t1 < t2, t3 < (t2 + t1)] + +testsMax : List String +testsMax = [show (the Bits8 (fromInteger (-1))), + show (the Bits16 (fromInteger (-1))), + show (the Bits32 (fromInteger (-1))), + show (the Bits64 (fromInteger (-1)))] + +main : IO () +main + = do printLn (t1 + t2) + printLn (t1 * t3) + printLn (t1 < t2) + printLn (prim__shl_Bits8 t3 1) + printLn (prim__shl_Bits8 t2 1) + printLn (t3 < (t2 + t1)) + printLn (the Bits8 (fromInteger (-8))) + printLn (the Bits8 257) + printLn (the Bits64 1234567890) + printLn (the Bits8 (fromInteger (-1))) + printLn (the Bits16 (fromInteger (-1))) + printLn (the Bits32 (fromInteger (-1))) + printLn (the Bits64 (fromInteger (-1))) + diff --git a/tests/node/node021/expected b/tests/node/node021/expected new file mode 100644 index 000000000..e9f4241ad --- /dev/null +++ b/tests/node/node021/expected @@ -0,0 +1,18 @@ +1 +200 +True +200 +254 +False +248 +1 +1234567890 +255 +65535 +4294967295 +18446744073709551615 +1/1: Building Bits (Bits.idr) +Main> ["257", "200", "248", "1", "255", "200", "254"] +Main> ["True", "True"] +Main> ["255", "65535", "4294967295", "18446744073709551615"] +Main> Main> Bye for now! diff --git a/tests/node/node021/input b/tests/node/node021/input new file mode 100644 index 000000000..4e908108d --- /dev/null +++ b/tests/node/node021/input @@ -0,0 +1,5 @@ +tests8 +testsCmp +testsMax +:exec main +:q diff --git a/tests/node/node021/run b/tests/node/node021/run new file mode 100644 index 000000000..ec06ec009 --- /dev/null +++ b/tests/node/node021/run @@ -0,0 +1,3 @@ +$1 --cg node --no-banner Bits.idr < input + +rm -rf build diff --git a/tests/node/reg001/expected b/tests/node/reg001/expected new file mode 100644 index 000000000..019b3ed52 --- /dev/null +++ b/tests/node/reg001/expected @@ -0,0 +1,10 @@ +3 +4.2 +"1.2" +4 +1 +"2.7" +5.9 +2 +2 +2 diff --git a/tests/node/reg001/numbers.idr b/tests/node/reg001/numbers.idr new file mode 100644 index 000000000..2952989bc --- /dev/null +++ b/tests/node/reg001/numbers.idr @@ -0,0 +1,21 @@ +-- the commented-out cases are still wrong, +-- but fixing them as well would make other tests fail for mysterious reasons +-- see https://github.com/edwinb/Idris2/pull/281 +main : IO () +main = do + printLn $ 3 + printLn $ 4.2 + printLn $ "1.2" + + printLn $ cast {to = Int} 4.8 + printLn $ cast {to = Integer} 1.2 + printLn $ cast {to = String} 2.7 + + -- printLn $ cast {to = Int} "1.2" + -- printLn $ cast {to = Integer} "2.7" + printLn $ cast {to = Double} "5.9" + + printLn $ (the Int 6 `div` the Int 3) + printLn $ (the Integer 6 `div` the Integer 3) + printLn $ (cast {to = Int} "6.6" `div` cast "3.9") + -- printLn $ (cast {to = Integer} "6.6" `div` cast "3.9") diff --git a/tests/node/reg001/run b/tests/node/reg001/run new file mode 100755 index 000000000..367ca66b4 --- /dev/null +++ b/tests/node/reg001/run @@ -0,0 +1,3 @@ +$1 --cg node numbers.idr -x main + +rm -rf build