]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Bool.hs
Clarify names, and add commentaries (bis).
[haskell/symantic.git] / Language / Symantic / Compiling / Bool.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Bool'.
4 module Language.Symantic.Compiling.Bool where
5
6 import Control.Monad
7 import qualified Data.Bool as Bool
8 import Data.Monoid
9 import Data.Proxy
10 import Data.Text (Text)
11 import qualified Data.Text as Text
12 import Data.Type.Equality ((:~:)(Refl))
13 import Prelude hiding ((&&), not, (||))
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_Bool'
22 class Sym_Bool term where
23 bool :: Bool -> term Bool
24 not :: term Bool -> term Bool
25 (&&) :: term Bool -> term Bool -> term Bool
26 (||) :: term Bool -> term Bool -> term Bool
27 xor :: term Bool -> term Bool -> term Bool
28 xor x y = (x || y) && not (x && y)
29
30 default bool :: Trans t term => Bool -> t term Bool
31 default not :: Trans t term => t term Bool -> t term Bool
32 default (&&) :: Trans t term => t term Bool -> t term Bool -> t term Bool
33 default (||) :: Trans t term => t term Bool -> t term Bool -> t term Bool
34
35 bool = trans_lift . bool
36 not = trans_map1 not
37 (&&) = trans_map2 (&&)
38 (||) = trans_map2 (||)
39
40 infixr 2 ||
41 infixr 2 `xor`
42 infixr 3 &&
43
44 type instance Sym_of_Iface (Proxy Bool) = Sym_Bool
45 type instance Consts_of_Iface (Proxy Bool) = Proxy Bool ': Consts_imported_by Bool
46 type instance Consts_imported_by Bool =
47 [ Proxy Bounded
48 , Proxy Enum
49 , Proxy Eq
50 , Proxy Ord
51 , Proxy Show
52 ]
53
54 instance Sym_Bool HostI where
55 bool = HostI
56 not = liftM Bool.not
57 (&&) = liftM2 (Bool.&&)
58 (||) = liftM2 (Bool.||)
59 instance Sym_Bool TextI where
60 bool a = TextI $ \_p _v ->
61 Text.pack (show a)
62 not (TextI x) =
63 TextI $ \p v ->
64 let p' = Precedence 9 in
65 paren p p' $ "not " <> x p' v
66 (&&) = textI_infix "&&" (Precedence 6)
67 (||) = textI_infix "||" (Precedence 5)
68 xor = textI_infix "`xor`" (Precedence 5)
69 instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (DupI r1 r2) where
70 bool x = bool x `DupI` bool x
71 not = dupI1 (Proxy @Sym_Bool) not
72 (&&) = dupI2 (Proxy @Sym_Bool) (&&)
73 (||) = dupI2 (Proxy @Sym_Bool) (||)
74 xor = dupI2 (Proxy @Sym_Bool) xor
75
76 instance Const_from Text cs => Const_from Text (Proxy Bool ': cs) where
77 const_from "Bool" k = k (ConstZ kind)
78 const_from s k = const_from s $ k . ConstS
79 instance Show_Const cs => Show_Const (Proxy Bool ': cs) where
80 show_const ConstZ{} = "Bool"
81 show_const (ConstS c) = show_const c
82
83 instance -- Proj_ConC
84 ( Proj_Const cs Bool
85 , Proj_Consts cs (Consts_imported_by Bool)
86 ) => Proj_ConC cs (Proxy Bool) where
87 proj_conC _ (TyConst q :$ TyConst c)
88 | Just Refl <- eq_skind (kind_of_const c) SKiType
89 , Just Refl <- proj_const c (Proxy::Proxy Bool)
90 = case () of
91 _ | Just Refl <- proj_const q (Proxy::Proxy Bounded) -> Just Con
92 | Just Refl <- proj_const q (Proxy::Proxy Enum) -> Just Con
93 | Just Refl <- proj_const q (Proxy::Proxy Eq) -> Just Con
94 | Just Refl <- proj_const q (Proxy::Proxy Ord) -> Just Con
95 | Just Refl <- proj_const q (Proxy::Proxy Show) -> Just Con
96 _ -> Nothing
97 proj_conC _c _q = Nothing
98 data instance TokenT meta (ts::[*]) (Proxy Bool)
99 = Token_Term_Bool Bool
100 | Token_Term_Bool_not
101 | Token_Term_Bool_and
102 | Token_Term_Bool_or
103 | Token_Term_Bool_xor
104 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Bool))
105 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Bool))
106 instance -- CompileI
107 ( Inj_Const (Consts_of_Ifaces is) Bool
108 , Inj_Const (Consts_of_Ifaces is) (->)
109 ) => CompileI is (Proxy Bool) where
110 compileI tok _ctx k =
111 case tok of
112 Token_Term_Bool b -> k (ty @Bool) $ TermO $ \_c -> bool b
113 Token_Term_Bool_not -> op1_from not
114 Token_Term_Bool_and -> op2_from (&&)
115 Token_Term_Bool_or -> op2_from (||)
116 Token_Term_Bool_xor -> op2_from xor
117 where
118 op1_from
119 (op::forall term. Sym_Bool term => term Bool -> term Bool) =
120 k (ty @Bool ~> ty @Bool) $ TermO $ \_c -> lam op
121 op2_from
122 (op::forall term. Sym_Bool term => term Bool -> term Bool -> term Bool) =
123 k (ty @Bool ~> ty @Bool ~> ty @Bool) $ TermO $ \_c -> lam $ lam . op