cg-0.0.9.0: CG/Base.hs

{-# LANGUAGE DeriveGeneric, TypeSynonymInstances, FlexibleInstances,
    FlexibleContexts, RecordWildCards, UndecidableInstances #-}
module CG.Base (ConId(..)
               ,nullary,unary,binary
               ,unaryLogical,unaryStructural
               ,binaryLogical,binaryStructural
               ,sequents
               ,toLogical,toStructural
               ,ASCII(..),Result(..)
               ,module X
               ) where


import CG.Prover as X
import Control.DeepSeq (NFData)
import Data.Hashable   (Hashable)
import Data.Serialize  (Serialize)
import Data.Void       (Void)
import GHC.Generics    (Generic)


-- * Operators

data ConId

  -- atomic formulas
  = PosAtom String
  | NegAtom String

  -- mediator between logical and structural formulas
  | Down

  -- logical operators
  | FProd | FImpR | FImpL
  | FPlus | FSubL | FSubR
  | F0L   | F0R   | FBox
  | F1L   | F1R   | FDia

  -- structural operators
  | SProd | SImpR | SImpL
  | SPlus | SSubL | SSubR
  | S0L   | S0R   | SBox
  | S1L   | S1R   | SDia
  | Comma

  -- hollow product and slashes
  | HProd | HImpR | HImpL

  -- sequents
  | JAlgebr | JStruct
  | JFocusL | JFocusR

  deriving (Eq,Ord,Show,Generic)


instance Hashable  ConId
instance NFData    ConId
instance Serialize ConId


-- * Groupings of operators.

unaryLogical :: [ConId]
unaryLogical = [F0L, F0R, FBox, F1L, F1R, FDia, HProd, HImpR, HImpL]

unaryStructural :: [ConId]
unaryStructural = [S0L, S0R, SBox, S1L, S1R, SDia]

binaryLogical :: [ConId]
binaryLogical = [FProd, FImpR, FImpL, FPlus, FSubL, FSubR]

binaryStructural :: [ConId]
binaryStructural = [SProd, SImpR, SImpL, SPlus, SSubL, SSubR, Comma]

sequents :: [ConId]
sequents = [JAlgebr, JStruct, JFocusL, JFocusL]


-- |Convert structural operators to their logical equivalents.
toLogical :: ConId -> ConId
toLogical SProd = FProd
toLogical SImpR = FImpR
toLogical SImpL = FImpL
toLogical SPlus = FPlus
toLogical SSubL = FSubL
toLogical SSubR = FSubR
toLogical S0L   = F0L
toLogical S0R   = F0R
toLogical SBox  = FBox
toLogical S1L   = F1L
toLogical S1R   = F1R
toLogical SDia  = FDia
toLogical c     = c


-- |Convert logical operators to their structural equivalents.
toStructural :: ConId -> ConId
toStructural FProd = SProd
toStructural FImpR = SImpR
toStructural FImpL = SImpL
toStructural FPlus = SPlus
toStructural FSubL = SSubL
toStructural FSubR = SSubR
toStructural F0L   = S0L
toStructural F0R   = S0R
toStructural FBox  = SBox
toStructural F1L   = S1L
toStructural F1R   = S1R
toStructural FDia  = SDia
toStructural c     = c


-- * Utility constructors

nullary :: ConId -> Term ConId v
nullary c = Con c []

unary   :: ConId -> Term ConId v -> Term ConId v
unary   c x = Con c [x]

binary  :: ConId -> Term ConId v -> Term ConId v -> Term ConId v
binary  c x y = Con c [x,y]


-- * Guards

instance Guardable ConId where

  isAtomic (Con (PosAtom _) _) = True
  isAtomic (Con (NegAtom _) _) = True
  isAtomic _                   = False

  isPositive (Var          _)    = True
  isPositive (Con (PosAtom _) _) = True
  isPositive (Con (NegAtom _) _) = False
  isPositive (Con  FProd   _)    = True
  isPositive (Con  FSubL   _)    = True
  isPositive (Con  FSubR   _)    = True
  isPositive (Con  HProd   _)    = True
  isPositive (Con  F1L     _)    = True
  isPositive (Con  F1R     _)    = True
  isPositive (Con  FDia    _)    = True
  isPositive _                   = False

  isNegative (Var          _)    = True
  isNegative (Con (PosAtom _) _) = False
  isNegative (Con (NegAtom _) _) = True
  isNegative (Con  FPlus   _)    = True
  isNegative (Con  FImpR   _)    = True
  isNegative (Con  FImpL   _)    = True
  isNegative (Con  HImpR   _)    = True
  isNegative (Con  HImpL   _)    = True
  isNegative (Con  F0L     _)    = True
  isNegative (Con  F0R     _)    = True
  isNegative (Con  FBox    _)    = True
  isNegative _                   = False



-- * Printing

instance ToString ConId where
  toString (PosAtom x) = x
  toString (NegAtom x) = x ++ "⁻"
  toString F0L     = "₀"; toString F0R     = "⁰"; toString FBox  = "□"
  toString F1L     = "₁"; toString F1R     = "¹"; toString FDia  = "◇"
  toString FProd   = "⊗"; toString FImpR   = "⇒"; toString FImpL = "⇐"
  toString SProd   = "⊗"; toString SImpR   = "⇒"; toString SImpL = "⇐"
  toString HProd   = "∘"; toString HImpR   = "⇨"; toString HImpL = "⇦"
  toString FPlus   = "⊕"; toString FSubL   = "⇚"; toString FSubR = "⇛"
  toString SPlus   = "⊕"; toString SSubL   = "⇚"; toString SSubR = "⇛"
  toString S0L     = "₀"; toString S0R     = "⁰"; toString SBox  = "[]"
  toString S1L     = "₁"; toString S1R     = "¹"; toString SDia  = "⟨⟩"
  toString JAlgebr = "⊢"; toString JStruct = "⊢"
  toString JFocusL = "⊢"; toString JFocusR = "⊢"
  toString Down    = "·"; toString Comma   = ","

instance Operator ConId where

  prec (PosAtom _) = 0
  prec (NegAtom _) = 0
  prec F0L     = 9; prec F0R     = 9; prec FBox  = 9
  prec F1L     = 9; prec F1R     = 9; prec FDia  = 9
  prec FProd   = 8; prec FImpR   = 7; prec FImpL = 7
  prec FPlus   = 8; prec FSubL   = 7; prec FSubR = 7
  prec HProd   = 8; prec HImpR   = 7; prec HImpL = 7
  prec S0L     = 6; prec S0R     = 6; prec SBox  = 0
  prec S1L     = 6; prec S1R     = 6; prec SDia  = 0
  prec SProd   = 5; prec SImpR   = 4; prec SImpL = 4
  prec SPlus   = 5; prec SSubL   = 4; prec SSubR = 4
  prec JAlgebr = 0; prec JStruct = 0
  prec JFocusL = 0; prec JFocusR = 0
  prec Down    = 0; prec Comma   = 3

  template (PosAtom x) _ = showString x . showChar ' '
  template (NegAtom x) _ = showString x . showString "⁻ "
  template F0L     [x]   = showString "₀ " . x
  template F0R     [x]   = x . showString "⁰ "
  template FBox    [x]   = showString "□ " . x
  template F1L     [x]   = showString "₁ " . x
  template F1R     [x]   = x . showString "¹ "
  template FDia    [x]   = showString "◇ " . x
  template FProd   [x,y] = x . showString "⊗ " . y
  template FImpR   [x,y] = x . showString "⇒ " . y
  template FImpL   [x,y] = x . showString "⇐ " . y
  template SProd   [x,y] = x . showString "⊗ " . y
  template SImpR   [x,y] = x . showString "⇒ " . y
  template SImpL   [x,y] = x . showString "⇐ " . y
  template HProd   [x,y] = x . showString "∘ " . y
  template HImpR   [x,y] = x . showString "⇨ " . y
  template HImpL   [x,y] = x . showString "⇦ " . y
  template FPlus   [x,y] = x . showString "⊕ " . y
  template FSubL   [x,y] = x . showString "⇚ " . y
  template FSubR   [x,y] = x . showString "⇛ " . y
  template SPlus   [x,y] = x . showString "⊕ " . y
  template SSubL   [x,y] = x . showString "⇚ " . y
  template SSubR   [x,y] = x . showString "⇛ " . y
  template S0L     [x]   = showString "₀ " . x
  template S0R     [x]   = x . showString "⁰ "
  template SBox    [x]   = showString "[ " . x . showString "]"
  template S1L     [x]   = showString "₁ " . x
  template S1R     [x]   = x . showString "¹ "
  template SDia    [x]   = showString "⟨ " . x . showString "⟩"
  template JAlgebr [x,y] = x . showString "⊢ " . y
  template JStruct [x,y] = x . showString "⊢ " . y
  template JFocusL [x,y] = showString "[ " . x . showString "]⊢ " . y
  template JFocusR [x,y] = x . showString "⊢[ " . y . showString "] "
  template Down    [x]   = showString "· " . x . showString "· "
  template Comma   [x,y] = x . showString ", " . y


-- * ASCII printing

newtype ASCII a = ASCII a

instance ToString (ASCII ConId) where
  toString (ASCII (PosAtom x)) = x
  toString (ASCII (NegAtom x)) = x ++ "'"
  toString (ASCII F0L)     = "0" ; toString (ASCII F0R)     = "0" ; toString (ASCII FBox)  = "[]"
  toString (ASCII F1L)     = "1" ; toString (ASCII F1R)     = "1" ; toString (ASCII FDia)  = "<>"
  toString (ASCII FProd)   = "*" ; toString (ASCII FImpR)   = "->"; toString (ASCII FImpL) = "<-"
  toString (ASCII SProd)   = "*" ; toString (ASCII SImpR)   = "->"; toString (ASCII SImpL) = "<-"
  toString (ASCII HProd)   = "o" ; toString (ASCII HImpR)   = "-o"; toString (ASCII HImpL) = "o-"
  toString (ASCII FPlus)   = "+" ; toString (ASCII FSubL)   = "<="; toString (ASCII FSubR) = "=>"
  toString (ASCII SPlus)   = "+" ; toString (ASCII SSubL)   = "<="; toString (ASCII SSubR) = "=>"
  toString (ASCII S0L)     = "0" ; toString (ASCII S0R)     = "0" ; toString (ASCII SBox)  = "[]"
  toString (ASCII S1L)     = "1" ; toString (ASCII S1R)     = "1" ; toString (ASCII SDia)  = "<>"
  toString (ASCII JAlgebr) = "|-"; toString (ASCII JStruct) = "|-"
  toString (ASCII JFocusL) = "|-"; toString (ASCII JFocusR) = "|-"
  toString (ASCII Down)    = "." ; toString (ASCII Comma)   = ","


-- * Proofs

type Proof = Term RuleId Void

data Result
  = Solved                 (Term ConId Void) Proof
  | Parsed String [String] (Term ConId Void) Proof
  deriving (Show)