]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Compiling/Term.hs
Change Term to be a GADT, to avoid type applications and allow TypeOf Term.
[haskell/symantic.git] / symantic / Language / Symantic / Compiling / Term.hs
1 {-# LANGUAGE AllowAmbiguousTypes #-}
2 {-# LANGUAGE ConstraintKinds #-}
3 {-# LANGUAGE ExistentialQuantification #-}
4 {-# LANGUAGE GADTs #-}
5 {-# LANGUAGE TypeInType #-}
6 {-# LANGUAGE UndecidableInstances #-}
7 {-# OPTIONS_GHC -fno-warn-orphans #-}
8 module Language.Symantic.Compiling.Term where
9
10 import Data.Maybe (isJust)
11 import Data.Semigroup (Semigroup(..))
12 import qualified Data.Kind as K
13 import qualified Data.Set as Set
14 import qualified Data.Text as Text
15
16 import Language.Symantic.Grammar
17 import Language.Symantic.Interpreting
18 import Language.Symantic.Transforming.Trans
19 import Language.Symantic.Typing
20
21 -- * Type 'Term'
22 data Term src ss ts vs (t::K.Type) where
23 Term :: Type src vs q
24 -> Type src vs t
25 -> TeSym ss ts (q #> t)
26 -> Term src ss ts vs (q #> t)
27 instance Source src => Eq (Term src ss ts vs t) where
28 Term qx tx _ == Term qy ty _ = qx == qy && tx == ty
29 instance Source src => Show (Term src ss ts vs t) where
30 showsPrec p (Term q t _te) = showsPrec p (q #> t)
31
32 -- Source
33 type instance SourceOf (Term src ss ts vs t) = src
34 instance Source src => Sourced (Term src ss ts vs t) where
35 sourceOf (Term _q t _te) = sourceOf t
36 setSource (Term q t te) src = Term q (setSource t src) te
37
38 -- Const
39 instance ConstsOf (Term src ss ts vs t) where
40 constsOf (Term q t _te) = constsOf q `Set.union` constsOf t
41
42 -- Var
43 type instance VarsOf (Term src ss ts vs t) = vs
44 instance LenVars (Term src ss ts vs t) where
45 lenVars (Term _q t _te) = lenVars t
46 instance AllocVars (Term src ss ts) where
47 allocVarsL len (Term q t te) = Term (allocVarsL len q) (allocVarsL len t) te
48 allocVarsR len (Term q t te) = Term (allocVarsR len q) (allocVarsR len t) te
49
50 -- Fam
51 instance ExpandFam (Term src ss ts vs t) where
52 expandFam (Term q t te) = Term (expandFam q) (expandFam t) te
53
54 -- Type
55 instance Inj_Source (TermT src ss ts vs) src => TypeOf (Term src ss ts vs) where
56 typeOf t = typeOfTerm t `source` TermT t
57
58 typeOfTerm :: Source src => Term src ss ts vs t -> Type src vs t
59 typeOfTerm (Term q t _) = q #> t
60
61 -- ** Type 'TermT'
62 -- | 'Term' with existentialized 'Type'.
63 data TermT src ss ts vs = forall t. TermT (Term src ss ts vs t)
64 instance Source src => Show (TermT src ss ts vs) where
65 showsPrec p (TermT t) = showsPrec p t
66
67 -- ** Type 'TermVT'
68 -- | 'Term' with existentialized 'Var's and 'Type'.
69 data TermVT src ss ts = forall vs t. TermVT (Term src ss ts vs t)
70 instance Source src => Eq (TermVT src ss ts) where
71 TermVT x == TermVT y =
72 case appendVars x y of
73 (Term qx' tx' _, Term qy' ty' _) ->
74 isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty')
75 instance Source src => Show (TermVT src ss ts) where
76 showsPrec p (TermVT t) = showsPrec p t
77 type instance SourceOf (TermVT src ss ts) = src
78 instance Source src => Sourced (TermVT src ss ts) where
79 sourceOf (TermVT t) = sourceOf t
80 setSource (TermVT t) src = TermVT $ setSource t src
81
82 liftTermVT :: TermVT src ss '[] -> TermVT src ss ts
83 liftTermVT (TermVT (Term q t (TeSym te))) =
84 TermVT $ Term q t $
85 TeSym $ \_c -> te CtxTeZ
86
87 -- ** Type 'TermAVT'
88 -- | Like 'TermVT', but 'CtxTe'-free.
89 data TermAVT src ss = forall vs t. TermAVT (forall ts. Term src ss ts vs t)
90 type instance SourceOf (TermAVT src ss) = src
91 instance Source src => Sourced (TermAVT src ss) where
92 sourceOf (TermAVT t) = sourceOf t
93 setSource (TermAVT t) src = TermAVT (setSource t src)
94 instance Source src => Eq (TermAVT src ss) where
95 TermAVT x == TermAVT y =
96 case appendVars x y of
97 (Term qx' tx' _, Term qy' ty' _) ->
98 isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty')
99 instance Source src => Show (TermAVT src ss) where
100 showsPrec p (TermAVT t) = showsPrec p t
101
102 -- * Type 'TeSym'
103 -- | Symantic of a 'Term'.
104 newtype TeSym ss ts (t::K.Type)
105 = TeSym
106 ( forall term.
107 Syms ss term =>
108 Sym_Lambda term =>
109 QualOf t =>
110 CtxTe term ts -> term (UnQualOf t)
111 )
112
113 -- | Like 'TeSym', but 'CtxTe'-free
114 -- and using 'inj_Sym' to be able to use 'Sym'@ (@'Proxy'@ s)@ inside.
115 teSym ::
116 forall s ss ts t.
117 Inj_Sym ss s =>
118 (forall term. Sym (Proxy s) term => Sym_Lambda term => QualOf t => term (UnQualOf t)) ->
119 TeSym ss ts t
120 teSym t = inj_Sym @s (TeSym $ const t)
121
122 -- ** Type family 'QualOf'
123 -- | Qualification
124 type family QualOf (t::K.Type) :: Constraint where
125 QualOf (q #> t) = q -- (q # QualOf t)
126 QualOf t = (()::Constraint)
127
128 -- ** Type family 'UnQualOf'
129 -- | Unqualification
130 type family UnQualOf (t::K.Type) :: K.Type where
131 UnQualOf (q #> t) = t -- UnQualOf t
132 UnQualOf t = t
133
134 -- | Return 'K.Constraint' and 'K.Type' part of given 'Type'.
135 unQualTy ::
136 Source src =>
137 Type src vs (t::K.Type) ->
138 ( TypeK src vs K.Constraint
139 , TypeK src vs K.Type )
140 unQualTy (TyApp _ (TyApp _ c q) t)
141 | Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) c
142 = (TypeK q, TypeK t)
143 unQualTy t = (TypeK $ noConstraintLen (lenVars t), TypeK t)
144
145 -- | Remove 'K.Constraint's from given 'Type'.
146 unQualsTy :: Source src => Type src vs (t::kt) -> TypeK src vs kt
147 unQualsTy (TyApp _ (TyApp _ c _q) t)
148 | Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) c
149 = unQualsTy t
150 unQualsTy (TyApp src f a)
151 | TypeK f' <- unQualsTy f
152 , TypeK a' <- unQualsTy a
153 = TypeK $ TyApp src f' a'
154 unQualsTy t = TypeK t
155
156 -- * Type 'CtxTe'
157 -- | GADT for an /interpreting context/:
158 -- accumulating at each /lambda abstraction/
159 -- the @term@ of the introduced variable.
160 data CtxTe (term::K.Type -> K.Type) (hs::[K.Type]) where
161 CtxTeZ :: CtxTe term '[]
162 CtxTeS :: term t
163 -> CtxTe term ts
164 -> CtxTe term (t ': ts)
165 infixr 5 `CtxTeS`
166
167 -- ** Type 'TermDef'
168 -- | Convenient type alias for defining 'Term'.
169 type TermDef s vs t = forall src ss ts. Source src => Inj_Sym ss s => Term src ss ts vs t
170
171 -- ** Type family 'Sym'
172 type family Sym (s::K.Type) :: {-term-}(K.Type -> K.Type) -> Constraint
173
174 -- ** Type family 'Syms'
175 type family Syms (ss::[K.Type]) (term:: K.Type -> K.Type) :: Constraint where
176 Syms '[] term = ()
177 Syms (s ': ss) term = (Sym s term, Syms ss term)
178
179 -- ** Type 'Inj_Sym'
180 -- | Convenient type synonym wrapping 'Inj_SymP'
181 -- applied on the correct 'Index'.
182 type Inj_Sym ss s = Inj_SymP (Index ss (Proxy s)) ss s
183
184 -- | Inject a given /symantic/ @s@ into a list of them,
185 -- by returning a function which given a 'TeSym' on @s@
186 -- returns the same 'TeSym' on @ss@.
187 inj_Sym ::
188 forall s ss ts t.
189 Inj_Sym ss s =>
190 TeSym '[Proxy s] ts t ->
191 TeSym ss ts t
192 inj_Sym = inj_SymP (Proxy @(Index ss (Proxy s)))
193
194 -- *** Class 'Inj_SymP'
195 class Inj_SymP p ss s where
196 inj_SymP :: Proxy p -> TeSym '[Proxy s] ts t -> TeSym ss ts t
197 instance Inj_SymP Zero (Proxy s ': ss) (s::k) where
198 inj_SymP _ = \(TeSym te) -> TeSym te
199 instance Inj_SymP p ss s => Inj_SymP (Succ p) (not_s ': ss) s where
200 inj_SymP _p = \(te::TeSym '[Proxy s] ts t) ->
201 case inj_SymP (Proxy @p) te :: TeSym ss ts t of
202 TeSym te' -> TeSym te'
203
204 -- * Class 'Sym_Lambda'
205 class Sym_Lambda term where
206 -- | /Function application/.
207 apply :: term ((a -> b) -> a -> b)
208 default apply :: Sym_Lambda (UnT term) => Trans term => term ((a -> b) -> a -> b)
209 apply = trans apply
210
211 -- | /Lambda application/.
212 app :: term (a -> b) -> (term a -> term b); infixr 0 `app`
213 default app :: Sym_Lambda (UnT term) => Trans term => term (arg -> res) -> term arg -> term res
214 app = trans2 app
215
216 -- | /Lambda abstraction/.
217 lam :: (term a -> term b) -> term (a -> b)
218 default lam :: Sym_Lambda (UnT term) => Trans term => (term arg -> term res) -> term (arg -> res)
219 lam f = trans $ lam (unTrans . f . trans)
220
221 -- | Convenient 'lam' and 'app' wrapper.
222 let_ :: term var -> (term var -> term res) -> term res
223 let_ x f = lam f `app` x
224
225 -- | /Lambda abstraction/ beta-reducable without duplication
226 -- (i.e. whose variable is used once at most),
227 -- mainly useful in compiled 'Term's
228 -- whose symantics are not a single 'term'
229 -- but a function between 'term's,
230 -- which happens because those are more usable when used as an embedded DSL.
231 lam1 :: (term a -> term b) -> term (a -> b)
232 default lam1 :: Sym_Lambda (UnT term) => Trans term => (term a -> term b) -> term (a -> b)
233 lam1 = lam
234
235 -- | /Qualification/.
236 --
237 -- Workaround used in 'readTermWithCtx'.
238 qual :: proxy q -> term t -> term (q #> t)
239 default qual :: Sym_Lambda (UnT term) => Trans term => proxy q -> term t -> term (q #> t)
240 qual q = trans1 (qual q)
241
242 lam2 :: Sym_Lambda term => (term a -> term b -> term c) -> term (a -> b -> c)
243 lam3 :: Sym_Lambda term => (term a -> term b -> term c -> term d) -> term (a -> b -> c -> d)
244 lam4 :: Sym_Lambda term => (term a -> term b -> term c -> term d -> term e) -> term (a -> b -> c -> d -> e)
245 lam2 f = lam1 $ lam1 . f
246 lam3 f = lam1 $ lam2 . f
247 lam4 f = lam1 $ lam3 . f
248
249 -- Interpreting
250 instance Sym_Lambda Eval where
251 apply = Eval ($)
252 app = (<*>)
253 lam f = Eval (unEval . f . Eval)
254 lam1 = lam
255 qual _q (Eval t) = Eval $ Qual t
256 let_ x f = f x -- NOTE: like flip ($)
257 instance Sym_Lambda View where
258 apply = View $ \_po _v -> "($)"
259 app (View a1) (View a2) = View $ \po v ->
260 parenInfix po op $
261 a1 (op, SideL) v <> " " <> a2 (op, SideR) v
262 where op = infixN 10
263 lam f = View $ \po v ->
264 let x = "x" <> Text.pack (show v) in
265 parenInfix po op $
266 "\\" <> x <> " -> " <>
267 unView (f (View $ \_po _v -> x)) (op, SideL) (succ v)
268 where op = infixN 1
269 lam1 = lam
270 qual _q (View t) = View t -- TODO: maybe print q
271 let_ x f =
272 View $ \po v ->
273 let x' = "x" <> Text.pack (show v) in
274 parenInfix po op $
275 "let" <> " " <> x' <> " = "
276 <> unView x (infixN 0, SideL) (succ v) <> " in "
277 <> unView (f (View $ \_po _v -> x')) (op, SideL) (succ v)
278 where op = infixN 1
279 instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (Dup r1 r2) where
280 apply = dup0 @Sym_Lambda apply
281 app = dup2 @Sym_Lambda app
282 lam f = dup_1 lam_f `Dup` dup_2 lam_f
283 where lam_f = lam f
284 lam1 = lam
285 qual q = dup1 @Sym_Lambda (qual q)