Skip to content

Commit 1d94905

Browse files
cstmlcstml
committed
format
1 parent 380e322 commit 1d94905

File tree

2 files changed

+60
-113
lines changed

2 files changed

+60
-113
lines changed

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

Lines changed: 60 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
22

33
module LambdaBuffers.Compiler.KindCheck (
4-
-- * Kindchecking functions.
4+
-- * Kind checking functions.
55
check,
66
check_,
77

8-
-- * Testing functions
8+
-- * Tested functions
99
foldWithArrowToType,
1010
) where
1111

@@ -64,16 +64,12 @@ data KindCheck a where
6464
makeEffect ''KindCheck
6565

6666
--------------------------------------------------------------------------------
67+
-- Runners
6768

6869
-- | The Check effect runner.
6970
runCheck :: Eff '[Check, Err] a -> Either CompilerErr a
7071
runCheck =
71-
run
72-
. runError
73-
. runKindCheck
74-
. localStrategy
75-
. moduleStrategy
76-
. globalStrategy
72+
run . runError . runKindCheck . localStrategy . moduleStrategy . globalStrategy
7773

7874
{- | Run the check - return the validated context or the failure. The main API
7975
function of the library.
@@ -86,12 +82,14 @@ check_ :: PC.CompilerInput -> Either CompilerErr ()
8682
check_ = void . runCheck . kCheck
8783

8884
--------------------------------------------------------------------------------
85+
-- Transformations
8986

9087
{- | A transformation (in the context of the Kind Checker) is a mapping from one
91-
Effect to another. All effects can fial via the `Err` effect - which is
88+
Effect to another. All effects can fail via the `Err` effect - which is
9289
essentially the Kind Check failure.
9390
-}
94-
type Transform x y = forall effs {a}. Member Err effs => Eff (x ': effs) a -> Eff (y ': effs) a
91+
type Transform x y =
92+
forall effs {a}. Member Err effs => Eff (x ': effs) a -> Eff (y ': effs) a
9593

9694
-- Transformation strategies
9795
globalStrategy :: Transform Check GlobalCheck
@@ -103,25 +101,26 @@ globalStrategy = reinterpret $ \case
103101

104102
moduleStrategy :: Transform GlobalCheck ModuleCheck
105103
moduleStrategy = reinterpret $ \case
106-
CreateContext ci -> resolveCreateContext ci
107-
ValidateModule cx md -> do
104+
CreateContext ci ->
105+
resolveCreateContext ci
106+
ValidateModule cx md ->
108107
traverse_ (kCTypeDefinition (md ^. #moduleName) cx) (md ^. #typeDefs)
109108

110109
localStrategy :: Transform ModuleCheck KindCheck
111110
localStrategy = reinterpret $ \case
112-
KCTypeDefinition mname ctx tydef -> do
113-
desiredK <- getSpecifiedKind mname tydef
114-
k <- inferTypeKind mname tydef ctx desiredK
115-
checkKindConsistency mname tydef ctx k
111+
KCTypeDefinition modName ctx tyDef -> do
112+
desiredK <- getSpecifiedKind modName tyDef
113+
k <- inferTypeKind modName tyDef ctx desiredK
114+
checkKindConsistency modName tyDef ctx k
116115

117116
runKindCheck :: forall effs {a}. Member Err effs => Eff (KindCheck ': effs) a -> Eff effs a
118117
runKindCheck = interpret $ \case
119-
-- TypesFromTyDef modName tydef -> runReader modName (tyDef2Types tydef)
120-
InferTypeKind modName tyDef ctx k -> either (handleErr modName tyDef) pure $ I.infer ctx tyDef k modName
121-
CheckKindConsistency modName tydef ctx k -> runReader modName $ resolveKindConsistency tydef ctx k
122-
GetSpecifiedKind modName tyDef -> do
123-
(_, k) <- runReader modName $ tyDef2NameAndKind tyDef
124-
pure k
118+
InferTypeKind modName tyDef ctx k ->
119+
either (handleErr modName tyDef) pure $ I.infer ctx tyDef k modName
120+
CheckKindConsistency modName tyDef ctx k ->
121+
runReader modName $ resolveKindConsistency tyDef ctx k
122+
GetSpecifiedKind modName tyDef ->
123+
fmap snd $ runReader modName $ tyDef2NameAndKind tyDef
125124
where
126125
handleErr :: forall {b}. PC.ModuleName -> PC.TyDef -> I.InferErr -> Eff effs b
127126
handleErr modName td = \case
@@ -130,17 +129,32 @@ runKindCheck = interpret $ \case
130129
ForeignRef fr ->
131130
if (fr ^. #moduleName) == modName
132131
then -- We're looking at the local module.
133-
throwError . PC.CompKindCheckError $ PC.UnboundTyRefError td (PC.LocalI $ fr ^. PC.foreignRef2LocalRef) modName
132+
133+
throwError
134+
. PC.CompKindCheckError
135+
$ PC.UnboundTyRefError td (PC.LocalI $ fr ^. PC.foreignRef2LocalRef) modName
134136
else -- We're looking at a foreign module.
135-
throwError . PC.CompKindCheckError $ PC.UnboundTyRefError td (PC.ForeignI fr) modName
136-
TyVar tv -> throwError . PC.CompKindCheckError $ PC.UnboundTyVarError td (PC.TyVar tv) modName
137+
138+
throwError
139+
. PC.CompKindCheckError
140+
$ PC.UnboundTyRefError td (PC.ForeignI fr) modName
141+
TyVar tv ->
142+
throwError
143+
. PC.CompKindCheckError
144+
$ PC.UnboundTyVarError td (PC.TyVar tv) modName
137145
I.InferUnifyTermErr (I.Constraint (k1, k2)) ->
138-
throwError . PC.CompKindCheckError $ PC.IncorrectApplicationError td (kind2ProtoKind k1) (kind2ProtoKind k2) modName
146+
throwError
147+
. PC.CompKindCheckError
148+
$ PC.IncorrectApplicationError td (kind2ProtoKind k1) (kind2ProtoKind k2) modName
139149
I.InferRecursiveSubstitutionErr _ ->
140-
throwError . PC.CompKindCheckError $ PC.RecursiveKindError td modName
150+
throwError
151+
. PC.CompKindCheckError
152+
$ PC.RecursiveKindError td modName
141153
I.InferImpossibleErr t ->
142-
throwError . PC.InternalError $ t
154+
throwError $
155+
PC.InternalError t
143156

157+
--------------------------------------------------------------------------------
144158
-- Resolvers
145159
resolveKindConsistency ::
146160
forall effs.
@@ -149,16 +163,16 @@ resolveKindConsistency ::
149163
Context ->
150164
Kind ->
151165
Eff effs Kind
152-
resolveKindConsistency tydef _ctx inferredKind = do
153-
modname <- ask @PC.ModuleName
154-
(_, k) <- tyDef2NameAndKind tydef
155-
guard tydef k inferredKind modname
166+
resolveKindConsistency tyDef _ctx inferredKind = do
167+
(_, k) <- tyDef2NameAndKind tyDef
168+
guard tyDef k inferredKind
156169
pure inferredKind
157170
where
158-
guard :: PC.TyDef -> Kind -> Kind -> PC.ModuleName -> Eff effs ()
159-
guard t i d mn
171+
guard :: PC.TyDef -> Kind -> Kind -> Eff effs ()
172+
guard t i d
160173
| i == d = pure ()
161-
| otherwise =
174+
| otherwise = do
175+
mn <- ask
162176
throwError
163177
. PC.CompKindCheckError
164178
$ PC.InconsistentTypeError t (kind2ProtoKind i) (kind2ProtoKind d) mn
@@ -194,9 +208,15 @@ tyDef2NameAndKind ::
194208
Eff effs (InfoLess Variable, Kind)
195209
tyDef2NameAndKind tyDef = do
196210
curModName <- ask
197-
let tyname = tyDef ^. #tyName
198-
let name = ForeignRef $ view (PC.localRef2ForeignRef curModName) $ PC.LocalRef tyname def
199-
let k = tyAbsLHS2Kind (tyDef ^. #tyAbs)
211+
212+
-- InfoLess name - the SourceInfo doesn't matter therefore it is defaulted.
213+
let name =
214+
ForeignRef
215+
. view (PC.localRef2ForeignRef curModName)
216+
$ PC.LocalRef (tyDef ^. #tyName) def
217+
218+
k = tyAbsLHS2Kind (tyDef ^. #tyAbs)
219+
200220
pure (mkInfoLess name, k)
201221

202222
tyAbsLHS2Kind :: PC.TyAbs -> Kind
@@ -220,13 +240,12 @@ foldWithArrowToType = foldWithArrowToKind KType
220240
foldWithArrowToKind :: Kind -> [Kind] -> Kind
221241
foldWithArrowToKind = foldr (:->:)
222242

223-
-- =============================================================================
243+
--------------------------------------------------------------------------------
224244
-- To Kind Conversion functions
225245

226246
pKind2Kind :: PC.Kind -> Kind
227247
pKind2Kind k =
228248
case k ^. #kind of
229249
PC.KindRef PC.KType -> KType
230250
PC.KindArrow l r -> pKind2Kind l :->: pKind2Kind r
231-
-- NOTE(cstml): What is an undefined Kind type meant to mean?
232-
_ -> error "Fixme undefined type"
251+
PC.KindRef PC.KUnspecified -> KType -- (for now) defaulting unspecified kinds to Type

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

Lines changed: 0 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,6 @@ module Test.KindCheck (test) where
33
import LambdaBuffers.Compiler.KindCheck (
44
check_,
55
foldWithArrowToType,
6-
-- foldWithProduct,
7-
-- foldWithSum,
86
)
97

108
import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, (:->:)))
@@ -66,76 +64,6 @@ testFolds =
6664
[testArrowFold0, testArrowFold1, testArrowFold2, testArrowFold3HK, testArrowFold4HK, testArrowFoldHHK, testFoldWithArrowToTypeTotal]
6765
]
6866

69-
{-
70-
prod = tyProd
71-
unit' = tyUnit
72-
73-
-- | [ ] -> unit
74-
testFoldProd0 :: TestTree
75-
testFoldProd0 =
76-
testCase "Fold with product - 0 type" $
77-
foldWithProduct [] @?= unit'
78-
79-
-- | [ a ] -> prod unit a
80-
testFoldProd1 :: TestTree
81-
testFoldProd1 =
82-
testCase "Fold with product - 1 type" $
83-
foldWithProduct [lVar "a"] @?= prod unit' (lVar "a")
84-
85-
-- | [b ,a] -> prod (prod unit b) a
86-
testFoldProd2 :: TestTree
87-
testFoldProd2 =
88-
testCase "Fold with product - 2 types" $
89-
foldWithProduct [lVar "b", lVar "a"]
90-
@?= prod (prod unit' (lVar "b")) (lVar "a")
91-
92-
-- | [ a, b ,c ] -> prod (prod (prod unit c) b) a
93-
testFoldProd3 :: TestTree
94-
testFoldProd3 =
95-
testCase "Fold with product - 2 types" $
96-
foldWithProduct [lVar "c", lVar "b", lVar "a"]
97-
@?= prod (prod (prod unit' (lVar "c")) (lVar "b")) (lVar "a")
98-
99-
testPProdFoldTotal :: TestTree
100-
testPProdFoldTotal =
101-
testProperty "ProductFold is total" $
102-
forAll arbitrary $
103-
\ts -> foldWithProduct ts === foldWithProduct ts
104-
105-
sum' :: Type -> Type -> Type
106-
sum' = App . App (Var tySum)
107-
108-
void' :: Type
109-
void' = Var tyVoid
110-
111-
-- | [ ] -> void
112-
testSumFold0 :: TestTree
113-
testSumFold0 =
114-
testCase "Fold 0 type" $
115-
foldWithSum [] @?= void'
116-
117-
-- | [ a ] -> sum void a
118-
testSumFold1 :: TestTree
119-
testSumFold1 =
120-
testCase "Fold 1 type" $
121-
foldWithSum [lVar "a"] @?= sum' void' (lVar "a")
122-
123-
-- | [ a , b ] -> sum (sum void a) b
124-
testSumFold2 :: TestTree
125-
testSumFold2 =
126-
testCase "Fold 2 type" $
127-
foldWithSum [lVar "b", lVar "a"]
128-
@?= sum' (sum' void' (lVar "b")) (lVar "a")
129-
130-
-- | [ a , b , c ] -> a | ( b | c )
131-
testSumFold3 :: TestTree
132-
testSumFold3 =
133-
testCase "Fold 3 types" $
134-
foldWithSum [lVar "c", lVar "b", lVar "a"]
135-
@?= sum' (sum' (sum' void' (lVar "c")) (lVar "b")) (lVar "a")
136-
137-
-}
138-
13967
ty :: Kind
14068
ty = KType
14169

0 commit comments

Comments
 (0)