{-# LANGUAGE BlockArguments      #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE ViewPatterns        #-}

module Dovetail.Core.Data.HeytingAlgebra where

import Data.Foldable (fold)
import Dovetail
import Dovetail.Evaluate (builtIn)

env :: forall ctx. Env ctx
env :: Env ctx
env = do
  let _ModuleName :: ModuleName
_ModuleName = Text -> ModuleName
ModuleName Text
"Data.HeytingAlgebra"

  [Env ctx] -> Env ctx
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
    [ -- boolConj :: Boolean -> Boolean -> Boolean
      ModuleName -> Text -> (Bool -> Bool -> Eval ctx Bool) -> Env ctx
forall ctx a. ToValue ctx a => ModuleName -> Text -> a -> Env ctx
builtIn @ctx @(Bool -> Bool -> Eval ctx Bool) 
        ModuleName
_ModuleName Text
"boolConj" 
        \Bool
b1 Bool
b2 -> Bool -> Eval ctx Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
b1 Bool -> Bool -> Bool
&& Bool
b2)
    , -- boolDisj :: Boolean -> Boolean -> Boolean
      ModuleName -> Text -> (Bool -> Bool -> Eval ctx Bool) -> Env ctx
forall ctx a. ToValue ctx a => ModuleName -> Text -> a -> Env ctx
builtIn @ctx @(Bool -> Bool -> Eval ctx Bool) 
        ModuleName
_ModuleName Text
"boolDisj" 
        \Bool
b1 Bool
b2 -> Bool -> Eval ctx Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
b1 Bool -> Bool -> Bool
|| Bool
b2)
    , -- boolNot :: Boolean -> Boolean
      ModuleName -> Text -> (Bool -> Eval ctx Bool) -> Env ctx
forall ctx a. ToValue ctx a => ModuleName -> Text -> a -> Env ctx
builtIn @ctx @(Bool -> Eval ctx Bool) 
        ModuleName
_ModuleName Text
"boolNot"
        \Bool
b -> Bool -> Eval ctx Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Bool
not Bool
b)
    ]