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