symantic/Language/Symantic/Compiling/Term.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5 {-# OPTIONS_GHC -fno-warn-orphans #-}
   6 module Language.Symantic.Compiling.Term
   7  ( module Language.Symantic.Compiling.Term
   8  , module Language.Symantic.Compiling.Term.Grammar
   9  ) where
  10
  11 import Data.Proxy (Proxy(..))
  12 import qualified Data.Text as Text
  13 import Data.Type.Equality ((:~:)(..))
  14 import GHC.Exts (Constraint)
  15 import qualified Data.Kind as K
  16
  17 import Language.Symantic.Helper.Data.Type.List
  18 import Language.Symantic.Parsing
  19 import Language.Symantic.Typing
  20
  21 import Language.Symantic.Compiling.Term.Grammar
  22
  23 -- * Type 'Term'
  24 -- | An open term (i.e. depending on a 'TeCtx').
  25 -- The data type wraps a universal quantification
  26 -- over an interpreter @term@
  27 -- qualified by the symantics of a term.
  28 --
  29 -- Moreover the term is abstracted by a /lambda term context/
  30 -- built top-down by 'compile',
  31 -- to enable a /Higher-Order Abstract Syntax/ (HOAS)
  32 -- for /lambda abstractions/ ('lam').
  33 --
  34 -- This data type is used to keep a parsed term polymorphic enough
  35 -- to stay interpretable by different interpreters.
  36 --
  37 -- * @(@'Sym_of_Ifaces'@ is term)@
  38 -- is needed when a symantic method includes a polymorphic type
  39 -- and thus calls: 'compile'.
  40 --
  41 -- * @(@'Sym_of_Ifaces'@ ls term)@ and @(@'Sym_of_Ifaces'@ rs term)@
  42 -- make a zipper needed to be able to write the recursing 'CompileR' instance.
  43 --
  44 -- * @(@'Sym_of_Iface'@ (@'Proxy'@ (->)) term)@
  45 -- is needed to handle partially applied functions.
  46 data Term hs h is ls rs
  47  =   Term
  48  (forall term. ( Sym_of_Ifaces is term
  49                , Sym_of_Ifaces ls term
  50                , Sym_of_Ifaces rs term
  51                , Sym_of_Iface (Proxy (->)) term
  52                ) => TeCtx term hs -> term h)
  53
  54 -- ** Type 'ETerm'
  55 -- | Existential 'Term', with its 'Type'.
  56 data ETerm src hs cs is
  57  = forall (h:: *). ETerm (Type src cs h) (Term hs h is '[] is)
  58
  59 -- ** Type 'TermClosed'
  60 -- | Closed 'Term'.
  61 data TermClosed is h
  62  =   TermClosed
  63  (forall term. ( Sym_of_Ifaces is term
  64                , Sym_of_Iface (Proxy (->)) term
  65                ) => term h)
  66
  67 -- * Type 'ETermClosed'
  68 -- | Existential 'TermClosed', with its 'Type'.
  69 data ETermClosed src cs is
  70  = forall (h:: *). ETermClosed (Type src cs h) (TermClosed is h)
  71
  72 -- * Type 'Compile'
  73 -- | Convenient class wrapping 'CompileR' to initiate its recursion.
  74 class CompileR cs is '[] is => Compile cs is where
  75         compile :: AST_Term src is -> Compiler src hs ret cs is '[] is
  76 instance CompileR cs is '[] is => Compile cs is where
  77         compile (TokTree0 (EToken tok))            = compileR tok Nothing
  78         compile (TokTree0 (EToken x) `TokTree1` y) = compileR x (Just y)
  79         {-
  80         compile (tok_fun `TokTree1` tok_arg) = \ctx k ->
  81                 compile tok_fun ctx $ \ty_fun (Term fun) ->
  82                 compile tok_arg ctx $ \ty_arg (Term arg) ->
  83                 check_TyEq2 (ty @(->)) (At (Just tok_fun) ty_fun) $ \Refl ty_param ty_res ->
  84                 check_TyEq
  85                  (At (Just tok_fun) ty_param)
  86                  (At (Just tok_arg) ty_arg) $ \Refl ->
  87                 k ty_res $ Term $
  88                  \c -> fun c .$ arg c
  89         -}
  90
  91 -- ** Type 'CompilerWithTyCtx'
  92 -- | Convenient type synonym defining a term compiler
  93 -- with independant 'TyCtx' and 'TeCtx'.
  94 --
  95 -- This is the most general term compiler.
  96 --
  97 -- Useful to let the compiled term use
  98 -- terms whose type is known before 'compile' is run
  99 -- but actually available only after.
 100 type CompilerWithTyCtx src hs_ty hs_te ret cs is ls rs
 101  = TyCtx TeName cs hs_ty
 102  -- ^ The bound variables in scope and their types:
 103  -- built top-down in the heterogeneous list @hs@,
 104  -- from the closest including /lambda abstraction/ to the farest.
 105  -> ( forall h.
 106        Type src cs (h:: *)
 107     -> Term hs_te h is ls rs
 108     -> Either (Error_Term src cs is) ret )
 109  -- ^ The accumulating continuation, called bottom-up.
 110  -> Either (Error_Term src cs is) ret
 111
 112 -- | Like 'compile' but also enables the use of a 'TyCtx'
 113 -- whose actual terms are only known after 'compile' has been run.
 114 -- This also enables to 'compile' a term once
 115 -- and interpret it with different 'TeCtx's,
 116 -- providing the types of those terms match the given 'TyCtx'.
 117 compileWithTyCtx
 118  :: Compile cs is
 119  => AST_Term src is
 120  -> TyCtx TeName cs hs_ty
 121  -> Either (Error_Term src cs is) (ETerm src hs_ty cs is)
 122 compileWithTyCtx tok ctx =
 123         compile tok ctx $ \typ -> Right . ETerm typ
 124
 125 -- | Return given 'Compiler' augmented with given 'TyCtx'.
 126 compilerWithTyCtx
 127  :: Compile cs is
 128  => TyCtx TeName cs hs_ty
 129  -> (forall hs. Compiler src hs ret cs is ls rs)
 130  -> CompilerWithTyCtx src hs_te (hs_ty ++ hs_te) ret cs is ls rs
 131 compilerWithTyCtx tyCtx comp ctx =
 132         comp (appendTyCtx tyCtx ctx)
 133
 134 -- | Compile, closing the 'TyCtx'.
 135 compilerWithTyCtx_close
 136  :: CompilerWithTyCtx src '[] hs_te (ETerm src hs_te cs is) cs is '[] is
 137  -> Either (Error_Term src cs is) (ETerm src hs_te cs is)
 138 compilerWithTyCtx_close comp =
 139         comp TyCtxZ $ \typ -> Right . ETerm typ
 140
 141 -- ** Type 'Compiler'
 142 -- | Convenient type synonym defining a term compiler.
 143 -- with matching 'TyCtx' and 'TeCtx'.
 144 --
 145 -- Useful to let the compiled term use
 146 -- terms known before 'compile' is run.
 147 type Compiler          src hs    ret cs is ls rs
 148  =   CompilerWithTyCtx src hs hs ret cs is ls rs
 149
 150 -- | Compile with an empty /lambda context/.
 151 compileWithoutCtx
 152  :: Compile cs is
 153  => AST_Term src is
 154  -> Either (Error_Term src cs is) (ETermClosed src cs is)
 155 compileWithoutCtx tok = compilerWithCtx_close (compile tok)
 156
 157 -- ** Type 'ACompileWithCtx'
 158 -- | Wrap 'Compiler' to keep the /lambda context/ fully polymorphic.
 159 --
 160 -- Useful in 'compilerWithCtx' to help GHC's type solver, which
 161 -- "Cannot instantiate unification variable with a type involving foralls".
 162 data ACompileWithCtx src ret cs is ls rs
 163  =   ACompileWithCtx
 164  { unACompileWithCtx :: forall hs. Compiler src hs ret cs is ls rs }
 165
 166 -- | Compile with given /lambda context/.
 167 compilerWithCtx
 168  :: Foldable f
 169  => f (TeName, ETermClosed src cs is)
 170  -> (forall hs'. Compiler src hs' ret cs is ls rs)
 171  -> Compiler src hs ret cs is ls rs
 172 compilerWithCtx env comp = unACompileWithCtx $
 173         foldr
 174          (\e (ACompileWithCtx c) -> ACompileWithCtx $ compilerWithCtx_push e c)
 175          (ACompileWithCtx comp) env
 176
 177 -- | Return given 'Compiler' with a /lambda context/ augmented with given 'ETermClosed'.
 178 compilerWithCtx_push
 179  :: (TeName, ETermClosed src cs is)
 180  -> (forall hs'. Compiler src hs' ret cs is ls rs)
 181  -> Compiler src hs ret cs is ls rs
 182 compilerWithCtx_push (n, ETermClosed ty_n (TermClosed te_n)) comp ctx k =
 183         comp (TyCtxS n ty_n ctx) $ \ty_y (Term y) ->
 184         k ty_y $ Term $
 185          \c -> y (te_n `TeCtxS` c)
 186
 187 -- | Compile with given 'Compiler', closing the /lambda context/.
 188 compilerWithCtx_close
 189  :: (forall hs. Compiler src hs (ETermClosed src cs is) cs is '[] is)
 190  -> Either (Error_Term src cs is) (ETermClosed src cs is)
 191 compilerWithCtx_close comp =
 192         comp TyCtxZ $ \typ (Term te) ->
 193         Right $ ETermClosed typ $ TermClosed $ te TeCtxZ
 194
 195 -- ** Class 'CompileR'
 196 -- | Intermediate type class to construct an instance of 'Compile'
 197 -- from many instances of 'CompileI', one for each item of @is@.
 198 --
 199 -- * @is@: starting  list of /interfaces/.
 200 -- * @ls@: done      list of /interfaces/.
 201 -- * @rs@: remaining list of /interfaces/.
 202 class CompileR (cs::[*]) (is::[*]) (ls::[*]) (rs::[*]) where
 203         compileR :: TokenR src is rs i
 204                  -> Maybe (AST_Term src is)
 205                  -> Compiler src hs ret cs is ls rs
 206
 207 -- | Recurse into into the given 'TokenR'
 208 -- to call the 'compileI' instance associated
 209 -- to the 'TokenT' it contains.
 210 instance
 211  ( CompileI cs is i
 212  , CompileR cs is (i ': ls) (r ': rs)
 213  ) => CompileR cs is ls (i ': r ': rs) where
 214         compileR tok arg ctx k =
 215                 case tok of
 216                  TokenZ _src t -> compileI t arg ctx k
 217                  TokenS t ->
 218                         compileR t arg ctx $ \typ (Term te :: Term hs h is (i ': ls) (r ': rs)) ->
 219                                 k typ (Term te :: Term hs h is ls (i ': r ': rs))
 220 -- | End the recursion.
 221 instance
 222  CompileI cs is i =>
 223  CompileR cs is ls (i ': '[]) where
 224         compileR (TokenZ _src t) arg  ctx  k = compileI t arg ctx k
 225         compileR TokenS{}        arg _ctx _k = error "Oops, the impossible happened..."
 226
 227 -- ** Class 'CompileI'
 228 -- | Handle the work of 'Compile' for a given /interface/ @i@.
 229 class CompileI (cs::[*]) (is::[*]) (i:: *) where
 230         compileI :: TokenT src is i
 231                  -> Maybe (AST_Term src is)
 232                  -> Compiler src hs ret cs is ls (i ': rs)
 233
 234 -- * Type family 'Sym_of_Ifaces'
 235 type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
 236         Sym_of_Ifaces '[] term = ()
 237         Sym_of_Ifaces (i ': is) term = (Sym_of_Iface i term, Sym_of_Ifaces is term)
 238
 239 -- ** Type family 'Sym_of_Iface'
 240 type family Sym_of_Iface (i:: *) :: {-term-}(* -> *) -> Constraint
 241
 242 -- * Type 'TyConsts_of_Ifaces'
 243 type TyConsts_of_Ifaces is = Nub (TyConsts_of_IfacesR is)
 244
 245 -- ** Type family 'TyConsts_of_IfacesR'
 246 type family TyConsts_of_IfacesR (is::[*]) where
 247         TyConsts_of_IfacesR '[]       = '[]
 248         TyConsts_of_IfacesR (i ': is) = TyConsts_of_Iface i ++ TyConsts_of_IfacesR is
 249
 250 {- NOTE: failed attempt to recursively collect TyConsts.
 251 -- ** Type family 'TyConsts_imported_byR'
 252 type family TyConsts_imported_byR (done::[*]) (cs::[*]) where
 253         TyConsts_imported_byR done '[] = done
 254         TyConsts_imported_byR done (c ': cs) =
 255                 If (Exists c done)
 256                  (TyConsts_imported_byR done cs)
 257                  (TyConsts_imported_byR (c ': done) (TyConsts_imported_by c ++ TyConsts_imported_byR done cs))
 258 -}
 259
 260 -- ** Type family 'TyConsts_of_Iface'
 261 type family TyConsts_of_Iface (i:: *) :: [*]
 262
 263 -- ** Type family 'TyConsts_imported_by'
 264 -- | Return the /type constant/s that a given /type constant/
 265 -- wants to be part of the final list of /type constants/.
 266 type family TyConsts_imported_by (c:: *) :: [*]
 267
 268 -- * Type 'TyCtx'
 269 -- | GADT for a /typing context/:
 270 -- accumulating at each /lambda abstraction/
 271 -- the 'Type' of the introduced variable.
 272 data TyCtx (name:: *) (cs::[*]) (hs::[*]) where
 273         TyCtxZ :: TyCtx name cs '[]
 274         TyCtxS :: name
 275                -> Type src cs h
 276                -> TyCtx name cs hs
 277                -> TyCtx name cs (h ': hs)
 278 infixr 5 `TyCtxS`
 279
 280 appendTyCtx
 281  :: TyCtx TeName cs hs0
 282  -> TyCtx TeName cs hs1
 283  -> TyCtx TeName cs (hs0 ++ hs1)
 284 appendTyCtx TyCtxZ c          = c
 285 appendTyCtx (TyCtxS n t c) c' = TyCtxS n t $ appendTyCtx c c'
 286
 287 -- * Type 'TeCtx'
 288 -- | GADT for an /interpreting context/:
 289 -- accumulating at each /lambda abstraction/
 290 -- the @term@ of the introduced variable.
 291 data TeCtx (term:: * -> *) (hs::[*]) where
 292         TeCtxZ :: TeCtx term '[]
 293         TeCtxS :: term h
 294                -> TeCtx term hs
 295                -> TeCtx term (h ': hs)
 296 infixr 5 `TeCtxS`
 297
 298 -- * Type 'Error_Term'
 299 data Error_Term src (cs::[*]) (is::[*])
 300  =   Error_Term_unbound TeName
 301  |   Error_Term_Typing (Error_Type src)
 302  |   Error_Term_Con_Type (Con_Type src cs)
 303  {- |   Error_Term_Con_Kind (Con_Kind src) -}
 304 deriving instance (Eq src, Eq_Token src is, Inj_Source (EType src cs) src) => Eq (Error_Term src cs is)
 305 deriving instance (Show src, Show_Token src is, Show_TyConst cs) => Show (Error_Term src cs is)
 306
 307 -- * Type 'Con_Type'
 308 data Con_Type src cs
 309  =   Con_TyEq  (EType src cs) (EType src cs)
 310  |   Con_TyApp (EType src cs)
 311  |   Con_TyCon (KType src cs Constraint)
 312  |   Con_TyFam (At src TyFamName) [EType src cs]
 313 deriving instance
 314  ( Eq src
 315  , Inj_Source (EType src cs) src
 316  ) => Eq (Con_Type src cs)
 317 deriving instance
 318  ( Show src
 319  , Show_TyConst cs
 320  ) => Show (Con_Type src cs)
 321
 322 instance Inj_Error (Error_Type src) (Error_Term src cs ts) where
 323         inj_Error = Error_Term_Typing . inj_Error
 324 instance Inj_Error (Error_Term src cs ts) (Error_Term src cs ts) where
 325         inj_Error = id
 326 instance Inj_Error (Con_Type src cs) (Error_Term src cs is) where
 327         inj_Error = Error_Term_Con_Type
 328 instance Inj_Error (Con_Kind src) (Error_Term src cs is) where
 329         inj_Error = Error_Term_Typing . Error_Type_Con_Kind
 330
 331 -- ** Checks
 332
 333 check_TyEq
 334  :: ( Inj_Error (Con_Type src cs) err
 335     , Inj_Source (EType src cs) src )
 336  => Type src cs x
 337  -> Type src cs y
 338  -> ((x :~: y) -> Either err ret) -> Either err ret
 339 check_TyEq x y k =
 340         case x `eq_Type` y of
 341          Just Refl -> k Refl
 342          Nothing -> Left $ inj_Error $
 343                 Con_TyEq (EType x) (EType y)
 344
 345 check_TyApp
 346  :: ( Inj_Error (Con_Type src cs) err
 347     , Inj_Source (EType src cs) src )
 348  => Type src cs (fa::kfa)
 349  -> (forall ka f a. (fa :~: f a)
 350   -> Type src cs (f::ka -> kfa)
 351   -> Type src cs (a::ka)
 352   -> Either err ret)
 353  -> Either err ret
 354 check_TyApp typ k =
 355         case typ of
 356          TyApp _src a b -> k Refl (a `source` EType typ) (b `source` EType typ)
 357          _ -> Left $ inj_Error $ Con_TyApp (EType typ)
 358
 359 check_TyEq1
 360  :: ( Inj_Error (Con_Type src cs) err
 361     , Inj_Error (Con_Kind src) err
 362     , Inj_Source (EType src cs) src
 363     )
 364  => Type src cs (f:: * -> *)
 365  -> Type src cs fa
 366  -> (forall a. (fa :~: f a)
 367   -> Type src cs a
 368   -> Either err ret)
 369  -> Either err ret
 370 check_TyEq1 typ ty_fa k =
 371         check_TyApp ty_fa $ \Refl ty_f ty_a ->
 372         check_Kind
 373          (kind @(K.Type -> K.Type))
 374          (kind_of ty_f) $ \Refl ->
 375         check_TyEq typ ty_f $ \Refl ->
 376         k Refl ty_a
 377
 378 check_TyEq2
 379  :: ( Inj_Error (Con_Type src cs) err
 380     , Inj_Error (Con_Kind src) err
 381     , Inj_Source (EType src cs) src )
 382  => Type src cs (f:: * -> * -> *)
 383  -> Type src cs fab
 384  -> (forall a b. (fab :~: f a b)
 385   -> Type src cs a
 386   -> Type src cs b
 387   -> Either err ret)
 388  -> Either err ret
 389 check_TyEq2 typ ty_fab k =
 390         check_TyApp ty_fab  $ \Refl ty_fa ty_b ->
 391         check_TyApp ty_fa $ \Refl ty_f ty_a ->
 392         check_Kind
 393          (kind @(K.Type -> K.Type -> K.Type))
 394          (kind_of ty_f) $ \Refl ->
 395         check_TyEq typ ty_f $ \Refl ->
 396         k Refl ty_a ty_b
 397
 398 check_TyCon
 399  :: ( Proj_TyCon cs
 400     , Inj_Error (Con_Type src cs) err
 401     , Inj_Source (EType src cs) src )
 402  => Type src cs (q::Constraint)
 403  -> (TyCon q -> Either err ret)
 404  -> Either err ret
 405 check_TyCon typ k =
 406         case proj_TyCon typ of
 407          Just Dict -> k Dict
 408          Nothing -> Left $ inj_Error $ Con_TyCon (KType typ)
 409
 410 check_TyCon1
 411  :: ( Proj_TyCon cs
 412     , Inj_Error (Con_Type src cs) err
 413     , Inj_Error (Con_Kind src) err
 414     , Inj_Source (EType src cs) src )
 415  => Type src cs con
 416  -> Type src cs (fa:: *)
 417  -> (forall f a. (fa :~: f a)
 418   -> TyCon (con f)
 419   -> Type src cs (f:: * -> *)
 420   -> Type src cs (a:: *)
 421   -> Either err ret)
 422  -> Either err ret
 423 check_TyCon1 con ty_fa k =
 424         check_TyApp ty_fa $ \Refl ty_f ty_a ->
 425         check_Kind
 426          (kind @(K.Type -> K.Type))
 427          (kind_of ty_f) $ \Refl ->
 428         check_TyCon (TyApp sourceLess con ty_f) $ \Dict ->
 429         k Refl Dict ty_f ty_a
 430
 431 check_TyFam
 432  :: ( Inj_Error (Con_Type src cs) err
 433     , Proj_TyFam cs fam
 434     , Show fam )
 435  => At src fam
 436  -> Types src cs hs
 437  -> (Type src cs (TyFam fam hs) -> Either err ret)
 438  -> Either err ret
 439 check_TyFam fam tys k =
 440         case proj_TyFam (unAt fam) tys of
 441          Just t -> k t
 442          Nothing -> Left $ inj_Error $
 443                 Con_TyFam
 444                  (Text.pack . show <$> fam)
 445                  (eTypes tys)