+{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
-{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-module Language.Symantic.Compiling.Term
- ( module Language.Symantic.Compiling.Term
- , module Language.Symantic.Compiling.Term.Grammar
- ) where
+module Language.Symantic.Compiling.Term where
-import qualified Data.Kind as Kind
-import Data.Proxy (Proxy(..))
+import Data.Maybe (isJust)
+import Data.Semigroup (Semigroup(..))
+import qualified Data.Kind as K
+import qualified Data.Set as Set
import qualified Data.Text as Text
-import Data.Type.Equality ((:~:)(..))
-import GHC.Exts (Constraint)
-import Language.Symantic.Helper.Data.Type.List
-import Language.Symantic.Parsing
+import Language.Symantic.Grammar
+import Language.Symantic.Interpreting
+import Language.Symantic.Transforming.Trans
import Language.Symantic.Typing
-import Language.Symantic.Compiling.Term.Grammar
-
-- * Type 'Term'
--- | Closed 'TermO'.
-data Term is h
- = Term
- (forall term. ( Sym_of_Ifaces is term
- , Sym_of_Iface (Proxy (->)) term
- ) => term h)
-
--- ** Type 'TermO'
--- | An open term (i.e. with a /lambda context/).
--- The data type wraps a universal quantification
--- over an interpreter @term@
--- qualified by the symantics of a term.
---
--- Moreover the term is abstracted by a 'LamCtx_Term'
--- built top-down by 'compileO',
--- to enable a /Higher-Order Abstract Syntax/ (HOAS)
--- for /lambda abstractions/ ('lam').
---
--- This data type is used to keep a parsed term polymorphic enough
--- to stay interpretable by different interpreters.
---
--- * @(@'Sym_of_Ifaces'@ is term)@
--- is needed when a symantic method includes a polymorphic type
--- and thus calls: 'compileO'.
---
--- * @(@'Sym_of_Ifaces'@ ls term)@ and @(@'Sym_of_Ifaces'@ rs term)@
--- make a zipper needed to be able to write the recursing 'CompileR' instance.
---
--- * @(@'Sym_of_Iface'@ (@'Proxy'@ (->)) term)@
--- is needed to handle partially applied functions.
-data TermO ctx h is ls rs
- = TermO
- (forall term. ( Sym_of_Ifaces is term
- , Sym_of_Ifaces ls term
- , Sym_of_Ifaces rs term
- , Sym_of_Iface (Proxy (->)) term
- ) => LamCtx_Term term ctx -> term h)
-
--- * Type 'ETerm'
--- | Existential 'Term', with its 'Type'.
-data ETerm is
- = forall (h::Kind.Type). ETerm
- (Type (TyConsts_of_Ifaces is) h)
- (Term is h)
+data Term src ss ts vs (t::K.Type)
+ = Term (Type src vs (QualOf t))
+ (Type src vs (UnQualOf t))
+ (TeSym ss ts t)
+instance Source src => Eq (Term src ss ts vs t) where
+ Term qx tx _ == Term qy ty _ = qx == qy && tx == ty
+instance Source src => Show (Term src ss ts vs t) where
+ showsPrec p (Term q t _te) = showsPrec p (q #> t)
--- * Type 'Compile'
--- | Convenient type synonym wrapping 'CompileR' to initiate its recursion.
-class Compile is where
- compileO :: EToken meta is -> CompileT meta ctx ret is '[] is
-instance CompileR is '[] is => Compile is where
- compileO (EToken tok) = compileR tok
+-- Source
+type instance SourceOf (Term src ss ts vs t) = src
+instance Source src => Sourced (Term src ss ts vs t) where
+ sourceOf (Term _q t _te) = sourceOf t
+ setSource (Term q t te) src = Term q (setSource t src) te
--- | Like 'compileO' but for a term with an empty /lambda context/.
-compile
- :: Compile is
- => EToken meta is
- -> Either (Error_Term meta is) (ETerm is)
-compile tok =
- compileO tok LamCtx_TypeZ $ \typ (TermO te) ->
- Right $ ETerm typ $ Term $ te LamCtx_TermZ
+-- Const
+instance ConstsOf (Term src ss ts vs t) where
+ constsOf (Term q t _te) = constsOf q `Set.union` constsOf t
--- ** Type 'CompileT'
--- | Convenient type synonym defining a term parser.
-type CompileT meta ctx ret is ls rs
- = LamCtx_Type is Term_Name ctx
- -- ^ The bound variables in scope and their types:
- -- built top-down in the heterogeneous list @ctx@,
- -- from the closest including /lambda abstraction/ to the farest.
- -> ( forall h.
- Type (TyConsts_of_Ifaces is) (h::Kind.Type)
- -> TermO ctx h is ls rs
- -> Either (Error_Term meta is) ret )
- -- ^ The accumulating continuation called bottom-up.
- -> Either (Error_Term meta is) ret
+-- Var
+type instance VarsOf (Term src ss ts vs t) = vs
+instance LenVars (Term src ss ts vs t) where
+ lenVars (Term _q t _te) = lenVars t
+instance AllocVars (Term src ss ts) where
+ allocVarsL len (Term q t te) = Term (allocVarsL len q) (allocVarsL len t) te
+ allocVarsR len (Term q t te) = Term (allocVarsR len q) (allocVarsR len t) te
--- ** Class 'CompileR'
--- | Intermediate type class to construct an instance of 'Compile'
--- from many instances of 'CompileI', one for each item of @is@.
---
--- * @is@: starting list of /term constants/.
--- * @ls@: done list of /term constants/.
--- * @rs@: remaining list of /term constants/.
-class CompileR (is::[*]) (ls::[*]) (rs::[*]) where
- compileR :: TokenR meta is rs i -> CompileT meta ctx ret is ls rs
+-- Fam
+instance ExpandFam (Term src ss ts vs t) where
+ expandFam (Term q t te) = Term (expandFam q) (expandFam t) te
--- | Recurse into into the given 'TokenR'
--- to call the 'compileI' instance associated
--- to the 'TokenT' it contains.
-instance
- ( CompileI is i
- , CompileR is (i ': ls) (r ': rs)
- ) => CompileR is ls (i ': r ': rs) where
- compileR tok ctx k =
- case tok of
- TokenZ _m t -> compileI t ctx k
- TokenS t ->
- compileR t ctx $ \typ (TermO te :: TermO ctx h is (i ': ls) (r ': rs)) ->
- k typ (TermO te :: TermO ctx h is ls (i ': r ': rs))
--- | End the recursion.
-instance
- CompileI is i =>
- CompileR is ls (i ': '[]) where
- compileR (TokenZ _m t) ctx k = compileI t ctx k
- compileR TokenS{} _ctx _k = error "Oops, the impossible happened..."
+-- ** Type 'TermT'
+-- | 'Term' with existentialized 'Type'.
+data TermT src ss ts vs = forall t. TermT (Term src ss ts vs t)
+instance Source src => Show (TermT src ss ts vs) where
+ showsPrec p (TermT t) = showsPrec p t
--- ** Class 'CompileI'
--- | Handle the work of 'Compile' for a given /interface/ @i@.
-class CompileI (is::[*]) (i:: *) where
- compileI :: TokenT meta is i -> CompileT meta ctx ret is ls (i ': rs)
+-- ** Type 'TermVT'
+-- | 'Term' with existentialized 'Var's and 'Type'.
+data TermVT src ss ts = forall vs t. TermVT (Term src ss ts vs t)
+instance Source src => Eq (TermVT src ss ts) where
+ TermVT x == TermVT y =
+ let (Term qx' tx' _, Term qy' ty' _) = appendVars x y in
+ isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty')
+instance Source src => Show (TermVT src ss ts) where
+ showsPrec p (TermVT t) = showsPrec p t
+type instance SourceOf (TermVT src ss ts) = src
+instance Source src => Sourced (TermVT src ss ts) where
+ sourceOf (TermVT t) = sourceOf t
+ setSource (TermVT t) src = TermVT $ setSource t src
--- * Type family 'Sym_of_Ifaces'
-type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
- Sym_of_Ifaces '[] term = ()
- Sym_of_Ifaces (i ': is) term = (Sym_of_Iface i term, Sym_of_Ifaces is term)
+liftTermVT :: TermVT src ss '[] -> TermVT src ss ts
+liftTermVT (TermVT (Term q t (TeSym te))) =
+ TermVT $ Term @_ @_ @_ @_ @(_ #> _) q t $
+ TeSym $ \_c -> te CtxTeZ
--- ** Type family 'Sym_of_Iface'
-type family Sym_of_Iface (i:: *) :: {-term-}(* -> *) -> Constraint
+-- ** Type 'TermAVT'
+-- | Like 'TermVT', but 'CtxTe'-free.
+data TermAVT src ss = forall vs t. TermAVT (forall ts. Term src ss ts vs t)
+type instance SourceOf (TermAVT src ss) = src
+instance Source src => Sourced (TermAVT src ss) where
+ sourceOf (TermAVT t) = sourceOf t
+ setSource (TermAVT t) src = TermAVT (setSource t src)
+instance Source src => Eq (TermAVT src ss) where
+ TermAVT x == TermAVT y =
+ let (Term qx' tx' _, Term qy' ty' _) = appendVars x y in
+ isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty')
+instance Source src => Show (TermAVT src ss) where
+ showsPrec p (TermAVT t) = showsPrec p t
--- * Type 'TyConsts_of_Ifaces'
-type TyConsts_of_Ifaces is = Nub (TyConsts_of_IfaceR is)
+-- * Type 'TeSym'
+-- | Symantic of a 'Term'.
+newtype TeSym ss ts (t::K.Type)
+ = TeSym
+ ( forall term.
+ Syms ss term =>
+ Sym_Lambda term =>
+ QualOf t =>
+ CtxTe term ts -> term (UnQualOf t)
+ )
--- ** Type family 'TyConsts_of_IfaceR'
-type family TyConsts_of_IfaceR (is::[*]) where
- TyConsts_of_IfaceR '[] = '[]
- TyConsts_of_IfaceR (i ': is) = TyConsts_of_Iface i ++ TyConsts_of_IfaceR is
+-- | Like 'TeSym', but 'CtxTe'-free
+-- and using 'inj_Sym' to be able to use 'Sym'@ (@'Proxy'@ s)@ inside.
+teSym ::
+ forall s ss ts t.
+ Inj_Sym ss s =>
+ (forall term. Sym (Proxy s) term => Sym_Lambda term => QualOf t => term (UnQualOf t)) ->
+ TeSym ss ts t
+teSym t = inj_Sym @s (TeSym $ const t)
--- ** Type family 'TyConsts_of_Iface'
-type family TyConsts_of_Iface (i:: *) :: [*]
-type instance TyConsts_of_Iface (Proxy Enum) = Proxy Enum ': TyConsts_imported_by Enum
+-- ** Type family 'QualOf'
+-- | Qualification
+type family QualOf (t::K.Type) :: Constraint where
+ QualOf (q #> t) = q -- (q # QualOf t)
+ QualOf t = (()::Constraint)
--- * Type 'LamCtx_Type'
--- | GADT for a typing context,
--- accumulating an @item@ at each lambda;
--- used to accumulate object-types (in 'Expr_From')
--- or host-terms (in 'HostI')
--- associated with the 'LamVar's in scope.
-data LamCtx_Type (is::[*]) (name:: *) (ctx::[*]) where
- LamCtx_TypeZ :: LamCtx_Type is name '[]
- LamCtx_TypeS :: name
- -> Type (TyConsts_of_Ifaces is) (h::Kind.Type)
- -> LamCtx_Type is name hs
- -> LamCtx_Type is name (h ': hs)
-infixr 5 `LamCtx_TypeS`
+-- ** Type family 'UnQualOf'
+-- | Unqualification
+type family UnQualOf (t::K.Type) :: K.Type where
+ UnQualOf (q #> t) = t -- UnQualOf t
+ UnQualOf t = t
--- * Type 'LamCtx_Term'
-data LamCtx_Term (term:: * -> *) (ctx::[*]) where
- LamCtx_TermZ :: LamCtx_Term term '[]
- LamCtx_TermS :: term h
- -> LamCtx_Term term hs
- -> LamCtx_Term term (h ': hs)
-infixr 5 `LamCtx_TermS`
+-- | Return 'K.Constraint' and 'K.Type' part of given 'Type'.
+unQualTy ::
+ Source src =>
+ Type src vs (t::K.Type) ->
+ ( TypeK src vs K.Constraint
+ , TypeK src vs K.Type )
+unQualTy (TyApp _ (TyApp _ c q) t)
+ | Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) c
+ = (TypeK q, TypeK t)
+unQualTy t = (TypeK $ noConstraintLen (lenVars t), TypeK t)
--- * Type 'Error_Term'
-data Error_Term meta (is::[*])
- = Error_Term_unbound Term_Name
- | Error_Term_Typing (Error_Type meta '[Proxy Token_Type])
- | Error_Term_Con_Type
- (Either
- (Con_Type meta '[Proxy Token_Type] (TyConsts_of_Ifaces is))
- (Con_Type meta is (TyConsts_of_Ifaces is)))
- | Error_Term_Con_Kind (Con_Kind meta is)
-deriving instance (Eq meta, Eq_Token meta is) => Eq (Error_Term meta is)
-deriving instance (Show meta, Show_Token meta is, Show_TyConst (TyConsts_of_Ifaces is)) => Show (Error_Term meta is)
+-- | Remove 'K.Constraint's from given 'Type'.
+unQualsTy :: Source src => Type src vs (t::kt) -> TypeK src vs kt
+unQualsTy (TyApp _ (TyApp _ c _q) t)
+ | Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) c
+ = unQualsTy t
+unQualsTy (TyApp src f a)
+ | TypeK f' <- unQualsTy f
+ , TypeK a' <- unQualsTy a
+ = TypeK $ TyApp src f' a'
+unQualsTy t = TypeK t
--- * Type 'Con_Type'
-data Con_Type meta ts cs
- = Con_TyEq (Either (At meta '[Proxy Token_Type] (EType cs))
- (At meta ts (EType cs)))
- (At meta ts (EType cs))
- | Con_TyApp (At meta ts (EType cs))
- | Con_TyCon (At meta ts (KType cs Constraint))
- | Con_TyFam (At meta ts TyFamName) [EType cs]
-deriving instance
- ( Eq meta
- , Eq_Token meta ts
- ) => Eq (Con_Type meta ts cs)
-deriving instance
- ( Show meta
- , Show_Token meta ts
- , Show_TyConst cs
- ) => Show (Con_Type meta ts cs)
+-- * Type 'CtxTe'
+-- | GADT for an /interpreting context/:
+-- accumulating at each /lambda abstraction/
+-- the @term@ of the introduced variable.
+data CtxTe (term::K.Type -> K.Type) (hs::[K.Type]) where
+ CtxTeZ :: CtxTe term '[]
+ CtxTeS :: term t
+ -> CtxTe term ts
+ -> CtxTe term (t ': ts)
+infixr 5 `CtxTeS`
-instance MonoLift (Error_Type meta '[Proxy Token_Type]) (Error_Term meta ts) where
- olift = Error_Term_Typing . olift
-instance MonoLift (Error_Term meta ts) (Error_Term meta ts) where
- olift = Prelude.id
-instance
- cs ~ TyConsts_of_Ifaces is =>
- MonoLift (Con_Type meta is cs) (Error_Term meta is) where
- olift = Error_Term_Con_Type . Right
-instance
- cs ~ TyConsts_of_Ifaces is =>
- MonoLift (Con_Type meta '[Proxy Token_Type] cs) (Error_Term meta is) where
- olift = Error_Term_Con_Type . Left
-instance MonoLift (Con_Kind meta '[Proxy Token_Type]) (Error_Term meta is) where
- olift = Error_Term_Typing . Error_Type_Con_Kind
-instance MonoLift (Con_Kind meta is) (Error_Term meta is) where
- olift = Error_Term_Con_Kind
+-- ** Type 'TermDef'
+-- | Convenient type alias for defining 'Term'.
+type TermDef s vs t = forall src ss ts. Source src => Inj_Sym ss s => Term src ss ts vs t
--- ** Checks
-check_TyEq
- :: MonoLift (Con_Type meta ts cs) err
- => At meta ts (Type cs x)
- -> At meta ts (Type cs y)
- -> ((x :~: y) -> Either err ret) -> Either err ret
-check_TyEq x y k =
- case unAt x `eq_Type` unAt y of
- Just Refl -> k Refl
- Nothing -> Left $ olift $
- Con_TyEq (Right $ EType <$> x) (EType <$> y)
+-- ** Type family 'Sym'
+type family Sym (s::K.Type) :: {-term-}(K.Type -> K.Type) -> Constraint
-check_Type_is
- :: MonoLift (Con_Type meta ts cs) err
- => At meta '[Proxy Token_Type] (Type cs x)
- -> At meta ts (Type cs y)
- -> ((x :~: y) -> Either err ret) -> Either err ret
-check_Type_is x y k =
- case unAt x `eq_Type` unAt y of
- Just Refl -> k Refl
- Nothing -> Left $ olift $
- Con_TyEq (Left $ EType <$> x) (EType <$> y)
+-- ** Type family 'Syms'
+type family Syms (ss::[K.Type]) (term:: K.Type -> K.Type) :: Constraint where
+ Syms '[] term = ()
+ Syms (s ': ss) term = (Sym s term, Syms ss term)
-check_TyApp
- :: MonoLift (Con_Type meta ts cs) err
- => At meta ts (Type cs (fa::kfa))
- -> (forall ka f a. (fa :~: f a)
- -> Type cs (f::ka -> kfa)
- -> Type cs (a::ka)
- -> Either err ret)
- -> Either err ret
-check_TyApp typ k =
- case unAt typ of
- a :$ b -> k Refl a b
- _ -> Left $ olift $
- Con_TyApp (EType <$> typ)
+-- ** Type 'Inj_Sym'
+-- | Convenient type synonym wrapping 'Inj_SymP'
+-- applied on the correct 'Index'.
+type Inj_Sym ss s = Inj_SymP (Index ss (Proxy s)) ss s
-check_TyEq1
- :: ( MonoLift (Con_Type meta ts cs) err
- , MonoLift (Con_Kind meta ts) err )
- => Type cs (f:: * -> *)
- -> At meta ts (Type cs fa)
- -> (forall a. (fa :~: f a)
- -> Type cs a
- -> Either err ret)
- -> Either err ret
-check_TyEq1 typ ty_fa k =
- check_TyApp ty_fa $ \Refl ty_f ty_a ->
- check_Kind
- (At Nothing $ SKiType `SKiArrow` SKiType)
- (kind_of ty_f <$ ty_fa) $ \Refl ->
- check_TyEq
- (At Nothing typ)
- (ty_f <$ ty_fa) $ \Refl ->
- k Refl ty_a
+-- | Inject a given /symantic/ @s@ into a list of them,
+-- by returning a function which given a 'TeSym' on @s@
+-- returns the same 'TeSym' on @ss@.
+inj_Sym ::
+ forall s ss ts t.
+ Inj_Sym ss s =>
+ TeSym '[Proxy s] ts t ->
+ TeSym ss ts t
+inj_Sym = inj_SymP (Proxy @(Index ss (Proxy s)))
-check_TyEq2
- :: ( MonoLift (Con_Type meta ts cs) err
- , MonoLift (Con_Kind meta ts) err )
- => Type cs (f:: * -> * -> *)
- -> At meta ts (Type cs fab)
- -> (forall a b. (fab :~: f a b)
- -> Type cs a
- -> Type cs b
- -> Either err ret)
- -> Either err ret
-check_TyEq2 typ ty_fab k =
- check_TyApp ty_fab $ \Refl ty_fa ty_b ->
- check_TyApp (ty_fa <$ ty_fab) $ \Refl ty_f ty_a ->
- check_Kind
- (At Nothing $ SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
- (kind_of ty_f <$ ty_fab) $ \Refl ->
- check_TyEq
- (At Nothing typ)
- (ty_f <$ ty_fab) $ \Refl ->
- k Refl ty_a ty_b
+-- *** Class 'Inj_SymP'
+class Inj_SymP p ss s where
+ inj_SymP :: Proxy p -> TeSym '[Proxy s] ts t -> TeSym ss ts t
+instance Inj_SymP Zero (Proxy s ': ss) (s::k) where
+ inj_SymP _ = \(TeSym te) -> TeSym te
+instance Inj_SymP p ss s => Inj_SymP (Succ p) (not_s ': ss) s where
+ inj_SymP _p = \(te::TeSym '[Proxy s] ts t) ->
+ case inj_SymP (Proxy @p) te :: TeSym ss ts t of
+ TeSym te' -> TeSym te'
-check_TyCon
- :: ( Proj_TyCon cs
- , MonoLift (Con_Type meta ts cs) err )
- => At meta ts (Type cs (q::Constraint))
- -> (TyCon q -> Either err ret)
- -> Either err ret
-check_TyCon typ k =
- case proj_TyCon $ unAt typ of
- Just TyCon -> k TyCon
- Nothing -> Left $ olift $
- Con_TyCon (KType <$> typ)
+-- * Class 'Sym_Lambda'
+class Sym_Lambda term where
+ -- | /Function application/.
+ apply :: term ((a -> b) -> a -> b)
+ default apply :: Sym_Lambda (UnT term) => Trans term => term ((a -> b) -> a -> b)
+ apply = trans apply
+
+ -- | /Lambda application/.
+ app :: term (a -> b) -> (term a -> term b); infixr 0 `app`
+ default app :: Sym_Lambda (UnT term) => Trans term => term (arg -> res) -> term arg -> term res
+ app = trans2 app
+
+ -- | /Lambda abstraction/.
+ lam :: (term a -> term b) -> term (a -> b)
+ default lam :: Sym_Lambda (UnT term) => Trans term => (term arg -> term res) -> term (arg -> res)
+ lam f = trans $ lam (unTrans . f . trans)
+
+ -- | Convenient 'lam' and 'app' wrapper.
+ let_ :: term var -> (term var -> term res) -> term res
+ let_ x f = lam f `app` x
+
+ -- | /Lambda abstraction/ beta-reducable without duplication
+ -- (i.e. whose variable is used once at most),
+ -- mainly useful in compiled 'Term's
+ -- whose symantics are not a single 'term'
+ -- but a function between 'term's,
+ -- which happens because those are more usable when used as an embedded DSL.
+ lam1 :: (term a -> term b) -> term (a -> b)
+ default lam1 :: Sym_Lambda (UnT term) => Trans term => (term a -> term b) -> term (a -> b)
+ lam1 = lam
+
+ -- | /Qualification/.
+ --
+ -- Workaround used in 'readTermWithCtx'.
+ qual :: proxy q -> term t -> term (q #> t)
+ default qual :: Sym_Lambda (UnT term) => Trans term => proxy q -> term t -> term (q #> t)
+ qual q = trans1 (qual q)
-check_TyCon1
- :: ( Proj_TyCon cs
- , MonoLift (Con_Type meta ts cs) err
- , MonoLift (Con_Kind meta ts) err )
- => Type cs con
- -> At meta ts (Type cs (fa:: *))
- -> (forall f a. (fa :~: f a)
- -> TyCon (con f)
- -> Type cs (f:: * -> *)
- -> Type cs (a:: *)
- -> Either err ret)
- -> Either err ret
-check_TyCon1 con ty_fa k =
- check_TyApp ty_fa $ \Refl ty_f ty_a ->
- check_Kind
- (At Nothing (SKiType `SKiArrow` SKiType))
- (kind_of ty_f <$ ty_fa) $ \Refl ->
- check_TyCon ((con :$ ty_f) <$ ty_fa) $ \TyCon ->
- k Refl TyCon ty_f ty_a
+lam2 :: Sym_Lambda term => (term a -> term b -> term c) -> term (a -> b -> c)
+lam3 :: Sym_Lambda term => (term a -> term b -> term c -> term d) -> term (a -> b -> c -> d)
+lam4 :: Sym_Lambda term => (term a -> term b -> term c -> term d -> term e) -> term (a -> b -> c -> d -> e)
+lam2 f = lam1 $ lam1 . f
+lam3 f = lam1 $ lam2 . f
+lam4 f = lam1 $ lam3 . f
-check_TyFam
- :: ( MonoLift (Con_Type meta ts cs) err
- , Proj_TyFam cs fam
- , Show fam )
- => At meta ts fam
- -> Types cs hs
- -> (Type cs (TyFam fam hs) -> Either err ret)
- -> Either err ret
-check_TyFam fam tys k =
- case proj_TyFam (unAt fam) tys of
- Just t -> k t
- Nothing -> Left $ olift $
- Con_TyFam
- (Text.pack . show <$> fam)
- (eTypes tys)
+-- Interpreting
+instance Sym_Lambda Eval where
+ apply = Eval ($)
+ app = (<*>)
+ lam f = Eval (unEval . f . Eval)
+ lam1 = lam
+ qual _q (Eval t) = Eval $ Qual t
+ let_ x f = f x -- NOTE: like flip ($)
+instance Sym_Lambda View where
+ apply = View $ \_po _v -> "($)"
+ app (View a1) (View a2) = View $ \po v ->
+ parenInfix po op $
+ a1 (op, SideL) v <> " " <> a2 (op, SideR) v
+ where op = infixN 10
+ lam f = View $ \po v ->
+ let x = "x" <> Text.pack (show v) in
+ parenInfix po op $
+ "\\" <> x <> " -> " <>
+ unView (f (View $ \_po _v -> x)) (op, SideL) (succ v)
+ where op = infixN 1
+ lam1 = lam
+ qual _q (View t) = View t -- TODO: maybe print q
+ let_ x f =
+ View $ \po v ->
+ let x' = "x" <> Text.pack (show v) in
+ parenInfix po op $
+ "let" <> " " <> x' <> " = "
+ <> unView x (infixN 0, SideL) (succ v) <> " in "
+ <> unView (f (View $ \_po _v -> x')) (op, SideL) (succ v)
+ where op = infixN 1
+instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (Dup r1 r2) where
+ apply = dup0 @Sym_Lambda apply
+ app = dup2 @Sym_Lambda app
+ lam f = dup_1 lam_f `Dup` dup_2 lam_f
+ where lam_f = lam f
+ lam1 = lam
+ qual q = dup1 @Sym_Lambda (qual q)
sourcephile / git / haskell / symantic.git / blobdiff