Skip to content

Commit b57f591

Browse files
gnumonikgnumonik
committed
Ported over TypeClass modules which do not depend upon Solve, minor updates to use new P.TyClassRef
1 parent e07d156 commit b57f591

File tree

4 files changed

+289
-0
lines changed

4 files changed

+289
-0
lines changed

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -110,6 +110,9 @@ library
110110
LambdaBuffers.Compiler.NamingCheck
111111
LambdaBuffers.Compiler.ProtoCompat
112112
LambdaBuffers.Compiler.ProtoCompat.Types
113+
LambdaBuffers.Compiler.TypeClass.Pat
114+
LambdaBuffers.Compiler.TypeClass.Pretty
115+
LambdaBuffers.Compiler.TypeClass.Rules
113116
LambdaBuffers.Compiler.TypeClassCheck
114117

115118
hs-source-dirs: src

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

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
{-# LANGUAGE LambdaCase #-}
2+
3+
module LambdaBuffers.Compiler.TypeClass.Pat (
4+
Pat (..),
5+
toProd,
6+
toRec,
7+
toSum,
8+
patList,
9+
matches,
10+
) where
11+
12+
import Data.Text (Text)
13+
14+
{- A simple ADT to represent patterns.
15+
16+
Note that this ADT allows us to represent nonsensical types (i.e. we can "put the wrong pattern in a hole").
17+
This could be ameliorated by using a GADT, which would give us correct-by-construction patterns at the
18+
cost of significantly more complex type signatures.
19+
-}
20+
21+
data Pat
22+
= {- extremely stupid, unfortunately necessary -}
23+
Name Text
24+
| ModuleName [Text] -- also stupid, also necessary -_-
25+
| Opaque
26+
| {- Lists (constructed from Nil and :*) with bare types are used to
27+
encode products (where a list of length n encodes an n-tuple)
28+
Lists with field labels (l := t) are used to encode records and sum types
29+
These representations let us "peer into the structure" of the TyBody, and are
30+
somewhat analogous to the Generics.SOP representation or, in the case of records (or sums
31+
interpreted as variants), to a row-types representation. We can imagine that each record and
32+
sum are backed by an implicit row.
33+
Unfortunately this encoding allows us to generate Pats which do not correspond to
34+
any possible types. For the purposes of instance resolution/code generation this shouldn't matter
35+
so long as the patterns are only generalizations of "real" types. We could ameliorate this problem by
36+
using a GADT for Pat, but this would greatly complicate the constraint solving/deriving
37+
algorithms and require copious use of type families (and possibly singletons).
38+
-}
39+
Nil -- Nil and :* are hacks to write rules for ProdP and SumP. A bare Nil == Unit
40+
| Pat :* Pat -- cons
41+
| Pat := Pat {- field labels or constr names. The LHS should be (Name "Foo")
42+
for schema types, but should be a PatVar for deriving rules and instances -}
43+
| RecP Pat {- where the Pat arg is expected to be (l := t :* rest) or Nil, where rest
44+
is also a pat-list of labeled fields or Nil -}
45+
| ProdP Pat {- Pat arg should be a list of "Bare types" -}
46+
| SumP Pat {- where the Pat arg is expected to be (Constr l t :* rest) or Nil, where
47+
rest is either Nil or a tyList of Constrs -}
48+
| VarP Text {- This isn't a type variable. Although it is used to represent them in certain contexts,
49+
it is also used more generally to refer to any "hole" in a pattern to which another pattern
50+
may be substituted. We could have separate constr for type variables but it doesn't appear to be
51+
necessary at this time. -}
52+
| RefP Pat Pat {- 1st arg should be a ModuleName -}
53+
| AppP Pat Pat {- Pattern for Type applications -}
54+
| {- This last one is a bit special. This represents a complete type declaration.
55+
The first Pat should be instantiated to `Name l` where l is a concrete name.
56+
The second Pat should be instantiated to a Pat-List (using :*/Nil) which only contains Names.
57+
The final Pat should be instantiated to a Pat body.
58+
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
59+
outermost inner sum for constructing types). -}
60+
DecP Pat Pat Pat
61+
deriving stock (Show, Eq, Ord)
62+
63+
infixr 5 :*
64+
65+
{- Utility functions. Turn a list of types into a product/record/sum type.
66+
-}
67+
toProd :: [Pat] -> Pat
68+
toProd = ProdP . foldr (:*) Nil
69+
70+
toRec :: [Pat] -> Pat
71+
toRec = RecP . foldr (:*) Nil
72+
73+
toSum :: [Pat] -> Pat
74+
toSum = SumP . foldr (:*) Nil
75+
76+
{- Converts a pattern that consists of a well formed pattern list
77+
(i.e. patterns formed from :* and Nil) into a list of patterns.
78+
-}
79+
patList :: Pat -> Maybe [Pat]
80+
patList = \case
81+
Nil -> Just []
82+
p1 :* p2 -> (p1 :) <$> patList p2
83+
_ -> Nothing
84+
85+
{- This is used as a predicate to filter instances or Gens which are structurally compatible
86+
with the argument type.
87+
The first argument is the inner Pat from an instance head or Gen.
88+
The second argument is the Pat representation of a type that we want to derive an instance / generate code for.
89+
NOTE: Is not bidirectional! The first Pat has to be more general than the first
90+
(more specifically: The second Pat should be a substitution instance of the first)
91+
-}
92+
matches :: Pat -> Pat -> Bool
93+
matches t1 t2 | t1 == t2 = True -- need the guard
94+
matches (VarP _) _ = True
95+
matches (x :* xs) (x' :* xs') = matches x x' && matches xs xs'
96+
matches (l := t) (l' := t') = matches l l' && matches t t'
97+
matches (ProdP xs) (ProdP xs') = matches xs xs'
98+
matches (RecP xs) (RecP xs') = matches xs xs'
99+
matches (SumP xs) (SumP xs') = matches xs xs'
100+
matches (AppP t1 t2) (AppP t1' t2') = matches t1 t1' && matches t2 t2'
101+
matches (RefP mn t1) (RefP mn' t2) = matches mn mn' && matches t1 t2
102+
matches (DecP t1 t2 t3) (DecP t1' t2' t3') =
103+
matches t1 t1' && matches t2 t2' && matches t3 t3'
104+
matches _ _ = False

‎lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClass/Pretty.hs‎

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
{-# LANGUAGE OverloadedLabels #-}
2+
{-# LANGUAGE OverloadedStrings #-}
3+
-- orphans are the whole point of this module!
4+
{-# OPTIONS_GHC -Wno-orphans #-}
5+
6+
module LambdaBuffers.Compiler.TypeClass.Pretty (
7+
spaced,
8+
pointies,
9+
(<//>),
10+
(<///>),
11+
) where
12+
13+
import Control.Lens ((^.))
14+
import Data.Generics.Labels ()
15+
import LambdaBuffers.Compiler.ProtoCompat qualified as P
16+
import LambdaBuffers.Compiler.TypeClass.Pat (Pat (AppP, DecP, ModuleName, Name, Nil, Opaque, ProdP, RecP, RefP, SumP, VarP, (:*), (:=)), patList)
17+
import LambdaBuffers.Compiler.TypeClass.Rules (
18+
Class (Class),
19+
Constraint (C),
20+
Instance,
21+
Rule ((:<=)),
22+
)
23+
import Prettyprinter (
24+
Doc,
25+
Pretty (pretty),
26+
braces,
27+
encloseSep,
28+
hcat,
29+
line,
30+
list,
31+
nest,
32+
parens,
33+
punctuate,
34+
(<+>),
35+
)
36+
37+
instance Pretty P.TyClassRef where
38+
pretty = \case
39+
P.ForeignCI (P.ForeignClassRef cn mn _) -> pretty mn <> "." <> pretty (cn ^. #name)
40+
P.LocalCI (P.LocalClassRef cn _) -> pretty (cn ^. #name)
41+
42+
instance Pretty P.ModuleName where
43+
pretty (P.ModuleName pts _) = hcat . punctuate "." $ map (\x -> pretty $ x ^. #name) pts
44+
45+
instance Pretty Class where
46+
pretty (Class nm _) = pretty nm
47+
48+
instance Pretty Constraint where
49+
pretty (C cls p) = pretty cls <+> pretty p
50+
51+
instance Pretty Instance where
52+
pretty (c :<= []) = pretty c
53+
pretty (c :<= cs) = pretty c <+> "<=" <+> list (pretty <$> cs)
54+
55+
instance Pretty P.SourcePosition where
56+
pretty (P.SourcePosition col row) = pretty row <> ":" <> pretty col
57+
58+
instance Pretty P.SourceInfo where
59+
pretty (P.SourceInfo fname f t) =
60+
pretty fname <+> pretty f <> "-" <> pretty t
61+
62+
-- pretty should emit valid Haskell for well-formed DecPs
63+
instance Pretty Pat where
64+
pretty = \case
65+
Name t -> pretty t
66+
ModuleName ts -> hcat . punctuate "." . map pretty $ ts
67+
Opaque -> "<OPAQUE>"
68+
RecP ps -> case patList ps of
69+
Nothing -> pretty ps
70+
Just fields -> case traverse prettyField fields of
71+
Just fs -> braces . nest 2 . hcat . punctuate ", " $ fs
72+
Nothing -> pretty ps
73+
ProdP Nil -> ""
74+
ProdP xs -> case patList xs of
75+
Just [f] -> pretty f
76+
Just fs -> parens . hcat . punctuate ", " . map pretty $ fs
77+
_ -> pretty xs
78+
SumP xs -> case patList xs of
79+
Nothing -> pretty xs
80+
Just cs -> case traverse prettyConstr cs of
81+
Nothing -> pretty cs
82+
Just cstrs -> nest 2 . sumFmt $ cstrs
83+
plist@(p1 :* p2) -> case patList plist of
84+
Just pl -> list . map pretty $ pl
85+
Nothing -> pretty p1 <+> ":*" <+> pretty p2
86+
Nil -> "Nil"
87+
RefP mn@(ModuleName _) n@(Name _) -> pretty mn <> "." <> pretty n
88+
RefP Nil (Name n) -> pretty n
89+
RefP p1 p2 -> parens $ "Ref" <+> pretty p1 <+> pretty p2
90+
VarP t -> pretty t
91+
ap@(AppP p1 p2) -> case prettyApp ap of
92+
Just pap -> parens pap
93+
Nothing -> "App" <+> pretty p1 <+> pretty p2
94+
p1 := p2 -> pretty p1 <+> ":=" <+> pretty p2
95+
DecP nm args body -> case nm of
96+
Name n -> case patList args of
97+
Nothing -> "Dec" <+> pretty n <+> pretty args <+> "=" <+> pretty body
98+
Just [] ->
99+
"data"
100+
<+> pretty n
101+
<+> "="
102+
<+> pretty body
103+
Just vars ->
104+
"data"
105+
<+> pretty n
106+
<+> hcat (punctuate " " . map pretty $ vars)
107+
<+> "="
108+
<+> pretty body
109+
_ -> "Dec" <+> pretty nm <+> pretty args <+> "=" <+> pretty body
110+
where
111+
prettyField :: forall a. Pat -> Maybe (Doc a)
112+
prettyField = \case
113+
Name l := t -> Just $ pretty l <+> "::" <+> pretty t
114+
_ -> Nothing
115+
116+
prettyConstr :: forall a. Pat -> Maybe (Doc a)
117+
prettyConstr = \case
118+
Name l := (ProdP Nil) -> Just $ pretty l
119+
Name l := t -> Just $ pretty l <+> pretty t
120+
_ -> Nothing
121+
122+
-- this is kind of annoying to get right, don't think this is it
123+
prettyApp :: forall a. Pat -> Maybe (Doc a)
124+
prettyApp = \case
125+
AppP p1 p2 -> (pretty p1 <+>) <$> prettyApp p2
126+
other -> Just $ pretty other
127+
128+
sumFmt :: [Doc a] -> Doc a
129+
sumFmt = encloseSep "" "" " | "
130+
131+
spaced :: Doc a -> Doc a
132+
spaced d = line <> d <> line
133+
134+
(<//>) :: Doc a -> Doc a -> Doc a
135+
d1 <//> d2 = d1 <> line <> d2
136+
137+
(<///>) :: Doc a -> Doc a -> Doc a
138+
d1 <///> d2 = d1 <> line <> line <> d2
139+
140+
pointies :: Doc a -> Doc a
141+
pointies d = "<<" <> d <> ">>"

‎lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClass/Rules.hs‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
{-# LANGUAGE GADTs #-}
2+
{-# LANGUAGE TypeFamilies #-}
3+
4+
module LambdaBuffers.Compiler.TypeClass.Rules (
5+
Class (..),
6+
Constraint (..),
7+
Rule (..),
8+
type Instance,
9+
mapPat,
10+
) where
11+
12+
import LambdaBuffers.Compiler.ProtoCompat qualified as P
13+
import LambdaBuffers.Compiler.TypeClass.Pat (Pat)
14+
15+
data Class = Class
16+
{ name :: P.TyClassRef
17+
, supers :: [Class]
18+
}
19+
deriving stock (Show, Eq, Ord)
20+
21+
{- A type which represents instances. Can be either a single simple instance or
22+
a complex instance with its instance constraints. We can use the instance constraint
23+
constr (:<=) to write deriving rules using PatVars in the Pat argument.
24+
NOTE: Rule constraints are written backwards, i.e. "purescript-style"
25+
NOTE: All variables to the right of the first :<= must occur to the left of the first :<=
26+
-}
27+
28+
data Constraint = C Class Pat
29+
deriving stock (Show, Eq, Ord)
30+
31+
data Rule where
32+
(:<=) :: Constraint -> [Constraint] -> Rule
33+
deriving stock (Show, Eq, Ord)
34+
infixl 7 :<=
35+
36+
type Instance = Rule
37+
38+
{- Map over the Pats inside of an Rule
39+
-}
40+
mapPat :: (Pat -> Pat) -> Rule -> Rule
41+
mapPat f (C c ty :<= is) = C c (f ty) :<= map (\(C cx p) -> C cx (f p)) is

0 commit comments

Comments
 (0)