{- |
Module : ./HasCASL/AsToLe.hs
Description : final static analysis
Copyright : (c) Christian Maeder and Uni Bremen 2003-2005
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : experimental
Portability : portable
conversion from As to Le
-}
module HasCASL.AsToLe where
import HasCASL.As
import HasCASL.Le
import HasCASL.ClassAna
import HasCASL.VarDecl
import HasCASL.Unify
import HasCASL.OpDecl
import HasCASL.TypeAna
import HasCASL.TypeDecl
import HasCASL.Builtin
import HasCASL.PrintLe
import HasCASL.Merge
import Common.AS_Annotation
import Common.GlobalAnnotations
import Common.Id
import Common.Result
import Common.ExtSign
import Common.Prec
import Common.Lib.State
import qualified Data.Map as Map
import qualified Data.Set as Set
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 (PolyId (Id ts _ ps) _ _) = Id ts [] ps
getPolyId (PolyId i _ _) = i
in case oi of
OpDecl os _ _ _ -> case b of
Pred -> Set.union (Set.fromList $ map getPolyId os) $ Set.fromList
$ map stripCompound os
_ -> Set.empty
OpDefn p _ _ _ _ -> case b of
Pred -> Set.fromList [getPolyId p, stripCompound p]
_ -> Set.empty
-- * basic analysis
-- | basic analysis
basicAnalysis :: (BasicSpec, Env, GlobalAnnos) ->
Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])
basicAnalysis (b, e, ga) =
let (nb, ne) = runState (anaBasicSpec ga b) e
in Result (reverse $ envDiags ne) $
Just (nb, ExtSign (cleanEnv ne) $ declSymbs ne,
reverse $ sentences ne)
-- | is the first argument a subsignature of the second?
isSubEnv :: Env -> Env -> Bool
isSubEnv e1 e2 =
let c2 = classMap e2
cm = addCpoMap c2
t2 = typeMap e2
tm = addUnit cm t2
expTy = expand tm . opType
in Map.isSubmapOfBy (\ (ClassInfo _ k1) (ClassInfo _ k2) ->
Set.null $ Set.filter
(\ k -> Set.null $ Set.filter (flip (lesserKind cm) k) k2) k1)
(classMap e1) c2
&& Map.isSubmapOfBy (\ ti1 ti2 -> let
k1 = otherTypeKinds ti1
k2 = otherTypeKinds ti2
in Set.null $ Set.filter (\ k -> Set.null $
Set.filter (flip (lesserKind cm) k) k2) k1)
(typeMap e1) (typeMap e2)
&& Map.isSubmapOfBy (\ s1 s2 ->
all (\ t -> any (instScheme tm 1 (expTy t) . expTy)
$ Set.toList s2)
$ Set.toList s1) (assumps e1) (assumps e2)
-- | compute difference of signatures
diffEnv :: Env -> Env -> Env
diffEnv e1 e2 = let
tm = typeMap e2
cm = diffClassMap (classMap e1) $ classMap e2
acm = addClassMap (classMap e1) $ classMap e2
in initialEnv
{ classMap = cm
, typeMap = diffTypeMap acm (typeMap e1) tm
, assumps = Map.differenceWith diffAss (assumps e1) $ assumps e2
, binders = Map.differenceWith
(\ i1 i2 -> if i1 == i2 then Nothing else Just i1)
(binders e1) $ binders e2 }
-- | compute difference of operations
diffAss :: Set.Set OpInfo -> Set.Set OpInfo
-> Maybe (Set.Set OpInfo)
diffAss s1 s2 =
let s3 = Set.difference s1 s2 in
if Set.null s3 then Nothing else Just s3
-- | clean up finally accumulated environment
cleanEnv :: Env -> Env
cleanEnv e = delPreDefs initialEnv
{ classMap = classMap e
, typeMap = typeMap e
, assumps = assumps e
, binders = binders e }
-- | 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 l
return $ BasicSpec ul
-- | analyse basic item
anaBasicItem :: BasicItem -> State Env BasicItem
anaBasicItem bi = case bi of
SigItems i -> fmap SigItems $ anaSigItems Loose i
ClassItems inst l ps -> do
ul <- mapAnM (anaClassItem 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 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 Generated) l
return $ GenItems ul ps
AxiomItems decls fs ps -> do
tm <- gets localTypeVars -- save type map
vs <- gets localVars -- save vars
ds <- mapM (anaddGenVarDecl True) decls
ts <- mapM anaFormula fs
e <- get
putLocalVars vs -- restore
putLocalTypeVars tm -- restore
let newFs = catMaybes ts
newDs = catMaybes ds
sens = map ( \ (_, f) -> makeNamedSen $ replaceAnnoted (Formula
$ mkEnvForall e (item f) ps) f) newFs
appendSentences sens
return $ AxiomItems newDs (map fst newFs) ps
Internal l ps -> do
ul <- mapAnM anaBasicItem l
return $ Internal ul ps
-- | analyse sig items
anaSigItems :: GenKind -> SigItems -> State Env SigItems
anaSigItems gk si = case si of
TypeItems inst l ps -> do
ul <- anaTypeItems gk l
return $ TypeItems inst ul ps
OpItems b l ps -> do
ul <- mapM (anaOpItem b) l
let al = foldr (\ i -> case item i of
Nothing -> id
Just v -> (replaceAnnoted v i :)) [] ul
return $ OpItems b al ps
-- | analyse a class item
anaClassItem :: Instance -> ClassItem -> State Env ClassItem
anaClassItem _ (ClassItem d l ps) = do
cd <- anaClassDecls d
ul <- mapAnM anaBasicItem l
return $ ClassItem cd ul ps