-- D. Sannella. M Fourman, H. Peng and P. Wadler
-- Introduction to Computation: Haskell, Logic and Automata
-- Undergraduate Topics in Computer Science, Springer (2021)
-- ISBN 978-3-030-76907

-- Chapter 14 : Sequent Calculus

-- Required for "instance Show (u -> Bool) ..." in Exercise 1

{-# LANGUAGE FlexibleInstances #-}

module Chap14_sequent_calculus where

-- used in Exercise 1

import Test.QuickCheck (Arbitrary, arbitrary, elements, CoArbitrary, coarbitrary, variant)

-- Combining predicates

-- Predicate is from "Features and Predicates"

type Predicate u = u -> Bool

neg :: Predicate u -> Predicate u
(neg a) x = not (a x)

(&:&) :: Predicate u -> Predicate u -> Predicate u
(a &:& b) x = a x && b x

(|:|) :: Predicate u -> Predicate u -> Predicate u
(a |:| b) x = a x || b x

-- Exercise 1

-- Thing is from "Features and Predicates"

data Thing = R | S | T | U | V | W | X | Y | Z deriving (Eq,Show)

instance Arbitrary Thing where
  arbitrary = elements [R, S, T, U, V, W, X, Y, Z]

instance CoArbitrary Thing where
  coarbitrary R = variant 0
  coarbitrary S = variant 1
  coarbitrary T = variant 2
  coarbitrary U = variant 3
  coarbitrary V = variant 4
  coarbitrary W = variant 5
  coarbitrary X = variant 6
  coarbitrary Y = variant 7
  coarbitrary Z = variant 8

instance Show (u -> Bool) where
  show p = "a predicate"