Language/Symantic/Compiling/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.Compiling.List where
   6
   7 import Control.Monad (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 Data.Text (Text)
  15 import qualified Data.Text as Text
  16 import qualified Data.Traversable as Traversable
  17 import Data.Type.Equality ((:~:)(Refl))
  18 import Prelude hiding (zipWith)
  19
  20 import Language.Symantic.Parsing
  21 import Language.Symantic.Typing
  22 import Language.Symantic.Compiling.Term
  23 import Language.Symantic.Interpreting
  24 import Language.Symantic.Transforming.Trans
  25
  26 -- * Class 'Sym_List'
  27 class Sym_List term where
  28         list_empty :: term [a]
  29         zipWith    :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
  30         list       :: [term a] -> term [a]
  31
  32         default list_empty :: Trans t term => t term [a]
  33         default zipWith    :: Trans t term => t term (a -> b -> c) -> t term [a] -> t term [b] -> t term [c]
  34         default list       :: Trans t term => [t term a] -> t term [a]
  35
  36         list_empty = trans_lift list_empty
  37         zipWith    = trans_map3 zipWith
  38         list l     = trans_lift (list (trans_apply Functor.<$> l))
  39
  40 type instance Sym_of_Iface (Proxy []) = Sym_List
  41 type instance Consts_of_Iface (Proxy []) = Proxy [] ': Consts_imported_by []
  42 type instance Consts_imported_by [] =
  43  [ Proxy Applicative
  44  , Proxy Bool
  45  , Proxy Eq
  46  , Proxy Foldable
  47  , Proxy Functor
  48  , Proxy Monad
  49  , Proxy Monoid
  50  , Proxy Ord
  51  , Proxy Show
  52  , Proxy Traversable
  53  ]
  54
  55 instance Sym_List HostI where
  56         list_empty = return []
  57         list       = Traversable.sequence
  58         zipWith    = liftM3 List.zipWith
  59 instance Sym_List TextI where
  60         list_empty = TextI $ \_p _v -> "[]"
  61         list l = TextI $ \_p v ->
  62                 let p' = precedence_Toplevel in
  63                 "[" <> Text.intercalate ", " ((\(TextI a) -> a p' v) Functor.<$> l) <> "]"
  64         zipWith = textI_app3 "zipWith"
  65 instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
  66         list_empty = dupI0 (Proxy @Sym_List) list_empty
  67         list l =
  68                 let (l1, l2) =
  69                         Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) ->
  70                                 (x1:xs1, x2:xs2)) ([], []) l in
  71                 list l1 `DupI` list l2
  72         zipWith = dupI3 (Proxy @Sym_List) zipWith
  73
  74 instance Const_from Text cs => Const_from Text (Proxy [] ': cs) where
  75         const_from "[]" k = k (ConstZ kind)
  76         const_from s k = const_from s $ k . ConstS
  77 instance Show_Const cs => Show_Const (Proxy [] ': cs) where
  78         show_const ConstZ{} = "[]"
  79         show_const (ConstS c) = show_const c
  80 instance Const_from String cs => Const_from String (Proxy String ': cs) where
  81         const_from "String" k = k (ConstZ kind)
  82         const_from s k = const_from s $ k . ConstS
  83 instance Show_Const cs => Show_Const (Proxy String ': cs) where
  84         show_const ConstZ{} = "String"
  85         show_const (ConstS c) = show_const c
  86
  87 instance -- Proj_ConC
  88  ( Proj_Const cs []
  89  , Proj_Consts cs (Consts_imported_by [])
  90  , Proj_Con cs
  91  ) => Proj_ConC cs (Proxy []) where
  92         proj_conC _ (TyConst q :$ TyConst c)
  93          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  94          , Just Refl <- proj_const c (Proxy::Proxy [])
  95          = case () of
  96                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
  97                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
  98                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
  99                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 100                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
 101                  _ -> Nothing
 102         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
 103          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 104          , Just Refl <- proj_const c (Proxy::Proxy [])
 105          = case () of
 106                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
 107                    , Just Con  <- proj_con (t :$ a) -> Just Con
 108                    | Just Refl <- proj_const q (Proxy::Proxy Monoid) -> Just Con
 109                    | Just Refl <- proj_const q (Proxy::Proxy Show)
 110                    , Just Con  <- proj_con (t :$ a) -> Just Con
 111                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
 112                    , Just Con  <- proj_con (t :$ a) -> Just Con
 113                  _ -> Nothing
 114         proj_conC _c _q = Nothing
 115 data instance TokenT meta (ts::[*]) (Proxy [])
 116  = Token_Term_List_empty   (EToken meta '[Proxy Token_Type])
 117  | Token_Term_List_list    (EToken meta '[Proxy Token_Type]) [EToken meta ts]
 118  | Token_Term_List_zipWith (EToken meta ts)
 119 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy []))
 120 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy []))
 121 instance -- Term_fromI
 122  ( Const_from Name_LamVar (Consts_of_Ifaces is)
 123  , Inj_Const (Consts_of_Ifaces is) []
 124  , Inj_Const (Consts_of_Ifaces is) (->)
 125  , Term_from is
 126  ) => Term_fromI is (Proxy []) where
 127         term_fromI
 128          :: forall meta ctx ret ls rs.
 129          TokenT meta is (Proxy [])
 130          -> Term_fromT meta ctx ret is ls (Proxy [] ': rs)
 131         term_fromI tok ctx k =
 132                 case tok of
 133                  Token_Term_List_empty tok_ty_a ->
 134                         -- [] :: [a]
 135                         type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
 136                         check_kind
 137                          (At Nothing SKiType)
 138                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 139                         k (ty @[] :$ ty_a) $ TermLC $
 140                                 Fun.const list_empty
 141                  Token_Term_List_list tok_ty_a tok_as ->
 142                         type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
 143                         check_kind
 144                          (At Nothing SKiType)
 145                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 146                         go (At (Just tok_ty_a) ty_a) [] tok_as
 147                         where
 148                         go :: At meta '[Proxy Token_Type] (Type (Consts_of_Ifaces is) ty_a)
 149                            -> [TermLC ctx ty_a is '[] is]
 150                            -> [EToken meta is]
 151                            -> Either (Error_Term meta is) ret
 152                         go ty_a as [] =
 153                                 k (ty @[] :$ unAt ty_a) $ TermLC $
 154                                  \c -> list $ (\(TermLC a) -> a c)
 155                                          Functor.<$> List.reverse as
 156                         go ty_a as (tok_x:tok_xs) =
 157                                 term_from tok_x ctx $ \ty_x x ->
 158                                 check_type_is ty_a (At (Just tok_x) ty_x) $ \Refl ->
 159                                 go ty_a (x:as) tok_xs
 160                  Token_Term_List_zipWith tok_a2b2c ->
 161                         -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
 162                         term_from tok_a2b2c ctx $ \ty_a2b2c (TermLC a2b2c) ->
 163                         check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c) $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
 164                         check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c_b2c) $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
 165                         k ( ty @[] :$ ty_a2b2c_a
 166                          ~> ty @[] :$ ty_a2b2c_b2c_b
 167                          ~> ty @[] :$ ty_a2b2c_b2c_c ) $ TermLC $
 168                          \c -> lam $ lam . zipWith (a2b2c c)