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 -- | Symantic for 'NonNull'.
  17 module Language.Symantic.Compiling.NonNull where
  18
  19 import Control.Monad (liftM)
  20 import Data.MonoTraversable (MonoFoldable)
  21 import qualified Data.MonoTraversable as MT
  22 import Data.NonNull (NonNull)
  23 import qualified Data.NonNull as NonNull
  24 import Data.Proxy
  25 import Data.String (IsString)
  26 import Data.Text (Text)
  27 import Data.Type.Equality ((:~:)(Refl))
  28
  29 import Language.Symantic.Typing
  30 import Language.Symantic.Compiling.Term
  31 import Language.Symantic.Compiling.Maybe (tyMaybe)
  32 import Language.Symantic.Compiling.MonoFunctor
  33 import Language.Symantic.Compiling.MonoFoldable
  34 import Language.Symantic.Interpreting
  35 import Language.Symantic.Transforming.Trans
  36
  37 -- * Class 'Sym_NonNull'
  38 class Sym_NonNull term where
  39         fromNullable :: MonoFoldable o => term o -> term (Maybe (NonNull o))
  40         toNullable :: MonoFoldable o => term (NonNull o) -> term o
  41         default fromNullable :: (Trans t term, MonoFoldable o) => t term o -> t term (Maybe (NonNull o))
  42         default toNullable :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term o
  43         fromNullable = trans_map1 fromNullable
  44         toNullable   = trans_map1 toNullable
  45
  46 type instance Sym_of_Iface (Proxy NonNull) = Sym_NonNull
  47 type instance Consts_of_Iface (Proxy NonNull) = Proxy NonNull ': Consts_imported_by NonNull
  48 type instance Consts_imported_by NonNull =
  49  [ Proxy Eq
  50  , Proxy Maybe
  51  , Proxy Ord
  52  , Proxy MT.MonoFoldable
  53  , Proxy MT.MonoFunctor
  54  ]
  55
  56 instance Sym_NonNull HostI where
  57         fromNullable = liftM NonNull.fromNullable
  58         toNullable   = liftM NonNull.toNullable
  59 instance Sym_NonNull TextI where
  60         fromNullable = textI_app1 "fromNullable"
  61         toNullable   = textI_app1 "toNullable"
  62 instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (DupI r1 r2) where
  63         fromNullable = dupI1 sym_NonNull fromNullable
  64         toNullable   = dupI1 sym_NonNull toNullable
  65
  66 instance Const_from Text cs => Const_from Text (Proxy NonNull ': cs) where
  67         const_from "NonNull" k = k (ConstZ kind)
  68         const_from s k = const_from s $ k . ConstS
  69 instance Show_Const cs => Show_Const (Proxy NonNull ': cs) where
  70         show_const ConstZ{} = "NonNull"
  71         show_const (ConstS c) = show_const c
  72
  73 instance -- Fam_MonoElement
  74  ( Proj_Const cs NonNull
  75  , Proj_Fam cs Fam_MonoElement
  76  ) => Proj_FamC cs Fam_MonoElement NonNull where
  77         proj_famC _c _fam ((TyConst c :$ ty_o) `TypesS` TypesZ)
  78          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  79          , Just Refl <- proj_const c (Proxy::Proxy NonNull)
  80          = proj_fam Fam_MonoElement (ty_o `TypesS` TypesZ)
  81         proj_famC _c _fam _ty = Nothing
  82 instance -- Proj_ConC
  83  ( Proj_Const cs NonNull
  84  , Proj_Consts cs (Consts_imported_by NonNull)
  85  , Proj_Con cs
  86  ) => Proj_ConC cs (Proxy NonNull) where
  87         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ o))
  88          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  89          , Just Refl <- proj_const c (Proxy::Proxy NonNull)
  90          = case () of
  91                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
  92                    , Just Con  <- proj_con (t :$ o) -> Just Con
  93                    | Just Refl <- proj_const q (Proxy::Proxy MT.MonoFoldable)
  94                    , Just Con  <- proj_con (t :$ o) -> Just Con
  95                    | Just Refl <- proj_const q (Proxy::Proxy MT.MonoFunctor)
  96                    , Just Con  <- proj_con (t :$ o) -> Just Con
  97                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
  98                    , Just Con  <- proj_con (t :$ o) -> Just Con
  99                  _ -> Nothing
 100         proj_conC _c _q = Nothing
 101 instance -- Term_fromI
 102  ( AST ast
 103  , Lexem ast ~ LamVarName
 104  , Inj_Const (Consts_of_Ifaces is) NonNull
 105  , Inj_Const (Consts_of_Ifaces is) Maybe
 106  , Inj_Const (Consts_of_Ifaces is) MonoFoldable
 107  , Proj_Con  (Consts_of_Ifaces is)
 108  , Term_from is ast
 109  ) => Term_fromI is (Proxy NonNull) ast where
 110         term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy NonNull ': rs)
 111         term_fromI ast ctx k =
 112                 case ast_lexem ast of
 113                  "fromNullable" -> fromNullable_from
 114                  "toNullable"   -> toNullable_from
 115                  _ -> Left $ Error_Term_unsupported
 116                 where
 117                 fromNullable_from =
 118                  -- fromNullable :: MonoFoldable o => o -> Maybe (NonNull o)
 119                         from_ast1 ast $ \ast_o as ->
 120                         term_from ast_o ctx $ \ty_o (TermLC o) ->
 121                         check_constraint (At (Just ast_o) (tyMonoFoldable :$ ty_o)) $ \Con ->
 122                         k as (tyMaybe :$ (tyNonNull :$ ty_o)) $ TermLC $
 123                          \c -> fromNullable (o c)
 124                 toNullable_from =
 125                  -- toNullable :: MonoFoldable o => NonNull o -> o
 126                         from_ast1 ast $ \ast_n as ->
 127                         term_from ast_n ctx $ \ty_n (TermLC n) ->
 128                         check_type1 tyNonNull ast_n ty_n $ \Refl ty_o ->
 129                         check_constraint (At (Just ast_n) (tyMonoFoldable :$ ty_o)) $ \Con ->
 130                         k as ty_o $ TermLC $
 131                          \c -> toNullable (n c)
 132
 133 -- | The 'NonNull' 'Type'
 134 tyNonNull :: Inj_Const cs NonNull => Type cs NonNull
 135 tyNonNull = TyConst inj_const
 136
 137 sym_NonNull :: Proxy Sym_NonNull
 138 sym_NonNull = Proxy
 139
 140 syNonNull :: IsString a => [Syntax a] -> Syntax a
 141 syNonNull = Syntax "NonNull"