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