AsToLe.hs revision 5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : maeder@tzi.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : experimental
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederconversion from As to Le
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Rel as Rel
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Map as Map
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiimport qualified Common.Lib.Set as Set
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- * extract predicate ids from As for mixfix analysis
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiunite :: [Ids] -> Ids
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiidsOfBasicSpec :: BasicSpec -> Ids
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiidsOfBasicSpec (BasicSpec l) = unite $ map (idsOfBasicItem . item) l
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiidsOfBasicItem :: BasicItem -> Ids
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiidsOfBasicItem (SigItems i) = idsOfSigItems i
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidsOfBasicItem (ClassItems _ l _ ) = unite $ map (idsOfClassItem . item) l
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidsOfBasicItem (GenItems l _) = unite $ map (idsOfSigItems . item) l
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidsOfBasicItem (Internal l _) = unite $ map (idsOfBasicItem . item) l
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidsOfBasicItem _ = Set.empty
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiidsOfClassItem :: ClassItem -> Ids
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiidsOfClassItem (ClassItem _ l _) = unite $ map (idsOfBasicItem . item) l
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidsOfSigItems :: SigItems -> Ids
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidsOfSigItems (TypeItems _ _ _) = Set.empty
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiidsOfSigItems (OpItems b l _) = unite $ map (idsOfOpItem b . item) l
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiidsOfOpItem :: OpBrand -> OpItem -> Ids
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidsOfOpItem b (OpDecl os _ _ _) =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let ois = Set.fromList $ map ( \ (OpId i _ _) -> i) os
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskiidsOfOpItem b (OpDefn (OpId i _ _) _ _ _ _ _) =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- * basic analysis
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | basic analysis
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederbasicAnalysis :: (BasicSpec, Env, GlobalAnnos) ->
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Result (BasicSpec, Env, [Named Sentence])
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederbasicAnalysis (b, e, ga) =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder let (nb, ne) = runState (anaBasicSpec ga b) e
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder in Result (reverse $ envDiags ne) $
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Just (nb, cleanEnv ne, reverse $ sentences ne)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski-- | is the signature empty?
5e46b572ed576c0494768998b043d9d340594122Till MossakowskiisEmptyEnv :: Env -> Bool
5e46b572ed576c0494768998b043d9d340594122Till MossakowskiisEmptyEnv e = Map.null (classMap e)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder && Map.null (typeMap e)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder && Map.null (assumps e)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- | is the first argument a subsignature of the second?
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiisSubEnv :: Env -> Env -> Bool
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiisSubEnv e1 e2 = isEmptyEnv $ diffEnv e1 e2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- a rough equality
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance Eq Env where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski e1 == e2 = isSubEnv e1 e2 && isSubEnv e2 e1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | compute difference of signatures
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskidiffEnv :: Env -> Env -> Env
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederdiffEnv e1 e2 = let tm = typeMap e2 in
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder { classMap = Map.differenceWith diffClass (classMap e1) (classMap e2)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , typeMap = Map.differenceWith diffType (typeMap e1) tm
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , assumps = Map.differenceWith (diffAss $ addUnit tm)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (assumps e1) (assumps e2)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | compute difference of class infos
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederdiffClass :: ClassInfo -> ClassInfo -> Maybe ClassInfo
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederdiffClass _ _ = Nothing
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | compute difference of type infos
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskidiffType :: TypeInfo -> TypeInfo -> Maybe TypeInfo
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskidiffType _ _ = Nothing
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski-- | compute difference of overloaded operations
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskidiffAss :: TypeMap -> OpInfos -> OpInfos -> Maybe OpInfos
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskidiffAss tm (OpInfos l1) (OpInfos l2) =
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski let l3 = diffOps l1 l2 in
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski if null l3 then Nothing else Just (OpInfos l3)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski where diffOps [] _ = []
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski diffOps (o:os) ps =
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski let rs = diffOps os ps
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski n = mapOpInfo (id, expandAlias tm) o
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder in if any (instScheme tm 1 (opType n) . expand tm . opType) ps
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder then rs else n:rs
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | environment with predefined types and operations
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederaddPreDefs :: Env -> Env
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederaddPreDefs e = e { typeMap = addUnit $ typeMap e
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , assumps = addOps $ assumps e }
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- | environment with predefined types and operations
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederpreEnv = addPreDefs initialEnv
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | clean up finally accumulated environment
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercleanEnv :: Env -> Env
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercleanEnv e = diffEnv initialEnv
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder { classMap = classMap e
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , typeMap = typeMap e
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , assumps = assumps e }
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | analyse basic spec
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederanaBasicSpec :: GlobalAnnos -> BasicSpec -> State Env BasicSpec
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederanaBasicSpec ga b@(BasicSpec l) = do
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let newAs = assumps e
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder preds = Rel.keysSet $ Map.filter (any ( \ oi ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder case opDefn oi of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder NoOpDefn Pred -> True
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Definition Pred _ -> True
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder _ -> False) . opInfos) newAs
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder newPreds = idsOfBasicSpec b
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder rels = Set.union preds newPreds
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder newGa = addBuiltins ga
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder precs = mkPrecIntMap $ prec_annos newGa
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder put (addPreDefs e) { preIds = (precs, rels), globAnnos = newGa }
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ul <- mapAnM (anaBasicItem newGa) l
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ BasicSpec ul
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | analyse basic item
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederanaBasicItem :: GlobalAnnos -> BasicItem -> State Env BasicItem
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederanaBasicItem ga (SigItems i) = fmap SigItems $ anaSigItems ga Loose i
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederanaBasicItem ga (ClassItems inst l ps) =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do ul <- mapAnM (anaClassItem ga inst) l
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski return $ ClassItems inst ul ps
5e46b572ed576c0494768998b043d9d340594122Till MossakowskianaBasicItem _ (GenVarItems l ps) =
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski do ul <- mapM (anaddGenVarDecl True) l
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski return $ GenVarItems (catMaybes ul) ps
5e46b572ed576c0494768998b043d9d340594122Till MossakowskianaBasicItem ga (ProgItems l ps) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do ul <- mapAnMaybe (anaProgEq ga) l
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ ProgItems ul ps
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskianaBasicItem _ (FreeDatatype l ps) =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do al <- mapAnMaybe ana1Datatype l
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder tys <- mapM (dataPatToType . item) al
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder mapAnMaybe (anaDatatype Free Plain tys) al
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder addDataSen tys
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ FreeDatatype l ps
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederanaBasicItem ga (GenItems l ps) =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do ul <- mapAnM (anaSigItems ga Generated) l
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ GenItems ul ps
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederanaBasicItem ga (AxiomItems decls fs ps) =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do tm <- gets typeMap -- save type map
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski as <- gets assumps -- save vars
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ds <- mapM (anaddGenVarDecl True) decls
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ts <- mapM (anaFormula ga) fs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski putTypeMap tm -- restore
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder putAssumps as -- restore
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let newFs = catMaybes ts
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski newDs = catMaybes ds
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sens = map (( \ f -> (emptyName $ Formula $ mkForall newDs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (item f) ps) { senName = getRLabel f }) . snd)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski appendSentences sens
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return $ AxiomItems newDs (map fst newFs) ps
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskianaBasicItem ga (Internal l ps) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do ul <- mapAnM (anaBasicItem ga) l
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return $ Internal ul ps
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimkForall :: [GenVarDecl] -> Term -> Range -> Term
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimkForall _vs t _ps = t -- look for a minimal quantification
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- if null vs then t else QuantifiedTerm Universal vs t ps
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | analyse sig items
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskianaSigItems :: GlobalAnnos -> GenKind -> SigItems -> State Env SigItems
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederanaSigItems ga gk (TypeItems inst l ps) =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do ul <- anaTypeItems ga gk inst l
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ TypeItems inst ul ps
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskianaSigItems ga _ (OpItems b l ps) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do ul <- mapAnMaybe (anaOpItem ga b) l
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ OpItems b ul ps
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | analyse a class item
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskianaClassItem :: GlobalAnnos -> Instance -> ClassItem
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> State Env ClassItem
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskianaClassItem ga _ (ClassItem d l ps) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do cd <- anaClassDecls d
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ul <- mapAnM (anaBasicItem ga) l
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return $ ClassItem cd ul ps