module Logic.Language where

type List a = [a]

-- Formal language (/grammar/production system/whatever)
class (Eq symbol, Show symbol) => Language symbol where
  isWellFormed :: [symbol] -> Bool

  -- If Haskell had dependent types these could be generalized.

  -- axiomN : N wffs -> theorem
  axiom0 :: [[symbol]]
  axiom1 :: [[symbol] -> [symbol]]
  axiom2 :: [[symbol] -> [symbol] -> [symbol]]
  axiom3 :: [[symbol] -> [symbol] -> [symbol] -> [symbol]]

  -- inferN : N theorems -> theorem
  -- (axiom0 and infer0 would mean the same thing.)
  infer1 :: [[symbol] -> List [symbol]]
  infer2 :: [[symbol] -> [symbol] -> List [symbol]]

  axiom0 = []
  axiom1 = []
  axiom2 = []
  axiom3 = []
  infer1 = []
  infer2 = []

-- Convenience newtype so strings are less ugly
newtype Seq symbol = Seq [symbol]
instance Show a => Show (Seq a) where
  show (Seq xs) = concat $ map show xs