module Hylotab where 

import Data.List  ( nub, intersect, (\\) )
import Form ( Form(..), NomSymbol(..), PropSymbol(..), RelSymbol(..), Rel, parse )
import Control.Monad(when)

type Index    = Int
type Domain   = [NomSymbol]

{- Generic Satisfiability Checking -}

-- Distinguish between two modes of satisfiability checking: 

data Mode = Extend -- for extending with a new nominal at each
                   --                 encounter with a diamond
          | Try    -- for trial and error extension, including
                   --               checking existing nominals

-- If psi defines a frame property, then any model M satisfying (A psi)
-- will be in the frame class with that property. For suppose that
-- M does not have the frame property. Then there is a world w with
-- M , w |/= psi, hence M |/= A psi. Thus, we can
-- build an engine for the frame class of psi by loading the proof
-- engine with (A psi) as a universal constraint. This leads to the
-- following generic satisfiability checker (the first argument gives
-- the mode of satisfiability checking, the second argument lists the
-- formulas defining the frame class under consideration):

data SatFlag = SAT Tableau | UNSAT

genSat  :: Bool -> Mode -> [Form] -> Form -> IO SatFlag
genSat verbose Extend props form =
 do res <- expand verbose (initTab form props)
    case res of
     OPEN nodes -> return $ SAT nodes
     CLOSED     -> return UNSAT
genSat verbose Try    props form =
 do res <- cautiousExpand verbose (initTab form props)
    case res of
     OPEN nodes -> return $ SAT nodes
     CLOSED     -> return UNSAT

{- Theorem Proving -}

-- The function initTab creates an initial tableau for a
-- formula. The initial tableau for phi is just one node, with list of
-- pending formulas [@ m phi], where m is a fresh nominal. We assume
-- that no nominals of the form (N i) appear in the formula. The
-- node index is set to the index of the first fresh constant nominal,
-- i.e., 1.

initTab :: Form  -> [Form] -> Tableau 
initTab form props = 
   [Nd {idx = 1 + newIdx,
        dom = dom',
        neqs = [], accs = [], ufs = [],
        boxes = [], cboxes = [], pos = [],
        neg = [], forms= forms'
       }
   ]
  where noms = nomsInForms (form:props)
        newIdx = case noms of
                   [] -> 0
                   _  -> 1 + maximum [ n | (N n)  <- noms]
        newNom = N newIdx
        dom' =  newNom : nomsInForms (form:props)
        forms' = [At newNom form] ++
                  case props of
                   []     -> []
                   [prop] -> [At newNom (A prop)]
                   _      -> [At newNom (A (Conj props))]

{- Tableau Nodes and Tableaux -}

                                                       -- A node of a tableau consists of 
data Node = Nd {   idx :: Index,                       -- a tableau index (needed to generate fresh tableau parameters)
                   dom :: Domain,                      -- a domain (all nominals occurring at the node)
                  neqs :: [(NomSymbol,NomSymbol)],     -- a list of n != m constraints on the node
                  accs :: [(NomSymbol,Rel,NomSymbol)], -- a list of n<Ri>m accessibilities on the node 
                   ufs :: [Form],                      -- the A formulas that have been applied to all nominals in the domain of the node 
                 boxes :: [(NomSymbol,Rel,Form)],      -- the (@n [i] phi) formulas of the node that have been combined
                                                       -- with all the (n<i>m) accessibilities on the node
                                                       -- (the boxed constraints of the node)
                cboxes :: [(NomSymbol,Rel,Form)],      -- the (@n [-i] phi) formulas of the node that have
                                                       -- been combined with all the (m<i>n) accessibilities on the node
                                                       -- (the converse boxed constraints of the node)
                   pos :: [(NomSymbol,PropSymbol)],    -- the positive atom attributions (@ n p_i) on the node
                   neg :: [(NomSymbol,PropSymbol)],    -- the negative atom attributions (@ n - p_i) on the node
                 forms :: [Form]                       -- pending formulas yet to be treated by the proof engine 
               }
              deriving (Eq)

instance Show Node where
 show nd
   = unlines ["Node:",
              "index: "    ++ show (idx nd),
              "domain: "   ++ show (dom nd),
              "neqs: "     ++ show (neqs nd),
              "accs: "     ++ show (accs nd),
              "ufs:  "     ++ show (ufs nd),
              "boxes: "    ++ show (boxes nd),
              "cboxes: "   ++ show (cboxes nd),
              "pos: "      ++ show (pos nd),
              "neg: "      ++ show (neg nd),
              "formulas: " ++ show (forms nd)]

type Tableau = [Node]

-- collect the constant nominals and the free occurrences of
-- variable nominals from a formula or a formula list. 
nomsInForm :: Form -> [NomSymbol]
nomsInForm (Nom nom)      = [nom]
nomsInForm (Neg f)        = nomsInForm f
nomsInForm (Conj fs)      = nomsInForms fs
nomsInForm (Disj fs)      = nomsInForms fs
nomsInForm (Impl f1 f2)   = nomsInForms [f1,f2]
nomsInForm (A f)          = nomsInForm f
nomsInForm (E f)          = nomsInForm f
nomsInForm (Box _ f)      = nomsInForm f
nomsInForm (Dia _ f)      = nomsInForm f
nomsInForm (At nom f)     = add nom (nomsInForm f)
nomsInForm (Down x f)     = filter (/= x) (nomsInForm f)
nomsInForm _              = []

nomsInForms :: [Form] -> [NomSymbol]
nomsInForms = nub . concatMap nomsInForm 

type Subst = (NomSymbol,NomSymbol)

-- Application of a substitution to a nominal:
appNom :: Subst -> NomSymbol -> NomSymbol
appNom (n,m) nom = if n == nom then m else nom 

-- Application of a substitution to a domain. Note that the substitution
-- may identify individuals, so after the substitutition we have to clean
-- up the list with nub to remove possible duplicates.
appDomain :: Subst -> Domain -> Domain
appDomain = map . appNom

appNNs :: Subst -> [(NomSymbol,NomSymbol)] -> [(NomSymbol,NomSymbol)]
appNNs b = map (\ (n,m) -> (appNom b n, appNom b m))

appNRNs :: Subst -> [(NomSymbol,Rel,NomSymbol)] -> [(NomSymbol,Rel,NomSymbol)]
appNRNs b = map (\ (n,r,m) -> (appNom b n, r, appNom b m))

appNPs :: Subst -> [(NomSymbol,PropSymbol)] -> [(NomSymbol,PropSymbol)]
appNPs b = map (\ (n,name) -> (appNom b n, name))

-- Application of a substitution to a formula or a formula list.  
-- Note that substitutions only affect the _free_ 
-- variables of a formula

appF :: Subst -> Form -> Form 
appF _ Top             = Top
appF _ Bot             = Bot
appF _ (Prop p)        = Prop p
appF b (Nom nom)       = Nom (appNom b nom)
appF b (Neg f)         = Neg (appF b f)
appF b (Conj fs)       = Conj (appFs b fs)
appF b (Disj fs)       = Disj (appFs b fs)
appF b (Impl f1 f2)    = Impl (appF b f1) (appF b f2)
appF b (A f)           = A (appF b f)
appF b (E f)           = E (appF b f)
appF b (Box r f)       = Box r (appF b f)
appF b (Dia r f)       = Dia r (appF b f)
appF b (IBox r f)      = IBox r (appF b f)
appF b (IDia r f)      = IDia r (appF b f)
appF b (At n f)        = At (appNom b n) (appF b f)
appF b (Down n f)      = Down (appNom b n) (appF b f) 

appFs :: Subst -> [Form] -> [Form]
appFs = map . appF 

appNRFs :: Subst -> [(NomSymbol,Rel,Form)] -> [(NomSymbol,Rel,Form)]
appNRFs b = map (\ (n,r,f) -> (appNom b n, r, appF b f))

{- Formulas compensating lack of pattern matching -}
  
isAlpha, isBeta :: Form -> Bool
isAlpha (Conj _)         = True
isAlpha (Neg (Disj _))   = True
isAlpha (Neg (Impl _ _)) = True
isAlpha _                = False 
isBeta (Disj _)          = True
isBeta (Impl _ _)        = True 
isBeta (Neg (Conj _))    = True
isBeta _                 = False

isA, isE :: Form -> Bool
isA (A _)             = True
isA (Neg (E _))       = True
isA _                 = False
isE (E _)             = True
isE (Neg (A _))       = True
isE _                 = False

isBox, isDiamond :: Form -> Bool
isBox (Box _ _)             = True
isBox (Neg (Dia _ _))       = True
isBox  _                    = False
isDiamond (Dia _ _)         = True
isDiamond (Neg (Box _ _))   = True 
isDiamond  _                = False

isDown, isLabel :: Form -> Bool 
isDown (Down _ _ )       = True
isDown (Neg (Down _ _ )) = True
isDown _                 = False 
isLabel (At _ _)         = True
isLabel (Neg (At _ _))   = True
isLabel _                = False 

isTrue,isFalse,isPlit, isNlit :: Form -> Bool
isTrue Top              = True
isTrue _                = False
isFalse Bot             = True
isFalse _               = False
isPlit (Prop _)         = True 
isPlit _                = False
isNlit (Neg (Prop _))   = True 
isNlit _                = False 

isNom, isNgNom, isAcc, isDneg :: Form -> Bool
isNom (Nom _)                       = True 
isNom  _                            = False 
isNgNom (Neg (Nom _))               = True 
isNgNom _                           = False 
isAcc (Dia _ (Nom _))               = True
isAcc (Neg (Box _ (Neg (Nom _))))   = True
isAcc _                             = False
isDneg (Neg (Neg _))                = True
isDneg _                            = False

isInvRel :: Form -> Bool
isInvRel (Box _ _)         = False
isInvRel (Dia _ _)         = False
isInvRel (Neg (Box _ _)) = False
isInvRel (Neg (Dia _ _)) = False
isInvRel (IBox _ _)       = True
isInvRel (IDia _ _)       = True
isInvRel (Neg (IBox _ _)) = True
isInvRel (Neg (IDia _ _)) = True
isInvRel f                              = error $ "error isInvRel: " ++ show f

-- Function for converting a literal (a propositional atom or a negation
-- of a propositional atom) at a nominal n to a pair consisting of the
-- n and the name of the atom.

nf2np :: NomSymbol -> Form -> (NomSymbol,PropSymbol)
nf2np nom (Prop name)       = (nom,name)
nf2np nom (Neg (Prop name)) = (nom,name)
nf2np _ _                   = error "error nf2np"

-- Function for converting a nominal m or negated nominal !m, at a 
-- nominal n, to the pair (n,m). 

nf2nn :: NomSymbol -> Form -> (NomSymbol,NomSymbol)
nf2nn n (Nom m)       = (n,m)
nf2nn n (Neg (Nom m)) = (n,m) 
nf2nn _ _             = error "error nf2nn"

-- Function for getting the nominal out of a nominal formula, a negated 
-- nominal formula, or an access formula 

getNom :: Form -> NomSymbol 
getNom (Nom nom)                      = nom
getNom (Neg (Nom nom))                = nom
getNom (Dia _ (Nom nom))              = nom
getNom (Neg (Box _ (Neg (Nom nom))))  = nom
getNom _                              = error "error getNom"

-- Function for getting the relation and the target nominal out of a 
-- box or diamond formula: 

getRel :: Form -> Rel
getRel (Neg f)                           = getRel f
getRel (Dia (RelSymbol rel) _)           = rel
getRel (IDia (RelSymbol rel) _)        = rel
getRel (Box (RelSymbol rel) _)           = rel
getRel (IBox (RelSymbol rel) _)        = rel
getRel _                  = error "error getRel"

-- The components of a (non-literal) formula are given by: 

components :: Form -> [Form]
components (Conj fs)          = fs
components (Disj fs)          = fs 
components (Impl f1 f2)       = [Neg f1,f2]
components (Neg (Conj fs))    = map Neg fs 
components (Neg (Disj fs))    = map Neg fs 
components (Neg (Impl f1 f2)) = [f1,Neg f2]
components (Neg (Neg f))      = [f]
components (A f)              = [f]
components (Neg (A f))        = [Neg f]
components (E f)              = [f]
components (Neg (E f))        = [Neg f]
components (Box _ f)          = [f]
components (Neg (Box _ f))    = [Neg f]
components (Dia _ f)          = [f]
components (Neg (Dia _ f))    = [Neg f]
components (Down _ f)         = [f]
components (Neg (Down _ f))   = [Neg f]
components (At _ f)           = [f] 
components (Neg (At _ f))     = [Neg f]
components _                  = error "error components"

-- Located components of a (non-literal) formula: 

lcomponents :: NomSymbol -> Form -> [Form]
lcomponents nom f = [At nom f' | f' <- components f ]

-- For label formulas, the following function returns the label: 

getLabel :: Form -> NomSymbol
getLabel (At nom _)       = nom
getLabel (Neg (At nom _)) = nom
getLabel _                = error "error getLabel"

-- For binder formulas, the following function returns the binder: 

binder :: Form -> Int 
binder (Down (X x) _)       = x
binder (Neg (Down (X x) _)) = x
binder _                    = error "error binder"

-- Check a list of formulas for nominal contradiction. 

checkNom :: [Form] -> Bool
checkNom fs = null [ m | (At n (Neg (Nom m))) <- fs, m == n ]

-- Checking a node for closure, with closure indicated by return of [] 

check :: Node -> [Node]
check node =
  if checkNN (neqs node)
     && checkPN (pos node) (neg node)
     && checkNom (forms node)
  then [node] else []
  where checkNN           = all (\(m,n) -> m /= n)     
        checkPN poss negs = intersect poss negs == []

-- Sometimes we just have to check the final component of a node: 

checkNdNom :: Node -> [Node]
checkNdNom node = if checkNom (forms node) then [node] else []


{- Tableau Expansion -}

step :: Node -> Tableau

-- Applying an expansion step to a node N yields a tableau, i.e., a list 
-- of nodes. If the expansion step results in closure of N, we return 
-- []. Otherwise we return a non-empty list of open tableau nodes. 

-- If the function is called for a node N with an empty pending formula
-- list, there is nothing left to do, so we return [N].

step node | null (forms node) = check node

-- If the list of pending formulas starts with a Boolean constant, then 
-- remove it if it is the constant True, otherwise close the node: 

step node 
  | isTrue  f = [node{forms=fs}]
  | isFalse f = []

-- The list of pending formulas starts with a propositional literal:
-- check for closure; if the node does not close, then add the literal to
-- the appropriate list.

  | isPlit f = let 
                 ni   = nf2np nom f 
                 pos' = add ni (pos node)
               in 
    if ni `elem` neg node then [] 
    else [node{forms=fs, pos=pos'}]

  | isNlit  f = let 
                 ni   = nf2np nom f  
                 neg' = add ni (neg node)
                in 
    if ni `elem` pos node then [] 
    else [node{forms=fs, neg=neg'}]

-- The list of pending formulas starts with a nominal. In this case we
-- perform a substitution and check for closure. Note the following: 

-- * Applying a substitution to a list of access relations may result
--  in a _change_ in the access relations, and thus in a violation of 
--  a universal constraint, thus destroying the invariant that the universal
--  constraints hold for all nominals present at the node. To restore 
-- that invariant, we have to take care that the universal constraints 
-- get (re-)applied to the new nominal that fuses two old ones. 

-- * Applying a
-- substitution to a list of access relations may result in new access
-- relations, thus destroying the invariant that the box and converse box
-- constraints of the node have been applied for all access relations of
-- the node. To restore that invariant, we have to take care that all box
-- and converse box constraints get applied to the new access relations.

-- * Applying a substitution to a list of box constraints may result 
-- in new box constraints, thus destroying the invariant that the box
-- constraints of the node have been applied for all access relations of
-- the node. To restore that invariant, we have to apply all new box
-- constraints to all access relations of the node.

-- * Applying a substitution to a list of converse box constraints may result 
-- in new converse box constraints, thus destroying the invariant that
-- the converse box constraints of the node have been applied for all
-- access relations of the node. To restore that invariant, we have to
-- apply all new converse box constraints to all access relations of the
-- node.

  | isNom f =
    if getNom f == nom
     then [node{forms=fs}]
     else 
          let 
            k_        = getNom f 
            m         = min k_ nom
            n         = max k_ nom
            dom'      = nub $ appDomain (n,m) (dom node)
            neqs'     = nub $ appNNs (n,m) (neqs node)
            accs'     = nub $ appNRNs (n,m) (accs node)
            ufs'      = nub $ appFs (n,m) (ufs node)
            boxes'    = nub $ appNRFs (n,m) (boxes node)
            newboxes  = boxes' \\ boxes node
            cboxes'   = nub $ appNRFs (n,m) (cboxes node)
            newcboxes = cboxes' \\ cboxes node
            pos'      = nub $ appNPs (n,m) (pos node)
            neg'      = nub $ appNPs (n,m) (neg node)
            forms'    = nub $ appFs  (n,m) (forms node)
            newaccs   = accs' \\ accs node
            us        = [ At m g | g <- ufs'          ]
            bs1       = [ At l g | (k,r,l)   <- newaccs, 
                                   (k',r',g) <- boxes',
                                   k == k', r == r'   ]
            bs2       = [ At l g | (k,r,l)   <- accs',
                                   (k',r',g) <- newboxes,
                                   k == k', r == r'   ]
            cs1       = [ At k g | (k,r,l)   <- newaccs, 
                                   (l',r',g) <- cboxes',
                                    l == l', r == r'   ]
            cs2       = [ At k g | (k,r,l)   <- accs', 
                                   (l',r',g) <- newcboxes,
                                    l == l', r == r'   ]
            newforms  = nub $ forms' ++ us ++ bs1 ++ bs2 ++ cs1 ++ cs2
         in
     check node{dom = dom',
                neqs = neqs',
                accs = accs',
                ufs = ufs',
                boxes = boxes',
                cboxes = cboxes',
                pos = pos',
                neg = neg',
                forms = newforms}

-- The list of pending formulas starts with a negated nominal: check for
-- closure. If the node does not close, add a new inequality (m != n)
-- to the inequality list of the node.

  | isNgNom f =
      if getNom f == nom
       then []
       else 
          let 
            k = getNom f
            m = min k nom
            n = max k nom
            neqs' = add (m,n) (neqs node)
          in
         [node{neqs = neqs', forms = fs}]

-- The list of pending formulas starts with an access formula

  | isAcc f && not (isInvRel f)
      =
          let 
            (r,n) = (getRel f, getNom f)
            accs' = add (nom,r,n) (accs node)
            dom'  = add n (dom node)
            fs'   = if (nom,r,n) `elem` accs node -- check is the access relation is already in the node
                     then fs 
                     else nub $ fs ++ us ++ bs ++ cs
            us    = [ At n g   | g <- ufs node           ] -- add universal constraints 
            bs    = [ At n g   | (m,s,g) <- boxes node,
                                  m == nom, s == r       ] -- add box constaints
            cs    = [ At nom g | (m,s,g) <- cboxes node,
                                  m == n, s == r         ] -- add inverse box constraints
          in 
    checkNdNom node{dom = dom',
                    accs = accs',
                    forms = fs'
                   }

  | isAcc f && isInvRel f
      =
           let 
             (r,n) = (getRel f, getNom f)
             accs' = add (n,r,nom) (accs node)
             dom'  = add n (dom node)
             fs'   = if (n,r,nom) `elem` accs node
                      then fs
                      else nub $ fs ++ us ++ bs ++ cs
             us    = [ At n g     | g <- ufs node            ]
             bs    = [ At nom g   | (m,s,g) <- boxes node,
                                     m == n, s == r          ]
             cs    = [ At n g     | (m,s,g) <- cboxes node,
                                     m == nom, s == r        ]
           in 
    checkNdNom node{dom = dom',
                    accs = accs',
                    forms = fs'
                   }

-- The list of pending formulas starts with a double negation: apply the 
-- double negation rule. 

  | isDneg  f 
            =  let 
                [g] = lcomponents nom f
                fs' = add g fs
               in
              [node{forms=fs'}]

-- The list of pending formulas starts with an alpha formula: 
-- add the components alpha_i to the node. 

  | isAlpha f = 
              let 
                fs' = nub $ lcomponents nom f ++ fs
              in 
    [node{forms=fs'}]
   
-- The list of pending formulas starts with a beta formula: 
-- split the node and add a component beta_i to each new branch. 

  | isBeta  f = [ node{forms=(f':fs)} | f' <- lcomponents nom f ]

-- The list of pending formulas starts with an A formula (@ k phi).
-- Add { @ m phi' | m in D } where D is 
-- the domain of the node, to the list of pending formulas, and store 
-- phi' as a universal constraint. 

  | isA   f = let 
                newfs  = [ At n g | n <- dom node,
                                    g <- components f ]
                fs'    = nub $ fs ++ newfs
                [f']   = components f
                ufs'   = nub (f':ufs node)
              in
    checkNdNom node{ufs = ufs',
                    forms = fs'}

-- The list of pending formulas starts with an E formula (@ k phi).
-- Take a fresh nominal n, add it to the domain of the node, 
-- add (@ n phi') and { @ n psi | psi in U } to the list 
-- of pending formulas.

  | isE   f = let 
                n      = N (idx node)
                dom'   = add n (dom node)
                ls     = lcomponents n f
                us     = [ At n g | g <- ufs node ]
                fs'    = nub $ fs ++ ls ++ us
              in
    [node{idx=(succ $ idx node), dom=dom', forms=fs'}]

-- The list of pending formulas starts with a [i] formula (@k phi).
-- Add the list [@ m phi' | k<i>m in A ], 
-- where A is the list of access formulas of the node, to the list of
-- pending formulas, and store the [i] formula as a box
-- constraint. Actually, for convenience, we store (k,i,phi').

  | isBox   f  && not (isInvRel f)
        = let
                r      = getRel f
                newfs  = [ At n g | (m,s,n) <- accs node,
                                     g      <- components f,
                                     m == nom, s == r           ]
                fs'    = nub $ fs ++ newfs
                boxes' = nub $
                          [(nom,r,g) | g <- components f] ++ boxes node
              in
    checkNdNom node{boxes=boxes',forms=fs'}

-- The list of pending formulas starts with a [-i] formula 
-- (@k phi). Add the list [@ m phi' | m<i>k in A]
-- where A is the list of access formulas of the node, to the list of
-- pending formulas, and store the [-i] formula as a converse box
-- constraint.  Actually, for convenience we store (k,i,phi').

  | isBox  f && isInvRel f
      = let
                r       = getRel f
                newfs   = [ At n g | (n,s,m) <- accs node,
                                      g      <- components f, 
                                      m == nom, s == r           ]
                fs'     = nub $ fs ++ newfs
                cboxes' = nub $
                           [(nom,r,g) | g <- components f] ++ cboxes node
              in
    checkNdNom node{cboxes=cboxes', forms=fs'}

-- The list of pending formulas starts with a diamond formula: use the
-- node index i to generate a fresh nominal constant n_i, increment
-- the node index, add (k<j>n_i) to the access list of the node, and put
-- (@ n_i phi'), where phi' is the component of the diamond
-- formula, on the list of pending formulas.  Also, generate appropriate
-- formulas for n_i from the universal constraints and from the 
-- box constraints on k, and append them to the list of pending formulas.

  | isDiamond f && not (isInvRel f)
      =
             let 
               n     = N (idx node)
               idx'  = succ $ idx node
               r     = getRel f
               accs' = (nom,r,n):(accs node)
               dom'  = add n (dom node)
               ls    = lcomponents n f
               us    = [ At n g   | g <- ufs node  ]
               bs    = [ At n g | (m,s,g) <- boxes node,
                                   m == nom, s == r  ]
               fs'   = nub $ fs ++ ls ++ us ++ bs
             in
    [node{idx=idx', dom=dom', accs=accs', forms=fs'}]

-- The list of pending formulas starts with a inverse diamond
-- formula: use the node index i to generate a fresh nominal constant
-- n_i, increment the node index, add (n_i<j>k) to the access list of
-- the node, generate the appropriate formulas for n_i from the converse
-- box constraints of the node, and append them, together with the
-- component of the <-> formula, to the list of pending formulas.

  | isDiamond f && isInvRel f
      =
             let 
               n      = N (idx node)
               idx'   = succ $ idx node
               r      = getRel f
               accs'  = (n,r,nom):(accs node)
               dom'   = add n (dom node)
               ls     = lcomponents n f
               us     = [ At n g | g <- ufs node     ]
               cs     = [ At n g | (m,s,g) <- cboxes node,
                                    m == nom, s == r  ]
               fs'    = nub $ fs ++ ls ++ us ++ cs
              in
    [node{idx = idx', dom=dom', accs=accs', forms=fs'}]

-- The list of pending formulas starts with an @ formula (@k @n phi)
-- (or (@ k - @ n phi)): add (@ n phi) (or (@ n - phi)) to the
-- list of pending formulas.

  | isLabel f
            = let 
                fs'  = add f' fs
                n    = getLabel f
                [f'] = lcomponents n f
              in
    [node{forms=fs'}] 

-- The list of pending formulas starts with a down-arrow formula: add
-- its component to the list of pending formulas, after the appropriate
-- substitution.

  | isDown  f
            = let 
                x   = binder f
                [g] = components f
                f'  = At nom (appF (X x,nom) g)
                fs' = add f' fs 
              in 
    [node{forms=fs'}]
 where (At nom f:fs) = forms node

step nd = error $ "error step: " ++ show nd
  
-- These are all the possible cases, so this ends the treatment of 
-- a single tableau expansion step. 

-- A tableau node is fully expanded (complete) if its list of pending
-- formulas is empty.

complete :: Node -> Bool 
complete node | null $ forms node = True
complete  _                       = False

-- In general, we are not interested in generating all models for 
-- a satisfiable formula: one model is enough. This allows for 
-- a considerable reduction.

data OpenFlag = OPEN [Node] | CLOSED

expand :: Bool -> Tableau -> IO OpenFlag
expand verbose []   = do when verbose $ putStrLn "Closed"
                         return CLOSED
expand verbose (node:nodes) =
 do when verbose $ putStrLn (show node)
    if complete node
     then return $ OPEN [node]
     else do let newnodes = step node
             expand verbose (nodes ++ newnodes)

{- Cautious Tableau Expansion -}

-- Tableau expansion according to the `trial and error' versions of the
-- E, Diamond and Cdia rules is useful for finding minimal
-- models. In cautious tableau expansion we reuse existing nominals, and
-- we should check carefully whether this disturbs our constraints
-- invariant. The following functions take care of this:

noAccTo, noAccFrom :: [(NomSymbol,Rel,NomSymbol)] -> NomSymbol -> Rel -> Bool
noAccTo   accs_ m r = null [ (k,r,m) | (k,r',m') <- accs_, r==r', m==m' ]
noAccFrom accs_ m r = null [ (m,r,k) | (m',r',k) <- accs_, r==r', m==m' ]

-- Thus, if (noAccTo accs m r) is true at a node, where accs
-- is the list of access arrows of the node, this means that there 
-- is no arrow (x <r> m) at the
-- node. This means in turn that adding a new r arrow that
-- points to m may disturb the box constraint invariant. Similarly, 
-- truth of (noAccFrom accs m r) at a node, accs
-- is the list of access arrows of the node, indicates that the addition 
-- of a new r-relation arrow that departs from m may violate 
-- the converse box constraint invariant of the node. 
-- 
-- We are ready now to replace the step function by the following
-- alternative:

cautiousStep :: Node -> Tableau

-- Cautious step are like ordinary steps, except for the cases where
-- the formula to be decomposed is a E, Diamond and Cdia formula.
-- 
-- If the function is called for a node  N with an empty pending formula
-- list, again, there is nothing left to do, and we return [N].
 
cautiousStep node
  | null $ forms node = [node]

-- If the list of pending formulas starts with an E formula, we branch
-- to all the possible ways of letting the existential obligation be
-- fulfilled by an existing nominal, and append the result of doing the
-- extension step that introduces a fresh nominal. Note that no accessibilities 
-- are added, so no box or converse box constraints can be violated. Also, 
-- no nominals are added, so no universal constraints can be violated. 
  | isE   f = 
    [ node{forms = nub (lcomponents n f ++ fs)} | n <- dom node]
    ++ step node

-- If the list of pending formulas starts with a Diamond or Cdia formula, 
-- we branch to all the ways of letting an existing nominal discharge
-- the existential obligation, and append the result of the
-- expansion step that introduces a fresh nominal. Now we have to 
-- take measures to ensure that the invariant for the box constraints 
-- gets restored, if necessary. 

  | isDiamond f && not (isInvRel f)
     =
    let r = getRel f in 
    [ node{accs = add (nom,r,n) (accs node),
           forms= nub (lcomponents n f ++ fs ++ [ At n g | (m,s,g) <- boxes node,  m == nom, s == r,  noAccTo (accs node) n r ])
          }     | n <- dom node ]
     ++ step node

  | isDiamond f && isInvRel f
     =
    let r = getRel f in 
    [ node{accs = add (n,r,nom) (accs node),
           forms= nub (lcomponents n f ++ fs ++ [ At n g | (m,s,g) <- cboxes node, m == nom, s == r,noAccFrom (accs node) n r ])
          }     | n  <- dom node]
     ++ step node

  | otherwise = step node
 where (At nom f:fs) = forms node


-- Cautious expansion of a tableau:
cautiousExpand :: Bool -> Tableau -> IO OpenFlag
cautiousExpand verbose []   = do when verbose $ putStrLn "Closed"
                                 return CLOSED
cautiousExpand verbose (node:nodes) =
 do when verbose $ putStrLn (show node)
    if complete node
     then return $ OPEN [node]
     else do let newnodes = cautiousStep node
             cautiousExpand verbose (nodes ++ newnodes)

{- Model Generation -}

extract :: Node -> String 
extract node =
 unwords $
  show (reverse (dom node)) 
   :  [ show n ++ show i ++ show m | (n,i,m) <- reverse (accs node)]
   ++ [ show i ++ ":"    ++ show p | (i,p)   <- reverse (pos node) ]
   ++ [ show i ++ ":-"   ++ show p | (i,p)   <- reverse (neg node) ]

{- Frame Properties -}

-- Here is a list of pure formulas (formulas without proposition letters) 
-- that define frame properties. In fact, any pure formula defines 
-- a frame condition, and characterizes a class of frames. 

trans, k4, intrans, refl, kt, irrefl, symm     :: Form
kb, asymm, s4, kt4, s5, serial, kd, euclid, k5 :: Form
kdb, kd4, kd5, k45, kd45, kb4, ktb, antisymm   :: Form
trans     = parse "begin down x1 . [][]<->x1 end"
k4        = trans
intrans   = parse "begin down x1 . [][][-]-x1 end"
refl      = parse "begin down x1 . <>x1 end"
kt        = refl
irrefl    = parse "begin down x1 . []-x1 end"
symm      = parse "begin down x1 . []<>x1 end"
kb        = symm
asymm     = parse "begin down x1 . [][]-x1 end"
s4        = parse "begin down x1 . (<>x1 & [][] <->x1) end"
kt4       = s4
s5        = parse "begin down x1 . ((<>x1) & ([]<>x1) & ([][]<->x1)) end"
serial    = parse "begin <>true end"
kd        = serial
euclid    = parse "begin down x1 . [] down x2 . @ x1 []<>x2 end"
k5        = euclid 
kdb       = parse "begin (<>true & down x1 . []<->x1) end"
kd4       = parse "begin (<>true & down x1 . [][]<->x1) end"
kd5       = parse "begin (<>true & down x1 . [] down x2 . @ x1 []<>x2) end"
k45       = parse "begin down x1 . x1([][]<->1 & [] down x2 . @ x1 []<>x2) end"
kd45      = parse "begin down x1 . ((<>true) & ([][]<->x1) & ([] down x2 . @ x1 []<>x2)) end"
kb4       = parse "begin down x1 . ([]<>x1 & [][] <->x1) end"
ktb       = parse "begin down x1 . (<>x1 & []<>x1) end"
antisymm  = parse "begin down x1 . [] down x2 . [] (x1 -> x2) end"

add :: (Eq a) => a -> [a] -> [a]
add x xs = if x `elem` xs then xs else x:xs