]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Bool.hs
Separate tests into test/.
[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 Prelude hiding ((&&), not, (||))
8 import qualified Data.Bool as Bool
9 import qualified Data.Text as Text
10
11 import Language.Symantic
12 import Language.Symantic.Lib.Function ()
13
14 -- * Class 'Sym_Bool'
15 type instance Sym Bool = Sym_Bool
16 class Sym_Bool term where
17 bool :: Bool -> term Bool
18 not :: term Bool -> term Bool
19 (&&) :: term Bool -> term Bool -> term Bool; infixr 3 &&
20 (||) :: term Bool -> term Bool -> term Bool; infixr 2 ||
21 xor :: term Bool -> term Bool -> term Bool; infixr 2 `xor`
22 xor x y = (x || y) && not (x && y)
23
24 default bool :: Sym_Bool (UnT term) => Trans term => Bool -> term Bool
25 default not :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool
26 default (&&) :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool -> term Bool
27 default (||) :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool -> term Bool
28
29 bool = trans . bool
30 not = trans1 not
31 (&&) = trans2 (&&)
32 (||) = trans2 (||)
33
34 -- Interpreting
35 instance Sym_Bool Eval where
36 bool = Eval
37 not = liftM Bool.not
38 (&&) = liftM2 (Bool.&&)
39 (||) = liftM2 (Bool.||)
40 instance Sym_Bool View where
41 bool o = View $ \_p _v -> Text.pack (show o)
42 not = view1 "not"
43 (&&) = viewInfix "&&" (infixR 3)
44 (||) = viewInfix "||" (infixR 2)
45 xor = viewInfix "`xor`" (infixR 2)
46 instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (Dup r1 r2) where
47 bool b = bool b `Dup` bool b
48 not = dup1 @Sym_Bool not
49 (&&) = dup2 @Sym_Bool (&&)
50 (||) = dup2 @Sym_Bool (||)
51 xor = dup2 @Sym_Bool xor
52
53 -- Transforming
54 instance (Sym_Lambda term, Sym_Bool term) => Sym_Bool (BetaT term) where
55 xor = trans2 xor
56
57 -- Typing
58 instance NameTyOf Bool where
59 nameTyOf _c = ["Bool"] `Mod` "Bool"
60 instance ClassInstancesFor Bool where
61 proveConstraintFor _ (TyConst _ _ q :@ b)
62 | Just HRefl <- proj_ConstKiTy @_ @Bool b
63 = case () of
64 _ | Just Refl <- proj_Const @Bounded q -> Just Dict
65 | Just Refl <- proj_Const @Enum q -> Just Dict
66 | Just Refl <- proj_Const @Eq q -> Just Dict
67 | Just Refl <- proj_Const @Ord q -> Just Dict
68 | Just Refl <- proj_Const @Show q -> Just Dict
69 _ -> Nothing
70 proveConstraintFor _c _q = Nothing
71 instance TypeInstancesFor Bool
72
73 -- Compiling
74 instance Gram_Term_AtomsFor src ss g Bool
75 instance (Source src, SymInj ss Bool) => ModuleFor src ss Bool where
76 moduleFor = ["Bool"] `moduleWhere`
77 [ "False" := teBool False
78 , "True" := teBool True
79 , "not" := teBool_not
80 , "and" `withInfixR` 3 := teBool_and
81 , "or" `withInfixR` 2 := teBool_or
82 , "xor" `withInfixR` 2 := teBool_xor
83 ]
84
85 -- ** 'Type's
86 tyBool :: Source src => LenInj vs => Type src vs Bool
87 tyBool = tyConst @(K Bool) @Bool
88
89 -- ** 'Term's
90 teBool :: Source src => SymInj ss Bool => Bool -> Term src ss ts '[] (() #> Bool)
91 teBool b = Term noConstraint tyBool $ teSym @Bool $ bool b
92
93 teBool_not :: TermDef Bool '[] (() #> (Bool -> Bool))
94 teBool_not = Term noConstraint (tyBool ~> tyBool) $ teSym @Bool $ lam1 not
95
96 teBool_and, teBool_or, teBool_xor :: TermDef Bool '[] (() #> (Bool -> Bool -> Bool))
97 teBool_and = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 (&&)
98 teBool_or = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 (||)
99 teBool_xor = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 xor