{-# LANGUAGE ExistentialQuantification #-}
{- |
Module      :  ./TopHybrid/StatAna.hs
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  nevrenato@gmail.com
Stability   :  experimental
Portability :  not portable

Description :
Static analysis of hybrid logic with an arbitrary logic below.
-}

module TopHybrid.StatAna (thAna, anaForm', simSen) where

import Logic.Logic
import TopHybrid.AS_TopHybrid
import TopHybrid.TopHybridSign
import TopHybrid.Print_AS ()
import TopHybrid.Utilities
import TopHybrid.ATC_TopHybrid ()
import CASL.Sign -- Symbols, this should be removed...
import Common.GlobalAnnotations
import Common.Result
import Common.ExtSign
import Common.AS_Annotation
import Common.Id
import Common.DocUtils
import Control.Monad
import Data.List
import Data.Set
import Unsafe.Coerce
import ATerm.Lib

bimap :: (t1 -> t2) -> (s1 -> s2) -> (t1, s1) -> (t2, s2)
bimap f g (a, b) = (f a, g b)

-- | Collects the newly declared nomies and modies
colnomsMods :: [TH_BASIC_ITEM] -> ([MODALITY], [NOMINAL])
colnomsMods = Data.List.foldr f ([], [])
        where f (Simple_mod_decl ms) = bimap (++ ms) id
              f (Simple_nom_decl ns) = bimap id (++ ns)

{- | Adds the newly declared nomies/modies, and the analysed base
signature to a new sig
checking for redundancy of modalities and nominals declarations
Note : If there are repeated declarations, the size of the sets should
be differnt that the size of the lists -}
topAna :: (Logic l sub bs sen si smi sign mor symb raw pf) =>
                [TH_BASIC_ITEM] -> l -> sign -> Result Sgn_Wrap
topAna ds l sig = if not rep then return newSig else mkHint newSig msg
                where
                x = colnomsMods ds
                x' = bimap fromList fromList x
                rep = size (uncurry Data.Set.union x') /=
                      length (uncurry (++) x)
                s = uncurry THybridSign x' sig
                newSig = Sgn_Wrap l s
                msg = maybeE 0 Nothing

{- Checks if the modalities and nominals referred in a sentence, really exist
in the signature -}
nomOrModCheck :: (Pretty f, GetRange f) => Set SIMPLE_ID -> SIMPLE_ID ->
                                           TH_FORMULA f -> Result (TH_FORMULA f)
nomOrModCheck xs x = if member x xs then return else mkError msg
     where msg = maybeE 1 Nothing


{- | Top Formula analyser
The l argument could be discarded, but then we would need an extra unsafe
function, to convert the spec type...
As l corresponds to the underlying logic bs should correspond to the
underlying spec, as some formula analysers need the spec associated
with it -}
anaForm :: (Logic l sub bs sen si smi sign mor symb raw pf) =>
        l -> bs -> Sgn_Wrap -> Frm_Wrap -> Result Frm_Wrap
anaForm l bs s (Frm_Wrap _ f) = liftM (Frm_Wrap l) $ unroll l bs s f

{- Static analysis of an hybridized sentence, when it's called by an upper
level logic. (This is only used when we want to analyse 2 or more times
hybridized, sentences). Probably this function can be merged smoothly with
the above. I will check this later

An hybridized sentence, with the correpondent sign already built, doesn't
need the top spec, hence we can discard it and just use the underlying (und) -}
anaForm' :: (Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap
anaForm' (Spc_Wrap l bs _, s, f) = anaForm l (und bs) s f

-- | Unrolling the formula, so that we can analyse it further
unroll :: (Show f, GetRange f, ShATermConvertible f,
             Logic l sub bs sen sy sm si mo sy' rs pf) =>
                l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l bs s'@(Sgn_Wrap _ s) f =
        case f of
                  (At n f') -> liftM (At n) $ unroll l bs s' f' >>=
                                 nomOrModCheck (nomies s) n
                  (Box m f') -> liftM (Box m) $ unroll l bs s' f' >>=
                                 nomOrModCheck (modies s) m
                  (Dia m f') -> liftM (Dia m) $ unroll l bs s' f' >>=
                                 nomOrModCheck (modies s) m
                  (Conjunction f' f'') -> liftM2 Conjunction
                                           (unroll l bs s' f')
                                           (unroll l bs s' f'')
                  (Disjunction f' f'') -> liftM2 Disjunction
                                           (unroll l bs s' f')
                                           (unroll l bs s' f'')
                  (Implication f' f'') -> liftM2 Implication
                                           (unroll l bs s' f')
                                           (unroll l bs s' f'')
                  (BiImplication f' f'') -> liftM2 BiImplication
                                             (unroll l bs s' f')
                                             (unroll l bs s' f'')
                  (Here n) -> nomOrModCheck (nomies s) n $ Here n
                  (Neg f') -> liftM Neg (unroll l bs s' f')
                  (Uni n f') -> (liftM $ Uni n) (unroll l bs
                   (addNomToSig n s') f') >>= checkForRepNom n (nomies s)
                  (Exist n f') -> (liftM $ Exist n) (unroll l bs
                   (addNomToSig n s') f') >>= checkForRepNom n (nomies s)
                  (UnderLogic f') ->
                   liftM UnderLogic $ undFormAna l (extended s) f' bs
                  (Par f') -> liftM Par (unroll l bs s' f')
                  TrueA -> return TrueA
                  FalseA -> return FalseA
unroll _ _ EmptySign _ = error "Signature not computable"

-- helper function
addNomToSig :: NOMINAL -> Sgn_Wrap -> Sgn_Wrap
addNomToSig n (Sgn_Wrap l s) = Sgn_Wrap l s
 { nomies = Data.Set.insert n $ nomies s}
addNomToSig _ EmptySign = error "Signature not computable"

checkForRepNom :: (Pretty f, GetRange f) =>
        NOMINAL -> Set NOMINAL -> TH_FORMULA f -> Result (TH_FORMULA f)
checkForRepNom n s = if member n s
        then mkError "conflict in nominal decl and quantification"
        else return
{- | Lift of the formula analyser
Analyses each formula and collects the results. Converting also the
annotations to the correct format. The function flipM is needed because
we want the annotations independent from the analyser -}
anaForms :: (Logic l sub bs sen si smi sign mor symb raw pf) =>
        l -> bs -> [Annoted Frm_Wrap] -> Sgn_Wrap -> Result [Named Frm_Wrap]
anaForms l bs f s = mapM (flipM . makeNamedSen . fmap (anaForm l bs s)) f

-- Just flips the monad position with the functor
flipM :: (Monad m) => Named (m a) -> m (Named a)
flipM y = sentence y >>= \ a -> return $ mapNamed (const a) y

{- | Examining the list of formulas and collecting results

Analyses first the underlying spec; Then analyses the top spec
(without the axioms) and merges the resulting sig with the underlying one.
Also translates the underlying axioms into hybridized ones, so that in the
end all axioms are of the same type;
Next analyses the hybrid axioms and puts them together with the already
translated axioms.
Finnaly prepares the tuple format for outputting. -}
thAna :: (Spc_Wrap, Sgn_Wrap, GlobalAnnos) ->
        Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])
thAna (Spc_Wrap l sp fs, _, _) = finalRes
        where
        undA = undAna l $ und sp
        partMerge = undA >>= \ (x1, x2, x3) -> topAna (bitems sp) l
                     (plainSign x2) >>= \ x -> return (x1, x, formMap x3)
        partMerge' = partMerge >>= \ (x1, x2, x3) ->
                      anaForms l x1 fs x2 >>= \ x -> return (x1, x2, x3 ++ x)
        finalRes = partMerge' >>= \ (x1, x2, x3) ->
                    return (mergSpec x1, mkExtSign x2, x3)
        formMap = Data.List.map $ mapNamed $ Frm_Wrap l . UnderLogic
        mergSpec e = Spc_Wrap l (Bspec (bitems sp) e) fs


-- Analysis of the underlying logic spec
undAna :: (StaticAnalysis l bs sen si smi sign mor symb raw) =>
                l -> bs -> Result (bs, ExtSign sign symb, [Named sen])
undAna l b = (maybeE 2 $ basic_analysis l) x
        where x = (b, empty_signature l, emptyGlobalAnnos)

unsafeToForm :: (StaticAnalysis l bs sen si smi sign mor symb raw) =>
                l -> a -> sen
unsafeToForm _ = unsafeCoerce
unsafeToSig :: (StaticAnalysis l bs sen si smi sign mor symb raw) =>
               l -> a -> sign
unsafeToSig _ = unsafeCoerce

{- Analysis of the sentences part the corresponds to the underlying logic. We
   need to use the unsafe functions here, because the typechecker has no way
   to check the (simple) relations (l -> sig) and (l -> sen). In other words
   it can't check that the arguments l and a belong to the Logic class,
   likewise for l -> b. The unsafe functions will give the "right"
   type associated with l. -}
undFormAna :: (StaticAnalysis l bs sen si smi sign mor symb raw) =>
                l -> a -> b -> bs -> Result sen
undFormAna l a b c = (maybeE 4 $ sen_analysis l) (c, a', b')
        where a' = unsafeToSig l a
              b' = unsafeToForm l b


{- -- Operations on sentences ----
How can we guarantee that the l in Sgn_Wrap is equal
to the l in Frm_Wrap ? -}
simSen :: Sgn_Wrap -> Frm_Wrap -> Frm_Wrap
simSen (Sgn_Wrap _ s) (Frm_Wrap l f) = Frm_Wrap l $
                uroll l (unsafeCoerce (extended s)) f
simSen EmptySign _ = error "The signature cannot be empty"

uroll :: (Logic l sub bs f s sm sgn mo sy rw pf) =>
        l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l s f = case f of
                At n f' -> At n $ uroll l s f'
                Box m f' -> Box m $ uroll l s f'
                Dia m f' -> Dia m $ uroll l s f'
                Conjunction f' f'' -> Conjunction (uroll l s f') $ uroll l s f''
                Disjunction f' f'' -> Disjunction (uroll l s f') $ uroll l s f''
                Implication f' f'' -> Implication (uroll l s f') $ uroll l s f''
                BiImplication f' f'' -> BiImplication (uroll l s f') $
                                         uroll l s f''
                Here n -> Here n
                Neg f' -> Neg $ uroll l s f'
                Par f' -> Par $ uroll l s f'
                UnderLogic f' -> UnderLogic $ simplify_sen l s f'
                x -> x

{- These instances should be automatically generated by DriFT, but it cannot
since they are not declared in a usual format -}
instance ShATermConvertible Sgn_Wrap where
         toShATermAux att (Sgn_Wrap _ s) = toShATermAux att s
         toShATermAux _ EmptySign = error "I entered in emptySign"
         fromShATermAux _ _ = error "I entered here"

instance ShATermConvertible Spc_Wrap where
         toShATermAux att (Spc_Wrap _ s _) = toShATermAux att s
         fromShATermAux _ _ = error "I entered here"

instance ShATermConvertible Frm_Wrap where
        toShATermAux att (Frm_Wrap _ f) = toShATermAux att f
        fromShATermAux _ _ = error "I entered here"