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                         from_ast2 ast $ \ast_b ast_a2b as ->
 120                         term_from ast_b   ctx $ \ty_b   (TermLC b) ->
 121                         term_from ast_a2b ctx $ \ty_a2b (TermLC a2b) ->
 122                         check_type2 tyFun ast_a2b ty_a2b $ \Refl ty_a2b_a ty_a2b_b ->
 123                         check_type (At (Just ast_a2b) ty_a2b_b) (At (Just ast_b) ty_b) $ \Refl ->
 124                         k as (tyMaybe :$ ty_a2b_a ~> ty_b) $ TermLC $
 125                          \c -> lam $ maybe (b c) (a2b c)
 126                 _Just_from =
 127                  -- Just :: a -> Maybe a
 128                         from_ast1 ast $ \ast_a as ->
 129                         term_from ast_a ctx $ \ty_a (TermLC a) ->
 130                         k as (tyMaybe :$ ty_a) $ TermLC $
 131                          \c -> _Just (a c)
 132                 _Nothing_from =
 133                  -- Nothing :: Maybe a
 134                         from_ast1 ast $ \ast_ty_a as ->
 135                         either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 136                         type_from ast_ty_a $ \ty_a -> Right $
 137                         check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
 138                         k as (tyMaybe :$ ty_a) $ TermLC $
 139                         Fun.const _Nothing
 140
 141 -- | The 'Maybe' 'Type'
 142 tyMaybe :: Inj_Const cs Maybe => Type cs Maybe
 143 tyMaybe = TyConst inj_const
 144
 145 sym_Maybe :: Proxy Sym_Maybe
 146 sym_Maybe = Proxy
 147
 148 syMaybe :: IsString a => [Syntax a] -> Syntax a
 149 syMaybe = Syntax "Maybe"
 150
 151 syNothing :: IsString a => [Syntax a] -> Syntax a
 152 syNothing = Syntax "Nothing"
 153
 154 syJust :: IsString a => [Syntax a] -> Syntax a
 155 syJust = Syntax "Just"