Skip to content

Commit 01a001d

Browse files
cstmlcstml
committed
update: modify .proto to add modules and change to tydef
1 parent bc86243 commit 01a001d

File tree

5 files changed

+87
-70
lines changed

5 files changed

+87
-70
lines changed

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

Lines changed: 38 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ makeEffect ''GlobalCheck
6969

7070
-- | Interactions that happen at the level of the
7171
data ModuleCheck a where -- Module
72-
KCTypeDefinition :: ModName -> Context -> PC.TyDef -> ModuleCheck Kind
72+
KCTypeDefinition :: PC.ModuleName -> Context -> PC.TyDef -> ModuleCheck Kind
7373

7474
-- NOTE(cstml & gnumonik): Lets reach consensus on these - Note(1).
7575
-- KCClassInstance :: Context -> P.InstanceClause -> ModuleCheck ()
@@ -78,9 +78,9 @@ data ModuleCheck a where -- Module
7878
makeEffect ''ModuleCheck
7979

8080
data KindCheck a where
81-
TypesFromTyDef :: ModName -> PC.TyDef -> KindCheck [Type]
82-
InferTypeKind :: ModName -> PC.TyDef -> Context -> Type -> KindCheck Kind
83-
CheckKindConsistency :: ModName -> PC.TyDef -> Context -> Kind -> KindCheck Kind
81+
TypesFromTyDef :: PC.ModuleName -> PC.TyDef -> KindCheck [Type]
82+
InferTypeKind :: PC.ModuleName -> PC.TyDef -> Context -> Type -> KindCheck Kind
83+
CheckKindConsistency :: PC.ModuleName -> PC.TyDef -> Context -> Kind -> KindCheck Kind
8484

8585
makeEffect ''KindCheck
8686

@@ -120,7 +120,7 @@ moduleStrategy :: Transform GlobalCheck ModuleCheck
120120
moduleStrategy = reinterpret $ \case
121121
CreateContext ci -> evalState (mempty @(M.Map Variable PC.TyDef)) . resolveCreateContext $ ci
122122
ValidateModule cx md -> do
123-
traverse_ (kCTypeDefinition (module2ModuleName md) cx) (md ^. #typeDefs)
123+
traverse_ (kCTypeDefinition (module2ModName md) cx) (md ^. #typeDefs)
124124

125125
localStrategy :: Transform ModuleCheck KindCheck
126126
localStrategy = reinterpret $ \case
@@ -141,30 +141,30 @@ localStrategy = reinterpret $ \case
141141
-- | Internal to External term association map ~ a mapping between a Variable and the term it originated from. Allows us to throw meaningful errors.
142142
type IETermMap = M.Map Variable (Either PC.TyVar PC.TyRef)
143143

144-
type HandleErrorEnv a = Eff '[Reader ModName, Writer IETermMap] a
144+
type HandleErrorEnv a = Eff '[Reader PC.ModuleName, Writer IETermMap] a
145145

146146
runKindCheck :: forall effs {a}. Member Err effs => Eff (KindCheck ': effs) a -> Eff effs a
147147
runKindCheck = interpret $ \case
148148
TypesFromTyDef modName tydef -> runReader modName (tyDef2Types tydef)
149149
InferTypeKind modName tyDef ctx ty -> either (handleErr modName tyDef) pure $ infer ctx ty
150150
CheckKindConsistency modName def ctx k -> runReader modName $ resolveKindConsistency def ctx k
151151
where
152-
handleErr :: forall {b}. ModName -> PC.TyDef -> InferErr -> Eff effs b
152+
handleErr :: forall {b}. PC.ModuleName -> PC.TyDef -> InferErr -> Eff effs b
153153
handleErr modName td = \case
154154
InferUnboundTermErr uA -> do
155155
tt <- getTermType modName td uA
156156
throwError . PC.CompKindCheckError $ case tt of
157-
Right r -> PC.UnboundTyRefError td r
158-
Left l -> PC.UnboundTyVarError td l
157+
Right r -> PC.UnboundTyRefError td r modName
158+
Left l -> PC.UnboundTyVarError td l modName
159159
InferUnifyTermErr (I.Constraint (k1, k2)) ->
160-
throwError . PC.CompKindCheckError $ PC.IncorrectApplicationError (tyDef2TyName td) (kind2ProtoKind k1) (kind2ProtoKind k2)
160+
throwError . PC.CompKindCheckError $ PC.IncorrectApplicationError td (kind2ProtoKind k1) (kind2ProtoKind k2) modName
161161
InferRecursiveSubstitutionErr _ ->
162-
throwError . PC.CompKindCheckError $ PC.RecursiveKindError $ tyDef2TyName td
162+
throwError . PC.CompKindCheckError $ PC.RecursiveKindError td modName
163163
InferImpossibleErr t ->
164164
throwError . PC.InternalError $ t
165165

166166
-- Gets the original term associated with the Variable.
167-
getTermType :: ModName -> PC.TyDef -> Variable -> Eff effs (Either PC.TyVar PC.TyRef)
167+
getTermType :: PC.ModuleName -> PC.TyDef -> Variable -> Eff effs (Either PC.TyVar PC.TyRef)
168168
getTermType modName td va = do
169169
let termMap = snd . run . runWriter . runReader modName $ tyDef2Map td
170170
case termMap M.!? va of
@@ -229,27 +229,24 @@ runKindCheck = interpret $ \case
229229

230230
resolveKindConsistency ::
231231
forall effs.
232-
Members '[Reader ModName, Err] effs =>
232+
Members '[Reader PC.ModuleName, Err] effs =>
233233
PC.TyDef ->
234234
Context ->
235235
Kind ->
236236
Eff effs Kind
237237
resolveKindConsistency tydef _ctx inferredKind = do
238-
mName <- ask @ModName
239-
let tyName = tyDef2TyName tydef
240-
(_, k) <- tyDef2NameAndKind mName tydef
241-
guard tyName k inferredKind
238+
modname <- ask @PC.ModuleName
239+
(_, k) <- tyDef2NameAndKind (moduleName2ModName modname) tydef
240+
guard tydef k inferredKind modname
242241
pure inferredKind
243242
where
244-
guard :: PC.TyName -> Kind -> Kind -> Eff effs ()
245-
guard n i d
243+
guard :: PC.TyDef -> Kind -> Kind -> PC.ModuleName -> Eff effs ()
244+
guard t i d mn
246245
| i == d = pure ()
247246
| otherwise =
248-
throwError . PC.CompKindCheckError $
249-
PC.InconsistentTypeError n (kind2ProtoKind i) (kind2ProtoKind d)
250-
251-
tyDef2TyName :: PC.TyDef -> PC.TyName
252-
tyDef2TyName (PC.TyDef n _ _) = n
247+
throwError
248+
. PC.CompKindCheckError
249+
$ PC.InconsistentTypeError t (kind2ProtoKind i) (kind2ProtoKind d) mn
253250

254251
--------------------------------------------------------------------------------
255252
-- Context Creation
@@ -379,14 +376,14 @@ tyArg2Var = LocalRef . view (#argName . #name)
379376

380377
constructor2Type ::
381378
forall eff.
382-
Members '[Reader ModName, Err] eff =>
379+
Members '[Reader PC.ModuleName, Err] eff =>
383380
PC.Constructor ->
384381
Eff eff Type
385382
constructor2Type co = product2Type (co ^. #product)
386383

387384
product2Type ::
388385
forall eff.
389-
Members '[Reader ModName, Err] eff =>
386+
Members '[Reader PC.ModuleName, Err] eff =>
390387
PC.Product ->
391388
Eff eff Type
392389
product2Type = \case
@@ -395,14 +392,14 @@ product2Type = \case
395392

396393
record2Type ::
397394
forall eff.
398-
Members '[Reader ModName, Err] eff =>
395+
Members '[Reader PC.ModuleName, Err] eff =>
399396
PC.Record ->
400397
Eff eff Type
401398
record2Type r = foldWithProduct <$> traverse field2Type (toList $ r ^. #fields)
402399

403400
tuple2Type ::
404401
forall eff.
405-
Members '[Reader ModName, Err] eff =>
402+
Members '[Reader PC.ModuleName, Err] eff =>
406403
PC.Tuple ->
407404
Eff eff Type
408405
tuple2Type tu = do
@@ -411,14 +408,14 @@ tuple2Type tu = do
411408

412409
field2Type ::
413410
forall eff.
414-
Members '[Reader ModName, Err] eff =>
411+
Members '[Reader PC.ModuleName, Err] eff =>
415412
PC.Field ->
416413
Eff eff Type
417414
field2Type f = ty2Type (f ^. #fieldTy)
418415

419416
ty2Type ::
420417
forall eff.
421-
Members '[Reader ModName, Err] eff =>
418+
Members '[Reader PC.ModuleName, Err] eff =>
422419
PC.Ty ->
423420
Eff eff Type
424421
ty2Type = \case
@@ -437,7 +434,7 @@ tyVar2Variable = LocalRef . view (#varName . #name)
437434

438435
tyApp2Type ::
439436
forall eff.
440-
Members '[Reader ModName, Err] eff =>
437+
Members '[Reader PC.ModuleName, Err] eff =>
441438
PC.TyApp ->
442439
Eff eff Type
443440
tyApp2Type ta = do
@@ -447,14 +444,14 @@ tyApp2Type ta = do
447444

448445
tyRef2Type ::
449446
forall eff.
450-
Members '[Reader ModName, Err] eff =>
447+
Members '[Reader PC.ModuleName, Err] eff =>
451448
PC.TyRef ->
452449
Eff eff Type
453450
tyRef2Type = fmap Var . tyRef2Variable
454451

455452
tyRef2Variable ::
456453
forall eff.
457-
Members '[Reader ModName] eff =>
454+
Members '[Reader PC.ModuleName] eff =>
458455
PC.TyRef ->
459456
Eff eff Variable
460457
tyRef2Variable = \case
@@ -463,16 +460,15 @@ tyRef2Variable = \case
463460

464461
localTyRef2Variable ::
465462
forall eff.
466-
Members '[Reader ModName] eff =>
463+
Members '[Reader PC.ModuleName] eff =>
467464
PC.LocalRef ->
468465
Eff eff Variable
469466
localTyRef2Variable ltr = do
470-
moduleName <- ask
467+
moduleName <- moduleName2ModName <$> ask
471468
pure $ ForeignRef moduleName (ltr ^. #tyName . #name)
472469

473470
foreignTyRef2Variable ::
474471
forall eff.
475-
Members '[Reader ModName] eff =>
476472
PC.ForeignRef ->
477473
Eff eff Variable
478474
foreignTyRef2Variable ftr = do
@@ -488,7 +484,7 @@ foreignTyRef2Variable ftr = do
488484
-}
489485
tyDef2Types ::
490486
forall eff.
491-
Members '[Reader ModName, Err] eff =>
487+
Members '[Reader PC.ModuleName, Err] eff =>
492488
PC.TyDef ->
493489
Eff eff [Type]
494490
tyDef2Types tyde = do
@@ -498,14 +494,14 @@ tyDef2Types tyde = do
498494

499495
tyAbsRHS2Types ::
500496
forall eff.
501-
Members '[Reader ModName, Err] eff =>
497+
Members '[Reader PC.ModuleName, Err] eff =>
502498
PC.TyAbs ->
503499
Eff eff [Type]
504500
tyAbsRHS2Types tyab = tyBody2Types (tyab ^. #tyBody)
505501

506502
tyBody2Types ::
507503
forall eff.
508-
Members '[Reader ModName, Err] eff =>
504+
Members '[Reader PC.ModuleName, Err] eff =>
509505
PC.TyBody ->
510506
Eff eff [Type]
511507
tyBody2Types = \case
@@ -514,7 +510,7 @@ tyBody2Types = \case
514510

515511
sum2Types ::
516512
forall eff.
517-
Members '[Reader ModName, Err] eff =>
513+
Members '[Reader PC.ModuleName, Err] eff =>
518514
PC.Sum ->
519515
Eff eff [Type]
520516
sum2Types su = traverse constructor2Type $ M.elems (su ^. #constructors)
@@ -531,5 +527,5 @@ foldWithProduct = foldl' (App . App (Var tyProd)) (Var tyUnit)
531527
foldWithSum :: [Type] -> Type
532528
foldWithSum = foldl' (App . App (Var tySum)) (Var tyVoid)
533529

534-
module2ModuleName :: PC.Module -> ModName
535-
module2ModuleName = moduleName2ModName . (^. #moduleName)
530+
module2ModName :: PC.Module -> PC.ModuleName
531+
module2ModName = view #moduleName

‎lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs‎

Lines changed: 21 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -670,47 +670,57 @@ instance IsMessage P.KindCheckError PC.KindCheckError where
670670
PC.UnboundTyVarError
671671
<$> fromProto (err ^. P.tyDef)
672672
<*> fromProto (err ^. P.tyVar)
673+
<*> fromProto (err ^. P.moduleName)
673674
P.KindCheckError'UnboundTyRefError' err ->
674675
PC.UnboundTyRefError
675676
<$> fromProto (err ^. P.tyDef)
676677
<*> fromProto (err ^. P.tyRef)
678+
<*> fromProto (err ^. P.moduleName)
677679
P.KindCheckError'ImpossibleUnificationError' err ->
678680
PC.IncorrectApplicationError
679-
<$> fromProto (err ^. P.tyName)
681+
<$> fromProto (err ^. P.tyDef)
680682
<*> fromProto (err ^. P.tyKindLhs)
681683
<*> fromProto (err ^. P.tyKindRhs)
684+
<*> fromProto (err ^. P.moduleName)
682685
P.KindCheckError'RecursiveKindError' err ->
683686
PC.RecursiveKindError
684-
<$> fromProto (err ^. P.tyName)
687+
<$> fromProto (err ^. P.tyDef)
688+
<*> fromProto (err ^. P.moduleName)
685689
P.KindCheckError'InconsistentTypeError' err ->
686690
PC.InconsistentTypeError
687-
<$> fromProto (err ^. P.tyName)
691+
<$> fromProto (err ^. P.tyDef)
688692
<*> fromProto (err ^. P.actualKind)
689693
<*> fromProto (err ^. P.expectedKind)
694+
<*> fromProto (err ^. P.moduleName)
690695
Nothing -> throwOneOfError (messageName (Proxy @P.KindCheckError)) "kind_check_error"
691696

692697
toProto = \case
693-
PC.UnboundTyVarError tydef tyvar ->
698+
PC.UnboundTyVarError tydef tyvar modname ->
694699
defMessage
695700
& (P.unboundTyVarError . P.tyDef) .~ toProto tydef
696701
& (P.unboundTyVarError . P.tyVar) .~ toProto tyvar
697-
PC.UnboundTyRefError tydef tyref ->
702+
& (P.unboundTyVarError . P.moduleName) .~ toProto modname
703+
PC.UnboundTyRefError tydef tyref modname ->
698704
defMessage
699705
& (P.unboundTyRefError . P.tyDef) .~ toProto tydef
700706
& (P.unboundTyRefError . P.tyRef) .~ toProto tyref
701-
PC.IncorrectApplicationError name k1 k2 ->
707+
& (P.unboundTyRefError . P.moduleName) .~ toProto modname
708+
PC.IncorrectApplicationError tydef k1 k2 modname ->
702709
defMessage
703-
& (P.impossibleUnificationError . P.tyName) .~ toProto name
710+
& (P.impossibleUnificationError . P.tyDef) .~ toProto tydef
704711
& (P.impossibleUnificationError . P.tyKindLhs) .~ toProto k1
705712
& (P.impossibleUnificationError . P.tyKindRhs) .~ toProto k2
706-
PC.RecursiveKindError err ->
713+
& (P.impossibleUnificationError . P.moduleName) .~ toProto modname
714+
PC.RecursiveKindError tydef modname ->
707715
defMessage
708-
& (P.recursiveKindError . P.tyName) .~ toProto err
709-
PC.InconsistentTypeError name ki kd ->
716+
& (P.recursiveKindError . P.tyDef) .~ toProto tydef
717+
& (P.recursiveKindError . P.moduleName) .~ toProto modname
718+
PC.InconsistentTypeError tydef ki kd modname ->
710719
defMessage
711-
& (P.inconsistentTypeError . P.tyName) .~ toProto name
720+
& (P.inconsistentTypeError . P.tyDef) .~ toProto tydef
712721
& (P.inconsistentTypeError . P.actualKind) .~ toProto ki
713722
& (P.inconsistentTypeError . P.expectedKind) .~ toProto kd
723+
& (P.inconsistentTypeError . P.moduleName) .~ toProto modname
714724

715725
instance IsMessage P.CompilerError PC.CompilerError where
716726
fromProto _ = throwInternalError "fromProto CompilerError not implemented"

‎lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -316,11 +316,11 @@ instance Arbitrary CompilerInput where
316316
fn n = CompilerInput <$> resize n arbitrary
317317

318318
data KindCheckError
319-
= UnboundTyVarError TyDef TyVar
320-
| UnboundTyRefError TyDef TyRef
321-
| IncorrectApplicationError TyName Kind Kind
322-
| RecursiveKindError TyName
323-
| InconsistentTypeError TyName Kind Kind
319+
= UnboundTyVarError TyDef TyVar ModuleName
320+
| UnboundTyRefError TyDef TyRef ModuleName
321+
| IncorrectApplicationError TyDef Kind Kind ModuleName
322+
| RecursiveKindError TyDef ModuleName
323+
| InconsistentTypeError TyDef Kind Kind ModuleName
324324
deriving stock (Show, Eq, Ord, Generic)
325325
deriving (Arbitrary) via GenericArbitrary KindCheckError
326326
instance Exception KindCheckError

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

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,12 @@
11
module Test.KindCheck.Errors (testGKindCheckErrors) where
22

33
import LambdaBuffers.Compiler.KindCheck (check_)
4-
import LambdaBuffers.Compiler.ProtoCompat.Types (CompilerError (CompKindCheckError), KindCheckError (UnboundTyRefError, UnboundTyVarError))
4+
import LambdaBuffers.Compiler.ProtoCompat qualified as PC
5+
import LambdaBuffers.Compiler.ProtoCompat.Types (CompilerError (CompKindCheckError), KindCheckError (UnboundTyRefError, UnboundTyVarError), Module)
56
import Test.Tasty (TestTree, testGroup)
67
import Test.Tasty.HUnit (testCase, (@?=))
78
import Test.Utils.CompilerInput (compilerInput'undefinedForeignTyRef, compilerInput'undefinedLocalTyRef, compilerInput'undefinedVariable)
9+
import Test.Utils.Constructors (_ModuleName)
810
import Test.Utils.TyDef (tyDef'undefinedForeignTyRef, tyDef'undefinedForeignTyRef'TyRef, tyDef'undefinedLocalTyRef, tyDef'undefinedLocalTyRef'TyRef, tyDef'undefinedVar, tyDef'undefinedVar'var)
911

1012
testGKindCheckErrors :: TestTree
@@ -13,14 +15,20 @@ testGKindCheckErrors = testGroup "Kind Check Error Tests" [undefinedVariable, un
1315
undefinedVariable :: TestTree
1416
undefinedVariable =
1517
testCase "Catch undefined(free) variable in Type Definition." $
16-
check_ compilerInput'undefinedVariable @?= Left (CompKindCheckError $ UnboundTyVarError tyDef'undefinedVar tyDef'undefinedVar'var)
18+
check_ compilerInput'undefinedVariable
19+
@?= (Left . CompKindCheckError . withDefModule) (UnboundTyVarError tyDef'undefinedVar tyDef'undefinedVar'var)
1720

1821
undefinedLocalTyRef :: TestTree
1922
undefinedLocalTyRef =
2023
testCase "Catch undefined Local TyRef in Type Definition." $
21-
check_ compilerInput'undefinedLocalTyRef @?= Left (CompKindCheckError $ UnboundTyRefError tyDef'undefinedLocalTyRef tyDef'undefinedLocalTyRef'TyRef)
24+
check_ compilerInput'undefinedLocalTyRef
25+
@?= (Left . CompKindCheckError . withDefModule) (UnboundTyRefError tyDef'undefinedLocalTyRef tyDef'undefinedLocalTyRef'TyRef)
2226

2327
undefinedForeignTyRef :: TestTree
2428
undefinedForeignTyRef =
2529
testCase "Catch undefined Foreign TyRef in Type Definition." $
26-
check_ compilerInput'undefinedForeignTyRef @?= Left (CompKindCheckError $ UnboundTyRefError tyDef'undefinedForeignTyRef tyDef'undefinedForeignTyRef'TyRef)
30+
check_ compilerInput'undefinedForeignTyRef
31+
@?= (Left . CompKindCheckError . withDefModule) (UnboundTyRefError tyDef'undefinedForeignTyRef tyDef'undefinedForeignTyRef'TyRef)
32+
33+
withDefModule :: forall a. (PC.ModuleName -> a) -> a
34+
withDefModule f = f (_ModuleName ["Module"])

0 commit comments

Comments
 (0)