{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
-- | Symantic for 'MonoFunctor'.
module Language.Symantic.Lib.MonoFunctor where
-import Control.Monad (liftM2)
import Data.MonoTraversable (MonoFunctor)
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
-import GHC.Exts (Constraint)
import qualified Data.MonoTraversable as MT
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
+import Language.Symantic
+import Language.Symantic.Lib.Function ()
+
+-- * Type 'Element'
+data Element
+type instance Fam Element '[h] = MT.Element (UnProxy h)
+instance NameTyOf Element where
+ nameTyOf _c = ["MonoFunctor"] `Mod` "Element"
+instance ClassInstancesFor Element
+instance TypeInstancesFor Element where
+ expandFamFor _c _len f (TyApp _ (TyApp _ z _ty_r) a `TypesS` TypesZ)
+ | Just HRefl <- proj_ConstKi @_ @Element f
+ , Just HRefl <- proj_ConstKiTy @_ @(->) z
+ = Just a
+ expandFamFor _c _len _fam _as = Nothing
+
+-- ** 'Type's
+famElement :: Source src => Type src vs t -> Type src vs (MT.Element t)
+famElement o = TyFam noSource (lenVars o) (constInj @Element) (o `TypesS` TypesZ)
-- * Class 'Sym_MonoFunctor'
+type instance Sym MonoFunctor = Sym_MonoFunctor
class Sym_MonoFunctor term where
omap :: MonoFunctor o => term (MT.Element o -> MT.Element o) -> term o -> term o
- default omap :: (Trans t term, MonoFunctor o)
- => t term (MT.Element o -> MT.Element o) -> t term o -> t term o
- omap = trans_map2 omap
+ default omap
+ :: Sym_MonoFunctor (UnT term)
+ => Trans term
+ => MonoFunctor o
+ => term (MT.Element o -> MT.Element o) -> term o -> term o
+ omap = trans2 omap
+
+-- Interpreting
+instance Sym_MonoFunctor Eval where
+ omap = eval2 MT.omap
+instance Sym_MonoFunctor View where
+ omap = view2 "omap"
+instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (Dup r1 r2) where
+ omap = dup2 @Sym_MonoFunctor omap
-type instance Sym_of_Iface (Proxy MonoFunctor) = Sym_MonoFunctor
-type instance TyConsts_of_Iface (Proxy MonoFunctor) = Proxy MonoFunctor ': TyConsts_imported_by (Proxy MonoFunctor)
-type instance TyConsts_imported_by (Proxy MonoFunctor) = '[ Proxy (->) ]
+-- Transforming
+instance (Sym_MonoFunctor term, Sym_Lambda term) => Sym_MonoFunctor (BetaT term)
-instance Sym_MonoFunctor HostI where
- omap = liftM2 MT.omap
-instance Sym_MonoFunctor TextI where
- omap = textI2 "omap"
-instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (DupI r1 r2) where
- omap = dupI2 @Sym_MonoFunctor omap
+-- Typing
+instance NameTyOf MonoFunctor where
+ nameTyOf _c = ["MonoFunctor"] `Mod` "MonoFunctor"
+instance FixityOf MonoFunctor
+instance ClassInstancesFor MonoFunctor
+instance TypeInstancesFor MonoFunctor
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs MonoFunctor
- ) => Read_TyNameR TyName cs (Proxy MonoFunctor ': rs) where
- read_TyNameR _cs (TyName "MonoFunctor") k = k (ty @MonoFunctor)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy MonoFunctor ': cs) where
- show_TyConst TyConstZ{} = "MonoFunctor"
- show_TyConst (TyConstS c) = show_TyConst c
+-- Compiling
+instance Gram_Term_AtomsFor src ss g MonoFunctor
+instance (Source src, SymInj ss MonoFunctor) => ModuleFor src ss MonoFunctor where
+ moduleFor = ["MonoFunctor"] `moduleWhere`
+ [ "omap" := teMonoFunctor_omap
+ ]
--- * Type 'TyFam_MonoElement'
-data TyFam_MonoElement
- = TyFam_MonoElement
- deriving (Eq, Show)
-type instance TyFam TyFam_MonoElement '[h] = MT.Element (UnProxy h)
+-- ** 'Type's
+tyMonoFunctor :: Source src => Type src vs a -> Type src vs (MonoFunctor a)
+tyMonoFunctor a = tyConstLen @(K MonoFunctor) @MonoFunctor (lenVars a) `tyApp` a
-instance -- Constraint
- Proj_TyFamC cs TyFam_MonoElement (c::Constraint)
-instance -- k -> Constraint
- Proj_TyFamC cs TyFam_MonoElement (c::k -> Constraint)
+o0 :: Source src => LenInj vs => KindInj (K o) =>
+ Type src (Proxy o ': vs) o
+o0 = tyVar "o" varZ
-instance Proj_TyConC cs (Proxy MonoFunctor)
+e1 :: Source src => LenInj vs => KindInj (K e) =>
+ Type src (a ': Proxy e ': vs) e
+e1 = tyVar "e" $ VarS varZ
-data instance TokenT meta (ts::[*]) (Proxy MonoFunctor)
- = Token_Term_MonoFunctor_omap (EToken meta ts) (EToken meta ts)
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFunctor))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFunctor))
-instance -- CompileI
- ( Inj_TyConst cs MonoFunctor
- , Inj_TyConst cs (->)
- , Proj_TyCon cs
- , Proj_TyFam cs TyFam_MonoElement
- , Compile cs is
- ) => CompileI cs is (Proxy MonoFunctor) where
- compileI tok ctx k =
- case tok of
- Token_Term_MonoFunctor_omap tok_f tok_o ->
- -- omap :: (Element o -> Element o) -> o -> o
- compile tok_f ctx $ \ty_f (Term f) ->
- compile tok_o ctx $ \ty_o (Term m) ->
- check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_f_b ->
- check_TyEq
- (At (Just tok_f) ty_f_a)
- (At (Just tok_f) ty_f_b) $ \Refl ->
- check_TyCon (At (Just tok_f) (ty @MonoFunctor :$ ty_o)) $ \TyCon ->
- check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
- check_TyEq
- (At Nothing ty_o_e)
- (At (Just tok_f) ty_f_a) $ \Refl ->
- k ty_o $ Term $
- \c -> omap (f c) (m c)
-instance -- TokenizeT
- Inj_Token meta ts MonoFunctor =>
- TokenizeT meta ts (Proxy MonoFunctor) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ tokenize2 "omap" infixN5 Token_Term_MonoFunctor_omap
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy MonoFunctor) g
+-- ** 'Term's
+teMonoFunctor_omap :: TermDef MonoFunctor '[Proxy o, Proxy e] (MonoFunctor o # e #~ MT.Element o #> ((e -> e) -> o -> o))
+teMonoFunctor_omap = Term (tyMonoFunctor o0 # e1 #~ famElement o0) ((e1 ~> e1) ~> o0 ~> o0) $ teSym @MonoFunctor $ lam2 omap
sourcephile / git / haskell / symantic.git / blobdiff