Skip to content

Commit 5cc0c59

Browse files
gnumonikgnumonik
committed
merged #26 
2 parents 00bd75b + a51fe83 commit 5cc0c59

File tree

7 files changed

+215
-126
lines changed

7 files changed

+215
-126
lines changed

‎lambda-buffers-common/src/LambdaBuffers/Common/ProtoCompat/Types.hs‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -73,10 +73,16 @@ data ModuleNamePart = ModuleNamePart {name :: Text, sourceInfo :: SourceInfo}
7373
data VarName = VarName {name :: Text, sourceInfo :: SourceInfo}
7474
deriving stock (Show, Eq, Ord, Generic)
7575

76-
data FieldName = FieldName {name :: Text, sourceInfo :: SourceInfo}
76+
data FieldName = FieldName
77+
{ name :: Text
78+
, sourceInfo :: SourceInfo
79+
}
7780
deriving stock (Show, Eq, Ord, Generic)
7881

79-
data ClassName = ClassName {name :: Text, sourceInfo :: SourceInfo}
82+
data ClassName = ClassName
83+
{ name :: Text
84+
, sourceInfo :: SourceInfo
85+
}
8086
deriving stock (Show, Eq, Ord, Generic)
8187

8288
data Kind = Kind

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

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,7 @@ common common-language
6464
PolyKinds
6565
PostfixOperators
6666
RankNTypes
67+
RecordWildCards
6768
RelaxedPolyRec
6869
ScopedTypeVariables
6970
StandaloneDeriving
@@ -83,16 +84,18 @@ library
8384
import: common-language
8485
build-depends:
8586
, base >=4.16
86-
, containers
87+
, containers >=0.6.5.1
8788
, freer-simple >=1.2
88-
, lambda-buffers-common
89+
, lambda-buffers-common >=0.1.0.0
8990
, lambda-buffers-compiler-pb >=0.1.0.0
9091
, lens >=5.2
9192
, prettyprinter >=1.7
9293
, text >=1.2
9394

9495
exposed-modules:
9596
LambdaBuffers.Compiler.KindCheck
97+
LambdaBuffers.Compiler.KindCheck.Atom
98+
LambdaBuffers.Compiler.KindCheck.Context
9699
LambdaBuffers.Compiler.KindCheck.Inference
97100
LambdaBuffers.Compiler.TypeClassCheck
98101

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

Lines changed: 122 additions & 64 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
{-# LANGUAGE DuplicateRecordFields #-}
2+
{-# LANGUAGE OverloadedLabels #-}
3+
{-# LANGUAGE RecordWildCards #-}
14
{-# LANGUAGE TemplateHaskell #-}
25

36
{- | Note: At the moment the Kind Checker disregards multiple Modules for
@@ -6,64 +9,33 @@ simplicity of testing and developing. This will be changed ASAP. :fixme:
69
module LambdaBuffers.Compiler.KindCheck (
710
KindCheckFailure (..),
811
runKindCheck,
9-
TypeDefinition (..),
1012

1113
-- * Testing Utils
1214
kindCheckType,
1315
runKindCheckEff,
1416
) where
1517

1618
import Control.Exception (Exception)
17-
import Control.Lens (folded, makeLenses, to, (&), (.~), (^.), (^..))
18-
import Control.Monad.Freer (Eff, interpret, run)
19+
import Control.Lens ((&), (.~), (^.))
1920
import Control.Monad.Freer.Error (Error, runError, throwError)
2021
import Control.Monad.Freer.TH (makeEffect)
21-
import Data.Text (Text, intercalate, unpack)
22+
import Data.Text (Text, intercalate)
2223
import LambdaBuffers.Compiler.KindCheck.Inference (
2324
Context,
2425
InferErr,
2526
Kind (Type, (:->:)),
26-
Type (Abs, App, Var),
27+
Type (Var),
2728
context,
2829
infer,
2930
)
3031

31-
import Control.Monad (void)
32-
import Data.Traversable (for)
33-
import Proto.Compiler (
34-
Product'NTuple,
35-
Product'Product (Product'Ntuple, Product'Record'),
36-
Product'Record,
37-
Sum,
38-
Ty,
39-
Ty'Ty (Ty'TyApp, Ty'TyRef, Ty'TyVar),
40-
TyApp,
41-
TyBody'TyBody (TyBody'Opaque, TyBody'Sum),
42-
TyDef,
43-
TyRef,
44-
TyRef'TyRef (TyRef'ForeignTyRef, TyRef'LocalTyRef),
45-
)
46-
import Proto.Compiler_Fields as PF (
47-
constrName,
48-
constructors,
49-
fieldTy,
50-
fields,
51-
maybe'product,
52-
maybe'ty,
53-
maybe'tyBody,
54-
maybe'tyRef,
55-
moduleName,
56-
name,
57-
parts,
58-
product,
59-
tyAbs,
60-
tyArgs,
61-
tyBody,
62-
tyFunc,
63-
tyName,
64-
tyVars,
65-
varName,
66-
)
32+
import Control.Monad
33+
import Control.Monad.Freer
34+
import LambdaBuffers.Common.ProtoCompat qualified as P
35+
36+
import Data.Foldable
37+
38+
import Data.Map qualified as M
6739

6840
--------------------------------------------------------------------------------
6941
-- Types
@@ -72,54 +44,139 @@ import Proto.Compiler_Fields as PF (
7244
data KindCheckFailure
7345
= CheckFailure String
7446
| LookupVarFailure Text
75-
| LookupRefFailure TyRef
47+
| LookupRefFailure P.TyRef
7648
| AppWrongArgKind Kind Kind -- Expected Kind got Kind
7749
| AppToManyArgs Int
7850
| InvalidProto Text
7951
| AppNoArgs -- No args
8052
| InvalidType
81-
| InferenceFailed TypeDefinition InferErr
53+
| InferenceFailed P.TyDef InferErr
8254
deriving stock (Show, Eq)
8355

8456
instance Exception KindCheckFailure
8557

86-
{- | Validated Type Definition.
87-
:fixme: Add to compiler.proto
88-
-}
89-
data TypeDefinition = TypeDefinition
90-
{ _td'name :: String
91-
, _td'variables :: [String]
92-
, _td'sop :: Type
93-
}
94-
deriving stock (Show, Eq)
58+
type Err = Error KindCheckFailure
59+
60+
-- | Main interface to the Kind Checker.
61+
data Check a where
62+
KindCheck :: P.CompilerInput -> Check ()
63+
64+
makeEffect ''Check
65+
66+
-- | Interactions that happen at the level of the Global Checker.
67+
data GlobalCheck a where
68+
CreateContext :: P.CompilerInput -> GlobalCheck Context
69+
ValidateModule :: Context -> P.Module -> GlobalCheck ()
9570

96-
makeLenses 'TypeDefinition
71+
makeEffect ''GlobalCheck
72+
73+
-- | Interactions that happen at the level of the
74+
data ModuleCheck a where -- Module
75+
KCTypeDefinition :: Context -> P.TyDef -> ModuleCheck Kind
76+
KCClassInstance :: Context -> P.InstanceClause -> ModuleCheck ()
77+
KCClass :: Context -> P.ClassDef -> ModuleCheck ()
78+
79+
makeEffect ''ModuleCheck
9780

9881
data KindCheck a where
99-
ValidateInput :: [TyDef] -> KindCheck [TypeDefinition]
100-
CreateContext :: [TypeDefinition] -> KindCheck Context
101-
KindCheck :: Context -> TypeDefinition -> KindCheck Kind
82+
KindFromTyDef :: P.TyDef -> KindCheck Type
83+
InferTypeKind :: Context -> Type -> KindCheck Kind
84+
CheckKindConsistency :: P.TyDef -> Context -> Kind -> KindCheck Kind
10285

10386
makeEffect ''KindCheck
10487

105-
type KindCheckFailEff = '[Error KindCheckFailure]
106-
type KindCheckEff = KindCheck ': KindCheckFailEff
88+
type Transform x y = forall effs {a}. Eff (x ': effs) a -> Eff (y ': effs) a
89+
90+
-- Transformation strategies
91+
92+
globalStrategy :: Transform Check GlobalCheck
93+
globalStrategy = reinterpret $ \case
94+
KindCheck ci -> do
95+
ctx <- createContext ci
96+
void $ validateModule ctx `traverse` (ci ^. #modules)
97+
98+
moduleStrategy :: Transform GlobalCheck ModuleCheck
99+
moduleStrategy = reinterpret $ \case
100+
CreateContext ci -> resolveCreateContext ci
101+
ValidateModule cx md -> do
102+
traverse_ (kCTypeDefinition cx) (md ^. #typeDefs)
103+
traverse_ (kCClassInstance cx) (md ^. #instances)
104+
traverse_ (kCClass cx) (md ^. #classDefs)
105+
106+
localStrategy :: Transform ModuleCheck KindCheck
107+
localStrategy = reinterpret $ \case
108+
KCTypeDefinition ctx tydef -> kindFromTyDef tydef >>= inferTypeKind ctx >>= checkKindConsistency tydef ctx
109+
KCClassInstance ctx instClause -> error "FIXME"
110+
KCClass ctx classDef -> error "Fixme"
111+
112+
runKindCheck :: Eff '[KindCheck] a -> Eff '[Err] a
113+
runKindCheck = reinterpret $ \case
114+
KindFromTyDef tydef -> tyDef2Kind tydef
115+
InferTypeKind ctx ty -> either (\_ -> throwError InvalidType) pure $ infer ctx ty
116+
CheckKindConsistency def ctx k -> resolveKindConsistency def ctx k
117+
118+
runCheck :: Eff (Check ': '[]) a -> Either KindCheckFailure a
119+
runCheck = run . runError . runKindCheck . localStrategy . moduleStrategy . globalStrategy
120+
121+
kindCheckType = undefined
122+
runKindCheckEff = undefined
123+
124+
-- Resolvers
125+
126+
resolveKindConsistency tydef ctx k = do
127+
let
128+
undefined
129+
130+
resolveCreateContext :: forall effs. P.CompilerInput -> Eff effs Context
131+
resolveCreateContext ci = mconcat <$> traverse module2Context (ci ^. #modules)
132+
133+
module2Context :: forall effs. P.Module -> Eff effs Context
134+
module2Context m = mconcat <$> traverse (tyDef2Context (flattenModuleName (m ^. #moduleName))) (P.typeDefs m)
135+
where
136+
flattenModuleName :: P.ModuleName -> Text
137+
flattenModuleName mName = intercalate "." $ (\p -> p ^. #name) <$> mName ^. #parts
138+
139+
type ModuleName = Text
140+
141+
tyDef2Context :: forall effs. ModuleName -> P.TyDef -> Eff effs Context
142+
tyDef2Context curModName tyDef = do
143+
let name = show $ curModName <> "." <> (tyDef ^. #tyName . #name) -- name is qualified
144+
let ty = tyAbs2Type (tyDef ^. #tyAbs)
145+
pure $ mempty & context .~ M.singleton name ty
146+
147+
tyAbs2Type :: P.TyAbs -> Kind
148+
tyAbs2Type tyAbs = foldWithArrow $ pKind2Kind . (\x -> x ^. #argKind) <$> (tyAbs ^. #tyArgs)
149+
150+
foldWithArrow :: [Kind] -> Kind
151+
foldWithArrow = \case [] -> Type; (x : xs) -> x :->: foldWithArrow xs
152+
153+
pKind2Kind :: P.Kind -> Kind
154+
pKind2Kind k =
155+
case k ^. #kind of
156+
P.KindRef P.KType -> Type
157+
P.KindArrow l r -> pKind2Kind l :->: pKind2Kind r
158+
_ -> error "Fixme undefined type" -- FIXME what is an undefined type meant to mean?
159+
160+
tyDef2Kind = undefined
107161

108162
--------------------------------------------------------------------------------
109163
-- API
110-
164+
{-
111165
-- | Main Kind Checking function
112-
runKindCheck :: [TyDef] -> Either KindCheckFailure ()
166+
runKindCheck :: P.CompilerInput -> Either KindCheckFailure ()
113167
runKindCheck tDefs = void $ run $ runError $ interpretKindCheck $ kindCheckDefs tDefs
168+
-}
169+
170+
-- runKindCheckEff :: Eff KindCheckEff a -> Either KindCheckFailure a
171+
-- runKindCheckEff = run . runError . interpretKindCheck
114172

115-
runKindCheckEff :: Eff KindCheckEff a -> Either KindCheckFailure a
116-
runKindCheckEff = run . runError . interpretKindCheck
173+
-- kindCheckType = undefined
117174

118175
--------------------------------------------------------------------------------
119176
-- Strategy
120-
177+
{-
121178
-- | Strategy for kind checking.
122-
kindCheckDefs :: [TyDef] -> Eff KindCheckEff ()
179+
kindCheckDefs :: [PTyDef] -> Eff KindCheckEff ()
123180
kindCheckDefs tyDefs = validateInput tyDefs >>= void . kindCheckType
124181
125182
kindCheckType :: [TypeDefinition] -> Eff KindCheckEff [Kind]
@@ -238,3 +295,4 @@ tyRefToType tR = do
238295
Just (TyRef'LocalTyRef t) -> pure $ Var $ t ^. tyName . name . to unpack
239296
Just (TyRef'ForeignTyRef t) -> pure $ Var $ (t ^. moduleName . parts . to (\ps -> unpack $ intercalate "." [p ^. name | p <- ps])) <> "." <> (t ^. tyName . name . to unpack)
240297
Nothing -> throwError $ InvalidProto "TyRef Cannot be empty"
298+
-}

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
module LambdaBuffers.Compiler.KindCheck.Atom where
2+
3+
type Atom = String
4+
type Var = String

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

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
module LambdaBuffers.Compiler.KindCheck.Context where
2+
3+
import Control.Lens hiding (Context)
4+
import Data.Bifunctor
5+
import Data.Map qualified as M
6+
import LambdaBuffers.Compiler.KindCheck.Atom
7+
import LambdaBuffers.Compiler.KindCheck.Kind
8+
import Prettyprinter
9+
10+
data Context = Context
11+
{ _context :: M.Map Atom Kind
12+
, _addContext :: M.Map Atom Kind
13+
}
14+
deriving stock (Show, Eq)
15+
16+
makeLenses ''Context
17+
18+
instance Pretty Context where
19+
pretty c = case M.toList (c ^. addContext) of
20+
[] -> "Γ"
21+
ctx -> "Γ" <+> "∪" <+> braces (setPretty ctx)
22+
where
23+
setPretty :: [(Atom, Kind)] -> Doc ann
24+
setPretty = hsep . punctuate comma . fmap (\(v, t) -> pretty v <> ":" <+> pretty t)
25+
26+
instance Semigroup Context where
27+
(Context a1 b1) <> (Context a2 b2) = Context (a1 <> a2) (b1 <> b2)
28+
29+
instance Monoid Context where
30+
mempty = Context mempty mempty
31+
32+
class IsMap a b c where
33+
toMap :: a -> M.Map b c
34+
fromMap :: M.Map b c -> a
35+
36+
data ContextType = L | G
37+
deriving (Eq, Ord, Show)
38+
39+
-- | Utility to unify the two.
40+
getAllContext :: Context -> M.Map Atom Kind
41+
getAllContext c = c ^. context <> c ^. addContext

0 commit comments

Comments
 (0)