{-# 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.Map.Strict (Map)
import Data.MonoTraversable (MonoFunctor)
import qualified Data.MonoTraversable as MT
-import Data.Proxy
-import Data.Text (Text)
-import Data.Ratio (Ratio)
-import Data.Type.Equality ((:~:)(Refl))
-import GHC.Exts (Constraint)
-import qualified System.IO as IO
-import Language.Symantic.Helper.Data.Type.List hiding (Map)
-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 (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
+
+-- Transforming
+instance (Sym_MonoFunctor term, Sym_Lambda term) => Sym_MonoFunctor (BetaT term)
-type instance Sym_of_Iface (Proxy MonoFunctor) = Sym_MonoFunctor
-type instance TyConsts_of_Iface (Proxy MonoFunctor) = Proxy MonoFunctor ': TyConsts_imported_by MonoFunctor
-type instance TyConsts_imported_by MonoFunctor =
- [ Proxy (->)
- , Proxy (,)
- , Proxy []
- , Proxy Either
- , Proxy IO
- , Proxy Map
- , Proxy Maybe
- , Proxy Text
- ] ++ TyConsts_imported_by IO
+-- Typing
+instance NameTyOf MonoFunctor where
+ nameTyOf _c = ["MonoFunctor"] `Mod` "MonoFunctor"
+instance FixityOf MonoFunctor
+instance ClassInstancesFor MonoFunctor
+instance TypeInstancesFor MonoFunctor
-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
+-- 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
+ ]
-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
+-- ** 'Type's
+tyMonoFunctor :: Source src => Type src vs a -> Type src vs (MonoFunctor a)
+tyMonoFunctor a = tyConstLen @(K MonoFunctor) @MonoFunctor (lenVars a) `tyApp` a
--- * Type 'TyFam_MonoElement'
-data TyFam_MonoElement
- = TyFam_MonoElement
- deriving (Eq, Show)
-type instance TyFam TyFam_MonoElement '[h] = MT.Element (UnProxy h)
+o0 :: Source src => LenInj vs => KindInj (K o) =>
+ Type src (Proxy o ': vs) o
+o0 = tyVar "o" varZ
-instance -- Constraint
- Proj_TyFamC cs TyFam_MonoElement (c::Constraint)
-instance -- k -> Constraint
- Proj_TyFamC cs TyFam_MonoElement (c::k -> Constraint)
-instance -- (->)
- ( Proj_TyConst cs (->)
- ) => Proj_TyFamC cs TyFam_MonoElement (->) where
- proj_TyFamC _c _fam ((TyConst c :$ _ty_r :$ ty_a) `TypesS` TypesZ)
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @(->))
- = Just ty_a
- proj_TyFamC _c _fam _ty = Nothing
-instance -- []
- ( Proj_TyConst cs []
- ) => Proj_TyFamC cs TyFam_MonoElement [] where
- proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @[])
- = Just ty_a
- proj_TyFamC _c _fam _ty = Nothing
-instance -- ()
- Proj_TyFamC cs TyFam_MonoElement ()
-instance -- (,)
- ( Proj_TyConst cs (,)
- ) => Proj_TyFamC cs TyFam_MonoElement (,) where
- proj_TyFamC _c _fam ((TyConst c :$ _ty_a :$ ty_b) `TypesS` TypesZ)
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @(,))
- = Just ty_b
- proj_TyFamC _c _fam _ty = Nothing
-instance -- Bool
- Proj_TyFamC cs TyFam_MonoElement Bool
-instance -- Char
- Proj_TyFamC cs TyFam_MonoElement Char
-instance -- Either
- ( Proj_TyConst cs Either
- ) => Proj_TyFamC cs TyFam_MonoElement Either where
- proj_TyFamC _c _fam ((TyConst c :$ _ty_l :$ ty_r) `TypesS` TypesZ)
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @Either)
- = Just ty_r
- proj_TyFamC _c _fam _ty = Nothing
-instance -- Int
- Proj_TyFamC cs TyFam_MonoElement Int
-instance -- Integer
- Proj_TyFamC cs TyFam_MonoElement Integer
-instance -- IO
- ( Proj_TyConst cs IO
- ) => Proj_TyFamC cs TyFam_MonoElement IO where
- proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @IO)
- = Just ty_a
- proj_TyFamC _c _fam _ty = Nothing
-instance -- IO.Handle
- Proj_TyFamC cs TyFam_MonoElement IO.Handle
-instance -- IO.IOMode
- Proj_TyFamC cs TyFam_MonoElement IO.IOMode
-instance -- Map
- ( Proj_TyConst cs Map
- ) => Proj_TyFamC cs TyFam_MonoElement Map where
- proj_TyFamC _c _fam ((TyConst c :$ _ty_k :$ ty_a) `TypesS` TypesZ)
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @Map)
- = Just ty_a
- proj_TyFamC _c _fam _ty = Nothing
-instance -- Maybe
- ( Proj_TyConst cs Maybe
- ) => Proj_TyFamC cs TyFam_MonoElement Maybe where
- proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @Maybe)
- = Just ty_a
- proj_TyFamC _c _fam _ty = Nothing
-instance -- Ordering
- Proj_TyFamC cs TyFam_MonoElement Ordering
-instance -- Ratio
- Proj_TyFamC cs TyFam_MonoElement Ratio
-instance -- Text
- ( Proj_TyConst cs Text
- , Inj_TyConst cs (MT.Element Text)
- ) => Proj_TyFamC cs TyFam_MonoElement Text where
- proj_TyFamC _c _fam (TyConst c `TypesS` TypesZ)
- | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
- , Just Refl <- proj_TyConst c (Proxy @Text)
- = Just (TyConst inj_TyConst::Type cs (MT.Element Text))
- proj_TyFamC _c _fam _ty = Nothing
+e1 :: Source src => LenInj vs => KindInj (K e) =>
+ Type src (a ': Proxy e ': vs) e
+e1 = tyVar "e" $ VarS varZ
-instance -- Proj_TyConC
- ( Proj_TyConst cs MonoFunctor
- , Proj_TyConsts cs (TyConsts_imported_by MonoFunctor)
- ) => Proj_TyConC cs (Proxy MonoFunctor) where
- proj_TyConC _ (TyConst q :$ typ)
- | Just Refl <- eq_skind (kind_of_TyConst q) (SKiType `SKiArrow` SKiConstraint)
- , Just Refl <- proj_TyConst q (Proxy @MonoFunctor)
- = case typ of
- TyConst c
- | Just Refl <- proj_TyConst c (Proxy @Text) -> Just TyCon
- TyConst c :$ _a
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
- -> case () of
- _ | Just Refl <- proj_TyConst c (Proxy @[]) -> Just TyCon
- | Just Refl <- proj_TyConst c (Proxy @IO) -> Just TyCon
- | Just Refl <- proj_TyConst c (Proxy @Maybe) -> Just TyCon
- _ -> Nothing
- TyConst c :$ _a :$ _b
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
- -> case () of
- _ | Just Refl <- proj_TyConst c (Proxy @(->)) -> Just TyCon
- | Just Refl <- proj_TyConst c (Proxy @(,)) -> Just TyCon
- | Just Refl <- proj_TyConst c (Proxy @Either) -> Just TyCon
- | Just Refl <- proj_TyConst c (Proxy @Map) -> Just TyCon
- _ -> Nothing
- _ -> Nothing
- proj_TyConC _c _q = Nothing
-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
- compileO tok_f ctx $ \ty_f (TermO f) ->
- compileO tok_o ctx $ \ty_o (TermO 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 $ TermO $
- \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