Language/Symantic/Compiling/Tuple2.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=11 #-}
  14 -- | Symantic for @(,)@.
  15 module Language.Symantic.Compiling.Tuple2 where
  16
  17 import Control.Monad (liftM, liftM2)
  18 import Data.Monoid ((<>))
  19 import Data.Proxy
  20 import Data.String (IsString)
  21 import Data.Text (Text)
  22 import qualified Data.Tuple as Tuple
  23 import Data.Type.Equality ((:~:)(Refl))
  24 import Prelude hiding (fst, snd)
  25
  26 import Language.Symantic.Typing
  27 import Language.Symantic.Compiling.Term
  28 import Language.Symantic.Compiling.Monoid (tyMonoid)
  29 import Language.Symantic.Interpreting
  30 import Language.Symantic.Transforming.Trans
  31
  32 -- * Class 'Sym_Tuple2'
  33 class Sym_Tuple2 term where
  34         tuple2 :: term a -> term b -> term (a, b)
  35         fst :: term (a, b) -> term a
  36         snd :: term (a, b) -> term b
  37
  38         default tuple2 :: Trans t term => t term a -> t term b -> t term (a, b)
  39         default fst :: Trans t term => t term (a, b) -> t term a
  40         default snd :: Trans t term => t term (a, b) -> t term b
  41
  42         tuple2 = trans_map2 tuple2
  43         fst    = trans_map1 fst
  44         snd    = trans_map1 snd
  45
  46 type instance Sym_of_Iface (Proxy (,)) = Sym_Tuple2
  47 type instance Consts_of_Iface (Proxy (,)) = Proxy (,) ': Consts_imported_by (,)
  48 type instance Consts_imported_by (,) =
  49  [ Proxy Applicative
  50  , Proxy Bounded
  51  , Proxy Eq
  52  , Proxy Foldable
  53  , Proxy Functor
  54  , Proxy Monad
  55  , Proxy Monoid
  56  , Proxy Ord
  57  , Proxy Traversable
  58  ]
  59
  60 instance Sym_Tuple2 HostI where
  61         tuple2 = liftM2 (,)
  62         fst    = liftM  Tuple.fst
  63         snd    = liftM  Tuple.snd
  64 instance Sym_Tuple2 TextI where
  65         tuple2 (TextI a) (TextI b) =
  66                 TextI $ \_p v ->
  67                         let p' = precedence_Toplevel in
  68                         "(" <> a p' v <> ", " <> b p' v <> ")"
  69         fst = textI_app1 "fst"
  70         snd = textI_app1 "snd"
  71 instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (DupI r1 r2) where
  72         tuple2 = dupI2 sym_Tuple2 tuple2
  73         fst    = dupI1 sym_Tuple2 fst
  74         snd    = dupI1 sym_Tuple2 snd
  75
  76 instance Const_from Text cs => Const_from Text (Proxy (,) ': cs) where
  77         const_from "(,)" k = k (ConstZ kind)
  78         const_from s k = const_from s $ k . ConstS
  79 instance Show_Const cs => Show_Const (Proxy (,) ': cs) where
  80         show_const ConstZ{} = "(,)"
  81         show_const (ConstS c) = show_const c
  82
  83 instance -- Proj_ConC
  84  ( Proj_Const cs (,)
  85  , Proj_Consts cs (Consts_imported_by (,))
  86  , Proj_Con cs
  87  , Inj_Const cs Monoid
  88  ) => Proj_ConC cs (Proxy (,)) where
  89         proj_conC _ (TyConst q :$ (TyConst c :$ a))
  90          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
  91          , Just Refl <- proj_const c (Proxy::Proxy (,))
  92          = case () of
  93                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative)
  94                    , Just Con  <- proj_con (tyMonoid :$ a) -> Just Con
  95                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
  96                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
  97                    | Just Refl <- proj_const q (Proxy::Proxy Monad)
  98                    , Just Con  <- proj_con (tyMonoid :$ a) -> Just Con
  99                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
 100                  _ -> Nothing
 101         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a :$ b))
 102          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 103          , Just Refl <- proj_const c (Proxy::Proxy (,))
 104          = case () of
 105                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded)
 106                    , Just Con  <- proj_con (t :$ a)
 107                    , Just Con  <- proj_con (t :$ b) -> Just Con
 108                    | Just Refl <- proj_const q (Proxy::Proxy Eq)
 109                    , Just Con  <- proj_con (t :$ a)
 110                    , Just Con  <- proj_con (t :$ b) -> Just Con
 111                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 112                    , Just Con  <- proj_con (t :$ a)
 113                    , Just Con  <- proj_con (t :$ b) -> Just Con
 114                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
 115                    , Just Con  <- proj_con (t :$ a)
 116                    , Just Con  <- proj_con (t :$ b) -> Just Con
 117                  _ -> Nothing
 118         proj_conC _c _q = Nothing
 119 instance -- Term_fromI
 120  ( AST ast
 121  , Lexem ast ~ LamVarName
 122  , Inj_Const (Consts_of_Ifaces is) (,)
 123  , Term_from is ast
 124  ) => Term_fromI is (Proxy (,)) ast where
 125         term_fromI ast ctx k =
 126                 case ast_lexem ast of
 127                  "(,)" -> tuple2_from
 128                  "fst" -> fst_from
 129                  "snd" -> snd_from
 130                  _ -> Left $ Error_Term_unsupported
 131                 where
 132                 tuple2_from =
 133                  -- (,) :: a -> b -> (a, b)
 134                         from_ast2 ast $ \ast_a ast_b as ->
 135                         term_from ast_a ctx $ \ty_a (TermLC a) ->
 136                         term_from ast_b ctx $ \ty_b (TermLC b) ->
 137                         k as (tyTuple2 :$ ty_a :$ ty_b) $ TermLC $
 138                          \c -> tuple2 (a c) (b c)
 139                 fst_from =
 140                  -- fst :: (a, b) -> a
 141                         from_ast1 ast $ \ast_ab as ->
 142                         term_from ast_ab ctx $ \ty_ab (TermLC ab) ->
 143                         check_type2 tyTuple2 ast_ab ty_ab $ \Refl ty_a _ty_b ->
 144                         k as ty_a $ TermLC $
 145                          \c -> fst (ab c)
 146                 snd_from =
 147                  -- snd :: (a, b) -> b
 148                         from_ast1 ast $ \ast_ab as ->
 149                         term_from ast_ab ctx $ \ty_ab (TermLC ab) ->
 150                         check_type2 tyTuple2 ast_ab ty_ab $ \Refl _ty_a ty_b ->
 151                         k as ty_b $ TermLC $
 152                          \c -> snd (ab c)
 153
 154 -- | The '(,)' 'Type'
 155 tyTuple2 :: Inj_Const cs (,) => Type cs (,)
 156 tyTuple2 = TyConst inj_const
 157
 158 sym_Tuple2 :: Proxy Sym_Tuple2
 159 sym_Tuple2 = Proxy
 160
 161 syTuple2 :: IsString a => [Syntax a] -> Syntax a
 162 syTuple2 = Syntax "(,)"