Language/Symantic/Compiling/Maybe.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-}
   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 Traversable
  45  ]
  46
  47 instance Sym_Maybe HostI where
  48         _Nothing = HostI Nothing
  49         _Just    = liftM Just
  50         maybe    = liftM3 Maybe.maybe
  51 instance Sym_Maybe TextI where
  52         _Nothing = textI_app0 "Nothing"
  53         _Just    = textI_app1 "Just"
  54         maybe    = textI_app3 "maybe"
  55 instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (DupI r1 r2) where
  56         _Nothing = dupI0 (Proxy @Sym_Maybe) _Nothing
  57         _Just    = dupI1 (Proxy @Sym_Maybe) _Just
  58         maybe    = dupI3 (Proxy @Sym_Maybe) maybe
  59
  60 instance Const_from Text cs => Const_from Text (Proxy Maybe ': cs) where
  61         const_from "Maybe" k = k (ConstZ kind)
  62         const_from s k = const_from s $ k . ConstS
  63 instance Show_Const cs => Show_Const (Proxy Maybe ': cs) where
  64         show_const ConstZ{} = "Maybe"
  65         show_const (ConstS c) = show_const c
  66
  67 instance -- Proj_ConC
  68  ( Proj_Const cs Maybe
  69  , Proj_Consts cs (Consts_imported_by Maybe)
  70  , Proj_Con cs
  71  ) => Proj_ConC cs (Proxy Maybe) where
  72         proj_conC _ (TyConst q :$ TyConst c)
  73          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  74          , Just Refl <- proj_const c (Proxy::Proxy Maybe)
  75          = case () of
  76                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
  77                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
  78                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
  79                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
  80                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
  81                  _ -> Nothing
  82         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
  83          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  84          , Just Refl <- proj_const c (Proxy::Proxy Maybe)
  85          = case () of
  86                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
  87                    , Just Con  <- proj_con (t :$ a) -> Just Con
  88                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)
  89                    , Just Con  <- proj_con (t :$ a) -> Just Con
  90                  _ -> Nothing
  91         proj_conC _c _q = Nothing
  92 data instance TokenT meta (ts::[*]) (Proxy Maybe)
  93  = Token_Term_Maybe_Nothing (EToken meta '[Proxy Token_Type])
  94  | Token_Term_Maybe_Just    (EToken meta ts)
  95  | Token_Term_Maybe_maybe   (EToken meta ts) (EToken meta ts)
  96 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Maybe))
  97 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Maybe))
  98 instance -- Term_fromI
  99  ( Const_from Name_LamVar (Consts_of_Ifaces is)
 100  , Inj_Const  (Consts_of_Ifaces is) Maybe
 101  , Inj_Const  (Consts_of_Ifaces is) (->)
 102  , Term_from is
 103  ) => Term_fromI is (Proxy Maybe) where
 104         term_fromI tok ctx k =
 105                 case tok of
 106                  Token_Term_Maybe_Nothing tok_ty_a ->
 107                         -- Nothing :: Maybe a
 108                         type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
 109                         check_kind
 110                          (At Nothing SKiType)
 111                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
 112                         k (ty @Maybe :$ ty_a) $ TermLC $
 113                                 Fun.const _Nothing
 114                  Token_Term_Maybe_Just tok_a ->
 115                         -- Just :: a -> Maybe a
 116                         term_from tok_a ctx $ \ty_a (TermLC a) ->
 117                         k (ty @Maybe :$ ty_a) $ TermLC $
 118                          \c -> _Just (a c)
 119                  Token_Term_Maybe_maybe tok_b tok_a2b ->
 120                         -- maybe :: b -> (a -> b) -> Maybe a -> b
 121                         term_from tok_b   ctx $ \ty_b   (TermLC b) ->
 122                         term_from tok_a2b ctx $ \ty_a2b (TermLC a2b) ->
 123                         check_type2 (ty @(->)) (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
 124                         check_type
 125                          (At (Just tok_a2b) ty_a2b_b)
 126                          (At (Just tok_b) ty_b) $ \Refl ->
 127                         k (ty @Maybe :$ ty_a2b_a ~> ty_b) $ TermLC $
 128                          \c -> lam $ maybe (b c) (a2b c)