]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Lambda.hs
Add compileWithTyCtx.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Lambda.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE PolyKinds #-}
4 {-# LANGUAGE UndecidableInstances #-}
5 {-# OPTIONS_GHC -fno-warn-orphans #-}
6 -- | Symantic for '(->)'.
7 module Language.Symantic.Lib.Lambda where
8
9 import Data.MonoTraversable (MonoFunctor)
10 import Data.Monoid ((<>))
11 import Data.Proxy (Proxy(..))
12 import Data.Type.Equality ((:~:)(..))
13 import Prelude hiding ((^))
14 import qualified Data.Function as Fun
15 import qualified Data.Text as Text
16
17 import Language.Symantic.Parsing
18 import Language.Symantic.Typing
19 import Language.Symantic.Compiling
20 import Language.Symantic.Interpreting
21 import Language.Symantic.Transforming
22 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
23
24 -- * Class 'Sym_Lambda'
25 class Sym_Lambda term where
26 -- | /Lambda abstraction/.
27 lam :: (term arg -> term res) -> term (arg -> res)
28 default lam :: Trans t term => (t term arg -> t term res) -> t term (arg -> res)
29 lam f = trans_lift $ lam $ trans_apply . f . trans_lift
30
31 -- | /Lambda application/.
32 (.$) :: term (arg -> res) -> term arg -> term res
33 default (.$) :: Trans t term => t term (arg -> res) -> t term arg -> t term res
34 infixr 0 .$
35 (.$) f x = trans_lift (trans_apply f .$ trans_apply x)
36
37 -- | Convenient 'lam' and '.$' wrapper.
38 let_ :: term var -> (term var -> term res) -> term res
39 let_ x y = lam y .$ x
40
41 id :: term a -> term a
42 id a = lam Fun.id .$ a
43
44 const :: term a -> term b -> term a
45 const a b = (lam (lam . Fun.const) .$ a) .$ b
46
47 -- | /Lambda composition/.
48 (^) :: term (b -> c) -> term (a -> b) -> term (a -> c)
49 (^) f g = lam $ \a -> f .$ (g .$ a)
50 infixr 9 ^
51
52 flip :: term (a -> b -> c) -> term (b -> a -> c)
53 flip f = lam $ \b -> lam $ \a -> (f .$ a) .$ b
54
55 type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
56 type instance TyConsts_of_Iface (Proxy (->)) = Proxy (->) ': TyConsts_imported_by (Proxy (->))
57 type instance TyConsts_imported_by (Proxy (->)) =
58 [ Proxy Applicative
59 , Proxy Functor
60 , Proxy Monad
61 , Proxy Monoid
62 , Proxy MonoFunctor
63 ]
64
65 instance Sym_Lambda HostI where
66 lam f = HostI (unHostI . f . HostI)
67 (.$) = (<*>)
68 instance Sym_Lambda TextI where
69 lam f = TextI $ \po v ->
70 let x = "x" <> Text.pack (show v) in
71 infix_paren po op $
72 "\\" <> x <> " -> " <>
73 unTextI (f (TextI $ \_po _v -> x)) (op, L) (succ v)
74 where op = infixN 1
75 -- (.$) = textI_infix "$" (Precedence 0)
76 (.$) (TextI a1) (TextI a2) = TextI $ \po v ->
77 infix_paren po op $
78 a1 (op, L) v <> " " <> a2 (op, R) v
79 where op = infixN 10
80 let_ e in_ =
81 TextI $ \po v ->
82 let x = "x" <> Text.pack (show v) in
83 infix_paren po op $
84 "let" <> " " <> x <> " = "
85 <> unTextI e (infixN 0, L) (succ v) <> " in "
86 <> unTextI (in_ (TextI $ \_po _v -> x)) (op, L) (succ v)
87 where op = infixN 2
88 (^) = textI_infix "." (infixR 9)
89 id = textI1 "id"
90 const = textI2 "const"
91 flip = textI1 "flip"
92 instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
93 lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
94 where lam_f = lam f
95 (.$) = dupI2 @Sym_Lambda (.$)
96
97 instance
98 ( Read_TyNameR TyName cs rs
99 , Inj_TyConst cs (->)
100 ) => Read_TyNameR TyName cs (Proxy (->) ': rs) where
101 read_TyNameR _cs (TyName "(->)") k = k (ty @(->))
102 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
103 instance Show_TyConst cs => Show_TyConst (Proxy (->) ': cs) where
104 show_TyConst TyConstZ{} = "(->)"
105 show_TyConst (TyConstS c) = show_TyConst c
106
107 instance -- Proj_TyFamC TyFam_MonoElement
108 ( Proj_TyConst cs (->)
109 ) => Proj_TyFamC cs TyFam_MonoElement (->) where
110 proj_TyFamC _c _fam ((TyConst c :$ _ty_r :$ ty_a) `TypesS` TypesZ)
111 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
112 , Just Refl <- proj_TyConst c (Proxy @(->))
113 = Just ty_a
114 proj_TyFamC _c _fam _ty = Nothing
115
116 instance -- Proj_TyConC (->)
117 ( Proj_TyConst cs (->)
118 , Proj_TyConsts cs (TyConsts_imported_by (Proxy (->)))
119 , Proj_TyCon cs
120 ) => Proj_TyConC cs (Proxy (->)) where
121 proj_TyConC _ (TyConst q :$ (TyConst c :$ _r))
122 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
123 , Just Refl <- proj_TyConst c (Proxy @(->))
124 = case () of
125 _ | Just Refl <- proj_TyConst q (Proxy @Functor) -> Just TyCon
126 | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
127 | Just Refl <- proj_TyConst q (Proxy @Monad) -> Just TyCon
128 _ -> Nothing
129 proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
130 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
131 , Just Refl <- proj_TyConst c (Proxy @(->))
132 = case () of
133 _ | Just Refl <- proj_TyConst q (Proxy @Monoid)
134 , Just TyCon <- proj_TyCon (t :$ b) -> Just TyCon
135 | Just Refl <- proj_TyConst q (Proxy @MonoFunctor) -> Just TyCon
136 _ -> Nothing
137 proj_TyConC _c _q = Nothing
138 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy (->)))
139 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy (->)))
140
141 instance -- CompileI (->)
142 ( Inj_TyConst cs (->)
143 , Read_TyName TyName cs
144 , Compile cs is
145 ) => CompileI cs is (Proxy (->)) where
146 compileI tok ctx k =
147 case tok of
148 Token_Term_Abst name_arg tok_ty_arg tok_body ->
149 compile_Type tok_ty_arg $ \(ty_arg::Type cs h) ->
150 check_Kind
151 (At Nothing SKiType)
152 (At (Just $ tok_ty_arg) $ kind_of ty_arg) $ \Refl ->
153 compile tok_body
154 (TyCtxS name_arg ty_arg ctx) $
155 \ty_res (Term res) ->
156 k (ty_arg ~> ty_res) $ Term $
157 \c -> lam $ \arg ->
158 res (arg `TeCtxS` c)
159 Token_Term_App tok_lam tok_arg_actual ->
160 compile tok_lam ctx $ \ty_lam (Term lam_) ->
161 compile tok_arg_actual ctx $ \ty_arg_actual (Term arg_actual) ->
162 check_TyEq2 (ty @(->)) (At (Just tok_lam) ty_lam) $ \Refl ty_arg ty_res ->
163 check_TyEq
164 (At (Just tok_lam) ty_arg)
165 (At (Just tok_arg_actual) ty_arg_actual) $ \Refl ->
166 k ty_res $ Term $
167 \c -> lam_ c .$ arg_actual c
168 Token_Term_Let name tok_bound tok_body ->
169 compile tok_bound ctx $ \ty_bound (Term bound) ->
170 compile tok_body (TyCtxS name ty_bound ctx) $ \ty_res (Term res) ->
171 k ty_res $ Term $
172 \c -> let_ (bound c) $ \arg -> res (arg `TeCtxS` c)
173 Token_Term_Var nam -> lookup_var nam ctx k
174 where
175 lookup_var :: forall meta hs ret ls rs.
176 TeName
177 -> TyCtx TeName cs hs
178 -> ( forall h.
179 Type cs (h:: *)
180 -> Term hs h is ls rs
181 -> Either (Error_Term meta cs is) ret )
182 -> Either (Error_Term meta cs is) ret
183 lookup_var name tyCtx k' =
184 case tyCtx of
185 TyCtxZ -> Left $ Error_Term_unbound name
186 TyCtxS n typ _ | n == name ->
187 k' typ $ Term $ \(te `TeCtxS` _) -> te
188 TyCtxS _n _typ tyCtx' ->
189 lookup_var name tyCtx' $ \typ (Term te::Term hs' h is '[] is) ->
190 k' typ $ Term $ \(_ `TeCtxS` c) -> te c
191 Token_Term_Compose tok_f tok_g ->
192 -- (.) :: (b -> c) -> (a -> b) -> a -> c
193 compile tok_f ctx $ \ty_f (Term f) ->
194 compile tok_g ctx $ \ty_g (Term g) ->
195 check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_b ty_c ->
196 check_TyEq2 (ty @(->)) (At (Just tok_g) ty_g) $ \Refl ty_a ty_g_b ->
197 check_TyEq
198 (At (Just tok_f) ty_f_b)
199 (At (Just tok_g) ty_g_b) $ \Refl ->
200 k (ty_a ~> ty_c) $ Term $
201 \c -> (^) (f c) (g c)
202 instance
203 Inj_Token meta ts (->) =>
204 TokenizeT meta ts (Proxy (->)) where
205 tokenizeT _t = mempty
206 { tokenizers_infix = tokenizeTMod []
207 [ tokenize2 "." (infixR 9) Token_Term_Compose
208 , tokenize2 "$" (infixR 0) Token_Term_App
209 ]
210 }
211 instance Gram_Term_AtomsT meta ts (Proxy (->)) g
212
213 -- | The function 'Type' @(->)@,
214 -- with an infix notation more readable.
215 (~>) :: forall cs a b. Inj_TyConst cs (->)
216 => Type cs a -> Type cs b -> Type cs (a -> b)
217 (~>) a b = ty @(->) :$ a :$ b
218 infixr 5 ~>