symantic-lib/Language/Symantic/Lib/NonNull.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'NonNull'.
   4 module Language.Symantic.Lib.NonNull where
   5
   6 import Data.MonoTraversable (MonoFoldable)
   7 import Data.NonNull (NonNull)
   8 import Data.Sequences (IsSequence, SemiSequence)
   9 import Prelude hiding (head, init, last, tail)
  10 import qualified Data.MonoTraversable as MT
  11 import qualified Data.NonNull as NonNull
  12
  13 import Language.Symantic
  14 import Language.Symantic.Lib.Bool (tyBool)
  15 import Language.Symantic.Lib.Maybe (tyMaybe)
  16 import Language.Symantic.Lib.MonoFoldable (tyMonoFoldable)
  17 import Language.Symantic.Lib.MonoFunctor (Element, famElement, o0, e1)
  18 import Language.Symantic.Lib.Sequences (tySemiSequence, tyIsSequence, s0)
  19 import Language.Symantic.Lib.Tuple2 (tyTuple2)
  20
  21 -- * Class 'Sym_NonNull'
  22 type instance Sym NonNull = Sym_NonNull
  23 class Sym_NonNull term where
  24         fromNullable :: MonoFoldable o => term o -> term (Maybe (NonNull o))
  25         toNullable   :: MonoFoldable o => term (NonNull o) -> term o
  26         ncons        :: SemiSequence s => term (MT.Element s) -> term s -> term (NonNull s)
  27         nuncons      :: IsSequence s   => term (NonNull s) -> term (MT.Element s, Maybe (NonNull s))
  28         head         :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
  29         last         :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
  30         tail         :: IsSequence s   => term (NonNull s) -> term s
  31         init         :: IsSequence s   => term (NonNull s) -> term s
  32         nfilter      :: IsSequence s   => term (MT.Element s -> Bool) -> term (NonNull s) -> term s
  33         default fromNullable :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term o -> term (Maybe (NonNull o))
  34         default toNullable   :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term (NonNull o) -> term o
  35         default ncons        :: Sym_NonNull (UnT term) => Trans term => SemiSequence s => term (MT.Element s) -> term s -> term (NonNull s)
  36         default nuncons      :: Sym_NonNull (UnT term) => Trans term => IsSequence s   => term (NonNull s) -> term (MT.Element s, Maybe (NonNull s))
  37         default head         :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term (NonNull o) -> term (MT.Element o)
  38         default last         :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term (NonNull o) -> term (MT.Element o)
  39         default tail         :: Sym_NonNull (UnT term) => Trans term => IsSequence s   => term (NonNull s) -> term s
  40         default init         :: Sym_NonNull (UnT term) => Trans term => IsSequence s   => term (NonNull s) -> term s
  41         default nfilter      :: Sym_NonNull (UnT term) => Trans term => IsSequence s   => term (MT.Element s -> Bool) -> term (NonNull s) -> term s
  42         fromNullable = trans1 fromNullable
  43         toNullable   = trans1 toNullable
  44         ncons        = trans2 ncons
  45         nuncons      = trans1 nuncons
  46         head         = trans1 head
  47         last         = trans1 last
  48         tail         = trans1 tail
  49         init         = trans1 init
  50         nfilter      = trans2 nfilter
  51
  52 -- Interpreting
  53 instance Sym_NonNull Eval where
  54         fromNullable = eval1 NonNull.fromNullable
  55         toNullable   = eval1 NonNull.toNullable
  56         ncons        = eval2 NonNull.ncons
  57         nuncons      = eval1 NonNull.nuncons
  58         head         = eval1 NonNull.head
  59         last         = eval1 NonNull.last
  60         tail         = eval1 NonNull.tail
  61         init         = eval1 NonNull.init
  62         nfilter      = eval2 NonNull.nfilter
  63 instance Sym_NonNull View where
  64         fromNullable = view1 "fromNullable"
  65         toNullable   = view1 "toNullable"
  66         ncons        = view2 "ncons"
  67         nuncons      = view1 "nuncons"
  68         head         = view1 "head"
  69         last         = view1 "last"
  70         tail         = view1 "tail"
  71         init         = view1 "init"
  72         nfilter      = view2 "nfilter"
  73 instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (Dup r1 r2) where
  74         fromNullable = dup1 @Sym_NonNull fromNullable
  75         toNullable   = dup1 @Sym_NonNull toNullable
  76         ncons        = dup2 @Sym_NonNull ncons
  77         nuncons      = dup1 @Sym_NonNull nuncons
  78         head         = dup1 @Sym_NonNull head
  79         last         = dup1 @Sym_NonNull last
  80         tail         = dup1 @Sym_NonNull tail
  81         init         = dup1 @Sym_NonNull init
  82         nfilter      = dup2 @Sym_NonNull nfilter
  83
  84 -- Transforming
  85 instance (Sym_NonNull term, Sym_Lambda term) => Sym_NonNull (BetaT term)
  86
  87 -- Typing
  88 instance NameTyOf NonNull where
  89         nameTyOf _c = ["NonNull"] `Mod` "NonNull"
  90 instance FixityOf NonNull
  91 instance TypeInstancesFor NonNull where
  92         expandFamFor c len f (TyApp _ z o `TypesS` TypesZ)
  93          | Just HRefl <- proj_ConstKi @_ @Element f
  94          , Just HRefl <- proj_ConstKiTy @_ @NonNull z
  95          = expandFamFor c len f (o `TypesS` TypesZ)
  96         expandFamFor _c _len _fam _as = Nothing
  97 instance ClassInstancesFor NonNull where
  98         proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c o))
  99          | Just HRefl <- proj_ConstKiTy @_ @NonNull c
 100          = case () of
 101                  _ | Just Refl <- proj_Const @Eq q
 102                    , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
 103                    | Just Refl <- proj_Const @MT.MonoFoldable q
 104                    , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
 105                    | Just Refl <- proj_Const @MT.MonoFunctor q
 106                    , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
 107                    | Just Refl <- proj_Const @Ord q
 108                    , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
 109                    | Just Refl <- proj_Const @SemiSequence q
 110                    , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
 111                    | Just Refl <- proj_Const @Show q
 112                    , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
 113                  _ -> Nothing
 114         proveConstraintFor _c _q = Nothing
 115
 116 -- Compiling
 117 instance Gram_Term_AtomsFor src ss g NonNull
 118 instance (Source src, SymInj ss NonNull) => ModuleFor src ss NonNull where
 119         moduleFor = ["NonNull"] `moduleWhere`
 120          [ "fromNullable" := teNonNull_fromNullable
 121          , "toNullable"   := teNonNull_toNullable
 122          , "ncons"        := teNonNull_ncons
 123          , "nuncons"      := teNonNull_nuncons
 124          , "head"         := teNonNull_head
 125          , "last"         := teNonNull_last
 126          , "tail"         := teNonNull_tail
 127          , "init"         := teNonNull_init
 128          , "nfilter"      := teNonNull_nfilter
 129          ]
 130
 131 -- ** 'Type's
 132 tyNonNull :: Source src => Type src vs a -> Type src vs (NonNull a)
 133 tyNonNull a = tyConstLen @(K NonNull) @NonNull (lenVars a) `tyApp` a
 134
 135 -- ** 'Term's
 136 teNonNull_fromNullable :: TermDef NonNull '[Proxy o] (MonoFoldable o #> (o -> Maybe (NonNull o)))
 137 teNonNull_fromNullable = Term (tyMonoFoldable o0) (o0 ~> tyMaybe (tyNonNull o0)) $ teSym @NonNull $ lam1 fromNullable
 138
 139 teNonNull_toNullable :: TermDef NonNull '[Proxy o] (MonoFoldable o #> (NonNull o -> o))
 140 teNonNull_toNullable = Term (tyMonoFoldable o0) (tyNonNull o0 ~> o0) $ teSym @NonNull $ lam1 toNullable
 141
 142 teNonNull_ncons :: TermDef NonNull '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (e -> s -> NonNull s))
 143 teNonNull_ncons = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> tyNonNull s0) $ teSym @NonNull $ lam2 ncons
 144
 145 teNonNull_nuncons :: TermDef NonNull '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> (NonNull s -> (e, Maybe (NonNull s))))
 146 teNonNull_nuncons = Term (tyIsSequence s0 # e1 #~ famElement s0) (tyNonNull s0 ~> e1 `tyTuple2` tyMaybe (tyNonNull s0)) $ teSym @NonNull $ lam1 nuncons
 147
 148 teNonNull_nfilter :: TermDef NonNull '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> ((e -> Bool) -> NonNull s -> s))
 149 teNonNull_nfilter = Term (tyIsSequence s0 # e1 #~ famElement s0) ((e1 ~> tyBool) ~> tyNonNull s0 ~> s0) $ teSym @NonNull $ lam2 nfilter
 150
 151 teNonNull_head, teNonNull_last :: TermDef NonNull '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (NonNull o -> e))
 152 teNonNull_head = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (tyNonNull o0 ~> e1) $ teSym @NonNull $ lam1 head
 153 teNonNull_last = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (tyNonNull o0 ~> e1) $ teSym @NonNull $ lam1 head
 154
 155 teNonNull_tail, teNonNull_init :: TermDef NonNull '[Proxy s] (IsSequence s #> (NonNull s -> s))
 156 teNonNull_tail = Term (tyIsSequence s0) (tyNonNull s0 ~> s0) $ teSym @NonNull $ lam1 tail
 157 teNonNull_init = Term (tyIsSequence s0) (tyNonNull s0 ~> s0) $ teSym @NonNull $ lam1 init