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 SourceInj (TermT src ss ts vs) src => TypeOf (Term src ss ts vs) where
  56         typeOf t = typeOfTerm t `withSource` 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 'symInj' to be able to use 'Sym'@ s@ inside.
 115 teSym ::
 116  forall s ss ts t.
 117  SymInj ss s =>
 118  (forall term. Sym s term => Sym_Lambda term => QualOf t => term (UnQualOf t)) ->
 119  TeSym ss ts t
 120 teSym t = symInj @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 to define a 'Term'.
 169 type TermDef s vs t = forall src ss ts. Source src => SymInj ss s => Term src ss ts vs t
 170
 171 -- ** Type family 'Sym'
 172 type family Sym (s::k) :: {-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 (Proxy s ': ss) term = (Sym s term, Syms ss term)
 178
 179 -- ** Type 'SymInj'
 180 -- | Convenient type synonym wrapping 'SymPInj'
 181 -- applied on the correct 'Index'.
 182 type SymInj ss s = SymInjP (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 symInj ::
 188  forall s ss ts t.
 189  SymInj ss s =>
 190  TeSym '[Proxy s] ts t ->
 191  TeSym ss ts t
 192 symInj = symInjP @(Index ss (Proxy s))
 193
 194 -- *** Class 'SymPInj'
 195 class SymInjP p ss s where
 196         symInjP :: TeSym '[Proxy s] ts t -> TeSym ss ts t
 197 instance SymInjP Zero (Proxy s ': ss) (s::k) where
 198         symInjP (TeSym te) = TeSym te
 199 instance SymInjP p ss s => SymInjP (Succ p) (Proxy not_s ': ss) s where
 200         symInjP (te::TeSym '[Proxy s] ts t) =
 201                 case symInjP @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)