4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder{- |

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian MaederModule : $Header$

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian MaederDescription : final static analysis

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian MaederMaintainer : Christian.Maeder@dfki.de

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian MaederStability : experimental

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian MaederPortability : portable

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maederconversion from As to Le

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-}

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maedermodule HasCASL.AsToLe where

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maederimport Common.AS_Annotation

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maederimport Common.GlobalAnnotations

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maederimport Common.Id

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maederimport Common.Result

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maederimport Common.Prec

8878f7411a09d4dc54bf1941cc7a243e35ddb530Christian Maederimport Common.Lib.State

8878f7411a09d4dc54bf1941cc7a243e35ddb530Christian Maederimport qualified Data.Map as Map

8878f7411a09d4dc54bf1941cc7a243e35ddb530Christian Maederimport qualified Data.Set as Set

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maederimport HasCASL.As

import HasCASL.Le

import HasCASL.TypeAna

import HasCASL.ClassAna

import HasCASL.VarDecl

import HasCASL.Unify

import HasCASL.OpDecl

import HasCASL.TypeDecl

import HasCASL.Builtin

import HasCASL.PrintLe

import HasCASL.Merge

import HasCASL.MapTerm

import HasCASL.FoldTerm

import HasCASL.TypeCheck

import Data.Maybe

-- * extract predicate ids from As for mixfix analysis

type Ids = Set.Set Id

unite :: [Ids] -> Ids

unite = Set.unions

idsOfBasicSpec :: BasicSpec -> Ids

idsOfBasicSpec (BasicSpec l) = unite $ map (idsOfBasicItem . item) l

idsOfBasicItem :: BasicItem -> Ids

idsOfBasicItem bi = case bi of

SigItems i -> idsOfSigItems i

ClassItems _ l _ -> unite $ map (idsOfClassItem . item) l

GenItems l _ -> unite $ map (idsOfSigItems . item) l

Internal l _ -> unite $ map (idsOfBasicItem . item) l

_ -> Set.empty

idsOfClassItem :: ClassItem -> Ids

idsOfClassItem (ClassItem _ l _) = unite $ map (idsOfBasicItem . item) l

idsOfSigItems :: SigItems -> Ids

idsOfSigItems si = case si of

TypeItems _ _ _ -> Set.empty

OpItems b l _ -> unite $ map (idsOfOpItem b . item) l

idsOfOpItem :: OpBrand -> OpItem -> Ids

idsOfOpItem b oi = let stripCompound (Id ts _ ps) = Id ts [] ps in case oi of

OpDecl os _ _ _ -> case b of

Pred -> Set.union (Set.fromList os) $ Set.fromList

$ map stripCompound os

_ -> Set.empty

OpDefn i _ _ _ _ -> case b of

Pred -> Set.fromList [i, stripCompound i]

_ -> Set.empty

-- * basic analysis

-- | basic analysis

basicAnalysis :: (BasicSpec, Env, GlobalAnnos) ->

Result (BasicSpec, Env, [Named Sentence])

basicAnalysis (b, e, ga) =

let (nb, ne) = runState (anaBasicSpec ga b) e

in Result (reverse $ envDiags ne) $

Just (nb, cleanEnv ne, reverse $ sentences ne)

-- | is the signature empty?

isEmptyEnv :: Env -> Bool

isEmptyEnv e = Map.null (classMap e)

&& Map.null (typeMap e)

&& Map.null (assumps e)

-- | is the first argument a subsignature of the second?

isSubEnv :: Env -> Env -> Bool

isSubEnv e1 e2 = if e1 == e2 then True else isEmptyEnv $ diffEnv e1 e2

-- | compute difference of signatures

diffEnv :: Env -> Env -> Env

diffEnv e1 e2 = let

tm = typeMap e2

cm = Map.differenceWith diffClass (classMap e1) $ classMap e2

in initialEnv

{ classMap = cm

, typeMap = diffTypeMap cm (typeMap e1) tm

, assumps = Map.differenceWith (diffAss cm (filterAliases tm)

$ addUnit cm tm) (assumps e1) $ assumps e2

}

-- | compute difference of class infos

diffClass :: ClassInfo -> ClassInfo -> Maybe ClassInfo

diffClass _ _ = Nothing

-- | compute difference of overloaded operations

diffAss :: ClassMap -> TypeMap -> TypeMap -> Set.Set OpInfo -> Set.Set OpInfo

-> Maybe (Set.Set OpInfo)

diffAss cm tAs tm s1 s2 =

let s3 = diffOps cm tAs tm s1 s2 in

if Set.null s3 then Nothing else Just s3

diffOps :: ClassMap -> TypeMap -> TypeMap -> Set.Set OpInfo -> Set.Set OpInfo

-> Set.Set OpInfo

diffOps cm tAs tm s1 s2 = if Set.null s1 then s1 else

let (o, os) = Set.deleteFindMin s1

rs = diffOps cm tAs tm os s2

n = mapOpInfo (id, expandAliases tAs) o

in if Set.null $ Set.filter

(instScheme tm 1 (opType n) . expand tAs . opType) s2

then Set.insert n rs else rs

-- | clean up finally accumulated environment

cleanEnv :: Env -> Env

cleanEnv e = diffEnv initialEnv

{ classMap = classMap e

, typeMap = typeMap e

, assumps = assumps e } preEnv

-- | analyse basic spec

anaBasicSpec :: GlobalAnnos -> BasicSpec -> State Env BasicSpec

anaBasicSpec ga b@(BasicSpec l) = do

e <- get

let newAs = assumps e

preds = Map.keysSet $ Map.filter (not . Set.null . Set.filter ( \ oi ->

case opDefn oi of

NoOpDefn Pred -> True

Definition Pred _ -> True

_ -> False)) newAs

newPreds = idsOfBasicSpec b

rels = Set.union preds newPreds

newGa = addBuiltins ga

precs = mkPrecIntMap $ prec_annos newGa

Result _ (Just ne) = merge preEnv e

put ne { preIds = (precs, rels), globAnnos = newGa }

ul <- mapAnM (anaBasicItem newGa) l

return $ BasicSpec ul

-- | analyse basic item

anaBasicItem :: GlobalAnnos -> BasicItem -> State Env BasicItem

anaBasicItem ga bi = case bi of

SigItems i -> fmap SigItems $ anaSigItems ga Loose i

ClassItems inst l ps -> do

ul <- mapAnM (anaClassItem ga inst) l

return $ ClassItems inst ul ps

GenVarItems l ps -> do

ul <- mapM (anaddGenVarDecl True) l

return $ GenVarItems (catMaybes ul) ps

ProgItems l ps -> do

ul <- mapAnMaybe (anaProgEq ga) l

return $ ProgItems ul ps

FreeDatatype l ps -> do

al <- mapAnMaybe ana1Datatype l

tys <- mapM (dataPatToType . item) al

ul <- mapAnMaybe (anaDatatype Free tys) al

addDataSen tys

return $ FreeDatatype ul ps

GenItems l ps -> do

ul <- mapAnM (anaSigItems ga Generated) l

return $ GenItems ul ps

AxiomItems decls fs ps -> do

tm <- gets typeMap -- save type map

as <- gets assumps -- save vars

ds <- mapM (anaddGenVarDecl True) decls

ts <- mapM (anaFormula ga) fs

e <- get

putTypeMap tm -- restore

putAssumps as -- restore

let newFs = catMaybes ts

newDs = catMaybes ds

sens = map ( \ (_, f) -> makeNamed (getRLabel f) $ Formula

$ mkEnvForall e (item f) ps) newFs

appendSentences sens

return $ AxiomItems newDs (map fst newFs) ps

Internal l ps -> do

ul <- mapAnM (anaBasicItem ga) l

return $ Internal ul ps

freeVars :: Term -> Set.Set VarDecl

freeVars = foldTerm FoldRec

{ foldQualVar = \ _ t -> Set.singleton t

, foldQualOp = \ _ _ _ _ _ _ -> Set.empty

, foldApplTerm = \ _ t1 t2 _ -> Set.union t1 t2

, foldTupleTerm = \ _ tts _ -> Set.unions tts

, foldTypedTerm = \ _ ts _ _ _ -> ts

, foldAsPattern = \ _ t ts _ -> Set.insert t ts

, foldQuantifiedTerm = \ _ _ gvs ts _ -> Set.difference ts $

foldr ( \ gv -> case gv of

GenVarDecl t -> Set.insert t

_ -> id) Set.empty gvs

, foldLambdaTerm = \ _ pats _ ts _ -> Set.difference ts $ Set.unions pats

, foldCaseTerm = \ _ ts tts _ -> Set.difference

(Set.unions $ ts : map snd tts) $ Set.unions $ map fst tts

, foldLetTerm = \ _ _ tts ts _ -> Set.difference

(Set.unions $ ts : map snd tts) $ Set.unions $ map fst tts

, foldResolvedMixTerm = \ _ _ _ tts _ -> Set.unions tts

, foldTermToken = \ _ _ -> Set.empty

, foldMixTypeTerm = \ _ _ _ _ -> Set.empty

, foldMixfixTerm = \ _ tts -> Set.unions tts

, foldBracketTerm = \ _ _ tts _ -> Set.unions tts

, foldProgEq = \ _ ps ts _ -> (ps, ts) }

-- | quantify

mkEnvForall :: Env -> Term -> Range -> Term

mkEnvForall e t ps =

let tys = Set.fromList $ map (fst . snd) $ concatMap (leaves (>= 0))

$ getAllTypes t

tyVs = map ( \ (i, TypeVarDefn v vk rk c) -> GenTypeVarDecl $

TypeArg i v vk rk c Other ps) $ Map.toList

$ Map.filterWithKey ( \ i _ -> Set.member i tys) $ localTypeVars e

vs = tyVs ++ map GenVarDecl (Set.toList $ freeVars t)

in if null vs then t else QuantifiedTerm Universal vs t ps

-- | analyse sig items

anaSigItems :: GlobalAnnos -> GenKind -> SigItems -> State Env SigItems

anaSigItems ga gk si = case si of

TypeItems inst l ps -> do

ul <- anaTypeItems ga gk l

return $ TypeItems inst ul ps

OpItems b l ps -> do

ul <- mapAnMaybe (anaOpItem ga b) l

return $ OpItems b ul ps

-- | analyse a class item

anaClassItem :: GlobalAnnos -> Instance -> ClassItem

-> State Env ClassItem

anaClassItem ga _ (ClassItem d l ps) = do

cd <- anaClassDecls d

ul <- mapAnM (anaBasicItem ga) l

return $ ClassItem cd ul ps