Skip to content

Commit 2ed02a2

Browse files
bladyjokerbladyjoker
authored
Merge pull request #69 from mlabs-haskell/compiler/additional-tests
Compiler: additional Tests
2 parents 39ef8b9 + 924cf85 commit 2ed02a2

File tree

6 files changed

+128
-13
lines changed

6 files changed

+128
-13
lines changed

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

Lines changed: 11 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -225,9 +225,17 @@ derive x = deriveTyAbs x
225225

226226
deriveTyApp :: PC.TyApp -> Derive Derivation
227227
deriveTyApp ap = do
228-
f <- deriveTy (ap ^. #tyFunc)
229-
args <- deriveTy `traverse` (ap ^. #tyArgs)
230-
applyDerivation f args
228+
c <- ask
229+
df <- deriveTy (ap ^. #tyFunc)
230+
foldrM
231+
( \arg df' -> do
232+
darg <- deriveTy arg
233+
v <- KVar <$> fresh
234+
tell [Constraint ((darg ^. d'kind) :->: v, df' ^. d'kind)]
235+
return $ Application (Judgement c (App (df' ^. d'type) (darg ^. d'type)) v) df' darg
236+
)
237+
df
238+
(ap ^. #tyArgs)
231239

232240
deriveTuple :: PC.Tuple -> Derive Derivation
233241
deriveTuple t = do
@@ -257,16 +265,6 @@ derive x = deriveTyAbs x
257265
tell $ Constraint <$> [(d1 ^. d'kind, KType), (d2 ^. d'kind, KType)]
258266
pure $ Application (Judgement ctx (Sum t1 t2) KType) d1 d2
259267

260-
applyDerivation :: Derivation -> [Derivation] -> Derive Derivation
261-
applyDerivation d1 = \case
262-
[] -> pure d1
263-
d : ds -> do
264-
c <- ask
265-
d2 <- applyDerivation d ds
266-
v <- KVar <$> fresh
267-
tell [Constraint ((d2 ^. d'kind) :->: v, d1 ^. d'kind)]
268-
pure $ Application (Judgement c (App (d ^. d'type) (d2 ^. d'type)) v) d1 d2
269-
270268
{- | Gets the binding from the context - if the variable is not bound throw an
271269
error.
272270
-}

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

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,9 @@ import Test.Utils.CompilerInput (
1717
compilerInput'either,
1818
compilerInput'incoherent,
1919
compilerInput'maybe,
20+
compilerInput'newTypeEither,
21+
compilerInput'newTypeEither',
22+
compilerInput'newTypeEither'',
2023
compilerInput'recDef,
2124
)
2225
import Test.Utils.Constructors (_CompilerInput)
@@ -46,6 +49,9 @@ testCheck =
4649
, kcTestEither
4750
, kcTestMaybe'n'Either
4851
, kcTestRec
52+
, kcWrappedTestEither
53+
, kcWrappedTestEither'
54+
, kcWrappedTestEither''
4955
]
5056

5157
trivialKCTest :: TestTree
@@ -63,6 +69,21 @@ kcTestEither =
6369
testCase "Kind check Either." $
6470
check_ compilerInput'either @?= Right ()
6571

72+
kcWrappedTestEither :: TestTree
73+
kcWrappedTestEither =
74+
testCase "Kind check Either + Wrapped Either." $
75+
check_ compilerInput'newTypeEither @?= Right ()
76+
77+
kcWrappedTestEither' :: TestTree
78+
kcWrappedTestEither' =
79+
testCase "Kind check Either (defined Opaque) + Wrapped Either." $
80+
check_ compilerInput'newTypeEither' @?= Right ()
81+
82+
kcWrappedTestEither'' :: TestTree
83+
kcWrappedTestEither'' =
84+
testCase "Kind check Either + Wrapped (Either Int Int) ." $
85+
check_ compilerInput'newTypeEither'' @?= Right ()
86+
6687
kcTestMaybe'n'Either :: TestTree
6788
kcTestMaybe'n'Either =
6889
testCase "Kind check Maybe and Either." $

‎lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,9 @@ module Test.Utils.CompilerInput (
66
compilerInput'either,
77
compilerInput'undefinedForeignTyRef,
88
compilerInput'recDef,
9+
compilerInput'newTypeEither,
10+
compilerInput'newTypeEither',
11+
compilerInput'newTypeEither'',
912
) where
1013

1114
import LambdaBuffers.Compiler.ProtoCompat qualified as P
@@ -14,6 +17,9 @@ import Test.Utils.Module (
1417
module'either,
1518
module'incoherent,
1619
module'maybe,
20+
module'newTypeEither,
21+
module'newTypeEither',
22+
module'newTypeEither'',
1723
module'recDef,
1824
module'undefinedForeignTyRef,
1925
module'undefinedLocalTyRef,
@@ -28,6 +34,15 @@ compilerInput'maybe = _CompilerInput [module'maybe]
2834
compilerInput'either :: P.CompilerInput
2935
compilerInput'either = _CompilerInput [module'either]
3036

37+
compilerInput'newTypeEither :: P.CompilerInput
38+
compilerInput'newTypeEither = _CompilerInput [module'newTypeEither]
39+
40+
compilerInput'newTypeEither' :: P.CompilerInput
41+
compilerInput'newTypeEither' = _CompilerInput [module'newTypeEither']
42+
43+
compilerInput'newTypeEither'' :: P.CompilerInput
44+
compilerInput'newTypeEither'' = _CompilerInput [module'newTypeEither'']
45+
3146
-- | Compiler Input containing 1 module with 1 definition - Either.
3247
compilerInput'recDef :: P.CompilerInput
3348
compilerInput'recDef = _CompilerInput [module'recDef]

‎lambda-buffers-compiler/test/Test/Utils/Constructors.hs‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,8 @@ module Test.Utils.Constructors (
2323
_LocalRef',
2424
_ForeignRef',
2525
_TyApp,
26+
_Opaque,
27+
_TyAbs',
2628
) where
2729

2830
import Control.Lens ((^.))
@@ -99,6 +101,9 @@ _TupleI x =
99101
, PC.sourceInfo = def
100102
}
101103

104+
_Opaque :: PC.TyBody
105+
_Opaque = PC.OpaqueI def
106+
102107
_Constructor :: Text -> PC.Product -> PC.Constructor
103108
_Constructor c f =
104109
PC.Constructor
@@ -138,6 +143,14 @@ _TyAbs args body =
138143
, sourceInfo = def
139144
}
140145

146+
_TyAbs' :: [(Text, PC.KindType)] -> PC.TyBody -> PC.TyAbs
147+
_TyAbs' args body =
148+
PC.TyAbs
149+
{ PC.tyArgs = OMap.fromList [(PC.mkInfoLess $ ta ^. #argName, ta) | ta <- _TyArg <$> args]
150+
, PC.tyBody = body
151+
, sourceInfo = def
152+
}
153+
141154
_TyArg :: (Text, PC.KindType) -> PC.TyArg
142155
_TyArg (a, k) =
143156
PC.TyArg

‎lambda-buffers-compiler/test/Test/Utils/Module.hs‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,14 +6,21 @@ module Test.Utils.Module (
66
module'undefinedForeignTyRef,
77
module'either,
88
module'recDef,
9+
module'newTypeEither,
10+
module'newTypeEither',
11+
module'newTypeEither'',
912
) where
1013

1114
import LambdaBuffers.Compiler.ProtoCompat qualified as P
1215
import Test.Utils.Constructors (_Module, _ModuleName)
1316
import Test.Utils.TyDef (
17+
tyDef'Int,
1418
tyDef'either,
19+
tyDef'either'opaque,
1520
tyDef'incoherent,
1621
tyDef'maybe,
22+
tyDef'ntEither,
23+
tyDef'ntEither'saturated,
1724
tyDef'recDef,
1825
tyDef'undefinedForeignTyRef,
1926
tyDef'undefinedLocalTyRef,
@@ -28,6 +35,15 @@ module'maybe = _Module (_ModuleName ["Prelude"]) [tyDef'maybe] mempty mempty
2835
module'either :: P.Module
2936
module'either = _Module (_ModuleName ["Prelude"]) [tyDef'either] mempty mempty
3037

38+
module'newTypeEither :: P.Module
39+
module'newTypeEither = _Module (_ModuleName ["Prelude"]) [tyDef'either, tyDef'ntEither] mempty mempty
40+
41+
module'newTypeEither' :: P.Module
42+
module'newTypeEither' = _Module (_ModuleName ["Prelude"]) [tyDef'either'opaque, tyDef'ntEither] mempty mempty
43+
44+
module'newTypeEither'' :: P.Module
45+
module'newTypeEither'' = _Module (_ModuleName ["Prelude"]) [tyDef'either'opaque, tyDef'Int, tyDef'ntEither'saturated] mempty mempty
46+
3147
module'recDef :: P.Module
3248
module'recDef = _Module (_ModuleName ["Prelude"]) [tyDef'recDef] mempty mempty
3349

‎lambda-buffers-compiler/test/Test/Utils/TyDef.hs‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,10 @@ module Test.Utils.TyDef (
99
tyDef'undefinedForeignTyRef'TyRef,
1010
tyDef'recDef,
1111
tyDef'either,
12+
tyDef'ntEither,
13+
tyDef'either'opaque,
14+
tyDef'Int,
15+
tyDef'ntEither'saturated,
1216
) where
1317

1418
import LambdaBuffers.Compiler.ProtoCompat.Types (Ty (TyVarI))
@@ -17,9 +21,11 @@ import Test.Utils.Constructors (
1721
_ForeignRef',
1822
_LocalRef',
1923
_ModuleName,
24+
_Opaque,
2025
_SourceInfo,
2126
_TupleI,
2227
_TyAbs,
28+
_TyAbs',
2329
_TyApp,
2430
_TyDef,
2531
_TyName,
@@ -41,6 +47,17 @@ tyDef'maybe =
4147
]
4248
)
4349

50+
tyDef'either'opaque :: P.TyDef
51+
tyDef'either'opaque =
52+
_TyDef
53+
(_TyName "Either")
54+
( _TyAbs'
55+
[ ("a", _Type)
56+
, ("b", _Type)
57+
]
58+
_Opaque
59+
)
60+
4461
tyDef'either :: P.TyDef
4562
tyDef'either =
4663
_TyDef
@@ -54,6 +71,41 @@ tyDef'either =
5471
]
5572
)
5673

74+
tyDef'Int :: P.TyDef
75+
tyDef'Int = _TyDef (_TyName "Int") (_TyAbs' mempty _Opaque)
76+
77+
tyDef'ntEither'saturated :: P.TyDef
78+
tyDef'ntEither'saturated =
79+
_TyDef
80+
(_TyName "WrapEither")
81+
( _TyAbs
82+
mempty
83+
[
84+
( "Foo"
85+
, _TupleI
86+
[ _TyApp
87+
( _TyApp
88+
(_TyRefILocal "Either")
89+
(_TyRefILocal "Int")
90+
)
91+
(_TyRefILocal "Int")
92+
]
93+
)
94+
]
95+
)
96+
97+
tyDef'ntEither :: P.TyDef
98+
tyDef'ntEither =
99+
_TyDef
100+
(_TyName "WrapEither")
101+
( _TyAbs
102+
[ ("a", _Type)
103+
, ("b", _Type)
104+
]
105+
[ ("Foo", _TupleI [_TyApp (_TyApp (_TyRefILocal "Either") (_TyVarI "a")) (_TyVarI "b")])
106+
]
107+
)
108+
57109
-- data F a = Rec F (F a)
58110
tyDef'recDef :: P.TyDef
59111
tyDef'recDef =

0 commit comments

Comments
 (0)