module Language.Symantic.Lib.Bool where
import Control.Monad
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding ((&&), not, (||))
import qualified Data.Bool as Bool
import qualified Data.Text as Text
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Lambda
-import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
+import Language.Symantic
+import Language.Symantic.Lib.Function ()
-- * Class 'Sym_Bool'
+type instance Sym Bool = Sym_Bool
class Sym_Bool term where
bool :: Bool -> term Bool
not :: term Bool -> term Bool
xor :: term Bool -> term Bool -> term Bool; infixr 2 `xor`
xor x y = (x || y) && not (x && y)
- default bool :: Trans t term => Bool -> t term Bool
- default not :: Trans t term => t term Bool -> t term Bool
- default (&&) :: Trans t term => t term Bool -> t term Bool -> t term Bool
- default (||) :: Trans t term => t term Bool -> t term Bool -> t term Bool
+ default bool :: Sym_Bool (UnT term) => Trans term => Bool -> term Bool
+ default not :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool
+ default (&&) :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool -> term Bool
+ default (||) :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool -> term Bool
- bool = trans_lift . bool
- not = trans_map1 not
- (&&) = trans_map2 (&&)
- (||) = trans_map2 (||)
+ bool = trans . bool
+ not = trans1 not
+ (&&) = trans2 (&&)
+ (||) = trans2 (||)
-type instance Sym_of_Iface (Proxy Bool) = Sym_Bool
-type instance TyConsts_of_Iface (Proxy Bool) = Proxy Bool ': TyConsts_imported_by (Proxy Bool)
-type instance TyConsts_imported_by (Proxy Bool) =
- [ Proxy Bounded
- , Proxy Enum
- , Proxy Eq
- , Proxy Ord
- , Proxy Show
- ]
-
-instance Sym_Bool HostI where
- bool = HostI
+-- Interpreting
+instance Sym_Bool Eval where
+ bool = Eval
not = liftM Bool.not
(&&) = liftM2 (Bool.&&)
(||) = liftM2 (Bool.||)
-instance Sym_Bool TextI where
- bool o = TextI $ \_p _v ->
- Text.pack (show o)
- not = textI1 "not"
- (&&) = textI_infix "&&" (infixR 3)
- (||) = textI_infix "||" (infixR 2)
- xor = textI_infix "`xor`" (infixR 2)
-instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (DupI r1 r2) where
- bool b = bool b `DupI` bool b
- not = dupI1 @Sym_Bool not
- (&&) = dupI2 @Sym_Bool (&&)
- (||) = dupI2 @Sym_Bool (||)
- xor = dupI2 @Sym_Bool xor
-
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Bool
- ) => Read_TyNameR TyName cs (Proxy Bool ': rs) where
- read_TyNameR _cs (TyName "Bool") k = k (ty @Bool)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Bool ': cs) where
- show_TyConst TyConstZ{} = "Bool"
- show_TyConst (TyConstS c) = show_TyConst c
+instance Sym_Bool View where
+ bool o = View $ \_p _v -> Text.pack (show o)
+ not = view1 "not"
+ (&&) = viewInfix "&&" (infixR 3)
+ (||) = viewInfix "||" (infixR 2)
+ xor = viewInfix "`xor`" (infixR 2)
+instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (Dup r1 r2) where
+ bool b = bool b `Dup` bool b
+ not = dup1 @Sym_Bool not
+ (&&) = dup2 @Sym_Bool (&&)
+ (||) = dup2 @Sym_Bool (||)
+ xor = dup2 @Sym_Bool xor
-instance Proj_TyFamC cs TyFam_MonoElement Bool
+-- Transforming
+instance (Sym_Lambda term, Sym_Bool term) => Sym_Bool (BetaT term) where
+ xor = trans2 xor
-instance -- Proj_TyConC
- ( Proj_TyConst cs Bool
- , Proj_TyConsts cs (TyConsts_imported_by (Proxy Bool))
- ) => Proj_TyConC cs (Proxy Bool) where
- proj_TyConC _ (TyConst q :$ TyConst c)
- | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
- , Just Refl <- proj_TyConst c (Proxy @Bool)
+-- Typing
+instance NameTyOf Bool where
+ nameTyOf _c = ["Bool"] `Mod` "Bool"
+instance ClassInstancesFor Bool where
+ proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
+ | Just HRefl <- proj_ConstKiTy @_ @Bool c
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Ord) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Show) -> Just TyCon
+ _ | Just Refl <- proj_Const @Bounded q -> Just Dict
+ | Just Refl <- proj_Const @Enum q -> Just Dict
+ | Just Refl <- proj_Const @Eq q -> Just Dict
+ | Just Refl <- proj_Const @Ord q -> Just Dict
+ | Just Refl <- proj_Const @Show q -> Just Dict
_ -> Nothing
- proj_TyConC _c _q = Nothing
-data instance TokenT meta (ts::[*]) (Proxy Bool)
- = Token_Term_Bool Bool
- | Token_Term_Bool_not
- | Token_Term_Bool_and
- | Token_Term_Bool_or
- | Token_Term_Bool_xor
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Bool))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Bool))
+ proveConstraintFor _c _q = Nothing
+instance TypeInstancesFor Bool
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Bool
+instance (Source src, SymInj ss Bool) => ModuleFor src ss Bool where
+ moduleFor = ["Bool"] `moduleWhere`
+ [ "False" := teBool False
+ , "True" := teBool True
+ , "not" := teBool_not
+ , "and" `withInfixR` 3 := teBool_and
+ , "or" `withInfixR` 2 := teBool_or
+ , "xor" `withInfixR` 2 := teBool_xor
+ ]
+
+-- ** 'Type's
+tyBool :: Source src => LenInj vs => Type src vs Bool
+tyBool = tyConst @(K Bool) @Bool
+
+-- ** 'Term's
+teBool :: Source src => SymInj ss Bool => Bool -> Term src ss ts '[] (() #> Bool)
+teBool b = Term noConstraint tyBool $ teSym @Bool $ bool b
+
+teBool_not :: TermDef Bool '[] (() #> (Bool -> Bool))
+teBool_not = Term noConstraint (tyBool ~> tyBool) $ teSym @Bool $ lam1 not
-instance -- CompileI
- ( Inj_TyConst cs Bool
- , Inj_TyConst cs (->)
- ) => CompileI cs is (Proxy Bool) where
- compileI tok _ctx k =
- case tok of
- Token_Term_Bool b -> k (ty @Bool) $ Term $ \_c -> bool b
- Token_Term_Bool_not -> op1_from not
- Token_Term_Bool_and -> op2_from (&&)
- Token_Term_Bool_or -> op2_from (||)
- Token_Term_Bool_xor -> op2_from xor
- where
- op1_from
- (op::forall term. Sym_Bool term => term Bool -> term Bool) =
- k (ty @Bool ~> ty @Bool) $ Term $ \_c -> lam op
- op2_from
- (op::forall term. Sym_Bool term => term Bool -> term Bool -> term Bool) =
- k (ty @Bool ~> ty @Bool ~> ty @Bool) $ Term $ \_c -> lam $ lam . op
-instance -- TokenizeT
- Inj_Token meta ts Bool =>
- TokenizeT meta ts (Proxy Bool) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ tokenize0 "False" infixN5 $ Token_Term_Bool False
- , tokenize0 "True" infixN5 $ Token_Term_Bool True
- , tokenize0 "not" infixN5 Token_Term_Bool_not
- , tokenize0 "and" (infixR 3) Token_Term_Bool_and
- , tokenize0 "or" (infixR 2) Token_Term_Bool_or
- , tokenize0 "xor" (infixR 2) Token_Term_Bool_xor
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy Bool) g
+teBool_and, teBool_or, teBool_xor :: TermDef Bool '[] (() #> (Bool -> Bool -> Bool))
+teBool_and = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 (&&)
+teBool_or = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 (||)
+teBool_xor = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 xor
sourcephile / git / haskell / symantic.git / blobdiff