update: some minor refactoring

Author: cstml

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

@@ -9,7 +9,8 @@ module LambdaBuffers.Compiler.KindCheck (
   foldWithArrowToType,
 ) where
 
-import Control.Lens (Getter, to, view, (&), (.~), (^.))
+import Control.Lens (view, (&), (.~), (^.))
+import Control.Lens.Iso (withIso)
 import Control.Monad (void)
 import Control.Monad.Freer (Eff, Member, Members, interpret, reinterpret, run)
 import Control.Monad.Freer.Error (Error, runError, throwError)
@@ -18,11 +19,16 @@ import Control.Monad.Freer.TH (makeEffect)
 import Data.Default (Default (def))
 import Data.Foldable (Foldable (toList), traverse_)
 import Data.Map qualified as M
-
-import LambdaBuffers.Compiler.KindCheck.Derivation (Context, context)
+import LambdaBuffers.Compiler.KindCheck.Derivation (Context, constraintContext, context)
+import LambdaBuffers.Compiler.KindCheck.Inference (protoKind2Kind)
 import LambdaBuffers.Compiler.KindCheck.Inference qualified as I
-import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, (:->:)), kind2ProtoKind)
-import LambdaBuffers.Compiler.KindCheck.Type (Variable (QualifiedTyRef, TyVar))
+import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KConstraint, KType, KVar, (:->:)))
+import LambdaBuffers.Compiler.KindCheck.Type (
+  Variable (QualifiedConstraint, QualifiedTyRef, TyVar),
+  ftrISOqtr,
+  ltrISOqtr,
+  qTyRef'moduleName,
+ )
 import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, mkInfoLess)
 import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC
 
@@ -50,18 +56,20 @@ makeEffect ''GlobalCheck
 -- | Interactions that happen at the level of the
 data ModuleCheck a where -- Module
   KCTypeDefinition :: PC.ModuleName -> Context -> PC.TyDef -> ModuleCheck Kind
+  KCClassInstance :: PC.ModuleName -> Context -> PC.ClassDef -> ModuleCheck ()
 
--- NOTE(cstml & gnumonik): Lets reach consensus on these - Note(1).
---  KCClassInstance :: Context -> P.InstanceClause -> ModuleCheck ()
 --  KCClass :: Context -> P.ClassDef -> ModuleCheck ()
 
 makeEffect ''ModuleCheck
 
 data KindCheck a where
   GetSpecifiedKind :: PC.ModuleName -> PC.TyDef -> KindCheck Kind
   InferTypeKind :: PC.ModuleName -> PC.TyDef -> Context -> Kind -> KindCheck Kind
+  CheckClassDefinition :: PC.ModuleName -> PC.ClassDef -> Context -> KindCheck ()
   CheckKindConsistency :: PC.ModuleName -> PC.TyDef -> Context -> Kind -> KindCheck Kind
 
+--  CheckClassInstance :: PC.ModuleName -> KindCheck Kind
+
 makeEffect ''KindCheck
 
 --------------------------------------------------------------------------------
@@ -113,57 +121,48 @@ localStrategy = reinterpret $ \case
     desiredK <- getSpecifiedKind modName tyDef
     k <- inferTypeKind modName tyDef ctx desiredK
     checkKindConsistency modName tyDef ctx k
+  KCClassInstance modName ctx classDef -> do
+    _ <- checkClassDefinition modName classDef ctx
+    pure ()
 
 runKindCheck :: forall effs {a}. Member Err effs => Eff (KindCheck ': effs) a -> Eff effs a
 runKindCheck = interpret $ \case
-  InferTypeKind modName tyDef ctx k ->
-    either (handleErr modName tyDef) pure $ I.infer ctx tyDef k modName
+  InferTypeKind modName tyDef ctx _k ->
+    either (handleErr modName tyDef) pure $ I.infer ctx tyDef modName
   CheckKindConsistency modName tyDef ctx k ->
     runReader modName $ resolveKindConsistency tyDef ctx k
   GetSpecifiedKind modName tyDef ->
     fmap snd $ runReader modName $ tyDef2NameAndKind tyDef
+  CheckClassDefinition modName classDef ctx ->
+    either (handleErr2 modName classDef) pure $ I.runClassDefCheck ctx modName classDef
   where
+    handleErr2 = undefined
+
     handleErr :: forall {b}. PC.ModuleName -> PC.TyDef -> I.InferErr -> Eff effs b
     handleErr modName td = \case
-      I.InferUnboundTermErr uA -> do
-        case uA of
-          QualifiedTyRef fr ->
-            if (fr ^. #moduleName) == modName
-              then -- We're looking at the local module.
-
-                throwError
-                  . PC.CompKindCheckError
-                  $ PC.UnboundTyRefError td (PC.LocalI $ fr ^. foreignRef2LocalRef) modName
-              else -- We're looking at a foreign module.
-
-                throwError
-                  . PC.CompKindCheckError
-                  $ PC.UnboundTyRefError td (PC.ForeignI fr) modName
+      I.InferUnboundTermErr ut ->
+        case ut of
+          QualifiedTyRef qtr -> do
+            if qtr ^. qTyRef'moduleName == modName
+              then do
+                -- We're looking at the local module.
+                let localRef = PC.LocalI . fst . withIso ltrISOqtr (\_ f -> f) $ qtr
+                let err = PC.UnboundTyRefError td localRef modName
+                throwError . PC.CompKindCheckError $ err
+              else do
+                -- We're looking at a foreign module.
+                let foreignRef = PC.ForeignI . withIso ftrISOqtr (\_ f -> f) $ qtr
+                throwError . PC.CompKindCheckError $ PC.UnboundTyRefError td foreignRef modName
           TyVar tv ->
-            throwError
-              . PC.CompKindCheckError
-              $ PC.UnboundTyVarError td (PC.TyVar tv) modName
-      I.InferUnifyTermErr (I.Constraint (k1, k2)) ->
-        throwError
-          . PC.CompKindCheckError
-          $ PC.IncorrectApplicationError td (kind2ProtoKind k1) (kind2ProtoKind k2) modName
+            throwError . PC.CompKindCheckError $ PC.UnboundTyVarError td (PC.TyVar tv) modName
+          QualifiedConstraint _ -> error "NOTE(cstml): FIXME."
+      I.InferUnifyTermErr (I.Constraint (k1, k2)) -> do
+        err <- PC.IncorrectApplicationError td <$> kind2ProtoKind k1 <*> kind2ProtoKind k2 <*> pure modName
+        throwError $ PC.CompKindCheckError err
       I.InferRecursiveSubstitutionErr _ ->
-        throwError
-          . PC.CompKindCheckError
-          $ PC.RecursiveKindError td modName
+        throwError . PC.CompKindCheckError $ PC.RecursiveKindError td modName
       I.InferImpossibleErr t ->
-        throwError $
-          PC.InternalError t
-
-    foreignRef2LocalRef :: Getter PC.ForeignRef PC.LocalRef
-    foreignRef2LocalRef =
-      to
-        ( \fr ->
-            PC.LocalRef
-              { tyName = fr ^. #tyName
-              , sourceInfo = fr ^. #sourceInfo
-              }
-        )
+        throwError $ PC.InternalError t
 
 --------------------------------------------------------------------------------
 -- Resolvers
@@ -183,24 +182,28 @@ resolveKindConsistency tyDef _ctx inferredKind = do
     guard t i d
       | i == d = pure ()
       | otherwise = do
-          mn <- ask
-          throwError
-            . PC.CompKindCheckError
-            $ PC.InconsistentTypeError t (kind2ProtoKind i) (kind2ProtoKind d) mn
+          err <- PC.InconsistentTypeError t <$> kind2ProtoKind i <*> kind2ProtoKind d <*> ask
+          throwError $ PC.CompKindCheckError err
 
 --------------------------------------------------------------------------------
 -- Context Creation
 
 -- | Resolver function for the context creation. There is a guarantee from ProtoCompat that the input is sanitised.
 resolveCreateContext :: forall effs. PC.CompilerInput -> Eff effs Context
-resolveCreateContext ci =
-  mconcat <$> traverse module2Context (toList $ ci ^. #modules)
+resolveCreateContext = fmap mconcat . traverse module2Context . toList . view #modules
 
 module2Context :: forall effs. PC.Module -> Eff effs Context
 module2Context m = do
   let typeDefinitions = toList $ m ^. #typeDefs
-  ctxs <- runReader (m ^. #moduleName) $ traverse tyDef2Context typeDefinitions
-  pure $ mconcat ctxs
+  let classDefinitions = toList $ m ^. #classDefs
+  -- Context built from type definitions.
+  typeDefCtx <- fmap mconcat . runReader (m ^. #moduleName) $ traverse tyDef2Context typeDefinitions
+  -- Context built from class definitions.
+  classDefCtx <- fmap mconcat . runReader (m ^. #moduleName) $ traverse classDef2Context classDefinitions
+  return $ typeDefCtx <> classDefCtx
+
+--------------------------------------------------------------------------------
+-- Type Definition Based Context Building.
 
 -- | Creates a Context entry from one type definition.
 tyDef2Context ::
@@ -219,19 +222,45 @@ tyDef2NameAndKind ::
   Eff effs (InfoLess Variable, Kind)
 tyDef2NameAndKind tyDef = do
   curModName <- ask
-
-  -- InfoLess name - the SourceInfo doesn't matter therefore it is defaulted.
+  -- InfoLess Qualified name - the SourceInfo doesn't matter therefore it is defaulted.
   let name =
         QualifiedTyRef
-          . view (PC.localRef2ForeignRef curModName)
+          . withIso ltrISOqtr const
+          . (,curModName)
           $ PC.LocalRef (tyDef ^. #tyName) def
 
       k = tyAbsLHS2Kind (tyDef ^. #tyAbs)
 
   pure (mkInfoLess name, k)
 
 tyAbsLHS2Kind :: PC.TyAbs -> Kind
-tyAbsLHS2Kind tyAbs = foldWithArrowToType $ pKind2Kind . (\x -> x ^. #argKind) <$> toList (tyAbs ^. #tyArgs)
+tyAbsLHS2Kind tyAbs = foldWithArrowToType $ tyArg2Kind <$> toList (tyAbs ^. #tyArgs)
+
+tyArg2Kind :: PC.TyArg -> Kind
+tyArg2Kind = protoKind2Kind . view #argKind
+
+--------------------------------------------------------------------------------
+-- Class Definition Based Context Building.
+
+--- | Convert from internal Kind to Proto Kind.
+kind2ProtoKind :: forall effs. Member Err effs => Kind -> Eff effs PC.Kind
+kind2ProtoKind = \case
+  k1 :->: k2 -> fmap PC.Kind $ PC.KindArrow <$> kind2ProtoKind k1 <*> kind2ProtoKind k2
+  KType -> pure . PC.Kind . PC.KindRef $ PC.KType
+  KVar _ -> pure . PC.Kind . PC.KindRef $ PC.KUnspecified -- this shouldn't happen.
+  KConstraint -> pure . PC.Kind . PC.KindRef $ PC.KConstraint
+
+--------------------------------------------------------------------------------
+-- Class Definition Based Context Building.
+
+classDef2Context :: forall effs. PC.ClassDef -> Eff effs Context
+classDef2Context cDef = do
+  let className = mkInfoLess . view #className $ cDef
+  let classArg = tyArg2Kind . view #classArgs $ cDef
+  pure $ mempty & constraintContext .~ M.singleton className classArg
+
+--------------------------------------------------------------------------------
+-- utilities
 
 {- | Folds kinds and appends them to a Kind result type. In essence creates a
  curried function with a Type final kind.
@@ -250,13 +279,3 @@ foldWithArrowToType = foldWithArrowToKind KType
 
 foldWithArrowToKind :: Kind -> [Kind] -> Kind
 foldWithArrowToKind = foldr (:->:)
-
---------------------------------------------------------------------------------
--- To Kind Conversion functions
-
-pKind2Kind :: PC.Kind -> Kind
-pKind2Kind k =
-  case k ^. #kind of
-    PC.KindRef PC.KType -> KType
-    PC.KindArrow l r -> pKind2Kind l :->: pKind2Kind r
-    PC.KindRef PC.KUnspecified -> KType -- (for now) defaulting unspecified kinds to Type

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

@@ -1,5 +1,6 @@
 module LambdaBuffers.Compiler.KindCheck.Derivation (
   Derivation (Axiom, Abstraction, Application, Implication),
+  QClassName (QClassName),
   d'type,
   d'kind,
   Judgement (Judgement),
@@ -10,12 +11,15 @@ module LambdaBuffers.Compiler.KindCheck.Derivation (
   context,
   addContext,
   getAllContext,
+  constraintContext,
 ) where
 
 import Control.Lens (Lens', lens, makeLenses, (&), (.~), (^.))
+import Control.Lens.Operators ((%~))
 import Data.Map qualified as M
 import LambdaBuffers.Compiler.KindCheck.Kind (Kind)
 import LambdaBuffers.Compiler.KindCheck.Type (Type, Variable)
+import LambdaBuffers.Compiler.ProtoCompat qualified as PC
 import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess)
 import Prettyprinter (
   Doc,
@@ -33,9 +37,13 @@ import Prettyprinter (
   (<+>),
  )
 
+-- | Qualified Class Name.
+data QClassName = QClassName
+
 data Context = Context
   { _context :: M.Map (InfoLess Variable) Kind
   , _addContext :: M.Map (InfoLess Variable) Kind
+  , _constraintContext :: M.Map (InfoLess PC.ClassName) Kind
   }
   deriving stock (Show, Eq)
 
@@ -50,12 +58,16 @@ instance Pretty Context where
       setPretty = hsep . punctuate comma . fmap (\(v, t) -> pretty v <> ":" <+> pretty t)
 
 instance Semigroup Context where
-  (Context a1 b1) <> (Context a2 b2) = Context (a1 <> a2) (b1 <> b2)
+  c1 <> c2 =
+    c1
+      & context %~ (<> c2 ^. context)
+      & addContext %~ (<> c2 ^. addContext)
+      & constraintContext %~ (<> c2 ^. constraintContext)
 
 instance Monoid Context where
-  mempty = Context mempty mempty
+  mempty = Context mempty mempty mempty
 
--- | Utility to unify the two.
+-- | Utility to unify the two T.
 getAllContext :: Context -> M.Map (InfoLess Variable) Kind
 getAllContext c = c ^. context <> c ^. addContext