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.Parsing.Grammar
  21 import Language.Symantic.Typing
  22 import Language.Symantic.Compiling
  23 import Language.Symantic.Interpreting
  24 import Language.Symantic.Transforming.Trans
  25 import Language.Symantic.Lib.Lambda
  26
  27 -- * Class 'Sym_List'
  28 class Sym_List term where
  29         list_empty     :: term [a]
  30         list_singleton :: term a -> term [a]
  31         (.:)           :: term a -> term [a] -> term [a]
  32         list           :: [term a] -> term [a]
  33         zipWith        :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
  34
  35         default list_empty     :: Trans t term => t term [a]
  36         default list_singleton :: Trans t term => t term a -> t term [a]
  37         default (.:)           :: Trans t term => t term a -> t term [a] -> t term [a]
  38         default list           :: Trans t term => [t term a] -> t term [a]
  39         default zipWith        :: Trans t term => t term (a -> b -> c) -> t term [a] -> t term [b] -> t term [c]
  40
  41         list_empty     = trans_lift list_empty
  42         list_singleton = trans_map1 list_singleton
  43         (.:)           = trans_map2 (.:)
  44         list l         = trans_lift (list (trans_apply Functor.<$> l))
  45         zipWith        = trans_map3 zipWith
  46
  47 infixr 5 .:
  48
  49 type instance Sym_of_Iface (Proxy []) = Sym_List
  50 type instance Consts_of_Iface (Proxy []) = Proxy [] ': Consts_imported_by []
  51 type instance Consts_imported_by [] =
  52  [ Proxy Applicative
  53  , Proxy Bool
  54  , Proxy Eq
  55  , Proxy Foldable
  56  , Proxy Functor
  57  , Proxy Monad
  58  , Proxy Monoid
  59  , Proxy Ord
  60  , Proxy Show
  61  , Proxy Traversable
  62  ]
  63
  64 instance Sym_List HostI where
  65         list_empty     = return []
  66         list_singleton = liftM return
  67         (.:)           = liftM2 (:)
  68         list           = Traversable.sequence
  69         zipWith        = liftM3 List.zipWith
  70 instance Sym_List TextI where
  71         list_empty = TextI $ \_p _v -> "[]"
  72         list_singleton a = textI_infix ":" op a list_empty
  73                 where op = infixR 5
  74         (.:) = textI_infix ":" (infixR 5)
  75         list l = TextI $ \_po v ->
  76                 "[" <> Text.intercalate ", " ((\(TextI a) -> a op v) Functor.<$> l) <> "]"
  77                 where op = (infixN0, L)
  78         zipWith = textI3 "zipWith"
  79 instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
  80         list_empty = dupI0 (Proxy @Sym_List) list_empty
  81         list_singleton = dupI1 (Proxy @Sym_List) list_singleton
  82         (.:) = dupI2 (Proxy @Sym_List) (.:)
  83         list l =
  84                 let (l1, l2) =
  85                         Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) ->
  86                                 (x1:xs1, x2:xs2)) ([], []) l in
  87                 list l1 `DupI` list l2
  88         zipWith = dupI3 (Proxy @Sym_List) zipWith
  89
  90 instance
  91  ( Read_TypeNameR Type_Name cs rs
  92  , Inj_Const cs []
  93  ) => Read_TypeNameR Type_Name cs (Proxy [] ': rs) where
  94         read_typenameR _cs (Type_Name "[]") k = k (ty @[])
  95         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  96 instance Show_Const cs => Show_Const (Proxy [] ': cs) where
  97         show_const ConstZ{} = "[]"
  98         show_const (ConstS c) = show_const c
  99 instance Show_Const cs => Show_Const (Proxy String ': cs) where
 100         show_const ConstZ{} = "String"
 101         show_const (ConstS c) = show_const c
 102
 103 instance -- Proj_ConC
 104  ( Proj_Const cs []
 105  , Proj_Consts cs (Consts_imported_by [])
 106  , Proj_Con cs
 107  ) => Proj_ConC cs (Proxy []) where
 108         proj_conC _ (TyConst q :$ TyConst c)
 109          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 110          , Just Refl <- proj_const c (Proxy @[])
 111          = case () of
 112                  _ | Just Refl <- proj_const q (Proxy @Applicative) -> Just Con
 113                    | Just Refl <- proj_const q (Proxy @Foldable)    -> Just Con
 114                    | Just Refl <- proj_const q (Proxy @Functor)     -> Just Con
 115                    | Just Refl <- proj_const q (Proxy @Monad)       -> Just Con
 116                    | Just Refl <- proj_const q (Proxy @Traversable) -> Just Con
 117                  _ -> Nothing
 118         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
 119          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 120          , Just Refl <- proj_const c (Proxy @[])
 121          = case () of
 122                  _ | Just Refl <- proj_const q (Proxy @Eq)
 123                    , Just Con  <- proj_con (t :$ a) -> Just Con
 124                    | Just Refl <- proj_const q (Proxy @Monoid) -> Just Con
 125                    | Just Refl <- proj_const q (Proxy @Show)
 126                    , Just Con  <- proj_con (t :$ a) -> Just Con
 127                    | Just Refl <- proj_const q (Proxy @Ord)
 128                    , Just Con  <- proj_con (t :$ a) -> Just Con
 129                  _ -> Nothing
 130         proj_conC _c _q = Nothing
 131 data instance TokenT meta (ts::[*]) (Proxy [])
 132  = Token_Term_List_empty     (EToken meta '[Proxy Token_Type])
 133  | Token_Term_List_cons      (EToken meta ts) (EToken meta ts)
 134  | Token_Term_List_singleton (EToken meta ts)
 135  | Token_Term_List_list      (EToken meta '[Proxy Token_Type]) [EToken meta ts]
 136  | Token_Term_List_zipWith   (EToken meta ts)
 137 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy []))
 138 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy []))
 139 instance -- CompileI
 140  ( Read_TypeName Type_Name (Consts_of_Ifaces is)
 141  , Inj_Const (Consts_of_Ifaces is) []
 142  , Inj_Const (Consts_of_Ifaces is) (->)
 143  , Compile is
 144  ) => CompileI is (Proxy []) where
 145         compileI
 146          :: forall meta ctx ret ls rs.
 147          TokenT meta is (Proxy [])
 148          -> CompileT meta ctx ret is ls (Proxy [] ': rs)
 149         compileI tok ctx k =
 150                 case tok of
 151                  Token_Term_List_empty tok_ty_a ->
 152                         -- [] :: [a]
 153                         compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
 154                         check_kind
 155                          (At Nothing SKiType)
 156                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 157                         k (ty @[] :$ ty_a) $ TermO $
 158                                 Fun.const list_empty
 159                  Token_Term_List_singleton tok_a ->
 160                         -- [a] :: [a]
 161                         compileO tok_a ctx $ \ty_a (TermO a) ->
 162                         check_kind
 163                          (At Nothing SKiType)
 164                          (At (Just tok_a) $ kind_of ty_a) $ \Refl ->
 165                         k (ty @[] :$ ty_a) $ TermO $
 166                          \c -> list_singleton (a c)
 167                  Token_Term_List_cons tok_a tok_as ->
 168                         compileO tok_a ctx $ \ty_a (TermO a) ->
 169                         compileO tok_as ctx $ \ty_as (TermO as) ->
 170                         check_type1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_as_a ->
 171                         check_type (At (Just tok_a) ty_a) (At (Just tok_as) ty_as_a) $ \Refl ->
 172                         k ty_as $ TermO $
 173                          \c -> a c .: as c
 174                  Token_Term_List_list tok_ty_a tok_as ->
 175                         compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
 176                         check_kind
 177                          (At Nothing SKiType)
 178                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 179                         go (At (Just tok_ty_a) ty_a) [] tok_as
 180                         where
 181                         go :: At meta '[Proxy Token_Type] (Type (Consts_of_Ifaces is) ty_a)
 182                            -> [TermO ctx ty_a is '[] is]
 183                            -> [EToken meta is]
 184                            -> Either (Error_Term meta is) ret
 185                         go ty_a as [] =
 186                                 k (ty @[] :$ unAt ty_a) $ TermO $
 187                                  \c -> list $ (\(TermO a) -> a c)
 188                                          Functor.<$> List.reverse as
 189                         go ty_a as (tok_x:tok_xs) =
 190                                 compileO tok_x ctx $ \ty_x x ->
 191                                 check_type_is ty_a (At (Just tok_x) ty_x) $ \Refl ->
 192                                 go ty_a (x:as) tok_xs
 193                  Token_Term_List_zipWith tok_a2b2c ->
 194                         -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
 195                         compileO tok_a2b2c ctx $ \ty_a2b2c (TermO a2b2c) ->
 196                         check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c) $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
 197                         check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c_b2c) $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
 198                         k ( ty @[] :$ ty_a2b2c_a
 199                          ~> ty @[] :$ ty_a2b2c_b2c_b
 200                          ~> ty @[] :$ ty_a2b2c_b2c_c ) $ TermO $
 201                          \c -> lam $ lam . zipWith (a2b2c c)
 202 instance -- TokenizeT
 203  Inj_Token meta ts [] =>
 204  TokenizeT meta ts (Proxy []) where
 205         tokenizeT _t = mempty
 206          { tokenizers_infix = tokenizeTMod []
 207                  [ (Term_Name "[]",) $ Term_ProTok
 208                          { term_protok = \meta -> ProTokPi $ \a ->
 209                                 ProTok $ inj_etoken meta $ Token_Term_List_empty a
 210                          , term_fixity = infixN5
 211                          }
 212                  , tokenize2 ":" (infixR 5) Token_Term_List_cons
 213                  , tokenize1 "zipWith" infixN0 Token_Term_List_zipWith
 214                  ]
 215          }
 216 instance
 217  ( App g
 218  , Gram_Rule g
 219  , Gram_Lexer g
 220  , Gram_Term ts meta g
 221  , Inj_Token meta ts (->)
 222  , Inj_Token meta ts []
 223  ) => Gram_Term_AtomsT meta ts (Proxy []) g where
 224         term_atomsT _t =
 225          [ rule "term_list" $
 226                 ProTok <$> between (symbol "[") (symbol "]") listG
 227          , rule "term_list_empty" $
 228                 metaG $
 229                 (\meta -> ProTokPi $ \a -> ProTok $ inj_etoken meta $ Token_Term_List_empty a)
 230                  <$ symbol "["
 231                  <* symbol "]"
 232          ]
 233                 where
 234                 listG :: CF g (EToken meta ts)
 235                 listG = rule "list" $
 236                         metaG $
 237                         (\a mb meta -> inj_etoken meta $ case mb of
 238                          Just b  -> Token_Term_List_cons a b
 239                          Nothing -> Token_Term_List_singleton a)
 240                          <$> termG
 241                          <*> option Nothing (Just <$ symbol "," <*> listG)