Language/Symantic/Compiling/Maybe.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# LANGUAGE UndecidableInstances #-}
  12 {-# OPTIONS_GHC -fno-warn-orphans #-}
  13 {-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-}
  14 -- | Symantic for 'Maybe'.
  15 module Language.Symantic.Compiling.Maybe where
  16
  17 import Control.Monad
  18 import qualified Data.Function as Fun
  19 import qualified Data.Maybe as Maybe
  20 import Data.Proxy
  21 import Data.String (IsString)
  22 import Data.Text (Text)
  23 import Data.Type.Equality ((:~:)(Refl))
  24 import Prelude hiding (maybe)
  25
  26 import Language.Symantic.Typing
  27 import Language.Symantic.Compiling.Term
  28 import Language.Symantic.Interpreting
  29 import Language.Symantic.Transforming.Trans
  30
  31 -- * Class 'Sym_Maybe_Lam'
  32 class Sym_Maybe term where
  33         _Nothing :: term (Maybe a)
  34         _Just    :: term a -> term (Maybe a)
  35         maybe    :: term b -> term (a -> b) -> term (Maybe a) -> term b
  36
  37         default _Nothing :: Trans t term => t term (Maybe a)
  38         default _Just    :: Trans t term => t term a -> t term (Maybe a)
  39         default maybe    :: Trans t term => t term b -> t term (a -> b) -> t term (Maybe a) -> t term b
  40
  41         _Nothing = trans_lift _Nothing
  42         _Just    = trans_map1 _Just
  43         maybe    = trans_map3 maybe
  44
  45 type instance Sym_of_Iface (Proxy Maybe) = Sym_Maybe
  46 type instance Consts_of_Iface (Proxy Maybe) = Proxy Maybe ': Consts_imported_by Maybe
  47 type instance Consts_imported_by Maybe =
  48  [ Proxy Applicative
  49  , Proxy Eq
  50  , Proxy Foldable
  51  , Proxy Functor
  52  , Proxy Monad
  53  , Proxy Monoid
  54  , Proxy Traversable
  55  ]
  56
  57 instance Sym_Maybe HostI where
  58         _Nothing = HostI Nothing
  59         _Just    = liftM Just
  60         maybe    = liftM3 Maybe.maybe
  61 instance Sym_Maybe TextI where
  62         _Nothing = textI_app0 "Nothing"
  63         _Just    = textI_app1 "Just"
  64         maybe    = textI_app3 "maybe"
  65 instance (Sym_Maybe r1, Sym_Maybe r2) => Sym_Maybe (DupI r1 r2) where
  66         _Nothing = dupI0 sym_Maybe _Nothing
  67         _Just    = dupI1 sym_Maybe _Just
  68         maybe    = dupI3 sym_Maybe maybe
  69
  70 instance Const_from Text cs => Const_from Text (Proxy Maybe ': cs) where
  71         const_from "Maybe" k = k (ConstZ kind)
  72         const_from s k = const_from s $ k . ConstS
  73 instance Show_Const cs => Show_Const (Proxy Maybe ': cs) where
  74         show_const ConstZ{} = "Maybe"
  75         show_const (ConstS c) = show_const c
  76
  77 instance -- Proj_ConC
  78  ( Proj_Const cs Maybe
  79  , Proj_Consts cs (Consts_imported_by Maybe)
  80  , Proj_Con cs
  81  ) => Proj_ConC cs (Proxy Maybe) where
  82         proj_conC _ (TyConst q :$ TyConst c)
  83          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  84          , Just Refl <- proj_const c (Proxy::Proxy Maybe)
  85          = Just $ case () of
  86                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
  87                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
  88                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
  89                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
  90                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
  91                  _ -> Nothing
  92         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
  93          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  94          , Just Refl <- proj_const c (Proxy::Proxy Maybe)
  95          = Just $ case () of
  96                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
  97                    , Just Con  <- proj_con (t :$ a) -> Just Con
  98                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)
  99                    , Just Con  <- proj_con (t :$ a) -> Just Con
 100                  _ -> Nothing
 101         proj_conC _c _q = Nothing
 102 instance -- Term_fromI
 103  ( AST ast
 104  , Lexem ast ~ LamVarName
 105  , Const_from (Lexem ast) (Consts_of_Ifaces is)
 106  , Inj_Const  (Consts_of_Ifaces is) Maybe
 107  , Inj_Const  (Consts_of_Ifaces is) (->)
 108  , Term_from is ast
 109  ) => Term_fromI is (Proxy Maybe) ast where
 110         term_fromI ast ctx k =
 111                 case ast_lexem ast of
 112                  "maybe"   -> maybe_from
 113                  "Just"    -> _Just_from
 114                  "Nothing" -> _Nothing_from
 115                  _ -> Left $ Error_Term_unsupported
 116                 where
 117                 maybe_from =
 118                  -- maybe :: b -> (a -> b) -> Maybe a -> b
 119                         case ast_nodes ast of
 120                          [] -> Left $ Error_Term_Syntax $
 121                                 Error_Syntax_more_arguments_needed $ At (Just ast) 3
 122                          [ast_b, ast_a2b] ->
 123                                 term_from ast_b   ctx $ \ty_b   (TermLC b) ->
 124                                 term_from ast_a2b ctx $ \ty_a2b (TermLC a2b) ->
 125                                 check_type2 tyFun ast_a2b ty_a2b $ \Refl ty_a2b_a ty_a2b_b ->
 126                                 check_type (At (Just ast_a2b) ty_a2b_b) (At (Just ast_b) ty_b) $ \Refl ->
 127                                 k (tyMaybe :$ ty_a2b_a ~> ty_b) $ TermLC $
 128                                  \c -> lam $ maybe (b c) (a2b c)
 129                          [ast_b, ast_a2b, ast_ma] ->
 130                                 term_from ast_b   ctx $ \ty_b   (TermLC b) ->
 131                                 term_from ast_a2b ctx $ \ty_a2b (TermLC a2b) ->
 132                                 term_from ast_ma  ctx $ \ty_ma  (TermLC ma) ->
 133                                 check_type2 tyFun ast_a2b ty_a2b $ \Refl ty_a2b_a ty_a2b_b ->
 134                                 check_type1 tyMaybe ast_ma ty_ma $ \Refl ty_ma_a ->
 135                                 check_type (At (Just ast_a2b) ty_a2b_a) (At (Just ast_ma) ty_ma_a) $ \Refl ->
 136                                 check_type (At (Just ast_a2b) ty_a2b_b) (At (Just ast_b)  ty_b)   $ \Refl ->
 137                                 k ty_b $ TermLC $
 138                                  \c -> maybe (b c) (a2b c) (ma c)
 139                          _ -> Left $ Error_Term_Syntax $
 140                                 Error_Syntax_too_many_arguments $ At (Just ast) 3
 141                 _Just_from =
 142                  -- Just :: a -> Maybe a
 143                         from_ast1 ast $ \ast_a ->
 144                         term_from ast_a ctx $ \ty_a (TermLC a) ->
 145                         k (tyMaybe :$ ty_a) $ TermLC $
 146                          \c -> _Just (a c)
 147                 _Nothing_from =
 148                  -- Nothing :: Maybe a
 149                         from_ast1 ast $ \ast_ty_a ->
 150                         either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 151                         type_from ast_ty_a $ \ty_a -> Right $
 152                         check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
 153                         k (tyMaybe :$ ty_a) $ TermLC $
 154                         Fun.const _Nothing
 155
 156 -- | The 'Maybe' 'Type'
 157 tyMaybe :: Inj_Const cs Maybe => Type cs Maybe
 158 tyMaybe = TyConst inj_const
 159
 160 sym_Maybe :: Proxy Sym_Maybe
 161 sym_Maybe = Proxy
 162
 163 syMaybe :: IsString a => [Syntax a] -> Syntax a
 164 syMaybe = Syntax "Maybe"
 165
 166 syNothing :: IsString a => [Syntax a] -> Syntax a
 167 syNothing = Syntax "Nothing"
 168
 169 syJust :: IsString a => [Syntax a] -> Syntax a
 170 syJust = Syntax "Just"