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