11{-# LANGUAGE LambdaCase #-}
22
3- module LambdaBuffers.Compiler.TypeClass.Pat (
4- Pat (.. ),
5- toProd ,
6- toRec ,
7- toSum ,
8- patList ,
9- matches ,
10- ) where
3+ module LambdaBuffers.Compiler.TypeClass.Pat where
114
5+ import Data.Kind (Type )
126import Data.Text (Text )
137
148{- A simple ADT to represent patterns.
@@ -18,15 +12,15 @@ This could be ameliorated by using a GADT, which would give us correct-by-constr
1812cost of significantly more complex type signatures.
1913-}
2014
21- data Pat
22- = {- Name / ModuleName / Opaque / TyVarP are literal patterns (or ground terms)
23- because hey cannot contain any VarPs and therefore "have no holes".
24- Every TyDef or subcomponent thereof will be translated into a composite
25- pattern "without any holes". (Nil is also a literal/ground term, I guess) -}
26- Name Text
15+ data Literal
16+ = Name Text
2717 | ModuleName [Text ]
2818 | Opaque
29- | TyVarP Text
19+ | TyVar Text
20+ deriving stock (Show , Eq , Ord )
21+
22+ data Pat
23+ = LitP Literal
3024 | {- Lists (constructed from Nil and :*) with bare types are used to
3125 encode products (where a list of length n encodes an n-tuple)
3226 Lists with field labels (l := t) are used to encode records and sum types
@@ -40,10 +34,10 @@ data Pat
4034 using a GADT for Pat, but this would greatly complicate the constraint solving/deriving
4135 algorithms and require copious use of type families (and possibly singletons).
4236 -}
43- Nil -- Nil and :* are hacks to write rules for ProdP and SumP. A bare Nil == Unit
44- | Pat :* Pat -- cons
45- | Pat := Pat {- field labels or constr names. The LHS should be (Name "Foo")
46- for schema types, but should be a PatVar for deriving rules and instances -}
37+ NilP -- Nil and :* are hacks to write rules for ProdP and SumP. A bare Nil == Unit
38+ | ConsP Pat Pat -- cons
39+ | LabelP Pat Pat {- field labels or constr names. The LHS should be (Name "Foo")
40+ for schema types, but should be a PatVar for deriving rules and instances -}
4741 | RecP Pat {- where the Pat arg is expected to be (l := t :* rest) or Nil, where rest
4842 is also a pat-list of labeled fields or Nil -}
4943 | ProdP Pat {- Pat arg should be a list of "Bare types" -}
@@ -62,26 +56,83 @@ data Pat
6256 DecP Pat Pat Pat
6357 deriving stock (Show , Eq , Ord )
6458
65- infixr 5 :*
59+ -- infixr 5 :*
6660
6761{- Utility functions. Turn a list of types into a product/record/sum type.
6862-}
69- toProd :: [Pat ] -> Pat
70- toProd = ProdP . foldr (:*) Nil
63+ toProdP :: [Pat ] -> Pat
64+ toProdP = ProdP . foldr ConsP NilP
7165
72- toRec :: [Pat ] -> Pat
73- toRec = RecP . foldr (:*) Nil
66+ toRecP :: [Pat ] -> Pat
67+ toRecP = RecP . foldr ConsP NilP
7468
75- toSum :: [Pat ] -> Pat
76- toSum = SumP . foldr (:*) Nil
69+ toSumP :: [Pat ] -> Pat
70+ toSumP = SumP . foldr ConsP NilP
7771
7872{- Converts a pattern that consists of a well formed pattern list
7973 (i.e. patterns formed from :* and Nil) into a list of patterns.
8074-}
8175patList :: Pat -> Maybe Pat ]
8276patList = \ case
83- Nil -> Just []
84- p1 :* p2 -> (p1 : ) <$> patList p2
77+ NilP -> Just []
78+ p1 `ConsP ` p2 -> (p1 : ) <$> patList p2
79+ _ -> Nothing
80+
81+ data Exp
82+ = LitE Literal
83+ | NilE
84+ | ConsE Exp Exp
85+ | LabelE Exp Exp
86+ | RecE Exp
87+ | ProdE Exp
88+ | SumE Exp
89+ | -- NO EXPRESSION VARS! EXPRESSIONS DON'T HAVE HOLES!
90+ RefE Exp Exp {- 1st arg should be a ModuleName -}
91+ | AppE Exp Exp {- Pattern for Type applications -}
92+ | DecE Exp Exp Exp
93+ deriving stock (Show , Eq , Ord )
94+
95+ class ExpressionLike (p :: Type ) where
96+ (*:) :: p -> p -> p
97+
98+ nil :: p
99+
100+ (*=) :: p -> p -> p
101+
102+ infixr 5 *:
103+
104+ instance ExpressionLike Pat where
105+ p1 *: p2 = p1 `ConsP ` p2
106+
107+ nil = NilP
108+
109+ p1 *= p2 = LabelP p1 p2
110+
111+ instance ExpressionLike Exp where
112+ p1 *: p2 = p1 `ConsE ` p2
113+
114+ nil = NilE
115+
116+ p1 *= p2 = LabelE p1 p2
117+
118+ {- Utility functions. Turn a list of types into a product/record/sum type.
119+ -}
120+ toProdE :: [Exp ] -> Exp
121+ toProdE = ProdE . foldr ConsE NilE
122+
123+ toRecE :: [Exp ] -> Exp
124+ toRecE = RecE . foldr ConsE NilE
125+
126+ toSumE :: [Exp ] -> Exp
127+ toSumE = SumE . foldr ConsE NilE
128+
129+ {- Converts a pattern that consists of a well formed pattern list
130+ (i.e. patterns formed from :* and Nil) into a list of patterns.
131+ -}
132+ expList :: Exp -> Maybe Exp ]
133+ expList = \ case
134+ NilE -> Just []
135+ p1 `ConsE ` p2 -> (p1 : ) <$> expList p2
85136 _ -> Nothing
86137
87138{- This is used as a predicate to filter instances or Gens which are structurally compatible
@@ -91,16 +142,17 @@ patList = \case
91142 NOTE: Is not bidirectional! The first Pat has to be more general than the first
92143 (more specifically: The second Pat should be a substitution instance of the first)
93144-}
94- matches :: Pat -> Pat -> Bool
95- matches t1 t2 | t1 == t2 = True -- need the guard
145+ matches :: Pat -> Exp -> Bool
146+ matches ( LitP l1) ( LitE l2) = l1 == l2
96147matches (VarP _) _ = True
97- matches (x :* xs) (x' :* xs') = matches x x' && matches xs xs'
98- matches (l := t) (l' := t') = matches l l' && matches t t'
99- matches (ProdP xs) (ProdP xs') = matches xs xs'
100- matches (RecP xs) (RecP xs') = matches xs xs'
101- matches (SumP xs) (SumP xs') = matches xs xs'
102- matches (AppP t1 t2) (AppP t1' t2') = matches t1 t1' && matches t2 t2'
103- matches (RefP mn t1) (RefP mn' t2) = matches mn mn' && matches t1 t2
104- matches (DecP t1 t2 t3) (DecP t1' t2' t3') =
148+ matches (x ` ConsP ` xs) (x' ` ConsE ` xs') = matches x x' && matches xs xs'
149+ matches (LabelP l t) (LabelE l' t') = matches l l' && matches t t'
150+ matches (ProdP xs) (ProdE xs') = matches xs xs'
151+ matches (RecP xs) (RecE xs') = matches xs xs'
152+ matches (SumP xs) (SumE xs') = matches xs xs'
153+ matches (AppP t1 t2) (AppE t1' t2') = matches t1 t1' && matches t2 t2'
154+ matches (RefP mn t1) (RefE mn' t2) = matches mn mn' && matches t1 t2
155+ matches (DecP t1 t2 t3) (DecE t1' t2' t3') =
105156 matches t1 t1' && matches t2 t2' && matches t3 t3'
157+ matches NilP NilE = True
106158matches _ _ = False
0 commit comments