{-# 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 { Sign -> Map String Int
types :: Map.Map String Int
                 , Sign -> Map String HolType
ops :: Map.Map String HolType }
  deriving (Sign -> Sign -> Bool
(Sign -> Sign -> Bool) -> (Sign -> Sign -> Bool) -> Eq Sign
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sign -> Sign -> Bool
$c/= :: Sign -> Sign -> Bool
== :: Sign -> Sign -> Bool
$c== :: Sign -> Sign -> Bool
Eq, Eq Sign
Eq Sign =>
(Sign -> Sign -> Ordering)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Sign)
-> (Sign -> Sign -> Sign)
-> Ord Sign
Sign -> Sign -> Bool
Sign -> Sign -> Ordering
Sign -> Sign -> Sign
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Sign -> Sign -> Sign
$cmin :: Sign -> Sign -> Sign
max :: Sign -> Sign -> Sign
$cmax :: Sign -> Sign -> Sign
>= :: Sign -> Sign -> Bool
$c>= :: Sign -> Sign -> Bool
> :: Sign -> Sign -> Bool
$c> :: Sign -> Sign -> Bool
<= :: Sign -> Sign -> Bool
$c<= :: Sign -> Sign -> Bool
< :: Sign -> Sign -> Bool
$c< :: Sign -> Sign -> Bool
compare :: Sign -> Sign -> Ordering
$ccompare :: Sign -> Sign -> Ordering
$cp1Ord :: Eq Sign
Ord, Int -> Sign -> ShowS
[Sign] -> ShowS
Sign -> String
(Int -> Sign -> ShowS)
-> (Sign -> String) -> ([Sign] -> ShowS) -> Show Sign
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sign] -> ShowS
$cshowList :: [Sign] -> ShowS
show :: Sign -> String
$cshow :: Sign -> String
showsPrec :: Int -> Sign -> ShowS
$cshowsPrec :: Int -> Sign -> ShowS
Show, Typeable)

prettyTypes :: Map.Map String Int -> Doc
prettyTypes :: Map String Int -> Doc
prettyTypes = (String -> Doc)
-> (Int -> Doc)
-> (CSize -> Doc -> Doc)
-> ([Doc] -> Doc)
-> (Doc -> Doc -> Doc)
-> Map String Int
-> Doc
forall a b.
(a -> Doc)
-> (b -> Doc)
-> (CSize -> Doc -> Doc)
-> ([Doc] -> Doc)
-> (Doc -> Doc -> Doc)
-> Map a b
-> Doc
ppMap String -> Doc
text (\ i :: Int
i -> if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 then Doc
empty else Doc -> Doc
parens (Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
i))
  ((Doc -> Doc) -> CSize -> Doc -> Doc
forall a b. a -> b -> a
const Doc -> Doc
forall a. a -> a
id) [Doc] -> Doc
sepByCommas Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
(<>)

instance Pretty Sign where
  pretty :: Sign -> Doc
pretty s :: Sign
s = String -> Doc
keyword "types" Doc -> Doc -> Doc
<+> Map String Int -> Doc
prettyTypes (Sign -> Map String Int
types Sign
s)
    Doc -> Doc -> Doc
$++$ (String -> Doc)
-> (HolType -> Doc)
-> (CSize -> Doc -> Doc)
-> ([Doc] -> Doc)
-> (Doc -> Doc -> Doc)
-> Map String HolType
-> Doc
forall a b.
(a -> Doc)
-> (b -> Doc)
-> (CSize -> Doc -> Doc)
-> ([Doc] -> Doc)
-> (Doc -> Doc -> Doc)
-> Map a b
-> Doc
ppMap String -> Doc
text HolType -> Doc
ppPrintType
         ((Doc -> Doc) -> CSize -> Doc -> Doc
forall a b. a -> b -> a
const Doc -> Doc
forall a. a -> a
id) [Doc] -> Doc
vcat (\ a :: Doc
a -> ((Doc
a Doc -> Doc -> Doc
<+> Doc
colon) Doc -> Doc -> Doc
<+>)) (Sign -> Map String HolType
ops Sign
s)

emptySig :: Sign
emptySig :: Sign
emptySig = Sign :: Map String Int -> Map String HolType -> Sign
Sign {types :: Map String Int
types = Map String Int
forall k a. Map k a
Map.empty, ops :: Map String HolType
ops = Map String HolType
forall k a. Map k a
Map.empty }

isSubSig :: Sign -> Sign -> Bool
isSubSig :: Sign -> Sign -> Bool
isSubSig s1 :: Sign
s1 s2 :: Sign
s2 = Sign -> Map String Int
types Sign
s1 Map String Int -> Map String Int -> Bool
forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
`Map.isSubmapOf` Sign -> Map String Int
types Sign
s2
  Bool -> Bool -> Bool
&& Sign -> Map String HolType
ops Sign
s1 Map String HolType -> Map String HolType -> Bool
forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
`Map.isSubmapOf` Sign -> Map String HolType
ops Sign
s2

sigUnion :: Sign -> Sign -> Result Sign
sigUnion :: Sign -> Sign -> Result Sign
sigUnion (Sign {types :: Sign -> Map String Int
types = Map String Int
t1, ops :: Sign -> Map String HolType
ops = Map String HolType
o1})
         (Sign {types :: Sign -> Map String Int
types = Map String Int
t2, ops :: Sign -> Map String HolType
ops = Map String HolType
o2}) =
  Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return Sign :: Map String Int -> Map String HolType -> Sign
Sign {types :: Map String Int
types = Map String Int
t1 Map String Int -> Map String Int -> Map String Int
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map String Int
t2, ops :: Map String HolType
ops = Map String HolType
o1 Map String HolType -> Map String HolType -> Map String HolType
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map String HolType
o2}