01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{- |

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$

1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2002-2003

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : hets@tzi.de

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiCASL static analysis for basic specifications

1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiFollows Chaps. III:2 and III:3 of the CASL Reference Manual.

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski-}

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskimodule CASL.StaticAna where

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport CASL.AS_Basic_CASL

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport CASL.Sign

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport CASL.MixfixParser

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport CASL.Overload

f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maederimport Common.Lib.State

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.PrettyPrint

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.Lib.Pretty

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Map as Map

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederimport qualified Common.Lib.Set as Set

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.Id

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.AS_Annotation

5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiimport Common.GlobalAnnotations

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport Common.Result

0c2a90cbfb63865ff485c3fbe20a14589a5914beTill Mossakowskiimport Data.Maybe

9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowskiimport Data.List

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicheckPlaces :: [SORT] -> Id -> [Diagnosis]

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicheckPlaces args i =

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if let n = placeCount i in n == 0 || n == length args then []

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder else [mkDiag Error "wrong number of places" i]

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiaddOp :: OpType -> Id -> State (Sign f e) ()

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiaddOp ty i =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do mapM_ checkSort (opRes ty : opArgs ty)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski e <- get

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let m = opMap e

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski l = Map.findWithDefault Set.empty i m

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski check = addDiags $ checkPlaces (opArgs ty) i

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski store = do put e { opMap = Map.insert i (Set.insert ty l) m }

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski if Set.member ty l then

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski addDiags [mkDiag Hint "redeclared op" i]

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else case opKind ty of

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Partial -> if Set.member ty {opKind = Total} l then

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski addDiags [mkDiag Warning "partially redeclared" i]

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else store >> check

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Total -> do store

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if Set.member ty {opKind = Partial} l then

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder addDiags [mkDiag Hint "redeclared as total" i]

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder else check

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiaddAssocOp :: OpType -> Id -> State (Sign f e) ()

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiaddAssocOp ty i = do

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder e <- get

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let m = assocOps e

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pty = ty { opKind = Partial } -- ignore FunKind

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski l = Map.findWithDefault Set.empty i m

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski put e { assocOps = Map.insert i (Set.insert pty l) m }

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederaddPred :: PredType -> Id -> State (Sign f e) ()

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederaddPred ty i =

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do mapM_ checkSort $ predArgs ty

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder e <- get

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski let m = predMap e

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski l = Map.findWithDefault Set.empty i m

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if Set.member ty l then

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder addDiags [mkDiag Hint "redeclared pred" i]

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder else do put e { predMap = Map.insert i (Set.insert ty l) m }

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder addDiags $ checkPlaces (predArgs ty) i

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederallOpIds :: State (Sign f e) (Set.Set Id)

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaederallOpIds = do

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder e <- get

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ Set.fromDistinctAscList $ Map.keys $ opMap e

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederaddAssocs :: GlobalAnnos -> State (Sign f e) GlobalAnnos

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederaddAssocs ga = do

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder e <- get

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder return ga { assoc_annos =

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder foldr ( \ i m -> case Map.lookup i m of

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Nothing -> Map.insert i ALeft m

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder _ -> m ) (assoc_annos ga) (Map.keys $ assocOps e) }

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski

5e46b572ed576c0494768998b043d9d340594122Till MossakowskiformulaIds :: State (Sign f e) (Set.Set Id)

5e46b572ed576c0494768998b043d9d340594122Till MossakowskiformulaIds = do

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder e <- get

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder ops <- allOpIds

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder return (Set.fromDistinctAscList (map simpleIdToId $ Map.keys $ varMap e)

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder `Set.union` ops)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederallPredIds :: State (Sign f e) (Set.Set Id)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederallPredIds = do

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder e <- get

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder return $ Set.fromDistinctAscList $ Map.keys $ predMap e

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederaddSentences :: [Named (FORMULA f)] -> State (Sign f e) ()

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederaddSentences ds =

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder do e <- get

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder put e { sentences = ds ++ sentences e }

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- * traversing all data types of the abstract syntax

10a2cf8d9887524acde19d4ea59f8fea3a7f3258Till Mossakowski

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiana_BASIC_SPEC :: (b -> e -> e) -> (s -> e -> e) ->

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski GlobalAnnos -> BASIC_SPEC b s f -> State (Sign f e) (BASIC_SPEC b s f)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiana_BASIC_SPEC ab as ga (Basic_spec al) = fmap Basic_spec $

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder mapAnM (ana_BASIC_ITEMS ab as ga) al

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- looseness of a datatype

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederdata GenKind = Free | Generated | Loose deriving (Show, Eq, Ord)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermkForall :: [VAR_DECL] -> FORMULA f -> [Pos] -> FORMULA f

4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedermkForall vl f ps = if null vl then f else

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Quantification Universal vl f ps

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maederana_BASIC_ITEMS :: (b -> e -> e) -> (s -> e -> e) ->

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder GlobalAnnos -> (BASIC_ITEMS b s f)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> State (Sign f e) (BASIC_ITEMS b s f)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederana_BASIC_ITEMS ab as ga bi =

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder case bi of

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Sig_items sis -> fmap Sig_items $ ana_SIG_ITEMS as ga Loose sis

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Free_datatype al ps ->

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski do let sorts = map (( \ (Datatype_decl s _ _) -> s) . item) al

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski mapM_ addSort sorts

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski mapAnM (ana_DATATYPE_DECL Free) al

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski toSortGenAx ps $ getDataGenSig al

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski closeSubsortRel

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski return bi

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Sort_gen al ps ->

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski do (gs,ul) <- ana_Generated as ga al

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski toSortGenAx ps (Set.unions $ map fst gs, Set.unions $ map snd gs)

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski return $ Sort_gen ul ps

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Var_items il _ ->

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do mapM_ addVars il

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return bi

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Local_var_axioms il afs ps ->

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do e <- get -- save

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder mapM_ addVars il

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ops <- formulaIds

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder put e -- restore

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder preds <- allPredIds

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder newGa <- addAssocs ga

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let rfs = map (resolveFormula newGa ops preds . item) afs

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ds = concatMap diags rfs

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder arfs = zipWith ( \ a m -> case maybeResult m of

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Nothing -> Nothing

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Just f -> Just a { item = f }) afs rfs

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ufs = catMaybes arfs

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder fufs = map ( \ a -> a { item = mkForall il

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (item a) ps } ) ufs

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sens = map ( \ a -> NamedSen (getRLabel a) $ item a) fufs

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski addDiags ds

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder addSentences sens

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ Local_var_axioms il ufs ps

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Axiom_items afs ps ->

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do ops <- formulaIds

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder preds <- allPredIds

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski newGa <- addAssocs ga

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder let rfs = map (resolveFormula newGa ops preds . item) afs

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder ds = concatMap diags rfs

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski arfs = zipWith ( \ a m -> case maybeResult m of

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder Nothing -> Nothing

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Just f -> Just a { item = f }) afs rfs

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski ufs = catMaybes arfs

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sens = map ( \ a -> NamedSen (getRLabel a) $ item a) ufs

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder addDiags ds

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder addSentences sens

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ Axiom_items ufs ps

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Ext_BASIC_ITEMS b -> do

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sig <- get

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder put sig { extendedInfo = ab b $ extendedInfo sig }

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return bi

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedertoSortGenAx :: [Pos] -> (Set.Set Id, Set.Set Component) -> State (Sign f e) ()

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskitoSortGenAx ps (sorts, ops) = do

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let sortList = Set.toList sorts

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski opSyms = map ( \ c -> Qual_op_name (compId c)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (toOP_TYPE $ compType c) []) $ Set.toList ops

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder resType _ (Op_name _) = False

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski resType s (Qual_op_name _ t _) = res_OP_TYPE t ==s

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski getIndex s = maybe (-1) id $ findIndex (==s) sortList

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski addIndices (Op_name _) =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski error "CASL/StaticAna: Internal error in function addIndices"

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski addIndices os@(Qual_op_name _ t _) =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (os,map getIndex $ args_OP_TYPE t)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski collectOps s =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Constraint s (map addIndices $ filter (resType s) opSyms) s

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski constrs = map collectOps sortList

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski f = Sort_gen_ax constrs

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski if null sortList then

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski addDiags[Diag Error "missing generated sort" (headPos ps)]

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else return ()

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski addSentences [NamedSen ("ga_generated_" ++

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski showSepList (showString "_") showId sortList "") f]

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiana_SIG_ITEMS :: (s -> e -> e) -> GlobalAnnos -> GenKind -> SIG_ITEMS s f

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> State (Sign f e) (SIG_ITEMS s f)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederana_SIG_ITEMS as ga gk si =

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder case si of

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Sort_items al ps ->

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do ul <- mapM (ana_SORT_ITEM ga) al

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski closeSubsortRel

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ Sort_items ul ps

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Op_items al ps ->

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do ul <- mapM (ana_OP_ITEM ga) al

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return $ Op_items ul ps

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Pred_items al ps ->

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do ul <- mapM (ana_PRED_ITEM ga) al

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return $ Pred_items ul ps

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Datatype_items al _ ->

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do let sorts = map (( \ (Datatype_decl s _ _) -> s) . item) al

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mapM_ addSort sorts

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mapAnM (ana_DATATYPE_DECL gk) al

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski closeSubsortRel

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return si

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Ext_SIG_ITEMS s ->

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do sig <- get

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski put sig { extendedInfo = as s $ extendedInfo sig }

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return si

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- helper

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiana_Generated :: (s -> e -> e) -> GlobalAnnos -> [Annoted (SIG_ITEMS s f)]

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> State (Sign f e)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ([(Set.Set Id, Set.Set Component)],[Annoted (SIG_ITEMS s f)])

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiana_Generated as ga al = do

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ul <- mapAnM (ana_SIG_ITEMS as ga Generated) al

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (map (getGenSig . item) ul,ul)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskigetGenSig :: SIG_ITEMS s f -> (Set.Set Id, Set.Set Component)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskigetGenSig si = case si of

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Sort_items al _ -> (Set.unions (map (getSorts . item) al), Set.empty)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Op_items al _ -> (Set.empty, Set.unions (map (getOps . item) al))

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Datatype_items dl _ -> getDataGenSig dl

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski _ -> (Set.empty, Set.empty)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskigetDataGenSig :: [Annoted DATATYPE_DECL] -> (Set.Set Id, Set.Set Component)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskigetDataGenSig dl =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let alts = map (( \ (Datatype_decl s al _) -> (s, al)) . item) dl

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sorts = map fst alts

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder cs = concatMap ( \ (s, al) -> map (( \ a ->

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder let (i, ty, _) = getConsType s a

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder in Component i ty))

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder $ filter ( \ a ->

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case a of

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Subsorts _ _ -> False

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski _ -> True)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $ map item al) alts

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski in (Set.fromList sorts, Set.fromList cs)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedergetSorts :: SORT_ITEM f -> Set.Set Id

4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedergetSorts si =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case si of

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder Sort_decl il _ -> Set.fromList il

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Subsort_decl il i _ -> Set.fromList (i:il)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Subsort_defn sub _ _ _ _ -> Set.single sub

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Iso_decl il _ -> Set.fromList il

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder

612749008484b6773aedf4d6bbc85b8d074d15c6Christian MaedergetOps :: OP_ITEM f -> Set.Set Component

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskigetOps oi = case oi of

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder Op_decl is ty _ _ ->

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder Set.fromList $ map ( \ i -> Component i $ toOpType ty) is

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Op_defn i par _ _ -> Set.single $ Component i $ toOpType $ headToType par

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maederana_SORT_ITEM :: GlobalAnnos -> Annoted (SORT_ITEM f)

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder -> State (Sign f e) (Annoted (SORT_ITEM f))

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maederana_SORT_ITEM ga asi =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case item asi of

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder Sort_decl il _ ->

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do mapM_ addSort il

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return asi

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder Subsort_decl il i _ ->

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder do mapM_ addSort (i:il)

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder mapM_ (addSubsort i) il

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder return asi

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Subsort_defn sub v super af ps ->

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do ops <- allOpIds

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder preds <- allPredIds

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder newGa <- addAssocs ga

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let Result ds mf = resolveFormula newGa

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Set.insert (simpleIdToId v) ops) preds $ item af

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder lb = getRLabel af

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski lab = if null lb then getRLabel asi else lb

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski addDiags ds

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder addSort sub

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder addSubsort super sub

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case mf of

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder Nothing -> return asi { item = Subsort_decl [sub] super ps}

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Just f -> do

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let p = [posOfId sub]

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder pv = [tokPos v]

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder addSentences[NamedSen lab $

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder mkForall [Var_decl [v] super pv]

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (Equivalence

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (Membership (Qual_var v super pv) sub p)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder f p) p]

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder return asi { item = Subsort_defn sub v super af { item = f } ps}

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Iso_decl il _ ->

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder do mapM_ addSort il

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder mapM_ ( \ i -> mapM_ (addSubsort i) il) il

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder return asi

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederana_OP_ITEM :: GlobalAnnos -> Annoted (OP_ITEM f)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder -> State (Sign f e) (Annoted (OP_ITEM f))

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederana_OP_ITEM ga aoi =

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder case item aoi of

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Op_decl ops ty il ps ->

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do let oty = toOpType ty

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder mapM_ (addOp oty) ops

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ul <- mapM (ana_OP_ATTR ga oty ops) il

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski if null $ filter ( \ i -> case i of

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Assoc_op_attr -> True

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder _ -> False) il

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder then return ()

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder else mapM_ (addAssocOp oty) ops

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return aoi {item = Op_decl ops ty (catMaybes ul) ps}

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Op_defn i par at ps ->

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder do let ty = headToType par

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski lb = getRLabel at

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski lab = if null lb then getRLabel aoi else lb

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder args = case par of

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Total_op_head as _ _ -> as

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Partial_op_head as _ _ -> as

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder vs = map (\ (Arg_decl v s qs) -> (Var_decl v s qs)) args

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder arg = concatMap ( \ (Var_decl v s qs) ->

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder map ( \ j -> Qual_var j s qs) v) vs

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder addOp (toOpType ty) i

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ops <- allOpIds

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder preds <- allPredIds

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski newGa <- addAssocs ga

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski let vars = concatMap ( \ (Arg_decl v _ _) -> v) args

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder allOps = foldr ( \ v s -> Set.insert (simpleIdToId v) s)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ops vars

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Result ds mt = resolveMixfix newGa allOps preds False $ item at

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder addDiags ds

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder case mt of

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Nothing -> return aoi { item = Op_decl [i] ty [] ps }

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Just t -> do let p = [posOfId i]

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder addSentences [NamedSen lab $

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder mkForall vs

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (Strong_equation

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (Application (Qual_op_name i ty p) arg ps)

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski t p) ps]

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder return aoi {item = Op_defn i par at { item = t } ps }

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski

5e46b572ed576c0494768998b043d9d340594122Till MossakowskiheadToType :: OP_HEAD -> OP_TYPE

5e46b572ed576c0494768998b043d9d340594122Till MossakowskiheadToType (Total_op_head args r ps) =

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Total_op_type (sortsOfArgs args) r ps

5e46b572ed576c0494768998b043d9d340594122Till MossakowskiheadToType (Partial_op_head args r ps) =

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Partial_op_type (sortsOfArgs args) r ps

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski

5e46b572ed576c0494768998b043d9d340594122Till MossakowskisortsOfArgs :: [ARG_DECL] -> [SORT]

5e46b572ed576c0494768998b043d9d340594122Till MossakowskisortsOfArgs = concatMap ( \ (Arg_decl l s _) -> map (const s) l)

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski

5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiana_OP_ATTR :: GlobalAnnos -> OpType -> [Id] -> (OP_ATTR f)

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -> State (Sign f e) (Maybe (OP_ATTR f))

5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiana_OP_ATTR ga ty ois oa =

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski let sty = toOP_TYPE ty

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski rty = opRes ty

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder q = [posOfId rty] in

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski case oa of

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Unit_op_attr t ->

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski do ops <- allOpIds

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski preds <- allPredIds

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski newGa <- addAssocs ga

a938729e277da5c7742bb88946ab2c150416fd5dTill Mossakowski let Result ds mt = resolveMixfix newGa ops preds False t

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski addDiags ds

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski case mt of

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Nothing -> return Nothing

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Just e -> do

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski addSentences $ map (makeUnit True e ty) ois

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski addSentences $ map (makeUnit False e ty) ois

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski return $ Just $ Unit_op_attr e

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Assoc_op_attr -> do

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski let ns = map mkSimpleId ["x", "y", "z"]

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski vs = map ( \ v -> Var_decl [v] rty q) ns

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski [v1, v2, v3] = map ( \ v -> Qual_var v rty q) ns

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski makeAssoc i = let p = [posOfId i]

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski qi = Qual_op_name i sty p in

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski NamedSen ("ga_assoc_" ++ showId i "") $

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski mkForall vs

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (Strong_equation

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (Application qi [v1, Application qi [v2, v3] p] p)

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (Application qi [Application qi [v1, v2] p, v3] p) p) p

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski addSentences $ map makeAssoc ois

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski return $ Just oa

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Comm_op_attr -> do

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski let ns = map mkSimpleId ["x", "y"]

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski atys = opArgs ty

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski vs = zipWith ( \ v t -> Var_decl [v] t (map posOfId atys) ) ns atys

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski args = map toQualVar vs

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder makeComm i = let p = [posOfId i]

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder qi = Qual_op_name i sty p in

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder NamedSen ("ga_comm_" ++ showId i "") $

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mkForall vs

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder (Strong_equation

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder (Application qi args p)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (Application qi (reverse args) p) p) p

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder case atys of

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder [_,_] -> addSentences $ map makeComm ois

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski _ -> addDiags [Diag Error "expecting two arguments for commutativity"

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $ posOfId rty]

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder return $ Just oa

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Idem_op_attr -> do

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder let v = mkSimpleId "x"

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder vd = Var_decl [v] rty q

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder qv = toQualVar vd

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder makeIdem i = let p = [posOfId i] in

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder NamedSen ("ga_idem_" ++ showId i "") $

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder mkForall [vd]

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (Strong_equation

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (Application (Qual_op_name i sty p) [qv, qv] p)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder qv p) p

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder addSentences $ map makeIdem ois

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder return $ Just oa

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermakeUnit :: Bool -> TERM f -> OpType -> Id -> Named (FORMULA f)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermakeUnit b t ty i =

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let lab = "ga_" ++ (if b then "right" else "left") ++ "_unit_"

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ++ showId i ""

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder v = mkSimpleId "x"

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder vty = opRes ty

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder q = [posOfId vty]

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder p = [posOfId i]

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder qv = Qual_var v vty q

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder args = [qv, t]

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder rargs = if b then args else reverse args

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski in NamedSen lab $ mkForall [Var_decl [v] vty q]

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (Strong_equation

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (Application (Qual_op_name i (toOP_TYPE ty) p) rargs p)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder qv p) p

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederana_PRED_ITEM :: GlobalAnnos -> Annoted (PRED_ITEM f)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> State (Sign f e) (Annoted (PRED_ITEM f))

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederana_PRED_ITEM ga ap =

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder case item ap of

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Pred_decl preds ty _ ->

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder do mapM (addPred $ toPredType ty) preds

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder return ap

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Pred_defn i par at ps ->

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder do let Pred_head args rs = par

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski lb = getRLabel at

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder lab = if null lb then getRLabel ap else lb

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ty = Pred_type (sortsOfArgs args) rs

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski vs = map (\ (Arg_decl v s qs) -> (Var_decl v s qs)) args

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder arg = concatMap ( \ (Var_decl v s qs) ->

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder map ( \ j -> Qual_var j s qs) v) vs

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski addPred (toPredType ty) i

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ops <- allOpIds

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder preds <- allPredIds

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski newGa <- addAssocs ga

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder let vars = concatMap ( \ (Arg_decl v _ _) -> v) args

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder allOps = foldr ( \ v s -> Set.insert (simpleIdToId v) s)

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder ops vars

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Result ds mt = resolveFormula newGa allOps preds $ item at

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski addDiags ds

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case mt of

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> return ap {item = Pred_decl [i] ty ps}

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just t -> do

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let p = [posOfId i]

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder addSentences [NamedSen lab $

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mkForall vs

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Equivalence (Predication (Qual_pred_name i ty p)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski arg p) t p) p]

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return ap {item = Pred_defn i par at { item = t } ps}

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- full function type of a selector (result sort is component sort)

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maederdata Component = Component { compId :: Id, compType :: OpType }

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski deriving (Show)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederinstance Eq Component where

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Component i1 t1 == Component i2 t2 =

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (i1, opArgs t1, opRes t1) == (i2, opArgs t2, opRes t2)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance Ord Component where

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Component i1 t1 <= Component i2 t2 =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (i1, opArgs t1, opRes t1) <= (i2, opArgs t2, opRes t2)

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder

612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maederinstance PrettyPrint Component where

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski printText0 ga (Component i ty) =

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder printText0 ga i <+> colon <> printText0 ga ty

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder

cdee35b1b16886e4f341e2a2a69fa0e6be30b3faTill Mossakowskiinstance PosItem Component where

cdee35b1b16886e4f341e2a2a69fa0e6be30b3faTill Mossakowski get_pos = Just . posOfId . compId

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | return list of constructors

cdee35b1b16886e4f341e2a2a69fa0e6be30b3faTill Mossakowskiana_DATATYPE_DECL :: GenKind -> DATATYPE_DECL -> State (Sign f e) [Component]

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederana_DATATYPE_DECL gk (Datatype_decl s al _) =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do ul <- mapM (ana_ALTERNATIVE s . item) al

cdee35b1b16886e4f341e2a2a69fa0e6be30b3faTill Mossakowski let constr = catMaybes ul

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder cs = map fst constr

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder if null constr then return ()

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder else do addDiags $ checkUniqueness cs

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let totalSels = Set.unions $ map snd constr

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder wrongConstr = filter ((totalSels /=) . snd) constr

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder addDiags $ map ( \ (c, _) -> mkDiag Error

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ("total selectors '" ++ showSepList (showString ",")

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder showPretty (Set.toList totalSels)

cdee35b1b16886e4f341e2a2a69fa0e6be30b3faTill Mossakowski "'\n\tmust appear in alternative") c) wrongConstr

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder case gk of

cdee35b1b16886e4f341e2a2a69fa0e6be30b3faTill Mossakowski Free -> do

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let allts = map item al

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (alts, subs) = partition ( \ a -> case a of

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Subsorts _ _ -> False

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder _ -> True) allts

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder sbs = concatMap ( \ (Subsorts ss _) -> ss) subs

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder comps = map (getConsType s) alts

cdee35b1b16886e4f341e2a2a69fa0e6be30b3faTill Mossakowski ttrips = map (( \ (a, vs, t, ses) -> (a, vs, t, catSels ses))

cdee35b1b16886e4f341e2a2a69fa0e6be30b3faTill Mossakowski . selForms1 "X" ) comps

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder sels = concatMap ( \ (_, _, _, ses) -> ses) ttrips

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder addSentences $ map makeInjective

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder $ filter ( \ (_, _, ces) -> not $ null ces)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder comps

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder addSentences $ concatMap ( \ as -> map (makeDisjToSort as) sbs)

comps

addSentences $ makeDisjoint comps

addSentences $ catMaybes $ concatMap

( \ ses ->

map (makeUndefForm ses) ttrips) sels

_ -> return ()

return cs

makeDisjToSort :: (Id, OpType, [COMPONENTS]) -> SORT -> Named (FORMULA f)

makeDisjToSort a s =

let (c, v, t, _) = selForms1 "X" a

p = [posOfId s] in

NamedSen ("ga_disjoint_" ++ showId c "_sort_" ++ showId s "") $

mkForall v (Negation (Membership t s p) p) p

makeInjective :: (Id, OpType, [COMPONENTS]) -> Named (FORMULA f)

makeInjective a =

let (c, v1, t1, _) = selForms1 "X" a

(_, v2, t2, _) = selForms1 "Y" a

p = [posOfId c]

in NamedSen ("ga_injective_" ++ showId c "") $

mkForall (v1 ++ v2)

(Equivalence (Strong_equation t1 t2 p)

(let ces = zipWith ( \ w1 w2 -> Strong_equation

(toQualVar w1) (toQualVar w2) p) v1 v2

in if isSingle ces then head ces else Conjunction ces p)

p) p

makeDisjoint :: [(Id, OpType, [COMPONENTS])] -> [Named (FORMULA f)]

makeDisjoint [] = []

makeDisjoint (a:as) = map (makeDisj a) as ++ makeDisjoint as

makeDisj :: (Id, OpType, [COMPONENTS])

-> (Id, OpType, [COMPONENTS])

-> Named (FORMULA f)

makeDisj a1 a2 =

let (c1, v1, t1, _) = selForms1 "X" a1

(c2, v2, t2, _) = selForms1 "Y" a2

p = [posOfId c1, posOfId c2]

in NamedSen ("ga_disjoint_" ++ showId c1 "_" ++ showId c2 "") $

mkForall (v1 ++ v2)

(Negation (Strong_equation t1 t2 p) p) p

catSels :: [(Maybe Id, OpType)] -> [(Id, OpType)]

catSels = map ( \ (m, t) -> (fromJust m, t)) .

filter ( \ (m, _) -> isJust m)

makeUndefForm :: (Id, OpType) -> (Id, [VAR_DECL], TERM f, [(Id, OpType)])

-> Maybe (Named (FORMULA f))

makeUndefForm (s, ty) (i, vs, t, sels) =

let p = [posOfId s] in

if any ( \ (se, ts) -> s == se && opRes ts == opRes ty ) sels

then Nothing else

Just $ NamedSen ("ga_selector_undef_" ++ showId s "_"

++ showId i "") $

mkForall vs

(Negation

(Definedness

(Application (Qual_op_name s (toOP_TYPE ty) p) [t] p)

p) p) p

getConsType :: SORT -> ALTERNATIVE -> (Id, OpType, [COMPONENTS])

getConsType s c =

let (part, i, il) = case c of

Subsorts _ _ -> error "getConsType"

Total_construct a l _ -> (Total, a, l)

Partial_construct a l _ -> (Partial, a, l)

in (i, OpType part (concatMap

(map (opRes . snd) . getCompType s) il) s, il)

getCompType :: SORT -> COMPONENTS -> [(Maybe Id, OpType)]

getCompType s (Total_select l cs _) =

map (\ i -> (Just i, OpType Total [s] cs)) l

getCompType s (Partial_select l cs _) =

map (\ i -> (Just i, OpType Partial [s] cs)) l

getCompType s (Sort cs) = [(Nothing, OpType Partial [s] cs)]

genSelVars :: String -> Int -> [(Maybe Id, OpType)] -> [VAR_DECL]

genSelVars _ _ [] = []

genSelVars str n ((_, ty):rs) =

Var_decl [mkSelVar str n] (opRes ty) [] : genSelVars str (n+1) rs

mkSelVar :: String -> Int -> Token

mkSelVar str n = mkSimpleId (str ++ show n)

makeSelForms :: Int -> (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)])

-> [Named (FORMULA f)]

makeSelForms _ (_, _, _, []) = []

makeSelForms n (i, vs, t, (mi, ty):rs) =

(case mi of

Nothing -> []

Just j -> let p = [posOfId j]

rty = opRes ty

q = [posOfId rty] in

[NamedSen ("ga_selector_" ++ showId j "")

$ mkForall vs

(Strong_equation

(Application (Qual_op_name j (toOP_TYPE ty) p) [t] p)

(Qual_var (mkSelVar "X" n) rty q) p) p]

) ++ makeSelForms (n+1) (i, vs, t, rs)

selForms1 :: String -> (Id, OpType, [COMPONENTS])

-> (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)])

selForms1 str (i, ty, il) =

let cs = concatMap (getCompType $ opRes ty) il

vs = genSelVars str 1 cs

in (i, vs, Application (Qual_op_name i (toOP_TYPE ty) [])

(map toQualVar vs) [], cs)

toQualVar :: VAR_DECL -> TERM f

toQualVar (Var_decl v s ps) =

if isSingle v then Qual_var (head v) s ps else error "toQualVar"

selForms :: (Id, OpType, [COMPONENTS]) -> [Named (FORMULA f)]

selForms = makeSelForms 1 . selForms1 "X"

-- | return the constructor and the set of total selectors

ana_ALTERNATIVE :: SORT -> ALTERNATIVE

-> State (Sign f e) (Maybe (Component, Set.Set Component))

ana_ALTERNATIVE s c =

case c of

Subsorts ss _ ->

do mapM_ (addSubsort s) ss

return Nothing

_ -> do let cons@(i, ty, il) = getConsType s c

addOp ty i

ul <- mapM (ana_COMPONENTS s) il

let ts = concatMap fst ul

addDiags $ checkUniqueness (ts ++ concatMap snd ul)

addSentences $ selForms cons

return $ Just (Component i ty, Set.fromList ts)

-- | return total and partial selectors

ana_COMPONENTS :: SORT -> COMPONENTS

-> State (Sign f e) ([Component], [Component])

ana_COMPONENTS s c = do

let cs = getCompType s c

sels <- mapM ( \ (mi, ty) ->

case mi of

Nothing -> return Nothing

Just i -> do addOp ty i

return $ Just $ Component i ty) cs

return $ partition ((==Total) . opKind . compType) $ catMaybes sels

-- wrap it all up for a logic

basicAnalysis :: PrettyPrint f => (b -> e -> e)

-> (s -> e -> e) -> (f -> Result f)

->(BASIC_SPEC b s f, Sign f e, GlobalAnnos)

-> Result (BASIC_SPEC b s f, Sign f e, Sign f e, [Named (FORMULA f)])

basicAnalysis ab as af (bs, inSig, ga) = do

let (newBs, accSig) = runState (ana_BASIC_SPEC ab as ga bs) inSig

ds = reverse $ envDiags accSig

sents = reverse $ sentences accSig

cleanSig = accSig { envDiags = [], sentences = [], varMap = Map.empty }

diff = diffSig cleanSig inSig

remPartOpsS s = s { opMap = remPartOpsM $ opMap s }

checked_sents <- overloadResolution af accSig sents

Result ds (Just ()) -- insert diags

return ( newBs

, remPartOpsS diff

, remPartOpsS cleanSig

, reverse checked_sents )