Language/Symantic/Compiling/Maybe.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
   4 -- | Symantic for 'Maybe'.
   5 module Language.Symantic.Compiling.Maybe where
   6
   7 import Control.Monad
   8 import qualified Data.Function as Fun
   9 import qualified Data.Maybe as Maybe
  10 import Data.Proxy
  11 import Data.Text (Text)
  12 import Data.Type.Equality ((:~:)(Refl))
  13 import Prelude hiding (maybe)
  14
  15 import Language.Symantic.Parsing
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling.Term
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  20
  21 -- * Class 'Sym_Maybe_Lam'
  22 class Sym_Maybe term where
  23         _Nothing :: term (Maybe a)
  24         _Just    :: term a -> term (Maybe a)
  25         maybe    :: term b -> term (a -> b) -> term (Maybe a) -> term b
  26
  27         default _Nothing :: Trans t term => t term (Maybe a)
  28         default _Just    :: Trans t term => t term a -> t term (Maybe a)
  29         default maybe    :: Trans t term => t term b -> t term (a -> b) -> t term (Maybe a) -> t term b
  30
  31         _Nothing = trans_lift _Nothing
  32         _Just    = trans_map1 _Just
  33         maybe    = trans_map3 maybe
  34
  35 type instance Sym_of_Iface (Proxy Maybe) = Sym_Maybe
  36 type instance Consts_of_Iface (Proxy Maybe) = Proxy Maybe ': Consts_imported_by Maybe
  37 type instance Consts_imported_by Maybe =
  38  [ Proxy Applicative
  39  , Proxy Eq
  40  , Proxy Foldable
  41  , Proxy Functor
  42  , Proxy Monad
  43  , Proxy Monoid
  44  , Proxy Show
  45  , Proxy Traversable
  46  ]
  47
  48 instance Sym_Maybe HostI where
  49         _Nothing = HostI Nothing
  50         _Just    = liftM Just
  51         maybe    = liftM3 Maybe.maybe
  52 instance Sym_Maybe TextI where
  53         _Nothing = textI_app0 "Nothing"
  54         _Just    = textI_app1 "Just"
  55         maybe    = textI_app3 "maybe"
  56 instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (DupI r1 r2) where
  57         _Nothing = dupI0 (Proxy @Sym_Maybe) _Nothing
  58         _Just    = dupI1 (Proxy @Sym_Maybe) _Just
  59         maybe    = dupI3 (Proxy @Sym_Maybe) maybe
  60
  61 instance Const_from Text cs => Const_from Text (Proxy Maybe ': cs) where
  62         const_from "Maybe" k = k (ConstZ kind)
  63         const_from s k = const_from s $ k . ConstS
  64 instance Show_Const cs => Show_Const (Proxy Maybe ': cs) where
  65         show_const ConstZ{} = "Maybe"
  66         show_const (ConstS c) = show_const c
  67
  68 instance -- Proj_ConC
  69  ( Proj_Const cs Maybe
  70  , Proj_Consts cs (Consts_imported_by Maybe)
  71  , Proj_Con cs
  72  ) => Proj_ConC cs (Proxy Maybe) where
  73         proj_conC _ (TyConst q :$ TyConst c)
  74          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  75          , Just Refl <- proj_const c (Proxy::Proxy Maybe)
  76          = case () of
  77                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
  78                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
  79                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
  80                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
  81                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
  82                  _ -> Nothing
  83         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
  84          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  85          , Just Refl <- proj_const c (Proxy::Proxy Maybe)
  86          = case () of
  87                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
  88                    , Just Con  <- proj_con (t :$ a) -> Just Con
  89                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)
  90                    , Just Con  <- proj_con (t :$ a) -> Just Con
  91                    | Just Refl <- proj_const q (Proxy::Proxy Show)
  92                    , Just Con  <- proj_con (t :$ a) -> Just Con
  93                  _ -> Nothing
  94         proj_conC _c _q = Nothing
  95 data instance TokenT meta (ts::[*]) (Proxy Maybe)
  96  = Token_Term_Maybe_Nothing (EToken meta '[Proxy Token_Type])
  97  | Token_Term_Maybe_Just    (EToken meta ts)
  98  | Token_Term_Maybe_maybe   (EToken meta ts) (EToken meta ts)
  99 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Maybe))
 100 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Maybe))
 101 instance -- Term_fromI
 102  ( Const_from Name_LamVar (Consts_of_Ifaces is)
 103  , Inj_Const  (Consts_of_Ifaces is) Maybe
 104  , Inj_Const  (Consts_of_Ifaces is) (->)
 105  , Term_from is
 106  ) => Term_fromI is (Proxy Maybe) where
 107         term_fromI tok ctx k =
 108                 case tok of
 109                  Token_Term_Maybe_Nothing tok_ty_a ->
 110                         -- Nothing :: Maybe a
 111                         type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
 112                         check_kind
 113                          (At Nothing SKiType)
 114                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 115                         k (ty @Maybe :$ ty_a) $ TermLC $
 116                                 Fun.const _Nothing
 117                  Token_Term_Maybe_Just tok_a ->
 118                         -- Just :: a -> Maybe a
 119                         term_from tok_a ctx $ \ty_a (TermLC a) ->
 120                         k (ty @Maybe :$ ty_a) $ TermLC $
 121                          \c -> _Just (a c)
 122                  Token_Term_Maybe_maybe tok_b tok_a2b ->
 123                         -- maybe :: b -> (a -> b) -> Maybe a -> b
 124                         term_from tok_b   ctx $ \ty_b   (TermLC b) ->
 125                         term_from tok_a2b ctx $ \ty_a2b (TermLC a2b) ->
 126                         check_type2 (ty @(->)) (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
 127                         check_type
 128                          (At (Just tok_a2b) ty_a2b_b)
 129                          (At (Just tok_b) ty_b) $ \Refl ->
 130                         k (ty @Maybe :$ ty_a2b_a ~> ty_b) $ TermLC $
 131                          \c -> lam $ maybe (b c) (a2b c)