Language/Symantic/Compiling/Tuple2.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=11 #-}
   4 -- | Symantic for @(,)@.
   5 module Language.Symantic.Compiling.Tuple2 where
   6
   7 import Control.Monad (liftM, liftM2)
   8 import Data.Monoid ((<>))
   9 import Data.Proxy
  10 import Data.Text (Text)
  11 import qualified Data.Tuple as Tuple
  12 import Data.Type.Equality ((:~:)(Refl))
  13 import Prelude hiding (fst, snd)
  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_Tuple2'
  22 class Sym_Tuple2 term where
  23         tuple2 :: term a -> term b -> term (a, b)
  24         fst :: term (a, b) -> term a
  25         snd :: term (a, b) -> term b
  26
  27         default tuple2 :: Trans t term => t term a -> t term b -> t term (a, b)
  28         default fst :: Trans t term => t term (a, b) -> t term a
  29         default snd :: Trans t term => t term (a, b) -> t term b
  30
  31         tuple2 = trans_map2 tuple2
  32         fst    = trans_map1 fst
  33         snd    = trans_map1 snd
  34
  35 type instance Sym_of_Iface (Proxy (,)) = Sym_Tuple2
  36 type instance Consts_of_Iface (Proxy (,)) = Proxy (,) ': Consts_imported_by (,)
  37 type instance Consts_imported_by (,) =
  38  [ Proxy Applicative
  39  , Proxy Bounded
  40  , Proxy Eq
  41  , Proxy Foldable
  42  , Proxy Functor
  43  , Proxy Monad
  44  , Proxy Monoid
  45  , Proxy Ord
  46  , Proxy Traversable
  47  ]
  48
  49 instance Sym_Tuple2 HostI where
  50         tuple2 = liftM2 (,)
  51         fst    = liftM  Tuple.fst
  52         snd    = liftM  Tuple.snd
  53 instance Sym_Tuple2 TextI where
  54         tuple2 (TextI a) (TextI b) =
  55                 TextI $ \_p v ->
  56                         let p' = precedence_Toplevel in
  57                         "(" <> a p' v <> ", " <> b p' v <> ")"
  58         fst = textI_app1 "fst"
  59         snd = textI_app1 "snd"
  60 instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (DupI r1 r2) where
  61         tuple2 = dupI2 (Proxy @Sym_Tuple2) tuple2
  62         fst    = dupI1 (Proxy @Sym_Tuple2) fst
  63         snd    = dupI1 (Proxy @Sym_Tuple2) snd
  64
  65 instance Const_from Text cs => Const_from Text (Proxy (,) ': cs) where
  66         const_from "(,)" k = k (ConstZ kind)
  67         const_from s k = const_from s $ k . ConstS
  68 instance Show_Const cs => Show_Const (Proxy (,) ': cs) where
  69         show_const ConstZ{} = "(,)"
  70         show_const (ConstS c) = show_const c
  71
  72 instance -- Proj_ConC
  73  ( Proj_Const cs (,)
  74  , Proj_Consts cs (Consts_imported_by (,))
  75  , Proj_Con cs
  76  , Inj_Const cs Monoid
  77  ) => Proj_ConC cs (Proxy (,)) where
  78         proj_conC _ (TyConst q :$ (TyConst c :$ a))
  79          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  80          , Just Refl <- proj_const c (Proxy::Proxy (,))
  81          = case () of
  82                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative)
  83                    , Just Con  <- proj_con (ty @Monoid :$ a) -> Just Con
  84                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
  85                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
  86                    | Just Refl <- proj_const q (Proxy::Proxy Monad)
  87                    , Just Con  <- proj_con (ty @Monoid :$ a) -> Just Con
  88                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
  89                  _ -> Nothing
  90         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a :$ b))
  91          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  92          , Just Refl <- proj_const c (Proxy::Proxy (,))
  93          = case () of
  94                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded)
  95                    , Just Con  <- proj_con (t :$ a)
  96                    , Just Con  <- proj_con (t :$ b) -> Just Con
  97                    | Just Refl <- proj_const q (Proxy::Proxy Eq)
  98                    , Just Con  <- proj_con (t :$ a)
  99                    , Just Con  <- proj_con (t :$ b) -> Just Con
 100                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 101                    , Just Con  <- proj_con (t :$ a)
 102                    , Just Con  <- proj_con (t :$ b) -> Just Con
 103                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
 104                    , Just Con  <- proj_con (t :$ a)
 105                    , Just Con  <- proj_con (t :$ b) -> Just Con
 106                  _ -> Nothing
 107         proj_conC _c _q = Nothing
 108 data instance TokenT meta (ts::[*]) (Proxy (,))
 109  = Token_Term_Tuple2     (EToken meta ts) (EToken meta ts)
 110  | Token_Term_Tuple2_fst (EToken meta ts)
 111  | Token_Term_Tuple2_snd (EToken meta ts)
 112 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy (,)))
 113 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy (,)))
 114 instance -- Term_fromI
 115  ( Inj_Const (Consts_of_Ifaces is) (,)
 116  , Term_from is
 117  ) => Term_fromI is (Proxy (,)) where
 118         term_fromI tok ctx k =
 119                 case tok of
 120                  Token_Term_Tuple2 tok_a tok_b ->
 121                         -- (,) :: a -> b -> (a, b)
 122                         term_from tok_a ctx $ \ty_a (TermLC a) ->
 123                         term_from tok_b ctx $ \ty_b (TermLC b) ->
 124                         k (ty @(,) :$ ty_a :$ ty_b) $ TermLC $
 125                          \c -> tuple2 (a c) (b c)
 126                  Token_Term_Tuple2_fst tok_ab ->
 127                         -- fst :: (a, b) -> a
 128                         term_from tok_ab ctx $ \ty_ab (TermLC ab) ->
 129                         check_type2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl ty_a _ty_b ->
 130                         k ty_a $ TermLC $
 131                          \c -> fst (ab c)
 132                  Token_Term_Tuple2_snd tok_ab ->
 133                         -- snd :: (a, b) -> b
 134                         term_from tok_ab ctx $ \ty_ab (TermLC ab) ->
 135                         check_type2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl _ty_a ty_b ->
 136                         k ty_b $ TermLC $
 137                          \c -> snd (ab c)