Skip to content

Commit 2b83a78

Browse files
authored
Generics: Derive sum type instances with a balanced binary tree of Eithers
Add test case from GitHub Discussion 414
1 parent e4361d9 commit 2b83a78

10 files changed

+280
-92
lines changed

src/comp/CSyntaxUtil.hs

+23-17
Original file line numberDiff line numberDiff line change
@@ -17,10 +17,12 @@ tMkTuple pos (t:ts) = tMkPair pos t (tMkTuple pos ts)
1717
tMkPair :: Position -> Type -> Type -> Type
1818
tMkPair pos t1 t2 = TAp (TAp (cTCon (setIdPosition pos idPrimPair)) t1) t2
1919

20-
tMkEitherChain :: Position -> [CType] -> Type
21-
tMkEitherChain pos [] = error "Either with no options"
22-
tMkEitherChain pos [t] = t
23-
tMkEitherChain pos (t:ts) = tMkEither pos t (tMkEitherChain pos ts)
20+
tMkEitherTree :: Position -> [CType] -> Type
21+
tMkEitherTree pos [] = error "Either with no options"
22+
tMkEitherTree pos [t] = t
23+
tMkEitherTree pos ts =
24+
tMkEither pos (tMkEitherTree pos $ take index ts) (tMkEitherTree pos $ drop index ts)
25+
where index = (length ts + 1) `div` 2
2426

2527
tMkEither :: Position -> Type -> Type -> Type
2628
tMkEither pos t1 t2 = TAp (TAp (cTCon (setIdPosition pos idEither)) t1) t2
@@ -39,19 +41,23 @@ pMkTuple pos [] = CPstruct (Just True) (setIdPosition pos idPrimUnit) []
3941
pMkTuple pos [p] = p
4042
pMkTuple pos (p:ps) = CPCon (setIdPosition pos idComma) [p, pMkTuple pos ps]
4143

42-
mkEitherChain :: Position -> Int -> Int -> CExpr -> CExpr
43-
mkEitherChain pos 0 1 e = e
44-
mkEitherChain pos 0 _ e = CCon idLeft [e]
45-
mkEitherChain pos i n e
46-
| i < n = CCon idRight [mkEitherChain pos (i - 1) (n - 1) e]
47-
| otherwise = error $ "Index " ++ show i ++ " out of range for Either chain of size " ++ show n
48-
49-
pMkEitherChain :: Position -> Int -> Int -> CPat -> CPat
50-
pMkEitherChain pos 0 1 e = e
51-
pMkEitherChain pos 0 _ e = CPCon idLeft [e]
52-
pMkEitherChain pos i n e
53-
| i < n = CPCon idRight [pMkEitherChain pos (i - 1) (n - 1) e]
54-
| otherwise = error $ "Index " ++ show i ++ " out of range for Either chain of size " ++ show n
44+
mkEitherTree :: Position -> Int -> Int -> CExpr -> CExpr
45+
mkEitherTree pos 0 1 e = e
46+
mkEitherTree pos i n e
47+
| i < leftSize = CCon idLeft [mkEitherTree pos i leftSize e]
48+
| i < n = CCon idRight [mkEitherTree pos (i - leftSize) rightSize e]
49+
| otherwise = error $ "Index " ++ show i ++ " out of range for Either tree of size " ++ show n
50+
where leftSize = (n + 1) `div` 2
51+
rightSize = n `div` 2
52+
53+
pMkEitherTree :: Position -> Int -> Int -> CPat -> CPat
54+
pMkEitherTree pos 0 1 e = e
55+
pMkEitherTree pos i n e
56+
| i < leftSize = CPCon idLeft [pMkEitherTree pos i leftSize e]
57+
| i < n = CPCon idRight [pMkEitherTree pos (i - leftSize) rightSize e]
58+
| otherwise = error $ "Index " ++ show i ++ " out of range for Either tree of size " ++ show n
59+
where leftSize = (n + 1) `div` 2
60+
rightSize = n `div` 2
5561

5662
mkMaybe :: (Maybe CExpr) -> CExpr
5763
mkMaybe Nothing = CCon idInvalid []

src/comp/Deriving.hs

+3-3
Original file line numberDiff line numberDiff line change
@@ -769,7 +769,7 @@ mkGenericInstance r packageid dpos i vs isData summands =
769769
_ -> cTCon idConArg
770770
| v <- vs],
771771
cTNum (toInteger $ length summands) dpos],
772-
tMkEitherChain dpos
772+
tMkEitherTree dpos
773773
[cTApplys (cTCon idMeta)
774774
[cTApplys (cTCon $ case mfns of
775775
Just _ -> idMetaConsNamed
@@ -792,7 +792,7 @@ mkGenericInstance r packageid dpos i vs isData summands =
792792
then CPCon1 i cn (CPVar id_x)
793793
else CPVar id_x] [] $
794794
CCon idMeta
795-
[mkEitherChain dpos k (length summands) $
795+
[mkEitherTree dpos k (length summands) $
796796
CCon idMeta
797797
[mkTuple dpos
798798
[CCon idMeta
@@ -809,7 +809,7 @@ mkGenericInstance r packageid dpos i vs isData summands =
809809
to = CLValue idToNQ
810810
[CClause
811811
[CPCon idMeta
812-
[pMkEitherChain dpos k (length summands) $
812+
[pMkEitherTree dpos k (length summands) $
813813
CPCon idMeta
814814
[pMkTuple dpos
815815
[CPCon idMeta
+206
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,206 @@
1+
// Copyright(c) 2016. Atomic Rules LLC. All rights reserved.
2+
3+
////////////////////////////////////////////////////////////////////////////////
4+
/// IPv4 Header and support types
5+
/// Ed Czeck
6+
/// May 2015
7+
/// for Atomic Rules LLC
8+
////////////////////////////////////////////////////////////////////////////////
9+
10+
11+
////////////////////////////////////////////////////////////////////////////////
12+
/// IP Protocol values
13+
////////////////////////////////////////////////////////////////////////////////
14+
typedef enum {
15+
HOPOPT = 0
16+
,ICMP = 1
17+
,IGMP = 2
18+
,GGP = 3
19+
,IPv4 = 4
20+
,ST = 5
21+
,TCP = 6
22+
,CBT = 7
23+
,EGP = 8
24+
,IGP = 9
25+
,BBN_RCC_MON = 10
26+
,NVP_II = 11
27+
,PUP = 12
28+
,ARGUS = 13
29+
,EMCON = 14
30+
,XNET = 15
31+
,CHAOS = 16
32+
,UDP = 17
33+
,MUX = 18
34+
,DCN_MEAS = 19
35+
,HMP = 20
36+
,PRM = 21
37+
,XNS_IDP = 22
38+
,TRUNK_1 = 23
39+
,TRUNK_2 = 24
40+
,LEAF_1 = 25
41+
,LEAF_2 = 26
42+
,RDP = 27
43+
,IRTP = 28
44+
,ISO_TP4 = 29
45+
,NETBLT = 30
46+
,MFE_NSP = 31
47+
,MERIT_INP = 32
48+
,DCCP = 33
49+
,PC_3 = 34
50+
,IDPR = 35
51+
,XTP = 36
52+
,DDP = 37
53+
,IDPR_CMTP = 38
54+
,TPplusplus = 39
55+
,IL = 40
56+
,IPv6 = 41
57+
,SDRP = 42
58+
,IPv6_Route = 43
59+
,IPv6_Frag = 44
60+
,IDRP = 45
61+
,RSVP = 46
62+
,GRE = 47
63+
,DSR = 48
64+
,BNA = 49
65+
,ESP = 50
66+
,AH = 51
67+
,I_NLSP = 52
68+
,SWIPE = 53
69+
,NARP = 54
70+
,MOBILE = 55
71+
,TLSP = 56
72+
,SKIP = 57
73+
,IPv6_ICMP = 58
74+
,IPv6_NoNxt = 59
75+
,IPv6_Opts = 60
76+
,UA61 = 61
77+
,CFTP = 62
78+
,UA63 = 63
79+
,SAT_EXPAK = 64
80+
,KRYPTOLAN = 65
81+
,RVD = 66
82+
,IPPC = 67
83+
,UA68 = 68
84+
,SAT_MON = 69
85+
,VISA = 70
86+
,IPCV = 71
87+
,CPNX = 72
88+
,CPHB = 73
89+
,WSN = 74
90+
,PVP = 75
91+
,BR_SAT_MON = 76
92+
,SUN_ND = 77
93+
,WB_MON = 78
94+
,WB_EXPAK = 79
95+
,ISO_IP = 80
96+
,VMTP = 81
97+
,SECURE_VMTP = 82
98+
,VINES = 83
99+
,TTP_IPTM = 84
100+
,NSFNET_IGP = 85
101+
,DGP = 86
102+
,TCF = 87
103+
,EIGRP = 88
104+
,OSPFIGP = 89
105+
,Sprite_RPC = 90
106+
,LARP = 91
107+
,MTP = 92
108+
,AX_25 = 93
109+
,IPIP = 94
110+
,MICP = 95
111+
,SCC_SP = 96
112+
,ETHERIP = 97
113+
,ENCAP = 98
114+
,UA99 = 99
115+
,GMTP = 100
116+
,IFMP = 101
117+
,PNNI = 102
118+
,PIM = 103
119+
,ARIS = 104
120+
,SCPS = 105
121+
,QNX = 106
122+
,A_N = 107
123+
,IPComp = 108
124+
,SNP = 109
125+
,Compaq_Peer = 110
126+
,IPX_in_IP = 111
127+
,VRRP = 112
128+
,PGM = 113
129+
,XX114 = 114
130+
,L2TP = 115
131+
,DDX = 116
132+
,IATP = 117
133+
,STP = 118
134+
,SRP = 119
135+
,UTI = 120
136+
,SMP = 121
137+
,SM = 122
138+
,PTP = 123
139+
,ISIS = 124
140+
,FIRE = 125
141+
,CRTP = 126
142+
,CRUDP = 127
143+
,SSCOPMCE = 128
144+
,IPLT = 129
145+
,SPS = 130
146+
,PIPE = 131
147+
,SCTP = 132
148+
,FC = 133
149+
,RSVP_E2E_IGNORE = 134
150+
,Mobility_Header = 135
151+
,UDPLite = 136
152+
,MPLS_in_IP = 137
153+
,Manet = 138
154+
,HIP = 139
155+
,Shi = 140
156+
,WESP = 141
157+
,ROHC = 142
158+
// Unassigned
159+
,UA143 = 143 ,UA144 = 144 ,UA145 = 145 ,UA146 = 146
160+
,UA147 = 147 ,UA148 = 148 ,UA149 = 149 ,UA150 = 150
161+
,UA151 = 151 ,UA152 = 152 ,UA153 = 153 ,UA154 = 154
162+
,UA155 = 155 ,UA156 = 156 ,UA157 = 157 ,UA158 = 158
163+
,UA159 = 159 ,UA160 = 160 ,UA161 = 161 ,UA162 = 162
164+
,UA163 = 163 ,UA164 = 164 ,UA165 = 165 ,UA166 = 166
165+
,UA167 = 167 ,UA168 = 168 ,UA169 = 169 ,UA170 = 170
166+
,UA171 = 171 ,UA172 = 172 ,UA173 = 173 ,UA174 = 174
167+
,UA175 = 175 ,UA176 = 176 ,UA177 = 177 ,UA178 = 178
168+
,UA179 = 179 ,UA180 = 180 ,UA181 = 181 ,UA182 = 182
169+
,UA183 = 183 ,UA184 = 184 ,UA185 = 185 ,UA186 = 186
170+
,UA187 = 187 ,UA188 = 188 ,UA189 = 189 ,UA190 = 190
171+
,UA191 = 191 ,UA192 = 192 ,UA193 = 193 ,UA194 = 194
172+
,UA195 = 195 ,UA196 = 196 ,UA197 = 197 ,UA198 = 198
173+
,UA199 = 199 ,UA200 = 200 ,UA201 = 201 ,UA202 = 202
174+
,UA203 = 203 ,UA204 = 204 ,UA205 = 205 ,UA206 = 206
175+
,UA207 = 207 ,UA208 = 208 ,UA209 = 209 ,UA210 = 210
176+
,UA211 = 211 ,UA212 = 212 ,UA213 = 213 ,UA214 = 214
177+
,UA215 = 215 ,UA216 = 216 ,UA217 = 217 ,UA218 = 218
178+
,UA219 = 219 ,UA220 = 220 ,UA221 = 221 ,UA222 = 222
179+
,UA223 = 223 ,UA224 = 224 ,UA225 = 225 ,UA226 = 226
180+
,UA227 = 227 ,UA228 = 228 ,UA229 = 229 ,UA230 = 230
181+
,UA231 = 231 ,UA232 = 232 ,UA233 = 233 ,UA234 = 234
182+
,UA235 = 235 ,UA236 = 236 ,UA237 = 237 ,UA238 = 238
183+
,UA239 = 239 ,UA240 = 240 ,UA241 = 241 ,UA242 = 242
184+
,UA243 = 243 ,UA244 = 244 ,UA245 = 245 ,UA246 = 246
185+
,UA247 = 247 ,UA248 = 248 ,UA249 = 249 ,UA250 = 250
186+
,UA251 = 251 ,UA252 = 252 ,UA253 = 253 ,UA254 = 254
187+
,Reserved = 255
188+
} IPProtocol deriving (Bits, Eq);
189+
190+
// We derive our own version of FShow here to speed compiles.
191+
// bsc does not like decoding big enums
192+
instance FShow#(IPProtocol);
193+
function Fmt fshow (IPProtocol p);
194+
UInt#(8) px = unpack(pack(p));
195+
return
196+
case (p)
197+
ICMP : return $format("ICMP");
198+
IGMP : return $format("IGMP");
199+
UDP : return $format("UDP");
200+
TCP : return $format("TCP");
201+
default : return $format ("P%0d", px);
202+
endcase;
203+
endfunction
204+
endinstance
205+
206+
+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
# for "make clean" to work everywhere
2+
3+
CONFDIR = $(realpath ../../..)
4+
5+
include $(CONFDIR)/clean.mk
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
2+
# GitHub Issue #334
3+
4+
compile_pass IPv4.bsv

testsuite/bsc.typechecker/generics/CustomBits.bs

+13-47
Original file line numberDiff line numberDiff line change
@@ -18,53 +18,20 @@ instance (Generic a r, MyBits' r n) => MyBits a n where
1818
mypack x = mypack' $ from x
1919
myunpack bs = to $ myunpack' bs
2020

21-
class incoherent MyBits' r n | r -> n where
21+
class MyBits' r n | r -> n where
2222
mypack' :: r -> Bit n
2323
myunpack' :: Bit n -> r
2424

25-
-- Compute the number of tag bits required for the number of
26-
-- constructors at the top-level MetaData instance
27-
instance (Log ncons ntag, ConBits 0 r ndata, Add ntag ndata n) =>
28-
MyBits' (Meta (MetaData name pkg ta ncons) r) n where
29-
mypack' (Meta x) =
30-
let (tagNum, dat) = packCon x
31-
tag = pack ((fromInteger tagNum) :: UInt ntag)
32-
in tag ++ dat
25+
-- Instance for sum types
26+
instance (MyBits' r1 n1, MyBits' r2 n2, Max n1 n2 c, Add 1 c n, Add p1 n1 c, Add p2 n2 c) =>
27+
MyBits' (Either r1 r2) n where
28+
mypack' (Left x) = 1'b0 ++ extend (mypack' x)
29+
mypack' (Right x) = 1'b1 ++ extend (mypack' x)
3330
myunpack' bs =
34-
let (tag, dat) = split bs
35-
in Meta $ unpackCon (unpack (tag :: Bit ntag)) dat
36-
37-
-- ConBits type class is used for sum types and has extra parameters:
38-
-- i is the index of the first constructor, computed bottom-up from the metadata.
39-
-- Note that we can't compute i top down (moving i to the other side of the
40-
-- fundep arrow), as this would require an Add context on the Either instance
41-
-- that could not be used in determining what instance matches in the next level
42-
-- of recursion.
43-
class ConBits i r n | r -> i n where
44-
packCon :: r -> (Integer, Bit n)
45-
unpackCon :: UInt m -> Bit n -> r
46-
47-
-- Instance for sum types determines the constructor requiring the largest number
48-
-- of bits and adds padding as needed.
49-
instance (ConBits i1 a1 n1, ConBits i2 a2 n2, Max n1 n2 n, Add p1 n1 n, Add p2 n2 n) =>
50-
ConBits i1 (Either a1 a2) n where
51-
packCon (Left x) =
52-
let (tag, bs) = packCon x
53-
in (tag, extend bs)
54-
packCon (Right x) =
55-
let (tag, bs) = packCon x
56-
in (tag, extend bs)
57-
unpackCon i bs when i == fromInteger (valueOf i1) =
58-
Left $ unpackCon i (truncate bs)
59-
unpackCon i bs = Right $ unpackCon i (truncate bs)
60-
61-
instance (MyBits' r n) => ConBits idx (Meta (MetaConsNamed name idx nfields) r) n where
62-
packCon (Meta x) = (valueOf idx, mypack' x)
63-
unpackCon _ bs = Meta $ myunpack' bs
64-
65-
instance (MyBits' r n) => ConBits idx (Meta (MetaConsAnon name idx nfields) r) n where
66-
packCon (Meta x) = (valueOf idx, mypack' x)
67-
unpackCon _ bs = Meta $ myunpack' bs
31+
let (tag, content) = (split bs) :: (Bit 1, Bit c)
32+
in case tag of
33+
0 -> Left $ myunpack' $ truncate content
34+
1 -> Right $ myunpack' $ truncate content
6835

6936
-- Instance for product types
7037
instance (MyBits' r1 n1, MyBits' r2 n2, Add n1 n2 n) => MyBits' (r1, r2) n where
@@ -76,10 +43,9 @@ instance MyBits' () 0 where
7643
mypack' () = 0'b0
7744
myunpack' _ = ()
7845

79-
instance (MyBits' a m, Bits (Vector n (Bit m)) l) =>
80-
MyBits' (Meta (MetaData name pkg ta 1) (Vector n a)) l where
81-
mypack' (Meta v) = pack $ map mypack' v
82-
myunpack' = Meta `compose` map myunpack' `compose` unpack
46+
instance (MyBits' a m, Bits (Vector n (Bit m)) l) => MyBits' (Vector n a) l where
47+
mypack' v = pack $ map mypack' v
48+
myunpack' = map myunpack' `compose` unpack
8349

8450
-- Ignore other types of metadata
8551
instance (MyBits' r n) => MyBits' (Meta m r) n where

testsuite/bsc.typechecker/generics/GenericNegativeTests.bs.bsc-out.expected

+5-5
Original file line numberDiff line numberDiff line change
@@ -12,13 +12,13 @@ Error: "GenericNegativeTests.bs", line 26, column 10: (T0020)
1212
GenericNegativeTests.TypeEq
1313
(Prelude.Meta (Prelude.MetaData "Foo" "GenericNegativeTests" () 3)
1414
(Prelude.Either
15-
(Prelude.Meta (Prelude.MetaConsAnon "A" 0 2)
16-
(Prelude.Meta (Prelude.MetaField "_1" 0) (Prelude.Conc (Prelude.UInt 8)),
17-
Prelude.Meta (Prelude.MetaField "_2" 1) (Prelude.Conc Prelude.Bool)))
1815
(Prelude.Either
16+
(Prelude.Meta (Prelude.MetaConsAnon "A" 0 2)
17+
(Prelude.Meta (Prelude.MetaField "_1" 0) (Prelude.Conc (Prelude.UInt 8)),
18+
Prelude.Meta (Prelude.MetaField "_2" 1) (Prelude.Conc Prelude.Bool)))
1919
(Prelude.Meta (Prelude.MetaConsAnon "B" 1 1)
20-
(Prelude.Meta (Prelude.MetaField "_1" 0) (Prelude.Conc (Prelude.UInt 16))))
21-
(Prelude.Meta (Prelude.MetaConsAnon "C" 2 0) ()))))
20+
(Prelude.Meta (Prelude.MetaField "_1" 0) (Prelude.Conc (Prelude.UInt 16)))))
21+
(Prelude.Meta (Prelude.MetaConsAnon "C" 2 0) ())))
2222
(Prelude.Meta (Prelude.MetaData "Foo" "GenericTests" () 4)
2323
(Prelude.Either
2424
(Prelude.Meta (Prelude.MetaConsAnon "A" 0 3)

0 commit comments

Comments
 (0)