{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {-# OPTIONS_GHC -fconstraint-solver-iterations=9 #-} -- | Symantic for '[]'. module Language.Symantic.Lib.List where import Control.Monad (liftM, liftM2, liftM3) import qualified Data.Foldable as Foldable import qualified Data.Function as Fun import qualified Data.Functor as Functor import qualified Data.List as List import Data.Monoid ((<>)) import Data.Proxy import qualified Data.Text as Text import qualified Data.Traversable as Traversable import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding (zipWith) 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 -- * Class 'Sym_List' class Sym_List term where list_empty :: term [a] list_singleton :: term a -> term [a] (.:) :: term a -> term [a] -> term [a]; infixr 5 .: list :: [term a] -> term [a] zipWith :: term (a -> b -> c) -> term [a] -> term [b] -> term [c] default list_empty :: Trans t term => t term [a] default list_singleton :: Trans t term => t term a -> t term [a] default (.:) :: Trans t term => t term a -> t term [a] -> t term [a] default list :: Trans t term => [t term a] -> t term [a] default zipWith :: Trans t term => t term (a -> b -> c) -> t term [a] -> t term [b] -> t term [c] list_empty = trans_lift list_empty list_singleton = trans_map1 list_singleton (.:) = trans_map2 (.:) list l = trans_lift (list (trans_apply Functor.<$> l)) zipWith = trans_map3 zipWith type instance Sym_of_Iface (Proxy []) = Sym_List type instance TyConsts_of_Iface (Proxy []) = Proxy [] ': TyConsts_imported_by [] type instance TyConsts_imported_by [] = [ Proxy Applicative , Proxy Bool , Proxy Eq , Proxy Foldable , Proxy Functor , Proxy Monad , Proxy Monoid , Proxy Ord , Proxy Show , Proxy Traversable ] instance Sym_List HostI where list_empty = return [] list_singleton = liftM return (.:) = liftM2 (:) list = Traversable.sequence zipWith = liftM3 List.zipWith instance Sym_List TextI where list_empty = TextI $ \_p _v -> "[]" list_singleton a = textI_infix ":" op a list_empty where op = infixR 5 (.:) = textI_infix ":" (infixR 5) list l = TextI $ \_po v -> "[" <> Text.intercalate ", " ((\(TextI a) -> a op v) Functor.<$> l) <> "]" where op = (infixN0, L) zipWith = textI3 "zipWith" instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where list_empty = dupI0 @Sym_List list_empty list_singleton = dupI1 @Sym_List list_singleton (.:) = dupI2 @Sym_List (.:) list l = let (l1, l2) = Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) -> (x1:xs1, x2:xs2)) ([], []) l in list l1 `DupI` list l2 zipWith = dupI3 @Sym_List zipWith instance ( Read_TyNameR TyName cs rs , Inj_TyConst cs [] ) => Read_TyNameR TyName cs (Proxy [] ': rs) where read_TyNameR _cs (TyName "[]") k = k (ty @[]) read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k instance Show_TyConst cs => Show_TyConst (Proxy [] ': cs) where show_TyConst TyConstZ{} = "[]" show_TyConst (TyConstS c) = show_TyConst c instance Show_TyConst cs => Show_TyConst (Proxy String ': cs) where show_TyConst TyConstZ{} = "String" show_TyConst (TyConstS c) = show_TyConst c instance -- Proj_TyConC ( Proj_TyConst cs [] , Proj_TyConsts cs (TyConsts_imported_by []) , Proj_TyCon cs ) => Proj_TyConC cs (Proxy []) where proj_TyConC _ (TyConst q :$ TyConst c) | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType) , Just Refl <- proj_TyConst c (Proxy @[]) = 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 _ -> 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 @[]) = 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 | Just Refl <- proj_TyConst q (Proxy @Show) , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon | Just Refl <- proj_TyConst q (Proxy @Ord) , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon _ -> Nothing proj_TyConC _c _q = Nothing data instance TokenT meta (ts::[*]) (Proxy []) = Token_Term_List_empty (EToken meta '[Proxy Token_Type]) | Token_Term_List_cons (EToken meta ts) (EToken meta ts) | Token_Term_List_singleton (EToken meta ts) | Token_Term_List_list (EToken meta '[Proxy Token_Type]) [EToken meta ts] | Token_Term_List_zipWith (EToken meta ts) deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy [])) deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy [])) instance -- CompileI ( Read_TyName TyName cs , Inj_TyConst cs [] , Inj_TyConst cs (->) , Compile cs is ) => CompileI cs is (Proxy []) where compileI :: forall meta ctx ret ls rs. TokenT meta is (Proxy []) -> CompileT meta ctx ret cs is ls (Proxy [] ': rs) compileI tok ctx k = case tok of Token_Term_List_empty tok_ty_a -> -- [] :: [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 @[] :$ ty_a) $ TermO $ Fun.const list_empty Token_Term_List_singleton tok_a -> -- [a] :: [a] compileO tok_a ctx $ \ty_a (TermO a) -> check_Kind (At Nothing SKiType) (At (Just tok_a) $ kind_of ty_a) $ \Refl -> k (ty @[] :$ ty_a) $ TermO $ \c -> list_singleton (a c) Token_Term_List_cons tok_a tok_as -> compileO tok_a ctx $ \ty_a (TermO a) -> compileO tok_as ctx $ \ty_as (TermO as) -> check_TyEq1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_as_a -> check_TyEq (At (Just tok_a) ty_a) (At (Just tok_as) ty_as_a) $ \Refl -> k ty_as $ TermO $ \c -> a c .: as c Token_Term_List_list tok_ty_a tok_as -> 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 -> go (At (Just tok_ty_a) ty_a) [] tok_as where go :: At meta '[Proxy Token_Type] (Type cs ty_a) -> [TermO ctx ty_a is '[] is] -> [EToken meta is] -> Either (Error_Term meta cs is) ret go ty_a as [] = k (ty @[] :$ unAt ty_a) $ TermO $ \c -> list $ (\(TermO a) -> a c) Functor.<$> List.reverse as go ty_a as (tok_x:tok_xs) = compileO tok_x ctx $ \ty_x x -> check_Type_is ty_a (At (Just tok_x) ty_x) $ \Refl -> go ty_a (x:as) tok_xs Token_Term_List_zipWith tok_a2b2c -> -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] compileO tok_a2b2c ctx $ \ty_a2b2c (TermO a2b2c) -> check_TyEq2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c) $ \Refl ty_a2b2c_a ty_a2b2c_b2c -> check_TyEq2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c_b2c) $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c -> k ( ty @[] :$ ty_a2b2c_a ~> ty @[] :$ ty_a2b2c_b2c_b ~> ty @[] :$ ty_a2b2c_b2c_c ) $ TermO $ \c -> lam $ lam . zipWith (a2b2c c) instance -- TokenizeT Inj_Token meta ts [] => TokenizeT meta ts (Proxy []) where tokenizeT _t = mempty { tokenizers_infix = tokenizeTMod [] [ (TeName "[]",) $ ProTok_Term { protok_term = \meta -> ProTokPi $ \a -> ProTok $ inj_EToken meta $ Token_Term_List_empty a , protok_fixity = infixN5 } , tokenize2 ":" (infixR 5) Token_Term_List_cons , tokenize1 "zipWith" infixN0 Token_Term_List_zipWith ] } instance ( App g , Gram_Rule g , Gram_Lexer g , Gram_Term ts meta g , Inj_Token meta ts (->) , Inj_Token meta ts [] ) => Gram_Term_AtomsT meta ts (Proxy []) g where gs_term_atomsT _t = [ rule "term_list" $ ProTok <$> between (symbol "[") (symbol "]") listG , rule "term_list_empty" $ metaG $ (\meta -> ProTokPi $ \a -> ProTok $ inj_EToken meta $ Token_Term_List_empty a) <$ symbol "[" <* symbol "]" ] where listG :: CF g (EToken meta ts) listG = rule "list" $ metaG $ (\a mb meta -> inj_EToken meta $ case mb of Just b -> Token_Term_List_cons a b Nothing -> Token_Term_List_singleton a) <$> g_term <*> option Nothing (Just <$ symbol "," <*> listG)