{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
-- | Symantic for 'Maybe'.
module Language.Symantic.Lib.Maybe where
import Control.Monad
-import qualified Data.Function as Fun
-import qualified Data.Maybe as Maybe
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (maybe)
+import qualified Data.Maybe as Maybe
+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.Lib.Lambda
+import Language.Symantic
+import Language.Symantic.Lib.Function (a0, b1)
+import Language.Symantic.Lib.MonoFunctor (Element)
--- * Class 'Sym_Maybe_Lam'
+-- * Class 'Sym_Maybe'
+type instance Sym Maybe = Sym_Maybe
class Sym_Maybe term where
_Nothing :: term (Maybe a)
_Just :: term a -> term (Maybe a)
maybe :: term b -> term (a -> b) -> term (Maybe a) -> term b
- default _Nothing :: Trans t term => t term (Maybe a)
- default _Just :: Trans t term => t term a -> t term (Maybe a)
- default maybe :: Trans t term => t term b -> t term (a -> b) -> t term (Maybe a) -> t term b
+ default _Nothing :: Sym_Maybe (UnT term) => Trans term => term (Maybe a)
+ default _Just :: Sym_Maybe (UnT term) => Trans term => term a -> term (Maybe a)
+ default maybe :: Sym_Maybe (UnT term) => Trans term => term b -> term (a -> b) -> term (Maybe a) -> term b
- _Nothing = trans_lift _Nothing
- _Just = trans_map1 _Just
- maybe = trans_map3 maybe
+ _Nothing = trans _Nothing
+ _Just = trans1 _Just
+ maybe = trans3 maybe
-type instance Sym_of_Iface (Proxy Maybe) = Sym_Maybe
-type instance TyConsts_of_Iface (Proxy Maybe) = Proxy Maybe ': TyConsts_imported_by Maybe
-type instance TyConsts_imported_by Maybe =
- [ Proxy Applicative
- , Proxy Eq
- , Proxy Foldable
- , Proxy Functor
- , Proxy Monad
- , Proxy Monoid
- , Proxy Show
- , Proxy Traversable
- ]
+-- Interpreting
+instance Sym_Maybe Eval where
+ _Nothing = Eval Nothing
+ _Just = eval1 Just
+ maybe = eval3 Maybe.maybe
+instance Sym_Maybe View where
+ _Nothing = view0 "Nothing"
+ _Just = view1 "Just"
+ maybe = view3 "maybe"
+instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (Dup r1 r2) where
+ _Nothing = dup0 @Sym_Maybe _Nothing
+ _Just = dup1 @Sym_Maybe _Just
+ maybe = dup3 @Sym_Maybe maybe
-instance Sym_Maybe HostI where
- _Nothing = HostI Nothing
- _Just = liftM Just
- maybe = liftM3 Maybe.maybe
-instance Sym_Maybe TextI where
- _Nothing = textI0 "Nothing"
- _Just = textI1 "Just"
- maybe = textI3 "maybe"
-instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (DupI r1 r2) where
- _Nothing = dupI0 @Sym_Maybe _Nothing
- _Just = dupI1 @Sym_Maybe _Just
- maybe = dupI3 @Sym_Maybe maybe
+-- Transforming
+instance (Sym_Maybe term, Sym_Lambda term) => Sym_Maybe (BetaT term)
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Maybe
- ) => Read_TyNameR TyName cs (Proxy Maybe ': rs) where
- read_TyNameR _cs (TyName "Maybe") k = k (ty @Maybe)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Maybe ': cs) where
- show_TyConst TyConstZ{} = "Maybe"
- show_TyConst (TyConstS c) = show_TyConst c
-
-instance -- Proj_TyConC
- ( Proj_TyConst cs Maybe
- , Proj_TyConsts cs (TyConsts_imported_by Maybe)
- , Proj_TyCon cs
- ) => Proj_TyConC cs (Proxy Maybe) where
- proj_TyConC _ (TyConst q :$ TyConst c)
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @Maybe)
+-- Typing
+instance NameTyOf Maybe where
+ nameTyOf _c = ["Maybe"] `Mod` "Maybe"
+instance FixityOf Maybe
+instance ClassInstancesFor Maybe where
+ proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
+ | Just HRefl <- proj_ConstKiTy @_ @Maybe c
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Foldable) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Functor) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Monad) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
+ _ | Just Refl <- proj_Const @Applicative q -> Just Dict
+ | Just Refl <- proj_Const @Foldable q -> Just Dict
+ | Just Refl <- proj_Const @Functor q -> Just Dict
+ | Just Refl <- proj_Const @Monad q -> Just Dict
+ | Just Refl <- proj_Const @Traversable q -> Just Dict
_ -> Nothing
- proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a))
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @Maybe)
+ proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))
+ | Just HRefl <- proj_ConstKiTy @_ @Maybe c
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Eq)
- , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Monoid)
- , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Show)
- , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
+ _ | Just Refl <- proj_Const @Eq q
+ , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+ | Just Refl <- proj_Const @Monoid q
+ , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+ | Just Refl <- proj_Const @Show q
+ , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
+ | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
+ | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
_ -> Nothing
- proj_TyConC _c _q = Nothing
-data instance TokenT meta (ts::[*]) (Proxy Maybe)
- = Token_Term_Maybe_Nothing (EToken meta '[Proxy Token_Type])
- | Token_Term_Maybe_Just (EToken meta ts)
- | Token_Term_Maybe_maybe (EToken meta ts) (EToken meta ts)
-deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Maybe))
-deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Maybe))
-instance -- CompileI
- ( Read_TyName TyName cs
- , Inj_TyConst cs Maybe
- , Inj_TyConst cs (->)
- , Compile cs is
- ) => CompileI cs is (Proxy Maybe) where
- compileI tok ctx k =
- case tok of
- Token_Term_Maybe_Nothing tok_ty_a ->
- -- Nothing :: Maybe a
- compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
- check_Kind
- (At Nothing SKiType)
- (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
- k (ty @Maybe :$ ty_a) $ TermO $
- Fun.const _Nothing
- Token_Term_Maybe_Just tok_a ->
- -- Just :: a -> Maybe a
- compileO tok_a ctx $ \ty_a (TermO a) ->
- k (ty @Maybe :$ ty_a) $ TermO $
- \c -> _Just (a c)
- Token_Term_Maybe_maybe tok_b tok_a2b ->
- -- maybe :: b -> (a -> b) -> Maybe a -> b
- compileO tok_b ctx $ \ty_b (TermO b) ->
- compileO tok_a2b ctx $ \ty_a2b (TermO a2b) ->
- check_TyEq2 (ty @(->)) (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
- check_TyEq
- (At (Just tok_a2b) ty_a2b_b)
- (At (Just tok_b) ty_b) $ \Refl ->
- k (ty @Maybe :$ ty_a2b_a ~> ty_b) $ TermO $
- \c -> lam $ maybe (b c) (a2b c)
-instance
- Inj_Token meta ts Maybe =>
- TokenizeT meta ts (Proxy Maybe) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ (Term_Name "Nothing",) Term_ProTok
- { term_protok = \meta -> ProTokPi $ \a ->
- ProTok $ inj_EToken meta $ Token_Term_Maybe_Nothing a
- , term_fixity = infixN5
- }
- , tokenize1 "Just" infixN5 Token_Term_Maybe_Just
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy Maybe) g
+ proveConstraintFor _c _q = Nothing
+instance TypeInstancesFor Maybe where
+ expandFamFor _c _len f (TyApp _ c a `TypesS` TypesZ)
+ | Just HRefl <- proj_ConstKi @_ @Element f
+ , Just HRefl <- proj_ConstKiTy @_ @Maybe c
+ = Just a
+ expandFamFor _c _len _fam _as = Nothing
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Maybe
+instance (Source src, SymInj ss Maybe) => ModuleFor src ss Maybe where
+ moduleFor = ["Maybe"] `moduleWhere`
+ [ "Nothing" := teMaybe_Nothing
+ , "Just" := teMaybe_Just
+ , "maybe" := teMaybe_maybe
+ ]
+
+-- ** 'Type's
+tyMaybe :: Source src => LenInj vs => Type src vs a -> Type src vs (Maybe a)
+tyMaybe = (tyConst @(K Maybe) @Maybe `tyApp`)
+
+-- ** 'Term's
+teMaybe_Nothing :: TermDef Maybe '[Proxy a] (() #> Maybe a)
+teMaybe_Nothing = Term noConstraint (tyMaybe a0) $ teSym @Maybe $ _Nothing
+
+teMaybe_Just :: TermDef Maybe '[Proxy a] (() #> (a -> Maybe a))
+teMaybe_Just = Term noConstraint (a0 ~> tyMaybe a0) $ teSym @Maybe $ lam1 _Just
+
+teMaybe_maybe :: TermDef Maybe '[Proxy a, Proxy b] (() #> (b -> (a -> b) -> Maybe a -> b))
+teMaybe_maybe = Term noConstraint (b1 ~> (a0 ~> b1) ~> tyMaybe a0 ~> b1) $ teSym @Maybe $ lam1 $ \b' -> lam $ lam . maybe b'
sourcephile / git / haskell / symantic.git / blobdiff