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

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