symantic-lib/Language/Symantic/Lib/List.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=12 #-}
   4 -- | Symantic for '[]'.
   5 module Language.Symantic.Lib.List where
   6
   7 import Control.Monad (liftM, liftM2, liftM3)
   8 import Data.Monoid ((<>))
   9 import Data.Proxy
  10 import Data.Type.Equality ((:~:)(Refl))
  11 import Prelude hiding (zipWith)
  12 import qualified Data.Foldable as Foldable
  13 import qualified Data.Function as Fun
  14 import qualified Data.Functor as Functor
  15 import qualified Data.List as List
  16 import qualified Data.MonoTraversable as MT
  17 import qualified Data.Sequences as Seqs
  18 import qualified Data.Text as Text
  19 import qualified Data.Traversable as Traversable
  20
  21 import Language.Symantic.Parsing
  22 import Language.Symantic.Typing
  23 import Language.Symantic.Compiling
  24 import Language.Symantic.Interpreting
  25 import Language.Symantic.Transforming
  26 import Language.Symantic.Lib.Lambda
  27 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement)
  28
  29 -- * Class 'Sym_List'
  30 class Sym_List term where
  31         list_empty     :: term [a]
  32         list_singleton :: term a -> term [a]
  33         (.:)           :: term a -> term [a] -> term [a]; infixr 5 .:
  34         list           :: [term a] -> term [a]
  35         zipWith        :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
  36
  37         default list_empty     :: Trans t term => t term [a]
  38         default list_singleton :: Trans t term => t term a -> t term [a]
  39         default (.:)           :: Trans t term => t term a -> t term [a] -> t term [a]
  40         default list           :: Trans t term => [t term a] -> t term [a]
  41         default zipWith        :: Trans t term => t term (a -> b -> c) -> t term [a] -> t term [b] -> t term [c]
  42
  43         list_empty     = trans_lift list_empty
  44         list_singleton = trans_map1 list_singleton
  45         (.:)           = trans_map2 (.:)
  46         list l         = trans_lift (list (trans_apply Functor.<$> l))
  47         zipWith        = trans_map3 zipWith
  48
  49 type instance Sym_of_Iface (Proxy []) = Sym_List
  50 type instance TyConsts_of_Iface (Proxy []) = Proxy [] ': TyConsts_imported_by (Proxy [])
  51 type instance TyConsts_imported_by (Proxy []) =
  52  [ Proxy Applicative
  53  , Proxy Bool
  54  , Proxy Eq
  55  , Proxy Foldable
  56  , Proxy Functor
  57  , Proxy Monad
  58  , Proxy MT.MonoFoldable
  59  , Proxy MT.MonoFunctor
  60  , Proxy Monoid
  61  , Proxy Ord
  62  , Proxy Seqs.IsSequence
  63  , Proxy Seqs.SemiSequence
  64  , Proxy Show
  65  , Proxy Traversable
  66  ]
  67
  68 instance Sym_List HostI where
  69         list_empty     = return []
  70         list_singleton = liftM return
  71         (.:)           = liftM2 (:)
  72         list           = Traversable.sequence
  73         zipWith        = liftM3 List.zipWith
  74 instance Sym_List TextI where
  75         list_empty = TextI $ \_p _v -> "[]"
  76         list_singleton a = textI_infix ":" op a list_empty
  77                 where op = infixR 5
  78         (.:) = textI_infix ":" (infixR 5)
  79         list l = TextI $ \_po v ->
  80                 "[" <> Text.intercalate ", " ((\(TextI a) -> a op v) Functor.<$> l) <> "]"
  81                 where op = (infixN0, L)
  82         zipWith = textI3 "zipWith"
  83 instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
  84         list_empty     = dupI0 @Sym_List list_empty
  85         list_singleton = dupI1 @Sym_List list_singleton
  86         (.:)           = dupI2 @Sym_List (.:)
  87         list l =
  88                 let (l1, l2) =
  89                         Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) ->
  90                                 (x1:xs1, x2:xs2)) ([], []) l in
  91                 list l1 `DupI` list l2
  92         zipWith = dupI3 @Sym_List zipWith
  93
  94 instance
  95  ( Read_TyNameR TyName cs rs
  96  , Inj_TyConst cs []
  97  ) => Read_TyNameR TyName cs (Proxy [] ': rs) where
  98         read_TyNameR _cs (TyName "[]") k = k (ty @[])
  99         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 100 instance Show_TyConst cs => Show_TyConst (Proxy [] ': cs) where
 101         show_TyConst TyConstZ{} = "[]"
 102         show_TyConst (TyConstS c) = show_TyConst c
 103 instance Show_TyConst cs => Show_TyConst (Proxy String ': cs) where
 104         show_TyConst TyConstZ{} = "String"
 105         show_TyConst (TyConstS c) = show_TyConst c
 106
 107 instance -- Proj_TyFamC TyFam_MonoElement
 108  ( Proj_TyConst cs []
 109  ) => Proj_TyFamC cs TyFam_MonoElement [] where
 110         proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
 111          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
 112          , Just Refl <- proj_TyConst c (Proxy @[])
 113          = Just ty_a
 114         proj_TyFamC _c _fam _ty = Nothing
 115
 116 instance -- Proj_TyConC
 117  ( Proj_TyConst cs []
 118  , Proj_TyConsts cs (TyConsts_imported_by (Proxy []))
 119  , Proj_TyCon cs
 120  ) => Proj_TyConC cs (Proxy []) where
 121         proj_TyConC _ (TyConst q :$ TyConst c)
 122          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
 123          , Just Refl <- proj_TyConst c (Proxy @[])
 124          = case () of
 125                  _ | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
 126                    | Just Refl <- proj_TyConst q (Proxy @Foldable)    -> Just TyCon
 127                    | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
 128                    | Just Refl <- proj_TyConst q (Proxy @Monad)       -> Just TyCon
 129                    | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
 130                  _ -> Nothing
 131         proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a))
 132          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
 133          , Just Refl <- proj_TyConst c (Proxy @[])
 134          = case () of
 135                  _ | Just Refl <- proj_TyConst q (Proxy @Eq)
 136                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
 137                    | Just Refl <- proj_TyConst q (Proxy @Monoid) -> Just TyCon
 138                    | Just Refl <- proj_TyConst q (Proxy @Show)
 139                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
 140                    | Just Refl <- proj_TyConst q (Proxy @Ord)
 141                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
 142                    | Just Refl <- proj_TyConst q (Proxy @MT.MonoFoldable)   -> Just TyCon
 143                    | Just Refl <- proj_TyConst q (Proxy @MT.MonoFunctor)    -> Just TyCon
 144                    | Just Refl <- proj_TyConst q (Proxy @Seqs.IsSequence)   -> Just TyCon
 145                    | Just Refl <- proj_TyConst q (Proxy @Seqs.SemiSequence) -> Just TyCon
 146                  _ -> Nothing
 147         proj_TyConC _c _q = Nothing
 148 data instance TokenT meta (ts::[*]) (Proxy [])
 149  = Token_Term_List_empty     (EToken meta '[Proxy Token_Type])
 150  | Token_Term_List_cons      (EToken meta ts) (EToken meta ts)
 151  | Token_Term_List_singleton (EToken meta ts)
 152  | Token_Term_List_list      (EToken meta '[Proxy Token_Type]) [EToken meta ts]
 153  | Token_Term_List_zipWith   (EToken meta ts)
 154 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy []))
 155 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy []))
 156
 157 instance -- CompileI
 158  ( Read_TyName TyName cs
 159  , Inj_TyConst        cs []
 160  , Inj_TyConst        cs (->)
 161  , Compile cs is
 162  ) => CompileI cs is (Proxy []) where
 163         compileI
 164          :: forall meta ctx ret ls rs.
 165          TokenT meta is (Proxy [])
 166          -> Compiler meta ctx ret cs is ls (Proxy [] ': rs)
 167         compileI tok ctx k =
 168                 case tok of
 169                  Token_Term_List_empty tok_ty_a ->
 170                         -- [] :: [a]
 171                         compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
 172                         check_Kind
 173                          (At Nothing SKiType)
 174                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 175                         k (ty @[] :$ ty_a) $ Term $
 176                                 Fun.const list_empty
 177                  Token_Term_List_singleton tok_a ->
 178                         -- [a] :: [a]
 179                         compile tok_a ctx $ \ty_a (Term a) ->
 180                         check_Kind
 181                          (At Nothing SKiType)
 182                          (At (Just tok_a) $ kind_of ty_a) $ \Refl ->
 183                         k (ty @[] :$ ty_a) $ Term $
 184                          \c -> list_singleton (a c)
 185                  Token_Term_List_cons tok_a tok_as ->
 186                         compile tok_a ctx $ \ty_a (Term a) ->
 187                         compile tok_as ctx $ \ty_as (Term as) ->
 188                         check_TyEq1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_as_a ->
 189                         check_TyEq (At (Just tok_a) ty_a) (At (Just tok_as) ty_as_a) $ \Refl ->
 190                         k ty_as $ Term $
 191                          \c -> a c .: as c
 192                  Token_Term_List_list tok_ty_a tok_as ->
 193                         compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
 194                         check_Kind
 195                          (At Nothing SKiType)
 196                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 197                         go (At (Just tok_ty_a) ty_a) [] tok_as
 198                         where
 199                         go :: At meta '[Proxy Token_Type] (Type cs ty_a)
 200                            -> [Term ctx ty_a is '[] is]
 201                            -> [EToken meta is]
 202                            -> Either (Error_Term meta cs is) ret
 203                         go ty_a as [] =
 204                                 k (ty @[] :$ unAt ty_a) $ Term $
 205                                  \c -> list $ (\(Term a) -> a c)
 206                                          Functor.<$> List.reverse as
 207                         go ty_a as (tok_x:tok_xs) =
 208                                 compile tok_x ctx $ \ty_x x ->
 209                                 check_Type_is ty_a (At (Just tok_x) ty_x) $ \Refl ->
 210                                 go ty_a (x:as) tok_xs
 211                  Token_Term_List_zipWith tok_a2b2c ->
 212                         -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
 213                         compile tok_a2b2c ctx $ \ty_a2b2c (Term a2b2c) ->
 214                         check_TyEq2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c) $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
 215                         check_TyEq2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c_b2c) $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
 216                         k ( ty @[] :$ ty_a2b2c_a
 217                          ~> ty @[] :$ ty_a2b2c_b2c_b
 218                          ~> ty @[] :$ ty_a2b2c_b2c_c ) $ Term $
 219                          \c -> lam $ lam . zipWith (a2b2c c)
 220 instance -- TokenizeT
 221  Inj_Token meta ts [] =>
 222  TokenizeT meta ts (Proxy []) where
 223         tokenizeT _t = mempty
 224          { tokenizers_infix = tokenizeTMod []
 225                  [ (TeName "[]",) $ ProTok_Term
 226                          { protok_term = \meta -> ProTokPi $ \a ->
 227                                 ProTok $ inj_EToken meta $ Token_Term_List_empty a
 228                          , protok_fixity = infixN5
 229                          }
 230                  , tokenize2 ":" (infixR 5) Token_Term_List_cons
 231                  , tokenize1 "zipWith" infixN0 Token_Term_List_zipWith
 232                  ]
 233          }
 234 instance
 235  ( App g
 236  , Gram_Rule g
 237  , Gram_Lexer g
 238  , Gram_Term ts meta g
 239  , Inj_Token meta ts (->)
 240  , Inj_Token meta ts []
 241  ) => Gram_Term_AtomsT meta ts (Proxy []) g where
 242         gs_term_atomsT _t =
 243          [ rule "term_list" $
 244                 ProTok <$> between (symbol "[") (symbol "]") listG
 245          , rule "term_list_empty" $
 246                 metaG $
 247                 (\meta -> ProTokPi $ \a -> ProTok $ inj_EToken meta $ Token_Term_List_empty a)
 248                  <$ symbol "["
 249                  <* symbol "]"
 250          ]
 251                 where
 252                 listG :: CF g (EToken meta ts)
 253                 listG = rule "list" $
 254                         metaG $
 255                         (\a mb meta -> inj_EToken meta $ case mb of
 256                          Just b  -> Token_Term_List_cons a b
 257                          Nothing -> Token_Term_List_singleton a)
 258                          <$> g_term
 259                          <*> option Nothing (Just <$ symbol "," <*> listG)