edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-02 01:32:54 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #96 from abailly/add-version-command

Browse Source 
Add version command
This commit is contained in:
Edwin Brady 2019-09-23 22:54:36 +01:00 committed by GitHub
commit f9739b3f66
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
83 changed files with 194 additions and 128 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
Makefile
View File

@ -1,4 +1,8 @@
IDRIS2_VERSION := 0.0
# current Idris2 version components
MAJOR=0
MINOR=0
PATCH=0
IDRIS2_VERSION=${MAJOR}.${MINOR}.${PATCH}
PREFIX ?= ${HOME}/.idris2
IDRIS_VERSION := $(shell idris --version)
VALID_IDRIS_VERSION_REGEXP = "1.3.2.*"
@ -19,7 +23,7 @@ idris2: src/YafflePaths.idr check_version
idris --build idris2.ipkg
src/YafflePaths.idr:
echo 'module YafflePaths; export version : String; version = "${IDRIS2_VERSION}";' > src/YafflePaths.idr
echo 'module YafflePaths; export yversion : ((Nat,Nat,Nat), String); yversion = ((${MAJOR},${MINOR},${PATCH}), "")' > src/YafflePaths.idr
echo 'export yprefix : String; yprefix = "${PREFIX}"' >> src/YafflePaths.idr
prelude:

4
src/Idris/CommandLine.idr
View File

@ -2,6 +2,8 @@ module Idris.CommandLine
import YafflePaths
import Data.String
import Idris.Version
import YafflePaths
%default total
@ -143,7 +145,7 @@ optUsage d
export
versionMsg : String
versionMsg = "Idris 2, version " ++ version
versionMsg = "Idris 2, version " ++ showVersion version
export
usage : String

3
src/Idris/IDEMode/Commands.idr
View File

@ -25,6 +25,7 @@ data IDECommand
| MakeLemma Integer String
| MakeCase Integer String
| MakeWith Integer String
| Version
readHints : List SExp -> Maybe (List String)
readHints [] = Just []
@ -74,6 +75,7 @@ getIDECommand (SExpList [SymbolAtom "make-case", IntegerAtom l, StringAtom n])
= Just $ MakeCase l n
getIDECommand (SExpList [SymbolAtom "make-with", IntegerAtom l, StringAtom n])
= Just $ MakeWith l n
getIDECommand (SymbolAtom "version") = Just Version
getIDECommand _ = Nothing
export
@ -94,6 +96,7 @@ putIDECommand (GenerateDef line n) = (SExpList [SymbolAtom "generate-
putIDECommand (MakeLemma line n) = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n])
putIDECommand (MakeCase line n) = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n])
putIDECommand (MakeWith line n) = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n])
putIDECommand Version = SymbolAtom "version"
export
getMsg : SExp -> Maybe (IDECommand, Integer)

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

@ -187,6 +187,9 @@ process (MakeCase l n)
process (MakeWith l n)
= do Idris.REPL.process (Editing (MakeWith (fromInteger l) (UN n)))
pure ()
process Version
= do Idris.REPL.process ShowVersion
pure ()
processCatch : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->

9
src/Idris/Main.idr
View File

@ -19,9 +19,9 @@ import Idris.ProcessIdr
import Idris.REPL
import Idris.SetOptions
import Idris.Syntax
import Idris.Socket
import Idris.Socket.Data
import Idris.Version
import Data.Vect
import System
@ -65,9 +65,9 @@ updatePaths
addPkgDir "prelude"
addPkgDir "base"
addDataDir (dir_prefix (dirs (options defs)) ++ dirSep ++
"idris2-" ++ version ++ dirSep ++ "support")
"idris2-" ++ showVersion version ++ dirSep ++ "support")
addLibDir (dir_prefix (dirs (options defs)) ++ dirSep ++
"idris2-" ++ version ++ dirSep ++ "lib")
"idris2-" ++ showVersion version ++ dirSep ++ "lib")
updateREPLOpts : {auto o : Ref ROpts REPLOpts} ->
Core ()
@ -155,8 +155,7 @@ stMain opts
setOutput (IDEMode 0 file file)
replIDE {c} {u} {m}
else do
iputStrLn $ "Welcome to Idris 2 version " ++ version
++ ". Enjoy yourself!"
iputStrLn $ "Welcome to Idris 2. Enjoy yourself!"
repl {c} {u} {m}
else
-- exit with an error code if there was an error, otherwise

5
src/Idris/Package.idr
View File

@ -16,6 +16,7 @@ import Idris.ProcessIdr
import Idris.REPLOpts
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import Parser.Lexer
import Parser.Support
import Utils.Binary
@ -262,8 +263,8 @@ install pkg
(mainmod pkg)
srcdir <- coreLift currentDir
-- Make the package installation directory
let installPrefix = dir_prefix (dirs (options defs)) ++
dirSep ++ "idris2-" ++ version
let installPrefix = dir_prefix (dirs (options defs)) ++
dirSep ++ "idris2-" ++ showVersion version
True <- coreLift $ changeDir installPrefix
| False => throw (FileErr (name pkg) FileReadError)
Right _ <- coreLift $ mkdirs [name pkg]

93
src/Idris/REPL.idr
View File

@ -29,6 +29,7 @@ import Idris.Parser
import Idris.Resugar
import public Idris.REPLCommon
import Idris.Syntax
import Idris.Version
import TTImp.Elab
import TTImp.Elab.Check
@ -48,18 +49,18 @@ import System
showInfo : {auto c : Ref Ctxt Defs} ->
(Name, Int, GlobalDef) -> Core ()
showInfo (n, idx, d)
= do coreLift $ putStrLn (show (fullname d) ++ " ==> " ++
showInfo (n, idx, d)
= do coreLift $ putStrLn (show (fullname d) ++ " ==> " ++
show !(toFullNames (definition d)))
coreLift $ putStrLn (show (multiplicity d))
coreLift $ putStrLn ("Erasable args: " ++ show (eraseArgs d))
case compexpr d of
Nothing => pure ()
Just expr => coreLift $ putStrLn ("Compiled: " ++ show expr)
coreLift $ putStrLn ("Refers to: " ++
coreLift $ putStrLn ("Refers to: " ++
show !(traverse getFullName (keys (refersTo d))))
when (not (isNil (sizeChange d))) $
let scinfo = map (\s => show (fnCall s) ++ ": " ++
when (not (isNil (sizeChange d))) $
let scinfo = map (\s => show (fnCall s) ++ ": " ++
show (fnArgs s)) !(traverse toFullNames (sizeChange d)) in
coreLift $ putStrLn $
"Size change: " ++ showSep ", " scinfo
@ -69,7 +70,7 @@ isHole def
= case definition def of
Hole locs _ => Just locs
_ => Nothing
showCount : RigCount -> String
showCount Rig0 = " 0 "
showCount Rig1 = " 1 "
@ -90,14 +91,14 @@ tidy n = show n
showEnv : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> Env Term vars -> Name -> Nat -> Term vars ->
Defs -> Env Term vars -> Name -> Nat -> Term vars ->
Core (List (Name, String), String)
showEnv defs env fn (S args) (Bind fc x (Let c val ty) sc)
= showEnv defs env fn args (subst val sc)
showEnv defs env fn (S args) (Bind fc x b sc)
= do ity <- resugar env !(normalise defs env (binderType b))
let pre = if showName x
then showCount (multiplicity b) ++
then showCount (multiplicity b) ++
impBracket (implicitBind b) (tidy x ++ " : " ++ show ity) ++ "\n"
else ""
(envstr, ret) <- showEnv defs (b :: env) fn args sc
@ -116,12 +117,12 @@ showEnv defs env fn args ty
showHole : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> Env Term vars -> Name -> Nat -> Term vars ->
Defs -> Env Term vars -> Name -> Nat -> Term vars ->
Core String
showHole gam env fn args ty
= do (envs, ret) <- showEnv gam env fn args ty
pp <- getPPrint
let envs' = if showImplicits pp
let envs' = if showImplicits pp
then envs
else dropShadows envs
pure (concat (map snd envs') ++ ret)
@ -135,9 +136,9 @@ showHole gam env fn args ty
displayType : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> (Name, Int, GlobalDef) ->
Defs -> (Name, Int, GlobalDef) ->
Core String
displayType defs (n, i, gdef)
displayType defs (n, i, gdef)
= maybe (do tm <- resugar [] !(normaliseHoles defs [] (type gdef))
pure (show (fullname gdef) ++ " : " ++ show tm))
(\num => showHole defs [] n num (type gdef))
@ -153,7 +154,7 @@ getEnvTerm _ env tm = (_ ** (env, tm))
displayTerm : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> ClosedTerm ->
Defs -> ClosedTerm ->
Core String
displayTerm defs tm
= do ptm <- resugar [] !(normaliseHoles defs [] tm)
@ -161,7 +162,7 @@ displayTerm defs tm
displayPatTerm : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> ClosedTerm ->
Defs -> ClosedTerm ->
Core String
displayPatTerm defs tm
= do ptm <- resugarNoPatvars [] !(normaliseHoles defs [] tm)
@ -169,7 +170,7 @@ displayPatTerm defs tm
displayClause : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> (vs ** (Env Term vs, Term vs, Term vs)) ->
Defs -> (vs ** (Env Term vs, Term vs, Term vs)) ->
Core String
displayClause defs (vs ** (env, lhs, rhs))
= do lhstm <- resugar env !(normaliseHoles defs env lhs)
@ -178,7 +179,7 @@ displayClause defs (vs ** (env, lhs, rhs))
displayPats : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> (Name, Int, GlobalDef) ->
Defs -> (Name, Int, GlobalDef) ->
Core String
displayPats defs (n, idx, gdef)
= case definition gdef of
@ -191,16 +192,16 @@ displayPats defs (n, idx, gdef)
setOpt : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
REPLOpt -> Core ()
setOpt (ShowImplicits t)
setOpt (ShowImplicits t)
= do pp <- getPPrint
setPPrint (record { showImplicits = t } pp)
setOpt (ShowNamespace t)
setOpt (ShowNamespace t)
= do pp <- getPPrint
setPPrint (record { fullNamespace = t } pp)
setOpt (ShowTypes t)
setOpt (ShowTypes t)
= do opts <- get ROpts
put ROpts (record { showTypes = t } opts)
setOpt (EvalMode m)
setOpt (EvalMode m)
= do opts <- get ROpts
put ROpts (record { evalMode = m } opts)
setOpt (Editor e)
@ -212,7 +213,7 @@ setOpt (CG e)
Nothing => coreLift $ putStrLn "No such code generator available"
findCG : {auto c : Ref Ctxt Defs} -> Core Codegen
findCG
findCG
= do defs <- get Ctxt
case codegen (session (options defs)) of
Chez => pure codegenChez
@ -248,9 +249,9 @@ execExp ctm
inidx <- resolveName (UN "[input]")
(tm, ty) <- elabTerm inidx InExpr [] (MkNested [])
[] ttimp Nothing
tm_erased <- linearCheck replFC Rig1 True [] tm
tm_erased <- linearCheck replFC Rig1 True [] tm
execute !findCG tm_erased
anyAt : (FC -> Bool) -> FC -> a -> Bool
anyAt p loc y = p loc
@ -272,7 +273,7 @@ printClause i (ImpossibleClause _ lhsraw)
= do lhs <- pterm lhsraw
pure (pack (replicate i ' ') ++ show lhs ++ " impossible")
lookupDefTyName : Name -> Context ->
lookupDefTyName : Name -> Context ->
Core (List (Name, Int, (Def, ClosedTerm)))
lookupDefTyName = lookupNameBy (\g => (definition g, type g))
@ -318,25 +319,25 @@ processEdit (ExprSearch line name hints all)
do tms <- exprSearch replFC name []
defs <- get Ctxt
restms <- traverse (normaliseHoles defs []) tms
itms <- the (Core (List PTerm))
(traverse (\tm =>
itms <- the (Core (List PTerm))
(traverse (\tm =>
do let (_ ** (env, tm')) = dropLams locs [] tm
resugar env tm') restms)
if all
then printResult $ showSep "\n" (map show itms)
else case itms of
[] => printError "No search results"
(x :: xs) => printResult
(show (if brack
(x :: xs) => printResult
(show (if brack
then addBracket replFC x
else x))
[] => printError $ "Unknown name " ++ show name
_ => printError "Not a searchable hole"
where
dropLams : Nat -> Env Term vars -> Term vars ->
dropLams : Nat -> Env Term vars -> Term vars ->
(vars' ** (Env Term vars', Term vars'))
dropLams Z env tm = (_ ** (env, tm))
dropLams (S k) env (Bind _ _ b sc) = dropLams k (b :: env) sc
dropLams (S k) env (Bind _ _ b sc) = dropLams k (b :: env) sc
dropLams _ env tm = (_ ** (env, tm))
processEdit (GenerateDef line name)
= do defs <- get Ctxt
@ -344,7 +345,7 @@ processEdit (GenerateDef line name)
| Nothing => printError ("Can't find declaration for " ++ show name ++ " on line " ++ show line)
case !(lookupDefExact n' (gamma defs)) of
Just None =>
catch
catch
(do Just (fc, cs) <- makeDef (\p, n => onLine line p) n'
| Nothing => processEdit (AddClause line name)
ls <- traverse (printClause (cast (snd (startPos fc)))) cs
@ -368,7 +369,7 @@ processEdit (MakeLemma line name)
case idemode opts of
REPL _ => printResult (show name ++ " : " ++ show pty ++ "\n" ++ pappstr)
IDEMode i _ f =>
send f (SExpList [SymbolAtom "return",
send f (SExpList [SymbolAtom "return",
SExpList [SymbolAtom "ok",
SExpList [SymbolAtom "metavariable-lemma",
SExpList [SymbolAtom "replace-metavariable",
@ -411,7 +412,7 @@ process (Eval itm)
= do opts <- get ROpts
case evalMode opts of
Execute => do execExp itm; pure True
_ =>
_ =>
do ttimp <- desugar AnyExpr [] itm
inidx <- resolveName (UN "[input]")
(tm, gty) <- elabTerm inidx (emode (evalMode opts)) [] (MkNested [])
@ -501,24 +502,24 @@ process (ProofSearch n_in)
coreLift (putStrLn (show itm))
pure True
process (Missing n)
= do defs <- get Ctxt
= do defs <- get Ctxt
case !(lookupCtxtName n (gamma defs)) of
[] => throw (UndefinedName replFC n)
ts => do traverse (\fn =>
do tot <- getTotality replFC fn
the (Core ()) $ case isCovering tot of
MissingCases cs =>
MissingCases cs =>
do tms <- traverse (displayPatTerm defs) cs
printResult (show fn ++ ":\n" ++
showSep "\n" tms)
NonCoveringCall ns_in =>
do ns <- traverse getFullName ns_in
printResult
(show fn ++ ": Calls non covering function"
printResult
(show fn ++ ": Calls non covering function"
++ case ns of
[fn] => " " ++ show fn
_ => "s: " ++ showSep ", " (map show ns))
_ => iputStrLn (show fn ++ ": All cases covered"))
_ => iputStrLn (show fn ++ ": All cases covered"))
(map fst ts)
pure True
process (Total n)
@ -528,7 +529,7 @@ process (Total n)
ts => do traverse (\fn =>
do checkTotal replFC fn
tot <- getTotality replFC fn
iputStrLn (show fn ++ " is " ++ show !(toFullNames tot)))
iputStrLn (show fn ++ " is " ++ show !(toFullNames tot)))
(map fst ts)
pure True
process (DebugInfo n)
@ -559,11 +560,23 @@ process (Editing cmd)
processEdit cmd
setPPrint ppopts
pure True
process Quit
process Quit
= do iputStrLn "Bye for now!"
pure False
process NOP
= pure True
process ShowVersion
= do opts <- get ROpts
case idemode opts of
REPL _ => iputStrLn $ showVersion version
IDEMode i _ f => do
let MkVersion (maj, min, patch) t = version
send f (SExpList [SymbolAtom "return",
SExpList [SymbolAtom "ok",
SExpList [SExpList (map (IntegerAtom . cast) [maj, min, patch]),
SExpList [ StringAtom $ fromMaybe "" t ]]],
toSExp i])
pure False
processCatch : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->

7
src/Idris/SetOptions.idr
View File

@ -9,6 +9,7 @@ import Core.Unify
import Idris.CommandLine
import Idris.REPL
import Idris.Syntax
import Idris.Version
import YafflePaths
@ -21,12 +22,12 @@ addPkgDir : {auto c : Ref Ctxt Defs} ->
addPkgDir p
= do defs <- get Ctxt
addExtraDir (dir_prefix (dirs (options defs)) ++ dirSep ++
"idris2-" ++ version ++ dirSep ++ p)
"idris2-" ++ showVersion version ++ dirSep ++ p)
dirOption : Dirs -> DirCommand -> Core ()
dirOption dirs LibDir
= coreLift $ putStrLn
(dir_prefix dirs ++ dirSep ++ "idris2-" ++ version ++ dirSep)
= coreLift $ putStrLn
(dir_prefix dirs ++ dirSep ++ "idris2-" ++ showVersion version ++ dirSep)
-- Options to be processed before type checking. Return whether to continue.
export

1
src/Idris/Syntax.idr
View File

@ -279,6 +279,7 @@ data REPLCmd : Type where
SetLog : Nat -> REPLCmd
Metavars : REPLCmd
Editing : EditCmd -> REPLCmd
ShowVersion : REPLCmd
Quit : REPLCmd
NOP : REPLCmd

32
src/Idris/Version.idr Normal file
View File

@ -0,0 +1,32 @@
||| Sets and display version of Idris.
module Idris.Version
import YafflePaths
||| Semantic versioning with optional tag
||| See [semver](https://semver.org/) for proper definition of semantic versioning
public export
record Version where
constructor MkVersion
||| Semantic version
||| Should follow the (major, minor, patch) convention
semVer : (Nat, Nat, Nat)
||| Optional tag
||| Usually contains git sha1 of this software's build in between releases
versionTag : Maybe String
export
version : Version
version with (yversion)
| (s,"") = MkVersion s Nothing
| (s,t) = MkVersion s (Just t)
export
showVersion : Version -> String
showVersion (MkVersion (maj,min,patch) versionTag) =
concat (intersperse "." (map show [ maj, min, patch])) ++ showTag
where
showTag : String
showTag = case versionTag of
Nothing => ""
Just tag => "-" ++ tag

2
tests/Main.idr
View File

@ -66,7 +66,7 @@ chezTests
ideModeTests : List String
ideModeTests
= [ "ideMode001" ]
= [ "ideMode001", "ideMode002" ]
chdir : String -> IO Bool
chdir dir

2
tests/chez/chez001/expected
View File

@ -1,4 +1,4 @@
[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]
1/1: Building Total (Total.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main> Bye for now!

2
tests/chez/chez002/expected
View File

@ -1,4 +1,4 @@
[(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)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main> Bye for now!

2
tests/chez/chez003/expected
View File

@ -3,5 +3,5 @@
188
188
1/1: Building IORef (IORef.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main> Bye for now!

2
tests/chez/chez004/expected
View File

@ -6,5 +6,5 @@
[0, 94, 0, 0, 0, 0, 0, 0, 0, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 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, 0]
[0, 94, 0, 0, 0, 0, 0, 0, 0, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 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, 0]
1/1: Building Buffer (Buffer.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main> Bye for now!

2
tests/chez/chez005/expected
View File

@ -1,4 +1,4 @@
(3 ** [2, 4, 6])
1/1: Building Filter (Filter.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main> Bye for now!

2
tests/chez/chez006/expected
View File

@ -10,7 +10,7 @@
43
42
1/1: Building TypeCase (TypeCase.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main> Main.strangeId is total
Main> Main.strangeId':
strangeId' _

2
tests/chez/chez007/expected
View File

@ -2,5 +2,5 @@
"Function from Nat to Vector of 0 Int"
"Function on Type"
1/1: Building TypeCase (TypeCase.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main> Bye for now!

2
tests/chez/chez008/expected
View File

@ -2,5 +2,5 @@
1
1
1/1: Building Nat (Nat.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main> Bye for now!

3
tests/ideMode/ideMode002/expected Normal file
View File

@ -0,0 +1,3 @@
000018(:protocol-version 2 0)
000021(:return (:ok ((0 0 0) (""))) 1)
Alas the file is done, aborting

1
tests/ideMode/ideMode002/input Normal file
View File

@ -0,0 +1 @@
00000c(:version 1)

3
tests/ideMode/ideMode002/run Executable file
View File

@ -0,0 +1,3 @@
$1 --ide-mode < input
rm -rf build

2
tests/idris2/basic001/expected
View File

@ -1,5 +1,5 @@
1/1: Building Vect (Vect.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main> Cons (S Z) (Cons (S (S Z)) []) : Vect (S (S Z)) Nat
Main> (interactive):1:28--1:51:When unifying Vect (S (S Z)) Nat and Vect (S Z) Nat
Mismatch between:

2
tests/idris2/basic002/expected
View File

@ -1,5 +1,5 @@
1/1: Building Do (Do.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Just (S (S (S Z)))
Main> Just Z
Main> Just (S (S (S Z)))

4
tests/idris2/basic003/expected
View File

@ -1,10 +1,10 @@
1/1: Building Ambig1 (Ambig1.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Bye for now!
1/1: Building Ambig2 (Ambig2.idr)
Ambig2.idr:22:21--22:28:While processing right hand side of Main.keepUnique at Ambig2.idr:22:1--24:1:
Ambiguous elaboration. Possible correct results:
Main.Set.toList ?arg
Main.Vect.toList ?arg
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Bye for now!

2
tests/idris2/basic004/expected
View File

@ -1,6 +1,6 @@
1/2: Building Stuff (Stuff.idr)
2/2: Building Wheres (Wheres.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Wheres> [3, 2, 1]
Wheres> 8
Wheres> 84

2
tests/idris2/basic005/expected
View File

@ -2,5 +2,5 @@
NoInfer.idr:1:7--1:9:Unsolved holes:
Main.{_:1} introduced at NoInfer.idr:1:7--1:9
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Bye for now!

2
tests/idris2/basic006/expected
View File

@ -1,6 +1,6 @@
1/2: Building Stuff (Stuff.idr)
2/2: Building PMLet (PMLet.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> 99
Main> 64
Main> Bye for now!

2
tests/idris2/basic007/expected
View File

@ -1,6 +1,6 @@
1/2: Building Stuff (Stuff.idr)
2/2: Building DoLocal (DoLocal.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Just 1
Main> Just 0
Main> Just 94

2
tests/idris2/basic008/expected
View File

@ -1,5 +1,5 @@
1/1: Building If (If.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> "Zero"
Main> "Odd"
Main> "Even"

2
tests/idris2/basic009/expected
View File

@ -1,6 +1,6 @@
1/2: Building Stuff (Stuff.idr)
2/2: Building LetCase (LetCase.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> y : Nat
res : Nat
x : Nat

2
tests/idris2/basic010/expected
View File

@ -1,5 +1,5 @@
1/1: Building Comp (Comp.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main> Main.comp : {0 a : Type} -> {0 c : Type} -> {0 b : Type} -> (b -> c) -> (a -> b) -> a -> c
Main> Main.comp2 : {0 c : Type} -> {0 b : Type} -> (b -> c) -> {a : Type} -> (a -> b) -> a -> c
Main> Bye for now!

2
tests/idris2/basic017/expected
View File

@ -3,6 +3,6 @@ CaseInf.idr:6:17--6:24:While processing right hand side of Main.test3bad at Case
Ambiguous elaboration. Possible correct results:
Builtin.Pair (Prelude.fromInteger 1) (Prelude.fromInteger 2)
Builtin.MkPair (Prelude.fromInteger 1) (Prelude.fromInteger 2)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> S (S (S Z))
Main> Bye for now!

2
tests/idris2/basic019/expected
View File

@ -1,5 +1,5 @@
1/1: Building CaseBlock (CaseBlock.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main.foo : (x : Nat) -> (case x of { Z => Nat -> Nat ; S k => Nat })
Main> Prelude.elem : Eq a => a -> List a -> Bool
elem x [] = False

2
tests/idris2/basic020/expected
View File

@ -1,5 +1,5 @@
1/1: Building Mut (Mut.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> MyTrue
Main> MyFalse
Main> (True, False)

2
tests/idris2/basic021/expected
View File

@ -1,5 +1,5 @@
1/1: Building CaseDep (CaseDep.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main.foo : Nat -> (x : Bool) -> IntOrChar x -> String
foo num x i = if x then show num else show i
Main> Bye for now!

2
tests/idris2/basic022/expected
View File

@ -1,6 +1,6 @@
1/1: Building Erase (Erase.idr)
Erase.idr:5:1--6:1:Attempt to match on erased argument False in Main.bad
Erase.idr:19:1--20:1:Attempt to match on erased argument LeZ in Main.minusBad
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> \m => minus (S (S m)) m prf
Main> Bye for now!

2
tests/idris2/basic023/expected
View File

@ -1,5 +1,5 @@
1/1: Building Params (Params.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main.Dict : (a -> a -> Bool) -> Type -> Type
Main> Main.MkDict : (eq : (a -> a -> Bool)) -> List (a, b) -> Dict eq b
Main> Main.lookup : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b

2
tests/idris2/basic024/expected
View File

@ -1,5 +1,5 @@
1/1: Building PatLam (PatLam.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> [(2, 3), (4, 5), (6, 7)]
Main> [S (S (S Z)), S (S (S (S Z))), S (S (S (S (S Z))))]
Main> Bye for now!

2
tests/idris2/basic025/expected
View File

@ -1,4 +1,4 @@
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
Main> [1, 3, 5, 7, 9]
Main> [10, 9, 8, 7, 6, 5, 4, 3, 2, 1]

2
tests/idris2/basic028/expected
View File

@ -1,4 +1,4 @@
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> 1/1: Building Do (Do.idr)
Main> Just (S (S (S Z)))
Main> Just Z

2
tests/idris2/coverage001/expected
View File

@ -1,5 +1,5 @@
1/1: Building Vect (Vect.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main.append:
append (_ :: _) _
Main> Main.lookup: All cases covered

2
tests/idris2/coverage002/expected
View File

@ -1,5 +1,5 @@
1/1: Building Vect (Vect.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main.append: All cases covered
Main> Main.funny: All cases covered
Main> Main.notFunny:

2
tests/idris2/coverage003/expected
View File

@ -1,7 +1,7 @@
1/1: Building Cover (Cover.idr)
Cover.idr:14:1--14:8:While processing left hand side of Main.badBar at Cover.idr:14:1--15:1:
Can't match on Z as it has a polymorphic type
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main.foo:
foo (Z, S _)
foo (S _, _)

2
tests/idris2/coverage004/expected
View File

@ -1,7 +1,7 @@
1/1: Building Cover (Cover.idr)
Cover.idr:12:1--12:5:While processing left hand side of Main.bad at Cover.idr:12:1--13:1:
Can't match on Just (fromInteger 0) as it has a polymorphic type
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main.okay:
okay (S _) IsNat
okay False IsBool

2
tests/idris2/error008/expected
View File

@ -1,3 +1,3 @@
File error in DoesntExist.idr: File Not Found
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Bye for now!

2
tests/idris2/error009/expected
View File

@ -1,3 +1,3 @@
Exists.idr:1:1--3:1:DoesntExist not found
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Bye for now!

4
tests/idris2/import001/expected
View File

@ -1,10 +1,10 @@
1/3: Building Nat (Nat.idr)
2/3: Building Mult (Mult.idr)
3/3: Building Test (Test.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Test> S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))
Test> Bye for now!
2/3: Building Mult (Mult.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Test> S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))
Test> Bye for now!

2
tests/idris2/import002/expected
View File

@ -4,5 +4,5 @@
Test.idr:5:9--5:13:While processing type of Test.thing at Test.idr:5:1--6:1:
Name Nat.Nat is inaccessible since Nat is not explicitly imported
Test.idr:6:1--8:1:No type declaration for Test.thing
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Test> Bye for now!

4
tests/idris2/import003/expected
View File

@ -1,9 +1,9 @@
1/2: Building A (A.idr)
2/2: Building B (B.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
B> 1 hole: A.defA
B> Bye for now!
2/2: Building C (C.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
C> 1 hole: C.newHole
C> Bye for now!

2
tests/idris2/interactive001/expected
View File

@ -1,5 +1,5 @@
1/1: Building LocType (LocType.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main.Vect : Nat -> Type -> Type
Main> xs : Vect k a
Main> Bye for now!

2
tests/idris2/interactive002/expected
View File

@ -1,5 +1,5 @@
1/1: Building IEdit (IEdit.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> append {n = Z} [] ys = ?foo_1
append {n = (S k)} (x :: xs) ys = ?foo_2

4
tests/idris2/interactive003/expected
View File

@ -1,5 +1,5 @@
1/1: Building IEdit (IEdit.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> [] => ?bar_1
(x :: zs) => ?bar_2
@ -8,7 +8,7 @@ Main> map f (MkFoo x) = ?baz_1
Main> Bye for now!
1/1: Building IEdit2 (IEdit2.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> (x :: []) => ?bar_5
(x :: (y :: zs)) => ?bar_6

2
tests/idris2/interactive004/expected
View File

@ -1,5 +1,5 @@
1/1: Building IEdit (IEdit.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> f (x, y)
Main> f (fst x) (snd x)
Main> ys

2
tests/idris2/interactive005/expected
View File

@ -1,5 +1,5 @@
1/1: Building IEdit (IEdit.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> my_cong x x Refl = Refl
Main> curry f x y = f (x, y)
Main> uncurry f x = f (fst x) (snd x)

2
tests/idris2/interactive006/expected
View File

@ -1,5 +1,5 @@
1/1: Building IEdit (IEdit.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> empties : (m : Nat) -> Vect m (Vect Z a)
empties m
Main> transposeHelper : Vect k (Vect m a) -> Vect m a -> Vect m (Vect k a) -> Vect m (Vect (S k) a)

2
tests/idris2/interactive007/expected
View File

@ -1,5 +1,5 @@
1/1: Building IEdit (IEdit.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys
Main> Bye for now!

2
tests/idris2/interactive008/expected
View File

@ -1,5 +1,5 @@
1/1: Building IEdit (IEdit.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> \f => \g => \x => g (f x)
Main> (\x => \zs => x :: zs)
Main> f : a -> b -> c

2
tests/idris2/interactive009/expected
View File

@ -1,5 +1,5 @@
1/1: Building Door (Door.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> (y @@ res) => ?now_4
Main> (True @@ d) => ?now_4

2
tests/idris2/interactive010/expected
View File

@ -1,5 +1,5 @@
1/1: Building IEdit (IEdit.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> zipHere [] ys = []
zipHere (x :: xs) (y :: ys) = (x, y) :: zipHere xs ys
Main> Bye for now!

2
tests/idris2/interactive011/expected
View File

@ -1,5 +1,5 @@
1/1: Building IEdit (IEdit.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> natElim p x f Z = x
natElim p x f (S k) = f k (natElim p x f k)
Main> f k (natElim2 p x f k)

2
tests/idris2/interactive012/expected
View File

@ -1,5 +1,5 @@
1/1: Building WithLift (WithLift.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> succNotZero : (S k) = Z -> Void
succNotZero
Main> recNotEqLift : (k = j -> Void) -> (S k) = (S j) -> Void

4
tests/idris2/interface001/expected
View File

@ -1,11 +1,11 @@
1/2: Building Stuff (Stuff.idr)
2/2: Building IFace (IFace.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
IFace> True
IFace> False
IFace> Bye for now!
2/2: Building IFace1 (IFace1.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
IFace1> conArg : (DecEq a, Eq (p t))
0 a : Type
0 p : a -> Type

2
tests/idris2/interface002/expected
View File

@ -1,6 +1,6 @@
1/2: Building Stuff (Stuff.idr)
2/2: Building Functor (Functor.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> 0 b : Type
0 a : Type
0 d : Type

2
tests/idris2/interface003/expected
View File

@ -1,5 +1,5 @@
1/1: Building Do (Do.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> 0 b : Type
0 a' : Type
0 a : Type

2
tests/idris2/interface004/expected
View File

@ -1,5 +1,5 @@
1/1: Building Do (Do.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Just 9
Main> Nothing
Main> Bye for now!

2
tests/idris2/interface009/expected
View File

@ -1,5 +1,5 @@
1/1: Building Odd (Odd.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> 0 v : Type
0 k' : Type
0 k : Type

2
tests/idris2/lazy001/expected
View File

@ -1,5 +1,5 @@
1/1: Building Lazy (Lazy.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> 1 :: Delay ones
Main> [1, 1, 1, 1]
Main> Bye for now!

2
tests/idris2/linear001/expected
View File

@ -1,4 +1,4 @@
1/2: Building Stuff (Stuff.idr)
2/2: Building Door (Door.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Bye for now!

2
tests/idris2/linear002/expected
View File

@ -1,6 +1,6 @@
1/2: Building Stuff (Stuff.idr)
2/2: Building Door (Door.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> 0 m : Type -> Type
0 d : Door Closed
1 d' : Door Open

2
tests/idris2/linear003/expected
View File

@ -1,5 +1,5 @@
1/1: Building Linear (Linear.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> 0 y : Nat
1 x : Nat
-------------------------------------

2
tests/idris2/linear004/expected
View File

@ -1,6 +1,6 @@
1/2: Building Stuff (Stuff.idr)
2/2: Building Erase (Erase.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> S Z
Main> S (S Z)
Main> S Z

2
tests/idris2/linear005/expected
View File

@ -1,6 +1,6 @@
1/2: Building Linear (Linear.idr)
2/2: Building Door (Door.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Door> 0 m : Type -> Type
1 d : Door Closed
-------------------------------------

2
tests/idris2/linear006/expected
View File

@ -1,6 +1,6 @@
1/1: Building ZFun (ZFun.idr)
ZFun.idr:13:7--15:1:While processing right hand side of Main.bar at ZFun.idr:13:1--15:1:
Trying to use irrelevant name Main.test in relevant context
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> [tc] Main> S (S (S (S (S (S (S (S (S (S Z)))))))))
[tc] Main> Bye for now!

2
tests/idris2/record001/expected
View File

@ -1,5 +1,5 @@
1/1: Building Record (Record.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> [1, 2, 3, 4, 5]
Main> [1, 2, 3, 4, 5]
Main> some_fn testPerson : Nat -> Nat

2
tests/idris2/record002/expected
View File

@ -1,5 +1,5 @@
1/1: Building Record (Record.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> MkPerson "Fred" 1337 10 (MkStats 11 10)
Main> MkPerson "Fred" 1337 10 (MkStats 12 10)
Main> MkMyDPair (S (S (S (S (S (S Z)))))) [10, 1, 2, 3, 4, 5]

2
tests/idris2/total001/expected
View File

@ -1,5 +1,5 @@
1/1: Building Total (Total.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main.lookup: All cases covered
Main> Main.lookup':
lookup' FZ _

2
tests/idris2/total002/expected
View File

@ -1,5 +1,5 @@
1/1: Building Total (Total.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main.noFinZ: All cases covered
Main> Main.noFinZ': All cases covered
Main> Main.noEmpty: All cases covered

2
tests/idris2/total003/expected
View File

@ -1,5 +1,5 @@
1/1: Building Total (Total.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main.onlyOne:
onlyOne _
Main> Main.covered: All cases covered

2
tests/idris2/total004/expected
View File

@ -1,5 +1,5 @@
1/1: Building Total (Total.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main.ack is total
Main> Main.foo is total
Main> Main.ordElim is total

2
tests/idris2/total005/expected
View File

@ -1,5 +1,5 @@
1/1: Building Total (Total.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main.Bad is not strictly positive
Main> Main.Bad1 is not strictly positive
Main> Main.Bad2 is not terminating due to call to Main.Bad1

2
tests/idris2/total006/expected
View File

@ -1,5 +1,5 @@
1/1: Building Total (Total.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Welcome to Idris 2. Enjoy yourself!
Main> Main.count is total
Main> Main.badCount is not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:816:1--820:1 -> Prelude.map
Main> Main.process is total

2
tests/typedd-book/chapter01/expected
View File

@ -2,7 +2,7 @@
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!
Welcome to Idris 2. Enjoy yourself!
Main> -------------------------------------
convert : Char -> String
Main> Bye for now!