Language/Symantic/Compiling/NonNull.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 {-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
  17 -- | Symantic for 'NonNull'.
  18 module Language.Symantic.Compiling.NonNull where
  19
  20 import Control.Monad (liftM, liftM2)
  21 import Data.MonoTraversable (MonoFoldable)
  22 import qualified Data.MonoTraversable as MT
  23 import Data.NonNull (NonNull)
  24 import qualified Data.NonNull as NonNull
  25 import Data.Proxy
  26 import Data.Sequences (IsSequence, SemiSequence)
  27 import Data.String (IsString)
  28 import Data.Text (Text)
  29 import Data.Type.Equality ((:~:)(Refl))
  30 import Prelude hiding (head, init, last, tail)
  31
  32 import Language.Symantic.Typing
  33 import Language.Symantic.Compiling.Term
  34 import Language.Symantic.Compiling.Bool (tyBool)
  35 import Language.Symantic.Compiling.Maybe (tyMaybe)
  36 import Language.Symantic.Compiling.Tuple2 (tyTuple2)
  37 import Language.Symantic.Compiling.MonoFunctor
  38 import Language.Symantic.Compiling.MonoFoldable
  39 import Language.Symantic.Compiling.Sequences (tyIsSequence, tySemiSequence)
  40 import Language.Symantic.Interpreting
  41 import Language.Symantic.Transforming.Trans
  42
  43 -- * Class 'Sym_NonNull'
  44 class Sym_NonNull term where
  45         fromNullable :: MonoFoldable o => term o -> term (Maybe (NonNull o))
  46         toNullable :: MonoFoldable o => term (NonNull o) -> term o
  47         ncons :: SemiSequence s => term (MT.Element s) -> term s -> term (NonNull s)
  48         nuncons :: IsSequence s => term (NonNull s) -> term (MT.Element s, Maybe (NonNull s))
  49         head :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
  50         last :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
  51         tail :: IsSequence s => term (NonNull s) -> term s
  52         init :: IsSequence s => term (NonNull s) -> term s
  53         nfilter :: IsSequence s => term (MT.Element s -> Bool) -> term (NonNull s) -> term s
  54         default fromNullable :: (Trans t term, MonoFoldable o) => t term o -> t term (Maybe (NonNull o))
  55         default toNullable :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term o
  56         default ncons :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term (NonNull s)
  57         default nuncons :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term (MT.Element s, Maybe (NonNull s))
  58         default head :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term (MT.Element o)
  59         default last :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term (MT.Element o)
  60         default tail :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term s
  61         default init :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term s
  62         default nfilter :: (Trans t term, IsSequence s) => t term (MT.Element s -> Bool) -> t term (NonNull s) -> t term s
  63         fromNullable = trans_map1 fromNullable
  64         toNullable   = trans_map1 toNullable
  65         ncons        = trans_map2 ncons
  66         nuncons      = trans_map1 nuncons
  67         head         = trans_map1 head
  68         last         = trans_map1 last
  69         tail         = trans_map1 tail
  70         init         = trans_map1 init
  71         nfilter      = trans_map2 nfilter
  72
  73 type instance Sym_of_Iface (Proxy NonNull) = Sym_NonNull
  74 type instance Consts_of_Iface (Proxy NonNull) = Proxy NonNull ': Consts_imported_by NonNull
  75 type instance Consts_imported_by NonNull =
  76  [ Proxy (->)
  77  , Proxy (,)
  78  , Proxy Eq
  79  , Proxy Maybe
  80  , Proxy Ord
  81  , Proxy MT.MonoFoldable
  82  , Proxy MT.MonoFunctor
  83  , Proxy IsSequence
  84  , Proxy SemiSequence
  85  ]
  86
  87 instance Sym_NonNull HostI where
  88         fromNullable = liftM  NonNull.fromNullable
  89         toNullable   = liftM  NonNull.toNullable
  90         ncons        = liftM2 NonNull.ncons
  91         nuncons      = liftM  NonNull.nuncons
  92         head         = liftM  NonNull.head
  93         last         = liftM  NonNull.last
  94         tail         = liftM  NonNull.tail
  95         init         = liftM  NonNull.init
  96         nfilter      = liftM2 NonNull.nfilter
  97 instance Sym_NonNull TextI where
  98         fromNullable = textI_app1 "fromNullable"
  99         toNullable   = textI_app1 "toNullable"
 100         ncons        = textI_app2 "ncons"
 101         nuncons      = textI_app1 "nuncons"
 102         head         = textI_app1 "head"
 103         last         = textI_app1 "last"
 104         tail         = textI_app1 "tail"
 105         init         = textI_app1 "init"
 106         nfilter      = textI_app2 "nfilter"
 107 instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (DupI r1 r2) where
 108         fromNullable = dupI1 sym_NonNull fromNullable
 109         toNullable   = dupI1 sym_NonNull toNullable
 110         ncons        = dupI2 sym_NonNull ncons
 111         nuncons      = dupI1 sym_NonNull nuncons
 112         head         = dupI1 sym_NonNull head
 113         last         = dupI1 sym_NonNull last
 114         tail         = dupI1 sym_NonNull tail
 115         init         = dupI1 sym_NonNull init
 116         nfilter      = dupI2 sym_NonNull nfilter
 117
 118 instance Const_from Text cs => Const_from Text (Proxy NonNull ': cs) where
 119         const_from "NonNull" k = k (ConstZ kind)
 120         const_from s k = const_from s $ k . ConstS
 121 instance Show_Const cs => Show_Const (Proxy NonNull ': cs) where
 122         show_const ConstZ{} = "NonNull"
 123         show_const (ConstS c) = show_const c
 124
 125 instance -- Fam_MonoElement
 126  ( Proj_Const cs NonNull
 127  , Proj_Fam cs Fam_MonoElement
 128  ) => Proj_FamC cs Fam_MonoElement NonNull where
 129         proj_famC _c _fam ((TyConst c :$ ty_o) `TypesS` TypesZ)
 130          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 131          , Just Refl <- proj_const c (Proxy::Proxy NonNull)
 132          = proj_fam Fam_MonoElement (ty_o `TypesS` TypesZ)
 133         proj_famC _c _fam _ty = Nothing
 134 instance -- Proj_ConC
 135  ( Proj_Const cs NonNull
 136  , Proj_Consts cs (Consts_imported_by NonNull)
 137  , Proj_Con cs
 138  ) => Proj_ConC cs (Proxy NonNull) where
 139         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ o))
 140          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 141          , Just Refl <- proj_const c (Proxy::Proxy NonNull)
 142          = case () of
 143                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
 144                    , Just Con  <- proj_con (t :$ o) -> Just Con
 145                    | Just Refl <- proj_const q (Proxy::Proxy MT.MonoFoldable)
 146                    , Just Con  <- proj_con (t :$ o) -> Just Con
 147                    | Just Refl <- proj_const q (Proxy::Proxy MT.MonoFunctor)
 148                    , Just Con  <- proj_con (t :$ o) -> Just Con
 149                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
 150                    , Just Con  <- proj_con (t :$ o) -> Just Con
 151                    | Just Refl <- proj_const q (Proxy::Proxy SemiSequence)
 152                    , Just Con  <- proj_con (t :$ o) -> Just Con
 153                  _ -> Nothing
 154         proj_conC _c _q = Nothing
 155 instance -- Term_fromI
 156  ( AST ast
 157  , Lexem ast ~ LamVarName
 158  , Inj_Const (Consts_of_Ifaces is) NonNull
 159  , Inj_Const (Consts_of_Ifaces is) (->)
 160  , Inj_Const (Consts_of_Ifaces is) (,)
 161  , Inj_Const (Consts_of_Ifaces is) Bool
 162  , Inj_Const (Consts_of_Ifaces is) Maybe
 163  , Inj_Const (Consts_of_Ifaces is) MonoFoldable
 164  , Inj_Const (Consts_of_Ifaces is) IsSequence
 165  , Inj_Const (Consts_of_Ifaces is) SemiSequence
 166  , Proj_Con  (Consts_of_Ifaces is)
 167  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 168  , Term_from is ast
 169  ) => Term_fromI is (Proxy NonNull) ast where
 170         term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy NonNull ': rs)
 171         term_fromI ast ctx k =
 172                 case ast_lexem ast of
 173                  "fromNullable" -> fromNullable_from
 174                  "toNullable"   -> toNullable_from
 175                  "ncons"        -> ncons_from
 176                  "nuncons"      -> nuncons_from
 177                  "head"         -> n2e_from head
 178                  "last"         -> n2e_from last
 179                  "tail"         -> n2s_from tail
 180                  "init"         -> n2s_from init
 181                  "nfilter"      -> nfilter_from
 182                  _ -> Left $ Error_Term_unsupported
 183                 where
 184                 fromNullable_from =
 185                  -- fromNullable :: MonoFoldable o => o -> Maybe (NonNull o)
 186                         from_ast1 ast $ \ast_o as ->
 187                         term_from ast_o ctx $ \ty_o (TermLC o) ->
 188                         check_constraint (At (Just ast_o) (tyMonoFoldable :$ ty_o)) $ \Con ->
 189                         k as (tyMaybe :$ (tyNonNull :$ ty_o)) $ TermLC $
 190                          \c -> fromNullable (o c)
 191                 toNullable_from =
 192                  -- toNullable :: MonoFoldable o => NonNull o -> o
 193                         from_ast1 ast $ \ast_n as ->
 194                         term_from ast_n ctx $ \ty_n (TermLC n) ->
 195                         check_type1 tyNonNull ast_n ty_n $ \Refl ty_o ->
 196                         check_constraint (At (Just ast_n) (tyMonoFoldable :$ ty_o)) $ \Con ->
 197                         k as ty_o $ TermLC $
 198                          \c -> toNullable (n c)
 199                 ncons_from =
 200                  -- ncons :: SemiSequence s => MT.Element s -> s -> NonNull s
 201                         from_ast2 ast $ \ast_e ast_s as ->
 202                         term_from ast_e ctx $ \ty_e (TermLC e) ->
 203                         term_from ast_s ctx $ \ty_s (TermLC s) ->
 204                         check_constraint (At (Just ast_s) (tySemiSequence :$ ty_s)) $ \Con ->
 205                         check_family ast Fam_MonoElement (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 206                         check_type (At Nothing ty_s_e) (At (Just ast_e) ty_e) $ \Refl ->
 207                         k as (tyNonNull :$ ty_s) $ TermLC $
 208                          \c -> ncons (e c) (s c)
 209                 nuncons_from =
 210                  -- nuncons :: IsSequence s => NonNull s -> (MT.Element s, Maybe (NonNull s))
 211                         from_ast1 ast $ \ast_n as ->
 212                         term_from ast_n ctx $ \ty_n (TermLC n) ->
 213                         check_type1 tyNonNull ast_n ty_n $ \Refl ty_s ->
 214                         check_constraint (At (Just ast_n) (tyIsSequence :$ ty_s)) $ \Con ->
 215                         check_family ast Fam_MonoElement (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 216                         check_type (At Nothing ty_s_e) (At (Just ast_n) ty_s_e) $ \Refl ->
 217                         k as (tyTuple2 :$ ty_s_e :$ (tyMaybe :$ (tyNonNull :$ ty_s))) $ TermLC $
 218                          \c -> nuncons (n c)
 219                 n2e_from
 220                  (f::forall term o.
 221                          (Sym_NonNull term, MonoFoldable o)
 222                          => term (NonNull o) -> term (MT.Element o)) =
 223                  -- head :: MonoFoldable o => NonNull o -> MT.Element o
 224                  -- last :: MonoFoldable o => NonNull o -> MT.Element o
 225                         from_ast1 ast $ \ast_n as ->
 226                         term_from ast_n ctx $ \ty_n (TermLC n) ->
 227                         check_type1 tyNonNull ast_n ty_n $ \Refl ty_o ->
 228                         check_constraint (At (Just ast_n) (tyMonoFoldable :$ ty_o)) $ \Con ->
 229                         check_family ast Fam_MonoElement (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 230                         k as ty_o_e $ TermLC $
 231                          \c -> f (n c)
 232                 n2s_from
 233                  (f::forall term s.
 234                          (Sym_NonNull term, IsSequence s)
 235                          => term (NonNull s) -> term s) =
 236                  -- tail :: IsSequence s => NonNull s -> s
 237                  -- init :: IsSequence s => NonNull s -> s
 238                         from_ast1 ast $ \ast_n as ->
 239                         term_from ast_n ctx $ \ty_n (TermLC n) ->
 240                         check_type1 tyNonNull ast_n ty_n $ \Refl ty_s ->
 241                         check_constraint (At (Just ast_n) (tyIsSequence :$ ty_s)) $ \Con ->
 242                         k as ty_s $ TermLC $
 243                          \c -> f (n c)
 244                 nfilter_from =
 245                  -- filter :: IsSequence s => (MT.Element s -> Bool) -> NonNull s -> s
 246                         from_ast2 ast $ \ast_e2Bool ast_n as ->
 247                         term_from ast_e2Bool ctx $ \ty_e2Bool (TermLC e2Bool) ->
 248                         term_from ast_n      ctx $ \ty_n      (TermLC s) ->
 249                         check_type2 tyFun ast_e2Bool ty_e2Bool $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
 250                         check_type (At Nothing tyBool) (At (Just ast_e2Bool) ty_e2Bool_Bool) $ \Refl ->
 251                         check_type1 tyNonNull ast_n ty_n $ \Refl ty_s ->
 252                         check_constraint (At (Just ast_n) (tyIsSequence :$ ty_s)) $ \Con ->
 253                         check_family ast Fam_MonoElement (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 254                         check_type (At Nothing ty_s_e) (At (Just ast_e2Bool) ty_e2Bool_e) $ \Refl ->
 255                         k as ty_s $ TermLC $
 256                          \c -> nfilter (e2Bool c) (s c)
 257
 258 -- | The 'NonNull' 'Type'
 259 tyNonNull :: Inj_Const cs NonNull => Type cs NonNull
 260 tyNonNull = TyConst inj_const
 261
 262 sym_NonNull :: Proxy Sym_NonNull
 263 sym_NonNull = Proxy
 264
 265 syNonNull :: IsString a => [Syntax a] -> Syntax a
 266 syNonNull = Syntax "NonNull"