{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for '[]'. module Language.Symantic.Lib.List where import Data.Semigroup ((<>)) import Prelude hiding (zipWith) import qualified Data.Functor as Functor import qualified Data.List as List import qualified Data.MonoTraversable as MT import qualified Data.Sequences as Seqs import qualified Data.Text as Text import qualified Data.Traversable as Traversable import Language.Symantic import Language.Symantic.Grammar import Language.Symantic.Lib.Function (a0, b1, c2) import Language.Symantic.Lib.MonoFunctor (Element) -- * Class 'Sym_List' type instance Sym (Proxy []) = Sym_List class Sym_List term where list_empty :: term [a] list_cons :: term a -> term [a] -> term [a]; infixr 5 `list_cons` list :: [term a] -> term [a] zipWith :: term (a -> b -> c) -> term [a] -> term [b] -> term [c] default list_empty :: Sym_List (UnT term) => Trans term => term [a] default list_cons :: Sym_List (UnT term) => Trans term => term a -> term [a] -> term [a] default list :: Sym_List (UnT term) => Trans term => [term a] -> term [a] default zipWith :: Sym_List (UnT term) => Trans term => term (a -> b -> c) -> term [a] -> term [b] -> term [c] list_empty = trans list_empty list_cons = trans2 list_cons list l = trans (list (unTrans Functor.<$> l)) zipWith = trans3 zipWith -- Interpreting instance Sym_List Eval where list_empty = return [] list_cons = eval2 (:) list = Traversable.sequence zipWith = eval3 List.zipWith instance Sym_List View where list_empty = View $ \_p _v -> "[]" list_cons = viewInfix ":" (infixR 5) list l = View $ \_po v -> "[" <> Text.intercalate ", " ((\(View a) -> a op v) Functor.<$> l) <> "]" where op = (infixN0, SideL) zipWith = view3 "zipWith" instance (Sym_List r1, Sym_List r2) => Sym_List (Dup r1 r2) where list_empty = dup0 @Sym_List list_empty list_cons = dup2 @Sym_List list_cons list l = let (l1, l2) = foldr (\(x1 `Dup` x2) (xs1, xs2) -> (x1:xs1, x2:xs2)) ([], []) l in list l1 `Dup` list l2 zipWith = dup3 @Sym_List zipWith -- Transforming instance (Sym_List term, Sym_Lambda term) => Sym_List (BetaT term) -- Typing instance FixityOf [] where instance ClassInstancesFor [] where proveConstraintFor _ (TyApp _ (TyConst _ _ q) z) | Just HRefl <- proj_ConstKiTy @_ @[] z = case () of _ | 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 proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ z a)) | Just HRefl <- proj_ConstKiTy @_ @[] z = case () of _ | Just Refl <- proj_Const @Eq q , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict | Just Refl <- proj_Const @Monoid q -> Just Dict | Just Refl <- proj_Const @Show q , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict | Just Refl <- proj_Const @Ord 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 | Just Refl <- proj_Const @Seqs.IsSequence q -> Just Dict | Just Refl <- proj_Const @Seqs.SemiSequence q -> Just Dict _ -> Nothing proveConstraintFor _c _q = Nothing instance TypeInstancesFor [] where expandFamFor _c _len f ((TyApp _ z a) `TypesS` TypesZ) | Just HRefl <- proj_ConstKi @_ @Element f , Just HRefl <- proj_ConstKiTy @_ @[] z = Just a expandFamFor _c _len _fam _as = Nothing -- Compiling instance ( Gram_App g , Gram_Rule g , Gram_Comment g , Gram_Term src ss g , Inj_Sym ss [] ) => Gram_Term_AtomsFor src ss g [] where g_term_atomsFor _t = [ rule "teList_list" $ between (symbol "[") (symbol "]") listG , rule "teList_empty" $ withMeta $ (\src -> BinTree0 $ Token_Term $ TermVT_CF teList_empty `setSource` src) <$ symbol "[" <* symbol "]" ] where listG :: CF g (AST_Term src ss) listG = rule "list" $ withMeta $ (\a mb src -> case mb of Just b_ -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teList_cons) a) b_ Nothing -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teList_cons) a) (BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teList_empty)) <$> g_term <*> option Nothing (Just <$ symbol "," <*> listG) instance (Source src, Inj_Sym ss []) => Module src ss [] where module_ _s = [] `moduleWhere` [ "[]" := teList_empty , "zipWith" := teList_zipWith , ":" `withInfixR` 5 := teList_cons ] -- ** 'Type's tyList :: Source src => Inj_Len vs => Type src vs a -> Type src vs [a] tyList = (tyConst @(K []) @[] `tyApp`) -- ** 'Term's teList_empty :: Source src => Inj_Sym ss [] => Term src ss ts '[Proxy a] [a] teList_empty = Term noConstraint (tyList a0) $ teSym @[] $ list_empty teList_cons :: Source src => Inj_Sym ss [] => Term src ss ts '[Proxy a] (a -> [a] -> [a]) teList_cons = Term noConstraint (a0 ~> tyList a0 ~> tyList a0) $ teSym @[] $ lam2 list_cons teList_zipWith :: Source src => Inj_Sym ss [] => Term src ss ts '[Proxy a, Proxy b, Proxy c] ((a -> b -> c) -> [a] -> [b] -> [c]) teList_zipWith = Term noConstraint ((a0 ~> b1 ~> c2) ~> tyList a0 ~> tyList b1 ~> tyList c2) $ teSym @[] $ lam3 zipWith