{-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {-# OPTIONS_GHC -fconstraint-solver-iterations=11 #-} -- | Symantic for @(,)@. module Language.Symantic.Compiling.Tuple2 where import Control.Monad (liftM, liftM2) import Data.Monoid ((<>)) import Data.Proxy import Data.String (IsString) import Data.Text (Text) import qualified Data.Tuple as Tuple import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding (fst, snd) import Language.Symantic.Typing import Language.Symantic.Compiling.Term import Language.Symantic.Compiling.Monoid (tyMonoid) import Language.Symantic.Interpreting import Language.Symantic.Transforming.Trans -- * Class 'Sym_Tuple2' class Sym_Tuple2 term where tuple2 :: term a -> term b -> term (a, b) fst :: term (a, b) -> term a snd :: term (a, b) -> term b default tuple2 :: Trans t term => t term a -> t term b -> t term (a, b) default fst :: Trans t term => t term (a, b) -> t term a default snd :: Trans t term => t term (a, b) -> t term b tuple2 = trans_map2 tuple2 fst = trans_map1 fst snd = trans_map1 snd type instance Sym_of_Iface (Proxy (,)) = Sym_Tuple2 type instance Consts_of_Iface (Proxy (,)) = Proxy (,) ': Consts_imported_by (,) type instance Consts_imported_by (,) = [ Proxy Applicative , Proxy Bounded , Proxy Eq , Proxy Foldable , Proxy Functor , Proxy Monad , Proxy Monoid , Proxy Ord , Proxy Traversable ] instance Sym_Tuple2 HostI where tuple2 = liftM2 (,) fst = liftM Tuple.fst snd = liftM Tuple.snd instance Sym_Tuple2 TextI where tuple2 (TextI a) (TextI b) = TextI $ \_p v -> let p' = precedence_Toplevel in "(" <> a p' v <> ", " <> b p' v <> ")" fst = textI_app1 "fst" snd = textI_app1 "snd" instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (DupI r1 r2) where tuple2 = dupI2 sym_Tuple2 tuple2 fst = dupI1 sym_Tuple2 fst snd = dupI1 sym_Tuple2 snd instance Const_from Text cs => Const_from Text (Proxy (,) ': cs) where const_from "(,)" k = k (ConstZ kind) const_from s k = const_from s $ k . ConstS instance Show_Const cs => Show_Const (Proxy (,) ': cs) where show_const ConstZ{} = "(,)" show_const (ConstS c) = show_const c instance -- Proj_ConC ( Proj_Const cs (,) , Proj_Consts cs (Consts_imported_by (,)) , Proj_Con cs , Inj_Const cs Monoid ) => Proj_ConC cs (Proxy (,)) where proj_conC _ (TyConst q :$ (TyConst c :$ a)) | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType) , Just Refl <- proj_const c (Proxy::Proxy (,)) = Just $ case () of _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) , Just Con <- proj_con (tyMonoid :$ a) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Functor) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Foldable) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Monad) , Just Con <- proj_con (tyMonoid :$ a) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con _ -> Nothing proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a :$ b)) | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType) , Just Refl <- proj_const c (Proxy::Proxy (,)) = Just $ case () of _ | Just Refl <- proj_const q (Proxy::Proxy Bounded) , Just Con <- proj_con (t :$ a) , Just Con <- proj_con (t :$ b) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Eq) , Just Con <- proj_con (t :$ a) , Just Con <- proj_con (t :$ b) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Monoid) , Just Con <- proj_con (t :$ a) , Just Con <- proj_con (t :$ b) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Ord) , Just Con <- proj_con (t :$ a) , Just Con <- proj_con (t :$ b) -> Just Con _ -> Nothing proj_conC _c _q = Nothing instance -- Term_fromI ( AST ast , Lexem ast ~ LamVarName , Inj_Const (Consts_of_Ifaces is) (,) , Term_from is ast ) => Term_fromI is (Proxy (,)) ast where term_fromI ast ctx k = case ast_lexem ast of "(,)" -> tuple2_from "fst" -> fst_from "snd" -> snd_from _ -> Left $ Error_Term_unsupported where tuple2_from = -- (,) :: a -> b -> (a, b) from_ast2 ast $ \ast_a ast_b -> term_from ast_a ctx $ \ty_a (TermLC a) -> term_from ast_b ctx $ \ty_b (TermLC b) -> k (tyTuple2 :$ ty_a :$ ty_b) $ TermLC $ \c -> tuple2 (a c) (b c) fst_from = -- fst :: (a, b) -> a from_ast1 ast $ \ast_ab -> term_from ast_ab ctx $ \ty_ab (TermLC ab) -> check_type2 tyTuple2 ast_ab ty_ab $ \Refl ty_a _ty_b -> k ty_a $ TermLC $ \c -> fst (ab c) snd_from = -- snd :: (a, b) -> b from_ast1 ast $ \ast_ab -> term_from ast_ab ctx $ \ty_ab (TermLC ab) -> check_type2 tyTuple2 ast_ab ty_ab $ \Refl _ty_a ty_b -> k ty_b $ TermLC $ \c -> snd (ab c) -- | The '(,)' 'Type' tyTuple2 :: Inj_Const cs (,) => Type cs (,) tyTuple2 = TyConst inj_const sym_Tuple2 :: Proxy Sym_Tuple2 sym_Tuple2 = Proxy syTuple2 :: IsString a => [Syntax a] -> Syntax a syTuple2 = Syntax "(,)"