]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Either.hs
Fix lambda application.
[haskell/symantic.git] / 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 as ->
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 as ((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 as ->
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 as ((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 from_ast2 ast $ \ast_l2a ast_r2a as ->
138 term_from ast_l2a ctx $ \ty_l2a (TermLC l2a) ->
139 term_from ast_r2a ctx $ \ty_r2a (TermLC r2a) ->
140 check_type2 tyFun ast_l2a ty_l2a $ \Refl ty_l2a_l ty_l2a_a ->
141 check_type2 tyFun ast_r2a ty_r2a $ \Refl ty_r2a_r ty_r2a_a ->
142 check_type (At (Just ast_l2a) ty_l2a_a) (At (Just ast_r2a) ty_r2a_a) $ \Refl ->
143 k as ((tyEither :$ ty_l2a_l) :$ ty_r2a_r ~> ty_l2a_a) $ TermLC $
144 \c -> lam $ either (l2a c) (r2a c)
145
146 -- | The 'Either' 'Type'
147 tyEither :: Inj_Const cs Either => Type cs Either
148 tyEither = TyConst inj_const
149
150 sym_Either :: Proxy Sym_Either
151 sym_Either = Proxy
152
153 syEither :: IsString a => [Syntax a] -> Syntax a
154 syEither = Syntax "Either"