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