Sign.hs revision 902bfaac7e88afebb6684fe1f2414ae2efbc7edf
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingModule : $Header$
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingDescription : Signatures for Maude
b99dbaab171d91e1b664397cc40e039d0c087c65fieldingCopyright : (c) Martin Kuehl, Uni Bremen 2008
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingMaintainer : mkhl@informatik.uni-bremen.de
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingStability : experimental
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingPortability : portable
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingDefinition of signatures for Maude.
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding insertSort,
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding insertSubsort,
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding insertOpName,
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding includesSentence,
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport Data.Typeable (Typeable)
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport qualified Data.Foldable as Fold
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport qualified Data.Set as Set
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingimport qualified Data.Map as Map
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport qualified Common.Lib.Rel as Rel
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding-- for ShATermConvertible
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding-- for Pretty
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport Common.DocUtils (Pretty(..))
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingimport qualified Common.Doc as Doc
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingtype SubsortRel = Rel.Rel Sort
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingtype OpMap = Map.Map Symbol OpDeclSet
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingdata Sign = Sign {
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding sorts :: SortSet,
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding subsorts :: SubsortRel,
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding ops :: OpMap
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding } deriving (Show, Eq, Typeable)
3568de757bac0b47256647504c186d17ca272f85rbb-- TODO: Add real pretty-printing for Maude Signatures.
3568de757bac0b47256647504c186d17ca272f85rbbinstance Pretty Sign where
3568de757bac0b47256647504c186d17ca272f85rbb-- TODO: Replace dummy implementation for ShATermConvertible Sign.
3568de757bac0b47256647504c186d17ca272f85rbbinstance ShATermConvertible Sign where
3568de757bac0b47256647504c186d17ca272f85rbb toShATermAux table _ = return (table, 0)
3568de757bac0b47256647504c186d17ca272f85rbb fromShATermAux _ table = (table, empty)
3568de757bac0b47256647504c186d17ca272f85rbbinstance HasSorts Sign where
3568de757bac0b47256647504c186d17ca272f85rbb getSorts = sorts
3568de757bac0b47256647504c186d17ca272f85rbb mapSorts mp sign = sign {
3568de757bac0b47256647504c186d17ca272f85rbb sorts = mapSorts mp (sorts sign),
3568de757bac0b47256647504c186d17ca272f85rbb subsorts = mapSorts mp (subsorts sign)
3568de757bac0b47256647504c186d17ca272f85rbbinstance HasOps Sign where
3568de757bac0b47256647504c186d17ca272f85rbb getOps = Map.keysSet . ops
3568de757bac0b47256647504c186d17ca272f85rbb mapOps mp sign = sign {
3568de757bac0b47256647504c186d17ca272f85rbbinstance HasLabels Sign where
3568de757bac0b47256647504c186d17ca272f85rbb getLabels = getLabels . Map.elems . ops
3568de757bac0b47256647504c186d17ca272f85rbb mapLabels mp sign = sign {
3568de757bac0b47256647504c186d17ca272f85rbb ops = Map.map (mapLabels mp) (ops sign)
3568de757bac0b47256647504c186d17ca272f85rbb-- | extract the Signature of a Module
3568de757bac0b47256647504c186d17ca272f85rbbfromMod :: (Module a) => a -> Sign
3568de757bac0b47256647504c186d17ca272f85rbbfromMod modul = let
3568de757bac0b47256647504c186d17ca272f85rbb mk'subsorts = Rel.transClosure . Set.fold ins'subsort Rel.empty
3568de757bac0b47256647504c186d17ca272f85rbb sorts = modSorts modul,
3568de757bac0b47256647504c186d17ca272f85rbb subsorts = mk'subsorts (modSubsorts modul),
3568de757bac0b47256647504c186d17ca272f85rbb ops = mk'ops (modOps modul)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding-- | extract the Set of all Symbols from a Signature
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingsymbols :: Sign -> SymbolSet
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingsymbols sign = Set.unions [(getSorts sign), (getOps sign), (getLabels sign)]
3568de757bac0b47256647504c186d17ca272f85rbb-- | the empty Signature
3568de757bac0b47256647504c186d17ca272f85rbbempty :: Sign
3568de757bac0b47256647504c186d17ca272f85rbbempty = Sign { sorts = Set.empty, subsorts = Rel.empty, ops = Map.empty }
3568de757bac0b47256647504c186d17ca272f85rbb-- | insert a Sort into a Signature
db12cd62083041bf90945eeb90cc40fbd2340797trawickinsertSort :: Sort -> Sign -> Sign
db12cd62083041bf90945eeb90cc40fbd2340797trawickinsertSort sort sign = sign {sorts = ins'sort sort (sorts sign)}
333eac96e4fb7d6901cb75e6ca7bb22b2ccb84cetrawick-- | insert a Subsort declaration into a Signature
333eac96e4fb7d6901cb75e6ca7bb22b2ccb84cetrawickinsertSubsort :: SubsortDecl -> Sign -> Sign
3568de757bac0b47256647504c186d17ca272f85rbbinsertSubsort decl sign = sign {subsorts = ins'subsort decl (subsorts sign)}
3568de757bac0b47256647504c186d17ca272f85rbb-- | insert an Operator name into a Signature
3568de757bac0b47256647504c186d17ca272f85rbbinsertOpName :: Symbol -> Sign -> Sign
3568de757bac0b47256647504c186d17ca272f85rbbinsertOpName name sign = sign {ops = ins'opName name (ops sign)}
3568de757bac0b47256647504c186d17ca272f85rbb-- | insert an Operator declaration into a Signature
3568de757bac0b47256647504c186d17ca272f85rbbinsertOp :: OpDecl -> Sign -> Sign
3568de757bac0b47256647504c186d17ca272f85rbbinsertOp op sign = sign {ops = ins'op op (ops sign)}
3568de757bac0b47256647504c186d17ca272f85rbb-- | check that a Signature is legal
3568de757bac0b47256647504c186d17ca272f85rbbisLegal :: Sign -> Bool
3568de757bac0b47256647504c186d17ca272f85rbbisLegal sign = let
3568de757bac0b47256647504c186d17ca272f85rbb isLegalType typ = case typ of
3568de757bac0b47256647504c186d17ca272f85rbb Kind kind -> not $ null kind && all isLegalSort kind
3568de757bac0b47256647504c186d17ca272f85rbb -- TODO: Check that all sorts are in the same connected component.
3568de757bac0b47256647504c186d17ca272f85rbb Sort sort -> isLegalSort sort
3568de757bac0b47256647504c186d17ca272f85rbb isLegalSort sort = Set.member sort (sorts sign)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding isLegalOp op = isLegalType (op'domain op) && all isLegalType (op'range op)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding legal'subsorts = Fold.all isLegalSort $ Rel.nodes (subsorts sign)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding legal'ops = Fold.all (Fold.all isLegalOp) (ops sign)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding in all id [legal'subsorts, legal'ops]
8f3ec4772d2aeb347cf40e87c77627bb784dd018rbb-- | check that a Signature can include a Sentence
8f3ec4772d2aeb347cf40e87c77627bb784dd018rbbincludesSentence :: Sign -> Sentence -> Bool
3d96ee83babeec32482c9082c9426340cee8c44dwrowe-- includesSentence sign sen = True
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingincludesSentence sign sen = let
3568de757bac0b47256647504c186d17ca272f85rbb ops'subset = Set.isSubsetOf (getOps sen) (getOps sign)
3568de757bac0b47256647504c186d17ca272f85rbb sorts'subset = Set.isSubsetOf (getSorts sen) (getSorts sign)
3568de757bac0b47256647504c186d17ca272f85rbb labels'subset = Set.isSubsetOf (getLabels sen) (getLabels sign)
3568de757bac0b47256647504c186d17ca272f85rbb in all id [sorts'subset, ops'subset, labels'subset]
3568de757bac0b47256647504c186d17ca272f85rbb--- Helper functions for inserting Signature members into their respective collections.
3568de757bac0b47256647504c186d17ca272f85rbb-- insert a Sort into a Set of Sorts
3568de757bac0b47256647504c186d17ca272f85rbbins'sort :: Sort -> SortSet -> SortSet
3568de757bac0b47256647504c186d17ca272f85rbbins'sort sort set = Set.insert sort set
3568de757bac0b47256647504c186d17ca272f85rbb-- insert a Subsort declaration into a Subsort Relationship
3568de757bac0b47256647504c186d17ca272f85rbbins'subsort :: SubsortDecl -> SubsortRel -> SubsortRel
3568de757bac0b47256647504c186d17ca272f85rbbins'subsort sub rel = Rel.insert (subsort sub) (supersort sub) rel
3568de757bac0b47256647504c186d17ca272f85rbb-- insert an Operator name into an Operator Map
3568de757bac0b47256647504c186d17ca272f85rbbins'opName :: Symbol -> OpMap -> OpMap
3568de757bac0b47256647504c186d17ca272f85rbb-- insert an Operator declaration into an Operator Map
3568de757bac0b47256647504c186d17ca272f85rbbins'op :: OpDecl -> OpMap -> OpMap
3568de757bac0b47256647504c186d17ca272f85rbbins'op op opmap = let
3568de757bac0b47256647504c186d17ca272f85rbb name = op'name op
3568de757bac0b47256647504c186d17ca272f85rbb new'ops = Set.insert op old'ops
3568de757bac0b47256647504c186d17ca272f85rbb in Map.insert name new'ops opmap
3568de757bac0b47256647504c186d17ca272f85rbb-- map an OperatorMap key-value pair and insert it into the accumulator
3568de757bac0b47256647504c186d17ca272f85rbbmap'op :: SymbolMap -> Symbol -> OpDeclSet -> OpMap -> OpMap
3568de757bac0b47256647504c186d17ca272f85rbbmap'op mp op decls acc = let
3568de757bac0b47256647504c186d17ca272f85rbb key = mapToFunction mp op
3568de757bac0b47256647504c186d17ca272f85rbb val = mapOps mp decls
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding in Map.insert key val acc
3568de757bac0b47256647504c186d17ca272f85rbbmapToFunction :: (Ord a) => Map.Map a a -> (a -> a)
3568de757bac0b47256647504c186d17ca272f85rbbmapToFunction mp name = Map.findWithDefault name name mp