{-# LANGUAGE ExistentialQuantification #-}

{- |

Module : $Header$

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"