content: {-# LANGUAGE ScopedTypeVariables, MultiParamTypeClasses,
               FunctionalDependencies #-}
  {- |
  Module      :  $EmptyHeader$
  Description :  <optional short description entry>
  Copyright   :  (c) <Authors or Affiliations>
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  <email>
  Stability   :  unstable | experimental | provisional | stable | frozen
  Portability :  portable | non-portable (<reason>)
  
  <optional description>
  -}
  module Comp where
  
  import Debug.Trace
  import qualified Data.Set as Set
  import qualified Data.Map as Map
  
  data Boole a = F | T | And (Boole a) (Boole a) | Or (Boole a) (Boole a) |
                Not (Boole a) | At a deriving (Eq, Ord, Show)
  
  data K l = K (Boole l) deriving (Eq, Ord, Show)
  
  data RK = RK Int deriving Show
  
  data KD l = KD (Boole l) deriving (Eq, Ord, Show)
  
  data RKD = RKDPos Int | RKDNeg Int deriving Show
  
  data Segala a = S (Boole (KD (Boole (K (Segala a))))) deriving (Eq, Show)
  
  data Clause a = Implies (Set.Set a) (Set.Set a) deriving (Eq, Ord, Show)
  
  data Subst a = Subst (Map.Map Int a) deriving (Eq, Show)
  
  class Logic a b | a -> b, b -> a where
    match :: Clause (a c) -> [(b, Subst (Boole c))]
    clauses :: b -> [Clause Int]
    subclauses :: Ord c => Clause (a c) -> Set.Set (Clause (a c))
  
  instance Logic K RK where
    match ((Implies n p) :: Clause (K c)) =
      let i = Set.size n
          strip (K x) = x
          substHead = (i + 1, strip (head (Set.elems p)))
          substTail = zip [1 .. i] (map strip (Set.elems n))
      in [(RK i, Subst (Map.fromList (substHead : substTail)))]
    clauses (RK n) = [Implies (Set.fromList [1 .. n]) (Set.singleton (n + 1))]
    subclauses (Implies n p) =
      Set.fromList [Implies n (Set.singleton l) | l <- Set.elems p]
  
  instance Logic KD RKD where
    match ((Implies n p) :: Clause (KD c)) =
      let i = Set.size n
          strip (KD x) = x
          substHead = (i + 1, strip (head (Set.elems p)))
          substTail = zip [1 .. i] (map strip (Set.elems n))
      in [(RKDPos i, Subst (Map.fromList (substHead : substTail)))]
    clauses (RKDPos n) = [Implies (Set.fromList [1 .. n]) (Set.singleton (n + 1))]
    clauses (RKDNeg n) = [Implies (Set.fromList [1 .. n]) (Set.singleton (n + 1))]
    subclauses (Implies n p) =
      Set.fromList [Implies n (Set.singleton l) | l <- Set.elems p]
  