Language/Symantic/Compiling/List.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
   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 Traversable
  52  ]
  53
  54 instance Sym_List HostI where
  55         list_empty = return []
  56         list       = Traversable.sequence
  57         zipWith    = liftM3 List.zipWith
  58 instance Sym_List TextI where
  59         list_empty = TextI $ \_p _v -> "[]"
  60         list l = TextI $ \_p v ->
  61                 let p' = precedence_Toplevel in
  62                 "[" <> Text.intercalate ", " ((\(TextI a) -> a p' v) Functor.<$> l) <> "]"
  63         zipWith = textI_app3 "zipWith"
  64 instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
  65         list_empty = dupI0 (Proxy @Sym_List) list_empty
  66         list l =
  67                 let (l1, l2) =
  68                         Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) ->
  69                                 (x1:xs1, x2:xs2)) ([], []) l in
  70                 list l1 `DupI` list l2
  71         zipWith = dupI3 (Proxy @Sym_List) zipWith
  72
  73 instance Const_from Text cs => Const_from Text (Proxy [] ': cs) where
  74         const_from "[]" k = k (ConstZ kind)
  75         const_from s k = const_from s $ k . ConstS
  76 instance Show_Const cs => Show_Const (Proxy [] ': cs) where
  77         show_const ConstZ{} = "[]"
  78         show_const (ConstS c) = show_const c
  79
  80 instance -- Proj_ConC
  81  ( Proj_Const cs []
  82  , Proj_Consts cs (Consts_imported_by [])
  83  , Proj_Con cs
  84  ) => Proj_ConC cs (Proxy []) where
  85         proj_conC _ (TyConst q :$ TyConst c)
  86          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  87          , Just Refl <- proj_const c (Proxy::Proxy [])
  88          = case () of
  89                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
  90                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
  91                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
  92                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
  93                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
  94                  _ -> Nothing
  95         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
  96          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  97          , Just Refl <- proj_const c (Proxy::Proxy [])
  98          = case () of
  99                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
 100                    , Just Con  <- proj_con (t :$ a) -> Just Con
 101                    | Just Refl <- proj_const q (Proxy::Proxy Monoid) -> Just Con
 102                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
 103                    , Just Con  <- proj_con (t :$ a) -> Just Con
 104                  _ -> Nothing
 105         proj_conC _c _q = Nothing
 106 data instance TokenT meta (ts::[*]) (Proxy [])
 107  = Token_Term_List_empty   (EToken meta '[Proxy Token_Type])
 108  | Token_Term_List_list    (EToken meta '[Proxy Token_Type]) [EToken meta ts]
 109  | Token_Term_List_zipWith (EToken meta ts)
 110 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy []))
 111 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy []))
 112 instance -- Term_fromI
 113  ( Const_from Name_LamVar (Consts_of_Ifaces is)
 114  , Inj_Const (Consts_of_Ifaces is) []
 115  , Inj_Const (Consts_of_Ifaces is) (->)
 116  , Term_from is
 117  ) => Term_fromI is (Proxy []) where
 118         term_fromI
 119          :: forall meta ctx ret ls rs.
 120          TokenT meta is (Proxy [])
 121          -> Term_fromT meta ctx ret is ls (Proxy [] ': rs)
 122         term_fromI tok ctx k =
 123                 case tok of
 124                  Token_Term_List_empty tok_ty_a ->
 125                         -- [] :: [a]
 126                         type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
 127                         check_kind
 128                          (At Nothing SKiType)
 129                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 130                         k (ty @[] :$ ty_a) $ TermLC $
 131                                 Fun.const list_empty
 132                  Token_Term_List_list tok_ty_a tok_as ->
 133                         type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
 134                         check_kind
 135                          (At Nothing SKiType)
 136                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 137                         go (At (Just tok_ty_a) ty_a) [] tok_as
 138                         where
 139                         go :: At meta '[Proxy Token_Type] (Type (Consts_of_Ifaces is) ty_a)
 140                            -> [TermLC ctx ty_a is '[] is]
 141                            -> [EToken meta is]
 142                            -> Either (Error_Term meta is) ret
 143                         go ty_a as [] =
 144                                 k (ty @[] :$ unAt ty_a) $ TermLC $
 145                                  \c -> list $ (\(TermLC a) -> a c)
 146                                          Functor.<$> List.reverse as
 147                         go ty_a as (tok_x:tok_xs) =
 148                                 term_from tok_x ctx $ \ty_x x ->
 149                                 check_type_is ty_a (At (Just tok_x) ty_x) $ \Refl ->
 150                                 go ty_a (x:as) tok_xs
 151                  Token_Term_List_zipWith tok_a2b2c ->
 152                         -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
 153                         term_from tok_a2b2c ctx $ \ty_a2b2c (TermLC a2b2c) ->
 154                         check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c) $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
 155                         check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c_b2c) $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
 156                         k ( ty @[] :$ ty_a2b2c_a
 157                          ~> ty @[] :$ ty_a2b2c_b2c_b
 158                          ~> ty @[] :$ ty_a2b2c_b2c_c ) $ TermLC $
 159                          \c -> lam $ lam . zipWith (a2b2c c)