module HTab.Formula

(Nom, Prop, Rel, Prefix, Formula(..), Literal(..), Atom(..),
DependencySet, Dependency, Depth,
dsUnion, dsUnions, dsInsert, dsMember,
dsEmpty, dsMin, dsShow, addDeps,
PrFormula(..),showLess,
LanguageInfo(..), neg,
conj, disj, taut,
prop, nom, prefix, negPr,
replaceVar,
firstPrefixedFormula,
parse, simpleParse, Theory, RelInfo, Task,
showRelInfo, negLit,
encodeValidityTest, encodeSatTest, encodeRetrieveTask,
HyLoFormula, RelProperty(..),
isPositiveNom, isPositiveProp, isProp
,parseGenerators,Generator,applyGenerators
)

 where
import Debug.Trace
import qualified Data.Set as Set
import Data.Set ( Set )
import qualified Data.Map as Map
import Data.Map ( Map )
import qualified Data.IntSet as IntSet
import Data.List ( delete, nub, intercalate, isPrefixOf )

import Data.Char ( toUpper )

import qualified HyLo.Signature.String as S

import HyLo.Signature( HasSignature(..), nomSymbols, relSymbols )

import qualified HyLo.InputFile as InputFile
import qualified HyLo.InputFile.Parser as P
import qualified HyLo.Formula as F
import HTab.CommandLine ( Params(..) )

type Prefix  = Int
type Rel     = String
type Nom     = String
type Prop    = String
data Atom    = Taut | N String | P String deriving(Eq, Ord)
data Literal = PosLit Atom | NegLit Atom deriving(Eq, Ord)

negLit :: Literal -> Literal
negLit (PosLit a) = NegLit a
negLit (NegLit a) = PosLit a

isPositiveNom, isPositiveProp, isProp :: Literal -> Bool
isPositiveNom (PosLit (N _))  = True
isPositiveNom _               = False
isPositiveProp (PosLit (P _)) = True
isPositiveProp _              = False
isProp (PosLit (P _))         = True
isProp (NegLit (P _))         = True
isProp _                      = False 

instance Show Atom where
 show (Taut) = "T"
 show (N n)  = n
 show (P p)  = p

instance Show Literal where
 show (PosLit a) = show a
 show (NegLit a) =  '!' : show a

data Formula
     = Lit    Literal
     | Con   (Set Formula)
     | Dis   (Set Formula)
     | At     Nom Formula
     | Down   Nom Formula
     | Box    Rel     Formula
     | Dia    Rel     Formula
     | A      Formula
     | E      Formula
  deriving (Eq, Ord)

instance Show Formula where
 show (Lit a)    = show a
 show (Con fs)   = "^" ++ show (list fs)
 show (Dis fs)   = "v" ++ show (list fs)
 show (At n f)   =  n  ++ ":(" ++ show f ++ ")"
 show (Box r f)  = "[" ++ r ++ "]"   ++ show f
 show (Dia r f)  = "<" ++ r ++ ">"   ++ show f
 show (A f)      = "A" ++ show f
 show (E f)      = "E" ++ show f
 show (Down n f) = "down " ++ n ++ "." ++ show f

-- parsing of the input file

type Theory  = Formula
type Task    = P.InferenceTask
type PRelInfo = [P.RelInfo]

type RelInfo = Map String [RelProperty]
data RelProperty   =   Reflexive
                     | Transitive
                     | Universal
                     --
                     | SubsetOf [Rel]
                     deriving (Eq, Show, Ord)

showRelInfo :: RelInfo -> String
showRelInfo = Map.foldrWithKey (\r v -> (++ " " ++ show r ++ " -> " ++ show v )) ""

parse :: Params -> String -> (Theory,RelInfo,LanguageInfo,[Task])
parse p s
  = (theory, relInfo, fLang, tasks)
    where parseOutput = InputFile.myparse s       -- direct parse from hylolib
          pRelInfo    = P.relations parseOutput
          relInfo     = forceProperties p parseOutput $ convertToOurType pRelInfo
          theory      = convert relInfo $ P.theory parseOutput
          tasks       = P.tasks parseOutput
          fLang       = langInfo parseOutput

-- add properties specified by the --all-PROP parameters
-- in order to work in case of automatic signature

forceProperties :: Params -> P.ParseOutput -> RelInfo -> RelInfo
forceProperties p po relI
 = foldr addToAll relI (list rels)
   where
         rels = Set.map (\(S.RelSymbol r) -> up r) $ Set.unions $ map (relSymbols . getSignature) theory
         addToAll r = Map.insertWith (\c1 c2 -> nub $ c1 ++ c2) r conds
         conds = map snd $
                   filter fst   [(allTransitive p, Transitive),
                                 (allReflexive  p, Reflexive )]
         theory =  P.theory po


convertToOurType :: PRelInfo -> RelInfo
 -- and add for each relation in the formula, the relevant key
convertToOurType prelI = foldr insertRelProp Map.empty (concatMap convertOne prelI)
 where insertRelProp (rs,pr) = Map.insertWith (++) rs [pr]
       convertOne (r,props)  = concatMap (c r) props
       c r P.Reflexive       = [(up r,Reflexive    )]
       c _ P.Symmetric       = error "Symmetric not handled"
       c r P.Transitive      = [(up r,Transitive   )]
       c r P.Universal       = [(up r,Universal    )]
       c _ (P.InverseOf _)   = error "InverseOf not handled" 
       c r (P.SubsetOf ss)   = [(up r,SubsetOf [ up s | s <- ss])]
       c r (P.Equals ss)     = [(up r,SubsetOf [ up s | s <- ss])]
                               ++ [(up s,SubsetOf [up r]) | s <- ss]
       c _ (P.TClosureOf _)  = error "TClosureOf not handled"
       c _ (P.TRClosureOf _) = error "TRClosureOf not handled"
       c _ P.Functional      = error "Functional not handled"
       c _ P.Injective       = error "Injective not handled"
       c _ P.Difference      = error "Difference not handled"

simpleParse :: Params -> String -> (Theory,RelInfo,LanguageInfo)
simpleParse p s =
 let (t,r,i,_) = parse p $ "signature { automatic } theory { " ++ removeBeginEnd s ++ "}"
 in (t,r,i)
 where removeBeginEnd = unwords . delete "begin" . delete "end" . words

convert :: RelInfo -> [F.Formula S.NomSymbol S.PropSymbol S.RelSymbol]
             -> Formula
convert relI = conv_ relI . foldr (F.:&:) F.Top

conv_ :: RelInfo -> F.Formula S.NomSymbol S.PropSymbol S.RelSymbol
           -> Formula
conv_  _   F.Top               = taut
conv_  _   F.Bot               = neg taut
conv_  _   (F.Prop p)          = prop p
conv_  _   (F.Nom  n)          = nom n
conv_ relI (F.Neg  f)          = neg $ conv_ relI f
conv_ relI (f1 F.:&:    f2)    = conv_ relI f1 `conj` conv_ relI f2
conv_ relI (f1 F.:|:    f2)    = conv_ relI f1 `disj` conv_ relI f2
conv_ relI (f1 F.:-->:  f2)    = conv_ relI f1 `imp`  conv_ relI f2
conv_ relI (f1 F.:<-->: f2)    = conv_ relI f1 `dimp` conv_ relI f2
conv_ relI (F.Diam (S.RelSymbol r) f)        = specialiseDia (up r) relI (conv_ relI f)
conv_ relI (F.Box  (S.RelSymbol r) f)        = specialiseBox (up r) relI (conv_ relI f)
conv_ relI (F.At   n f)        = at        n (conv_ relI f)
conv_ relI (F.Down v f)        = downArrow v (conv_ relI f)
conv_ relI (F.A f)             = univMod     (conv_ relI f)
conv_ relI (F.E f)             = existMod    (conv_ relI f)
conv_ _    f                 = error (show f ++ "not supported")

type Connector = Formula -> Formula

specialiseDia :: String -> RelInfo -> Connector
specialiseDia r relI = specialise r relI (diamond, existMod)

specialiseBox :: String -> RelInfo -> Connector
specialiseBox r relI = specialise r relI (box, univMod)

specialise :: String -> RelInfo -> (String -> Connector, Connector)
                -> Connector
specialise r relI (relational, global)
 | Universal `elem` props  = global
 | otherwise = relational r
 where props = Map.findWithDefault [] r relI

type HyLoFormula = F.Formula S.NomSymbol S.PropSymbol S.RelSymbol

encodeValidityTest :: RelInfo -> Formula -> [HyLoFormula] -> Formula
encodeValidityTest relI th fs
 = neg $ conj th (convert relI fs)

encodeSatTest :: RelInfo -> Formula -> [HyLoFormula] -> Formula
encodeSatTest relI th fs
 = conj th (convert relI fs)

encodeRetrieveTask :: RelInfo -> LanguageInfo -> Formula -> [HyLoFormula]
                        -> ([String],[Formula])
encodeRetrieveTask relI fLang theory fs
 = (noms , map (\n -> conj theory (At n (neg $ convert relI fs))) noms)
   where noms = languageNoms fLang

-- CONSTRUCTORS

{- Atoms -}
taut :: Formula
nom  :: S.NomSymbol -> Formula
prop :: S.PropSymbol -> Formula

taut                  = Lit $ PosLit Taut
nom  (S.NomSymbol n)  = Lit $ PosLit $ N $ up n
prop (S.PropSymbol p) = Lit $ PosLit $ P $ up p

{- Modalities -}
box, diamond :: String -> Formula -> Formula
univMod, existMod :: Formula -> Formula
box        r    = Box   r
diamond    r    = Dia   r
univMod    = A
existMod   = E

{- binder -}
downArrow :: S.NomSymbol -> Formula -> Formula
downArrow (S.NomSymbol n) = Down (up n)

{- Hybrid operators -}
at :: S.NomSymbol -> Formula -> Formula
at (S.NomSymbol n) = At (up n)

{- Conjunction and disjunction -}

conj, disj :: Formula -> Formula -> Formula

conj    (Con xs) (Con ys) = Con (Set.union xs ys)
conj     f     c@(Con  _) = conj c f
conj c@(Con xs)   f
    | isTrue f            = c
    | isFalse f           = neg taut
    | otherwise           = Con (Set.insert f xs)
conj     f        f'
    | isTrue f            = f'
    | isFalse f           = neg taut
    | isTrue f'           = f
    | isFalse f'          = neg taut
    | otherwise           = skipSingleton Con (set [f,f'])

disj   (Dis xs)   (Dis ys) = Dis (Set.union xs ys)
disj    f       c@(Dis  _) = disj c f
disj c@(Dis xs)    f
    | isTrue f             = taut
    | isFalse f            = c
    | otherwise            = Dis (Set.insert f xs)
disj    f          f'
    | isTrue f             = taut
    | isFalse f            = f'
    | isTrue f'            = taut
    | isFalse f'           = f
    | otherwise            = skipSingleton Dis (set [f,f'])

dimp :: Formula -> Formula -> Formula
dimp f1 f2 = (neg f1 `disj` f2) `conj` (f1 `disj` neg f2)
-- this form is preferred so as to enhance lazy branching

-- TODO
-- ala Spartacus:
-- when there is no literal in the double implication,
-- use the following form:
--dimp f1 f2 = (f1 `conj` f2) `disj` (neg f1 `conj` neg f2)

imp :: Formula -> Formula -> Formula
imp f1 f2 = neg f1 `disj` f2

skipSingleton :: (Set Formula -> Formula) -> Set Formula -> Formula
skipSingleton c xs
 | Set.size xs == 1 = Set.findMin xs
 | otherwise       = c xs

isTrue, isFalse :: Formula -> Bool
isTrue  (Lit (PosLit Taut)) = True
isTrue   _                  = False
isFalse (Lit (NegLit Taut)) = True
isFalse  _                  = False

-- invariant : neg is only called on literals during
-- the run of the algorithm
neg :: Formula -> Formula
neg (Con l)          = Dis (Set.map neg l)
neg (Dis l)          = Con (Set.map neg l)
neg (At n f)         = At   n (neg f)
neg (Down v f)       = Down v (neg f)
neg (Box r f)        = Dia  r (neg f)
neg (Dia r f)        = Box  r (neg f)
neg (A f)            = E (neg f)
neg (E f)            = A (neg f)
neg (Lit (PosLit a)) = Lit (NegLit a)
neg (Lit (NegLit a)) = Lit (PosLit a)


-- prefixed formula

type Depth = Int -- modal depth of current formula wrt input formula

data PrFormula = PrFormula Prefix DependencySet Depth Formula
 deriving Eq

instance Show PrFormula where
 show (PrFormula pr ds md f) = show pr ++ ":" ++ dsShow ds ++ ":" ++ show md ++ ":" ++ show f

showLess :: PrFormula -> String
showLess (PrFormula pr _ md f) = show pr ++ ":" ++ show (md,f)

prefix :: Prefix -> DependencySet -> Depth -> Set Formula -> [PrFormula]
prefix p bps md fs = [PrFormula p bps md formula|formula <- list fs]

firstPrefixedFormula :: Formula -> PrFormula
firstPrefixedFormula = PrFormula 0 dsEmpty 0

negPr :: PrFormula -> PrFormula
negPr (PrFormula p ds md f) = PrFormula p ds md (neg f)

-- formula language

data LanguageInfo = LanguageInfo { languageNoms :: [String] } -- ascending

instance Show LanguageInfo where
 show li = "Input Language:\n|" ++ yesnol "Noms " ( languageNoms li )
  where yesnol s l | null l = "no " ++ s
        yesnol s l = s ++ intercalate ", " l

langInfo :: P.ParseOutput -> LanguageInfo
langInfo po
 = LanguageInfo { languageNoms = noms }
    where noms = nub $ map (\(S.NomSymbol n) -> up n) $ concatMap (list . nomSymbols . getSignature) theory
          theory =  P.theory po

-- composeXX functions follow the idea from
-- "A pattern for almost compositional functions", Bringert and Ranta.
composeMap :: (Formula -> Formula)
           -> (Formula -> Formula)
           -> (Formula -> Formula)
composeMap baseCase g e = case e of
    Con fs     -> Con $ Set.map g fs
    Dis fs     -> Dis $ Set.map g fs
    Dia r f  -> Dia r (g f)
    Box r f    -> Box r (g f)
    At   i f   -> At  i (g f)
    A f        -> A (g f)
    E f        -> E (g f)
    Down x f   -> Down x (g f)
    f          -> baseCase f

replaceVar :: String -> String -> Formula -> Formula
replaceVar v n a@(Lit (PosLit (N v2))) = if v == v2 then Lit (PosLit (N n)) else a
replaceVar v n a@(Lit (NegLit (N v2))) = if v == v2 then Lit (NegLit (N n)) else a
replaceVar v n a@(Down v2 f) = if v == v2 then a   -- variable capture
                                          else Down v2 (replaceVar v n f)
replaceVar v n (At v2 f)   = if v == v2 then At n (replaceVar v n f)
                                        else At v2 (replaceVar v n f)
replaceVar v n f = composeMap id (replaceVar v n) f

-- backjumping

type Dependency = Int
type DependencySet = IntSet.IntSet

instance Ord PrFormula where
 compare (PrFormula pr1 ds1 _ f1) (PrFormula pr2 ds2 _ f2) =
  case dsMin ds1 `compare` dsMin ds2 of
   LT -> LT
   GT -> GT
   EQ -> compare (pr1,f1) (pr2,f2)

dsUnion :: DependencySet -> DependencySet -> DependencySet
dsUnion = IntSet.union

dsUnions :: [DependencySet] -> DependencySet
dsUnions = IntSet.unions

dsInsert :: Dependency -> DependencySet -> DependencySet
dsInsert = IntSet.insert

dsMember :: Dependency -> DependencySet -> Bool
dsMember = IntSet.member

dsEmpty :: DependencySet
dsEmpty = IntSet.empty

dsMin :: DependencySet -> Int
dsMin ds = maybe 0 fst $ IntSet.minView ds

dsShow :: DependencySet -> String
dsShow = show . IntSet.toList

addDeps :: DependencySet -> PrFormula -> PrFormula
addDeps ds1 (PrFormula p ds2 md f) = PrFormula p (dsUnion ds1 ds2) md f

list :: Ord a => Set.Set a -> [a]
list = Set.toList

set :: Ord a => [a] -> Set.Set a
set = Set.fromList

-- symmetries
-- substitution of literals inside of formulas

type Generator = [(Depth,Literal,Literal)]

applyGenerators :: [Generator] -> PrFormula -> [PrFormula]
applyGenerators gens f
 = if null res
    then res
    else trace ("SYM on " ++ showLess f ++ ":" ++ intercalate "," (map showLess res))
               res
   where res =  delete f $ nub $ map (\gen -> subst gen f) gens

subst :: Generator -> PrFormula -> PrFormula
subst gen (PrFormula pr ds md f) = PrFormula pr ds md $ substNorm (normGen gen md) f

normGen :: Generator -> Depth -> Generator
normGen g md = [(md1-md,a1,a2) | (md1,a1,a2) <- g, md1 - md >= 0]

substNorm :: Generator -> Formula -> Formula
-- act as if we were at modal depth 0 and generator has been adjusted
substNorm gen (Lit a)     = Lit $ genOnLit gen a
substNorm gen (At n f)    = At n $ substNorm (normGen gen 1) f
substNorm gen (Box r f)   = Box r $ substNorm (normGen gen 1) f
substNorm gen (Dia r f)   = Dia r $ substNorm (normGen gen 1) f
substNorm gen (Down n f)  = Down n $ substNorm (normGen gen 1) f
substNorm gen (A f)       = A $ substNorm (normGen gen 1) f
substNorm gen (E f)       = E $ substNorm (normGen gen 1) f
substNorm gen f           = composeMap id (substNorm gen) f

genOnLit :: Generator -> Literal -> Literal
genOnLit [] l           = l
genOnLit ((d,x,y):g) l
 | d == 0 && x == l        = y
 | d == 0 && x == negLit l = negLit y
 | d == 0 && y == l        = x
 | d == 0 && y == negLit l = negLit x
 | otherwise               = genOnLit g l

parseGenerators :: String -> [Generator]
parseGenerators genString
 =  [lineToGen l [] | l <- lines genString,
                        not ("%" `isPrefixOf` l),
                        not (null l)            ]

-- turn such a line into a generator:
-- 4 -2 5, 5 3 5, 0 -6 -3
lineToGen :: String -> Generator -> Generator
lineToGen "" g    = g
lineToGen (',':l) g = lineToGen l g
lineToGen l g       = let triple = takeWhile (/= ',') l
                          remainder = dropWhile (/= ',') l
                          [md,l1,l2] = map read $ words triple
                          -- we read X for PX or -Y for -PY,
                          -- now we need to convert it in atom
                          a1 = if l1 < 0
                                then NegLit $ P $ "P" ++ show (negate l1)
                                else PosLit $ P $ "P" ++ show l1
                          a2 = if l2 < 0
                                then NegLit $ P $ "P" ++ show (negate l2)
                                else PosLit $ P $ "P" ++ show l2
                      in lineToGen remainder (g ++ [(md,a1,a2)])

up :: String -> String
up = map toUpper