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 FixityOf NonNull
  89 instance TypeInstancesFor NonNull where
  90         expandFamFor c len f (TyApp _ z o `TypesS` TypesZ)
  91          | Just HRefl <- proj_ConstKi @_ @Element f
  92          , Just HRefl <- proj_ConstKiTy @_ @NonNull z
  93          = expandFamFor c len f (o `TypesS` TypesZ)
  94         expandFamFor _c _len _fam _as = Nothing
  95 instance ClassInstancesFor NonNull where
  96         proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c o))
  97          | Just HRefl <- proj_ConstKiTy @_ @NonNull c
  98          = case () of
  99                  _ | Just Refl <- proj_Const @Eq q
 100                    , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
 101                    | Just Refl <- proj_Const @MT.MonoFoldable q
 102                    , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
 103                    | Just Refl <- proj_Const @MT.MonoFunctor q
 104                    , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
 105                    | Just Refl <- proj_Const @Ord q
 106                    , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
 107                    | Just Refl <- proj_Const @SemiSequence q
 108                    , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
 109                    | Just Refl <- proj_Const @Show q
 110                    , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
 111                  _ -> Nothing
 112         proveConstraintFor _c _q = Nothing
 113
 114 -- Compiling
 115 instance Gram_Term_AtomsFor src ss g NonNull
 116 instance (Source src, SymInj ss NonNull) => ModuleFor src ss NonNull where
 117         moduleFor = ["NonNull"] `moduleWhere`
 118          [ "fromNullable" := teNonNull_fromNullable
 119          , "toNullable"   := teNonNull_toNullable
 120          , "ncons"        := teNonNull_ncons
 121          , "nuncons"      := teNonNull_nuncons
 122          , "head"         := teNonNull_head
 123          , "last"         := teNonNull_last
 124          , "tail"         := teNonNull_tail
 125          , "init"         := teNonNull_init
 126          , "nfilter"      := teNonNull_nfilter
 127          ]
 128
 129 -- ** 'Type's
 130 tyNonNull :: Source src => Type src vs a -> Type src vs (NonNull a)
 131 tyNonNull a = tyConstLen @(K NonNull) @NonNull (lenVars a) `tyApp` a
 132
 133 -- ** 'Term's
 134 teNonNull_fromNullable :: TermDef NonNull '[Proxy o] (MonoFoldable o #> (o -> Maybe (NonNull o)))
 135 teNonNull_fromNullable = Term (tyMonoFoldable o0) (o0 ~> tyMaybe (tyNonNull o0)) $ teSym @NonNull $ lam1 fromNullable
 136
 137 teNonNull_toNullable :: TermDef NonNull '[Proxy o] (MonoFoldable o #> (NonNull o -> o))
 138 teNonNull_toNullable = Term (tyMonoFoldable o0) (tyNonNull o0 ~> o0) $ teSym @NonNull $ lam1 toNullable
 139
 140 teNonNull_ncons :: TermDef NonNull '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (e -> s -> NonNull s))
 141 teNonNull_ncons = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> tyNonNull s0) $ teSym @NonNull $ lam2 ncons
 142
 143 teNonNull_nuncons :: TermDef NonNull '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> (NonNull s -> (e, Maybe (NonNull s))))
 144 teNonNull_nuncons = Term (tyIsSequence s0 # e1 #~ famElement s0) (tyNonNull s0 ~> e1 `tyTuple2` tyMaybe (tyNonNull s0)) $ teSym @NonNull $ lam1 nuncons
 145
 146 teNonNull_nfilter :: TermDef NonNull '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> ((e -> Bool) -> NonNull s -> s))
 147 teNonNull_nfilter = Term (tyIsSequence s0 # e1 #~ famElement s0) ((e1 ~> tyBool) ~> tyNonNull s0 ~> s0) $ teSym @NonNull $ lam2 nfilter
 148
 149 teNonNull_head, teNonNull_last :: TermDef NonNull '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (NonNull o -> e))
 150 teNonNull_head = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (tyNonNull o0 ~> e1) $ teSym @NonNull $ lam1 head
 151 teNonNull_last = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (tyNonNull o0 ~> e1) $ teSym @NonNull $ lam1 head
 152
 153 teNonNull_tail, teNonNull_init :: TermDef NonNull '[Proxy s] (IsSequence s #> (NonNull s -> s))
 154 teNonNull_tail = Term (tyIsSequence s0) (tyNonNull s0 ~> s0) $ teSym @NonNull $ lam1 tail
 155 teNonNull_init = Term (tyIsSequence s0) (tyNonNull s0 ~> s0) $ teSym @NonNull $ lam1 init