Sign.hs revision 1a38107941725211e7c3f051f7a8f5e12199f03a
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{-# LANGUAGE DeriveDataTypeable #-}
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederModule : $Header$
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederDescription : HolLight signature
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : jonathan.von_schroeder@dfki.de
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederStability : experimental
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : portable
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederimport qualified Data.Map as Map
68d10d143f29fcff3c637ba24f90e983995ceae6Christian Maederdata Sign = Sign { types :: Map.Map String Int
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder , ops :: Map.Map String HolType }
01e383014b555bbcf639c0ca60c5810b3eff83c0Christian Maeder deriving (Eq, Ord, Show, Typeable)
9dac90ec2be2a72e03893095461960d483fe2fc2Christian MaederprettyTypes :: Map.Map String Int -> Doc
5e5d3e82af3bc2834f8718a52d9f45da80220273Dominik LueckeprettyTypes = ppMap text (\ i -> if i < 1 then empty else parens (pretty i))
124c859ba4741d5e36d5d98634886b430b7af093Christian Maeder (const id) sepByCommas (<>)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederinstance Pretty Sign where
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder pretty s = keyword "types" <+> prettyTypes (types s)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder $++$ ppMap text ppPrintType
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (const id) vcat (\ a -> (a <+> colon <+>)) (ops s)
c0c2380bced8159ff0297ece14eba948bd236471Christian MaederemptySig :: Sign
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus LuettichemptySig = Sign {types = Map.empty, ops = Map.empty }
ad270004874ce1d0697fb30d7309f180553bb315Christian MaederisSubSig :: Sign -> Sign -> Bool
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian MaederisSubSig s1 s2 = types s1 `Map.isSubmapOf` types s2
4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder && ops s1 `Map.isSubmapOf` ops s2
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus LuettichsigUnion :: Sign -> Sign -> Result Sign
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedersigUnion (Sign {types = t1, ops = o1})
74eed04be26f549d2f7ca35c370e1c03879b28b1Christian Maeder (Sign {types = t2, ops = o2}) =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder return Sign {types = t1 `Map.union` t2, ops = o1 `Map.union` o2}