Skip to content

Commit d3e7612

Browse files
cstmlcstml
committed
update: add failing test
1 parent 3f37ee8 commit d3e7612

File tree

3 files changed

+142
-157
lines changed

3 files changed

+142
-157
lines changed

‎lambda-buffers-compiler/lambda-buffers-compiler.cabal‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,9 @@ common common-language
8282
default-language: Haskell2010
8383

8484
common common-imports
85-
build-depends: base >=4.16
85+
build-depends:
86+
, base >=4.16
87+
, lens >=5.2
8688

8789
library
8890
import: common-language
@@ -92,7 +94,6 @@ library
9294
, freer-simple >=1.2
9395
, generic-lens >=2.2
9496
, lambda-buffers-compiler-pb >=0.1.0.0
95-
, lens >=5.2
9697
, mtl >=2.2
9798
, parsec >=3.1
9899
, prettyprinter >=1.7
@@ -121,7 +122,6 @@ executable lambda-buffers-compiler-cli
121122
, bytestring >=0.11
122123
, lambda-buffers-compiler
123124
, lambda-buffers-compiler-pb >=0.1.0.0
124-
, lens >=5.2
125125
, optparse-applicative >=0.17
126126
, proto-lens >=0.7
127127
, text >=1.2
@@ -138,7 +138,6 @@ test-suite tests
138138
build-depends:
139139
, lambda-buffers-compiler
140140
, lambda-buffers-compiler-pb >=0.1
141-
, lens >=5.2
142141
, proto-lens >=0.7
143142
, tasty >=1.4
144143
, tasty-hunit >=0.10

‎lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,9 @@ import Data.Map qualified as M
4242
--------------------------------------------------------------------------------
4343
-- Types
4444

45+
-- FIXME(cstml) - We should add the following tests:
46+
-- - double declaration of a type
47+
4548
-- | Kind Check failure types.
4649
data KindCheckFailure
4750
= CheckFailure String
@@ -330,6 +333,7 @@ foreignTyRef2Type ftr = do
330333
let moduleName = flattenModuleName (ftr ^. #moduleName)
331334
pure $ Var $ moduleName <> "." <> (ftr ^. #tyName . #name)
332335

336+
--------------------------------------------------------------------------------
333337
-- Utilities
334338

335339
foldWithApp :: NonEmpty Type -> Type

‎lambda-buffers-compiler/test/Test/KindCheck.hs‎

Lines changed: 135 additions & 153 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,10 @@
1+
{-# LANGUAGE DuplicateRecordFields #-}
2+
{-# LANGUAGE OverloadedLabels #-}
13
{-# OPTIONS_GHC -Wno-missing-signatures #-}
24

35
module Test.KindCheck (test) where
46

7+
import Control.Lens ((%~), (&), (.~))
58
import Data.List.NonEmpty (NonEmpty ((:|)), cons)
69
import LambdaBuffers.Compiler.KindCheck (
710
check,
@@ -11,93 +14,155 @@ import LambdaBuffers.Compiler.KindCheck (
1114
import LambdaBuffers.Compiler.KindCheck.Type (Type (App, Var))
1215
import LambdaBuffers.Compiler.ProtoCompat qualified as P
1316
import Test.Tasty (TestTree, testGroup)
14-
import Test.Tasty.HUnit (testCase, (@?=))
17+
import Test.Tasty.HUnit (assertBool, testCase, (@?=))
1518

1619
test :: TestTree
1720
test = testGroup "Compiler tests" [testCheck, testFolds]
1821

1922
--------------------------------------------------------------------------------
2023
-- Module tests
2124

22-
testCheck = testGroup "KindChecker Tests" [trivialKCTest, kcTestMaybe]
25+
testCheck = testGroup "KindChecker Tests" [trivialKCTest, kcTestMaybe, kcTestFailing]
2326

2427
trivialKCTest =
2528
testCase "Empty CompInput should check." $
2629
check (P.CompilerInput []) @?= Right ()
2730

2831
kcTestMaybe =
29-
testCase "Maybe should psss." $
32+
testCase "Maybe should pass." $
3033
check ci1 @?= Right ()
3134

35+
kcTestFailing =
36+
testCase "This should fail." $
37+
assertBool "Test should have failed." $
38+
check ci2 /= Right ()
39+
40+
esi = P.SourceInfo "Empty Info" (P.SourcePosition 0 0) (P.SourcePosition 0 1)
41+
42+
modMaybe =
43+
P.Module
44+
{ P.moduleName =
45+
P.ModuleName
46+
{ P.parts = [P.ModuleNamePart "Module" esi]
47+
, P.sourceInfo = esi
48+
}
49+
, P.typeDefs =
50+
[ P.TyDef
51+
{ P.tyName = P.TyName "Maybe" esi
52+
, P.tyAbs =
53+
P.TyAbs
54+
{ P.tyArgs =
55+
[ P.TyArg
56+
{ P.argName = P.VarName "a" esi
57+
, P.argKind =
58+
P.Kind
59+
{ P.kind = P.KindRef P.KType
60+
, P.sourceInfo = esi
61+
}
62+
, P.sourceInfo = esi
63+
}
64+
]
65+
, P.tyBody =
66+
P.SumI $
67+
P.Sum
68+
{ constructors =
69+
P.Constructor
70+
{ P.constrName = P.ConstrName {P.name = "Nothing", P.sourceInfo = esi}
71+
, P.product = P.TupleI $ P.Tuple {P.fields = [], P.sourceInfo = esi}
72+
}
73+
:| [ P.Constructor
74+
{ P.constrName = P.ConstrName {P.name = "Just", P.sourceInfo = esi}
75+
, P.product =
76+
P.TupleI $
77+
P.Tuple
78+
{ P.fields =
79+
[ P.TyVarI
80+
( P.TyVar
81+
{ P.varName =
82+
P.VarName
83+
{ P.name = "a"
84+
, P.sourceInfo = esi
85+
}
86+
, P.sourceInfo = esi
87+
}
88+
)
89+
]
90+
, P.sourceInfo = esi
91+
}
92+
}
93+
]
94+
, sourceInfo = esi
95+
}
96+
, P.sourceInfo = esi
97+
}
98+
, P.sourceInfo = esi
99+
}
100+
]
101+
, P.classDefs = mempty
102+
, P.instances = mempty
103+
, P.sourceInfo = esi
104+
}
105+
32106
ci1 :: P.CompilerInput
33-
ci1 =
34-
P.CompilerInput
35-
[ P.Module
36-
{ P.moduleName =
37-
P.ModuleName
38-
{ P.parts = [P.ModuleNamePart "Module" esi]
39-
, P.sourceInfo = esi
40-
}
41-
, P.typeDefs =
42-
[ P.TyDef
43-
{ P.tyName = P.TyName "Maybe" esi
44-
, P.tyAbs =
45-
P.TyAbs
46-
{ P.tyArgs =
47-
[ P.TyArg
48-
{ P.argName = P.VarName "a" esi
49-
, P.argKind =
50-
P.Kind
51-
{ P.kind = P.KindRef P.KType
52-
, P.sourceInfo = esi
53-
}
54-
, P.sourceInfo = esi
55-
}
56-
]
57-
, P.tyBody =
58-
P.SumI $
59-
P.Sum
60-
{ constructors =
61-
P.Constructor
62-
{ P.constrName = P.ConstrName {P.name = "Nothing", P.sourceInfo = esi}
63-
, P.product = P.TupleI $ P.Tuple {P.fields = [], P.sourceInfo = esi}
64-
}
65-
:| [ P.Constructor
66-
{ P.constrName = P.ConstrName {P.name = "Just", P.sourceInfo = esi}
67-
, P.product =
68-
P.TupleI $
69-
P.Tuple
70-
{ P.fields =
71-
[ P.TyVarI
72-
( P.TyVar
73-
{ P.varName =
74-
P.VarName
75-
{ P.name = "a"
76-
, P.sourceInfo = esi
77-
}
78-
, P.sourceInfo = esi
79-
}
80-
)
81-
]
82-
, P.sourceInfo = esi
83-
}
84-
}
85-
]
86-
, sourceInfo = esi
87-
}
88-
, P.sourceInfo = esi
89-
}
90-
, P.sourceInfo = esi
91-
}
92-
]
93-
, P.classDefs = mempty
94-
, P.instances = mempty
95-
, P.sourceInfo = esi
96-
}
97-
]
107+
ci1 = P.CompilerInput {P.modules = [modMaybe]}
108+
109+
{- | Maybe = ...
110+
B a = B Maybe
111+
112+
Should fail as B a defaults to B :: Type -> Type and Maybe is inferred as
113+
Type -> Type. This is an inconsistency failure.
114+
-}
115+
ci2 = ci1 & #modules .~ [addMod]
98116
where
99-
esi :: P.SourceInfo -- empty Source Info
100-
esi = P.SourceInfo "Empty Info" (P.SourcePosition 0 0) (P.SourcePosition 0 1)
117+
addMod =
118+
modMaybe
119+
& #typeDefs
120+
%~ ( <>
121+
[ -- B a = B Maybe
122+
P.TyDef
123+
{ P.tyName = P.TyName "B" esi
124+
, P.tyAbs =
125+
P.TyAbs
126+
{ P.tyArgs =
127+
[ P.TyArg
128+
{ P.argName = P.VarName "a" esi
129+
, P.argKind =
130+
P.Kind
131+
{ P.kind = P.KindRef P.KType
132+
, P.sourceInfo = esi
133+
}
134+
, P.sourceInfo = esi
135+
}
136+
]
137+
, P.tyBody =
138+
P.SumI $
139+
P.Sum
140+
{ constructors =
141+
P.Constructor
142+
{ P.constrName = P.ConstrName {P.name = "B", P.sourceInfo = esi}
143+
, P.product =
144+
P.TupleI $
145+
P.Tuple
146+
{ P.fields =
147+
[ P.TyRefI $
148+
P.LocalI $
149+
P.LocalRef
150+
{ P.tyName = P.TyName {P.name = "Maybe", P.sourceInfo = esi}
151+
, P.sourceInfo = esi
152+
}
153+
]
154+
, P.sourceInfo = esi
155+
}
156+
}
157+
:| []
158+
, sourceInfo = esi
159+
}
160+
, P.sourceInfo = esi
161+
}
162+
, P.sourceInfo = esi
163+
}
164+
]
165+
)
101166

102167
--------------------------------------------------------------------------------
103168
-- Fold tests
@@ -146,86 +211,3 @@ testSumFold3 =
146211
@?= App
147212
(App (Var "Σ") (Var "c"))
148213
(App (App (Var "Σ") (Var "b")) (Var "a"))
149-
150-
{-
151-
152-
runKC :: [TypeDefinition] -> Either KindCheckFailure [Kind]
153-
runKC = runKindCheckEff . kindCheckType
154-
155-
t1 :: TestTree
156-
t1 =
157-
testCase "No Definition, No Kinds" $
158-
runKC [] @?= Right []
159-
160-
t2 :: TestTree
161-
t2 =
162-
testCase "Maybe has the correct Kind" $
163-
runKC [tdMaybe] @?= Right [Type :->: Type]
164-
165-
t3 :: TestTree
166-
t3 =
167-
testCase "Maybe works correctly when used as a type" $
168-
runKC [tdT1, tdMaybe] @?= Right [Type :->: Type, Type :->: Type]
169-
170-
t4 :: TestTree
171-
t4 =
172-
testCase "Maybe and a term containing a maybe work correctly" $
173-
runKC [tdT1, tdMaybe, tdT2] @?= Right [Type :->: Type, Type :->: Type, Type :->: Type]
174-
175-
t5 :: TestTree
176-
t5 =
177-
testCase "Bad Type is caught and reported" $
178-
runKC [tdMaybe, tdBT0]
179-
@?= Left
180-
( InferenceFailed
181-
( TypeDefinition
182-
{ _td'name = "T"
183-
, _td'variables = []
184-
, _td'sop = App (Var "Maybe") (Var "Maybe")
185-
}
186-
)
187-
(ImpossibleUnificationErr "Cannot unify: * = * \8594 *\n")
188-
)
189-
190-
--------------------------------------------------------------------------------
191-
-- Manual type definitions.
192-
193-
tdMaybe :: TypeDefinition
194-
tdMaybe =
195-
TypeDefinition
196-
{ _td'name = "Maybe"
197-
, _td'variables = ["a"]
198-
, _td'sop =
199-
Abs "a" $
200-
App
201-
(App (Var "Either") (Var "()"))
202-
(Var "a")
203-
}
204-
205-
-- T1 ~ T a = T Maybe (Maybe a)
206-
tdT1 :: TypeDefinition
207-
tdT1 =
208-
TypeDefinition
209-
{ _td'name = "T"
210-
, _td'variables = ["b"]
211-
, _td'sop = Abs "b" $ App (Var "Maybe") (App (Var "Maybe") (Var "b"))
212-
}
213-
214-
-- T2 ~ T a = T Maybe (Maybe a)
215-
tdT2 :: TypeDefinition
216-
tdT2 =
217-
TypeDefinition
218-
{ _td'name = "T2"
219-
, _td'variables = ["a"]
220-
, _td'sop = Abs "a" $ App (Var "T") (App (Var "Maybe") (Var "a"))
221-
}
222-
223-
-- T2 ~ T = T Maybe Maybe
224-
tdBT0 :: TypeDefinition
225-
tdBT0 =
226-
TypeDefinition
227-
{ _td'name = "T"
228-
, _td'variables = []
229-
, _td'sop = App (Var "Maybe") (Var "Maybe")
230-
}
231-
-}

0 commit comments

Comments
 (0)