Language/Symantic/Compiling/Sequences.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE DefaultSignatures #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE InstanceSigs #-}
   7 {-# LANGUAGE MultiParamTypeClasses #-}
   8 {-# LANGUAGE OverloadedStrings #-}
   9 {-# LANGUAGE PolyKinds #-}
  10 {-# LANGUAGE Rank2Types #-}
  11 {-# LANGUAGE ScopedTypeVariables #-}
  12 {-# LANGUAGE TypeFamilies #-}
  13 {-# LANGUAGE TypeOperators #-}
  14 {-# LANGUAGE UndecidableInstances #-}
  15 {-# OPTIONS_GHC -fno-warn-orphans #-}
  16 -- | Symantic for 'Sequences'.
  17 module Language.Symantic.Compiling.Sequences where
  18
  19 import Control.Monad (liftM, liftM2)
  20 import qualified Data.MonoTraversable as MT
  21 import Data.Proxy
  22 import Data.Sequences (SemiSequence, IsSequence)
  23 import qualified Data.Sequences as Seqs
  24 import Data.String (IsString)
  25 import Data.Text (Text)
  26 import Data.Type.Equality ((:~:)(Refl))
  27 import Prelude hiding (filter, reverse)
  28
  29 import Language.Symantic.Typing
  30 import Language.Symantic.Compiling.Term
  31 import Language.Symantic.Compiling.Bool (tyBool)
  32 import Language.Symantic.Compiling.MonoFunctor (Fam_MonoElement(..))
  33 import Language.Symantic.Interpreting
  34 import Language.Symantic.Transforming.Trans
  35
  36 -- * Class 'Sym_SemiSequence'
  37 class Sym_SemiSequence term where
  38         intersperse :: SemiSequence s => term (MT.Element s) -> term s -> term s
  39         cons :: SemiSequence s => term (MT.Element s) -> term s -> term s
  40         snoc :: SemiSequence s => term s -> term (MT.Element s) -> term s
  41         reverse :: SemiSequence s => term s -> term s
  42         default intersperse :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term s
  43         default cons :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term s
  44         default snoc :: (Trans t term, SemiSequence s) => t term s -> t term (MT.Element s) -> t term s
  45         default reverse :: (Trans t term, SemiSequence s) => t term s -> t term s
  46         intersperse = trans_map2 cons
  47         cons        = trans_map2 cons
  48         snoc        = trans_map2 snoc
  49         reverse     = trans_map1 reverse
  50
  51 type instance Sym_of_Iface (Proxy SemiSequence) = Sym_SemiSequence
  52 type instance Consts_of_Iface (Proxy SemiSequence) = Proxy SemiSequence ': Consts_imported_by SemiSequence
  53 type instance Consts_imported_by SemiSequence =
  54  [ Proxy SemiSequence
  55  , Proxy []
  56  , Proxy Text
  57  ]
  58
  59 instance Sym_SemiSequence HostI where
  60         intersperse = liftM2 Seqs.intersperse
  61         cons        = liftM2 Seqs.cons
  62         snoc        = liftM2 Seqs.snoc
  63         reverse     = liftM  Seqs.reverse
  64 instance Sym_SemiSequence TextI where
  65         intersperse = textI_app2 "intersperse"
  66         cons        = textI_app2 "cons"
  67         snoc        = textI_app2 "snoc"
  68         reverse     = textI_app1 "reverse"
  69 instance (Sym_SemiSequence r1, Sym_SemiSequence r2) => Sym_SemiSequence (DupI r1 r2) where
  70         intersperse = dupI2 sym_SemiSequence intersperse
  71         cons        = dupI2 sym_SemiSequence cons
  72         snoc        = dupI2 sym_SemiSequence snoc
  73         reverse     = dupI1 sym_SemiSequence reverse
  74
  75 instance Const_from Text cs => Const_from Text (Proxy SemiSequence ': cs) where
  76         const_from "SemiSequence" k = k (ConstZ kind)
  77         const_from s k = const_from s $ k . ConstS
  78 instance Show_Const cs => Show_Const (Proxy SemiSequence ': cs) where
  79         show_const ConstZ{} = "SemiSequence"
  80         show_const (ConstS c) = show_const c
  81
  82 instance -- Proj_ConC
  83  ( Proj_Const cs SemiSequence
  84  , Proj_Consts cs (Consts_imported_by SemiSequence)
  85  ) => Proj_ConC cs (Proxy SemiSequence) where
  86         proj_conC _ (TyConst q :$ s)
  87          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
  88          , Just Refl <- proj_const q (Proxy::Proxy SemiSequence)
  89          = case s of
  90                  TyConst c
  91                   | Just Refl <- eq_skind (kind_of_const c) SKiType ->
  92                         case () of
  93                          _ | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
  94                          _ -> Nothing
  95                  TyConst c :$ _o
  96                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) ->
  97                         case () of
  98                          _ | Just Refl <- proj_const c (Proxy::Proxy []) -> Just Con
  99                          _ -> Nothing
 100                  _ -> Nothing
 101         proj_conC _c _q = Nothing
 102 instance -- Term_fromI
 103  ( AST ast
 104  , Lexem ast ~ LamVarName
 105  , Inj_Const (Consts_of_Ifaces is) SemiSequence
 106  , Proj_Con  (Consts_of_Ifaces is)
 107  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 108  , Term_from is ast
 109  ) => Term_fromI is (Proxy SemiSequence) ast where
 110         term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy SemiSequence ': rs)
 111         term_fromI ast ctx k =
 112                 case ast_lexem ast of
 113                  "intersperse" -> e2s2s_from intersperse
 114                  "cons"        -> e2s2s_from cons
 115                  "snoc"        -> snoc_from
 116                  "reverse"     -> reverse_from
 117                  _ -> Left $ Error_Term_unsupported
 118                 where
 119                 e2s2s_from
 120                  (f::forall term s.
 121                          (Sym_SemiSequence term, SemiSequence s)
 122                          => term (MT.Element s) -> term s -> term s) =
 123                  -- intersperse :: SemiSequence s => MT.Element s -> s -> s
 124                  -- cons        :: SemiSequence s => MT.Element s -> s -> s
 125                         from_ast2 ast $ \ast_e ast_s as ->
 126                         term_from ast_e ctx $ \ty_e (TermLC e) ->
 127                         term_from ast_s ctx $ \ty_s (TermLC s) ->
 128                         check_constraint (At (Just ast_s) (tySemiSequence :$ ty_s)) $ \Con ->
 129                         check_family ast Fam_MonoElement (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 130                         check_type (At Nothing ty_s_e) (At (Just ast_e) ty_e) $ \Refl ->
 131                         k as ty_s $ TermLC $
 132                          \c -> f (e c) (s c)
 133                 snoc_from =
 134                  -- snoc :: SemiSequence s => s -> MT.Element s -> s
 135                         from_ast2 ast $ \ast_s ast_e as ->
 136                         term_from ast_s ctx $ \ty_s (TermLC s) ->
 137                         term_from ast_e ctx $ \ty_e (TermLC e) ->
 138                         check_constraint (At (Just ast_s) (tySemiSequence :$ ty_s)) $ \Con ->
 139                         check_family ast Fam_MonoElement (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 140                         check_type (At Nothing ty_s_e) (At (Just ast_e) ty_e) $ \Refl ->
 141                         k as ty_s $ TermLC $
 142                          \c -> snoc (s c) (e c)
 143                 reverse_from =
 144                  -- reverse :: SemiSequence s => s -> s
 145                         from_ast1 ast $ \ast_s as ->
 146                         term_from ast_s ctx $ \ty_s (TermLC s) ->
 147                         check_constraint (At (Just ast_s) (tySemiSequence :$ ty_s)) $ \Con ->
 148                         k as ty_s $ TermLC $
 149                          \c -> reverse (s c)
 150
 151 -- | The 'SemiSequence' 'Type'
 152 tySemiSequence :: Inj_Const cs SemiSequence => Type cs SemiSequence
 153 tySemiSequence = TyConst inj_const
 154
 155 sym_SemiSequence :: Proxy Sym_SemiSequence
 156 sym_SemiSequence = Proxy
 157
 158 sySemiSequence :: IsString a => [Syntax a] -> Syntax a
 159 sySemiSequence = Syntax "SemiSequence"
 160
 161 -- * Class 'Sym_IsSequence'
 162 class Sym_IsSequence term where
 163         filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
 164         default filter :: (Trans t term, IsSequence s) => t term (MT.Element s -> Bool) -> t term s -> t term s
 165         filter  = trans_map2 filter
 166
 167 type instance Sym_of_Iface (Proxy IsSequence) = Sym_IsSequence
 168 type instance Consts_of_Iface (Proxy IsSequence) = Proxy IsSequence ': Consts_imported_by IsSequence
 169 type instance Consts_imported_by IsSequence =
 170  [ Proxy IsSequence
 171  , Proxy (->)
 172  , Proxy []
 173  , Proxy Text
 174  , Proxy Bool
 175  ]
 176
 177 instance Sym_IsSequence HostI where
 178         filter  = liftM2 Seqs.filter
 179 instance Sym_IsSequence TextI where
 180         filter  = textI_app2 "filter"
 181 instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (DupI r1 r2) where
 182         filter  = dupI2 sym_IsSequence filter
 183
 184 instance Const_from Text cs => Const_from Text (Proxy IsSequence ': cs) where
 185         const_from "IsSequence" k = k (ConstZ kind)
 186         const_from s k = const_from s $ k . ConstS
 187 instance Show_Const cs => Show_Const (Proxy IsSequence ': cs) where
 188         show_const ConstZ{} = "IsSequence"
 189         show_const (ConstS c) = show_const c
 190
 191 instance -- Proj_ConC
 192  ( Proj_Const cs IsSequence
 193  , Proj_Consts cs (Consts_imported_by IsSequence)
 194  ) => Proj_ConC cs (Proxy IsSequence) where
 195         proj_conC _ (TyConst q :$ s)
 196          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
 197          , Just Refl <- proj_const q (Proxy::Proxy IsSequence)
 198          = case s of
 199                  TyConst c
 200                   | Just Refl <- eq_skind (kind_of_const c) SKiType ->
 201                         case () of
 202                          _ | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
 203                          _ -> Nothing
 204                  TyConst c :$ _o
 205                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) ->
 206                         case () of
 207                          _ | Just Refl <- proj_const c (Proxy::Proxy []) -> Just Con
 208                          _ -> Nothing
 209                  _ -> Nothing
 210         proj_conC _c _q = Nothing
 211 instance -- Term_fromI
 212  ( AST ast
 213  , Lexem ast ~ LamVarName
 214  , Inj_Const (Consts_of_Ifaces is) IsSequence
 215  , Inj_Const (Consts_of_Ifaces is) (->)
 216  , Inj_Const (Consts_of_Ifaces is) Bool
 217  , Proj_Con  (Consts_of_Ifaces is)
 218  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 219  , Term_from is ast
 220  ) => Term_fromI is (Proxy IsSequence) ast where
 221         term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy IsSequence ': rs)
 222         term_fromI ast ctx k =
 223                 case ast_lexem ast of
 224                  "filter" -> filter_from
 225                  _ -> Left $ Error_Term_unsupported
 226                 where
 227                 filter_from =
 228                  -- filter :: IsSequence s => (MT.Element s -> Bool) -> s -> s
 229                         from_ast2 ast $ \ast_e2Bool ast_s as ->
 230                         term_from ast_e2Bool ctx $ \ty_e2Bool (TermLC e2Bool) ->
 231                         term_from ast_s      ctx $ \ty_s      (TermLC s) ->
 232                         check_type2 tyFun ast_e2Bool ty_e2Bool $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
 233                         check_type (At Nothing tyBool) (At (Just ast_e2Bool) ty_e2Bool_Bool) $ \Refl ->
 234                         check_constraint (At (Just ast_s) (tyIsSequence :$ ty_s)) $ \Con ->
 235                         check_family ast Fam_MonoElement (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 236                         check_type (At Nothing ty_s_e) (At (Just ast_e2Bool) ty_e2Bool_e) $ \Refl ->
 237                         k as ty_s $ TermLC $
 238                          \c -> filter (e2Bool c) (s c)
 239
 240 -- | The 'IsSequence' 'Type'
 241 tyIsSequence :: Inj_Const cs IsSequence => Type cs IsSequence
 242 tyIsSequence = TyConst inj_const
 243
 244 sym_IsSequence :: Proxy Sym_IsSequence
 245 sym_IsSequence = Proxy
 246
 247 syIsSequence :: IsString a => [Syntax a] -> Syntax a
 248 syIsSequence = Syntax "IsSequence"