{- |

Module : $Header$

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