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

Merge github.com:idris-lang/Idris2 into unify-postponing

Browse Source
This commit is contained in:
Edwin Brady 2021-05-15 20:10:43 +01:00
commit 70d8e4b337
67 changed files with 555 additions and 246 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
idris2api.ipkg
View File

@ -70,6 +70,7 @@ modules =
Idris.CommandLine,
Idris.Desugar,
Idris.Desugar.Mutual,
Idris.Env,
Idris.Doc.HTML,
Idris.DocString,

5
libs/base/Data/List1.idr
View File

@ -18,6 +18,11 @@ record List1 a where
------------------------------------------------------------------------
-- Basic functions
public export
fromList : List a -> Maybe (List1 a)
fromList [] = Nothing
fromList (x :: xs) = Just (x ::: xs)
public export
singleton : (x : a) -> List1 a
singleton a = a ::: []

2
libs/base/base.ipkg
View File

@ -1,7 +1,7 @@
package base
version = 0.3.0
opts = "--ignore-missing-ipkg"
opts = "--ignore-missing-ipkg --no-shadowing-warning"
modules = Control.App,
Control.App.Console,

2
libs/contrib/Data/List/HasLength.idr
View File

@ -124,7 +124,7 @@ listTerminating p = case view p of
data P : List Nat -> Type where
PNil : P []
PCon : P (map id xs) -> P (x :: xs)
PCon : P (map f xs) -> P (x :: xs)
covering
notListTerminating : (p : Subset Nat (HasLength xs)) -> P xs

2
libs/contrib/contrib.ipkg
View File

@ -1,7 +1,7 @@
package contrib
version = 0.3.0
opts = "--ignore-missing-ipkg"
opts = "--ignore-missing-ipkg --no-shadowing-warning"
modules = Control.ANSI,
Control.ANSI.SGR,

4
src/Compiler/ANF.idr
View File

@ -30,7 +30,9 @@ mutual
AApp : FC -> (lazy : Maybe LazyReason) -> (closure : AVar) -> (arg : AVar) -> ANF
ALet : FC -> (var : Int) -> ANF -> ANF -> ANF
ACon : FC -> Name -> ConInfo -> (tag : Maybe Int) -> List AVar -> ANF
AOp : FC -> (lazy : Maybe LazyReason) -> PrimFn arity -> Vect arity AVar -> ANF
AOp : {0 arity : Nat} -> FC -> (lazy : Maybe LazyReason) -> PrimFn arity -> Vect arity AVar -> ANF
-- ^ we explicitly bind arity here to silence the warning that it shadows
-- existing functions called arity.
AExtPrim : FC -> (lazy : Maybe LazyReason) -> Name -> List AVar -> ANF
AConCase : FC -> AVar -> List AConAlt -> Maybe ANF -> ANF
AConstCase : FC -> AVar -> List AConstAlt -> Maybe ANF -> ANF

6
src/Compiler/ES/ES.idr
View File

@ -22,7 +22,6 @@ record ESSt where
preamble : SortedMap String String
ccTypes : List String
jsString : String -> String
jsString s = "'" ++ (concatMap okchar (unpack s)) ++ "'"
where
@ -90,6 +89,7 @@ addStringIteratorToPreamble =
let newName = esName name
addToPreamble name newName defs
jsIdent : String -> String
jsIdent s = concatMap okchar (unpack s)
where
@ -285,7 +285,6 @@ div (Just k) x y =
else pure $ jsIntOfDouble k (x ++ " / " ++ y)
div Nothing x y = pure $ binOp "/" x y
-- Creates the definition of a binary arithmetic operation.
-- Rounding / truncation behavior is determined from the
-- `IntKind`.
@ -366,7 +365,8 @@ constPrimitives = MkConstantPrimitives {
(Unsigned m, Signed n) =>
if n > P m then pure expanded else shrunk
jsOp : {auto c : Ref ESs ESSt} -> PrimFn arity -> Vect arity String -> Core String
jsOp : {0 arity : Nat} -> {auto c : Ref ESs ESSt} ->
PrimFn arity -> Vect arity String -> Core String
jsOp (Add ty) [x, y] = arithOp (intKind ty) "+" x y
jsOp (Sub ty) [x, y] = arithOp (intKind ty) "-" x y
jsOp (Mul ty) [x, y] = mult (intKind ty) x y

4
src/Compiler/RefC/RefC.idr
View File

@ -174,7 +174,7 @@ plainOp op args = op ++ "(" ++ (showSep ", " args) ++ ")"
||| Generate scheme for a primitive function.
cOp : PrimFn arity -> Vect arity String -> String
cOp : {0 arity : Nat} -> PrimFn arity -> Vect arity String -> String
cOp (Neg ty) [x] = "negate_" ++ cConstant ty ++ "(" ++ x ++ ")"
cOp StrLength [x] = "stringLength(" ++ x ++ ")"
cOp StrHead [x] = "head(" ++ x ++ ")"
@ -427,7 +427,7 @@ showTag : Maybe Int -> String
showTag Nothing = "-1"
showTag (Just i) = show i
cArgsVectANF : Vect arity AVar -> Core (Vect arity String)
cArgsVectANF : {0 arity : Nat} -> Vect arity AVar -> Core (Vect arity String)
cArgsVectANF [] = pure []
cArgsVectANF (x :: xs) = pure $ (varName x) :: !(cArgsVectANF xs)

2
src/Compiler/Scheme/Common.idr
View File

@ -131,7 +131,7 @@ constPrimitives = MkConstantPrimitives {
if n >= m then x else op "blodwen-toUnsignedInt" [x,show n]
||| Generate scheme for a primitive function.
schOp : PrimFn arity -> Vect arity String -> Core String
schOp : {0 arity : Nat} -> PrimFn arity -> Vect arity String -> Core String
schOp (Add ty) [x, y] = pure $ add (intKind ty) x y
schOp (Sub ty) [x, y] = pure $ sub (intKind ty) x y
schOp (Mul ty) [x, y] = pure $ mul (intKind ty) x y

4
src/Compiler/VMCode.idr
View File

@ -36,7 +36,9 @@ data VMInst : Type where
APPLY : Reg -> (f : Reg) -> (a : Reg) -> VMInst
CALL : Reg -> (tailpos : Bool) -> Name -> (args : List Reg) -> VMInst
OP : Reg -> PrimFn arity -> Vect arity Reg -> VMInst
OP : {0 arity : Nat} -> Reg -> PrimFn arity -> Vect arity Reg -> VMInst
-- ^ we explicitly bind arity here to silence the warnings it is shadowing
-- an existing global definition
EXTPRIM : Reg -> Name -> List Reg -> VMInst
CASE : Reg -> -- scrutinee

2
src/Core/AutoSearch.idr
View File

@ -253,7 +253,7 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe
ambig (AmbiguousSearch _ _ _ _) = True
ambig _ = False
clearEnvType : {idx : Nat} -> (0 p : IsVar name idx vs) ->
clearEnvType : {idx : Nat} -> (0 p : IsVar nm idx vs) ->
FC -> Env Term vs -> Env Term vs
clearEnvType First fc (b :: env)
= Lam (binderLoc b) (multiplicity b) Explicit (Erased fc False) :: env

14
src/Core/CaseBuilder.idr
View File

@ -152,12 +152,12 @@ substInPats fc n tm (p :: ps)
pure (p' :: !(substInPats fc n tm ps'))
getPat : {idx : Nat} ->
(0 el : IsVar name idx ps) -> NamedPats ns ps -> PatInfo name ns
(0 el : IsVar nm idx ps) -> NamedPats ns ps -> PatInfo nm ns
getPat First (x :: xs) = x
getPat (Later p) (x :: xs) = getPat p xs
dropPat : {idx : Nat} ->
(0 el : IsVar name idx ps) ->
(0 el : IsVar nm idx ps) ->
NamedPats ns ps -> NamedPats ns (dropVar ps el)
dropPat First (x :: xs) = xs
dropPat (Later p) (x :: xs) = x :: dropPat p xs
@ -600,7 +600,7 @@ groupCons fc fn pvars cs
pure (g :: gs')
addGroup : {vars, todo, idx : _} ->
Pat -> (0 p : IsVar name idx vars) ->
Pat -> (0 p : IsVar nm idx vars) ->
NamedPats vars todo -> Int -> Term vars ->
List (Group vars todo) ->
Core (List (Group vars todo))
@ -778,12 +778,12 @@ pickNext {ps = q :: qs} fc phase fn npss
_ => do (_ ** MkNVar var) <- pickNext fc phase fn (map tail npss)
pure (_ ** MkNVar (Later var))
moveFirst : {idx : Nat} -> (0 el : IsVar name idx ps) -> NamedPats ns ps ->
NamedPats ns (name :: dropVar ps el)
moveFirst : {idx : Nat} -> (0 el : IsVar nm idx ps) -> NamedPats ns ps ->
NamedPats ns (nm :: dropVar ps el)
moveFirst el nps = getPat el nps :: dropPat el nps
shuffleVars : {idx : Nat} -> (0 el : IsVar name idx todo) -> PatClause vars todo ->
PatClause vars (name :: dropVar todo el)
shuffleVars : {idx : Nat} -> (0 el : IsVar nm idx todo) -> PatClause vars todo ->
PatClause vars (nm :: dropVar todo el)
shuffleVars el (MkPatClause pvars lhs pid rhs)
= MkPatClause pvars (moveFirst el lhs) pid rhs

62
src/Core/CompileExpr.idr
View File

@ -534,16 +534,16 @@ namespace SubstCEnv
(::) : CExp vars ->
SubstCEnv ds vars -> SubstCEnv (d :: ds) vars
findDrop : FC -> Var (drop ++ vars) ->
SubstCEnv drop vars -> CExp vars
findDrop : FC -> Var (dropped ++ vars) ->
SubstCEnv dropped vars -> CExp vars
findDrop fc (MkVar p) [] = CLocal fc p
findDrop fc (MkVar First) (tm :: env) = tm
findDrop fc (MkVar (Later p)) (tm :: env) = findDrop fc (MkVar p) env
find : FC ->
SizeOf outer ->
Var (outer ++ (drop ++ vars)) ->
SubstCEnv drop vars ->
Var (outer ++ (dropped ++ vars)) ->
SubstCEnv dropped vars ->
CExp (outer ++ vars)
find fc outer var env = case sizedView outer of
Z => findDrop fc var env
@ -554,8 +554,8 @@ find fc outer var env = case sizedView outer of
mutual
substEnv : SizeOf outer ->
SubstCEnv drop vars ->
CExp (outer ++ (drop ++ vars)) ->
SubstCEnv dropped vars ->
CExp (outer ++ (dropped ++ vars)) ->
CExp (outer ++ vars)
substEnv outer env (CLocal fc prf)
= find fc outer (MkVar prf) env
@ -589,35 +589,35 @@ mutual
substEnv _ _ (CCrash fc x) = CCrash fc x
substConAlt : SizeOf outer ->
SubstCEnv drop vars ->
CConAlt (outer ++ (drop ++ vars)) ->
SubstCEnv dropped vars ->
CConAlt (outer ++ (dropped ++ vars)) ->
CConAlt (outer ++ vars)
substConAlt {vars} {outer} {drop} p env (MkConAlt x ci tag args sc)
substConAlt {vars} {outer} {dropped} p env (MkConAlt x ci tag args sc)
= MkConAlt x ci tag args
(rewrite appendAssociative args outer vars in
substEnv (mkSizeOf args + p) env
(rewrite sym (appendAssociative args outer (drop ++ vars)) in
(rewrite sym (appendAssociative args outer (dropped ++ vars)) in
sc))
substConstAlt : SizeOf outer ->
SubstCEnv drop vars ->
CConstAlt (outer ++ (drop ++ vars)) ->
SubstCEnv dropped vars ->
CConstAlt (outer ++ (dropped ++ vars)) ->
CConstAlt (outer ++ vars)
substConstAlt outer env (MkConstAlt x sc) = MkConstAlt x (substEnv outer env sc)
export
substs : {drop, vars : _} ->
SubstCEnv drop vars -> CExp (drop ++ vars) -> CExp vars
substs : {dropped, vars : _} ->
SubstCEnv dropped vars -> CExp (dropped ++ vars) -> CExp vars
substs env tm = substEnv zero env tm
resolveRef : SizeOf later ->
resolveRef : SizeOf outer ->
SizeOf done ->
Bounds bound -> FC -> Name ->
Maybe (CExp (later ++ (done ++ bound ++ vars)))
Maybe (CExp (outer ++ (done ++ bound ++ vars)))
resolveRef _ _ None _ _ = Nothing
resolveRef {later} {vars} {done} p q (Add {xs} new old bs) fc n
resolveRef {outer} {vars} {done} p q (Add {xs} new old bs) fc n
= if n == old
then rewrite appendAssociative later done (new :: xs ++ vars) in
then rewrite appendAssociative outer done (new :: xs ++ vars) in
let MkNVar p = weakenNVar (p + q) (MkNVar First) in
Just (CLocal fc p)
else rewrite appendAssociative done [new] (xs ++ vars)
@ -625,10 +625,10 @@ resolveRef {later} {vars} {done} p q (Add {xs} new old bs) fc n
mutual
export
mkLocals : SizeOf later ->
mkLocals : SizeOf outer ->
Bounds bound ->
CExp (later ++ vars) ->
CExp (later ++ (bound ++ vars))
CExp (outer ++ vars) ->
CExp (outer ++ (bound ++ vars))
mkLocals later bs (CLocal {idx} {x} fc p)
= let MkNVar p' = addVars later bs (MkNVar p) in CLocal {x} fc p'
mkLocals later bs (CRef fc var)
@ -663,21 +663,21 @@ mutual
mkLocals later bs (CErased fc) = CErased fc
mkLocals later bs (CCrash fc x) = CCrash fc x
mkLocalsConAlt : SizeOf later ->
mkLocalsConAlt : SizeOf outer ->
Bounds bound ->
CConAlt (later ++ vars) ->
CConAlt (later ++ (bound ++ vars))
mkLocalsConAlt {bound} {later} {vars} p bs (MkConAlt x ci tag args sc)
= let sc' : CExp ((args ++ later) ++ vars)
= rewrite sym (appendAssociative args later vars) in sc in
CConAlt (outer ++ vars) ->
CConAlt (outer ++ (bound ++ vars))
mkLocalsConAlt {bound} {outer} {vars} p bs (MkConAlt x ci tag args sc)
= let sc' : CExp ((args ++ outer) ++ vars)
= rewrite sym (appendAssociative args outer vars) in sc in
MkConAlt x ci tag args
(rewrite appendAssociative args later (bound ++ vars) in
(rewrite appendAssociative args outer (bound ++ vars) in
mkLocals (mkSizeOf args + p) bs sc')
mkLocalsConstAlt : SizeOf later ->
mkLocalsConstAlt : SizeOf outer ->
Bounds bound ->
CConstAlt (later ++ vars) ->
CConstAlt (later ++ (bound ++ vars))
CConstAlt (outer ++ vars) ->
CConstAlt (outer ++ (bound ++ vars))
mkLocalsConstAlt later bs (MkConstAlt x sc) = MkConstAlt x (mkLocals later bs sc)
export

6
src/Core/Context.idr
View File

@ -271,7 +271,7 @@ record GlobalDef where
specArgs : List Nat -- arguments to specialise by
inferrable : List Nat -- arguments which can be inferred from elsewhere in the type
multiplicity : RigCount
vars : List Name -- environment name is defined in
localVars : List Name -- environment name is defined in
visibility : Visibility
totality : Totality
flags : List DefFlag
@ -624,7 +624,7 @@ newDef fc n rig vars ty vis def
, specArgs = []
, inferrable = []
, multiplicity = rig
, vars = vars
, localVars = vars
, visibility = vis
, totality = unchecked
, flags = []
@ -1329,7 +1329,7 @@ addBuiltin n ty tot op
, specArgs = []
, inferrable = []
, multiplicity = top
, vars = []
, localVars = []
, visibility = Public
, totality = tot
, flags = [Inline]

2
src/Core/Core.idr
View File

@ -160,6 +160,7 @@ public export
data Warning : Type where
UnreachableClause : {vars : _} ->
FC -> Env Term vars -> Term vars -> Warning
ShadowingGlobalDefs : FC -> List1 (String, List1 Name) -> Warning
Deprecated : String -> Warning
export
@ -412,6 +413,7 @@ getErrorLoc (MaybeMisspelling err _) = getErrorLoc err
export
getWarningLoc : Warning -> Maybe FC
getWarningLoc (UnreachableClause fc _ _) = Just fc
getWarningLoc (ShadowingGlobalDefs fc _) = Just fc
getWarningLoc (Deprecated _) = Nothing
-- Core is a wrapper around IO that is specialised for efficiency.

4
src/Core/Normalise.idr
View File

@ -182,7 +182,7 @@ parameters (defs : Defs, topopts : EvalOpts)
{free, vars : _} ->
Env Term free ->
FC -> Maybe Bool ->
(idx : Nat) -> (0 p : IsVar name idx (vars ++ free)) ->
(idx : Nat) -> (0 p : IsVar nm idx (vars ++ free)) ->
Stack free ->
LocalEnv free vars ->
Core (NF free)
@ -203,7 +203,7 @@ parameters (defs : Defs, topopts : EvalOpts)
env fc mrig (S idx) (Later p) stk (_ :: locs)
= evalLocal {vars = xs} env fc mrig idx p stk locs
updateLocal : (idx : Nat) -> (0 p : IsVar name idx (vars ++ free)) ->
updateLocal : (idx : Nat) -> (0 p : IsVar nm idx (vars ++ free)) ->
LocalEnv free vars -> NF free ->
LocalEnv free vars
updateLocal Z First (x :: locs) nf = MkNFClosure nf :: locs

3
src/Core/Options.idr
View File

@ -157,6 +157,7 @@ record Session where
dumpanf : Maybe String -- file to output ANF definitions
dumpvmcode : Maybe String -- file to output VM code definitions
profile : Bool -- generate profiling information, if supported
showShadowingWarning : Bool
public export
record PPrinter where
@ -205,7 +206,7 @@ export
defaultSession : Session
defaultSession = MkSessionOpts False False False Chez [] False defaultLogLevel
False False False Nothing Nothing
Nothing Nothing False
Nothing Nothing False True
export
defaultElab : ElabDirectives

4
src/Core/Primitives.idr
View File

@ -586,7 +586,7 @@ castTo DoubleType = castDouble
castTo _ = const Nothing
export
getOp : PrimFn arity ->
getOp : {0 arity : Nat} -> PrimFn arity ->
{vars : List Name} -> Vect arity (NF vars) -> Maybe (NF vars)
getOp (Add ty) = binOp add
getOp (Sub ty) = binOp sub
@ -637,7 +637,7 @@ prim : String -> Name
prim str = UN $ "prim__" ++ str
export
opName : PrimFn arity -> Name
opName : {0 arity : Nat} -> PrimFn arity -> Name
opName (Add ty) = prim $ "add_" ++ show ty
opName (Sub ty) = prim $ "sub_" ++ show ty
opName (Mul ty) = prim $ "mul_" ++ show ty

90
src/Core/TT.idr
View File

@ -556,11 +556,21 @@ Functor Binder where
map func (PLet fc c val ty) = PLet fc c (func val) (func ty)
map func (PVTy fc c ty) = PVTy fc c (func ty)
public export
data IsVar : Name -> Nat -> List Name -> Type where
First : IsVar n Z (n :: ns)
Later : IsVar n i ns -> IsVar n (S i) (m :: ns)
export
dropLater : IsVar nm (S idx) (v :: vs) -> IsVar nm idx vs
dropLater (Later p) = p
export
mkVar : (wkns : List Name) -> IsVar nm (length wkns) (wkns ++ nm :: vars)
mkVar [] = First
mkVar (w :: ws) = Later (mkVar ws)
public export
dropVar : (ns : List Name) -> {idx : Nat} -> (0 p : IsVar name idx ns) -> List Name
dropVar (n :: xs) First = xs
@ -1328,49 +1338,49 @@ namespace Bounds
sizeOf (Add _ _ b) = suc (sizeOf b)
export
addVars : SizeOf later -> Bounds bound ->
NVar name (later ++ vars) ->
NVar name (later ++ (bound ++ vars))
addVars : SizeOf outer -> Bounds bound ->
NVar name (outer ++ vars) ->
NVar name (outer ++ (bound ++ vars))
addVars p = insertNVarNames p . sizeOf
resolveRef : SizeOf later -> SizeOf done -> Bounds bound -> FC -> Name ->
Maybe (Term (later ++ (done ++ bound ++ vars)))
resolveRef : SizeOf outer -> SizeOf done -> Bounds bound -> FC -> Name ->
Maybe (Term (outer ++ (done ++ bound ++ vars)))
resolveRef p q None fc n = Nothing
resolveRef {later} {done} p q (Add {xs} new old bs) fc n
resolveRef {outer} {done} p q (Add {xs} new old bs) fc n
= if n == old
then rewrite appendAssociative later done (new :: xs ++ vars) in
then rewrite appendAssociative outer done (new :: xs ++ vars) in
let MkNVar p = weakenNVar (p + q) (MkNVar First) in
Just (Local fc Nothing _ p)
else rewrite appendAssociative done [new] (xs ++ vars)
in resolveRef p (sucR q) bs fc n
mkLocals : SizeOf later -> Bounds bound ->
Term (later ++ vars) -> Term (later ++ (bound ++ vars))
mkLocals later bs (Local fc r idx p)
= let MkNVar p' = addVars later bs (MkNVar p) in Local fc r _ p'
mkLocals later bs (Ref fc Bound name)
= maybe (Ref fc Bound name) id (resolveRef later zero bs fc name)
mkLocals later bs (Ref fc nt name)
mkLocals : SizeOf outer -> Bounds bound ->
Term (outer ++ vars) -> Term (outer ++ (bound ++ vars))
mkLocals outer bs (Local fc r idx p)
= let MkNVar p' = addVars outer bs (MkNVar p) in Local fc r _ p'
mkLocals outer bs (Ref fc Bound name)
= maybe (Ref fc Bound name) id (resolveRef outer zero bs fc name)
mkLocals outer bs (Ref fc nt name)
= Ref fc nt name
mkLocals later bs (Meta fc name y xs)
= maybe (Meta fc name y (map (mkLocals later bs) xs))
id (resolveRef later zero bs fc name)
mkLocals later bs (Bind fc x b scope)
= Bind fc x (map (mkLocals later bs) b)
(mkLocals (suc later) bs scope)
mkLocals later bs (App fc fn arg)
= App fc (mkLocals later bs fn) (mkLocals later bs arg)
mkLocals later bs (As fc s as tm)
= As fc s (mkLocals later bs as) (mkLocals later bs tm)
mkLocals later bs (TDelayed fc x y)
= TDelayed fc x (mkLocals later bs y)
mkLocals later bs (TDelay fc x t y)
= TDelay fc x (mkLocals later bs t) (mkLocals later bs y)
mkLocals later bs (TForce fc r x)
= TForce fc r (mkLocals later bs x)
mkLocals later bs (PrimVal fc c) = PrimVal fc c
mkLocals later bs (Erased fc i) = Erased fc i
mkLocals later bs (TType fc) = TType fc
mkLocals outer bs (Meta fc name y xs)
= maybe (Meta fc name y (map (mkLocals outer bs) xs))
id (resolveRef outer zero bs fc name)
mkLocals outer bs (Bind fc x b scope)
= Bind fc x (map (mkLocals outer bs) b)
(mkLocals (suc outer) bs scope)
mkLocals outer bs (App fc fn arg)
= App fc (mkLocals outer bs fn) (mkLocals outer bs arg)
mkLocals outer bs (As fc s as tm)
= As fc s (mkLocals outer bs as) (mkLocals outer bs tm)
mkLocals outer bs (TDelayed fc x y)
= TDelayed fc x (mkLocals outer bs y)
mkLocals outer bs (TDelay fc x t y)
= TDelay fc x (mkLocals outer bs t) (mkLocals outer bs y)
mkLocals outer bs (TForce fc r x)
= TForce fc r (mkLocals outer bs x)
mkLocals outer bs (PrimVal fc c) = PrimVal fc c
mkLocals outer bs (Erased fc i) = Erased fc i
mkLocals outer bs (TType fc) = TType fc
export
refsToLocals : Bounds bound -> Term vars -> Term (bound ++ vars)
@ -1429,8 +1439,8 @@ namespace SubstEnv
SubstEnv ds vars -> SubstEnv (d :: ds) vars
findDrop : FC -> Maybe Bool ->
Var (drop ++ vars) ->
SubstEnv drop vars ->
Var (dropped ++ vars) ->
SubstEnv dropped vars ->
Term vars
findDrop fc r (MkVar var) [] = Local fc r _ var
findDrop fc r (MkVar First) (tm :: env) = tm
@ -1439,8 +1449,8 @@ namespace SubstEnv
find : FC -> Maybe Bool ->
SizeOf outer ->
Var (outer ++ (drop ++ vars)) ->
SubstEnv drop vars ->
Var (outer ++ (dropped ++ vars)) ->
SubstEnv dropped vars ->
Term (outer ++ vars)
find fc r outer var env = case sizedView outer of
Z => findDrop fc r var env
@ -1450,8 +1460,8 @@ namespace SubstEnv
-- TODO: refactor to only weaken once?
substEnv : SizeOf outer ->
SubstEnv drop vars ->
Term (outer ++ (drop ++ vars)) ->
SubstEnv dropped vars ->
Term (outer ++ (dropped ++ vars)) ->
Term (outer ++ vars)
substEnv outer env (Local fc r _ prf)
= find fc r outer (MkVar prf) env
@ -1474,7 +1484,7 @@ namespace SubstEnv
substEnv outer env (TType fc) = TType fc
export
substs : SubstEnv drop vars -> Term (drop ++ vars) -> Term vars
substs : SubstEnv dropped vars -> Term (dropped ++ vars) -> Term vars
substs env tm = substEnv zero env tm
export

2
src/Core/TTC.idr
View File

@ -1021,7 +1021,7 @@ TTC GlobalDef where
toBuf b (safeErase gdef)
toBuf b (specArgs gdef)
toBuf b (inferrable gdef)
toBuf b (vars gdef)
toBuf b (localVars gdef)
toBuf b (visibility gdef)
toBuf b (totality gdef)
toBuf b (flags gdef)

2
src/Core/Unify.idr
View File

@ -510,7 +510,7 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
isSimple _ = False
updateIVar : {v : Nat} ->
forall vs, newvars . IVars vs newvars -> (0 p : IsVar name v newvars) ->
forall vs, newvars . IVars vs newvars -> (0 p : IsVar nm v newvars) ->
Maybe (Var vs)
updateIVar {v} (ICons Nothing rest) prf
= do MkVar prf' <- updateIVar rest prf

17
src/Core/UnifyState.idr
View File

@ -1,3 +1,4 @@
module Core.UnifyState
import Core.CaseTree
@ -292,11 +293,6 @@ mkConstantAppArgs {done} {vars = x :: xs} lets fc (b :: env) wkns
then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
rewrite (appendAssociative wkns [x] (xs ++ done)) in rec
else rewrite (appendAssociative wkns [x] (xs ++ done)) in rec
where
mkVar : (wkns : List Name) ->
IsVar name (length wkns) (wkns ++ name :: vars ++ done)
mkVar [] = First
mkVar (w :: ws) = Later (mkVar ws)
mkConstantAppArgsSub : {vars : _} ->
Bool -> FC -> Env Term vars ->
@ -319,11 +315,6 @@ mkConstantAppArgsSub {done} {vars = x :: xs}
then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
rewrite appendAssociative wkns [x] (xs ++ done) in rec
else rewrite appendAssociative wkns [x] (xs ++ done) in rec
where
mkVar : (wkns : List Name) ->
IsVar name (length wkns) (wkns ++ name :: vars ++ done)
mkVar [] = First
mkVar (w :: ws) = Later (mkVar ws)
mkConstantAppArgsOthers : {vars : _} ->
Bool -> FC -> Env Term vars ->
@ -346,12 +337,6 @@ mkConstantAppArgsOthers {done} {vars = x :: xs}
then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
rewrite appendAssociative wkns [x] (xs ++ done) in rec
else rewrite appendAssociative wkns [x] (xs ++ done) in rec
where
mkVar : (wkns : List Name) ->
IsVar name (length wkns) (wkns ++ name :: vars ++ done)
mkVar [] = First
mkVar (w :: ws) = Later (mkVar ws)
export
applyTo : {vars : _} ->

2
src/Core/Value.idr
View File

@ -65,7 +65,7 @@ mutual
-- The head of a value: things you can apply arguments to
public export
data NHead : List Name -> Type where
NLocal : Maybe Bool -> (idx : Nat) -> (0 p : IsVar name idx vars) ->
NLocal : Maybe Bool -> (idx : Nat) -> (0 p : IsVar nm idx vars) ->
NHead vars
NRef : NameType -> Name -> NHead vars
NMeta : Name -> Int -> List (Closure vars) -> NHead vars

6
src/Idris/CommandLine.idr
View File

@ -119,6 +119,8 @@ data CLOpt
Timing |
DebugElabCheck |
BlodwenPaths |
||| Do not print shadowing warnings
IgnoreShadowingWarnings |
||| Generate bash completion info
BashCompletion String String |
||| Generate bash completion script
@ -202,6 +204,10 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
MkOpt ["--profile"] [] [Profile]
(Just "Generate profile data when compiling, if supported"),
optSeparator,
MkOpt ["--no-shadowing-warning"] [] [IgnoreShadowingWarnings]
(Just "Do not print shadowing warnings"),
optSeparator,
MkOpt ["--prefix"] [] [ShowPrefix]
(Just "Show installation prefix"),

92
src/Idris/Desugar.idr
View File

@ -22,6 +22,8 @@ import Idris.Syntax
import Idris.Elab.Implementation
import Idris.Elab.Interface
import Idris.Desugar.Mutual
import Parser.Lexer.Source
import TTImp.BindImplicits
@ -653,7 +655,7 @@ mutual
desugarType ps (MkPTy fc nameFC n d ty)
= do addDocString n d
syn <- get Syn
pure $ MkImpTy fc nameFC n !(bindTypeNames (usingImpl syn)
pure $ MkImpTy fc nameFC n !(bindTypeNames fc (usingImpl syn)
ps !(desugar AnyExpr ps ty))
getClauseFn : RawImp -> Core Name
@ -727,14 +729,14 @@ mutual
= do addDocString n doc
syn <- get Syn
pure $ MkImpData fc n
!(bindTypeNames (usingImpl syn)
!(bindTypeNames fc (usingImpl syn)
ps !(desugar AnyExpr ps tycon))
opts
!(traverse (desugarType ps) datacons)
desugarData ps doc (MkPLater fc n tycon)
= do addDocString n doc
syn <- get Syn
pure $ MkImpLater fc n !(bindTypeNames (usingImpl syn)
pure $ MkImpLater fc n !(bindTypeNames fc (usingImpl syn)
ps !(desugar AnyExpr ps tycon))
desugarField : {auto s : Ref Syn SyntaxInfo} ->
@ -747,53 +749,9 @@ mutual
= do addDocStringNS ns n doc
syn <- get Syn
pure (MkIField fc rig !(traverse (desugar AnyExpr ps) p )
n !(bindTypeNames (usingImpl syn)
n !(bindTypeNames fc (usingImpl syn)
ps !(desugar AnyExpr ps ty)))
-- Get the declaration to process on each pass of a mutual block
-- Essentially: types on the first pass
-- i.e. type constructors of data declarations
-- function types
-- interfaces (in full, since it includes function types)
-- records (just the generated type constructor)
-- implementation headers (i.e. note their existence, but not the bodies)
-- Everything else on the second pass
getDecl : Pass -> PDecl -> Maybe PDecl
getDecl p (PImplementation fc vis opts _ is cons n ps iname nusing ds)
= Just (PImplementation fc vis opts p is cons n ps iname nusing ds)
getDecl p (PNamespace fc ns ds)
= Just (PNamespace fc ns (mapMaybe (getDecl p) ds))
getDecl AsType d@(PClaim _ _ _ _ _) = Just d
getDecl AsType (PData fc doc vis (MkPData dfc tyn tyc _ _))
= Just (PData fc doc vis (MkPLater dfc tyn tyc))
getDecl AsType d@(PInterface _ _ _ _ _ _ _ _ _) = Just d
getDecl AsType d@(PRecord fc doc vis n ps _ _)
= Just (PData fc doc vis (MkPLater fc n (mkRecType ps)))
where
mkRecType : List (Name, RigCount, PiInfo PTerm, PTerm) -> PTerm
mkRecType [] = PType fc
mkRecType ((n, c, p, t) :: ts) = PPi fc c p (Just n) t (mkRecType ts)
getDecl AsType d@(PFixity _ _ _ _) = Just d
getDecl AsType d@(PDirective _ _) = Just d
getDecl AsType d = Nothing
getDecl AsDef (PClaim _ _ _ _ _) = Nothing
getDecl AsDef d@(PData _ _ _ (MkPLater _ _ _)) = Just d
getDecl AsDef (PInterface _ _ _ _ _ _ _ _ _) = Nothing
getDecl AsDef d@(PRecord _ _ _ _ _ _ _) = Just d
getDecl AsDef (PFixity _ _ _ _) = Nothing
getDecl AsDef (PDirective _ _) = Nothing
getDecl AsDef d = Just d
getDecl p (PParameters fc ps pds)
= Just (PParameters fc ps (mapMaybe (getDecl p) pds))
getDecl p (PUsing fc ps pds)
= Just (PUsing fc ps (mapMaybe (getDecl p) pds))
getDecl Single d = Just d
export
desugarFnOpt : {auto s : Ref Syn SyntaxInfo} ->
{auto c : Ref Ctxt Defs} ->
@ -844,11 +802,11 @@ mutual
i' <- traverse (desugar AnyExpr ps) i
pure (n, rig, i', tm')) params
-- Look for implicitly bindable names in the parameters
let pnames = ifThenElse !isUnboundImplicits
(concatMap (findBindableNames True
(ps ++ map Builtin.fst params) [])
(map (Builtin.snd . Builtin.snd . Builtin.snd) params'))
[]
pnames <- ifThenElse (not !isUnboundImplicits) (pure [])
$ map concat
$ for (map (Builtin.snd . Builtin.snd . Builtin.snd) params')
$ findUniqueBindableNames fc True (ps ++ map Builtin.fst params) []
let paramsb = map (\(n, rig, info, tm) =>
(n, rig, info, doBind pnames tm)) params'
pure [IParameters fc paramsb (concat pds')]
@ -856,7 +814,7 @@ mutual
= do syn <- get Syn
let oldu = usingImpl syn
uimpls' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
btm <- bindTypeNames oldu ps tm'
btm <- bindTypeNames fc oldu ps tm'
pure (fst ntm, btm)) uimpls
put Syn (record { usingImpl = uimpls' ++ oldu } syn)
uds' <- traverse (desugarDecl ps) uds
@ -880,14 +838,11 @@ mutual
params
-- Look for bindable names in all the constraints and parameters
let mnames = map dropNS (definedIn body)
let bnames = ifThenElse !isUnboundImplicits
(concatMap (findBindableNames True
(ps ++ mnames ++ paramNames) [])
(map Builtin.snd cons') ++
concatMap (findBindableNames True
(ps ++ mnames ++ paramNames) [])
(map (snd . snd) params'))
[]
bnames <- ifThenElse (not !isUnboundImplicits) (pure [])
$ map concat
$ for (map Builtin.snd cons' ++ map (snd . snd) params')
$ findUniqueBindableNames fc True (ps ++ mnames ++ paramNames) []
let paramsb = map (\ (nm, (rig, tm)) =>
let tm' = doBind bnames tm in
(nm, (rig, tm')))
@ -924,11 +879,10 @@ mutual
params' <- traverse (desugar AnyExpr ps) params
let _ = the (List RawImp) params'
-- Look for bindable names in all the constraints and parameters
let bnames = if !isUnboundImplicits
then
concatMap (findBindableNames True ps []) (map snd cons') ++
concatMap (findBindableNames True ps []) params'
else []
bnames <- ifThenElse (not !isUnboundImplicits) (pure [])
$ map concat
$ for (map snd cons' ++ params')
$ findUniqueBindableNames fc True ps []
let paramsb = map (doBind bnames) params'
let isb = map (\ (n, r, tm) => (n, r, doBind bnames tm)) is'
@ -1006,8 +960,8 @@ mutual
desugarDecl ps (PFixity fc _ _ _)
= throw (GenericMsg fc "Fixity declarations must be for unqualified names")
desugarDecl ps (PMutual fc ds)
= do let mds = mapMaybe (getDecl AsType) ds ++ mapMaybe (getDecl AsDef) ds
mds' <- traverse (desugarDecl ps) mds
= do let (tys, defs) = splitMutual ds
mds' <- traverse (desugarDecl ps) (tys ++ defs)
pure (concat mds')
desugarDecl ps (PNamespace fc ns decls)
= withExtendedNS ns $ do

53
src/Idris/Desugar/Mutual.idr Normal file
View File

@ -0,0 +1,53 @@
module Idris.Desugar.Mutual
import Idris.Syntax
%default total
-- Get the declaration to process on each pass of a mutual block
-- Essentially: types on the first pass
-- i.e. type constructors of data declarations
-- function types
-- interfaces (in full, since it includes function types)
-- records (just the generated type constructor)
-- implementation headers (i.e. note their existence, but not the bodies)
-- Everything else on the second pass
getDecl : Pass -> PDecl -> Maybe PDecl
getDecl p (PImplementation fc vis opts _ is cons n ps iname nusing ds)
= Just (PImplementation fc vis opts p is cons n ps iname nusing ds)
getDecl p (PNamespace fc ns ds)
= Just (PNamespace fc ns (assert_total $ mapMaybe (getDecl p) ds))
getDecl AsType d@(PClaim _ _ _ _ _) = Just d
getDecl AsType (PData fc doc vis (MkPData dfc tyn tyc _ _))
= Just (PData fc doc vis (MkPLater dfc tyn tyc))
getDecl AsType d@(PInterface _ _ _ _ _ _ _ _ _) = Just d
getDecl AsType d@(PRecord fc doc vis n ps _ _)
= Just (PData fc doc vis (MkPLater fc n (mkRecType ps)))
where
mkRecType : List (Name, RigCount, PiInfo PTerm, PTerm) -> PTerm
mkRecType [] = PType fc
mkRecType ((n, c, p, t) :: ts) = PPi fc c p (Just n) t (mkRecType ts)
getDecl AsType d@(PFixity _ _ _ _) = Just d
getDecl AsType d@(PDirective _ _) = Just d
getDecl AsType d = Nothing
getDecl AsDef (PClaim _ _ _ _ _) = Nothing
getDecl AsDef d@(PData _ _ _ (MkPLater _ _ _)) = Just d
getDecl AsDef (PInterface _ _ _ _ _ _ _ _ _) = Nothing
getDecl AsDef d@(PRecord _ _ _ _ _ _ _) = Just d
getDecl AsDef (PFixity _ _ _ _) = Nothing
getDecl AsDef (PDirective _ _) = Nothing
getDecl AsDef d = Just d
getDecl p (PParameters fc ps pds)
= Just (PParameters fc ps (assert_total $ mapMaybe (getDecl p) pds))
getDecl p (PUsing fc ps pds)
= Just (PUsing fc ps (assert_total $ mapMaybe (getDecl p) pds))
getDecl Single d = Just d
export
splitMutual : List PDecl -> (List PDecl, List PDecl)
splitMutual ds = (mapMaybe (getDecl AsType) ds, mapMaybe (getDecl AsDef) ds)

2
src/Idris/Elab/Implementation.idr
View File

@ -407,7 +407,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
mty_params
let ibound = findImplicits mbase
mty <- bindTypeNamesUsed ibound vars mbase
mty <- bindTypeNamesUsed ifc ibound vars mbase
log "elab.implementation" 3 $
"Method " ++ show meth.name ++ " ==> " ++

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

@ -120,9 +120,9 @@ mkIfaceData {vars} ifc vis env constraints n conName ps dets meths
retty = apply (IVar vfc n) (map (IVar EmptyFC) pNames)
conty = mkTy Implicit (map jname ps) $
mkTy AutoImplicit (map bhere constraints) (mkTy Explicit (map bname meths) retty)
con = MkImpTy EmptyFC EmptyFC conName !(bindTypeNames [] (pNames ++ map fst meths ++ vars) conty) in
con = MkImpTy EmptyFC EmptyFC conName !(bindTypeNames ifc [] (pNames ++ map fst meths ++ vars) conty) in
pure $ IData vfc vis (MkImpData vfc n
!(bindTypeNames [] (pNames ++ map fst meths ++ vars)
!(bindTypeNames ifc [] (pNames ++ map fst meths ++ vars)
(mkDataTy vfc ps))
opts [con])
where
@ -156,7 +156,7 @@ getMethDecl : {vars : _} ->
Core (nm, RigCount, RawImp)
getMethDecl {vars} env nest params mnames (c, nm, ty)
= do let paramNames = map fst params
ty_imp <- bindTypeNames [] (paramNames ++ mnames ++ vars) ty
ty_imp <- bindTypeNames EmptyFC [] (paramNames ++ mnames ++ vars) ty
pure (nm, c, stripParams paramNames ty_imp)
where
-- We don't want the parameters to explicitly appear in the method
@ -191,7 +191,7 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params sig
-- which appear in other method types
let ty_constr =
substNames vars (map applyCon allmeths) sig.type
ty_imp <- bindTypeNames [] vars (bindPs params $ bindIFace vfc ity ty_constr)
ty_imp <- bindTypeNames EmptyFC [] vars (bindPs params $ bindIFace vfc ity ty_constr)
cn <- inCurrentNS sig.name
let tydecl = IClaim vfc sig.count vis (if sig.isData then [Inline, Invertible]
else [Inline])
@ -255,7 +255,7 @@ getConstraintHint : {vars : _} ->
getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, con)
= do let ity = apply (IVar fc iname) (map (IVar fc) params)
let fty = IPi fc top Explicit Nothing ity con
ty_imp <- bindTypeNames [] (meths ++ vars) fty
ty_imp <- bindTypeNames fc [] (meths ++ vars) fty
let hintname = DN ("Constraint " ++ show con)
(UN ("__" ++ show iname ++ "_" ++ show con))
@ -449,7 +449,7 @@ elabInterface {vars} ifc vis env nest constraints iname params dets mcon body
$ bindIFace vdfc ity -- bind interface (?!)
$ substNames vars methNameMap dty
dty_imp <- bindTypeNames [] (map name tydecls ++ vars) dty
dty_imp <- bindTypeNames dfc [] (map name tydecls ++ vars) dty
log "elab.interface.default" 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp
let dtydecl = IClaim vdfc rig vis [] (MkImpTy EmptyFC EmptyFC dn dty_imp)

9
src/Idris/Error.idr
View File

@ -478,6 +478,15 @@ pwarning (UnreachableClause fc env tm)
= pure $ errorDesc (reflow "Unreachable clause:"
<++> code !(pshow env tm))
<+> line <+> !(ploc fc)
pwarning (ShadowingGlobalDefs _ ns)
= pure $ vcat
$ reflow "We are about to implicitly bind the following lowercase names."
:: reflow "You may be unintentionally shadowing the associated global definitions:"
:: map (\ (n, ns) => indent 2 $ hsep $ pretty n
:: reflow "is shadowing"
:: punctuate comma (map pretty (forget ns)))
(forget ns)
pwarning (Deprecated s)
= pure $ pretty "Deprecation warning:" <++> pretty s

2
src/Idris/Parser.idr
View File

@ -1212,7 +1212,7 @@ namespaceDecl fname indents
ds <- blockAfter col (topDecl fname)
pure (doc, ns, ds))
(doc, ns, ds) <- pure b.val
pure (PNamespace (boundToFC fname b) ns (concat ds))
pure (PNamespace (boundToFC fname b) ns (collectDefs $ concat ds))
transformDecl : FileName -> IndentInfo -> Rule PDecl
transformDecl fname indents

44
src/Idris/ProcessIdr.idr
View File

@ -20,6 +20,7 @@ import TTImp.ProcessDecls
import TTImp.TTImp
import Idris.Desugar
import Idris.Desugar.Mutual
import Idris.Parser
import Idris.REPL.Common
import Idris.REPL.Opts
@ -33,31 +34,40 @@ import System.File
%default covering
processDecl : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
PDecl -> Core (Maybe Error)
processDecl decl
= catch (do impdecls <- desugarDecl [] decl
traverse_ (Check.processDecl [] (MkNested []) []) impdecls
pure Nothing)
(\err => do giveUpConstraints -- or we'll keep trying...
pure (Just err))
processDecls : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
List PDecl -> Core (List Error)
processDecl : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
PDecl -> Core (List Error)
-- Special cases to avoid treating these big blocks as units
-- This should give us better error recovery (the whole block won't fail
-- as soon as one of the definitions fails)
processDecl (PNamespace fc ns ps)
= withExtendedNS ns $ processDecls ps
processDecl (PMutual fc ps)
= let (tys, defs) = splitMutual ps in
processDecls (tys ++ defs)
processDecl decl
= catch (do impdecls <- desugarDecl [] decl
traverse_ (Check.processDecl [] (MkNested []) []) impdecls
pure [])
(\err => do giveUpConstraints -- or we'll keep trying...
pure [err])
processDecls decls
= do xs <- traverse processDecl decls
= do xs <- concat <$> traverse processDecl decls
Nothing <- checkDelayedHoles
| Just err => pure (case mapMaybe id xs of
[] => [err]
errs => errs)
| Just err => pure (if null xs then [err] else xs)
errs <- logTime ("+++ Totality check overall") getTotalityErrors
pure (mapMaybe id xs ++ errs)
pure (xs ++ errs)
readModule : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->

2
src/Idris/REPL.idr
View File

@ -819,7 +819,7 @@ process (TypeSearch searchTerm)
let curr = currentNS defs
let ctxt = gamma defs
rawTy <- desugar AnyExpr [] searchTerm
let bound = piBindNames replFC [] rawTy
bound <- piBindNames replFC [] rawTy
(ty, _) <- elabTerm 0 InType [] (MkNested []) [] bound Nothing
ty' <- toResolvedNames ty
filteredDefs <-

2
src/Idris/Resugar.idr
View File

@ -329,7 +329,7 @@ mutual
let args'
= if fenv
then args
else drop (length (vars def)) args
else drop (length (localVars def)) args
mkApp fn' args'
toPTermApp fn args
= do fn' <- toPTerm appPrec fn

3
src/Idris/SetOptions.idr
View File

@ -340,6 +340,9 @@ preOptions (ConsoleWidth n :: opts)
preOptions (Color b :: opts)
= do setColor b
preOptions opts
preOptions (IgnoreShadowingWarnings :: opts)
= do setSession (record { showShadowingWarning = False } !getSession)
preOptions opts
preOptions (BashCompletion a b :: _)
= do os <- opts a b
coreLift $ putStr $ unlines os

8
src/Libraries/Data/List1.idr
View File

@ -4,6 +4,14 @@ import public Data.List1
%default total
-- TODO: Remove this, once Data.List1.fromList from base is available
-- to the compiler
public export
fromList : List a -> Maybe (List1 a)
fromList [] = Nothing
fromList (x :: xs) = Just (x ::: xs)
-- TODO: Remove this, once Data.List1.unsnoc from base is available
-- to the compiler
export

23
src/TTImp/BindImplicits.idr
View File

@ -162,29 +162,30 @@ addUsing uimpls tm
export
bindTypeNames : {auto c : Ref Ctxt Defs} ->
List (Maybe Name, RawImp) ->
FC -> List (Maybe Name, RawImp) ->
List Name -> RawImp-> Core RawImp
bindTypeNames uimpls env tm
bindTypeNames fc uimpls env tm
= if !isUnboundImplicits
then let ns = nub (findBindableNames True env [] tm)
btm = doBind ns tm in
pure (addUsing uimpls btm)
then do ns <- findUniqueBindableNames fc True env [] tm
let btm = doBind ns tm
pure (addUsing uimpls btm)
else pure tm
export
bindTypeNamesUsed : {auto c : Ref Ctxt Defs} ->
List String -> List Name -> RawImp -> Core RawImp
bindTypeNamesUsed used env tm
FC -> List String -> List Name -> RawImp -> Core RawImp
bindTypeNamesUsed fc used env tm
= if !isUnboundImplicits
then do let ns = nub (findBindableNames True env used tm)
then do ns <- findUniqueBindableNames fc True env used tm
pure (doBind ns tm)
else pure tm
export
piBindNames : FC -> List Name -> RawImp -> RawImp
piBindNames : {auto c : Ref Ctxt Defs} ->
FC -> List Name -> RawImp -> Core RawImp
piBindNames loc env tm
= let ns = nub (findBindableNames True env [] tm) in
piBind (map fst ns) tm
= do ns <- findUniqueBindableNames loc True env [] tm
pure $ piBind (map fst ns) tm
where
piBind : List String -> RawImp -> RawImp
piBind [] ty = ty

4
src/TTImp/Elab/Case.idr
View File

@ -53,14 +53,14 @@ findLater {older} x (_ :: xs)
= let MkVar p = findLater {older} x xs in
MkVar (Later p)
toRig1 : {idx : Nat} -> (0 p : IsVar name idx vs) -> Env Term vs -> Env Term vs
toRig1 : {idx : Nat} -> (0 p : IsVar nm idx vs) -> Env Term vs -> Env Term vs
toRig1 First (b :: bs)
= if isErased (multiplicity b)
then setMultiplicity b linear :: bs
else b :: bs
toRig1 (Later p) (b :: bs) = b :: toRig1 p bs
toRig0 : {idx : Nat} -> (0 p : IsVar name idx vs) -> Env Term vs -> Env Term vs
toRig0 : {idx : Nat} -> (0 p : IsVar nm idx vs) -> Env Term vs -> Env Term vs
toRig0 First (b :: bs) = setMultiplicity b erased :: bs
toRig0 (Later p) (b :: bs) = b :: toRig0 p bs

5
src/TTImp/Elab/Check.idr
View File

@ -219,11 +219,6 @@ strengthenedEState {n} {vars} c e fc env
dropSub (DropCons sub) = pure sub
dropSub _ = throw (InternalError "Badly formed weakened environment")
-- This helps persuade the erasure checker that it can erase IsVar,
-- because there's no matching on it in removeArgVars below.
dropLater : IsVar name (S idx) (v :: vs) -> IsVar name idx vs
dropLater (Later p) = p
-- Remove any instance of the top level local variable from an
-- application. Fail if it turns out to be necessary.
-- NOTE: While this isn't strictly correct given the type of the hole

4
src/TTImp/Elab/ImplicitBind.idr
View File

@ -152,7 +152,7 @@ bindUnsolved {vars} fc elabmode _
_ => inTerm)
fc env tm bindtm
swapIsVarH : {idx : Nat} -> (0 p : IsVar name idx (x :: y :: xs)) ->
swapIsVarH : {idx : Nat} -> (0 p : IsVar nm idx (x :: y :: xs)) ->
Var (y :: x :: xs)
swapIsVarH First = MkVar (Later First)
swapIsVarH (Later p) = swapP p -- it'd be nice to do this all at the top
@ -165,7 +165,7 @@ swapIsVarH (Later p) = swapP p -- it'd be nice to do this all at the top
swapP (Later x) = MkVar (Later (Later x))
swapIsVar : (vs : List Name) ->
{idx : Nat} -> (0 p : IsVar name idx (vs ++ x :: y :: xs)) ->
{idx : Nat} -> (0 p : IsVar nm idx (vs ++ x :: y :: xs)) ->
Var (vs ++ y :: x :: xs)
swapIsVar [] prf = swapIsVarH prf
swapIsVar (x :: xs) First = MkVar First

4
src/TTImp/Interactive/ExprSearch.idr
View File

@ -38,9 +38,9 @@ import Data.List
-- of the LHS. Only recursive calls with a different structure are okay.
record RecData where
constructor MkRecData
{vars : List Name}
{localVars : List Name}
recname : Name -- resolved name
lhsapp : Term vars
lhsapp : Term localVars
-- Additional definitions required to support the result
ExprDefs : Type

4
src/TTImp/ProcessData.idr
View File

@ -346,7 +346,7 @@ processData : {vars : _} ->
ImpData -> Core ()
processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
= do n <- inCurrentNS n_in
ty_raw <- bindTypeNames [] vars ty_raw
ty_raw <- bindTypeNames fc [] vars ty_raw
defs <- get Ctxt
-- Check 'n' is undefined
@ -382,7 +382,7 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)
= do n <- inCurrentNS n_in
ty_raw <- bindTypeNames [] vars ty_raw
ty_raw <- bindTypeNames fc [] vars ty_raw
log "declare.data" 1 $ "Processing " ++ show n
defs <- get Ctxt

8
src/TTImp/ProcessDecls.idr
View File

@ -139,22 +139,22 @@ processTTImpDecls {vars} nest env decls
where
bindConNames : ImpTy -> Core ImpTy
bindConNames (MkImpTy fc nameFC n ty)
= do ty' <- bindTypeNames [] vars ty
= do ty' <- bindTypeNames fc [] vars ty
pure (MkImpTy fc nameFC n ty')
bindDataNames : ImpData -> Core ImpData
bindDataNames (MkImpData fc n t opts cons)
= do t' <- bindTypeNames [] vars t
= do t' <- bindTypeNames fc [] vars t
cons' <- traverse bindConNames cons
pure (MkImpData fc n t' opts cons')
bindDataNames (MkImpLater fc n t)
= do t' <- bindTypeNames [] vars t
= do t' <- bindTypeNames fc [] vars t
pure (MkImpLater fc n t')
-- bind implicits to make raw TTImp source a bit friendlier
bindNames : ImpDecl -> Core ImpDecl
bindNames (IClaim fc c vis opts (MkImpTy tfc nameFC n ty))
= do ty' <- bindTypeNames [] vars ty
= do ty' <- bindTypeNames fc [] vars ty
pure (IClaim fc c vis opts (MkImpTy tfc nameFC n ty'))
bindNames (IData fc vis d)
= do d' <- bindDataNames d

2
src/TTImp/ProcessDef.idr
View File

@ -629,7 +629,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env
-- If it's 'KeepCons/SubRefl' in 'outprf', that means it was in the outer
-- environment so we need to keep it in the same place in the 'with'
-- function. Hence, turn it to KeepCons whatever
keepOldEnv : {vs : _} ->
keepOldEnv : {0 outer : _} -> {vs : _} ->
(outprf : SubVars outer vs) -> SubVars vs' vs ->
(vs'' : List Name ** SubVars vs'' vs)
keepOldEnv {vs} SubRefl p = (vs ** SubRefl)

2
src/TTImp/ProcessParams.idr
View File

@ -40,7 +40,7 @@ processParams {vars} {c} {m} {u} nest env fc ps ds
-- then read off the environment from the elaborated type. This way
-- we'll get all the implicit names we need
let pty_raw = mkParamTy ps
pty_imp <- bindTypeNames [] vars (IBindHere fc (PI erased) pty_raw)
pty_imp <- bindTypeNames fc [] vars (IBindHere fc (PI erased) pty_raw)
log "declare.param" 10 $ "Checking " ++ show pty_imp
pty <- checkTerm (-1) InType []
nest env pty_imp (gType fc)

6
src/TTImp/ProcessRecord.idr
View File

@ -99,9 +99,9 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
= do let fc = virtualiseFC fc
let conty = mkTy paramTelescope $
mkTy (map farg fields) recTy
let con = MkImpTy EmptyFC EmptyFC cname !(bindTypeNames [] (map fst params ++
let con = MkImpTy EmptyFC EmptyFC cname !(bindTypeNames fc [] (map fst params ++
map fname fields ++ vars) conty)
let dt = MkImpData fc tn !(bindTypeNames [] (map fst params ++
let dt = MkImpData fc tn !(bindTypeNames fc [] (map fst params ++
map fname fields ++ vars)
(mkDataTy fc params)) [] [con]
log "declare.record" 5 $ "Record data type " ++ show dt
@ -144,7 +144,7 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
let rname = MN "rec" 0
-- Claim the projection type
projTy <- bindTypeNames []
projTy <- bindTypeNames fc []
(map fst params ++ map fname fields ++ vars) $
mkTy paramTelescope $
IPi bfc top Explicit (Just rname) recTy ty'

18
src/TTImp/Utils.idr
View File

@ -1,12 +1,14 @@
module TTImp.Utils
import Core.Context
import Core.Options
import Core.TT
import TTImp.TTImp
import Data.List
import Data.Strings
import Libraries.Data.List1 as Lib
import Libraries.Utils.String
%default covering
@ -66,6 +68,22 @@ findBindableNames arg env used (IAlternative fc u alts)
-- name should be bound, leave it to the programmer
findBindableNames arg env used tm = []
export
findUniqueBindableNames :
{auto c : Ref Ctxt Defs} ->
FC -> (arg : Bool) -> (env : List Name) -> (used : List String) ->
RawImp -> Core (List (String, String))
findUniqueBindableNames fc arg env used t
= do let assoc = nub (findBindableNames arg env used t)
when (showShadowingWarning !getSession) $
do defs <- get Ctxt
let ctxt = gamma defs
ns <- map catMaybes $ for assoc $ \ (n, _) => do
ns <- lookupCtxtName (UN n) ctxt
pure $ MkPair n . map fst <$> Lib.fromList ns
whenJust (Lib.fromList ns) $ recordWarning . ShadowingGlobalDefs fc
pure assoc
export
findAllNames : (env : List Name) -> RawImp -> List Name
findAllNames env (IVar fc n)

5
tests/Main.idr
View File

@ -62,6 +62,10 @@ idrisTestsCasetree = MkTestPool "Case tree building" []
-- Case tree building
["casetree001"]
idrisTestsWarning : TestPool
idrisTestsWarning = MkTestPool "Warnings" []
["warning001"]
idrisTestsError : TestPool
idrisTestsError = MkTestPool "Error messages" []
-- Error messages
@ -296,6 +300,7 @@ main = runner
, testPaths "idris2" idrisTestsCoverage
, testPaths "idris2" idrisTestsCasetree
, testPaths "idris2" idrisTestsError
, testPaths "idris2" idrisTestsWarning
, testPaths "idris2" idrisTestsInteractive
, testPaths "idris2" idrisTestsInterface
, testPaths "idris2" idrisTestsLiterate

41
tests/idris2/basic049/expected
View File

@ -1,4 +1,45 @@
1/1: Building Fld (Fld.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
a is shadowing Main.R1.R1.a
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
a is shadowing Main.R2.R2.a, Main.R1.R1.a
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
a is shadowing Main.R2.R2.a, Main.R1.R1.a
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
a is shadowing Main.R2.R2.a, Main.R1.R1.a
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
a is shadowing Main.R2.R2.a, Main.R1.R1.a
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
a is shadowing Main.R2.R2.a, Main.R1.R1.a
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
a is shadowing Main.R2.R2.a, Main.R1.R1.a
b is shadowing Main.Other.b
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
a is shadowing Main.R2.R2.a, Main.R1.R1.a
b is shadowing Main.Other.b
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
a is shadowing Main.R2.R2.a, Main.R1.R1.a
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
a is shadowing Main.R2.R2.a, Main.R1.R1.a
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
a is shadowing Main.R2.R2.a, Main.R1.R1.a
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
a is shadowing Main.R2.R2.a, Main.R1.R1.a
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
a is shadowing Main.R2.R2.a, Main.R1.R1.a
Error: While processing right hand side of r2_shouldNotTypecheck1. Ambiguous elaboration. Possible results:
Main.R2.MkR
Main.R1.MkR Type

9
tests/idris2/coverage015/expected
View File

@ -37,6 +37,15 @@ Missing cases:
test'' _
1/1: Building Issue1366 (Issue1366.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
f is shadowing Main.f
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
f is shadowing Main.f
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
f is shadowing Main.f
Error: decode is not covering.
Issue1366.idr:33:1--33:45

3
tests/idris2/interface008/expected
View File

@ -1,4 +1,7 @@
1/1: Building Deps (Deps.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
card is shadowing Main.card
Error: While processing right hand side of badcard. k is not accessible in this context.
Deps.idr:18:13--18:14

3
tests/idris2/real001/expected
View File

@ -1,3 +1,6 @@
1/3: Building Linear (Linear.idr)
2/3: Building Channel (Channel.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
any is shadowing Prelude.Interfaces.any
3/3: Building TestProto (TestProto.idr)

6
tests/idris2/real002/expected
View File

@ -1,4 +1,10 @@
1/3: Building Control.App (Control/App.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
any is shadowing Prelude.Interfaces.any
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
any is shadowing Prelude.Interfaces.any
2/3: Building Control.App.Console (Control/App/Console.idr)
3/3: Building Store (Store.idr)
3/3: Building StoreL (StoreL.idr)

6
tests/idris2/reflection006/expected
View File

@ -2,6 +2,12 @@
LOG 0: [x, y]
LOG 0: Left: ((Prelude.Types.plus x) y)
LOG 0: Right: ((Prelude.Types.plus y) x)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
any is shadowing Prelude.Interfaces.any
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
any is shadowing Prelude.Interfaces.any
Error: While processing right hand side of commutes. Error during reflection: Not done
refleq.idr:24:16--24:21

3
tests/idris2/warning001/Issue1401.idr Normal file
View File

@ -0,0 +1,3 @@
fstDup: (xs : List a) -> map fst (map dup xs) === xs
fstDup Nil = Refl
fstDup (x::xs) = ?a

11
tests/idris2/warning001/Issue539.idr Normal file
View File

@ -0,0 +1,11 @@
idF : a -> a
idF = id
extensionality : (f : a -> b) -> (g : a -> b) -> ((x : a) -> f x = g x) -> f = g
extensionality f g = believe_me
leftIdPoint : (f : a -> b) -> (x : a) -> idF (f x) = f x
leftIdPoint f x = Refl
leftId : (f : a -> b) -> (idF . f = f)
leftId f = ?hole

9
tests/idris2/warning001/Issue621.idr Normal file
View File

@ -0,0 +1,9 @@
a1 : Char
a1 = 'a'
a2 : Char
a2 = 'a'
whyNot : a1 = a2
whyNot = ?hole

16
tests/idris2/warning001/PR1407.idr Normal file
View File

@ -0,0 +1,16 @@
namespace Hoo
f : Either a b -> Either b a
f (Left a) = Right a
f (Right b) = Left b
natural : (xs : Either a b) -> ((f . f) . map g) xs === (map g . (f . f)) xs
natural = ?l
mutual
g : h === h
g = Refl
h : g === g
h = Refl

21
tests/idris2/warning001/expected Normal file
View File

@ -0,0 +1,21 @@
1/1: Building Issue539 (Issue539.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
idF is shadowing Main.idF
1/1: Building Issue621 (Issue621.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
a1 is shadowing Main.a1
a2 is shadowing Main.a2
1/1: Building Issue1401 (Issue1401.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
fst is shadowing Builtin.fst, Builtin.DPair.DPair.fst
dup is shadowing Prelude.Basics.dup
1/1: Building PR1407 (PR1407.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
f is shadowing Main.Hoo.f
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
g is shadowing Main.g

6
tests/idris2/warning001/run Executable file
View File

@ -0,0 +1,6 @@
$1 --no-color --console-width 0 --check Issue539.idr
$1 --no-color --console-width 0 --check Issue621.idr
$1 --no-color --console-width 0 --check Issue1401.idr
$1 --no-color --console-width 0 --check PR1407.idr
rm -rf build

15
tests/typedd-book/chapter03/expected
View File

@ -1,6 +1,21 @@
1/8: Building IsEven (IsEven.idr)
2/8: Building Matrix (Matrix.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Data.Vect.elem, Prelude.Types.elem
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Data.Vect.elem, Prelude.Types.elem
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Data.Vect.elem, Prelude.Types.elem
3/8: Building VecSort (VecSort.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Data.Vect.elem, Prelude.Types.elem
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Data.Vect.elem, Prelude.Types.elem
4/8: Building Vectors (Vectors.idr)
5/8: Building WordLength (WordLength.idr)
6/8: Building WordLength_vec (WordLength_vec.idr)

21
tests/typedd-book/chapter04/expected
View File

@ -1,4 +1,13 @@
1/12: Building BSTree (BSTree.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Prelude.Types.elem
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Prelude.Types.elem
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Prelude.Types.elem
2/12: Building DataStore (DataStore.idr)
3/12: Building Direction (Direction.idr)
4/12: Building Generic (Generic.idr)
@ -6,7 +15,19 @@
6/12: Building Shape (Shape.idr)
7/12: Building SumInputs (SumInputs.idr)
8/12: Building Tree (Tree.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Prelude.Types.elem
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Prelude.Types.elem
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Prelude.Types.elem
9/12: Building TryIndex (TryIndex.idr)
10/12: Building Vect (Vect.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Prelude.Types.elem
11/12: Building Vehicle (Vehicle.idr)
12/12: Building All (All.idr)

30
tests/typedd-book/chapter06/expected
View File

@ -1,6 +1,36 @@
1/8: Building Adder (Adder.idr)
2/8: Building DataStore (DataStore.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
schema is shadowing Main.DataStore.schema
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
schema is shadowing Main.DataStore.schema
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
schema is shadowing Main.DataStore.schema
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
schema is shadowing Main.DataStore.schema
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
schema is shadowing Main.DataStore.schema
3/8: Building DataStoreHoles (DataStoreHoles.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
schema is shadowing Main.DataStore.schema
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
schema is shadowing Main.DataStore.schema
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
schema is shadowing Main.DataStore.schema
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
schema is shadowing Main.DataStore.schema
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
schema is shadowing Main.DataStore.schema
4/8: Building Maybe (Maybe.idr)
5/8: Building Printf (Printf.idr)
6/8: Building TypeFuns (TypeFuns.idr)

12
tests/typedd-book/chapter07/expected
View File

@ -3,4 +3,16 @@
3/6: Building Expr (Expr.idr)
4/6: Building Fold (Fold.idr)
5/6: Building Tree (Tree.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Prelude.Types.elem
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Prelude.Types.elem
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Prelude.Types.elem
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Prelude.Types.elem
6/6: Building All (All.idr)

9
tests/typedd-book/chapter08/expected
View File

@ -1,4 +1,13 @@
1/10: Building AppendVec (AppendVec.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Data.Vect.elem, Prelude.Types.elem
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Data.Vect.elem, Prelude.Types.elem
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Data.Vect.elem, Prelude.Types.elem
2/10: Building CheckEqDec (CheckEqDec.idr)
3/10: Building CheckEqMaybe (CheckEqMaybe.idr)
4/10: Building EqNat (EqNat.idr)

3
tests/typedd-book/chapter11/expected
View File

@ -5,6 +5,9 @@
5/12: Building Greet (Greet.idr)
6/12: Building InfIO (InfIO.idr)
7/12: Building InfList (InfList.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
elem is shadowing Prelude.Types.elem
8/12: Building Label (Label.idr)
9/12: Building RunIO (RunIO.idr)
10/12: Building Streams (Streams.idr)

12
tests/typedd-book/chapter12/expected
View File

@ -1,5 +1,17 @@
1/10: Building ArithState (ArithState.idr)
2/10: Building DataStore (DataStore.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
schema is shadowing Main.DataStore.schema
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
schema is shadowing Main.DataStore.schema
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
schema is shadowing Main.DataStore.schema
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
schema is shadowing Main.DataStore.schema
3/10: Building Record (Record.idr)
4/10: Building State (State.idr)
5/10: Building StateMonad (StateMonad.idr)

3
tests/typedd-book/chapter14/expected
View File

@ -1,4 +1,7 @@
1/4: Building DoorJam (DoorJam.idr)
2/4: Building ATM (ATM.idr)
3/4: Building Hangman (Hangman.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
letters is shadowing Main.letters
4/4: Building All (All.idr)