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