edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-10 06:05:31 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of https://github.com/edwinb/Idris2 into network-lib

Browse Source
This commit is contained in:
Arnaud Bailly 2019-07-28 23:00:07 +02:00
commit 4d3e190e90
No known key found for this signature in database
GPG Key ID: 389CC2BC5448321E
33 changed files with 275 additions and 43 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Makefile
View File

@ -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

11
src/Compiler/Common.idr
View File

@ -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)

3
src/Compiler/CompileExpr.idr
View File

@ -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])

26
src/Compiler/Scheme/Chez.idr
View File

@ -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

12
src/Core/Binary.idr
View File

@ -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)

10
src/Core/Context.idr
View File

@ -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

17
src/Core/Directory.idr
View File

@ -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

6
src/Core/Options.idr
View File

@ -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

8
src/Core/UnifyState.idr
View File

@ -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} ->

23
src/Idris/Elab/Interface.idr
View File

@ -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'

4
src/Idris/IDEMode/REPL.idr
View File

@ -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 ()

11
src/Idris/Main.idr
View File

@ -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 ()

4
src/Idris/Parser.idr
View File

@ -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)))

2
src/TTImp/Elab/Binders.idr
View File

@ -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) <-

8
src/TTImp/Elab/Hole.idr
View File

@ -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

17
src/TTImp/Interactive/GenerateDef.idr
View File

@ -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))

54
tests/Main.idr
View File

@ -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 <idris2 path> [--only <name>]"
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

2
tests/Makefile
View File

@ -1,7 +1,7 @@
IDRIS2 = ../../../idris2
test:
../runtests $(IDRIS2)
@../runtests $(IDRIS2) --only $(only)
clean:
find . -name '*.ibc' | xargs rm -f

13
tests/README.md Normal file
View File

@ -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.

2
tests/idris2/error010/Loop.idr Normal file
View File

@ -0,0 +1,2 @@
example : String
example = ?example

3
tests/idris2/error010/expected Normal file
View File

@ -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

3
tests/idris2/error010/run Executable file
View File

@ -0,0 +1,3 @@
$1 Loop.idr --check
rm -rf build

2
tests/idris2/interactive002/IEdit.idr
View File

@ -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

2
tests/idris2/interactive002/expected
View File

@ -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!

26
tests/idris2/interface012/Defmeth.idr Normal file
View File

@ -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)

1
tests/idris2/interface012/expected Normal file
View File

@ -0,0 +1 @@
1/1: Building Defmeth (Defmeth.idr)

3
tests/idris2/interface012/run Executable file
View File

@ -0,0 +1,3 @@
$1 Defmeth.idr --check
rm -rf build

14
tests/idris2/interface013/TypeInt.idr Normal file
View File

@ -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

3
tests/idris2/interface013/expected Normal file
View File

@ -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

3
tests/idris2/interface013/run Executable file
View File

@ -0,0 +1,3 @@
$1 TypeInt.idr --check
rm -rf build

18
tests/idris2/perf001/Big.idr Normal file
View File

@ -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

1
tests/idris2/perf001/expected Normal file
View File

@ -0,0 +1 @@
1/1: Building Big (Big.idr)

3
tests/idris2/perf001/run Executable file
View File

@ -0,0 +1,3 @@
$1 --check Big.idr
rm -rf build