content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./HolLight/Sign.hs
  Description :  HolLight signature
  Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  jonathan.von_schroeder@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  -}
  
  module HolLight.Sign where
  
  import Data.Typeable
  import qualified Data.Map as Map
  import Common.DocUtils
  import Common.Doc
  import Common.Result
  import HolLight.Term
  import HolLight.Helper
  
  data Sign = Sign { types :: Map.Map String Int
                   , ops :: Map.Map String HolType }
    deriving (Eq, Ord, Show, Typeable)
  
  prettyTypes :: Map.Map String Int -> Doc
  prettyTypes = ppMap text (\ i -> if i < 1 then empty else parens (pretty i))
    (const id) sepByCommas (<>)
  
  instance Pretty Sign where
    pretty s = keyword "types" <+> prettyTypes (types s)
      $++$ ppMap text ppPrintType
           (const id) vcat (\ a -> ((a <+> colon) <+>)) (ops s)
  
  emptySig :: Sign
  emptySig = Sign {types = Map.empty, ops = Map.empty }
  
  isSubSig :: Sign -> Sign -> Bool
  isSubSig s1 s2 = types s1 `Map.isSubmapOf` types s2
    && ops s1 `Map.isSubmapOf` ops s2
  
  sigUnion :: Sign -> Sign -> Result Sign
  sigUnion (Sign {types = t1, ops = o1})
           (Sign {types = t2, ops = o2}) =
    return Sign {types = t1 `Map.union` t2, ops = o1 `Map.union` o2}
  