Merge remote-tracking branch 'origin/main' into compiler/arbitrary-instances

Author: cstml

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

@@ -118,6 +118,9 @@ library
     LambdaBuffers.Compiler.NamingCheck
     LambdaBuffers.Compiler.ProtoCompat
     LambdaBuffers.Compiler.ProtoCompat.Types
+    LambdaBuffers.Compiler.TypeClass.Pat
+    LambdaBuffers.Compiler.TypeClass.Pretty
+    LambdaBuffers.Compiler.TypeClass.Rules
     LambdaBuffers.Compiler.TypeClassCheck
 
   hs-source-dirs:  src

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

@@ -54,10 +54,10 @@ throwNamingError = either (Left . NamingError) return
 
 -- TODO(bladyjoker): Revisit and make part of compiler.proto
 data ProtoError
-  = MultipleInstanceHeads ClassName [Ty] SourceInfo
-  | NoInstanceHead ClassName SourceInfo
-  | NoConstraintArgs ClassName SourceInfo
-  | MultipleConstraintArgs ClassName [Ty] SourceInfo
+  = MultipleInstanceHeads TyClassRef [Ty] SourceInfo
+  | NoInstanceHead TyClassRef SourceInfo
+  | NoConstraintArgs TyClassRef SourceInfo
+  | MultipleConstraintArgs TyClassRef [Ty] SourceInfo
   | NoClassArgs ClassName SourceInfo
   | MultipleClassArgs ClassName SourceInfo
   | NoTyAppArgs SourceInfo
@@ -387,6 +387,41 @@ instance IsMessage P.Product'Record'Field Field where
     Classes, instances, constraints
 -}
 
+instance IsMessage P.TyClassRef'Local LocalClassRef where
+  fromProto lr = do
+    si <- fromProto $ lr ^. P.sourceInfo
+    nm <- fromProto $ lr ^. P.className
+    pure $ LocalClassRef nm si
+
+  toProto (LocalClassRef nm si) =
+    defMessage
+      & P.className .~ toProto nm
+      & P.sourceInfo .~ toProto si
+
+instance IsMessage P.TyClassRef'Foreign ForeignClassRef where
+  fromProto fr = do
+    si <- fromProto $ fr ^. P.sourceInfo
+    mn <- fromProto $ fr ^. P.moduleName
+    tn <- fromProto $ fr ^. P.className
+    pure $ ForeignClassRef tn mn si
+
+  toProto (ForeignClassRef tn mn si) =
+    defMessage
+      & P.className .~ toProto tn
+      & P.moduleName .~ toProto mn
+      & P.sourceInfo .~ toProto si
+
+instance IsMessage P.TyClassRef TyClassRef where
+  fromProto tr = case tr ^. P.maybe'classRef of
+    Nothing -> throwProtoError $ OneOfNotSet "class_ref"
+    Just x -> case x of
+      P.TyClassRef'LocalClassRef lr -> LocalCI <$> fromProto lr
+      P.TyClassRef'ForeignClassRef f -> ForeignCI <$> fromProto f
+
+  toProto = \case
+    LocalCI lr -> defMessage & P.localClassRef .~ toProto lr
+    ForeignCI fr -> defMessage & P.foreignClassRef .~ toProto fr
+
 instance IsMessage P.ClassDef ClassDef where
   fromProto cd = do
     si <- fromProto $ cd ^. P.sourceInfo
@@ -411,7 +446,7 @@ instance IsMessage P.ClassDef ClassDef where
 instance IsMessage P.InstanceClause InstanceClause where
   fromProto ic = do
     si <- fromProto $ ic ^. P.sourceInfo
-    cnm <- fromProto $ ic ^. P.className
+    cnm <- fromProto $ ic ^. P.classRef
     csts <- traverse fromProto $ ic ^. P.constraints
     hds <- ic ^. (P.heads . traversing fromProto)
     hd <- case hds of
@@ -422,15 +457,15 @@ instance IsMessage P.InstanceClause InstanceClause where
 
   toProto (InstanceClause cnm hd csts si) =
     defMessage
-      & P.className .~ toProto cnm
+      & P.classRef .~ toProto cnm
       & P.heads .~ pure (toProto hd)
       & P.constraints .~ (toProto <$> csts)
       & P.sourceInfo .~ toProto si
 
 instance IsMessage P.Constraint Constraint where
   fromProto c = do
     si <- fromProto $ c ^. P.sourceInfo
-    cnm <- fromProto $ c ^. P.className
+    cnm <- fromProto $ c ^. P.classRef
     args <- c ^. (P.arguments . traversing fromProto)
     arg <- case args of
       [] -> throwProtoError $ NoConstraintArgs cnm si
@@ -440,7 +475,7 @@ instance IsMessage P.Constraint Constraint where
 
   toProto (Constraint cnm arg si) =
     defMessage
-      & P.className .~ toProto cnm
+      & P.classRef .~ toProto cnm
       & P.arguments .~ pure (toProto arg)
       & P.sourceInfo .~ toProto si
 
@@ -454,15 +489,17 @@ instance IsMessage P.Module Module where
     tdefs <- traverse fromProto $ m ^. P.typeDefs
     cdefs <- traverse fromProto $ m ^. P.classDefs
     insts <- traverse fromProto $ m ^. P.instances
+    impts <- traverse fromProto $ m ^. P.imports
     si <- fromProto $ m ^. P.sourceInfo
-    pure $ Module mnm tdefs cdefs insts si
+    pure $ Module mnm tdefs cdefs insts impts si
 
-  toProto (Module mnm tdefs cdefs insts si) =
+  toProto (Module mnm tdefs cdefs insts impts si) =
     defMessage
       & P.moduleName .~ toProto mnm
       & P.typeDefs .~ (toProto <$> tdefs)
       & P.classDefs .~ (toProto <$> cdefs)
       & P.instances .~ (toProto <$> insts)
+      & P.imports .~ (toProto <$> impts)
       & P.sourceInfo .~ toProto si
 
 instance IsMessage P.CompilerInput CompilerInput where

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

@@ -16,13 +16,15 @@ module LambdaBuffers.Compiler.ProtoCompat.Types (
   Field (..),
   FieldName (..),
   ForeignRef (..),
+  ForeignClassRef (..),
   InstanceClause (..),
   Kind (..),
   KindRefType (..),
   KindCheckError (..),
   KindType (..),
   LBName (..),
   LocalRef (..),
+  LocalClassRef (..),
   Module (..),
   ModuleName (..),
   ModuleNamePart (..),
@@ -37,6 +39,7 @@ module LambdaBuffers.Compiler.ProtoCompat.Types (
   TyApp (..),
   TyArg (..),
   TyBody (..),
+  TyClassRef (..),
   TyDef (..),
   TyName (..),
   TyRef (..),
@@ -196,6 +199,21 @@ data Product = RecordI Record | TupleI Tuple
   deriving stock (Show, Eq, Ord, Generic)
   deriving (Arbitrary) via GenericArbitrary Product
 
+data ForeignClassRef = ForeignClassRef
+  { className :: ClassName
+  , moduleName :: ModuleName
+  , sourceInfo :: SourceInfo
+  }
+  deriving stock (Show, Eq, Ord, Generic)
+
+data LocalClassRef = LocalClassRef {className :: ClassName, sourceInfo :: SourceInfo}
+  deriving stock (Show, Eq, Ord, Generic)
+
+data TyClassRef
+  = LocalCI LocalClassRef
+  | ForeignCI ForeignClassRef
+  deriving stock (Show, Eq, Ord, Generic)
+
 data ClassDef = ClassDef
   { className :: ClassName
   , classArgs :: TyArg
@@ -207,7 +225,7 @@ data ClassDef = ClassDef
   deriving (Arbitrary) via GenericArbitrary ClassDef
 
 data InstanceClause = InstanceClause
-  { className :: ClassName
+  { classRef :: TyClassRef
   , head :: Ty
   , constraints :: [Constraint]
   , sourceInfo :: SourceInfo
@@ -225,7 +243,7 @@ instance Arbitrary InstanceClause where
           <*> resize n arbitrary
 
 data Constraint = Constraint
-  { className :: ClassName
+  { classRef :: TyClassRef
   , argument :: Ty
   , sourceInfo :: SourceInfo
   }
@@ -237,6 +255,7 @@ data Module = Module
   , typeDefs :: [TyDef]
   , classDefs :: [ClassDef]
   , instances :: [InstanceClause]
+  , imports :: [ModuleName]
   , sourceInfo :: SourceInfo
   }
   deriving stock (Show, Eq, Ord, Generic)

lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClass/Pat.hs

@@ -0,0 +1,104 @@
+{-# LANGUAGE LambdaCase #-}
+
+module LambdaBuffers.Compiler.TypeClass.Pat (
+  Pat (..),
+  toProd,
+  toRec,
+  toSum,
+  patList,
+  matches,
+) where
+
+import Data.Text (Text)
+
+{- A simple ADT to represent patterns.
+
+Note that this ADT allows us to represent nonsensical types (i.e. we can "put the wrong pattern in a hole").
+This could be ameliorated by using a GADT, which would give us correct-by-construction patterns at the
+cost of significantly more complex type signatures.
+-}
+
+data Pat
+  = {- extremely stupid, unfortunately necessary -}
+    Name Text
+  | ModuleName [Text] -- also stupid, also necessary -_-
+  | Opaque
+  | {- Lists (constructed from Nil and :*) with bare types are used to
+       encode products (where a list of length n encodes an n-tuple)
+       Lists with field labels (l := t) are used to encode records and sum types
+       These representations let us "peer into the structure" of the TyBody, and are
+       somewhat analogous to the Generics.SOP representation or, in the case of records (or sums
+       interpreted as variants), to a row-types representation. We can imagine that each record and
+       sum are backed by an implicit row.
+       Unfortunately this encoding allows us to generate Pats which do not correspond to
+       any possible types. For the purposes of instance resolution/code generation this shouldn't matter
+       so long as the patterns are only generalizations of "real" types. We could ameliorate this problem by
+       using a GADT for Pat, but this would greatly complicate the constraint solving/deriving
+       algorithms and require copious use of type families (and possibly singletons).
+    -}
+    Nil -- Nil and :*  are hacks to write rules for ProdP and SumP. A bare Nil == Unit
+  | Pat :* Pat -- cons
+  | Pat := Pat {- field labels or constr names. The LHS should be (Name "Foo")
+                  for schema types, but should be a PatVar for deriving rules and instances -}
+  | RecP Pat {- where the Pat arg is expected to be (l := t :* rest) or Nil, where rest
+                is also a pat-list  of labeled fields or Nil -}
+  | ProdP Pat {- Pat arg should be a list of "Bare types" -}
+  | SumP Pat {- where the Pat arg is expected to be (Constr l t :* rest) or Nil, where
+                rest is either Nil or a tyList of Constrs -}
+  | VarP Text {- This isn't a type variable. Although it is used to represent them in certain contexts,
+                 it is also used more generally to refer to any "hole" in a pattern to which another pattern
+                 may be substituted. We could have separate constr for type variables but it doesn't appear to be
+                 necessary at this time. -}
+  | RefP Pat Pat {- 1st arg should be a ModuleName  -}
+  | AppP Pat Pat {- Pattern for Type applications -}
+  | {- This last one is a bit special. This represents a complete type declaration.
+       The first Pat should be instantiated to `Name l` where l is a concrete name.
+       The second Pat should be instantiated to a Pat-List (using :*/Nil) which only contains Names.
+       The final Pat should be instantiated to a Pat body.
+       In some languages, parts of this may be ignored. E.g. in Rust the type name doesn't matter (we use the constr name of the
+       outermost inner sum for constructing types). -}
+    DecP Pat Pat Pat
+  deriving stock (Show, Eq, Ord)
+
+infixr 5 :*
+
+{- Utility functions. Turn a list of types into a product/record/sum type.
+-}
+toProd :: [Pat] -> Pat
+toProd = ProdP . foldr (:*) Nil
+
+toRec :: [Pat] -> Pat
+toRec = RecP . foldr (:*) Nil
+
+toSum :: [Pat] -> Pat
+toSum = SumP . foldr (:*) Nil
+
+{- Converts a pattern that consists of a well formed pattern list
+   (i.e. patterns formed from :* and Nil) into a list of patterns.
+-}
+patList :: Pat -> Maybe [Pat]
+patList = \case
+  Nil -> Just []
+  p1 :* p2 -> (p1 :) <$> patList p2
+  _ -> Nothing
+
+{- This is used as a predicate to filter instances or Gens which are structurally compatible
+   with the argument type.
+   The first argument is the inner Pat from an instance head or Gen.
+   The second argument is the Pat representation of a type that we want to derive an instance / generate code for.
+   NOTE: Is not bidirectional! The first Pat has to be more general than the first
+         (more specifically: The second Pat should be a substitution instance of the first)
+-}
+matches :: Pat -> Pat -> Bool
+matches t1 t2 | t1 == t2 = True -- need the guard
+matches (VarP _) _ = True
+matches (x :* xs) (x' :* xs') = matches x x' && matches xs xs'
+matches (l := t) (l' := t') = matches l l' && matches t t'
+matches (ProdP xs) (ProdP xs') = matches xs xs'
+matches (RecP xs) (RecP xs') = matches xs xs'
+matches (SumP xs) (SumP xs') = matches xs xs'
+matches (AppP t1 t2) (AppP t1' t2') = matches t1 t1' && matches t2 t2'
+matches (RefP mn t1) (RefP mn' t2) = matches mn mn' && matches t1 t2
+matches (DecP t1 t2 t3) (DecP t1' t2' t3') =
+  matches t1 t1' && matches t2 t2' && matches t3 t3'
+matches _ _ = False