idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 20:23:11 +03:00
Code Issues Projects Releases Wiki Activity

Merge remote-tracking branch 'upstream/master' into code-in-errors

Browse Source
This commit is contained in:
Giuseppe Lomurno 2020-06-13 18:20:12 +02:00
commit c995fe4a01
46 changed files with 355 additions and 188 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
CHANGELOG.md
View File

@ -18,6 +18,15 @@ Language changes:
invoking elaborator scripts. This means the function must always
be fully applied, and is run under `%runElab`
Library changes:
* Experimental `Data.Linear.Array` added to `contrib`, support mutable linear
arrays with constant time read/write, convertible to immutable arrays with
constant time read.
+ Anything in `Data.Linear` in `contrib`, just like the rest of `contrib`,
should be considered experimental with the API able to change at any time!
Further experiments in `Data.Linear` are welcome :).
Changes since Idris 2 v0.1.0
----------------------------

18
docs/source/app/linear.rst
View File

@ -83,7 +83,7 @@ access the resource directly:
.. code-block:: idris
data Res : (a : Type) -> (a -> Type) -> Type where
(@@) : (val : a) -> (1 resource : r val) -> Res a r
(#) : (val : a) -> (1 resource : r val) -> Res a r
login : (1 s : Store LoggedOut) -> (password : String) ->
Res Bool (\ok => Store (if ok then LoggedIn else LoggedOut))
@ -91,7 +91,7 @@ access the resource directly:
readSecret : (1 s : Store LoggedIn) ->
Res String (const (Store LoggedIn))
``Res`` is defined in ``Control.App`` since it is commonly useful. It is a
``Res`` is defined in the Prelude, since it is commonly useful. It is a
dependent pair type, which associates a value with a linear resource.
We'll leave the other definitions abstract, for the purposes of this
introductory example.
@ -108,10 +108,10 @@ secret data. It uses ``let (>>=) = bindL`` to redefine
do putStr "Password: "
password <- getStr
connect $ \s =>
do let True @@ s = login s password
| False @@ s => do putStrLn "Wrong password"
disconnect s
let str @@ s = readSecret s
do let True # s = login s password
| False # s => do putStrLn "Wrong password"
disconnect s
let str # s = readSecret s
putStrLn $ "Secret: " ++ show str
let s = logout s
disconnect s
@ -237,10 +237,10 @@ hard coded password and internal data:
login (MkStore str) pwd
= if pwd == "Mornington Crescent"
then pure1 (True @@ MkStore str)
else pure1 (False @@ MkStore str)
then pure1 (True # MkStore str)
else pure1 (False # MkStore str)
logout (MkStore str) = pure1 (MkStore str)
readSecret (MkStore str) = pure1 (str @@ MkStore str)
readSecret (MkStore str) = pure1 (str # MkStore str)
disconnect (MkStore _)
= putStrLn "Door destroyed"

6
libs/base/Control/App.idr
View File

@ -339,8 +339,6 @@ HasErr Void e => PrimIO e where
$ \_ =>
MkAppRes (Right ())
infix 5 @@
export
new1 : t -> (1 p : State tag t e => App1 {u} e a) -> App1 {u} e a
new1 val prog
@ -349,10 +347,6 @@ new1 val prog
MkApp1 res = prog @{st} in
res
public export
data Res : (a : Type) -> (a -> Type) -> Type where
(@@) : (val : a) -> (1 r : t val) -> Res a t
public export
data FileEx = GenericFileEx Int -- errno
| FileReadError

11
libs/base/Data/IOArray.idr
View File

@ -1,17 +1,8 @@
module Data.IOArray
import Data.IOArray.Prims
import Data.List
-- Implemented externally
data ArrayData : Type -> Type where
-- 'unsafe' primitive access, backend dependent
-- get and set assume that the bounds have been checked. Behavious is undefined
-- otherwise.
%extern prim__newArray : forall a . Int -> a -> PrimIO (ArrayData a)
%extern prim__arrayGet : forall a . ArrayData a -> Int -> PrimIO a
%extern prim__arraySet : forall a . ArrayData a -> Int -> a -> PrimIO ()
export
record IOArray elem where
constructor MkIOArray

11
libs/base/Data/IOArray/Prims.idr Normal file
View File

@ -0,0 +1,11 @@
module Data.IOArray.Prims
export
data ArrayData : Type -> Type where [external]
-- 'unsafe' primitive access, backend dependent
-- get and set assume that the bounds have been checked. Behaviour is undefined
-- otherwise.
export %extern prim__newArray : forall a . Int -> a -> PrimIO (ArrayData a)
export %extern prim__arrayGet : forall a . ArrayData a -> Int -> PrimIO a
export %extern prim__arraySet : forall a . ArrayData a -> Int -> a -> PrimIO ()

37
libs/base/Data/List.idr
View File

@ -33,6 +33,41 @@ drop Z xs = xs
drop (S n) [] = []
drop (S n) (x::xs) = drop n xs
||| Satisfiable if `k` is a valid index into `xs`
|||
||| @ k the potential index
||| @ xs the list into which k may be an index
public export
data InBounds : (k : Nat) -> (xs : List a) -> Type where
||| Z is a valid index into any cons cell
InFirst : InBounds Z (x :: xs)
||| Valid indices can be extended
InLater : InBounds k xs -> InBounds (S k) (x :: xs)
export
Uninhabited (InBounds k []) where
uninhabited InFirst impossible
uninhabited (InLater _) impossible
||| Decide whether `k` is a valid index into `xs`
export
inBounds : (k : Nat) -> (xs : List a) -> Dec (InBounds k xs)
inBounds k [] = No uninhabited
inBounds Z (x :: xs) = Yes InFirst
inBounds (S k) (x :: xs) with (inBounds k xs)
inBounds (S k) (x :: xs) | (Yes prf) = Yes (InLater prf)
inBounds (S k) (x :: xs) | (No contra)
= No (\p => case p of
InLater y => contra y)
||| Find a particular element of a list.
|||
||| @ ok a proof that the index is within bounds
export
index : (n : Nat) -> (xs : List a) -> {auto ok : InBounds n xs} -> a
index Z (x :: xs) {ok = InFirst} = x
index (S k) (x :: xs) {ok = (InLater p)} = index k xs
||| Generate a list by repeatedly applying a partial function until exhausted.
||| @ f the function to iterate
||| @ x the initial value that will be the head of the list
@ -595,7 +630,7 @@ revOnto xs [] = Refl
revOnto xs (v :: vs)
= rewrite revOnto (v :: xs) vs in
rewrite appendAssociative (reverse vs) [v] xs in
rewrite revOnto [v] vs in Refl
rewrite revOnto [v] vs in Refl
export
revAppend : (vs, ns : List a) -> reverse ns ++ reverse vs = reverse (vs ++ ns)

46
libs/base/Data/Nat.idr
View File

@ -466,8 +466,8 @@ multDistributesOverMinusRight left centre right =
-- power proofs
multPowerPowerPlus : (base, exp, exp' : Nat) ->
power base (exp + exp') = (power base exp) * (power base exp')
-- multPowerPowerPlus : (base, exp, exp' : Nat) ->
-- power base (exp + exp') = (power base exp) * (power base exp')
-- multPowerPowerPlus base Z exp' =
-- rewrite sym $ plusZeroRightNeutral (power base exp') in Refl
-- multPowerPowerPlus base (S exp) exp' =
@ -475,21 +475,21 @@ multPowerPowerPlus : (base, exp, exp' : Nat) ->
-- rewrite sym $ multAssociative base (power base exp) (power base exp') in
-- Refl
powerOneNeutral : (base : Nat) -> power base 1 = base
powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base
powerOneSuccOne : (exp : Nat) -> power 1 exp = 1
powerOneSuccOne Z = Refl
powerOneSuccOne (S exp) = rewrite powerOneSuccOne exp in Refl
powerPowerMultPower : (base, exp, exp' : Nat) ->
power (power base exp) exp' = power base (exp * exp')
powerPowerMultPower _ exp Z = rewrite multZeroRightZero exp in Refl
powerPowerMultPower base exp (S exp') =
rewrite powerPowerMultPower base exp exp' in
rewrite multRightSuccPlus exp exp' in
rewrite sym $ multPowerPowerPlus base exp (exp * exp') in
Refl
--powerOneNeutral : (base : Nat) -> power base 1 = base
--powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base
--
--powerOneSuccOne : (exp : Nat) -> power 1 exp = 1
--powerOneSuccOne Z = Refl
--powerOneSuccOne (S exp) = rewrite powerOneSuccOne exp in Refl
--
--powerPowerMultPower : (base, exp, exp' : Nat) ->
-- power (power base exp) exp' = power base (exp * exp')
--powerPowerMultPower _ exp Z = rewrite multZeroRightZero exp in Refl
--powerPowerMultPower base exp (S exp') =
-- rewrite powerPowerMultPower base exp exp' in
-- rewrite multRightSuccPlus exp exp' in
-- rewrite sym $ multPowerPowerPlus base exp (exp * exp') in
-- Refl
-- minimum / maximum proofs
@ -506,7 +506,7 @@ maximumCommutative Z (S _) = Refl
maximumCommutative (S _) Z = Refl
maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in Refl
maximumIdempotent : (n : Nat) -> maximum n n = n
-- maximumIdempotent : (n : Nat) -> maximum n n = n
-- maximumIdempotent Z = Refl
-- maximumIdempotent (S k) = cong $ maximumIdempotent k
@ -523,7 +523,7 @@ minimumCommutative Z (S _) = Refl
minimumCommutative (S _) Z = Refl
minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in Refl
minimumIdempotent : (n : Nat) -> minimum n n = n
-- minimumIdempotent : (n : Nat) -> minimum n n = n
-- minimumIdempotent Z = Refl
-- minimumIdempotent (S k) = cong (minimumIdempotent k)
@ -541,18 +541,18 @@ maximumSuccSucc : (left, right : Nat) ->
S (maximum left right) = maximum (S left) (S right)
maximumSuccSucc _ _ = Refl
sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
-- sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
-- sucMaxL Z = Refl
-- sucMaxL (S l) = cong $ sucMaxL l
sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
-- sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
-- sucMaxR Z = Refl
-- sucMaxR (S l) = cong $ sucMaxR l
sucMinL : (l : Nat) -> minimum (S l) l = l
-- sucMinL : (l : Nat) -> minimum (S l) l = l
-- sucMinL Z = Refl
-- sucMinL (S l) = cong $ sucMinL l
sucMinR : (l : Nat) -> minimum l (S l) = l
-- sucMinR : (l : Nat) -> minimum l (S l) = l
-- sucMinR Z = Refl
-- sucMinR (S l) = cong $ sucMinR l

1
libs/base/base.ipkg
View File

@ -13,6 +13,7 @@ modules = Control.App,
Data.Either,
Data.Fin,
Data.IOArray,
Data.IOArray.Prims,
Data.IORef,
Data.List,
Data.List.Elem,

74
libs/contrib/Data/Linear/Array.idr Normal file
View File

@ -0,0 +1,74 @@
module Data.Linear.Array
import Data.IOArray
-- Linear arrays. General idea: mutable arrays are constructed linearly,
-- using newArray. Once everything is set up, they can be converted to
-- read only arrays with constant time, pure, access, using toIArray.
-- Immutable arrays which can be read in constant time, but not updated
public export
interface Array arr where
read : (1 _ : arr t) -> Int -> Maybe t
size : (1 _ : arr t) -> Int
-- Mutable arrays which can be used linearly
public export
interface Array arr => MArray arr where
newArray : (size : Int) -> (1 _ : (1 _ : arr t) -> a) -> a
-- Array is unchanged if the index is out of bounds
write : (1 _ : arr t) -> Int -> t -> arr t
mread : (1 _ : arr t) -> Int -> LPair (Maybe t) (arr t)
msize : (1 _ : arr t) -> LPair Int (arr t)
export
data IArray : Type -> Type where
MkIArray : IOArray t -> IArray t
export
data LinArray : Type -> Type where
MkLinArray : IOArray t -> LinArray t
-- Convert a mutable array to an immutable array
export
toIArray : (1 _ : LinArray t) -> (IArray t -> a) -> a
toIArray (MkLinArray arr) k = k (MkIArray arr)
export
Array LinArray where
read (MkLinArray a) i = unsafePerformIO (readArray a i)
size (MkLinArray a) = max a
export
MArray LinArray where
newArray size k = k (MkLinArray (unsafePerformIO (newArray size)))
write (MkLinArray a) i el
= unsafePerformIO (do writeArray a i el
pure (MkLinArray a))
msize (MkLinArray a) = max a # MkLinArray a
mread (MkLinArray a) i
= unsafePerformIO (readArray a i) # MkLinArray a
export
Array IArray where
read (MkIArray a) i = unsafePerformIO (readArray a i)
size (MkIArray a) = max a
export
copyArray : MArray arr => (newsize : Int) -> (1 _ : arr t) -> (arr t, arr t)
copyArray newsize a
= let size # a = msize a in
newArray newsize $
(\a' => copyContent (min (newsize - 1) (size - 1)) a a')
where
copyContent : Int -> (1 _ : arr t) -> (1 _ : arr t) -> (arr t, arr t)
copyContent pos a a'
= if pos < 0
then (a, a')
else let val # a = mread a pos
1 a' = case val of
Nothing => a'
Just v => write a' pos v in
copyContent (pos - 1) a a'

2
libs/contrib/contrib.ipkg
View File

@ -2,6 +2,8 @@ package contrib
modules = Control.Delayed,
Data.Linear.Array,
Data.List.TailRec,
Data.List.Equalities,
Data.List.Reverse,

6
libs/network/Network/Socket.idr
View File

@ -173,10 +173,10 @@ recvAll sock = recvRec sock [] 64
recvRec : Socket -> List String -> ByteLength -> IO (Either SocketError String)
recvRec sock acc n = do res <- recv sock n
case res of
Left 0 => pure (Right $ concat $ reverse acc)
Left c => pure (Left c)
Right (str, _) => let n' = min (n * 2) 65536 in
recvRec sock (str :: acc) n'
Right (str, res) => let n' = min (n * 2) 65536 in
if res < n then pure (Right $ concat $ reverse $ str :: acc)
else recvRec sock (str :: acc) n'
||| Send a message.
|||

32
libs/prelude/Builtin.idr
View File

@ -67,22 +67,36 @@ snd (x, y) = y
-- This directive tells auto implicit search what to use to look inside pairs
%pair Pair fst snd
||| Dependent pairs aid in the construction of dependent types by providing
||| evidence that some value resides in the type.
|||
||| Formally, speaking, dependent pairs represent existential quantification -
||| they consist of a witness for the existential claim and a proof that the
||| property holds for it.
|||
||| @ a the value to place in the type.
||| @ p the dependent type that requires the value.
infix 5 #
||| A pair type for use in operations on linear resources, which return a
||| value and an updated resource
public export
data LPair : Type -> Type -> Type where
(#) : (x : a) -> (1 _ : b) -> LPair a b
namespace DPair
||| Dependent pairs aid in the construction of dependent types by providing
||| evidence that some value resides in the type.
|||
||| Formally, speaking, dependent pairs represent existential quantification -
||| they consist of a witness for the existential claim and a proof that the
||| property holds for it.
|||
||| @ a the value to place in the type.
||| @ p the dependent type that requires the value.
public export
record DPair a (p : a -> Type) where
constructor MkDPair
fst : a
snd : p fst
||| A dependent variant of LPair, pairing a result value with a resource
||| that depends on the result value
public export
data Res : (a : Type) -> (a -> Type) -> Type where
(#) : (val : a) -> (1 r : t val) -> Res a t
-- The empty type
||| The empty type, also known as the trivially false proposition.

8
src/Core/LinearCheck.idr
View File

@ -247,7 +247,13 @@ mutual
unusedHoleArgs _ ty = ty
lcheck rig_in erase env (Bind fc nm b sc)
= do (b', bt, usedb) <- lcheckBinder rig erase env b
= do (b', bt, usedb) <- handleUnify (lcheckBinder rig erase env b)
(\err =>
case err of
LinearMisuse _ _ r _ =>
lcheckBinder rig erase env
(setMultiplicity b linear)
_ => throw err)
-- Anything linear can't be used in the scope of a lambda, if we're
-- checking in general context
let env' = if rig_in == top

11
src/Core/Options.idr
View File

@ -49,6 +49,12 @@ Eq CG where
Gambit == Gambit = True
_ == _ = False
export
Show CG where
show Chez = "chez"
show Racket = "racket"
show Gambit = "gambit"
export
availableCGs : List (String, CG)
availableCGs
@ -138,13 +144,14 @@ record Options where
extensions : List LangExt
defaultDirs : Dirs
defaultDirs = MkDirs "." Nothing "build"
("build" </> "exec")
defaultDirs = MkDirs "." Nothing "build"
("build" </> "exec")
"/usr/local" ["."] [] []
defaultPPrint : PPrinter
defaultPPrint = MkPPOpts False True False
export
defaultSession : Session
defaultSession = MkSessionOpts False False False Chez 0 False False
Nothing Nothing Nothing Nothing

6
src/Idris/CommandLine.idr
View File

@ -4,6 +4,8 @@ import IdrisPaths
import Idris.Version
import Core.Options
import Data.List
import Data.Maybe
import Data.Strings
@ -44,7 +46,7 @@ data CLOpt
OutputFile String |
||| Execute a given function after checking the source file
ExecFn String |
||| Use a specific code generator (default chez)
||| Use a specific code generator
SetCG String |
||| Don't implicitly import Prelude
NoPrelude |
@ -113,7 +115,7 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
MkOpt ["--no-prelude"] [] [NoPrelude]
(Just "Don't implicitly import Prelude"),
MkOpt ["--codegen", "--cg"] ["backend"] (\f => [SetCG f])
(Just "Set code generator (default chez)"),
(Just $ "Set code generator (default \""++ show (codegen defaultSession) ++ "\")"),
MkOpt ["--package", "-p"] ["package"] (\f => [PkgPath f])
(Just "Add a package as a dependency"),

2
src/Idris/Main.idr
View File

@ -131,7 +131,6 @@ stMain opts
defs <- initDefs
c <- newRef Ctxt defs
s <- newRef Syn initSyntax
m <- newRef MD initMetadata
addPrimitives
setWorkingDir "."
@ -157,6 +156,7 @@ stMain opts
when (checkVerbose opts) $ -- override Quiet if implicitly set
setOutput (REPL False)
u <- newRef UST initUState
m <- newRef MD initMetadata
updateREPLOpts
session <- getSession
when (not $ nobanner session) $

16
src/Idris/Package.idr
View File

@ -444,15 +444,16 @@ getParseErrorLoc fname _ = replFC
-- Just load the 'Main' module, if it exists, which will involve building
-- it if necessary
runRepl : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
PkgDesc ->
List CLOpt ->
Core ()
runRepl pkg opts
= do addDeps pkg
processOptions (options pkg)
preOptions opts
throw (InternalError "Not implemented")
runRepl pkg opts = do
u <- newRef UST initUState
m <- newRef MD initMetadata
repl {u} {s}
processPackage : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
@ -480,7 +481,10 @@ processPackage cmd file opts
| errs => coreLift (exitWith (ExitFailure 1))
install pkg opts
Clean => clean pkg opts
REPL => runRepl pkg opts
REPL => do
[] <- build pkg opts
| errs => coreLift (exitWith (ExitFailure 1))
runRepl pkg opts
record POptsFilterResult where
constructor MkPFR

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

@ -201,17 +201,17 @@ checkLet rigc_in elabinfo nest env fc rigl n nTy nVal scope expty {vars}
(record { preciseInf = True } elabinfo)
nest env nVal (Just (gnf env tyv))
pure (fst c, snd c, rigl |*| rigc))
(\err => case err of
(LinearMisuse _ _ r _)
=> branchOne
(do c <- runDelays 0 $ check linear elabinfo
nest env nVal (Just (gnf env tyv))
pure (fst c, snd c, linear))
(do c <- check (rigl |*| rigc)
elabinfo -- without preciseInf
nest env nVal (Just (gnf env tyv))
pure (fst c, snd c, rigMult rigl rigc))
r
(\err => case linearErr err of
Just r
=> do branchOne
(do c <- runDelays 0 $ check linear elabinfo
nest env nVal (Just (gnf env tyv))
pure (fst c, snd c, linear))
(do c <- check (rigl |*| rigc)
elabinfo -- without preciseInf
nest env nVal (Just (gnf env tyv))
pure (fst c, snd c, rigMult rigl rigc))
r
_ => do c <- check (rigl |*| rigc)
elabinfo -- without preciseInf
nest env nVal (Just (gnf env tyv))
@ -229,3 +229,11 @@ checkLet rigc_in elabinfo nest env fc rigl n nTy nVal scope expty {vars}
-- build the term directly
pure (Bind fc n (Let rigb valv tyv) scopev,
gnf env (Bind fc n (Let rigb valv tyv) scopet))
where
linearErr : Error -> Maybe RigCount
linearErr (LinearMisuse _ _ r _) = Just r
linearErr (InType _ _ e) = linearErr e
linearErr (InCon _ _ e) = linearErr e
linearErr (InLHS _ _ e) = linearErr e
linearErr (InRHS _ _ e) = linearErr e
linearErr _ = Nothing

1
src/TTImp/Elab/Delayed.idr
View File

@ -179,6 +179,7 @@ recoverable (CantSolveEq _ env l r)
= do defs <- get Ctxt
pure $ not !(contra defs !(nf defs env l) !(nf defs env r))
recoverable (UndefinedName _ _) = pure False
recoverable (LinearMisuse _ _ _ _) = pure False
recoverable (InType _ _ err) = recoverable err
recoverable (InCon _ _ err) = recoverable err
recoverable (InLHS _ _ err) = recoverable err

2
tests/Main.idr
View File

@ -80,7 +80,7 @@ idrisTests
"perror001", "perror002", "perror003", "perror004", "perror005",
"perror006",
-- Packages and ipkg files
"pkg001", "pkg002", "pkg003",
"pkg001", "pkg002", "pkg003", "pkg004",
-- Larger programs arising from real usage. Typically things with
-- interesting interactions between features
"real001", "real002",

12
tests/ideMode/ideMode001/expected
View File

@ -2,13 +2,13 @@
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:260} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:261}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:260}_[] ?{_:261}_[])")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:262}_[] ?{_:261}_[])")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:269} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:270}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:269}_[] ?{_:270}_[])")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:271}_[] ?{_:270}_[])")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:251}_[] ?{_:250}_[])")))))) 1)
0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:241} : (Main.Vect n[0] a[1])) -> (({arg:242} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

12
tests/ideMode/ideMode003/expected
View File

@ -2,13 +2,13 @@
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:260} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:261}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:260}_[] ?{_:261}_[])")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:262}_[] ?{_:261}_[])")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:269} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:270}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:269}_[] ?{_:270}_[])")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:271}_[] ?{_:270}_[])")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:251}_[] ?{_:250}_[])")))))) 1)
0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:241} : (Main.Vect n[0] a[1])) -> (({arg:242} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

2
tests/idris2/coverage008/expected
View File

@ -1,6 +1,6 @@
1/1: Building wcov (wcov.idr)
Main> Main.tfoo is total
Main> Main.wfoo is total
Main> Main.wbar is not covering due to call to function Main.with block in 1372
Main> Main.wbar is not covering due to call to function Main.with block in 1376
Main> Main.wbar1 is total
Main> Bye for now!

2
tests/idris2/coverage010/expected
View File

@ -3,4 +3,4 @@ casetot.idr:12:1--13:1:main is not covering at:
12 main : IO ()
13 main = do
Calls non covering function Main.case block in 2071(287)
Calls non covering function Main.case block in 2075(296)

11
tests/idris2/interactive009/Door.idr
View File

@ -22,11 +22,6 @@ One = Use Once
Any : (Type -> Type) -> Type -> Type
Any = Use Many
infix 2 @@
data Res : (a : Type) -> (a -> Type) -> Type where
(@@) : (x : a) -> (1 res : r x) -> Res a r
data DoorState = Closed | Open
data Door : DoorState -> Type where
@ -57,7 +52,7 @@ doorProg2
r <- openDoor d
let x = 42
case r of
(res @@ d) => ?now_1
(res # d) => ?now_1
doorProg3 : Any m ()
doorProg3
@ -65,5 +60,5 @@ doorProg3
r <- openDoor d
let x = 42
case r of
(True @@ d) => ?now_2
(False @@ d) => ?now_3
(True # d) => ?now_2
(False # d) => ?now_3

6
tests/idris2/interactive009/expected
View File

@ -1,7 +1,7 @@
1/1: Building Door (Door.idr)
Main> (y @@ res) => ?now_4
Main> (True @@ d) => ?now_4
(False @@ d) => ?now_5
Main> (val # y) => ?now_4
Main> (True # d) => ?now_4
(False # d) => ?now_5
Main> 0 m : Type -> Type
1 d : Door Open
x : Integer

4
tests/idris2/interactive009/input
View File

@ -1,5 +1,5 @@
:cs 52 15 what
:cs 60 16 res
:cs 47 15 what
:cs 55 16 res
:t now_2
:t now_3
:q

6
tests/idris2/linear005/Linear.idr
View File

@ -30,9 +30,3 @@ One = Use Once
public export
Any : (Type -> Type) -> Type -> Type
Any = Use Many
infix 2 @@
public export
data Res : (a : Type) -> (a -> Type) -> Type where
(@@) : (x : a) -> (1 res : r x) -> Res a r

6
tests/idris2/linear008/Door.idr
View File

@ -56,12 +56,6 @@ public export
Any : (Type -> Type) -> Type -> Type
Any m = Lin m Many
infix 2 @@
public export
data Res : (a : Type) -> (a -> Type) -> Type where
(@@) : (val : a) -> (1 resource : r val) -> Res a r
data DoorState = Closed | Open
-- changes start here

11
tests/idris2/literate006/Door.lidr
View File

@ -22,11 +22,6 @@
> Any : (Type -> Type) -> Type -> Type
> Any = Use Many
> infix 2 @@
> data Res : (a : Type) -> (a -> Type) -> Type where
> (@@) : (x : a) -> (1 res : r x) -> Res a r
> data DoorState = Closed | Open
> data Door : DoorState -> Type where
@ -57,7 +52,7 @@
> r <- openDoor d
> let x = 42
> case r of
> (res @@ d) => ?now_1
> (res # d) => ?now_1
> doorProg3 : Any m ()
> doorProg3
@ -65,5 +60,5 @@
> r <- openDoor d
> let x = 42
> case r of
> (True @@ d) => ?now_2
> (False @@ d) => ?now_3
> (True # d) => ?now_2
> (False # d) => ?now_3

6
tests/idris2/literate006/expected
View File

@ -1,7 +1,7 @@
1/1: Building Door (Door.lidr)
Main> > (y @@ res) => ?now_4
Main> > (True @@ d) => ?now_4
> (False @@ d) => ?now_5
Main> > (val # y) => ?now_4
Main> > (True # d) => ?now_4
> (False # d) => ?now_5
Main> 0 m : Type -> Type
1 d : Door Open
x : Integer

4
tests/idris2/literate006/input
View File

@ -1,5 +1,5 @@
:cs 52 17 what
:cs 60 18 res
:cs 47 17 what
:cs 55 18 res
:t now_2
:t now_3
:q

7
tests/idris2/pkg004/Dummy.idr Normal file
View File

@ -0,0 +1,7 @@
module Dummy
something : String
something = "Something something"
data Proxy : Type -> Type where
MkProxy : Proxy a

9
tests/idris2/pkg004/dummy.ipkg Normal file
View File

@ -0,0 +1,9 @@
package dummy
authors = "Joe Bloggs"
maintainers = "Joe Bloggs"
license = "BSD3 but see LICENSE for more information"
brief = "This is a dummy package."
readme = "README.md"
modules = Dummy

12
tests/idris2/pkg004/expected Normal file
View File

@ -0,0 +1,12 @@
1/1: Building Dummy (Dummy.idr)
Dummy> (interactive):1:4--1:13:Undefined name undefined at:
1 :t undefined
^^^^^^^^^
Dummy> Dummy.something : String
Dummy> "Something something"
Dummy> Dummy.Proxy : Type -> Type
Dummy> Proxy
Dummy> Proxy String : Type
Dummy>
Bye for now!

6
tests/idris2/pkg004/input Normal file
View File

@ -0,0 +1,6 @@
:t undefined
:t something
something
:t Proxy
Proxy
:t Proxy String

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

@ -0,0 +1,3 @@
$1 --repl dummy.ipkg < input
rm -rf build

14
tests/idris2/real001/Channel.idr
View File

@ -134,11 +134,11 @@ tryRecv (MkChannel lock cond_lock cond local remote)
case dequeue rq of
Nothing =>
do lift $ mutexRelease lock
pure (Nothing @@ MkChannel lock cond_lock cond local remote)
pure (Nothing # MkChannel lock cond_lock cond local remote)
Just (rq', Entry {any} val) =>
do lift $ writeIORef local rq'
lift $ mutexRelease lock
pure (Just (believe_me {a=any} val) @@
pure (Just (believe_me {a=any} val) #
MkChannel lock cond_lock cond local remote)
-- blocks until the message is there
@ -158,7 +158,7 @@ recv (MkChannel lock cond_lock cond local remote)
Just (rq', Entry {any} val) =>
do lift $ writeIORef local rq'
lift $ mutexRelease lock
pure (believe_me {a=any} val @@
pure (believe_me {a=any} val #
MkChannel lock cond_lock cond local remote)
export
@ -180,14 +180,14 @@ timeoutRecv (MkChannel lock cond_lock cond local remote) timeout
lift $ mutexAcquire cond_lock
lift $ conditionWaitTimeout cond cond_lock timeout
lift $ mutexRelease cond_lock
res @@ chan <- tryRecv {ty} {next} (MkChannel lock cond_lock cond local remote)
res # chan <- tryRecv {ty} {next} (MkChannel lock cond_lock cond local remote)
case res of
Nothing => pure (Nothing @@ chan)
Just res => pure (Just res @@ chan)
Nothing => pure (Nothing # chan)
Just res => pure (Just res # chan)
Just (rq', Entry {any} val) =>
do lift $ writeIORef local rq'
lift $ mutexRelease lock
pure (Just (believe_me {a=any} val) @@
pure (Just (believe_me {a=any} val) #
MkChannel lock cond_lock cond local remote)
export

7
tests/idris2/real001/Linear.idr
View File

@ -54,13 +54,6 @@ public export
Any : (Type -> Type) -> Type -> Type
Any m = Lin m Many
infix 2 @@
public export
data Res : (a : Type) -> (a -> Type) -> Type where
(@@) : (val : a) -> (1 resource : r val) -> Res a r
{-
data DoorState = Closed | Open

14
tests/idris2/real001/MakeChans.idr
View File

@ -18,12 +18,12 @@ Utils
utilServer : (1 chan : Server Utils) -> Any IO ()
utilServer chan
= do cmd @@ chan <- recv chan
= do cmd # chan <- recv chan
case cmd of
Add => do (x, y) @@ chan <- recv chan
Add => do (x, y) # chan <- recv chan
chan <- send chan (x + y)
close chan
Append => do (x, y) @@ chan <- recv chan
Append => do (x, y) # chan <- recv chan
chan <- send chan (x ++ y)
close chan
@ -35,7 +35,7 @@ MakeUtils = do cmd <- Request Bool
sendUtils : (1 chan : Server MakeUtils) -> Any IO ()
sendUtils chan
= do cmd @@ chan <- recv chan
= do cmd # chan <- recv chan
if cmd
then do cchan <- Channel.fork utilServer
chan <- send chan cchan
@ -46,7 +46,7 @@ getUtilsChan : (1 chan : Client MakeUtils) ->
One IO (Client Utils, Client MakeUtils)
getUtilsChan chan
= do chan <- send chan True
cchan @@ chan <- recv chan
cchan # chan <- recv chan
pure (cchan, chan)
closeUtilsChan : (1 chan : Client MakeUtils) ->
@ -69,12 +69,12 @@ doThings
uchan1 <- send uchan1 Add
uchan2 <- send uchan2 Append
uchan2 <- send uchan2 ("aaa", "bbb")
res @@ uchan2 <- recv uchan2
res # uchan2 <- recv uchan2
close uchan2
lift $ printLn res
uchan1 <- send uchan1 (40, 54)
res @@ uchan1 <- recv uchan1
res # uchan1 <- recv uchan1
close uchan1
lift $ printLn res

4
tests/idris2/real001/TestProto.idr
View File

@ -18,14 +18,14 @@ testClient chan
lift $ putStrLn "Sending value"
chan <- send chan False
lift $ putStrLn "Sent"
c @@ chan <- recv chan
c # chan <- recv chan
lift $ putStrLn ("Result: " ++ c)
close chan
testServer : (1 chan : Server TestProto) -> Any IO ()
testServer chan
= do lift $ putStrLn "Waiting"
cmd @@ chan <- recv chan
cmd # chan <- recv chan
lift $ putStrLn ("Received " ++ show cmd)
lift $ sleep 1
lift $ putStrLn "Sending answer"

6
tests/idris2/real002/Control/App.idr
View File

@ -339,12 +339,6 @@ HasErr Void e => PrimIO e where
$ \_ =>
MkAppRes (Right ())
infix 5 @@
public export
data Res : (a : Type) -> (a -> Type) -> Type where
(@@) : (val : a) -> (1 r : t val) -> Res a t
public export
data FileEx = GenericFileEx Int -- errno
| FileReadError

14
tests/idris2/real002/Store.idr
View File

@ -23,10 +23,10 @@ Has [Console] e => StoreI e where
login (MkStore str) pwd
= if pwd == "Mornington Crescent"
then pure1 (True @@ MkStore str)
else pure1 (False @@ MkStore str)
then pure1 (True # MkStore str)
else pure1 (False # MkStore str)
logout (MkStore str) = pure1 (MkStore str)
readSecret (MkStore str) = pure1 (str @@ MkStore str)
readSecret (MkStore str) = pure1 (str # MkStore str)
disconnect (MkStore _)
= putStrLn "Door destroyed"
@ -38,11 +38,11 @@ storeProg
s <- connect
app $ putStr "Password: "
pwd <- app $ getStr
True @@ s <- login s pwd
| False @@ s => do app $ putStrLn "Login failed"
app $ disconnect s
True # s <- login s pwd
| False # s => do app $ putStrLn "Login failed"
app $ disconnect s
app $ putStrLn "Logged in"
secret @@ s <- readSecret s
secret # s <- readSecret s
app $ putStrLn ("Secret: " ++ secret)
s <- logout s
app $ putStrLn "Logged out"

10
tests/idris2/real002/StoreL.idr
View File

@ -25,8 +25,8 @@ login : (1 s : Store LoggedOut) -> (password : String) ->
Res Bool (\ok => Store (if ok then LoggedIn else LoggedOut))
login (MkStore secret) password
= if password == "Mornington Crescent"
then True @@ MkStore secret
else False @@ MkStore secret
then True # MkStore secret
else False # MkStore secret
logout : (1 s : Store LoggedIn) -> Store LoggedOut
logout (MkStore secret) = MkStore secret
@ -37,9 +37,9 @@ storeProg
do putStr "Password: "
password <- Console.getStr
connect $ \s =>
do let True @@ s = login s password
| False @@ s => do putStrLn "Incorrect password"
disconnect s
do let True # s = login s password
| False # s => do putStrLn "Incorrect password"
disconnect s
putStrLn "Door opened"
let s = logout s
putStrLn "Door closed"

18
tests/idris2/reflection003/expected
View File

@ -5,23 +5,23 @@ LOG 0: Name: Prelude.Strings.++
LOG 0: Type: (%pi Rig1 Explicit (Just _) String (%pi Rig1 Explicit (Just _) String String))
LOG 0: Resolved name: Prelude.Nat
LOG 0: Constructors: [Prelude.Z, Prelude.S]
refprims.idr:37:10--37:27:While processing right hand side of dummy1 at refprims.idr:37:1--39:1:
refprims.idr:43:10--43:27:While processing right hand side of dummy1 at refprims.idr:43:1--45:1:
Error during reflection: Not really trying at:
37 dummy1 = %runElab logPrims
43 dummy1 = %runElab logPrims
^^^^^^^^^^^^^^^^^
refprims.idr:40:10--40:30:While processing right hand side of dummy2 at refprims.idr:40:1--42:1:
refprims.idr:46:10--46:30:While processing right hand side of dummy2 at refprims.idr:46:1--48:1:
Error during reflection: Still not trying at:
40 dummy2 = %runElab logDataCons
46 dummy2 = %runElab logDataCons
^^^^^^^^^^^^^^^^^^^^
refprims.idr:43:10--43:25:While processing right hand side of dummy3 at refprims.idr:43:1--45:1:
refprims.idr:49:10--49:25:While processing right hand side of dummy3 at refprims.idr:49:1--51:1:
Error during reflection: Undefined name at:
43 dummy3 = %runElab logBad
49 dummy3 = %runElab logBad
^^^^^^^^^^^^^^^
refprims.idr:46:10--46:28:While processing right hand side of dummy4 at refprims.idr:46:1--48:1:
Error during reflection: failed after generating Main.{plus:6078} at:
46 dummy4 = %runElab tryGenSym
refprims.idr:52:10--52:28:While processing right hand side of dummy4 at refprims.idr:52:1--54:1:
Error during reflection: failed after generating Main.{plus:XXXX} at:
52 dummy4 = %runElab tryGenSym
^^^^^^^^^^^^^^^^^^

8
tests/idris2/reflection003/refprims.idr
View File

@ -27,11 +27,17 @@ logBad
logMsg 0 ("Constructors: " ++ show !(getCons n))
fail "Still not trying"
-- because the exact sequence number in a gensym depends on
-- the library and compiler internals we need to censor it so the
-- output won't be overly dependent on the exact versions used.
censorDigits : String -> String
censorDigits str = pack $ map (\c => if isDigit c then 'X' else c) (unpack str)
tryGenSym : Elab a
tryGenSym
= do n <- genSym "plus"
ns <- inCurrentNS n
fail $ "failed after generating " ++ show ns
fail $ "failed after generating " ++ censorDigits (show ns)
dummy1 : a
dummy1 = %runElab logPrims