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