update: comments

Author: cstml

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

@@ -111,13 +111,10 @@ library
   exposed-modules:
     LambdaBuffers.Compiler
     LambdaBuffers.Compiler.KindCheck
-    LambdaBuffers.Compiler.KindCheck.Context
     LambdaBuffers.Compiler.KindCheck.Derivation
     LambdaBuffers.Compiler.KindCheck.Inference
-    LambdaBuffers.Compiler.KindCheck.Judgement
     LambdaBuffers.Compiler.KindCheck.Kind
     LambdaBuffers.Compiler.KindCheck.Type
-    LambdaBuffers.Compiler.KindCheck.Variable
     LambdaBuffers.Compiler.NamingCheck
     LambdaBuffers.Compiler.ProtoCompat
     LambdaBuffers.Compiler.ProtoCompat.FromProto

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

@@ -9,7 +9,7 @@ module LambdaBuffers.Compiler.KindCheck (
   foldWithArrowToType,
 ) where
 
-import Control.Lens (view, (&), (.~), (^.))
+import Control.Lens (Getter, to, view, (&), (.~), (^.))
 import Control.Monad (void)
 import Control.Monad.Freer (Eff, Member, Members, interpret, reinterpret, run)
 import Control.Monad.Freer.Error (Error, runError, throwError)
@@ -18,10 +18,11 @@ 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.Context (Context, context)
+
+import LambdaBuffers.Compiler.KindCheck.Derivation (Context, context)
 import LambdaBuffers.Compiler.KindCheck.Inference qualified as I
 import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KType, (:->:)), kind2ProtoKind)
-import LambdaBuffers.Compiler.KindCheck.Variable (Variable (ForeignRef, TyVar))
+import LambdaBuffers.Compiler.KindCheck.Type (Variable (QualifiedTyRef, TyVar))
 import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess, mkInfoLess)
 import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC
 
@@ -126,13 +127,13 @@ runKindCheck = interpret $ \case
     handleErr modName td = \case
       I.InferUnboundTermErr uA -> do
         case uA of
-          ForeignRef fr ->
+          QualifiedTyRef fr ->
             if (fr ^. #moduleName) == modName
               then -- We're looking at the local module.
 
                 throwError
                   . PC.CompKindCheckError
-                  $ PC.UnboundTyRefError td (PC.LocalI $ fr ^. PC.foreignRef2LocalRef) modName
+                  $ PC.UnboundTyRefError td (PC.LocalI $ fr ^. foreignRef2LocalRef) modName
               else -- We're looking at a foreign module.
 
                 throwError
@@ -154,6 +155,16 @@ runKindCheck = interpret $ \case
         throwError $
           PC.InternalError t
 
+    foreignRef2LocalRef :: Getter PC.ForeignRef PC.LocalRef
+    foreignRef2LocalRef =
+      to
+        ( \fr ->
+            PC.LocalRef
+              { tyName = fr ^. #tyName
+              , sourceInfo = fr ^. #sourceInfo
+              }
+        )
+
 --------------------------------------------------------------------------------
 -- Resolvers
 resolveKindConsistency ::
@@ -211,7 +222,7 @@ tyDef2NameAndKind tyDef = do
 
   -- InfoLess name - the SourceInfo doesn't matter therefore it is defaulted.
   let name =
-        ForeignRef
+        QualifiedTyRef
           . view (PC.localRef2ForeignRef curModName)
           $ PC.LocalRef (tyDef ^. #tyName) def
 

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

@@ -1,24 +1,76 @@
 module LambdaBuffers.Compiler.KindCheck.Derivation (
   Derivation (Axiom, Abstraction, Application, Implication),
-  dType,
-  dTopKind,
+  d'type,
+  d'kind,
+  Judgement (Judgement),
+  j'type,
+  j'kind,
+  j'ctx,
+  Context (Context),
+  context,
+  addContext,
+  getAllContext,
 ) where
 
-import Control.Lens (Lens', lens, (&), (.~), (^.))
-import LambdaBuffers.Compiler.KindCheck.Judgement (Judgement, jKind, jType)
+import Control.Lens (Lens', lens, makeLenses, (&), (.~), (^.))
+import Data.Map qualified as M
 import LambdaBuffers.Compiler.KindCheck.Kind (Kind)
-import LambdaBuffers.Compiler.KindCheck.Type (Type)
+import LambdaBuffers.Compiler.KindCheck.Type (Type, Variable)
+import LambdaBuffers.Compiler.ProtoCompat.InfoLess (InfoLess)
+
 import Prettyprinter (
   Doc,
   Pretty (pretty),
+  braces,
+  comma,
   encloseSep,
   hang,
+  hsep,
   lbracket,
   line,
+  punctuate,
   rbracket,
   space,
+  (<+>),
  )
 
+data Context = Context
+  { _context :: M.Map (InfoLess Variable) Kind
+  , _addContext :: M.Map (InfoLess Variable) Kind
+  }
+  deriving stock (Show, Eq)
+
+makeLenses ''Context
+
+instance Pretty Context where
+  pretty c = case M.toList (c ^. addContext) of
+    [] -> "Γ"
+    ctx -> "Γ" <+> "∪" <+> braces (setPretty ctx)
+    where
+      setPretty :: [(InfoLess Variable, Kind)] -> Doc ann
+      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)
+
+instance Monoid Context where
+  mempty = Context mempty mempty
+
+-- | Utility to unify the two.
+getAllContext :: Context -> M.Map (InfoLess Variable) Kind
+getAllContext c = c ^. context <> c ^. addContext
+
+data Judgement = Judgement
+  { _j'ctx :: Context
+  , _j'type :: Type
+  , _j'kind :: Kind
+  }
+  deriving stock (Show, Eq)
+makeLenses ''Judgement
+
+instance Pretty Judgement where
+  pretty j = pretty (j ^. j'ctx) <+> "⊢" <+> pretty (j ^. j'type) <+> ":" <+> pretty (j ^. j'kind)
+
 data Derivation
   = Axiom Judgement
   | Abstraction Judgement Derivation
@@ -36,32 +88,32 @@ instance Pretty Derivation where
       dNest :: forall a b c. (Pretty a, Pretty b) => a -> [b] -> Doc c
       dNest j ds = pretty j <> line <> hang 2 (encloseSep (lbracket <> space) rbracket (space <> "∧" <> space) (pretty <$> ds))
 
-dType :: Lens' Derivation Type
-dType = lens from to
+d'type :: Lens' Derivation Type
+d'type = lens from to
   where
     from = \case
-      Axiom j -> j ^. jType
-      Abstraction j _ -> j ^. jType
-      Application j _ _ -> j ^. jType
-      Implication j _ -> j ^. jType
+      Axiom j -> j ^. j'type
+      Abstraction j _ -> j ^. j'type
+      Application j _ _ -> j ^. j'type
+      Implication j _ -> j ^. j'type
 
     to drv t = case drv of
-      Axiom j -> Axiom $ j & jType .~ t
-      Abstraction j d -> Abstraction (j & jType .~ t) d
-      Application j d1 d2 -> Application (j & jType .~ t) d1 d2
-      Implication j d -> Implication (j & jType .~ t) d
+      Axiom j -> Axiom $ j & j'type .~ t
+      Abstraction j d -> Abstraction (j & j'type .~ t) d
+      Application j d1 d2 -> Application (j & j'type .~ t) d1 d2
+      Implication j d -> Implication (j & j'type .~ t) d
 
-dTopKind :: Lens' Derivation Kind
-dTopKind = lens from to
+d'kind :: Lens' Derivation Kind
+d'kind = lens from to
   where
     from = \case
-      Axiom j -> j ^. jKind
-      Abstraction j _ -> j ^. jKind
-      Application j _ _ -> j ^. jKind
-      Implication j _ -> j ^. jKind
+      Axiom j -> j ^. j'kind
+      Abstraction j _ -> j ^. j'kind
+      Application j _ _ -> j ^. j'kind
+      Implication j _ -> j ^. j'kind
 
     to der t = case der of
-      Axiom j -> Axiom $ j & jKind .~ t
-      Abstraction j d -> Abstraction (j & jKind .~ t) d
-      Application j d1 d2 -> Application (j & jKind .~ t) d1 d2
-      Implication j d -> Abstraction (j & jKind .~ t) d
+      Axiom j -> Axiom $ j & j'kind .~ t
+      Abstraction j d -> Abstraction (j & j'kind .~ t) d
+      Application j d1 d2 -> Application (j & j'kind .~ t) d1 d2
+      Implication j d -> Abstraction (j & j'kind .~ t) d