Language/Symantic/Compiling/Either.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=7 #-}
  14 -- | Symantic for 'Either'.
  15 module Language.Symantic.Compiling.Either where
  16
  17 import Control.Monad (liftM, liftM3)
  18 import qualified Data.Either as Either
  19 import qualified Data.Function as Fun
  20 import Data.Proxy
  21 import Data.String (IsString)
  22 import Data.Text (Text)
  23 import Data.Type.Equality ((:~:)(Refl))
  24 import Prelude hiding (either)
  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_Tuple'
  32 class Sym_Either term where
  33         _Left  :: term l -> term (Either l r)
  34         _Right :: term r -> term (Either l r)
  35         either :: term (l -> a) -> term (r -> a) -> term (Either l r) -> term a
  36         default _Left  :: Trans t term => t term l -> t term (Either l r)
  37         default _Right :: Trans t term => t term r -> t term (Either l r)
  38         default either :: Trans t term => t term (l -> a) -> t term (r -> a) -> t term (Either l r) -> t term a
  39         _Left  = trans_map1 _Left
  40         _Right = trans_map1 _Right
  41         either = trans_map3 either
  42
  43 type instance Sym_of_Iface (Proxy Either) = Sym_Either
  44 type instance Consts_of_Iface (Proxy Either) = Proxy Either ': Consts_imported_by Either
  45 type instance Consts_imported_by Either =
  46  [ Proxy (->)
  47  , Proxy Applicative
  48  , Proxy Eq
  49  , Proxy Foldable
  50  , Proxy Functor
  51  , Proxy Monad
  52  , Proxy Ord
  53  , Proxy Traversable
  54  ]
  55
  56 instance Sym_Either HostI where
  57         _Right = liftM Right
  58         _Left  = liftM Left
  59         either = liftM3 Either.either
  60 instance Sym_Either TextI where
  61         _Right = textI_app1 "Right"
  62         _Left  = textI_app1 "Left"
  63         either = textI_app3 "either"
  64 instance (Sym_Either r1, Sym_Either r2) => Sym_Either (DupI r1 r2) where
  65         _Left  = dupI1 sym_Either _Left
  66         _Right = dupI1 sym_Either _Right
  67         either = dupI3 sym_Either either
  68
  69 instance Const_from Text cs => Const_from Text (Proxy Either ': cs) where
  70         const_from "Either" k = k (ConstZ kind)
  71         const_from s k = const_from s $ k . ConstS
  72 instance Show_Const cs => Show_Const (Proxy Either ': cs) where
  73         show_const ConstZ{} = "Either"
  74         show_const (ConstS c) = show_const c
  75 instance -- Proj_ConC
  76  ( Proj_Const cs Either
  77  , Proj_Consts cs (Consts_imported_by Either)
  78  , Proj_Con cs
  79  ) => Proj_ConC cs (Proxy Either) where
  80         proj_conC _ (TyConst q :$ (TyConst c :$ _l))
  81          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  82          , Just Refl <- proj_const c (Proxy::Proxy Either)
  83          = Just $ case () of
  84                  _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
  85                    | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
  86                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
  87                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
  88                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
  89                  _ -> Nothing
  90         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ l :$ r))
  91          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  92          , Just Refl <- proj_const c (Proxy::Proxy Either)
  93          = Just $ case () of
  94                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
  95                    , Just Con  <- proj_con (t :$ l)
  96                    , Just Con  <- proj_con (t :$ r) -> Just Con
  97                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
  98                    , Just Con  <- proj_con (t :$ l)
  99                    , Just Con  <- proj_con (t :$ r) -> 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) Either
 107  , Inj_Const (Consts_of_Ifaces is) (->)
 108  , Term_from is ast
 109  ) => Term_fromI is (Proxy Either) ast where
 110         term_fromI ast ctx k =
 111                 case ast_lexem ast of
 112                  "Left"   -> left_from
 113                  "Right"  -> right_from
 114                  "either" -> either_from
 115                  _ -> Left $ Error_Term_unsupported
 116                 where
 117                 left_from =
 118                  -- Left :: l -> Either l r
 119                         from_ast2 ast $ \ast_ty_r ast_l ->
 120                         Either.either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 121                         type_from ast_ty_r $ \ty_r -> Right $
 122                         check_kind ast SKiType (At (Just ast_ty_r) ty_r) $ \Refl ->
 123                         term_from ast_l ctx $ \ty_l (TermLC l) ->
 124                         k ((tyEither :$ ty_l) :$ ty_r) $ TermLC $
 125                          \c -> _Left (l c)
 126                 right_from =
 127                  -- Right :: r -> Either l r
 128                         from_ast2 ast $ \ast_ty_l ast_r ->
 129                         Either.either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
 130                         type_from ast_ty_l $ \ty_l -> Right $
 131                         check_kind ast SKiType (At (Just ast_ty_l) ty_l) $ \Refl ->
 132                         term_from ast_r ctx $ \ty_r (TermLC r) ->
 133                         k ((tyEither :$ ty_l) :$ ty_r) $ TermLC $
 134                          \c -> _Right (r c)
 135                 either_from =
 136                  -- either :: (l -> a) -> (r -> a) -> Either l r -> a
 137                         case ast_nodes ast of
 138                          [] -> Left $ Error_Term_Syntax $
 139                                 Error_Syntax_more_arguments_needed $ At (Just ast) 2
 140                          [ast_l2a, ast_r2a] ->
 141                                 term_from ast_l2a ctx $ \ty_l2a (TermLC l2a) ->
 142                                 term_from ast_r2a ctx $ \ty_r2a (TermLC r2a) ->
 143                                 check_type2 tyFun ast_l2a ty_l2a $ \Refl ty_l2a_l ty_l2a_a ->
 144                                 check_type2 tyFun ast_r2a ty_r2a $ \Refl ty_r2a_r ty_r2a_a ->
 145                                 check_type (At (Just ast_l2a) ty_l2a_a) (At (Just ast_r2a) ty_r2a_a) $ \Refl ->
 146                                 k ((tyEither :$ ty_l2a_l) :$ ty_r2a_r ~> ty_l2a_a) $ TermLC $
 147                                  \c -> lam $ either (l2a c) (r2a c)
 148                          [ast_l2a, ast_r2a, ast_e] ->
 149                                 term_from ast_l2a ctx $ \ty_l2a (TermLC l2a) ->
 150                                 term_from ast_r2a ctx $ \ty_r2a (TermLC r2a) ->
 151                                 term_from ast_e   ctx $ \ty_e   (TermLC e) ->
 152                                 check_type2 tyFun ast_l2a ty_l2a $ \Refl ty_l2a_l ty_l2a_a ->
 153                                 check_type2 tyFun ast_r2a ty_r2a $ \Refl ty_r2a_r ty_r2a_a ->
 154                                 check_type (At (Just ast_l2a) ty_l2a_a) (At (Just ast_r2a) ty_r2a_a) $ \Refl ->
 155                                 check_type2 tyEither ast_e ty_e $ \Refl ty_e_l ty_e_r ->
 156                                 check_type (At (Just ast_l2a) ty_l2a_l) (At (Just ast_e) ty_e_l) $ \Refl ->
 157                                 check_type (At (Just ast_r2a) ty_r2a_r) (At (Just ast_e) ty_e_r) $ \Refl ->
 158                                 k ty_l2a_a $ TermLC $
 159                                  \c -> either (l2a c) (r2a c) (e c)
 160                          _ -> Left $ Error_Term_Syntax $
 161                                 Error_Syntax_too_many_arguments $ At (Just ast) 3
 162
 163 -- | The 'Either' 'Type'
 164 tyEither :: Inj_Const cs Either => Type cs Either
 165 tyEither = TyConst inj_const
 166
 167 sym_Either :: Proxy Sym_Either
 168 sym_Either = Proxy
 169
 170 syEither :: IsString a => [Syntax a] -> Syntax a
 171 syEither = Syntax "Either"