git.iko.soy/generic-lens
on master help sign in
Switch from ghc-proofs to inspection-testing (#15)
85974a2Joachim Breitner
generic-lens.cabal+1−1
compare with master
unifiedsplit
@@ -68,7 +68,7 @@ test-suite generic-lens-test
68
68
69 build-depends: base >= 4.9 && <= 5.0
69 build-depends: base >= 4.9 && <= 5.0
70 , generic-lens
70 , generic-lens
71− , ghc-proofs >= 0.1.1
71+ , inspection-testing >= 0.1
72
72
73 default-language: Haskell2010
73 default-language: Haskell2010
74 ghc-options: -Wall
74 ghc-options: -Wall
stack.yaml+1−1
@@ -4,7 +4,7 @@ packages:
4- '.'
4- '.'
5
5
6extra-deps:
6extra-deps:
7−- 'ghc-proofs-0.1.1'
7+- 'inspection-testing-0.1'
8
8
9flags: {}
9flags: {}
10
10
test/Spec.hs+27−14
@@ -1,4 +1,4 @@
1−{-# OPTIONS_GHC -O -fplugin GHC.Proof.Plugin #-}
1+{-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}
2
2
3{-# LANGUAGE AllowAmbiguousTypes #-}
3{-# LANGUAGE AllowAmbiguousTypes #-}
4{-# LANGUAGE DataKinds #-}
4{-# LANGUAGE DataKinds #-}
@@ -8,12 +8,16 @@
8{-# LANGUAGE RankNTypes #-}
8{-# LANGUAGE RankNTypes #-}
9{-# LANGUAGE ScopedTypeVariables #-}
9{-# LANGUAGE ScopedTypeVariables #-}
10{-# LANGUAGE TypeApplications #-}
10{-# LANGUAGE TypeApplications #-}
11+{-# LANGUAGE TemplateHaskell #-}
12+{-# LANGUAGE CPP #-}
11
13
12module Main where
14module Main where
13
15
14import GHC.Generics
16import GHC.Generics
15import Data.Generics.Product
17import Data.Generics.Product
16−import GHC.Proof
18+#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0)
19+import Test.Inspection
20+#endif
17
21
18main :: IO ()
22main :: IO ()
19main = putStrLn "Hello world"
23main = putStrLn "Hello world"
@@ -42,19 +46,28 @@ subtypeLensManual f record
42
46
43--------------------------------------------------------------------------------
47--------------------------------------------------------------------------------
44-- * Tests
48-- * Tests
45−-- The ghc-proofs plugin checks that the following equalities hold, by checking
49+-- The inspection-testing plugin checks that the following equalities hold, by
46−-- that the LHSs and the RHSs are CSEd. This also means that the runtime
50+-- checking that the LHSs and the RHSs are CSEd. This also means that the
47−-- characteristics of the derived lenses is the same as the manually written
51+-- runtime characteristics of the derived lenses is the same as the manually
48−-- ones above.
52+-- written ones above.
49
53
50−fieldP :: Proof
54+fieldALensName :: Lens' Record Int
51−fieldP = L fieldALensManual === L (field @"fieldA")
55+fieldALensName = field @"fieldA"
52
56
53−typedP :: Proof
57+fieldALensType :: Lens' Record Int
54−typedP = L fieldALensManual === L (typed @Int)
58+fieldALensType = typed @Int
55
59
56−posP :: Proof
60+fieldALensPos :: Lens' Record Int
57−posP = L fieldALensManual === L (position @1)
61+fieldALensPos = position @1
58
62
59−subtypeP :: Proof
63+subtypeLensGeneric :: Lens' Record Record2
64+subtypeLensGeneric = super
65+
66+#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0)
67+-- It turns out that these equalities only hold with ghc-8.2 or newer,
68+-- probably due to improvements to CSE
69+inspect $ 'fieldALensManual === 'fieldALensName
70+inspect $ 'fieldALensManual === 'fieldALensType
71+inspect $ 'fieldALensManual === 'fieldALensPos
60−subtypeP = L subtypeLensManual === L super
72+inspect $ 'subtypeLensManual === 'subtypeLensGeneric
73+#endif