]> Git — Sourcephile - haskell/symantic-base.git/blob - src/Symantic/Semantics/Forall.hs
iface: add interpreter `LetInserter`
[haskell/symantic-base.git] / src / Symantic / Semantics / Forall.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE EmptyCase #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE QuantifiedConstraints #-}
5 {-# LANGUAGE RankNTypes #-}
6 {-# LANGUAGE UndecidableInstances #-}
7
8 -- | This module provides the 'Forall' semantic
9 -- which preserves the polymorphism of the semantic.
10 -- Useful when parsing the syntax from a text
11 -- (ie. when the domain-specific language
12 -- is not embedded into a Haskell file).
13 module Symantic.Semantics.Forall where
14
15 import Control.Applicative (Applicative (..))
16 import Control.Monad (Monad (..))
17 import Data.Bool (Bool (..))
18 import Data.Eq (Eq (..))
19 import Data.Eq qualified as Eq
20 import Data.Function qualified as Fun
21 import Data.Functor (Functor (..))
22 import Data.Kind (Type)
23 import Data.Tuple qualified as Tuple
24 import Text.Show (Show (..))
25 import Unsafe.Coerce (unsafeCoerce)
26
27 import Symantic.Syntaxes.Classes
28
29 -- * Type 'Forall'
30 newtype Forall (syns :: [Syntax]) (a :: Type)
31 = Forall (forall sem. Syntaxes syns sem => sem a)
32
33 {-# INLINE forall1 #-}
34 forall1 ::
35 (forall sem. Syntaxes syns sem => sem a -> sem b) ->
36 Forall syns a -> Forall syns b
37 forall1 f (Forall a) = Forall (f a)
38
39 {-# INLINE forall2 #-}
40 forall2 ::
41 (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c) ->
42 Forall syns a -> Forall syns b -> Forall syns c
43 forall2 f (Forall a) (Forall b) = Forall (f a b)
44
45 {-# INLINE forall3 #-}
46 forall3 ::
47 (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c -> sem d) ->
48 Forall syns a -> Forall syns b -> Forall syns c -> Forall syns d
49 forall3 f (Forall a) (Forall b) (Forall c) = Forall (f a b c)
50
51 {-# INLINE forall4 #-}
52 forall4 ::
53 (forall sem. Syntaxes syns sem => sem a -> sem b -> sem c -> sem d -> sem e) ->
54 Forall syns a -> Forall syns b -> Forall syns c -> Forall syns d -> Forall syns e
55 forall4 f (Forall a) (Forall b) (Forall c) (Forall d) = Forall (f a b c d)
56
57 instance
58 ( forall sem. Syntaxes syns sem => Functor sem
59 ) => Functor (Forall syns) where
60 fmap f = forall1 (fmap f)
61 (<$) a = forall1 (a <$)
62 instance
63 ( forall sem. Syntaxes syns sem => Applicative sem
64 , Functor (Forall syns)
65 ) => Applicative (Forall syns) where
66 pure a = Forall (pure a)
67 liftA2 f = forall2 (liftA2 f)
68 (<*>) = forall2 (<*>)
69 (<*) = forall2 (<*)
70 (*>) = forall2 (*>)
71 instance
72 ( forall sem. Syntaxes syns sem => Monad sem
73 , Applicative (Forall syns)
74 ) => Monad (Forall syns) where
75 (>>=) (Forall sa) f = Forall (sa >>= \a -> case f a of Forall sb -> sb)
76 return = pure
77 (>>) = (*>)
78 instance
79 ( forall sem. Syntaxes syns sem => Varable sem
80 ) => Varable (Forall syns) where
81 var = forall1 var
82 instance
83 (forall sem. Syntaxes syns sem => Instantiable sem) =>
84 Instantiable (Forall syns)
85 where
86 (.@) = forall2 (.@)
87 instance
88 ( forall sem. Syntaxes syns sem => Abstractable sem
89 , forall sem. Syntaxes syns sem => Instantiable sem
90 ) => Abstractable (Forall syns) where
91 lam f = Forall (lam (\a -> let Forall b = f (forallSem a) in b))
92 where
93 -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
94 forallSem :: sem a -> Forall syns a
95 forallSem a = Forall (unsafeCoerce a)
96 instance
97 ( forall sem. Syntaxes syns sem => Unabstractable sem
98 ) => Unabstractable (Forall syns) where
99 ap = Forall ap
100 const = Forall const
101 id = Forall id
102 (.) = Forall (.)
103 flip = Forall flip
104 ($) = Forall ($)
105 instance
106 ( forall sem. Syntaxes syns sem => Constantable c sem
107 ) => Constantable c (Forall syns) where
108 constant c = Forall (constant c)
109 instance
110 ( forall sem. Syntaxes syns sem => Eitherable sem
111 ) => Eitherable (Forall syns) where
112 either = Forall either
113 left = Forall left
114 right = Forall right
115 instance
116 ( forall sem. Syntaxes syns sem => Equalable sem
117 ) => Equalable (Forall syns) where
118 equal = Forall equal
119 instance
120 ( forall sem. Syntaxes syns sem => IfThenElseable sem
121 ) => IfThenElseable (Forall syns) where
122 ifThenElse = forall3 ifThenElse
123 instance
124 ( forall sem. Syntaxes syns sem => Inferable c sem
125 ) => Inferable c (Forall syns) where
126 infer = Forall infer
127 instance
128 ( forall sem. Syntaxes syns sem => Listable sem
129 ) => Listable (Forall syns) where
130 cons = Forall cons
131 nil = Forall nil
132 instance
133 ( forall sem. Syntaxes syns sem => Maybeable sem
134 ) => Maybeable (Forall syns) where
135 just = Forall just
136 nothing = Forall nothing
137 instance
138 ( forall sem. Syntaxes syns sem => IsoFunctor sem
139 ) => IsoFunctor (Forall syns) where
140 (<%>) iso = forall1 (iso <%>)
141 instance
142 ( forall sem. Syntaxes syns sem => ProductFunctor sem
143 , forall sem. Syntaxes syns sem => IsoFunctor sem
144 , Syntaxes syns (Forall syns)
145 ) => ProductFunctor (Forall syns) where
146 (<.>) = forall2 (<.>)
147 ra <. rb = Iso Tuple.fst (,()) <%> (ra <.> rb)
148 ra .> rb = Iso Tuple.snd ((),) <%> (ra <.> rb)
149 instance
150 ( forall sem. Syntaxes syns sem => SumFunctor sem
151 ) => SumFunctor (Forall syns) where
152 (<+>) = forall2 (<+>)
153 instance
154 ( forall sem. Syntaxes syns sem => AlternativeFunctor sem
155 ) => AlternativeFunctor (Forall syns) where
156 (<|>) = forall2 (<|>)
157 instance
158 ( forall sem. Syntaxes syns sem => Dicurryable sem
159 ) => Dicurryable (Forall syns) where
160 dicurry args constr destr = forall1 (dicurry args constr destr)
161 instance
162 ( forall sem. Syntaxes syns sem => Emptyable sem
163 ) => Emptyable (Forall syns) where
164 empty = Forall empty
165 instance
166 ( forall sem. Syntaxes syns sem => Semigroupable sem
167 ) => Semigroupable (Forall syns) where
168 concat = Forall concat
169 instance
170 ( forall sem. Syntaxes syns sem => Optionable sem
171 ) => Optionable (Forall syns) where
172 optional = forall1 optional
173 instance
174 ( forall sem. Syntaxes syns sem => Repeatable sem
175 ) => Repeatable (Forall syns) where
176 many0 = forall1 many0
177 many1 = forall1 many1
178 instance
179 ( forall sem. Syntaxes syns sem => Substractable sem
180 ) => Substractable (Forall syns) where
181 (<->) = forall2 (<->)
182 instance
183 ( forall sem. Syntaxes syns sem => Voidable sem
184 ) => Voidable (Forall syns) where
185 void a = forall1 (void a)
186
187 -- * Type 'PerSyntax'
188 data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where
189 PerSyntaxZ :: a syn -> PerSyntax (syn ': syns) a
190 PerSyntaxS :: PerSyntax syns a -> PerSyntax (skipSyn ': syns) a
191
192 instance Eq (PerSyntax '[] a) where
193 (==) = \case {}
194 instance
195 ( Eq (a syn)
196 , Eq (PerSyntax syns a)
197 ) =>
198 Eq (PerSyntax (syn ': syns) a)
199 where
200 PerSyntaxZ x == PerSyntaxZ y = x Eq.== y
201 PerSyntaxS x == PerSyntaxS y = x Eq.== y
202 _ == _ = False
203
204 instance Show (PerSyntax '[] a) where
205 showsPrec _p = \case {}
206 instance
207 ( Show (a syn)
208 , Show (PerSyntax syns a)
209 ) =>
210 Show (PerSyntax (syn ': syns) a)
211 where
212 showsPrec p = \case
213 PerSyntaxZ a -> showsPrec p a
214 PerSyntaxS s -> showsPrec p s
215
216 -- ** Class 'PerSyntaxable'
217 class PerSyntaxable (syns :: [Syntax]) (syn :: Syntax) where
218 perSyntax :: a syn -> PerSyntax syns a
219 instance {-# OVERLAPS #-} PerSyntaxable (syn ': syns) syn where
220 perSyntax = PerSyntaxZ
221 instance PerSyntaxable syns syn => PerSyntaxable (skipSyn ': syns) syn where
222 perSyntax = PerSyntaxS Fun.. perSyntax