module Logic.Language where

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

-- 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 :: [TypeAxiom0 symbol]
  axiom1 :: [TypeAxiom1 symbol]
  axiom2 :: [TypeAxiom2 symbol]
  axiom3 :: [TypeAxiom3 symbol]

  axiom0 = []
  axiom1 = []
  axiom2 = []
  axiom3 = []

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

  infer1 = []
  infer2 = []

type TypeAxiom0 s = [s]
type TypeAxiom1 s = [s] -> [s]
type TypeAxiom2 s = [s] -> [s] -> [s]
type TypeAxiom3 s = [s] -> [s] -> [s] -> [s]

type TypeInfer1 s = [s] -> [[s]]
type TypeInfer2 s = [s] -> [s] -> [[s]]