{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=9 #-}
-- | Symantic for 'MonoFoldable'.
module Language.Symantic.Lib.MonoFoldable where
-import Control.Monad (liftM, liftM2, liftM3)
import Data.MonoTraversable (MonoFoldable)
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
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.MonoFunctor
+import Language.Symantic
+import Language.Symantic.Lib.Bool (tyBool)
+import Language.Symantic.Lib.Function ()
+import Language.Symantic.Lib.Int (tyInt)
+import Language.Symantic.Lib.List (tyList)
+import Language.Symantic.Lib.MonoFunctor (famElement, o0, e1)
+import Language.Symantic.Lib.Monoid (tyMonoid)
-- * Class 'Sym_MonoFoldable'
-class Sym_MonoFunctor term => Sym_MonoFoldable term where
+type instance Sym MonoFoldable = Sym_MonoFoldable
+class Sym_MonoFoldable term where
ofoldMap :: (MonoFoldable o, Monoid m) => term (MT.Element o -> m) -> term o -> term m
ofoldr :: MonoFoldable o => term (MT.Element o -> b -> b) -> term b -> term o -> term b
ofoldl' :: MonoFoldable o => term (b -> MT.Element o -> b) -> term b -> term o -> term b
oall :: MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
oany :: MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
otoList :: MonoFoldable o => term o -> term [MT.Element o]
- default ofoldMap :: (Trans t term, MonoFoldable o, Monoid m)
- => t term (MT.Element o -> m) -> t term o -> t term m
- default ofoldr :: (Trans t term, MonoFoldable o)
- => t term (MT.Element o -> b -> b) -> t term b -> t term o -> t term b
- default ofoldl' :: (Trans t term, MonoFoldable o)
- => t term (b -> MT.Element o -> b) -> t term b -> t term o -> t term b
- default olength :: (Trans t term, MonoFoldable o) => t term o -> t term Int
- default onull :: (Trans t term, MonoFoldable o) => t term o -> t term Bool
- default oall :: (Trans t term, MonoFoldable o) => t term (MT.Element o -> Bool) -> t term o -> t term Bool
- default oany :: (Trans t term, MonoFoldable o) => t term (MT.Element o -> Bool) -> t term o -> t term Bool
- default otoList :: (Trans t term, MonoFoldable o) => t term o -> t term [MT.Element o]
- ofoldMap = trans_map2 ofoldMap
- ofoldr = trans_map3 ofoldr
- ofoldl' = trans_map3 ofoldl'
- olength = trans_map1 olength
- onull = trans_map1 onull
- oall = trans_map2 oall
- oany = trans_map2 oany
- otoList = trans_map1 otoList
-
-type instance Sym_of_Iface (Proxy MonoFoldable) = Sym_MonoFoldable
-type instance TyConsts_of_Iface (Proxy MonoFoldable) = Proxy MonoFoldable ': TyConsts_imported_by (Proxy MonoFoldable)
-type instance TyConsts_imported_by (Proxy MonoFoldable) =
- [ Proxy (->)
- , Proxy Bool
- , Proxy Int
- , Proxy Monoid
- ]
-
-instance Sym_MonoFoldable HostI where
- ofoldMap = liftM2 MT.ofoldMap
- ofoldr = liftM3 MT.ofoldr
- ofoldl' = liftM3 MT.ofoldl'
- olength = liftM MT.olength
- onull = liftM MT.onull
- oall = liftM2 MT.oall
- oany = liftM2 MT.oany
- otoList = liftM MT.otoList
-instance Sym_MonoFoldable TextI where
- ofoldMap = textI2 "ofoldMap"
- ofoldr = textI3 "ofoldr"
- ofoldl' = textI3 "ofoldl'"
- olength = textI1 "olength"
- onull = textI1 "onull"
- oall = textI2 "oall"
- oany = textI2 "oany"
- otoList = textI1 "otoList"
-instance (Sym_MonoFoldable r1, Sym_MonoFoldable r2) => Sym_MonoFoldable (DupI r1 r2) where
- ofoldMap = dupI2 @Sym_MonoFoldable ofoldMap
- ofoldr = dupI3 @Sym_MonoFoldable ofoldr
- ofoldl' = dupI3 @Sym_MonoFoldable ofoldl'
- olength = dupI1 @Sym_MonoFoldable olength
- onull = dupI1 @Sym_MonoFoldable onull
- oall = dupI2 @Sym_MonoFoldable oall
- oany = dupI2 @Sym_MonoFoldable oany
- otoList = dupI1 @Sym_MonoFoldable otoList
-
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs MonoFoldable
- ) => Read_TyNameR TyName cs (Proxy MonoFoldable ': rs) where
- read_TyNameR _cs (TyName "MonoFoldable") k = k (ty @MonoFoldable)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy MonoFoldable ': cs) where
- show_TyConst TyConstZ{} = "MonoFoldable"
- show_TyConst (TyConstS c) = show_TyConst c
-
-instance Proj_TyConC cs (Proxy MonoFoldable)
-
-data instance TokenT meta (ts::[*]) (Proxy MonoFoldable)
- = Token_Term_MonoFoldable_ofoldMap (EToken meta ts) (EToken meta ts)
- | Token_Term_MonoFoldable_ofoldr (EToken meta ts) (EToken meta ts) (EToken meta ts)
- | Token_Term_MonoFoldable_ofoldl' (EToken meta ts) (EToken meta ts) (EToken meta ts)
- | Token_Term_MonoFoldable_olength (EToken meta ts)
- | Token_Term_MonoFoldable_onull (EToken meta ts)
- | Token_Term_MonoFoldable_oall (EToken meta ts) (EToken meta ts)
- | Token_Term_MonoFoldable_oany (EToken meta ts) (EToken meta ts)
- | Token_Term_MonoFoldable_otoList (EToken meta ts)
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFoldable))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFoldable))
-instance -- CompileI
- ( Inj_TyConst cs MonoFoldable
- , Inj_TyConst cs (->)
- , Inj_TyConst cs []
- , Inj_TyConst cs Monoid
- , Inj_TyConst cs Bool
- , Inj_TyConst cs Int
- , Proj_TyCon cs
- , Proj_TyFam cs TyFam_MonoElement
- , Compile cs is
- ) => CompileI cs is (Proxy MonoFoldable) where
- compileI
- :: forall meta ctx ret ls rs.
- TokenT meta is (Proxy MonoFoldable)
- -> Compiler meta ctx ret cs is ls (Proxy MonoFoldable ': rs)
- compileI tok ctx k =
- case tok of
- Token_Term_MonoFoldable_ofoldMap tok_f tok_o ->
- -- ofoldMap :: Monoid m => (Element o -> m) -> o -> m
- compile tok_f ctx $ \ty_f (Term f) ->
- compile tok_o ctx $ \ty_o (Term o) ->
- check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_m ->
- check_TyCon (At (Just tok_f) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
- check_TyCon (At (Just tok_f) (ty @Monoid :$ ty_m)) $ \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_m $ Term $
- \c -> ofoldMap (f c) (o c)
- Token_Term_MonoFoldable_ofoldr tok_e2b2b tok_b tok_o ->
- ofoldr_from tok_e2b2b tok_b tok_o ofoldr
- Token_Term_MonoFoldable_ofoldl' tok_b2e2b tok_b tok_o ->
- ofoldl_from tok_b2e2b tok_b tok_o ofoldl'
- Token_Term_MonoFoldable_olength tok_o -> o2ty_from tok_o olength
- Token_Term_MonoFoldable_onull tok_o -> o2ty_from tok_o onull
- Token_Term_MonoFoldable_oall tok_e2Bool tok_o -> oalloany_from tok_e2Bool tok_o oall
- Token_Term_MonoFoldable_oany tok_e2Bool tok_o -> oalloany_from tok_e2Bool tok_o oany
- Token_Term_MonoFoldable_otoList tok_o ->
- -- otoList :: MonoFoldable o => o -> [MT.Element o]
- compile tok_o ctx $ \ty_o (Term o) ->
- check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
- check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
- k (ty @[] :$ ty_o_e) $ Term $
- \c -> otoList (o c)
- where
- ofoldr_from tok_e2b2b tok_b tok_o
- (fold::forall term o b.
- (Sym_MonoFoldable term, MonoFoldable o)
- => term (MT.Element o -> b -> b) -> term b -> term o -> term b) =
- -- ofoldr :: MonoFoldable o => (MT.Element o -> b -> b) -> b -> o -> b
- compile tok_e2b2b ctx $ \ty_e2b2b (Term e2b2b) ->
- compile tok_b ctx $ \ty_b (Term b) ->
- compile tok_o ctx $ \ty_o (Term o) ->
- check_TyEq2 (ty @(->)) (At (Just tok_e2b2b) ty_e2b2b) $ \Refl ty_e2b2b_e ty_e2b2b_b2b ->
- check_TyEq2 (ty @(->)) (At (Just tok_e2b2b) ty_e2b2b_b2b) $ \Refl ty_e2b2b_b2b_b0 ty_e2b2b_b2b_b1 ->
- check_TyEq
- (At (Just tok_e2b2b) ty_e2b2b_b2b_b0)
- (At (Just tok_e2b2b) ty_e2b2b_b2b_b1) $ \Refl ->
- check_TyEq
- (At (Just tok_e2b2b) ty_e2b2b_b2b_b0)
- (At (Just tok_b) ty_b) $ \Refl ->
- check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
- check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
- check_TyEq
- (At (Just tok_e2b2b) ty_e2b2b_e)
- (At (Just tok_o) ty_o_e) $ \Refl ->
- k ty_b $ Term $
- \c -> fold (e2b2b c) (b c) (o c)
- ofoldl_from tok_b2e2b tok_b tok_o
- (fold::forall term o b.
- (Sym_MonoFoldable term, MonoFoldable o)
- => term (b -> MT.Element o -> b) -> term b -> term o -> term b) =
- -- ofoldl' :: MonoFoldable o => (b -> MT.Element o -> b) -> b -> o -> b
- compile tok_b2e2b ctx $ \ty_b2e2b (Term b2e2b) ->
- compile tok_b ctx $ \ty_b (Term b) ->
- compile tok_o ctx $ \ty_o (Term o) ->
- check_TyEq2 (ty @(->)) (At (Just tok_b2e2b) ty_b2e2b) $ \Refl ty_b2e2b_b ty_b2e2b_a2b ->
- check_TyEq2 (ty @(->)) (At (Just tok_b2e2b) ty_b2e2b_a2b) $ \Refl ty_b2e2b_a2b_e ty_b2e2b_a2b_b ->
- check_TyEq
- (At (Just tok_b2e2b) ty_b2e2b_b)
- (At (Just tok_b2e2b) ty_b2e2b_a2b_b) $ \Refl ->
- check_TyEq
- (At (Just tok_b2e2b) ty_b2e2b_b)
- (At (Just tok_b) ty_b) $ \Refl ->
- check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
- check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
- check_TyEq
- (At (Just tok_b2e2b) ty_b2e2b_a2b_e)
- (At (Just tok_o) ty_o_e) $ \Refl ->
- k ty_b $ Term $
- \c -> fold (b2e2b c) (b c) (o c)
- o2ty_from
- :: forall typ. Inj_TyConst cs typ
- => EToken meta is
- -> (forall term o. (Sym_MonoFoldable term, MonoFoldable o) => term o -> term typ)
- -> Either (Error_Term meta cs is) ret
- o2ty_from tok_o f =
- -- olength :: MonoFoldable o => o -> Int
- -- onull :: MonoFoldable o => o -> Bool
- compile tok_o ctx $ \ty_o (Term o) ->
- check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
- k (TyConst inj_TyConst::Type cs typ) $ Term $
- \c -> f (o c)
- oalloany_from
- tok_e2Bool tok_o
- (g::forall term o.
- (Sym_MonoFoldable term, MonoFoldable o)
- => term (MT.Element o -> Bool) -> term o -> term Bool) =
- -- all :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
- -- any :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
- compile tok_e2Bool ctx $ \ty_e2Bool (Term e2Bool) ->
- compile tok_o ctx $ \ty_o (Term o) ->
- check_TyEq2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
- check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
- check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
- check_TyEq
- (At (Just tok_e2Bool) ty_e2Bool_e)
- (At (Just tok_o) ty_o_e) $ \Refl ->
- check_TyEq
- (At Nothing (ty @Bool))
- (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
- k (ty @Bool) $ Term $
- \c -> g (e2Bool c) (o c)
-instance -- TokenizeT
- Inj_Token meta ts MonoFoldable =>
- TokenizeT meta ts (Proxy MonoFoldable) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ tokenize2 "ofoldMap" infixN5 Token_Term_MonoFoldable_ofoldMap
- , tokenize3 "ofoldr" infixN5 Token_Term_MonoFoldable_ofoldr
- , tokenize3 "ofoldl'" infixN5 Token_Term_MonoFoldable_ofoldl'
- , tokenize1 "olength" infixN5 Token_Term_MonoFoldable_olength
- , tokenize1 "onull" infixN5 Token_Term_MonoFoldable_onull
- , tokenize2 "oall" infixN5 Token_Term_MonoFoldable_oall
- , tokenize2 "oany" infixN5 Token_Term_MonoFoldable_oany
- , tokenize1 "otoList" infixN5 Token_Term_MonoFoldable_otoList
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy MonoFoldable) g
+ default ofoldMap :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => Monoid m => term (MT.Element o -> m) -> term o -> term m
+ default ofoldr :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term (MT.Element o -> b -> b) -> term b -> term o -> term b
+ default ofoldl' :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term (b -> MT.Element o -> b) -> term b -> term o -> term b
+ default olength :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term o -> term Int
+ default onull :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term o -> term Bool
+ default oall :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
+ default oany :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
+ default otoList :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term o -> term [MT.Element o]
+ ofoldMap = trans2 ofoldMap
+ ofoldr = trans3 ofoldr
+ ofoldl' = trans3 ofoldl'
+ olength = trans1 olength
+ onull = trans1 onull
+ oall = trans2 oall
+ oany = trans2 oany
+ otoList = trans1 otoList
+
+-- Interpreting
+instance Sym_MonoFoldable Eval where
+ ofoldMap = eval2 MT.ofoldMap
+ ofoldr = eval3 MT.ofoldr
+ ofoldl' = eval3 MT.ofoldl'
+ olength = eval1 MT.olength
+ onull = eval1 MT.onull
+ oall = eval2 MT.oall
+ oany = eval2 MT.oany
+ otoList = eval1 MT.otoList
+instance Sym_MonoFoldable View where
+ ofoldMap = view2 "ofoldMap"
+ ofoldr = view3 "ofoldr"
+ ofoldl' = view3 "ofoldl'"
+ olength = view1 "olength"
+ onull = view1 "onull"
+ oall = view2 "oall"
+ oany = view2 "oany"
+ otoList = view1 "otoList"
+instance (Sym_MonoFoldable r1, Sym_MonoFoldable r2) => Sym_MonoFoldable (Dup r1 r2) where
+ ofoldMap = dup2 @Sym_MonoFoldable ofoldMap
+ ofoldr = dup3 @Sym_MonoFoldable ofoldr
+ ofoldl' = dup3 @Sym_MonoFoldable ofoldl'
+ olength = dup1 @Sym_MonoFoldable olength
+ onull = dup1 @Sym_MonoFoldable onull
+ oall = dup2 @Sym_MonoFoldable oall
+ oany = dup2 @Sym_MonoFoldable oany
+ otoList = dup1 @Sym_MonoFoldable otoList
+
+-- Transforming
+instance (Sym_MonoFoldable term, Sym_Lambda term) => Sym_MonoFoldable (BetaT term)
+
+-- Typing
+instance NameTyOf MonoFoldable where
+ nameTyOf _c = ["MonoFoldable"] `Mod` "MonoFoldable"
+instance FixityOf MonoFoldable
+instance ClassInstancesFor MonoFoldable
+instance TypeInstancesFor MonoFoldable
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g MonoFoldable
+instance (Source src, SymInj ss MonoFoldable) => ModuleFor src ss MonoFoldable where
+ moduleFor = ["MonoFoldable"] `moduleWhere`
+ [ "ofoldMap" := teMonoFoldable_ofoldMap
+ , "otoList" := teMonoFoldable_otoList
+ , "ofoldr" := teMonoFoldable_ofoldr
+ , "ofoldl'" := teMonoFoldable_ofoldl'
+ , "olength" := teMonoFoldable_olength
+ , "onull" := teMonoFoldable_onull
+ , "oall" := teMonoFoldable_oall
+ , "oany" := teMonoFoldable_oany
+ ]
+
+-- ** 'Type's
+tyMonoFoldable :: Source src => Type src vs a -> Type src vs (MonoFoldable a)
+tyMonoFoldable a = tyConstLen @(K MonoFoldable) @MonoFoldable (lenVars a) `tyApp` a
+
+-- ** 'Term's
+teMonoFoldable_ofoldMap :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy m] (MonoFoldable o # Monoid m # e #~ MT.Element o #> ((e -> m) -> o -> m))
+teMonoFoldable_ofoldMap = Term (tyMonoFoldable o0 # tyMonoid m # e1 #~ famElement o0) ((e1 ~> m) ~> o0 ~> m) $ teSym @MonoFoldable $ lam2 ofoldMap
+ where
+ m :: Source src => LenInj vs => KindInj (K m) => Type src (Proxy a ': Proxy b ': Proxy m ': vs) m
+ m = tyVar "m" $ VarS $ VarS varZ
+
+teMonoFoldable_otoList :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (o -> [MT.Element o]))
+teMonoFoldable_otoList = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (o0 ~> tyList (famElement o0)) $ teSym @MonoFoldable $ lam1 otoList
+
+teMonoFoldable_ofoldr :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy a] (MonoFoldable o # e #~ MT.Element o #> ((e -> a -> a) -> a -> o -> a))
+teMonoFoldable_ofoldr = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((e1 ~> a ~> a) ~> a ~> o0 ~> a) $ teSym @MonoFoldable $ lam1 $ \f -> lam $ lam . ofoldr f
+ where
+ a :: Source src => LenInj vs => KindInj (K a) => Type src (Proxy _a ': Proxy b ': Proxy a ': vs) a
+ a = tyVar "a" $ VarS $ VarS varZ
+
+teMonoFoldable_ofoldl' :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy a] (MonoFoldable o # e #~ MT.Element o #> ((a -> e -> a) -> a -> o -> a))
+teMonoFoldable_ofoldl' = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((a ~> e1 ~> a) ~> a ~> o0 ~> a) $ teSym @MonoFoldable $ lam1 $ \f -> lam $ lam . ofoldl' f
+ where
+ a :: Source src => LenInj vs => KindInj (K a) => Type src (Proxy _a ': Proxy b ': Proxy a ': vs) a
+ a = tyVar "a" $ VarS $ VarS varZ
+
+teMonoFoldable_olength :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (o -> Int))
+teMonoFoldable_olength = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (o0 ~> tyInt) $ teSym @MonoFoldable $ lam1 olength
+
+teMonoFoldable_onull :: TermDef MonoFoldable '[Proxy o] (MonoFoldable o #> (o -> Bool))
+teMonoFoldable_onull = Term (tyMonoFoldable o0) (o0 ~> tyBool) $ teSym @MonoFoldable $ lam1 onull
+
+teMonoFoldable_oall :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> ((e -> Bool) -> o -> Bool))
+teMonoFoldable_oall = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((e1 ~> tyBool) ~> o0 ~> tyBool) $ teSym @MonoFoldable $ lam2 oall
+
+teMonoFoldable_oany :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> ((e -> Bool) -> o -> Bool))
+teMonoFoldable_oany = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((e1 ~> tyBool) ~> o0 ~> tyBool) $ teSym @MonoFoldable $ lam2 oany
sourcephile / git / haskell / symantic.git / blobdiff