-- | Symantic for 'Sequences'.
module Language.Symantic.Lib.Sequences where
-import Control.Monad (liftM, liftM2)
-import qualified Data.MonoTraversable as MT
-import Data.Proxy
import Data.Sequences (SemiSequence, IsSequence)
-import qualified Data.Sequences as Seqs
-import Data.Text (Text)
-import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (filter, reverse)
+import qualified Data.MonoTraversable as MT
+import qualified Data.Sequences as Seqs
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
+import Language.Symantic
+import Language.Symantic.Lib.Function ()
+import Language.Symantic.Lib.Bool (tyBool)
+import Language.Symantic.Lib.MonoFunctor (e1, famElement)
-- * Class 'Sym_SemiSequence'
+type instance Sym SemiSequence = Sym_SemiSequence
class Sym_SemiSequence term where
intersperse :: SemiSequence s => term (MT.Element s) -> term s -> term s
cons :: SemiSequence s => term (MT.Element s) -> term s -> term s
snoc :: SemiSequence s => term s -> term (MT.Element s) -> term s
reverse :: SemiSequence s => term s -> term s
- default intersperse :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term s
- default cons :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term s
- default snoc :: (Trans t term, SemiSequence s) => t term s -> t term (MT.Element s) -> t term s
- default reverse :: (Trans t term, SemiSequence s) => t term s -> t term s
- intersperse = trans_map2 cons
- cons = trans_map2 cons
- snoc = trans_map2 snoc
- reverse = trans_map1 reverse
-
-type instance Sym_of_Iface (Proxy SemiSequence) = Sym_SemiSequence
-type instance TyConsts_of_Iface (Proxy SemiSequence) = Proxy SemiSequence ': TyConsts_imported_by SemiSequence
-type instance TyConsts_imported_by SemiSequence =
- [ Proxy SemiSequence
- , Proxy []
- , Proxy Text
- ]
-
-instance Sym_SemiSequence HostI where
- intersperse = liftM2 Seqs.intersperse
- cons = liftM2 Seqs.cons
- snoc = liftM2 Seqs.snoc
- reverse = liftM Seqs.reverse
-instance Sym_SemiSequence TextI where
- intersperse = textI2 "intersperse"
- cons = textI2 "cons"
- snoc = textI2 "snoc"
- reverse = textI1 "reverse"
-instance (Sym_SemiSequence r1, Sym_SemiSequence r2) => Sym_SemiSequence (DupI r1 r2) where
- intersperse = dupI2 (Proxy @Sym_SemiSequence) intersperse
- cons = dupI2 (Proxy @Sym_SemiSequence) cons
- snoc = dupI2 (Proxy @Sym_SemiSequence) snoc
- reverse = dupI1 (Proxy @Sym_SemiSequence) reverse
-
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs SemiSequence
- ) => Read_TyNameR TyName cs (Proxy SemiSequence ': rs) where
- read_TyNameR _cs (TyName "SemiSequence") k = k (ty @SemiSequence)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy SemiSequence ': cs) where
- show_TyConst TyConstZ{} = "SemiSequence"
- show_TyConst (TyConstS c) = show_TyConst c
-
-instance -- Proj_TyConC
- ( Proj_TyConst cs SemiSequence
- , Proj_TyConsts cs (TyConsts_imported_by SemiSequence)
- ) => Proj_TyConC cs (Proxy SemiSequence) where
- proj_TyConC _ (TyConst q :$ s)
- | Just Refl <- eq_skind (kind_of_TyConst q) (SKiType `SKiArrow` SKiConstraint)
- , Just Refl <- proj_TyConst q (Proxy @SemiSequence)
- = case s of
- TyConst c
- | Just Refl <- eq_skind (kind_of_TyConst c) SKiType ->
- case () of
- _ | Just Refl <- proj_TyConst c (Proxy @Text) -> Just TyCon
- _ -> Nothing
- TyConst c :$ _o
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType) ->
- case () of
- _ | Just Refl <- proj_TyConst c (Proxy @[]) -> Just TyCon
- _ -> Nothing
- _ -> Nothing
- proj_TyConC _c _q = Nothing
-data instance TokenT meta (ts::[*]) (Proxy SemiSequence)
- = Token_Term_SemiSequence_intersperse (EToken meta ts) (EToken meta ts)
- | Token_Term_SemiSequence_cons (EToken meta ts) (EToken meta ts)
- | Token_Term_SemiSequence_snoc (EToken meta ts) (EToken meta ts)
- | Token_Term_SemiSequence_reverse (EToken meta ts)
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy SemiSequence))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy SemiSequence))
-instance -- CompileI
- ( Inj_TyConst (TyConsts_of_Ifaces is) SemiSequence
- , Proj_TyCon (TyConsts_of_Ifaces is)
- , Proj_TyFam (TyConsts_of_Ifaces is) TyFam_MonoElement
- , Compile is
- ) => CompileI is (Proxy SemiSequence) where
- compileI
- :: forall meta ctx ret ls rs.
- TokenT meta is (Proxy SemiSequence)
- -> CompileT meta ctx ret is ls (Proxy SemiSequence ': rs)
- compileI tok ctx k =
- case tok of
- Token_Term_SemiSequence_intersperse tok_e tok_s ->
- e2s2s_from tok_e tok_s intersperse
- Token_Term_SemiSequence_cons tok_e tok_s ->
- e2s2s_from tok_e tok_s cons
- Token_Term_SemiSequence_snoc tok_s tok_e ->
- e2s2s_from tok_s tok_e (Prelude.flip snoc)
- Token_Term_SemiSequence_reverse tok_s ->
- -- reverse :: SemiSequence s => s -> s
- compileO tok_s ctx $ \ty_s (TermO s) ->
- check_TyCon (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \TyCon ->
- k ty_s $ TermO $
- \c -> reverse (s c)
- where
- e2s2s_from tok_e tok_s
- (f::forall term s.
- (Sym_SemiSequence term, SemiSequence s)
- => term (MT.Element s) -> term s -> term s) =
- -- intersperse :: SemiSequence s => MT.Element s -> s -> s
- -- cons :: SemiSequence s => MT.Element s -> s -> s
- -- snoc :: SemiSequence s => s -> MT.Element s -> s
- compileO tok_e ctx $ \ty_e (TermO e) ->
- compileO tok_s ctx $ \ty_s (TermO s) ->
- check_TyCon (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \TyCon ->
- check_TyFam (At (Just tok_s) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
- check_TyEq (At Nothing ty_s_e) (At (Just tok_e) ty_e) $ \Refl ->
- k ty_s $ TermO $
- \c -> f (e c) (s c)
-instance -- TokenizeT
- Inj_Token meta ts SemiSequence =>
- TokenizeT meta ts (Proxy SemiSequence) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ tokenize2 "intersperse" infixN5 Token_Term_SemiSequence_intersperse
- , tokenize2 "cons" infixN5 Token_Term_SemiSequence_cons
- , tokenize2 "snoc" infixN5 Token_Term_SemiSequence_snoc
- , tokenize1 "reverse" infixN5 Token_Term_SemiSequence_reverse
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy SemiSequence) g
+ default intersperse :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term (MT.Element s) -> term s -> term s
+ default cons :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term (MT.Element s) -> term s -> term s
+ default snoc :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term s -> term (MT.Element s) -> term s
+ default reverse :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term s -> term s
+ intersperse = trans2 cons
+ cons = trans2 cons
+ snoc = trans2 snoc
+ reverse = trans1 reverse
+
+-- Interpreting
+instance Sym_SemiSequence Eval where
+ intersperse = eval2 Seqs.intersperse
+ cons = eval2 Seqs.cons
+ snoc = eval2 Seqs.snoc
+ reverse = eval1 Seqs.reverse
+instance Sym_SemiSequence View where
+ intersperse = view2 "intersperse"
+ cons = view2 "cons"
+ snoc = view2 "snoc"
+ reverse = view1 "reverse"
+instance (Sym_SemiSequence r1, Sym_SemiSequence r2) => Sym_SemiSequence (Dup r1 r2) where
+ intersperse = dup2 @Sym_SemiSequence intersperse
+ cons = dup2 @Sym_SemiSequence cons
+ snoc = dup2 @Sym_SemiSequence snoc
+ reverse = dup1 @Sym_SemiSequence reverse
+
+-- Transforming
+instance (Sym_SemiSequence term, Sym_Lambda term) => Sym_SemiSequence (BetaT term)
+
+-- Typing
+instance FixityOf SemiSequence
+instance ClassInstancesFor SemiSequence
+instance TypeInstancesFor SemiSequence
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g SemiSequence
+instance (Source src, Inj_Sym ss SemiSequence) => ModuleFor src ss SemiSequence where
+ moduleFor = ["SemiSequence"] `moduleWhere`
+ [ "intersperse" := teSemiSequence_intersperse
+ , "cons" := teSemiSequence_cons
+ , "snoc" := teSemiSequence_snoc
+ , "reverse" := teSemiSequence_reverse
+ ]
+
+-- ** 'Type's
+tySemiSequence :: Source src => Type src vs a -> Type src vs (SemiSequence a)
+tySemiSequence a = tyConstLen @(K SemiSequence) @SemiSequence (lenVars a) `tyApp` a
+
+s0 :: Source src => Inj_Len vs => Inj_Kind (K s) =>
+ Type src (Proxy s ': vs) s
+s0 = tyVar "s" varZ
+
+-- ** 'Term's
+teSemiSequence_reverse :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (s -> s))
+teSemiSequence_reverse = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> s0) $ teSym @SemiSequence $ lam1 reverse
+
+teSemiSequence_intersperse, teSemiSequence_cons :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (e -> s -> s))
+teSemiSequence_intersperse = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> s0) $ teSym @SemiSequence $ lam2 intersperse
+teSemiSequence_cons = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> s0) $ teSym @SemiSequence $ lam2 cons
+
+teSemiSequence_snoc :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (s -> e -> s))
+teSemiSequence_snoc = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> e1 ~> s0) $ teSym @SemiSequence $ lam2 snoc
-- * Class 'Sym_IsSequence'
+type instance Sym IsSequence = Sym_IsSequence
class Sym_IsSequence term where
filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
- default filter :: (Trans t term, IsSequence s) => t term (MT.Element s -> Bool) -> t term s -> t term s
- filter = trans_map2 filter
-
-type instance Sym_of_Iface (Proxy IsSequence) = Sym_IsSequence
-type instance TyConsts_of_Iface (Proxy IsSequence) = Proxy IsSequence ': TyConsts_imported_by IsSequence
-type instance TyConsts_imported_by IsSequence =
- [ Proxy IsSequence
- , Proxy (->)
- , Proxy []
- , Proxy Text
- , Proxy Bool
- ]
-
-instance Sym_IsSequence HostI where
- filter = liftM2 Seqs.filter
-instance Sym_IsSequence TextI where
- filter = textI2 "filter"
-instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (DupI r1 r2) where
- filter = dupI2 (Proxy @Sym_IsSequence) filter
-
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs IsSequence
- ) => Read_TyNameR TyName cs (Proxy IsSequence ': rs) where
- read_TyNameR _cs (TyName "IsSequence") k = k (ty @IsSequence)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy IsSequence ': cs) where
- show_TyConst TyConstZ{} = "IsSequence"
- show_TyConst (TyConstS c) = show_TyConst c
-
-instance -- Proj_TyConC
- ( Proj_TyConst cs IsSequence
- , Proj_TyConsts cs (TyConsts_imported_by IsSequence)
- ) => Proj_TyConC cs (Proxy IsSequence) where
- proj_TyConC _ (TyConst q :$ s)
- | Just Refl <- eq_skind (kind_of_TyConst q) (SKiType `SKiArrow` SKiConstraint)
- , Just Refl <- proj_TyConst q (Proxy @IsSequence)
- = case s of
- TyConst c
- | Just Refl <- eq_skind (kind_of_TyConst c) SKiType ->
- case () of
- _ | Just Refl <- proj_TyConst c (Proxy @Text) -> Just TyCon
- _ -> Nothing
- TyConst c :$ _o
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType) ->
- case () of
- _ | Just Refl <- proj_TyConst c (Proxy @[]) -> Just TyCon
- _ -> Nothing
- _ -> Nothing
- proj_TyConC _c _q = Nothing
-data instance TokenT meta (ts::[*]) (Proxy IsSequence)
- = Token_Term_IsSequence_filter (EToken meta ts) (EToken meta ts)
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy IsSequence))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IsSequence))
-instance -- CompileI
- ( Inj_TyConst (TyConsts_of_Ifaces is) IsSequence
- , Inj_TyConst (TyConsts_of_Ifaces is) (->)
- , Inj_TyConst (TyConsts_of_Ifaces is) Bool
- , Proj_TyCon (TyConsts_of_Ifaces is)
- , Proj_TyFam (TyConsts_of_Ifaces is) TyFam_MonoElement
- , Compile is
- ) => CompileI is (Proxy IsSequence) where
- compileI
- :: forall meta ctx ret ls rs.
- TokenT meta is (Proxy IsSequence)
- -> CompileT meta ctx ret is ls (Proxy IsSequence ': rs)
- compileI tok ctx k =
- case tok of
- Token_Term_IsSequence_filter tok_e2Bool tok_s ->
- -- filter :: IsSequence s => (MT.Element s -> Bool) -> s -> s
- compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
- compileO tok_s ctx $ \ty_s (TermO s) ->
- check_TyEq2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
- check_TyEq
- (At Nothing (ty @Bool))
- (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
- check_TyCon (At (Just tok_s) (ty @IsSequence :$ ty_s)) $ \TyCon ->
- check_TyFam (At (Just tok_s) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
- check_TyEq
- (At Nothing ty_s_e)
- (At (Just tok_e2Bool) ty_e2Bool_e) $ \Refl ->
- k ty_s $ TermO $
- \c -> filter (e2Bool c) (s c)
-instance -- TokenizeT
- Inj_Token meta ts IsSequence =>
- TokenizeT meta ts (Proxy IsSequence) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ tokenize2 "filter" infixN5 Token_Term_IsSequence_filter
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy IsSequence) g
+ default filter :: Sym_IsSequence (UnT term) => Trans term => IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
+ filter = trans2 filter
+
+-- Interpreting
+instance Sym_IsSequence Eval where
+ filter = eval2 Seqs.filter
+instance Sym_IsSequence View where
+ filter = view2 "filter"
+instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (Dup r1 r2) where
+ filter = dup2 @Sym_IsSequence filter
+
+-- Transforming
+instance (Sym_IsSequence term, Sym_Lambda term) => Sym_IsSequence (BetaT term)
+
+-- Typing
+instance FixityOf IsSequence
+instance ClassInstancesFor IsSequence
+instance TypeInstancesFor IsSequence
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g IsSequence
+instance (Source src, Inj_Sym ss IsSequence) => ModuleFor src ss IsSequence where
+ moduleFor = ["IsSequence"] `moduleWhere`
+ [ "filter" := teIsSequence_filter
+ ]
+
+-- ** 'Type's
+tyIsSequence :: Source src => Type src vs a -> Type src vs (IsSequence a)
+tyIsSequence a = tyConstLen @(K IsSequence) @IsSequence (lenVars a) `tyApp` a
+
+-- ** 'Term's
+teIsSequence_filter :: TermDef IsSequence '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> ((e -> Bool) -> s -> s))
+teIsSequence_filter = Term (tyIsSequence s0 # e1 #~ famElement s0) ((e1 ~> tyBool) ~> s0 ~> s0) $ teSym @IsSequence $ lam2 filter
sourcephile / git / haskell / symantic.git / blobdiff