diff --git a/Makefile b/Makefile index 95ac294..5f7e72b 100644 --- a/Makefile +++ b/Makefile @@ -45,12 +45,13 @@ clean-libs: test: idris --build tests.ipkg - make -C tests + @make -C tests only=$(only) install: all install-exec install-libs install-exec: idris2 mkdir -p ${PREFIX}/bin + mkdir -p ${PREFIX}/idris2/lib mkdir -p ${PREFIX}/idris2/support/chez mkdir -p ${PREFIX}/idris2/support/chicken mkdir -p ${PREFIX}/idris2/support/racket diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index 772e103..28dcc57 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -63,6 +63,14 @@ mkNameTags defs tags t (n :: ns) => mkNameTags defs (insert n t tags) (t + 1) ns _ => mkNameTags defs tags t ns +natHackNames : List Name +natHackNames + = [UN "prim__add_Integer", + UN "prim__sub_Integer", + UN "prim__mul_Integer", + NS ["Prelude"] (UN "natToInteger"), + NS ["Prelude"] (UN "integerToNat")] + -- Find all the names which need compiling, from a given expression, and compile -- them to CExp form (and update that in the Defs) export @@ -71,7 +79,8 @@ findUsedNames : {auto c : Ref Ctxt Defs} -> Term vars -> findUsedNames tm = do defs <- get Ctxt let ns = getRefs (Resolved (-1)) tm - allNs <- getAllDesc (keys ns) empty defs + natHackNames' <- traverse toResolvedNames natHackNames + allNs <- getAllDesc (natHackNames' ++ keys ns) empty defs cns <- traverse toFullNames (keys allNs) -- Initialise the type constructor list with explicit names for -- the primitives (this is how we look up the tags) diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index da945f0..591761c 100644 --- a/src/Compiler/CompileExpr.idr +++ b/src/Compiler/CompileExpr.idr @@ -75,6 +75,9 @@ expandToArity num fn [] = etaExpand 0 num fn [] -- None of these should be hard coded, but we'll do it this way until we -- have a more general approach to optimising data types! +-- NOTE: Make sure that names mentioned here are listed in 'natHackNames' in +-- Common.idr, so that they get compiled, as they won't be spotted by the +-- usual calls to 'getRefs'. natHack : CExp vars -> CExp vars natHack (CCon fc (NS ["Prelude"] (UN "Z")) _ []) = CPrimVal fc (BI 0) natHack (CCon fc (NS ["Prelude"] (UN "S")) _ [k]) diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index e404bc2..24f1fdb 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -31,9 +31,26 @@ findChez x <- ["scheme", "chez", "chezscheme9.5"]] maybe (pure "/usr/bin/env scheme") pure e -findLibs : List String -> List String -findLibs = mapMaybe (isLib . trim) +-- Given the chez compiler directives, return a list of pairs of: +-- - the library file name +-- - the full absolute path of the library file name, if it's in one +-- of the library paths managed by Idris +-- If it can't be found, we'll assume it's a system library and that chez +-- will thus be able to find it. +findLibs : {auto c : Ref Ctxt Defs} -> + List String -> Core (List (String, String)) +findLibs ds + = do let libs = mapMaybe (isLib . trim) ds + traverse locate (nub libs) where + locate : String -> Core (String, String) + locate fname + = do fullname <- catch (findLibraryFile fname) + (\err => -- assume a system library so not + -- in our library path + pure fname) + pure (fname, fullname) + isLib : String -> Maybe String isLib d = if isPrefixOf "lib" d @@ -129,7 +146,7 @@ compileToSS : Ref Ctxt Defs -> ClosedTerm -> (outfile : String) -> Core () compileToSS c tm outfile = do ds <- getDirectives Chez - let libs = findLibs ds + libs <- findLibs ds (ns, tags) <- findUsedNames tm defs <- get Ctxt compdefs <- traverse (getScheme chezExtPrim defs) ns @@ -137,7 +154,8 @@ compileToSS c tm outfile main <- schExp chezExtPrim 0 [] !(compileExp tags tm) chez <- coreLift findChez support <- readDataFile "chez/support.ss" - let scm = schHeader chez libs ++ support ++ code ++ main ++ schFooter + let scm = schHeader chez (map snd libs) ++ + support ++ code ++ main ++ schFooter Right () <- coreLift $ writeFile outfile scm | Left err => throw (FileErr outfile err) coreLift $ chmod outfile 0o755 diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 4bf8ffe..54c7a45 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -67,6 +67,10 @@ HasNames a => HasNames (List a) where resolved c [] = pure [] resolved c (n :: ns) = pure $ !(resolved c n) :: !(resolved c ns) +HasNames (Int, FC, Name) where + full c (i, fc, n) = pure (i, fc, !(full c n)) + resolved c (i, fc, n) = pure (i, fc, !(resolved c n)) + HasNames (Name, Bool) where full c (n, b) = pure (!(full c n), b) resolved c (n, b) = pure (!(resolved c n), b) @@ -89,7 +93,9 @@ HasNames e => HasNames (TTCFile e) where namedirectives cgdirectives extra) = pure $ MkTTCFile version ifaceHash iHashes - holes guesses constraints + !(traverse (full gam) holes) + !(traverse (full gam) guesses) + constraints context !(traverse (full gam) autoHints) !(traverse (full gam) typeHints) @@ -128,7 +134,9 @@ HasNames e => HasNames (TTCFile e) where namedirectives cgdirectives extra) = pure $ MkTTCFile version ifaceHash iHashes - holes guesses constraints + !(traverse (resolved gam) holes) + !(traverse (resolved gam) guesses) + constraints context !(traverse (resolved gam) autoHints) !(traverse (resolved gam) typeHints) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index bf48a20..2248bcf 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -551,6 +551,8 @@ HasNames Def where full gam (TCon t a ps ds ms cs) = pure $ TCon t a ps ds !(traverse (full gam) ms) !(traverse (full gam) cs) + full gam (BySearch c d def) + = pure $ BySearch c d !(full gam def) full gam (Guess tm cs) = pure $ Guess !(full gam tm) cs full gam t = pure t @@ -567,6 +569,8 @@ HasNames Def where resolved gam (TCon t a ps ds ms cs) = pure $ TCon t a ps ds !(traverse (resolved gam) ms) !(traverse (resolved gam) cs) + resolved gam (BySearch c d def) + = pure $ BySearch c d !(resolved gam def) resolved gam (Guess tm cs) = pure $ Guess !(resolved gam tm) cs resolved gam t = pure t @@ -1569,6 +1573,12 @@ addDataDir dir = do defs <- get Ctxt put Ctxt (record { options->dirs->data_dirs $= (++ [dir]) } defs) +export +addLibDir : {auto c : Ref Ctxt Defs} -> String -> Core () +addLibDir dir + = do defs <- get Ctxt + put Ctxt (record { options->dirs->lib_dirs $= (++ [dir]) } defs) + export setBuildDir : {auto c : Ref Ctxt Defs} -> String -> Core () setBuildDir dir diff --git a/src/Core/Directory.idr b/src/Core/Directory.idr index 283ffb4..d27f370 100644 --- a/src/Core/Directory.idr +++ b/src/Core/Directory.idr @@ -36,7 +36,7 @@ dropExtension fname -- assert that root can't be empty reverse (assert_total (strTail root)) --- Return the contents of the first file available in the list +-- Return the name of the first file available in the list firstAvailable : List String -> Core (Maybe String) firstAvailable [] = pure Nothing firstAvailable (f :: fs) @@ -57,6 +57,21 @@ readDataFile fname | Left err => throw (FileErr f err) pure d +-- Look for a library file required by a code generator. Look in the +-- library directories, and in the lib/ subdirectoriy of all the 'extra import' +-- directories +export +findLibraryFile : {auto c : Ref Ctxt Defs} -> + String -> Core String +findLibraryFile fname + = do d <- getDirs + let fs = map (\p => p ++ cast sep ++ fname) + (lib_dirs d ++ map (\x => x ++ cast sep ++ "lib") + (extra_dirs d)) + Just f <- firstAvailable fs + | Nothing => throw (InternalError ("Can't find library " ++ fname)) + pure f + -- Given a namespace, return the full path to the checked module, -- looking first in the build directory then in the extra_dirs export diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 5f856c5..f052bf6 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -11,15 +11,17 @@ record Dirs where build_dir : String -- build directory, relative to working directory dir_prefix : String -- installation prefix, for finding data files (e.g. run time support) extra_dirs : List String -- places to look for import files + lib_dirs : List String -- places to look for libraries (for code generation) data_dirs : List String -- places to look for data file public export toString : Dirs -> String -toString (MkDirs wdir bdir dfix edirs ddirs) = +toString (MkDirs wdir bdir dfix edirs ldirs ddirs) = unlines [ "+ Working Directory :: " ++ show wdir , "+ Build Directory :: " ++ show bdir , "+ Installation Prefix :: " ++ show dfix , "+ Extra Directories :: " ++ show edirs + , "+ CG Library Directories :: " ++ show ldirs , "+ Data Directories :: " ++ show ddirs] public export @@ -105,7 +107,7 @@ record Options where extensions : List LangExt defaultDirs : Dirs -defaultDirs = MkDirs "." "build" "/usr/local" ["."] [] +defaultDirs = MkDirs "." "build" "/usr/local" ["."] ["."] [] defaultPPrint : PPrinter defaultPPrint = MkPPOpts False True False diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr index a8c5b1a..234e4ff 100644 --- a/src/Core/UnifyState.idr +++ b/src/Core/UnifyState.idr @@ -522,6 +522,11 @@ checkValidHole (idx, (fc, n)) Just gdef <- lookupCtxtExact (Resolved idx) (gamma defs) | Nothing => pure () case definition gdef of + BySearch _ _ _ => + do defs <- get Ctxt + Just ty <- lookupTyExact n (gamma defs) + | Nothing => pure () + throw (CantSolveGoal fc [] ty) Guess tm (con :: _) => do ust <- get UST let Just c = lookup con (constraints ust) @@ -550,7 +555,8 @@ checkValidHole (idx, (fc, n)) -- Bool flag says whether it's an error for there to have been holes left -- in the last session. Usually we can leave them to the end, but it's not -- valid for there to be holes remaining when checking a LHS. --- Also throw an error if there are unresolved guarded constants +-- Also throw an error if there are unresolved guarded constants or +-- unsolved searches export checkUserHoles : {auto u : Ref UST UState} -> {auto c : Ref Ctxt Defs} -> diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index a9f049f..3f70d96 100644 --- a/src/Idris/Elab/Interface.idr +++ b/src/Idris/Elab/Interface.idr @@ -303,20 +303,39 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body dty <- case lookup n tydecls of Just (_, _, t) => pure t Nothing => throw (GenericMsg fc ("No method named " ++ show n ++ " in interface " ++ show iname)) - log 5 $ "Default method " ++ show dn ++ " : " ++ show dty let ity = apply (IVar fc iname) (map (IVar fc) (map fst params)) - dty_imp <- bindTypeNames vars (bindIFace fc ity dty) + + -- Substitute the method names with their top level function + -- name, so they don't get implicitly bound in the name + methNameMap <- traverse (\n => + do cn <- inCurrentNS n + pure (n, applyParams (IVar fc cn) + (map fst params))) + (map fst tydecls) + let dty = substNames vars methNameMap dty + + dty_imp <- bindTypeNames (map fst tydecls ++ vars) + (bindIFace fc ity dty) + log 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp let dtydecl = IClaim fc RigW vis [] (MkImpTy fc dn dty_imp) processDecl [] nest env dtydecl let cs' = map (changeName dn) cs + log 5 $ "Default method body " ++ show cs' + processDecl [] nest env (IDef fc dn cs') -- Reset the original context, we don't need to keep the definition -- Actually we do for the metadata and name map! -- put Ctxt orig pure (n, cs) where + applyParams : RawImp -> List Name -> RawImp + applyParams tm [] = tm + applyParams tm (UN n :: ns) + = applyParams (IImplicitApp fc tm (Just (UN n)) (IBindVar fc n)) ns + applyParams tm (_ :: ns) = applyParams tm ns + changeNameTerm : Name -> RawImp -> RawImp changeNameTerm dn (IVar fc n') = if n == n' then IVar fc dn else IVar fc n' diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index a7d0d93..124bd6d 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -54,7 +54,6 @@ initIDESocketFile p = do putStrLn "Failed to open socket" exit 1 Right sock => do - putStrLn (show p) res <- bind sock (Just (Hostname "localhost")) p if res /= 0 then @@ -65,6 +64,7 @@ initIDESocketFile p = do then pure (Left ("Failed to listen on socket with error: " ++ show res)) else do + putStrLn (show p) res <- accept sock case res of Left err => @@ -231,7 +231,7 @@ loop processCatch cmd loop Nothing => - do printError "Unrecognised command" + do printError ("Unrecognised command: " ++ show sexp) loop where updateOutput : Integer -> Core () diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr index 6bf84f7..0e0d348 100644 --- a/src/Idris/Main.idr +++ b/src/Idris/Main.idr @@ -53,14 +53,21 @@ updatePaths Just path => do traverse addDataDir (map trim (split (==pathSep) path)) pure () Nothing => pure () - -- BLODWEN_PATH goes first so that it overrides this if there's - -- any conflicts. In particular, that means that setting BLODWEN_PATH + blibs <- coreLift $ getEnv "IDRIS2_LIBS" + case blibs of + Just path => do traverse addLibDir (map trim (split (==pathSep) path)) + pure () + Nothing => pure () + -- IDRIS2_PATH goes first so that it overrides this if there's + -- any conflicts. In particular, that means that setting IDRIS2_PATH -- for the tests means they test the local version not the installed -- version addPkgDir "prelude" addPkgDir "base" addDataDir (dir_prefix (dirs (options defs)) ++ dirSep ++ "idris2" ++ dirSep ++ "support") + addLibDir (dir_prefix (dirs (options defs)) ++ dirSep ++ + "idris2" ++ dirSep ++ "lib") updateREPLOpts : {auto o : Ref ROpts REPLOpts} -> Core () diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 6160d9c..0030cdb 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1285,7 +1285,7 @@ import_ fname indents pure (MkImport (MkFC fname start end) reexp ns nsAs) export -prog : FileName -> Rule Module +prog : FileName -> EmptyRule Module prog fname = do start <- location nspace <- option ["Main"] @@ -1293,7 +1293,7 @@ prog fname namespace_) end <- location imports <- block (import_ fname) - ds <- nonEmptyBlock (topDecl fname) + ds <- block (topDecl fname) pure (MkModule (MkFC fname start end) nspace imports (collectDefs (concat ds))) diff --git a/src/TTImp/Elab/Binders.idr b/src/TTImp/Elab/Binders.idr index 360cfcb..7a4d401 100644 --- a/src/TTImp/Elab/Binders.idr +++ b/src/TTImp/Elab/Binders.idr @@ -181,7 +181,7 @@ checkLet rigc_in elabinfo nest env fc rigl n nTy nVal scope expty nest env nVal (Just (gnf env tyv)) pure (fst c, snd c, Rig1) e => throw e) - let env' : Env Term (n :: _) = Let rigb valv tyv :: env + let env' : Env Term (n :: _) = Lam rigb Explicit tyv :: env let nest' = weaken (dropName n nest) expScope <- weakenExp env' expty (scopev, gscopet) <- diff --git a/src/TTImp/Elab/Hole.idr b/src/TTImp/Elab/Hole.idr index 766d85a..8cc11c3 100644 --- a/src/TTImp/Elab/Hole.idr +++ b/src/TTImp/Elab/Hole.idr @@ -26,6 +26,10 @@ checkHole : {vars : _} -> Core (Term vars, Glued vars) checkHole rig elabinfo nest env fc n_in (Just gexpty) = do nm <- inCurrentNS (UN n_in) + defs <- get Ctxt + Nothing <- lookupCtxtExact nm (gamma defs) + | _ => do log 1 $ show nm ++ " already defined" + throw (AlreadyDefined fc nm) expty <- getTerm gexpty -- Turn lets into lambda before making the hole so that they -- get abstracted over in the hole (it's fine here, unlike other @@ -42,6 +46,10 @@ checkHole rig elabinfo nest env fc n_in exp let env' = letToLam env ty <- metaVar fc Rig0 env' nmty (TType fc) nm <- inCurrentNS (UN n_in) + defs <- get Ctxt + Nothing <- lookupCtxtExact nm (gamma defs) + | _ => do log 1 $ show nm ++ " already defined" + throw (AlreadyDefined fc nm) (idx, metaval) <- metaVarI fc rig env' nm ty withCurrentLHS (Resolved idx) addUserHole nm diff --git a/src/TTImp/Interactive/GenerateDef.idr b/src/TTImp/Interactive/GenerateDef.idr index 2a22dbd..7ac5228 100644 --- a/src/TTImp/Interactive/GenerateDef.idr +++ b/src/TTImp/Interactive/GenerateDef.idr @@ -32,6 +32,20 @@ fnName lhs (NS _ n) = fnName lhs n fnName lhs (DN s _) = s fnName lhs n = show n +-- Make the hole on the RHS have a unique name +uniqueRHS : {auto c : Ref Ctxt Defs} -> + ImpClause -> Core ImpClause +uniqueRHS (PatClause fc lhs rhs) + = pure $ PatClause fc lhs !(mkUniqueName rhs) + where + mkUniqueName : RawImp -> Core RawImp + mkUniqueName (IHole fc' rhsn) + = do defs <- get Ctxt + rhsn' <- uniqueName defs [] rhsn + pure (IHole fc' rhsn') + mkUniqueName tm = pure tm -- it'll be a hole, but this is needed for covering +uniqueRHS c = pure c + expandClause : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto u : Ref UST UState} -> @@ -39,6 +53,7 @@ expandClause : {auto c : Ref Ctxt Defs} -> Core (List ImpClause) expandClause loc n c = do log 10 $ "Trying clause " ++ show c + c <- uniqueRHS c Just clause <- checkClause Rig1 False n [] (MkNested []) [] c | Nothing => pure [] -- TODO: impossible clause, do something -- appropriate @@ -90,7 +105,7 @@ trySplit : {auto m : Ref MD Metadata} -> trySplit loc lhsraw lhs rhs n = do OK updates <- getSplitsLHS loc 0 lhs n | _ => pure (n, []) - pure (n, map (\ups => PatClause loc (updateLHS ups lhsraw) rhs) + pure (n, map (\ups => PatClause loc (updateLHS ups lhsraw) rhs) (mapMaybe valid updates)) where valid : ClauseUpdate -> Maybe (List (Name, RawImp)) diff --git a/tests/Main.idr b/tests/Main.idr index b9baa64..76b197c 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -31,17 +31,19 @@ idrisTests "basic026", "basic027", "coverage001", "coverage002", "coverage003", "coverage004", "error001", "error002", "error003", "error004", "error005", - "error006", "error007", "error008", "error009", + "error006", "error007", "error008", "error009", "error010", "import001", "import002", "interactive001", "interactive002", "interactive003", "interactive004", "interactive005", "interactive006", "interactive007", "interactive008", "interactive009", "interactive010", "interactive011", "interactive012", "interface001", "interface002", "interface003", "interface004", "interface005", "interface006", "interface007", "interface008", - "interface009", "interface010", "interface011", + "interface009", "interface010", "interface011", "interface012", + "interface013", "lazy001", "linear001", "linear002", "linear003", "linear004", "linear005", "linear006", "linear007", + "perf001", "perror001", "perror002", "perror003", "perror004", "perror005", "perror006", "record001", "record002", @@ -69,10 +71,10 @@ fail err = do putStrLn err exitWith (ExitFailure 1) -runTest : String -> String -> String -> IO Bool -runTest dir prog test - = do chdir (dir ++ "/" ++ test) - putStr $ dir ++ "/" ++ test ++ ": " +runTest : String -> String -> IO Bool +runTest prog testPath + = do chdir testPath + putStr $ testPath ++ ": " system $ "sh ./run " ++ prog ++ " | tr -d '\\r' > output" Right out <- readFile "output" | Left err => do print err @@ -105,23 +107,39 @@ findChez Nothing => firstExists [p ++ x | p <- ["/usr/bin/", "/usr/local/bin/"], x <- ["scheme", "chez", "chezscheme9.5"]] +runChezTests : String -> List String -> IO (List Bool) +runChezTests prog tests + = do chexec <- findChez + maybe (do putStrLn "Chez Scheme not found" + pure []) + (\c => do putStrLn $ "Found Chez Scheme at " ++ c + traverse (runTest prog) tests) + chexec + main : IO () main - = do [_, idris2] <- getArgs - | _ => do putStrLn "Usage: runtests [ttimp path]" - ttimps <- traverse (runTest "ttimp" idris2) ttimpTests - idrs <- traverse (runTest "idris2" idris2) idrisTests - typedds <- traverse (runTest "typedd-book" 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 ++ typedds ++ idrs ++ chezs + = do args <- getArgs + let (_ :: idris2 :: _) = args + | _ => do putStrLn "Usage: runtests [--only ]" + let filterTests = case drop 2 args of + ("--only" :: onlyName :: _) => filter (\testName => isInfixOf onlyName testName) + _ => id + let filteredNonCGTests = + filterTests $ concat [testPaths "ttimp" ttimpTests, + testPaths "idris2" idrisTests, + testPaths "typedd-book" typeddTests] + let filteredChezTests = filterTests (testPaths "chez" chezTests) + nonCGTestRes <- traverse (runTest idris2) filteredNonCGTests + chezTestRes <- if length filteredChezTests > 0 + then runChezTests idris2 filteredChezTests + else pure [] + let res = nonCGTestRes ++ chezTestRes putStrLn (show (length (filter id res)) ++ "/" ++ show (length res) ++ " tests successful") if (any not res) then exitWith (ExitFailure 1) else exitWith ExitSuccess + where + testPaths : String -> List String -> List String + testPaths dir tests = map (\test => dir ++ "/" ++ test) tests diff --git a/tests/Makefile b/tests/Makefile index e1d77df..5c81407 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -1,7 +1,7 @@ IDRIS2 = ../../../idris2 test: - ../runtests $(IDRIS2) + @../runtests $(IDRIS2) --only $(only) clean: find . -name '*.ibc' | xargs rm -f diff --git a/tests/README.md b/tests/README.md new file mode 100644 index 0000000..6f5b5c8 --- /dev/null +++ b/tests/README.md @@ -0,0 +1,13 @@ +Tests +===== + +*Note: The commands listed in this section should be run from the repository's root folder.* + +Run all tests: `make test` + +To run only a subset of the tests use: `make test only=NAME`. `NAME` is matched against the path to each test case. + +Examples: +- `make test only=chez` will run all Chez Scheme tests. +- `make test only=ttimp/basic` will run all basic tests for `TTImp`. +- `make test only=idris2/basic001` will run a specific test. diff --git a/tests/idris2/error010/Loop.idr b/tests/idris2/error010/Loop.idr new file mode 100644 index 0000000..334f8d8 --- /dev/null +++ b/tests/idris2/error010/Loop.idr @@ -0,0 +1,2 @@ +example : String +example = ?example diff --git a/tests/idris2/error010/expected b/tests/idris2/error010/expected new file mode 100644 index 0000000..19bae6b --- /dev/null +++ b/tests/idris2/error010/expected @@ -0,0 +1,3 @@ +1/1: Building Loop (Loop.idr) +Loop.idr:2:11--3:1:While processing right hand side of Main.example at Loop.idr:2:1--3:1: +Main.example is already defined diff --git a/tests/idris2/error010/run b/tests/idris2/error010/run new file mode 100755 index 0000000..9980422 --- /dev/null +++ b/tests/idris2/error010/run @@ -0,0 +1,3 @@ +$1 Loop.idr --check + +rm -rf build diff --git a/tests/idris2/interactive002/IEdit.idr b/tests/idris2/interactive002/IEdit.idr index bde3689..fdeec47 100644 --- a/tests/idris2/interactive002/IEdit.idr +++ b/tests/idris2/interactive002/IEdit.idr @@ -15,5 +15,5 @@ suc : (x : Nat) -> (y : Nat) -> x = y -> S x = S y suc x y prf = ?quux suc' : x = y -> S x = S y -suc' {x} {y} prf = ?quux +suc' {x} {y} prf = ?quuz diff --git a/tests/idris2/interactive002/expected b/tests/idris2/interactive002/expected index 6429de8..d01104c 100644 --- a/tests/idris2/interactive002/expected +++ b/tests/idris2/interactive002/expected @@ -9,6 +9,6 @@ Main> vadd (x :: xs) (y :: ys) = ?baz_1 Main> suc x x Refl = ?quux_1 -Main> suc' {x = y} {y = y} Refl = ?quux_1 +Main> suc' {x = y} {y = y} Refl = ?quuz_1 Main> Bye for now! diff --git a/tests/idris2/interface012/Defmeth.idr b/tests/idris2/interface012/Defmeth.idr new file mode 100644 index 0000000..c152536 --- /dev/null +++ b/tests/idris2/interface012/Defmeth.idr @@ -0,0 +1,26 @@ + +import Data.Fin +import Data.Vect + +tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A) +tail f = f . FS + +toVect : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A +toVect {n = Z} _ = Nil +toVect {n = S m} f = (f FZ) :: (toVect (tail f)) + +record Iso a b where + constructor MkIso + to : a -> b + from : b -> a + toFrom : (y : b) -> to (from y) = y + fromTo : (x : a) -> from (to x) = x + +interface Finite t where + card : Nat + iso : Iso t (Fin card) + + -- default methods + + foo : Vect card t + foo = toVect (from iso) diff --git a/tests/idris2/interface012/expected b/tests/idris2/interface012/expected new file mode 100644 index 0000000..3a4e357 --- /dev/null +++ b/tests/idris2/interface012/expected @@ -0,0 +1 @@ +1/1: Building Defmeth (Defmeth.idr) diff --git a/tests/idris2/interface012/run b/tests/idris2/interface012/run new file mode 100755 index 0000000..a7e03a6 --- /dev/null +++ b/tests/idris2/interface012/run @@ -0,0 +1,3 @@ +$1 Defmeth.idr --check + +rm -rf build diff --git a/tests/idris2/interface013/TypeInt.idr b/tests/idris2/interface013/TypeInt.idr new file mode 100644 index 0000000..bccfcf2 --- /dev/null +++ b/tests/idris2/interface013/TypeInt.idr @@ -0,0 +1,14 @@ +-- %logging 5 + +interface Interface specifier where + 0 concrete : specifier -> Type + +record Value s where + constructor MkValue + specifier : s + +0 DependentValue : Interface s => Value s -> Type +DependentValue v = concrete (specifier v) + +data Record : s -> Type where + MkRecord : Value s -> DependentValue {s} value -> Record s diff --git a/tests/idris2/interface013/expected b/tests/idris2/interface013/expected new file mode 100644 index 0000000..9c6d231 --- /dev/null +++ b/tests/idris2/interface013/expected @@ -0,0 +1,3 @@ +1/1: Building TypeInt (TypeInt.idr) +TypeInt.idr:14:25--14:50:While processing constructor Main.MkRecord at TypeInt.idr:14:3--15:1: +Can't find an implementation for Interface ?s diff --git a/tests/idris2/interface013/run b/tests/idris2/interface013/run new file mode 100755 index 0000000..8db9ed5 --- /dev/null +++ b/tests/idris2/interface013/run @@ -0,0 +1,3 @@ +$1 TypeInt.idr --check + +rm -rf build diff --git a/tests/idris2/perf001/Big.idr b/tests/idris2/perf001/Big.idr new file mode 100644 index 0000000..9706bed --- /dev/null +++ b/tests/idris2/perf001/Big.idr @@ -0,0 +1,18 @@ +import Data.Vect + +test : Vect 33 Int -> IO Int +test bytes_list = do + let int1 = (index 0 bytes_list * 8) + + (index 1 bytes_list * 4) + + (index 2 bytes_list * 2) + (index 3 bytes_list) + let int2 = (index 4 bytes_list * 8) + (index 5 bytes_list * 4) + (index 6 bytes_list * 2) + (index 7 bytes_list) + let int3 = (index 8 bytes_list * 8) + (index 9 bytes_list * 4) + (index 10 bytes_list * 2) + (index 11 bytes_list) + let int4 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list) + let int5 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list) + let int6 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list) + let int7 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list) + let int8 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list) + let int9 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list) + let int10 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list) + pure int1 + diff --git a/tests/idris2/perf001/expected b/tests/idris2/perf001/expected new file mode 100644 index 0000000..57c29d0 --- /dev/null +++ b/tests/idris2/perf001/expected @@ -0,0 +1 @@ +1/1: Building Big (Big.idr) diff --git a/tests/idris2/perf001/run b/tests/idris2/perf001/run new file mode 100755 index 0000000..1402531 --- /dev/null +++ b/tests/idris2/perf001/run @@ -0,0 +1,3 @@ +$1 --check Big.idr + +rm -rf build