{-# 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.Categorical.Bifunctor

import Control.Monad

import Data.List

import Data.Set

import Unsafe.Coerce

import ATerm.Lib

-- | 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 $ Data.Set.union (fst x') (snd x')) /= (length $ fst x ++ (snd x))

s = THybridSign (fst x') (snd 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) = (unroll l bs s f) >>= return . (Frm_Wrap l)

-- 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') -> (unroll l bs s' f') >>= return . (At n) >>= nomOrModCheck (nomies s) n

(Box m f') -> (unroll l bs s' f') >>= return . (Box m) >>= nomOrModCheck (modies s) m

(Dia m f') -> (unroll l bs s' f') >>= return . (Dia m) >>= 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') -> (undFormAna l (extended s) f' bs) >>= (return . UnderLogic)

(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 x = (return x) >>= f

where f y = (sentence y) >>= \a -> return $ mapNamed (\_->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"