-- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Primitive/Booleans/Booleans.cbs
{-# LANGUAGE OverloadedStrings #-}

module Funcons.Core.Values.Primitive.Booleans.Booleans where

import Funcons.EDSL

import Funcons.Operations hiding (Values,libFromList)
entities :: [a]
entities = []

types :: TypeRelation
types = [(Name, DataTypeMembers)] -> TypeRelation
typeEnvFromList
    [(Name
"booleans",Name -> [TPattern] -> [DataTypeAltt] -> DataTypeMembers
DataTypeMemberss Name
"booleans" [] [Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"true" [] ([TPattern] -> Maybe [TPattern]
forall a. a -> Maybe a
Just []),Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"false" [] ([TPattern] -> Maybe [TPattern]
forall a. a -> Maybe a
Just [])]),(Name
"bools",Name -> [TPattern] -> [DataTypeAltt] -> DataTypeMembers
DataTypeMemberss Name
"bools" [] [Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"true" [] ([TPattern] -> Maybe [TPattern]
forall a. a -> Maybe a
Just []),Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"false" [] ([TPattern] -> Maybe [TPattern]
forall a. a -> Maybe a
Just [])])]

funcons :: FunconLibrary
funcons = [(Name, EvalFunction)] -> FunconLibrary
libFromList
    [(Name
"true",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepTrue),(Name
"false",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepFalse),(Name
"not",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepNot),(Name
"implies",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepImplies),(Name
"and",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepAnd),(Name
"or",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepOr),(Name
"exclusive-or",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepExclusive_or),(Name
"xor",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepExclusive_or),(Name
"booleans",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepBooleans),(Name
"bools",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepBooleans)]

true_ :: Funcons
true_ = Name -> Funcons
FName Name
"true"
stepTrue :: NullaryFuncon
stepTrue = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"datatype-value" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"list" [Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
116)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
114)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
117)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
101)])]))]) Env
forall k a. Map k a
env

false_ :: Funcons
false_ = Name -> Funcons
FName Name
"false"
stepFalse :: NullaryFuncon
stepFalse = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"datatype-value" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"list" [Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
102)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
97)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
108)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
115)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
101)])]))]) Env
forall k a. Map k a
env

not_ :: [Funcons] -> Funcons
not_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"not" ([Funcons]
fargs)
stepNot :: StrictFuncon
stepNot [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"false" []] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"true") Env
env
          rewrite2 :: NullaryFuncon
rewrite2 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"true" []] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"false") Env
env

implies_ :: [Funcons] -> Funcons
implies_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"implies" ([Funcons]
fargs)
stepImplies :: StrictFuncon
stepImplies [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2,NullaryFuncon
rewrite3,NullaryFuncon
rewrite4] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"false" [],Name -> [VPattern] -> VPattern
PADT Name
"false" []] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"true") Env
env
          rewrite2 :: NullaryFuncon
rewrite2 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"false" [],Name -> [VPattern] -> VPattern
PADT Name
"true" []] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"true") Env
env
          rewrite3 :: NullaryFuncon
rewrite3 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"true" [],Name -> [VPattern] -> VPattern
PADT Name
"true" []] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"true") Env
env
          rewrite4 :: NullaryFuncon
rewrite4 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"true" [],Name -> [VPattern] -> VPattern
PADT Name
"false" []] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"false") Env
env

and_ :: [Funcons] -> Funcons
and_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"and" ([Funcons]
fargs)
stepAnd :: StrictFuncon
stepAnd [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2,NullaryFuncon
rewrite3] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"true") Env
env
          rewrite2 :: NullaryFuncon
rewrite2 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"false" [],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"___" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"booleans") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"false") Env
env
          rewrite3 :: NullaryFuncon
rewrite3 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"true" [],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"B*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"booleans") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"and" [MetaVar -> FTerm
TVar MetaVar
"B*"]) Env
env

or_ :: [Funcons] -> Funcons
or_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"or" ([Funcons]
fargs)
stepOr :: StrictFuncon
stepOr [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2,NullaryFuncon
rewrite3] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"false") Env
env
          rewrite2 :: NullaryFuncon
rewrite2 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"true" [],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"___" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"booleans") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"true") Env
env
          rewrite3 :: NullaryFuncon
rewrite3 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"false" [],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"B*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"booleans") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"or" [MetaVar -> FTerm
TVar MetaVar
"B*"]) Env
env

exclusive_or_ :: [Funcons] -> Funcons
exclusive_or_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"exclusive-or" ([Funcons]
fargs)
xor_ :: [Funcons] -> Funcons
xor_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"exclusive-or" ([Funcons]
fargs)
stepExclusive_or :: StrictFuncon
stepExclusive_or [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2,NullaryFuncon
rewrite3,NullaryFuncon
rewrite4] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"false" [],Name -> [VPattern] -> VPattern
PADT Name
"false" []] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"false") Env
env
          rewrite2 :: NullaryFuncon
rewrite2 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"false" [],Name -> [VPattern] -> VPattern
PADT Name
"true" []] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"true") Env
env
          rewrite3 :: NullaryFuncon
rewrite3 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"true" [],Name -> [VPattern] -> VPattern
PADT Name
"false" []] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"true") Env
env
          rewrite4 :: NullaryFuncon
rewrite4 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"true" [],Name -> [VPattern] -> VPattern
PADT Name
"true" []] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"false") Env
env

booleans_ :: Funcons
booleans_ = Name -> Funcons
FName Name
"booleans"
stepBooleans :: NullaryFuncon
stepBooleans = Name -> StrictFuncon
rewriteType Name
"booleans" []