Skip to content

Commit

Permalink
[ fix ] Remove lambdas from top-level methods
Browse files Browse the repository at this point in the history
  • Loading branch information
@spcfox
spcfox committed Jan 22, 2025
1 parent 8e420d6 commit 340cf98
Show file tree
Hide file tree
Showing 14 changed files with 115 additions and 124 deletions.
17 changes: 1 addition & 16 deletions src/Idris/Elab/Interface.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,17 +191,13 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params sig
(MkImpTy vfc cn ty_imp))
let conapp = apply (IVar vfc cname)
(map (IBindVar EmptyFC) (map bindName allmeths))
let argns = getExplicitArgs 0 sig.type
-- eta expand the RHS so that we put implicits in the right place
let fnclause = PatClause vfc
(INamedApp vfc
(IVar cn.fc cn.val) -- See #3409
(UN $ Basic "__con")
conapp
)
(mkLam argns
(apply (IVar EmptyFC (methName sig.name.val))
(map (IVar EmptyFC) argns)))
(IVar EmptyFC (methName sig.name.val))
let fndef = IDef vfc cn.val [fnclause]
pure [tydecl, fndef]
where
Expand All @@ -219,17 +215,6 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params sig
applyCon n = let name = UN (Basic "__con") in
(n, INamedApp vfc (IVar vfc n) name (IVar vfc name))

getExplicitArgs : Int -> RawImp -> List Name
getExplicitArgs i (IPi _ _ Explicit n _ sc)
= MN "arg" i :: getExplicitArgs (i + 1) sc
getExplicitArgs i (IPi _ _ _ n _ sc) = getExplicitArgs i sc
getExplicitArgs i tm = []

mkLam : List Name -> RawImp -> RawImp
mkLam [] tm = tm
mkLam (x :: xs) tm
= ILam EmptyFC top Explicit (Just x) (Implicit vfc False) (mkLam xs tm)

bindName : Name -> String
bindName (UN n) = "__bind_" ++ displayUserName n
bindName (NS _ n) = bindName n
Expand Down
2 changes: 1 addition & 1 deletion tests/base/deriving_foldable/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ LOG derive.foldable.clauses:1:
foldMapIVect : {0 m : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> IVect {n = m} a -> b
foldMapIVect f (MkIVect x2) = foldMap f x2
LOG derive.foldable.clauses:1:
foldMapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> EqMap key {{conArg:5699} = eq} a -> b
foldMapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> EqMap key {{conArg:5696} = eq} a -> b
foldMapEqMap f (MkEqMap x3) = foldMap (foldMap f) x3
LOG derive.foldable.clauses:1:
foldMapTree : {0 l : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> Tree l a -> b
Expand Down
14 changes: 7 additions & 7 deletions tests/base/deriving_functor/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ LOG derive.functor.clauses:1:
LOG derive.functor.clauses:1:
mapBigTree : {0 a, b : Type} -> (a -> b) -> BigTree a -> BigTree b
mapBigTree f (End x1) = End (f x1)
mapBigTree f (Branch x1 x2 x3) = Branch x1 (map f x2) (\ {arg:4042} => mapBigTree f (x3 {arg:4042}))
mapBigTree f (Branch x1 x2 x3) = Branch x1 (map f x2) (\ {arg:4039} => mapBigTree f (x3 {arg:4039}))
mapBigTree f (Rose x1) = Rose (map (assert_total (mapBigTree f)) x1)
LOG derive.functor.clauses:1:
mapMatrix : {0 m, n : _} -> {0 a, b : Type} -> (a -> b) -> Matrix m n a -> Matrix m n b
Expand Down Expand Up @@ -59,7 +59,7 @@ LOG derive.functor.clauses:1:
LOG derive.functor.clauses:1:
mapFree : {0 f : _} -> {0 a, b : Type} -> (a -> b) -> Free f a -> Free f b
mapFree f (Pure x2) = Pure (f x2)
mapFree f (Bind x3 x4) = Bind x3 (\ {arg:5071} => mapFree f (x4 {arg:5071}))
mapFree f (Bind x3 x4) = Bind x3 (\ {arg:5068} => mapFree f (x4 {arg:5068}))
LOG derive.functor.assumption:10: I am assuming that the parameter m is a Functor
LOG derive.functor.clauses:1:
mapMaybeT : {0 m : _} -> Functor m => {0 a, b : Type} -> (a -> b) -> MaybeT m a -> MaybeT m b
Expand All @@ -75,20 +75,20 @@ LOG derive.functor.clauses:1:
mapIVect : {0 m : _} -> {0 a, b : Type} -> (a -> b) -> IVect {n = m} a -> IVect {n = m} b
mapIVect f (MkIVect x2) = MkIVect (map f x2)
LOG derive.functor.clauses:1:
mapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> (a -> b) -> EqMap key {{conArg:5684} = eq} a -> EqMap key {{conArg:5684} = eq} b
mapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> (a -> b) -> EqMap key {{conArg:5681} = eq} a -> EqMap key {{conArg:5681} = eq} b
mapEqMap f (MkEqMap x3) = MkEqMap (map (map f) x3)
LOG derive.functor.clauses:1:
mapCont : {0 r : _} -> {0 a, b : Type} -> (a -> b) -> Cont r a -> Cont r b
mapCont f (MkCont x2) = MkCont (\ {arg:6040} => x2 (\ {arg:6042} => {arg:6040} (f {arg:6042})))
mapCont f (MkCont x2) = MkCont (\ {arg:6037} => x2 (\ {arg:6039} => {arg:6037} (f {arg:6039})))
LOG derive.functor.clauses:1:
mapCont2 : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2 r e a -> Cont2 r e b
mapCont2 f (MkCont2 x3) = MkCont2 (\ {arg:6132} => \ {arg:6139} => x3 {arg:6132} (\ {arg:6141} => {arg:6139} (f {arg:6141})))
mapCont2 f (MkCont2 x3) = MkCont2 (\ {arg:6129} => \ {arg:6136} => x3 {arg:6129} (\ {arg:6138} => {arg:6136} (f {arg:6138})))
LOG derive.functor.clauses:1:
mapCont2' : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2' r e a -> Cont2' r e b
mapCont2' f (MkCont2' x3) = MkCont2' (\ {arg:6246} => x3 (mapFst (\ t => \ {arg:6248} => t (f {arg:6248})) {arg:6246}))
mapCont2' f (MkCont2' x3) = MkCont2' (\ {arg:6243} => x3 (mapFst (\ t => \ {arg:6245} => t (f {arg:6245})) {arg:6243}))
LOG derive.functor.clauses:1:
mapCont2'' : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2'' r e a -> Cont2'' r e b
mapCont2'' f (MkCont2'' x3) = MkCont2'' (\ {arg:6370} => x3 (Delay (mapFst (\ t => \ {arg:6373} => t (Delay (f {arg:6373}))) {arg:6370})))
mapCont2'' f (MkCont2'' x3) = MkCont2'' (\ {arg:6367} => x3 (Delay (mapFst (\ t => \ {arg:6370} => t (Delay (f {arg:6370}))) {arg:6367})))
LOG derive.functor.clauses:1:
mapWithImplicits : {0 a, b : Type} -> (a -> b) -> WithImplicits a -> WithImplicits b
mapWithImplicits f (MkImplicit {x = x1} x2) = MkImplicit {x = f x1} (f x2)
Expand Down
2 changes: 1 addition & 1 deletion tests/base/deriving_show/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ LOG derive.show.clauses:1:
LOG derive.show.assumption:10: I am assuming that the parameter key can be shown
LOG derive.show.assumption:10: I am assuming that the parameter val can be shown
LOG derive.show.clauses:1:
showPrecEqMap : {0 key : _} -> Show key => {0 eq, val : _} -> Show val => Prec -> EqMap key {{conArg:5120} = eq} val -> String
showPrecEqMap : {0 key : _} -> Show key => {0 eq, val : _} -> Show val => Prec -> EqMap key {{conArg:5117} = eq} val -> String
showPrecEqMap d (MkEqMap x0) = showCon d "MkEqMap" (showArg x0)
LOG derive.show.clauses:1:
showPrecX : Prec -> X -> String
Expand Down
2 changes: 1 addition & 1 deletion tests/base/deriving_traversable/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ LOG derive.traversable.clauses:1:
traverseIVect : {0 m : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> IVect {n = m} a -> f (IVect {n = m} b)
traverseIVect f (MkIVect x2) = MkIVect <$> (traverse f x2)
LOG derive.traversable.clauses:1:
traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13929} = eq} a -> f (EqMap key {{conArg:13929} = eq} b)
traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13924} = eq} a -> f (EqMap key {{conArg:13924} = eq} b)
traverseEqMap f (MkEqMap x3) = MkEqMap <$> (traverse (traverse f) x3)
LOG derive.traversable.clauses:1:
traverseTree : {0 l : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Tree l a -> f (Tree l b)
Expand Down
14 changes: 7 additions & 7 deletions tests/idris2/basic/basic044/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -117,33 +117,33 @@ Target type : ({arg:1} : (Data.Fin.Fin (Prelude.Types.S (Prelude.Types.S Prelude
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:3:
$resolved6
$resolved7
Target type : ?Vec.{a:4569}_[]
Target type : ?Vec.{a:4541}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:4:
(($resolved3 ((:: (fromInteger 0)) Nil)) Nil)
(($resolved4 ((:: (fromInteger 0)) Nil)) Nil)
(($resolved5 ((:: (fromInteger 0)) Nil)) Nil)
Target type : (Vec.Vec ?Vec.{a:4569}_[] ?Vec.{n:4568}_[])
Target type : (Vec.Vec ?Vec.{a:4541}_[] ?Vec.{n:4540}_[])
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:5:
(($resolved3 (fromInteger 0)) Nil)
(($resolved4 (fromInteger 0)) Nil)
(($resolved5 (fromInteger 0)) Nil)
Target type : ?Vec.{a:4572}_[]
Target type : ?Vec.{a:4544}_[]
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6:
($resolved1 0)
($resolved2 0)
With default. Target type : ?Vec.{a:4574}_[]
With default. Target type : ?Vec.{a:4546}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:7:
$resolved6
$resolved7
Target type : (Vec.Vec ?Vec.{a:4574}_[] ?Vec.{n:4573}_[])
Target type : (Vec.Vec ?Vec.{a:4546}_[] ?Vec.{n:4545}_[])
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6:
($resolved1 0)
($resolved2 0)
With default. Target type : ?Vec.{a:4573}_[]
With default. Target type : ?Vec.{a:4545}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:8:
$resolved6
$resolved7
Target type : (Vec.Vec ?Vec.{a:4572}_[] ?Vec.{n:4571}_[])
Target type : (Vec.Vec ?Vec.{a:4544}_[] ?Vec.{n:4543}_[])
LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:5:
(($resolved4 (fromInteger 0)) Nil)
Target type : (Prelude.Basics.List Prelude.Types.Nat)
Expand Down
2 changes: 1 addition & 1 deletion tests/idris2/error/error018/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ Issue1031-3:4:6--4:7

1/1: Building Issue1031-4 (Issue1031-4.idr)
Error: While processing left hand side of nice. Unsolved holes:
Main.{dotTm:815} introduced at:
Main.{dotTm:812} introduced at:
Issue1031-4:4:6--4:10
1 | %default total
2 |
Expand Down
150 changes: 75 additions & 75 deletions tests/idris2/evaluator/evaluator002/expected
View file
Original file line number Diff line number Diff line change
@@ -1,89 +1,89 @@
1/2: Building Lib (Lib.idr)
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2554}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
LOG eval.stuck.outofscope:5: Stuck function: {_:2556}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2545}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2545}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2545}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2545}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2549}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2546}
LOG eval.stuck.outofscope:5: Stuck function: {_:2551}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2552}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2552}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2552}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2553}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2553}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2553}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2553}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2554}
LOG eval.stuck.outofscope:5: Stuck function: {_:2560}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2561}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: {_:2565}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2566}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2565}
LOG eval.stuck.outofscope:5: Stuck function: Prelude.Types.List.reverse
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2585}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
LOG eval.stuck.outofscope:5: Stuck function: {_:2589}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2590}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2593}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2593}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2580}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2581}
LOG eval.stuck.outofscope:5: Stuck function: {_:2584}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2585}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2588}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2588}
LOG eval.stuck.outofscope:5: Stuck function: Lib.accMapAux
2/2: Building Main (Main.idr)
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2595}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2595}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2595}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2599}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2599}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2599}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2602}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2602}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2590}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2590}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2590}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2594}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2594}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2594}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2597}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2597}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2597}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2600}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2600}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2602}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2607}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2616}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2616}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2600}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2600}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2611}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2611}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.accMap
Main> LOG eval.stuck:5: Stuck function: Lib.accMapAux
LOG eval.stuck:5: Stuck function: Lib.accMapAux
Expand Down
6 changes: 3 additions & 3 deletions tests/idris2/evaluator/interpreter008/expected
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
1/1: Building Issue2041 (Issue2041.idr)
Error: Unsolved holes:
Main.{n:820} introduced at:
Main.{n:817} introduced at:
Issue2041:5:17--5:19
1 | ex : {n : Nat} -> String
2 | ex {n} = "hello" ++ show n
Expand All @@ -9,8 +9,8 @@ Issue2041:5:17--5:19
5 | main = putStrLn ex
^^

Main> Encountered unimplemented hole Main.{n:820}
Warning: compiling hole Main.{n:820}
Main> Encountered unimplemented hole Main.{n:817}
Warning: compiling hole Main.{n:817}
Main> Encountered unimplemented hole Main.{n:4}
Warning: compiling hole Main.{n:4}
Main>
Expand Down
Loading

0 comments on commit 340cf98

Please sign in to comment.