From 34251db6d1325b8e7a3ca06153047db61b9a3927 Mon Sep 17 00:00:00 2001 From: Robert Wright Date: Sun, 11 Jun 2023 14:23:16 +0100 Subject: [PATCH] Generalize Prelude proof helpers --- libs/base/Control/Function.idr | 2 +- libs/base/Data/Fin/Order.idr | 2 +- libs/base/Data/Nat.idr | 2 +- libs/base/Data/Vect.idr | 2 +- libs/base/Decidable/Equality/Core.idr | 2 +- libs/papers/Data/Container.idr | 6 +- libs/papers/Search/Auto.idr | 6 +- libs/prelude/Prelude/Basics.idr | 6 +- src/Core/Case/CaseBuilder.idr | 2 +- src/Core/Name.idr | 2 +- src/Core/TT.idr | 2 +- tests/idris2/evaluator002/expected | 138 +++++++++++++------------- tests/idris2/spec001/expected | 12 +-- tests/idris2/with010/NestedWith.idr | 4 +- 14 files changed, 94 insertions(+), 94 deletions(-) diff --git a/libs/base/Control/Function.idr b/libs/base/Control/Function.idr index a67e80a9a6e..d8b572a6233 100644 --- a/libs/base/Control/Function.idr +++ b/libs/base/Control/Function.idr @@ -53,7 +53,7 @@ public export public export [BiinjFromComp] {f : a -> b -> c} -> {g : c -> d} -> Biinjective (g .: f) => Biinjective f where - biinjective = biinjective {f = (g .: f)} . cong g + biinjective prf = biinjective {f = (g .: f)} $ cong g prf public export [FlipBiinjective] {f : a -> b -> c} -> diff --git a/libs/base/Data/Fin/Order.idr b/libs/base/Data/Fin/Order.idr index c7dac22a148..cba8ee8709c 100644 --- a/libs/base/Data/Fin/Order.idr +++ b/libs/base/Data/Fin/Order.idr @@ -43,7 +43,7 @@ using (k : Nat) connex {x = FZ} _ = Left $ FromNatPrf LTEZero connex {y = FZ} _ = Right $ FromNatPrf LTEZero connex {x = FS k} {y = FS j} prf = - case connex {rel = FinLTE} $ prf . (cong FS) of + case connex {rel = FinLTE} $ \c => prf $ cong FS c of Left (FromNatPrf p) => Left $ FromNatPrf $ LTESucc p Right (FromNatPrf p) => Right $ FromNatPrf $ LTESucc p diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr index 2e33caf1cbb..f632c68dfea 100644 --- a/libs/base/Data/Nat.idr +++ b/libs/base/Data/Nat.idr @@ -123,7 +123,7 @@ Connex Nat LTE where connex {x = Z} _ = Left LTEZero connex {y = Z} _ = Right LTEZero connex {x = S _} {y = S _} prf = - case connex $ prf . (cong S) of + case connex $ \xy => prf $ cong S xy of Left jk => Left $ LTESucc jk Right kj => Right $ LTESucc kj diff --git a/libs/base/Data/Vect.idr b/libs/base/Data/Vect.idr index 31b80e8db22..92433bca937 100644 --- a/libs/base/Data/Vect.idr +++ b/libs/base/Data/Vect.idr @@ -259,7 +259,7 @@ replaceAtDiffIndexPreserves : (xs : Vect n a) -> (i, j : Fin n) -> Not (i = j) - replaceAtDiffIndexPreserves (_::_) FZ FZ co _ = absurd $ co Refl replaceAtDiffIndexPreserves (_::_) FZ (FS _) _ _ = Refl replaceAtDiffIndexPreserves (_::_) (FS _) FZ _ _ = Refl -replaceAtDiffIndexPreserves (_::_) (FS z) (FS w) co y = replaceAtDiffIndexPreserves _ z w (co . cong FS) y +replaceAtDiffIndexPreserves (_::_) (FS z) (FS w) co y = replaceAtDiffIndexPreserves _ z w (\zw => co $ cong FS zw) y -------------------------------------------------------------------------------- -- Transformations diff --git a/libs/base/Decidable/Equality/Core.idr b/libs/base/Decidable/Equality/Core.idr index 32130d40aae..12208e45fe6 100644 --- a/libs/base/Decidable/Equality/Core.idr +++ b/libs/base/Decidable/Equality/Core.idr @@ -45,7 +45,7 @@ decEqCong $ No contra = No $ \c => contra $ inj f c public export decEqInj : (0 _ : Injective f) => Dec (f x = f y) -> Dec (x = y) decEqInj $ Yes prf = Yes $ inj f prf -decEqInj $ No contra = No $ contra . cong f +decEqInj $ No contra = No $ \c => contra $ cong f c public export decEqCong2 : (0 _ : Biinjective f) => Dec (x = y) -> Lazy (Dec (v = w)) -> Dec (f x v = f y w) diff --git a/libs/papers/Data/Container.idr b/libs/papers/Data/Container.idr index 8bef70815c6..b014dedffad 100644 --- a/libs/papers/Data/Container.idr +++ b/libs/papers/Data/Container.idr @@ -288,12 +288,12 @@ namespace Derivative toPair v = case fromSum {c = Pair (Derivative c) d} {d = Pair c (Derivative d)} v of Left p => let (MkExtension (shp1 ** p1) chld1, MkExtension shp2 chld2) = fromPair {c = Derivative c} p in MkExtension ((shp1, shp2) ** Left p1) $ \ (p' ** neq) => case p' of - Left p1' => chld1 (p1' ** (neq . cong Left)) + Left p1' => chld1 (p1' ** (\prf => neq $ cong Left prf)) Right p2' => chld2 p2' Right p => let (MkExtension shp1 chld1, MkExtension (shp2 ** p2) chld2) = fromPair {c} {d = Derivative d} p in MkExtension ((shp1, shp2) ** Right p2) $ \ (p' ** neq) => case p' of Left p1' => chld1 p1' - Right p2' => chld2 (p2' ** (neq . cong Right)) + Right p2' => chld2 (p2' ** (\prf => neq $ cong Right prf)) export fromPair : Extension (Derivative (Pair c d)) x -> @@ -323,7 +323,7 @@ namespace Derivative right = toCompose $ MkExtension (shp1 ** p1) $ \ (p1' ** neqp1) => MkExtension (shp2 p1') - $ \ p2' => chld ((p1' ** p2') ** (neqp1 . cong fst)) + $ \ p2' => chld ((p1' ** p2') ** (\prf => neqp1 $ cong fst prf)) export toCompose : ((s : _) -> DecEq (Position c s)) -> ((s : _) -> DecEq (Position d s)) -> diff --git a/libs/papers/Search/Auto.idr b/libs/papers/Search/Auto.idr index 87853d8d8f7..0448cf2771b 100644 --- a/libs/papers/Search/Auto.idr +++ b/libs/papers/Search/Auto.idr @@ -259,8 +259,8 @@ thinApart FZ FZ neq = absurd (neq Refl) thinApart FZ (FS y') neq = (y' ** Refl) thinApart (FS FZ) FZ neq = (FZ ** Refl) thinApart (FS (FS x)) FZ neq = (FZ ** Refl) -thinApart (FS x@FZ) (FS y) neq = bimap FS (cong FS) (thinApart x y (neq . cong FS)) -thinApart (FS x@(FS{})) (FS y) neq = bimap FS (cong FS) (thinApart x y (neq . cong FS)) +thinApart (FS x@FZ) (FS y) neq = bimap FS (\prf => cong FS prf) (thinApart x y (\prf => neq $ cong FS prf)) +thinApart (FS x@(FS{})) (FS y) neq = bimap FS (\prf => cong FS prf) (thinApart x y (\prf => neq $ cong FS prf)) public export data Thicken : (x, y : Fin n) -> Type where @@ -462,7 +462,7 @@ apply r args = let (premises, rest) = splitAt r.arity args in mkVars : (m : Nat) -> (vars : SnocList Name ** length vars = m) mkVars Z = ([<] ** Refl) -mkVars m@(S m') = bimap (:< UN (Basic $ "_invalidName" ++ show m)) (cong S) (mkVars m') +mkVars m@(S m') = bimap (:< UN (Basic $ "_invalidName" ++ show m)) (\prf => cong S prf) (mkVars m') solveAcc : {m : _} -> Nat -> HintDB -> PartialProof m -> Space Proof solveAcc idx rules (MkPartialProof 0 goals k) diff --git a/libs/prelude/Prelude/Basics.idr b/libs/prelude/Prelude/Basics.idr index c953c1d6f3e..87ad2e50eed 100644 --- a/libs/prelude/Prelude/Basics.idr +++ b/libs/prelude/Prelude/Basics.idr @@ -99,18 +99,18 @@ public export ||| Equality is a congruence. public export -cong : (0 f : t -> u) -> (p : a = b) -> f a = f b +cong : (0 f : t -> u) -> (0 p : a = b) -> f a = f b cong f Refl = Refl ||| Two-holed congruence. export -- These are natural in equational reasoning. -cong2 : (0 f : t1 -> t2 -> u) -> (p1 : a = b) -> (p2 : c = d) -> f a c = f b d +cong2 : (0 f : t1 -> t2 -> u) -> (0 p1 : a = b) -> (0 p2 : c = d) -> f a c = f b d cong2 f Refl Refl = Refl ||| Irrelevant equalities can always be made relevant export -irrelevantEq : (0 _ : a === b) -> a === b +irrelevantEq : (0 _ : a ~=~ b) -> a ~=~ b irrelevantEq Refl = Refl -------------- diff --git a/src/Core/Case/CaseBuilder.idr b/src/Core/Case/CaseBuilder.idr index babea82350c..257c1f1a05f 100644 --- a/src/Core/Case/CaseBuilder.idr +++ b/src/Core/Case/CaseBuilder.idr @@ -381,7 +381,7 @@ conTypeEq (CName x tag) (CName x' tag') Yes Refl => Just Refl No contra => Nothing conTypeEq CDelay CDelay = Just Refl -conTypeEq (CConst x) (CConst y) = cong CConst <$> constantEq x y +conTypeEq (CConst x) (CConst y) = (\xy => cong CConst xy) <$> constantEq x y conTypeEq _ _ = Nothing data Group : List Name -> -- variables in scope diff --git a/src/Core/Name.idr b/src/Core/Name.idr index 96b538604ec..7e3cf9ce1a0 100644 --- a/src/Core/Name.idr +++ b/src/Core/Name.idr @@ -410,7 +410,7 @@ nameEq (NS xs x) (NS ys y) with (decEq xs ys) nameEq (NS ys x) (NS ys y) | (Yes Refl) | Nothing = Nothing nameEq (NS ys y) (NS ys y) | (Yes Refl) | (Just Refl) = Just Refl nameEq (NS xs x) (NS ys y) | (No contra) = Nothing -nameEq (UN x) (UN y) = map (cong UN) (userNameEq x y) +nameEq (UN x) (UN y) = map (\xy => cong UN xy) (userNameEq x y) nameEq (MN x t) (MN x' t') with (decEq x x') nameEq (MN x t) (MN x t') | (Yes Refl) with (decEq t t') nameEq (MN x t) (MN x t) | (Yes Refl) | (Yes Refl) = Just Refl diff --git a/src/Core/TT.idr b/src/Core/TT.idr index 65750a260bd..47ae541c5a7 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -189,7 +189,7 @@ constantEq (Ch x) (Ch y) = case decEq x y of Yes Refl => Just Refl No contra => Nothing constantEq (Db x) (Db y) = Nothing -- no DecEq for Doubles! -constantEq (PrT x) (PrT y) = cong PrT <$> primTypeEq x y +constantEq (PrT x) (PrT y) = (\xy => cong PrT xy) <$> primTypeEq x y constantEq WorldVal WorldVal = Just Refl constantEq _ _ = Nothing diff --git a/tests/idris2/evaluator002/expected b/tests/idris2/evaluator002/expected index 184bd95f8b9..f114eeba77f 100644 --- a/tests/idris2/evaluator002/expected +++ b/tests/idris2/evaluator002/expected @@ -1,89 +1,89 @@ 1/2: Building Lib (Lib.idr) -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.{_:2555} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2559} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556} +LOG eval.stuck.outofscope:5: Stuck function: {_:2561} 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: {_:2564} -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.{_:2566} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2567} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2567} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2567} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2567} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2567} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2566} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2566} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2566} -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:2570} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2567} -LOG eval.stuck.outofscope:5: Stuck function: {_:2573} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2574} +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.{_:2563} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563} +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:2567} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564} +LOG eval.stuck.outofscope:5: Stuck function: {_:2570} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2571} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2572} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2572} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2572} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575} LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575} LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575} LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2578} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2578} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2578} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2578} LOG eval.stuck.outofscope:5: Stuck function: Prelude.Types.List.reverse -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2593} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2594} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2594} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2594} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2594} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2594} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2594} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2594} -LOG eval.stuck.outofscope:5: Stuck function: {_:2597} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2598} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2599} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2599} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2599} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2601} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2590} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591} +LOG eval.stuck.outofscope:5: Stuck function: {_:2594} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2595} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2596} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2596} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2596} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2598} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2598} LOG eval.stuck.outofscope:5: Stuck function: Lib.accMapAux 2/2: Building Main (Main.idr) -LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2603} +LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2600} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2600} +LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2600} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} -LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2603} -LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2603} LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2607} LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2607} LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2607} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610} LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2612} LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2613} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2613} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2615} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2613} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2613} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} -LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2624} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} -LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2624} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2621} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2621} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} 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 diff --git a/tests/idris2/spec001/expected b/tests/idris2/spec001/expected index aca2f77acae..2caaca59cd3 100644 --- a/tests/idris2/spec001/expected +++ b/tests/idris2/spec001/expected @@ -27,18 +27,18 @@ LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582 LOG specialise:5: New RHS: (alg[0] (Prelude.Types.bimap (Builtin.Pair a[1] a[1]) (Builtin.Pair (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec)))) Builtin.Unit Builtin.Unit (Prelude.Basics.id Builtin.Unit) \({arg:2} : (Builtin.Pair (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))))) => (Prelude.Types.bimap a[2] (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) a[2] (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (_PE.PE_fold_3a845f1ca594c582 a[2] alg[1]) (_PE.PE_fold_3a845f1ca594c582 a[2] alg[1]) {arg:2}[0]) t[2])) LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582 1/1: Building Desc2 (Desc2.idr) -LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_8abb50b713fe8e5e by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8738} : a[0]) -> b[2]) => \({arg:8743} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapImpl b[3] a[2] func[1] {arg:8743}[0]))), (3, Dynamic) +LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_8abb50b713fe8e5e by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8742} : a[0]) -> b[2]) => \({arg:8747} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapImpl b[3] a[2] func[1] {arg:8747}[0]))), (3, Dynamic) LOG specialise:3: Specialised type _PE.PE_fold_8abb50b713fe8e5e: ({arg:840} : ({arg:842} : (Prelude.Basics.List Prelude.Types.Nat)) -> Prelude.Types.Nat) -> ({arg:847} : (Main.Mu Prelude.Basics.List)) -> Prelude.Types.Nat LOG specialise:5: Attempting to specialise: -(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8792} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t)) +(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8796} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t)) LOG specialise:5: New patterns for _PE.PE_fold_8abb50b713fe8e5e: -((_PE.PE_fold_8abb50b713fe8e5e alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8792} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8743}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8743}))))))]) alg)) t)) -LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_a727631bc09e3761 by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8738} : a[0]) -> b[2]) => \({arg:8743} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapAppend a[2] b[3] (Prelude.Basics.Lin b[3]) func[1] {arg:8743}[0]))), (3, Dynamic) +((_PE.PE_fold_8abb50b713fe8e5e alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8796} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8747}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8747}))))))]) alg)) t)) +LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_a727631bc09e3761 by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8742} : a[0]) -> b[2]) => \({arg:8747} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapAppend a[2] b[3] (Prelude.Basics.Lin b[3]) func[1] {arg:8747}[0]))), (3, Dynamic) LOG specialise:3: Specialised type _PE.PE_fold_a727631bc09e3761: ({arg:840} : ({arg:842} : (Prelude.Basics.List Prelude.Types.Nat)) -> Prelude.Types.Nat) -> ({arg:847} : (Main.Mu Prelude.Basics.List)) -> Prelude.Types.Nat LOG specialise:5: Attempting to specialise: -(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8792} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t)) +(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8796} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t)) LOG specialise:5: New patterns for _PE.PE_fold_a727631bc09e3761: -((_PE.PE_fold_a727631bc09e3761 alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8792} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8743}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8743}))))))]) alg)) t)) +((_PE.PE_fold_a727631bc09e3761 alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8796} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8747}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8747}))))))]) alg)) t)) LOG specialise:5: Already specialised _PE.PE_fold_a727631bc09e3761 LOG specialise:5: New RHS: (alg[0] (Prelude.Types.List.mapAppend (Main.Mu Prelude.Basics.List) Prelude.Types.Nat (Prelude.Basics.Lin Prelude.Types.Nat) (_PE.PE_fold_a727631bc09e3761 alg[0]) t[1])) LOG specialise:5: Already specialised _PE.PE_fold_a727631bc09e3761 diff --git a/tests/idris2/with010/NestedWith.idr b/tests/idris2/with010/NestedWith.idr index 1eda843f366..35aa5d598bc 100644 --- a/tests/idris2/with010/NestedWith.idr +++ b/tests/idris2/with010/NestedWith.idr @@ -8,5 +8,5 @@ interface DecEq a where (DecEq a, DecEq b) => DecEq (a, b) where decEq (x, y) (a, b) with (decEq x a) | (decEq y b) _ | Yes eqL | Yes eqR = Yes (cong2 (,) eqL eqR) - _ | No neqL | _ = No (neqL . cong fst) - _ | _ | No neqR = No (neqR . cong snd) + _ | No neqL | _ = No $ \prf => neqL $ cong fst prf + _ | _ | No neqR = No $ \prf => neqR $ cong snd prf