]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Lib/Bool.hs
Add stack.yaml.
[haskell/symantic.git] / 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 qualified Data.Bool as Bool
8 import Data.Proxy
9 import qualified Data.Text as Text
10 import Data.Type.Equality ((:~:)(Refl))
11 import Prelude hiding ((&&), not, (||))
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
20 -- * Class 'Sym_Bool'
21 class Sym_Bool term where
22 bool :: Bool -> term Bool
23 not :: term Bool -> term Bool
24 (&&) :: term Bool -> term Bool -> term Bool
25 (||) :: term Bool -> term Bool -> term Bool
26 xor :: term Bool -> term Bool -> term Bool
27 xor x y = (x || y) && not (x && y)
28
29 default bool :: Trans t term => Bool -> t term Bool
30 default not :: Trans t term => t term Bool -> t term Bool
31 default (&&) :: Trans t term => t term Bool -> t term Bool -> t term Bool
32 default (||) :: Trans t term => t term Bool -> t term Bool -> t term Bool
33
34 bool = trans_lift . bool
35 not = trans_map1 not
36 (&&) = trans_map2 (&&)
37 (||) = trans_map2 (||)
38
39 infixr 2 ||
40 infixr 2 `xor`
41 infixr 3 &&
42
43 type instance Sym_of_Iface (Proxy Bool) = Sym_Bool
44 type instance Consts_of_Iface (Proxy Bool) = Proxy Bool ': Consts_imported_by Bool
45 type instance Consts_imported_by Bool =
46 [ Proxy Bounded
47 , Proxy Enum
48 , Proxy Eq
49 , Proxy Ord
50 , Proxy Show
51 ]
52
53 instance Sym_Bool HostI where
54 bool = HostI
55 not = liftM Bool.not
56 (&&) = liftM2 (Bool.&&)
57 (||) = liftM2 (Bool.||)
58 instance Sym_Bool TextI where
59 bool o = TextI $ \_p _v ->
60 Text.pack (show o)
61 not = textI1 "not"
62 (&&) = textI_infix "&&" (infixR 3)
63 (||) = textI_infix "||" (infixR 2)
64 xor = textI_infix "`xor`" (infixR 2)
65 instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (DupI r1 r2) where
66 bool b = bool b `DupI` bool b
67 not = dupI1 (Proxy @Sym_Bool) not
68 (&&) = dupI2 (Proxy @Sym_Bool) (&&)
69 (||) = dupI2 (Proxy @Sym_Bool) (||)
70 xor = dupI2 (Proxy @Sym_Bool) xor
71
72 instance
73 ( Read_TypeNameR Type_Name cs rs
74 , Inj_Const cs Bool
75 ) => Read_TypeNameR Type_Name cs (Proxy Bool ': rs) where
76 read_typenameR _cs (Type_Name "Bool") k = k (ty @Bool)
77 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
78 instance Show_Const cs => Show_Const (Proxy Bool ': cs) where
79 show_const ConstZ{} = "Bool"
80 show_const (ConstS c) = show_const c
81
82 instance -- Proj_ConC
83 ( Proj_Const cs Bool
84 , Proj_Consts cs (Consts_imported_by Bool)
85 ) => Proj_ConC cs (Proxy Bool) where
86 proj_conC _ (TyConst q :$ TyConst c)
87 | Just Refl <- eq_skind (kind_of_const c) SKiType
88 , Just Refl <- proj_const c (Proxy @Bool)
89 = case () of
90 _ | Just Refl <- proj_const q (Proxy @Bounded) -> Just Con
91 | Just Refl <- proj_const q (Proxy @Enum) -> Just Con
92 | Just Refl <- proj_const q (Proxy @Eq) -> Just Con
93 | Just Refl <- proj_const q (Proxy @Ord) -> Just Con
94 | Just Refl <- proj_const q (Proxy @Show) -> Just Con
95 _ -> Nothing
96 proj_conC _c _q = Nothing
97 data instance TokenT meta (ts::[*]) (Proxy Bool)
98 = Token_Term_Bool Bool
99 | Token_Term_Bool_not
100 | Token_Term_Bool_and
101 | Token_Term_Bool_or
102 | Token_Term_Bool_xor
103 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Bool))
104 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Bool))
105 instance -- CompileI
106 ( Inj_Const (Consts_of_Ifaces is) Bool
107 , Inj_Const (Consts_of_Ifaces is) (->)
108 ) => CompileI is (Proxy Bool) where
109 compileI tok _ctx k =
110 case tok of
111 Token_Term_Bool b -> k (ty @Bool) $ TermO $ \_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) $ TermO $ \_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) $ TermO $ \_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