{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-|
Module      : Translation
Description : Defines the translation \(\tau\) of a \(\mathcal{L}_{\square K}\) formula into a \(\mathcal{L}_{FO}\) formula
-}
module Translation (tau, tauSP)  where

import Data.List (delete) 
import Logics

tauSP :: ModalFormula -> Formula a -> ModalFormula
tauSP phi (Atom p)                    = phi ∧ Atom p
tauSP phi (Neg alpha)                 = Neg (tauSP phi alpha)
tauSP phi (Conj as)                   = Conj [tauSP phi a | a <- as]
tauSP phi (Disj as)                   = Disj [tauSP phi a | a <- as]
tauSP phi (Imp alpha1 alpha2)         = tauSP phi alpha1 ⇒ tauSP phi alpha2
tauSP phi (Equiv alpha1 alpha2)       = tauSP phi alpha1 ⇔ tauSP phi alpha2
tauSP phi (K ag alpha)                = mkForAll (nonobs ag) (phi ⇒ tauSP phi alpha)

---------------------------------
-- | The translation function @tau@
-- takes the constraint formula in 'FOLFormula' and a
-- target formula in 'ModalFormula'
---------------------------------
tau :: ModalFormula -> Formula a -> ModalFormula
tau phi (Atom p)                    = Atom p
tau phi (Neg alpha)                 = Neg (tau phi alpha)
tau phi (Conj as)                   = Conj [tau phi a | a <- as]
tau phi (Disj as)                   = Disj [tau phi a | a <- as]
tau phi (Imp alpha1 alpha2)         = tau phi alpha1 ⇒ tau phi alpha2
tau phi (Equiv alpha1 alpha2)       = (tau phi (alpha1 ⇒ alpha2)) ∧ (tau phi (alpha2 ⇒ alpha1))
tau phi (K ag alpha)                = mkForAll (nonobs ag) (phi ⇒ tau phi alpha)
tau phi (Box (Nondet ps) alpha)    = Conj [tau phi (Box p alpha) | p <- ps]
tau phi (BSub xs es (BSub xs' es' alpha))   = BSub (xs++xs') (es++es') alpha

tau phi (BSub xs es (Neg alpha))      = Neg (tau phi (BSub xs es alpha))
tau phi (BSub xs es (Conj as))        = Conj [tau phi (BSub xs es a)|a <- as]
tau phi (BSub xs es (Disj as))        = Disj [tau phi (BSub xs es a)|a <- as]
tau phi (BSub xs es (Imp f g))        = tau phi (BSub xs es f) ⇒  tau phi (BSub xs es g)
tau phi (BSub xs es (Equiv f g))      = tau phi (BSub xs es f) ⇔  tau phi (BSub xs es g)


tau phi (Box (BAssign x e) alpha)     = forAllB (\k -> tau (phi ∧ Atom (BEq (BValue k) e)) (Atom (BEq (BValue k) e) ⇒ sub x (BValue k) alpha))
tau phi (Box (Test beta) alpha)       = phi ⇒ tau (phi ∧ beta) alpha
tau phi (Box (Sequence [p]) alpha)    = tau phi (Box p alpha)
tau phi (Box (Sequence (p:ps)) alpha) = tau phi (Box p (Box (Sequence ps) alpha))
tau phi (Box (Nondet ps) alpha)       = Conj [tau phi (Box p alpha) | p <- ps ]

tau phi (ForAllB n alpha)             = ForAllB n (tau phi alpha)  
tau phi (ExistsB n alpha)             = ExistsB n (tau phi alpha)  

-- | 'mkForAll' writes 'Forall' for a vector (list) of variables.
-- Note that 'mkForAll' uses 'existsB', which is still another constructor for 'Forall',
-- 'forAllB' takes care of variable name binding
---------------------------------------------
--  it accepts a list of variables (of any type) 
mkForAll :: [Var] -> ModalFormula -> ModalFormula
mkForAll [] f          = f
mkForAll [BVar x] f    = forAllB (\z -> sub (BVar x) (BValue z) f)
mkForAll (BVar x:xs) f = mkForAll xs (forAllB (\z -> sub (BVar x) (BValue z) f))

-- | 'mkForExists' writes 'Exists' for a vector (list) of variables.
-- Note that 'mkForExists' uses 'existsB', which is still another constructor for 'Exists',
-- 'existsB' takes care of variable name binding
---------------------------------------------
mkExists :: [Var] -> ModalFormula -> ModalFormula
mkExists [] f          = f
mkExists [BVar x] f    = existsB (\z -> sub (BVar x) (BValue z) f)
mkExists (BVar x:xs) f = existsB (\z -> sub (BVar x) (BValue z) (mkExists xs f))