Ticket #3755: UpdateString.hs

File UpdateString.hs, 6.9 KB (added by simonpj, 4 years ago)

UpdateString? example

Line 
1{-# OPTIONS_GHC -fglasgow-exts    #-}
2{-# LANGUAGE OverlappingInstances #-}
3
4module Test where
5
6-----------------------------------------------------------------------------
7-- Functorial structural representation types.
8-----------------------------------------------------------------------------
9
10-- | Structure type for constant values.
11newtype K a r    = K { unK :: a }
12
13-- | Structure type for recursive values.
14newtype I r      = I { unI :: r }
15
16-- | Structure type for empty constructors.
17data U r         = U
18
19-- | Structure type for alternatives in a type.
20data (f :+: g) r = L (f r) | R (g r)
21
22-- | Structure type for fields of a constructor.
23data (f :*: g) r = f r :*: g r
24
25-- | Structure type to store the name of a constructor.
26data C c f r =  C { unC :: f r }
27
28infixr 6 :+:
29infixr 7 :*:
30
31-- | Class for datatypes that represent data constructors.
32-- For non-symbolic constructors, only 'conName' has to be defined.
33-- The weird argument is supposed to be instantiated with 'C' from
34-- base, hence the complex kind.
35class Constructor c where
36  conName   :: t c (f :: * -> *) r -> String
37  conFixity :: t c (f :: * -> *) r -> Fixity
38  conFixity = const Prefix
39  conIsRecord :: t c (f :: * -> *) r -> Bool
40  conIsRecord = const False
41
42-- | Datatype to represent the fixity of a constructor. An infix declaration
43-- directly corresponds to an application of 'Infix'.
44data Fixity = Prefix | Infix Associativity Int
45  deriving (Eq, Show, Ord, Read)
46
47data Associativity = LeftAssociative | RightAssociative | NotAssociative
48  deriving (Eq, Show, Ord, Read)
49
50-----------------------------------------------------------------------------
51-- Type class capturing the structural representation of a type and the
52-- corresponding embedding-projection pairs.
53-----------------------------------------------------------------------------
54-- | The type family @PF@ represents the pattern functor of a datatype.
55--
56-- To be able to use the generic functions, the user is required to provide
57-- an instance of this type family.
58type family PF a :: * -> *
59
60-- | The type class @Regular@ captures the structural representation of a
61-- type and the corresponding embedding-projection pairs.
62--
63-- To be able to use the generic functions, the user is required to provide
64-- an instance of this type class.
65class Regular a where
66  from      :: a -> PF a a
67  to        :: PF a a -> a
68
69-----------------------------------------------------------------------------
70-- Generic update function: updates all Strings, leaves the rest unchanged.
71-----------------------------------------------------------------------------
72
73class UpdateString f where
74  updateStringf :: (a -> a) -> f a -> f a
75
76instance UpdateString U where
77  updateStringf = updateStringfU
78
79instance UpdateString I where
80  updateStringf = updateStringfI
81
82instance UpdateString (K String) where
83  updateStringf = updateStringfKString
84
85instance UpdateString (K x) where
86  updateStringf = updateStringfK
87
88instance (UpdateString f, UpdateString g) => UpdateString (f :+: g) where
89  updateStringf = updateStringfPlus
90
91instance (UpdateString f, UpdateString g) => UpdateString (f :*: g) where
92  updateStringf = updateStringfTimes
93
94instance (UpdateString f) => UpdateString (C c f) where
95  updateStringf = updateStringfC
96
97{-# INLINE updateStringfU #-}
98updateStringfU _ = id
99
100{-# INLINE updateStringfI #-}
101updateStringfI f (I x) = I (f x)
102
103{-# INLINE updateStringfKString #-}
104updateStringfKString f (K "") = K ""
105updateStringfKString f (K s)  = K (last s : tail s)
106
107{-# INLINE updateStringfK #-}
108updateStringfK f (K x) = K x
109
110{-# INLINE updateStringfPlus #-}
111updateStringfPlus f (L x) = L (updateStringf f x)
112updateStringfPlus f (R x) = R (updateStringf f x)
113
114{-# INLINE updateStringfTimes #-}
115updateStringfTimes f (x :*: y) = updateStringf f x :*: updateStringf f y
116
117{-# INLINE updateStringfC #-}
118updateStringfC f (C x) = C (updateStringf f x)
119
120
121{-# INLINE updateString #-}
122updateString :: (Regular a, UpdateString (PF a)) => a -> a
123updateString = to . updateStringf (updateString) . from
124
125-----------------------------------------------------------------------------
126-- Test datatypes and their generic representations
127-----------------------------------------------------------------------------
128
129data Logic = Var String
130           | T                            -- true
131           | F                            -- false
132           | Not Logic                    -- not
133           | Impl  Logic Logic            -- implication
134           | Equiv Logic Logic            -- equivalence
135           | Conj  Logic Logic            -- and (conjunction)
136           | Disj  Logic Logic            -- or (disjunction)
137
138
139data Logic_Var_
140data Logic_Impl_
141data Logic_Equiv_
142data Logic_Conj_
143data Logic_Disj_
144data Logic_Not_
145data Logic_T_
146data Logic_F_
147
148instance Constructor Logic_Var_ where
149    { conName _ = "Var" }
150instance Constructor Logic_Impl_ where
151    { conName _ = "Impl" }
152instance Constructor Logic_Equiv_ where
153    { conName _ = "Equiv" }
154instance Constructor Logic_Conj_ where
155    { conName _ = "Conj" }
156instance Constructor Logic_Disj_ where
157    { conName _ = "Disj" }
158instance Constructor Logic_Not_ where
159    { conName _ = "Not" }
160instance Constructor Logic_T_ where
161    { conName _ = "T" }
162instance Constructor Logic_F_ where
163    { conName _ = "F" }
164   
165type PFLogic =
166      (C Logic_Var_ (K String))
167  :+: (C Logic_T_ U)
168  :+: (C Logic_F_ U)
169  :+: (C Logic_Not_ I)
170  :+: (C Logic_Impl_ ((:*:) I I))
171  :+: (C Logic_Equiv_ ((:*:) I I))
172  :+: (C Logic_Conj_ ((:*:) I I))
173  :+: (C Logic_Disj_ ((:*:) I I))
174
175type instance PF Logic = PFLogic
176instance Regular Logic where
177  from = fromLogic 
178  to   = toLogic
179
180fromLogic (Var f0) = L (C (K f0))
181fromLogic T = R (L (C U))
182fromLogic F = R (R (L (C U)))
183fromLogic (Not f0) = R (R (R (L (C (I f0)))))
184fromLogic (Impl f0 f1) = R (R (R (R (L (C ((:*:) (I f0) (I f1)))))))
185fromLogic (Equiv f0 f1) = R (R (R (R (R (L (C ((:*:) (I f0) (I f1))))))))
186fromLogic (Conj f0 f1) = R (R (R (R (R (R (L (C ((:*:) (I f0) (I f1)))))))))
187fromLogic (Disj f0 f1) = R (R (R (R (R (R (R (C ((:*:) (I f0) (I f1)))))))))
188
189toLogic (L (C (K f0))) = Var f0
190toLogic (R (L (C U))) = T
191toLogic (R (R (L (C U)))) = F
192toLogic (R (R (R (L (C (I f0)))))) = Not f0
193toLogic (R (R (R (R (L (C ((:*:) (I f0) (I f1)))))))) = Impl f0 f1
194toLogic (R (R (R (R (R (L (C ((:*:) (I f0) (I f1))))))))) = Equiv f0 f1
195toLogic (R (R (R (R (R (R (L (C ((:*:) (I f0) (I f1)))))))))) = Conj f0 f1
196toLogic (R (R (R (R (R (R (R (C ((:*:) (I f0) (I f1)))))))))) = Disj f0 f1
197
198-----------------------------------------------------------------------------
199-- INLINE pragmas for the generic representations
200-----------------------------------------------------------------------------
201
202{-# INLINE fromLogic #-}
203{-# INLINE toLogic #-}
204
205-----------------------------------------------------------------------------
206-- Test values
207-----------------------------------------------------------------------------
208
209logic :: Logic
210logic = Impl (Not T) (Var "x")
211
212testLogic = updateString logic