]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Bool.hs
Add compileWithTyCtx.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Bool.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Bool'.
4 module Language.Symantic.Lib.Bool where
5
6 import Control.Monad
7 import Data.Proxy
8 import Data.Type.Equality ((:~:)(Refl))
9 import Prelude hiding ((&&), not, (||))
10 import qualified Data.Bool as Bool
11 import qualified Data.Text as Text
12
13 import Language.Symantic.Parsing
14 import Language.Symantic.Typing
15 import Language.Symantic.Compiling
16 import Language.Symantic.Interpreting
17 import Language.Symantic.Transforming
18 import Language.Symantic.Lib.Lambda
19 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
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; infixr 3 &&
26 (||) :: term Bool -> term Bool -> term Bool; infixr 2 ||
27 xor :: term Bool -> term Bool -> term Bool; infixr 2 `xor`
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 type instance Sym_of_Iface (Proxy Bool) = Sym_Bool
41 type instance TyConsts_of_Iface (Proxy Bool) = Proxy Bool ': TyConsts_imported_by (Proxy Bool)
42 type instance TyConsts_imported_by (Proxy Bool) =
43 [ Proxy Bounded
44 , Proxy Enum
45 , Proxy Eq
46 , Proxy Ord
47 , Proxy Show
48 ]
49
50 instance Sym_Bool HostI where
51 bool = HostI
52 not = liftM Bool.not
53 (&&) = liftM2 (Bool.&&)
54 (||) = liftM2 (Bool.||)
55 instance Sym_Bool TextI where
56 bool o = TextI $ \_p _v ->
57 Text.pack (show o)
58 not = textI1 "not"
59 (&&) = textI_infix "&&" (infixR 3)
60 (||) = textI_infix "||" (infixR 2)
61 xor = textI_infix "`xor`" (infixR 2)
62 instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (DupI r1 r2) where
63 bool b = bool b `DupI` bool b
64 not = dupI1 @Sym_Bool not
65 (&&) = dupI2 @Sym_Bool (&&)
66 (||) = dupI2 @Sym_Bool (||)
67 xor = dupI2 @Sym_Bool xor
68
69 instance
70 ( Read_TyNameR TyName cs rs
71 , Inj_TyConst cs Bool
72 ) => Read_TyNameR TyName cs (Proxy Bool ': rs) where
73 read_TyNameR _cs (TyName "Bool") k = k (ty @Bool)
74 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
75 instance Show_TyConst cs => Show_TyConst (Proxy Bool ': cs) where
76 show_TyConst TyConstZ{} = "Bool"
77 show_TyConst (TyConstS c) = show_TyConst c
78
79 instance Proj_TyFamC cs TyFam_MonoElement Bool
80
81 instance -- Proj_TyConC
82 ( Proj_TyConst cs Bool
83 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Bool))
84 ) => Proj_TyConC cs (Proxy Bool) where
85 proj_TyConC _ (TyConst q :$ TyConst c)
86 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
87 , Just Refl <- proj_TyConst c (Proxy @Bool)
88 = case () of
89 _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon
90 | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon
91 | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
92 | Just Refl <- proj_TyConst q (Proxy @Ord) -> Just TyCon
93 | Just Refl <- proj_TyConst q (Proxy @Show) -> Just TyCon
94 _ -> Nothing
95 proj_TyConC _c _q = Nothing
96 data instance TokenT meta (ts::[*]) (Proxy Bool)
97 = Token_Term_Bool Bool
98 | Token_Term_Bool_not
99 | Token_Term_Bool_and
100 | Token_Term_Bool_or
101 | Token_Term_Bool_xor
102 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Bool))
103 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Bool))
104
105 instance -- CompileI
106 ( Inj_TyConst cs Bool
107 , Inj_TyConst cs (->)
108 ) => CompileI cs is (Proxy Bool) where
109 compileI tok _ctx k =
110 case tok of
111 Token_Term_Bool b -> k (ty @Bool) $ Term $ \_c -> bool b
112 Token_Term_Bool_not -> op1_from not
113 Token_Term_Bool_and -> op2_from (&&)
114 Token_Term_Bool_or -> op2_from (||)
115 Token_Term_Bool_xor -> op2_from xor
116 where
117 op1_from
118 (op::forall term. Sym_Bool term => term Bool -> term Bool) =
119 k (ty @Bool ~> ty @Bool) $ Term $ \_c -> lam op
120 op2_from
121 (op::forall term. Sym_Bool term => term Bool -> term Bool -> term Bool) =
122 k (ty @Bool ~> ty @Bool ~> ty @Bool) $ Term $ \_c -> lam $ lam . op
123 instance -- TokenizeT
124 Inj_Token meta ts Bool =>
125 TokenizeT meta ts (Proxy Bool) where
126 tokenizeT _t = mempty
127 { tokenizers_infix = tokenizeTMod []
128 [ tokenize0 "False" infixN5 $ Token_Term_Bool False
129 , tokenize0 "True" infixN5 $ Token_Term_Bool True
130 , tokenize0 "not" infixN5 Token_Term_Bool_not
131 , tokenize0 "and" (infixR 3) Token_Term_Bool_and
132 , tokenize0 "or" (infixR 2) Token_Term_Bool_or
133 , tokenize0 "xor" (infixR 2) Token_Term_Bool_xor
134 ]
135 }
136 instance Gram_Term_AtomsT meta ts (Proxy Bool) g