8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova{- |

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaModule : $Header$

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina SojakovaCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina SojakovaLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaMaintainer : maeder@tzi.de

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaStability : experimental

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaPortability : portable

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaconversion from As to Le

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-}

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovamodule HasCASL.AsToLe where

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.AS_Annotation

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Common.GlobalAnnotations

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.Id

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.Result

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.Prec

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.Lib.State

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport qualified Common.Lib.Rel as Rel

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport qualified Common.Lib.Map as Map

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport qualified Common.Lib.Set as Set

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport HasCASL.As

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport HasCASL.Le

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport HasCASL.TypeAna

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport HasCASL.ClassAna

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport HasCASL.VarDecl

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakovaimport HasCASL.Unify

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport HasCASL.OpDecl

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaimport HasCASL.TypeDecl

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaimport HasCASL.Builtin

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport HasCASL.MapTerm

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakovaimport Data.Maybe

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- * extract predicate ids from As for mixfix analysis

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovatype Ids = Set.Set Id

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaunite :: [Ids] -> Ids

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaunite = Set.unions

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovaidsOfBasicSpec :: BasicSpec -> Ids

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovaidsOfBasicSpec (BasicSpec l) = unite $ map (idsOfBasicItem . item) l

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovaidsOfBasicItem :: BasicItem -> Ids

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovaidsOfBasicItem (SigItems i) = idsOfSigItems i

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovaidsOfBasicItem (ClassItems _ l _ ) = unite $ map (idsOfClassItem . item) l

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovaidsOfBasicItem (GenItems l _) = unite $ map (idsOfSigItems . item) l

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovaidsOfBasicItem (Internal l _) = unite $ map (idsOfBasicItem . item) l

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovaidsOfBasicItem _ = Set.empty

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovaidsOfClassItem :: ClassItem -> Ids

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovaidsOfClassItem (ClassItem _ l _) = unite $ map (idsOfBasicItem . item) l

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovaidsOfSigItems :: SigItems -> Ids

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovaidsOfSigItems (TypeItems _ _ _) = Set.empty

345d3dcc9f809776009851c446916fc770aa428dKristina SojakovaidsOfSigItems (OpItems b l _) = unite $ map (idsOfOpItem b . item) l

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova

345d3dcc9f809776009851c446916fc770aa428dKristina SojakovaidsOfOpItem :: OpBrand -> OpItem -> Ids

345d3dcc9f809776009851c446916fc770aa428dKristina SojakovaidsOfOpItem b (OpDecl os _ _ _) =

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova let ois = Set.fromList $ map ( \ (OpId i _ _) -> i) os

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova in case b of

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova Pred -> ois

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova _ -> Set.empty

345d3dcc9f809776009851c446916fc770aa428dKristina SojakovaidsOfOpItem b (OpDefn (OpId i _ _) _ _ _ _ _) =

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova case b of

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova Pred -> (Set.singleton i)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova _ -> Set.empty

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-- * basic analysis

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-- | basic analysis

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovabasicAnalysis :: (BasicSpec, Env, GlobalAnnos) ->

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova Result (BasicSpec, Env, [Named Sentence])

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovabasicAnalysis (b, e, ga) =

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

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova in Result (reverse $ envDiags ne) $

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova Just (nb, cleanEnv ne, reverse $ sentences ne)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- | is the signature empty?

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovaisEmptyEnv :: Env -> Bool

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovaisEmptyEnv 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 = isEmptyEnv $ diffEnv e1 e2

-- a rough equality

instance Eq Env where

e1 == e2 = isSubEnv e1 e2 && isSubEnv e2 e1

-- | compute difference of signatures

diffEnv :: Env -> Env -> Env

diffEnv e1 e2 = let tm = typeMap e2 in

initialEnv

{ classMap = Map.differenceWith diffClass (classMap e1) (classMap e2)

, typeMap = Map.differenceWith diffType (typeMap e1) tm

, assumps = Map.differenceWith (diffAss $ addUnit tm)

(assumps e1) (assumps e2)

}

-- | compute difference of class infos

diffClass :: ClassInfo -> ClassInfo -> Maybe ClassInfo

diffClass _ _ = Nothing

-- | compute difference of type infos

diffType :: TypeInfo -> TypeInfo -> Maybe TypeInfo

diffType _ _ = Nothing

-- | compute difference of overloaded operations

diffAss :: TypeMap -> OpInfos -> OpInfos -> Maybe OpInfos

diffAss tm (OpInfos l1) (OpInfos l2) =

let l3 = diffOps l1 l2 in

if null l3 then Nothing else Just (OpInfos l3)

where diffOps [] _ = []

diffOps (o:os) ps =

let rs = diffOps os ps

n = mapOpInfo (id, expandAlias tm) o

in if any (instScheme tm 1 (opType n) . expand tm . opType) ps

then rs else n:rs

-- | environment with predefined types and operations

addPreDefs :: Env -> Env

addPreDefs e = e { typeMap = addUnit $ typeMap e

, assumps = addOps $ assumps e }

-- | environment with predefined types and operations

preEnv :: Env

preEnv = addPreDefs initialEnv

-- | clean up finally accumulated environment

cleanEnv :: Env -> Env

cleanEnv e = diffEnv initialEnv

{ classMap = classMap e

, typeMap = typeMap e

, assumps = assumps e }

preEnv where

-- | analyse basic spec

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

anaBasicSpec ga b@(BasicSpec l) = do

e <- get

let newAs = assumps e

preds = Rel.keysSet $ Map.filter (any ( \ oi ->

case opDefn oi of

NoOpDefn Pred -> True

Definition Pred _ -> True

_ -> False) . opInfos) newAs

newPreds = idsOfBasicSpec b

rels = Set.union preds newPreds

newGa = addBuiltins ga

precs = mkPrecIntMap $ prec_annos newGa

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

ul <- mapAnM (anaBasicItem newGa) l

return $ BasicSpec ul

-- | analyse basic item

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

anaBasicItem ga (SigItems i) = fmap SigItems $ anaSigItems ga Loose i

anaBasicItem ga (ClassItems inst l ps) =

do ul <- mapAnM (anaClassItem ga inst) l

return $ ClassItems inst ul ps

anaBasicItem _ (GenVarItems l ps) =

do ul <- mapM (anaddGenVarDecl True) l

return $ GenVarItems (catMaybes ul) ps

anaBasicItem ga (ProgItems l ps) =

do ul <- mapAnMaybe (anaProgEq ga) l

return $ ProgItems ul ps

anaBasicItem _ (FreeDatatype l ps) =

do al <- mapAnMaybe ana1Datatype l

tys <- mapM (dataPatToType . item) al

ul <- mapAnMaybe (anaDatatype Free Plain tys) al

addDataSen tys

return $ FreeDatatype ul ps

anaBasicItem ga (GenItems l ps) =

do ul <- mapAnM (anaSigItems ga Generated) l

return $ GenItems ul ps

anaBasicItem ga (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

putTypeMap tm -- restore

putAssumps as -- restore

let newFs = catMaybes ts

newDs = catMaybes ds

sens = map ( \ f -> (emptyName $ Formula $ mkForall newDs

(item f) ps) { senName = getRLabel f })

newFs

appendSentences sens

return $ AxiomItems newDs newFs ps

anaBasicItem ga (Internal l ps) =

do ul <- mapAnM (anaBasicItem ga) l

return $ Internal ul ps

-- | quantify

mkForall :: [GenVarDecl] -> Term -> Range -> Term

mkForall _vs t _ps = t -- look for a minimal quantification

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

-- | analyse sig items

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

anaSigItems ga gk (TypeItems inst l ps) =

do ul <- anaTypeItems ga gk inst l

return $ TypeItems inst ul ps

anaSigItems ga _ (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