import Language.Symantic.Typing
-- * Type 'Term'
-data Term src ss ts vs (t::K.Type)
- = Term (Type src vs (QualOf t::K.Constraint))
- (Type src vs (UnQualOf t::K.Type))
- (TeSym ss ts t)
+data Term src ss ts vs (t::K.Type) where
+ Term :: Type src vs q
+ -> Type src vs t
+ -> TeSym ss ts (q #> t)
+ -> Term src ss ts vs (q #> 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
instance ExpandFam (Term src ss ts vs t) where
expandFam (Term q t te) = Term (expandFam q) (expandFam t) te
+-- Type
+instance SourceInj (TermT src ss ts vs) src => TypeOf (Term src ss ts vs) where
+ typeOf t = typeOfTerm t `withSource` TermT t
+
+typeOfTerm :: Source src => Term src ss ts vs t -> Type src vs t
+typeOfTerm (Term q t _) = q #> t
+
-- ** Type 'TermT'
-- | 'Term' with existentialized 'Type'.
data TermT src ss ts vs = forall t. TermT (Term src ss ts vs t)
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') `eqTyKi` (qy' #> ty')
+ case appendVars x y of
+ (Term qx' tx' _, Term qy' ty' _) ->
+ 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
+
+liftTermVT :: TermVT src ss '[] -> TermVT src ss ts
+liftTermVT (TermVT (Term q t (TeSym te))) =
+ TermVT $ Term q t $
+ TeSym $ \_c -> te CtxTeZ
--- ** Type 'TermVT_CF'
+-- ** Type 'TermAVT'
-- | Like 'TermVT', but 'CtxTe'-free.
-data TermVT_CF src ss = forall vs t. TermVT_CF (forall ts. Term src ss ts vs t)
-type instance SourceOf (TermVT_CF src ss) = src
-instance Source src => Sourced (TermVT_CF src ss) where
- sourceOf (TermVT_CF t) = sourceOf t
- setSource (TermVT_CF t) src = TermVT_CF (setSource t src)
-instance Source src => Eq (TermVT_CF src ss) where
- TermVT_CF x == TermVT_CF y =
- let (Term qx' tx' _, Term qy' ty' _) = appendVars x y in
- isJust $ (qx' #> tx') `eqTyKi` (qy' #> ty')
-instance Source src => Show (TermVT_CF src ss) where
- showsPrec p (TermVT_CF t) = showsPrec p t
+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 =
+ case appendVars x y of
+ (Term qx' tx' _, Term qy' ty' _) ->
+ isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty')
+instance Source src => Show (TermAVT src ss) where
+ showsPrec p (TermAVT t) = showsPrec p t
-- * Type 'TeSym'
-- | Symantic of a 'Term'.
)
-- | Like 'TeSym', but 'CtxTe'-free
--- and using 'inj_Sym' to be able to use 'Sym'@ (@'Proxy'@ s)@ inside.
+-- and using 'symInj' to be able to use 'Sym'@ 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)) ->
+ SymInj ss s =>
+ (forall term. Sym s term => Sym_Lambda term => QualOf t => term (UnQualOf t)) ->
TeSym ss ts t
-teSym t = inj_Sym @s (TeSym $ const t)
+teSym t = symInj @s (TeSym $ const t)
-- ** Type family 'QualOf'
+-- | Qualification
type family QualOf (t::K.Type) :: Constraint where
QualOf (q #> t) = q -- (q # QualOf t)
QualOf t = (()::Constraint)
-- ** Type family 'UnQualOf'
+-- | Unqualification
type family UnQualOf (t::K.Type) :: K.Type where
UnQualOf (q #> t) = t -- UnQualOf t
UnQualOf t = t
infixr 5 `CtxTeS`
-- ** 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
+-- | Convenient type alias to define a 'Term'.
+type TermDef s vs t = forall src ss ts. Source src => SymInj ss s => Term src ss ts vs t
-- ** Type family 'Sym'
-type family Sym (s::K.Type) :: {-term-}(K.Type -> K.Type) -> Constraint
+type family Sym (s::k) :: {-term-}(K.Type -> K.Type) -> Constraint
-- ** Type family 'Syms'
-type family Syms (ss::[K.Type]) (term:: K.Type -> K.Type) :: Constraint where
+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)
+ Syms (Proxy s ': ss) term = (Sym s term, Syms ss term)
--- ** Type 'Inj_Sym'
--- | Convenient type synonym wrapping 'Inj_SymP'
+-- ** Type 'SymInj'
+-- | Convenient type synonym wrapping 'SymPInj'
-- applied on the correct 'Index'.
-type Inj_Sym ss s = Inj_SymP (Index ss (Proxy s)) ss s
+type SymInj ss s = SymInjP (Index ss (Proxy s)) ss s
-- | 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 ::
+symInj ::
forall s ss ts t.
- Inj_Sym ss s =>
+ SymInj ss s =>
TeSym '[Proxy s] ts t ->
TeSym ss ts t
-inj_Sym = inj_SymP (Proxy @(Index ss (Proxy s)))
-
--- *** 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
+symInj = symInjP @(Index ss (Proxy s))
+
+-- *** Class 'SymPInj'
+class SymInjP p ss s where
+ symInjP :: TeSym '[Proxy s] ts t -> TeSym ss ts t
+instance SymInjP Zero (Proxy s ': ss) (s::k) where
+ symInjP (TeSym te) = TeSym te
+instance SymInjP p ss s => SymInjP (Succ p) (Proxy not_s ': ss) s where
+ symInjP (te::TeSym '[Proxy s] ts t) =
+ case symInjP @p te :: TeSym ss ts t of
TeSym te' -> TeSym te'
-- * Class 'Sym_Lambda'
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)
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)
app = (<*>)
lam f = Eval (unEval . f . Eval)
lam1 = lam
- let_ x f = f x -- like flip ($)
+ 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 ->
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
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