{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}

{- |

Module : $Header$

Description : static analysis of VSE parts

Copyright : (c) C. Maeder, DFKI Bremen 2008

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

analysis of VSE logic extension of CASL

-}

module VSE.Ana

( VSESign

, uTrue

, uFalse

, aTrue

, aFalse

, uBoolean

, constBoolType

, boolSig

, lookupProc

, procsToOpMap

, procsToPredMap

, profileToOpType

, profileToPredType

, checkCases

, basicAna

, mapDlformula

, minExpForm

, simpDlformula

, correctSign

, correctTarget

, inducedExt

, VSEMorExt

, VSEMor

, VSEBasicSpec

, extVSEColimit

, vseMorExt

) where

import Control.Monad

import Data.Char (toLower)

import Data.List

import qualified Data.Map as Map

import qualified Data.Set as Set

import qualified Common.Lib.MapSet as MapSet

import qualified Common.Lib.Rel as Rel

import Common.AS_Annotation

import Common.GlobalAnnotations

import Common.ExtSign

import Common.Id

import Common.Result

import Common.Utils (hasMany)

import Common.Lib.State

import CASL.AS_Basic_CASL

import CASL.Fold

import CASL.Sign

import CASL.MixfixParser

import CASL.MapSentence as MapSen

import CASL.Morphism

import CASL.Overload

import CASL.Quantification

import CASL.StaticAna

import CASL.ShowMixfix as Paren

import CASL.SimplifySen

import VSE.As

import VSE.Fold

import Data.Graph.Inductive.Graph

import Common.Lib.Graph

type VSESign = Sign Dlformula Procs

getVariables :: Sentence -> Set.Set Token

getVariables = foldFormula $ getVarsRec $ getVSEVars . unRanged

getVarsRec :: (f -> Set.Set Token) -> Record f (Set.Set Token) (Set.Set Token)

getVarsRec f =

(constRecord f Set.unions Set.empty)

{ foldQuantification = \ _ _ vs r _ -> Set.union r

$ Set.fromList $ map fst $ flatVAR_DECLs vs

, foldQual_var = \ _ v _ _ -> Set.singleton v }

getVSEVars :: VSEforms -> Set.Set Token

getVSEVars vf = case vf of

Dlformula _ p s -> Set.union (getProgVars p) $ getVariables s

Defprocs l -> Set.unions $ map getDefprogVars l

_ -> Set.empty -- no variables in a sort generation constraint

getProgVars :: Program -> Set.Set Token

getProgVars =

let vrec = getVarsRec $ const Set.empty

getTermVars = foldTerm vrec

getCondVars = foldFormula vrec

in foldProg (progToSetRec getTermVars getCondVars)

{ foldAssign = \ _ v t -> Set.insert v $ getTermVars t

, foldBlock = \ _ vs p -> Set.union p

$ Set.fromList $ map fst $ flatVAR_DECLs vs }

getDefprogVars :: Defproc -> Set.Set Token

getDefprogVars (Defproc _ _ vs p _) = Set.union (getProgVars p)

$ Set.fromList vs

tokenToLower :: Token -> Token

tokenToLower (Token s r) = Token (map toLower s) r

idToLower :: Id -> Id

idToLower (Id ts cs r) = Id (map tokenToLower ts) (map idToLower cs) r

getCases :: String -> Set.Set Id -> [Diagnosis]

getCases msg =

map (mkDiag Error ("overlapping " ++ msg ++ " identifiers") . Set.toList)

. filter hasMany . Map.elems

. Set.fold (\ i -> MapSet.setInsert (idToLower i) i) Map.empty

getCaseDiags :: Sign f e -> [Diagnosis]

getCaseDiags sig =

getCases "sort" (sortSet sig)

++ getCases "op or function" (MapSet.keysSet $ opMap sig)

++ getCases "pred or proc" (MapSet.keysSet $ predMap sig)

uBoolean :: Id

uBoolean = stringToId "Boolean"

uTrue :: Id

uTrue = stringToId "True"

uFalse :: Id

uFalse = stringToId "False"

tBoolean :: OP_TYPE

tBoolean = Op_type Total [] uBoolean nullRange

constBoolType :: OpType

constBoolType = toOpType tBoolean

qBoolean :: Id -> OP_SYMB

qBoolean c = Qual_op_name c tBoolean nullRange

qTrue :: OP_SYMB

qTrue = qBoolean uTrue

qFalse :: OP_SYMB

qFalse = qBoolean uFalse

mkConstAppl :: OP_SYMB -> TERM f

mkConstAppl o = Application o [] nullRange

aTrue :: TERM f

aTrue = mkConstAppl qTrue

aFalse :: TERM f

aFalse = mkConstAppl qFalse

uOpMap :: OpMap

uOpMap = MapSet.fromList $ map (\ c -> (c, [constBoolType]))

[uFalse, uTrue]

boolSig :: Sign f Procs

boolSig = (emptySign emptyProcs)

{ sortRel = Rel.insertKey uBoolean Rel.empty

, opMap = uOpMap }

lookupProc :: Id -> Sign f Procs -> Maybe Profile

lookupProc i = Map.lookup i . procsMap . extendedInfo

procsSign :: Sign f Procs -> Sign f Procs

procsSign sig = (emptySign emptyProcs)

{ predMap = procsToPredMap $ extendedInfo sig }

-- | add procs as predicate

addProcs :: Sign f Procs -> Sign f Procs

addProcs sig = addSig const sig $ procsSign sig

-- | remove procs as predicate

subProcs :: Sign f Procs -> Sign f Procs

subProcs sig = diffSig const sig $ procsSign sig

checkCases :: Sign f e -> [Named Sentence] -> [Diagnosis]

checkCases sig2 sens = getCaseDiags sig2 ++ concatMap

(getCases "var" . Set.map simpleIdToId . getVariables . sentence) sens

type VSEBasicSpec = BASIC_SPEC () Procdecls Dlformula

basicAna :: (VSEBasicSpec, VSESign, GlobalAnnos)

-> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])

basicAna (bs, sig, ga) = do

let sigIn = subProcs $ addSig const sig boolSig

(bs2, ExtSign sig2 syms, sens) <-

basicAnalysis minExpForm (const return) anaProcdecls anaMix

(bs, sigIn, ga)

appendDiags $ checkCases sig2 sens

appendDiags . map

(mkDiag Error "illegal predicate declaration for procedure")

. Set.toList . MapSet.keysSet . interMapSet

(diffMapSet (predMap sig2) $ predMap sigIn)

. procsToPredMap $ extendedInfo sig2

let sig3 = diffSig const sig2 boolSig

(rSens, fSens) = partition (foldFormula (checkRec True) . sentence) sens

appendDiags $ map (mkDiag Error "unsupported VSE formula" . sentence) fSens

appendDiags . map (mkDiag Error "illegal overloading of")

. Set.toList . Set.intersection (MapSet.keysSet $ opMap sig3)

$ MapSet.keysSet uOpMap

return (bs2, ExtSign (addProcs sig3) syms, rSens)

anaMix :: Mix () Procdecls Dlformula Procs

anaMix = emptyMix

{ putParen = parenDlFormula

, mixResolve = resolveDlformula }

-- | put parens around ambiguous mixfix formulas (for error messages)

parenDlFormula :: Dlformula -> Dlformula

parenDlFormula (Ranged f r) = case f of

Dlformula b p s ->

let n = mapFormula parenDlFormula s

in Ranged (Dlformula b (parenProg p) n) r

Defprocs ps -> Ranged (Defprocs $ map parenDefproc ps) r

_ -> Ranged f r -- no mixfix formulas?

parenProg :: Program -> Program

parenProg = foldProg $ mapProg (Paren.mapTerm id) $ mapFormula id

parenDefproc :: Defproc -> Defproc

parenDefproc (Defproc k i vs p r) = Defproc k i vs (parenProg p) r

procsToPredMap :: Procs -> PredMap

procsToPredMap (Procs m) =

foldr (\ (n, pr@(Profile _ mr)) pm -> case mr of

Nothing -> MapSet.insert n (profileToPredType pr) pm

Just _ -> pm) MapSet.empty $ Map.toList m

procsToOpMap :: Procs -> OpMap

procsToOpMap (Procs m) =

foldr (\ (n, pr) om -> case profileToOpType pr of

Just ot -> MapSet.insert n ot om

Nothing -> om) MapSet.empty $ Map.toList m

-- | resolve mixfix applications of terms and formulas

resolveDlformula :: MixResolve Dlformula

resolveDlformula ga rules (Ranged f r) = case f of

Dlformula b p s -> do

np <- resolveProg ga rules p

n <- resolveMixFrm id resolveDlformula ga rules s

return $ Ranged (Dlformula b np n) r

Defprocs ps -> do

nps <- mapM (resolveDefproc ga rules) ps

return $ Ranged (Defprocs nps) r

_ -> return $ Ranged f r -- no mixfix?

resolveT :: MixResolve (TERM ())

resolveT = resolveMixTrm id (mixResolve emptyMix)

resolveF :: MixResolve (FORMULA ())

resolveF = resolveMixFrm id (mixResolve emptyMix)

resolveProg :: MixResolve Program

resolveProg ga rules p@(Ranged prg r) = case prg of

Abort -> return p

Skip -> return p

Assign v t -> do

nt <- resolveT ga rules t

return $ Ranged (Assign v nt) r

Call f -> do

nf <- resolveF ga rules f

return $ Ranged (Call nf) r

Return t -> do

nt <- resolveT ga rules t

return $ Ranged (Return nt) r

Block vs q -> do

np <- resolveProg ga rules q

return $ Ranged (Block vs np) r

Seq p1 p2 -> do

p3 <- resolveProg ga rules p1

p4 <- resolveProg ga rules p2

return $ Ranged (Seq p3 p4) r

If f p1 p2 -> do

c <- resolveF ga rules f

p3 <- resolveProg ga rules p1

p4 <- resolveProg ga rules p2

return $ Ranged (If c p3 p4) r

While f q -> do

c <- resolveF ga rules f

np <- resolveProg ga rules q

return $ Ranged (While c np) r

resolveDefproc :: MixResolve Defproc

resolveDefproc ga rules (Defproc k i vs p r) = do

np <- resolveProg ga rules p

return $ Defproc k i vs np r

-- | resolve overloading and type check terms and formulas

minExpForm :: Min Dlformula Procs

minExpForm sign (Ranged f r) = let sig = castSign sign in case f of

Dlformula b p s -> do

np <- minExpProg Set.empty Nothing sig p

n <- minExpFORMULA minExpForm sign s

return $ Ranged (Dlformula b np n) r

Defprocs ps -> do

nps <- mapM (minProcdecl sig) ps

return $ Ranged (Defprocs nps) r

_ -> fail "nyi for restricted constraints"

oneExpT :: Sign () Procs -> TERM () -> Result (TERM ())

oneExpT = oneExpTerm (const return)

minExpF :: Sign () Procs -> FORMULA () -> Result (FORMULA ())

minExpF = minExpFORMULA (const return)

checkRec :: Bool -> Record f Bool Bool

checkRec b = (constRecord (const False) and True)

{ foldQuantification = \ _ _ _ _ _ -> b

, foldDefinedness = \ _ _ _ -> False

, foldEquation = \ _ _ e _ _ -> e == Strong

, foldMembership = \ _ _ _ _ -> False

, foldCast = \ _ _ _ _ -> False

, foldConditional = \ _ _ _ _ _ -> False

, foldExtFORMULA = \ _ _ -> b }

minExpProg :: Set.Set VAR -> Maybe SORT -> Sign () Procs

-> Program -> Result Program

minExpProg invars res sig p@(Ranged prg r) = let

checkCond f = if foldFormula (checkRec False) f then return f else

mkError "illegal formula" f

checkTerm t = if foldTerm (checkRec False) t then return t else

mkError "illegal term" t

in case prg of

Abort -> return p

Skip -> return p

Assign v t -> case Map.lookup v $ varMap sig of

Nothing -> Result [mkDiag Error "undeclared program variable" v] Nothing

Just s -> do

nt <- oneExpT sig $ Sorted_term t s r

checkTerm nt

when (Set.member v invars)

$ appendDiags [mkDiag Warning "assignment to input variable" v]

return $ Ranged (Assign v nt) r

Call f -> case f of

Predication ps ts _ -> let i = predSymbName ps in

case lookupProc i sig of

Nothing -> Result [mkDiag Error "unknown procedure" i] Nothing

Just pr@(Profile l re) -> let

nl = case re of

Nothing -> l

Just s -> l ++ [Procparam Out s]

in if length nl /= length ts then

Result [mkDiag Error "non-matching number of parameters for" i]

Nothing

else do

sign <- if length l < length nl then

Result [mkDiag Warning "function used as procedure" i] $ Just

sig { predMap = MapSet.insert i (funProfileToPredType pr)

$ predMap sig }

else return sig { predMap = MapSet.insert i (profileToPredType pr)

$ predMap sig }

nf <- minExpF sign f

checkCond nf

return $ Ranged (Call nf) r

_ -> Result [mkDiag Error "no procedure call" f] Nothing

Return t -> case res of

Nothing -> Result [mkDiag Error "unexpected return statement" t] Nothing

Just s -> do

nt <- oneExpT sig $ Sorted_term t s r

checkTerm nt

return $ Ranged (Return nt) r

Block vs q -> do

let sign' = execState (mapM_ addVSEVars vs) sig { envDiags = [] }

appendDiags $ envDiags sign'

np <- minExpProg invars res sign' q

return $ Ranged (Block vs np) r

Seq p1 p2 -> do

p3 <- minExpProg invars res sig p1

p4 <- minExpProg invars res sig p2

return $ Ranged (Seq p3 p4) r

If f p1 p2 -> do

c <- minExpF sig f

checkCond c

p3 <- minExpProg invars res sig p1

p4 <- minExpProg invars res sig p2

return $ Ranged (If c p3 p4) r

While f q -> do

c <- minExpF sig f

checkCond c

np <- minExpProg invars res sig q

return $ Ranged (While c np) r

addVSEVars :: VAR_DECL -> State (Sign f Procs) ()

addVSEVars vd@(Var_decl vs _ _) = do

addVars vd

p <- gets $ procsMap . extendedInfo

mapM_ (addDiags . checkWithMap "var" "procedure" p . simpleIdToId) vs

minProcdecl :: Sign () Procs -> Defproc -> Result Defproc

minProcdecl sig (Defproc k i vs p r) = case lookupProc i sig of

Nothing -> Result [mkDiag Error "unknown procedure" i] Nothing

Just (Profile l re) -> if length vs /= length l then

Result [mkDiag Error "unknown procedure" i] Nothing

else do

let invars = Set.fromList $ map fst $

filter (\ (_, Procparam j _) -> j == In) $ zip vs l

np <- minExpProg invars re sig { varMap = Map.fromList $ zipWith

(\ v (Procparam _ s) -> (v, s)) vs l } p

return $ Defproc k i vs np r

-- | analyse and add procedure declarations

anaProcdecls :: Ana Procdecls () Procdecls Dlformula Procs

anaProcdecls _ ds@(Procdecls ps _) = do

mapM_ (anaProcdecl . item) ps

return ds

anaProcdecl :: Sigentry -> State (Sign Dlformula Procs) ()

anaProcdecl (Procedure i p@(Profile ps mr) q) = do

e <- get

let prM = predMap e

l = MapSet.lookup i prM

ea = emptyAnno ()

isPred = case mr of

Nothing -> Set.member (profileToPredType p) l

_ -> False

updateExtInfo (\ pm@(Procs m) ->

let n = Procs $ Map.insert i p m in case Map.lookup i m of

Just o -> if p == o then

hint n ("repeated procedure " ++ showId i "") q

else plain_error pm

("cannot change profile of procedure " ++ showId i "") q

Nothing -> if isPred then plain_error pm

("cannot change predicate to procedure " ++ showId i "") q

else return n)

case profileToOpType p of

Just t -> do

unless (all (\ (Procparam j _) -> j == In) ps)

$ addDiags [mkDiag Warning "function must have IN params only" i]

addOp ea t i

_ -> unless isPred

$ addAnnoSet ea $ Symbol i $ PredAsItemType $ profileToPredType p

paramsToArgs :: [Procparam] -> [SORT]

paramsToArgs = map (\ (Procparam _ s) -> s)

profileToPredType :: Profile -> PredType

profileToPredType (Profile a _) = PredType $ paramsToArgs a

funProfileToPredType :: Profile -> PredType

funProfileToPredType (Profile a r) = case r of

Nothing -> error "funProfileToPredType"

Just s -> PredType $ paramsToArgs a ++ [s]

profileToOpType :: Profile -> Maybe OpType

profileToOpType (Profile a r) = case r of

Nothing -> Nothing

Just s -> Just $ OpType Partial (paramsToArgs a) s

castSign :: Sign f e -> Sign a e

castSign s = s { sentences = [] }

castMor :: Morphism f e b -> Morphism a e b

castMor m = m

{ msource = castSign $ msource m

, mtarget = castSign $ mtarget m }

type VSEMorExt = DefMorExt Procs

type VSEMor = Morphism Dlformula Procs VSEMorExt

-- | apply a morphism

mapMorProg :: Morphism f Procs VSEMorExt -> Program -> Program

mapMorProg mor = let m = castMor mor in

foldProg (mapProg (MapSen.mapTerm (const id) m)

$ mapSen (const id) m)

{ foldBlock = \ (Ranged _ r) vs p ->

Ranged (Block (map (mapVars m) vs) p) r

, foldCall = \ (Ranged _ r) f -> case f of

Predication (Qual_pred_name i (Pred_type args r1) r2) ts r3 ->

case lookupProc i $ msource mor of

Nothing -> error "mapMorProg"

Just pr -> let

j = mapProcIdProfile mor i pr

nargs = map (mapSrt mor) args

nts = map (MapSen.mapTerm (const id) m) ts

in Ranged (Call $ Predication

(Qual_pred_name j (Pred_type nargs r1) r2) nts r3) r

_ -> error $ "mapMorProg " ++ show f }

mapProcId :: Morphism f Procs VSEMorExt -> Id -> Id

mapProcId m i = case lookupProc i $ msource m of

Just p -> mapProcIdProfile m i p

Nothing -> error $ "VSE.mapProcId unknown " ++ show i

mapProcIdProfile :: Morphism f Procs VSEMorExt -> Id -> Profile -> Id

mapProcIdProfile m = mapProcIdProfileExt (sort_map m) (op_map m) (pred_map m)

mapProcIdProfileExt :: Sort_map -> Op_map -> Pred_map -> Id -> Profile -> Id

mapProcIdProfileExt sm om pm i p = case profileToOpType p of

Just t -> fst $ mapOpSym sm om (i, t)

Nothing -> fst $ mapPredSym sm pm (i, profileToPredType p)

mapMorDefproc :: Morphism f Procs VSEMorExt -> Defproc -> Defproc

mapMorDefproc m (Defproc k i vs p r) =

Defproc k (mapProcId m i) vs (mapMorProg m p) r

mapDlformula :: MapSen Dlformula Procs VSEMorExt

mapDlformula m (Ranged f r) = case f of

Dlformula b p s ->

let n = mapSen mapDlformula m s

in Ranged (Dlformula b (mapMorProg m p) n) r

Defprocs ps -> Ranged (Defprocs $ map (mapMorDefproc m) ps) r

RestrictedConstraint constr restr flag ->

Ranged

(RestrictedConstraint

(map (MapSen.mapConstr m) constr)

(Map.fromList

$ map (\ (s, i) -> (mapSort (sort_map m) s, mapProcId m i))

$ Map.toList restr)

flag) r

-- | simplify fully qualified terms and formulas for pretty printing sentences

simpProg :: Sign () e -> Program -> Program

simpProg sig =

foldProg (mapProg (simplifyTerm dummyMin (const id) sig)

$ simplifySen dummyMin (const id) sig)

{ foldBlock = \ (Ranged b r) _ _ -> case b of

Block vs p -> Ranged (Block vs $ simpProg

(execState (mapM_ addVars vs) sig) p) r

_ -> error "VSE.Ana.simpProg" }

simpDefproc :: Sign () Procs -> Defproc -> Defproc

simpDefproc sign (Defproc k i vs p r) =

let sig = case lookupProc i sign of

Nothing -> sign

Just (Profile l _) -> if length vs /= length l then sign

else sign { varMap = Map.fromList $ zipWith

(\ v (Procparam _ s) -> (v, s)) vs l }

in Defproc k i vs (simpProg sig p) r

simpDlformula :: Sign Dlformula Procs -> Dlformula -> Dlformula

simpDlformula sign (Ranged f r) = let sig = castSign sign in case f of

Dlformula b p s -> let

q = simpProg sig p

n = simplifySen minExpForm simpDlformula sign s

in Ranged (Dlformula b q n) r

Defprocs ps -> Ranged (Defprocs $ map (simpDefproc sig) ps) r

RestrictedConstraint {} -> Ranged f r

-- how should this be for restricted constraints?

-- | free variables to be universally bound on the top level

freeProgVars :: Sign () e -> Program -> VarSet

freeProgVars sig = let ft = freeTermVars sig in

foldProg (progToSetRec ft (freeVars sig))

{ foldAssign = \ _ v t -> (case Map.lookup v $ varMap sig of

Just s -> Set.insert (v, s)

Nothing -> Set.insert (v, sortOfTerm t)) $ ft t

, foldBlock = \ (Ranged b _) _ _ -> case b of

Block vs p ->

Set.difference (freeProgVars (execState (mapM_ addVars vs) sig) p)

$ Set.fromList $ flatVAR_DECLs vs

_ -> error "VSE.Ana.freeProgVars" }

freeDlVars :: Sign Dlformula e -> Dlformula -> VarSet

freeDlVars sig (Ranged f _) = case f of

Dlformula _ p s -> Set.union (freeProgVars (castSign sig) p) $

freeVars sig s

Defprocs _ -> Set.empty

RestrictedConstraint {} -> Set.empty

instance TermExtension Dlformula where

freeVarsOfExt = freeDlVars

-- | adjust procs map in morphism target signature

correctTarget :: Morphism f Procs VSEMorExt -> Morphism f Procs VSEMorExt

correctTarget m = m

{ mtarget = correctSign $ mtarget m

, msource = correctSign $ msource m }

inducedExt :: InducedSign f Procs VSEMorExt Procs

inducedExt sm om pm _ = Procs . Map.fromList

. map (\ (i, p) -> (mapProcIdProfileExt sm om pm i p, mapProfile sm p))

. Map.toList . procsMap . extendedInfo

correctSign :: Sign f Procs -> Sign f Procs

correctSign sig = sig

{ extendedInfo = Procs $ Map.filterWithKey (\ i p -> case profileToOpType p of

Just t -> let s = MapSet.lookup i $ opMap sig in

Set.member t s || Set.member (mkTotal t) s

Nothing ->

Set.member (profileToPredType p) . MapSet.lookup i $ predMap sig

) $ procsMap $ extendedInfo sig }

mapProfile :: Sort_map -> Profile -> Profile

mapProfile m (Profile l r) = Profile

(map (\ (Procparam k s) -> Procparam k $ mapSort m s) l)

$ fmap (mapSort m) r

extVSEColimit :: Gr Procs (Int, VSEMorExt) ->

Map.Map Int VSEMor ->

(Procs, Map.Map Int VSEMorExt)

extVSEColimit graph morMap = let

procs = Map.fromList $ nub $

concatMap (\ (n, Procs p) -> let

phi = Map.findWithDefault (error "extVSEColimit") n morMap

in map (\ (idN, profile) ->

(mapProcId phi idN, mapProfile (sort_map phi) profile)) $

Map.toList p) $

labNodes graph

in (Procs procs, Map.fromList $ map (\ n -> (n, emptyMorExt)) $

nodes graph)

vseMorExt :: CASLMor -> (Op_map, Pred_map)

vseMorExt m = let

sm = Map.toList $ sort_map m

om = op_map m

pm = pred_map m

eqOps = Map.fromList $ map (\ (s, t) ->

((gnEqName s, OpType Partial [s, s] uBoolean)

, (gnEqName t, Partial))) sm

restrPreds = Map.fromList $ map (\ (s, t) ->

((gnRestrName s, PredType [s]), gnRestrName t)) sm

opsProcs = Map.fromList $ map (\ ((idN, OpType _ w s), (idN', _)) ->

((mkGenName idN, OpType Partial w s)

, (mkGenName idN', Partial))) $ Map.toList om

predProcs = Map.fromList $ map (\ ((idN, PredType w), idN') ->

((mkGenName idN, PredType w), mkGenName idN')) $ Map.toList pm

in (Map.union eqOps opsProcs, Map.union restrPreds predProcs)