-- GeNeRaTeD fOr: ../../CBS/Funcons/Values/Primitive values/booleans.aterm
{-# LANGUAGE OverloadedStrings #-}

module Funcons.Core.Values.PrimitiveValues.Booleans where

import Funcons.EDSL

entities = []

types = typeEnvFromList
    [("booleans",DataTypeMembers [] [DataTypeConstructor "false" (TTuple []),DataTypeConstructor "true" (TTuple [])])]

funcons = libFromList
    [("not",StrictFuncon stepNot),("implies",StrictFuncon stepImplies),("and",StrictFuncon stepAnd),("or",StrictFuncon stepOr),("xor",StrictFuncon stepXor),("is-equal",StrictFuncon stepIs_equal),("booleans",NullaryFuncon stepBooleans),("false",NullaryFuncon stepFalse),("true",NullaryFuncon stepTrue)]

-- |
-- /booleans/ is the type of truth-values.
--   /not(_)/ is logical negation.
--   /and(...)/ is logical conjunction of a tuple of /booleans/ .
--   /or(...)/ is logical disjunction of a tuple of /booleans/ .
--   /xor(_,_)/ is exclusive disjunction of two /booleans/ .
--   /implies(_,_)/ is logical implication between two /booleans/ .
--   /is-equal(_,_)/ tests equality of arbitrary /values/ .
not_ fargs = FApp "not" (FTuple fargs)
stepNot fargs =
    evalRules [rewrite1,rewrite2] []
    where rewrite1 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "false" []] env
            rewriteTo (FName "true")
          rewrite2 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "true" []] env
            rewriteTo (FName "false")

implies_ fargs = FApp "implies" (FTuple fargs)
stepImplies fargs =
    evalRules [rewrite1,rewrite2,rewrite3,rewrite4] []
    where rewrite1 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "false" [],PADT "false" []] env
            rewriteTo (FName "true")
          rewrite2 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "false" [],PADT "true" []] env
            rewriteTo (FName "true")
          rewrite3 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "true" [],PADT "true" []] env
            rewriteTo (FName "true")
          rewrite4 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "true" [],PADT "false" []] env
            rewriteTo (FName "false")

and_ fargs = FApp "and" (FTuple fargs)
stepAnd fargs =
    evalRules [rewrite1,rewrite2,rewrite3] []
    where rewrite1 = do
            let env = emptyEnv
            env <- vsMatch fargs [] env
            rewriteTo (FName "true")
          rewrite2 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "false" [],VPAnnotated (VPSeqVar "B*" StarOp) (TName "booleans")] env
            rewriteTo (FName "false")
          rewrite3 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "true" [],VPAnnotated (VPSeqVar "B*" StarOp) (TName "booleans")] env
            rewriteTermTo (TApp "and" (TTuple [TVar "B*"])) env

or_ fargs = FApp "or" (FTuple fargs)
stepOr fargs =
    evalRules [rewrite1,rewrite2,rewrite3] []
    where rewrite1 = do
            let env = emptyEnv
            env <- vsMatch fargs [] env
            rewriteTo (FName "false")
          rewrite2 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "true" [],VPAnnotated (VPSeqVar "B*" StarOp) (TName "booleans")] env
            rewriteTo (FName "true")
          rewrite3 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "false" [],VPAnnotated (VPSeqVar "B*" StarOp) (TName "booleans")] env
            rewriteTermTo (TApp "or" (TTuple [TVar "B*"])) env

xor_ fargs = FApp "xor" (FTuple fargs)
stepXor fargs =
    evalRules [rewrite1,rewrite2,rewrite3,rewrite4] []
    where rewrite1 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "false" [],PADT "false" []] env
            rewriteTo (FName "false")
          rewrite2 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "false" [],PADT "true" []] env
            rewriteTo (FName "true")
          rewrite3 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "true" [],PADT "false" []] env
            rewriteTo (FName "true")
          rewrite4 = do
            let env = emptyEnv
            env <- vsMatch fargs [PADT "true" [],PADT "true" []] env
            rewriteTo (FName "false")

is_equal_ fargs = FApp "is-equal" (FTuple fargs)
stepIs_equal fargs =
    evalRules [rewrite1,rewrite2] []
    where rewrite1 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPMetaVar "V1",VPMetaVar "V2"] env
            env <- sideCondition (SCEquality (TVar "V1") (TVar "V2")) env
            rewriteTo (FName "true")
          rewrite2 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPMetaVar "V1",VPMetaVar "V2"] env
            env <- sideCondition (SCInequality (TVar "V1") (TVar "V2")) env
            rewriteTo (FName "false")

stepFalse = rewritten (ADTVal "false" [])

stepTrue = rewritten (ADTVal "true" [])

stepBooleans = rewriteType "booleans" []