{- |
Module      :  ./HasCASL/PrintLe.hs
Description :  pretty printing signatures
Copyright   :  (c) Christian Maeder, Uni Bremen, DFKI GmbH 2002-2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

pretty printing a HasCASL environment
-}

module HasCASL.PrintLe
  ( diffClass
  , diffClassMap
  , mergeClassInfo
  , mergeClassMap
  , addClassMap
  , addCpoMap
  , minimizeClassMap
  , mergeMap
  , improveDiag
  , diffTypeMap
  , diffType
  , printMap1
  , mostSyms
  , delPreDefs
  ) where

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.PrintAs
import HasCASL.Le
import HasCASL.Builtin
import HasCASL.ClassAna

import Common.AS_Annotation
import Common.Doc
import Common.DocUtils
import Common.Id
import qualified Data.Map as Map
import qualified Data.Set as Set
import Common.Keywords
import Common.Result

import Control.Monad (foldM)
import Data.List
import Data.Maybe

instance Pretty ClassInfo where
    pretty :: ClassInfo -> Doc
pretty (ClassInfo rk :: RawKind
rk ks :: Set Kind
ks) = Doc
less Doc -> Doc -> Doc
<+>
        if Set Kind -> Bool
forall a. Set a -> Bool
Set.null Set Kind
ks then Kind -> Doc
forall a. Pretty a => a -> Doc
pretty (RawKind -> Kind
rawToKind RawKind
rk) else
        [Kind] -> Doc
forall a. Pretty a => [a] -> Doc
printList0 (Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList Set Kind
ks)

printGenKind :: GenKind -> Doc
printGenKind :: GenKind -> Doc
printGenKind k :: GenKind
k = case GenKind
k of
    Loose -> Doc
empty
    Free -> String -> Doc
text String
freeS
    Generated -> String -> Doc
text String
generatedS

instance Pretty TypeDefn where
    pretty :: TypeDefn -> Doc
pretty td :: TypeDefn
td = case TypeDefn
td of
        NoTypeDefn -> Doc
empty
        PreDatatype -> String -> Doc
text "%(data type)%"
        AliasTypeDefn s :: Type
s -> String -> Doc
text String
assignS Doc -> Doc -> Doc
<+> Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
s
        DatatypeDefn dd :: DataEntry
dd -> String -> Doc
text "%[" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> DataEntry -> Doc
forall a. Pretty a => a -> Doc
pretty DataEntry
dd Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "]%"

printAltDefn :: AltDefn -> Doc
printAltDefn :: AltDefn -> Doc
printAltDefn (Construct mi :: Maybe Id
mi ts :: [Type]
ts p :: Partiality
p sels :: [[Selector]]
sels) = case Maybe Id
mi of
    Just i :: Id
i -> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep (([Selector] -> Doc) -> [[Selector]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
parens (Doc -> Doc) -> ([Selector] -> Doc) -> [Selector] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Selector] -> Doc
forall a. Pretty a => [a] -> Doc
semiDs) [[Selector]]
sels) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Partiality -> Doc
forall a. Pretty a => a -> Doc
pretty Partiality
p
    Nothing -> String -> Doc
text (String
typeS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS) Doc -> Doc -> Doc
<+> [Type] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [Type]
ts

instance Pretty Selector where
    pretty :: Selector -> Doc
pretty (Select mi :: Maybe Id
mi t :: Type
t p :: Partiality
p) = let d :: Doc
d = Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
t in case Maybe Id
mi of
        Just i :: Id
i -> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i Doc -> Doc -> Doc
<+> case Partiality
p of
            Partial -> String -> Doc
text String
colonQuMark
               Doc -> Doc -> Doc
<+> if Type -> Bool
isSimpleType Type
t then Doc
d else Doc -> Doc
parens Doc
d
            Total -> Doc
colon
               Doc -> Doc -> Doc
<+> if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "?" (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show Doc
d then Doc -> Doc
parens Doc
d else Doc
d
        Nothing -> Doc
d

instance Pretty TypeInfo where
    pretty :: TypeInfo -> Doc
pretty (TypeInfo _ _ _ def :: TypeDefn
def) = TypeDefn -> Doc
forall a. Pretty a => a -> Doc
pretty TypeDefn
def

instance Pretty TypeVarDefn where
    pretty :: TypeVarDefn -> Doc
pretty (TypeVarDefn v :: Variance
v vk :: VarKind
vk _ i :: Int
i) =
        Variance -> VarKind -> Doc
printVarKind Variance
v VarKind
vk Doc -> Doc -> Doc
<+> String -> Doc
text ("%(var_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
forall a. Show a => a -> String -> String
shows Int
i ")%")

instance Pretty VarDefn where
    pretty :: VarDefn -> Doc
pretty (VarDefn ty :: Type
ty) =
        Doc
colon Doc -> Doc -> Doc
<+> Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
ty

instance Pretty ConstrInfo where
    pretty :: ConstrInfo -> Doc
pretty (ConstrInfo i :: Id
i t :: TypeScheme
t) =
        Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> TypeScheme -> Doc
forall a. Pretty a => a -> Doc
pretty TypeScheme
t

instance Pretty OpDefn where
    pretty :: OpDefn -> Doc
pretty od :: OpDefn
od = case OpDefn
od of
        NoOpDefn _ -> Doc
empty
        ConstructData _ -> String -> Doc
text "%(constructor)%"
        SelectData cs :: Set ConstrInfo
cs _ -> [Doc] -> Doc
sep
            [ String -> Doc
text "%(selector of constructor(s)"
            , [ConstrInfo] -> Doc
forall a. Pretty a => [a] -> Doc
printList0 (Set ConstrInfo -> [ConstrInfo]
forall a. Set a -> [a]
Set.toList Set ConstrInfo
cs) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text ")%" ]
        Definition b :: OpBrand
b t :: Term
t ->
            [Doc] -> Doc
sep [String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ "%[ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ if OpBrand -> Bool
isPred OpBrand
b then "<=>" else "="
                , Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
t Doc -> Doc -> Doc
<+> String -> Doc
text "]%" ]

isOpDefn :: OpBrand -> OpDefn -> Bool
isOpDefn :: OpBrand -> OpDefn -> Bool
isOpDefn b :: OpBrand
b od :: OpDefn
od = case OpDefn
od of
  NoOpDefn c :: OpBrand
c -> OpBrand
c OpBrand -> OpBrand -> Bool
forall a. Eq a => a -> a -> Bool
== OpBrand
b
  Definition c :: OpBrand
c _ -> OpBrand
c OpBrand -> OpBrand -> Bool
forall a. Eq a => a -> a -> Bool
== OpBrand
b
  _ -> Bool
False

isPredOpDefn :: OpDefn -> Bool
isPredOpDefn :: OpDefn -> Bool
isPredOpDefn = OpBrand -> OpDefn -> Bool
isOpDefn OpBrand
Pred

isFunOpDefn :: OpDefn -> Bool
isFunOpDefn :: OpDefn -> Bool
isFunOpDefn = OpBrand -> OpDefn -> Bool
isOpDefn OpBrand
Fun

instance Pretty OpInfo where
    pretty :: OpInfo -> Doc
pretty o :: OpInfo
o = let od :: OpDefn
od = OpInfo -> OpDefn
opDefn OpInfo
o in
      [Doc] -> Doc
sep [TypeScheme -> Doc
forall a. Pretty a => a -> Doc
pretty (TypeScheme -> Doc) -> TypeScheme -> Doc
forall a b. (a -> b) -> a -> b
$ (if OpDefn -> Bool
isPredOpDefn OpDefn
od then TypeScheme -> TypeScheme
unPredTypeScheme else TypeScheme -> TypeScheme
forall a. a -> a
id)
          (TypeScheme -> TypeScheme) -> TypeScheme -> TypeScheme
forall a b. (a -> b) -> a -> b
$ OpInfo -> TypeScheme
opType OpInfo
o, OpDefn -> Doc
forall a. Pretty a => a -> Doc
pretty OpDefn
od]

instance Pretty DataEntry where
    pretty :: DataEntry -> Doc
pretty (DataEntry im :: IdMap
im j :: Id
j k :: GenKind
k args :: [TypeArg]
args _ talts :: Set AltDefn
talts) = let
        i :: Id
i = Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
j Id
j IdMap
im
        mapAlt :: AltDefn -> AltDefn
mapAlt (Construct mi :: Maybe Id
mi tys :: [Type]
tys p :: Partiality
p sels :: [[Selector]]
sels) = Maybe Id -> [Type] -> Partiality -> [[Selector]] -> AltDefn
Construct Maybe Id
mi
          ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (IdMap -> Type -> Type
mapType IdMap
im) [Type]
tys) Partiality
p ([[Selector]] -> AltDefn) -> [[Selector]] -> AltDefn
forall a b. (a -> b) -> a -> b
$ ([Selector] -> [Selector]) -> [[Selector]] -> [[Selector]]
forall a b. (a -> b) -> [a] -> [b]
map ((Selector -> Selector) -> [Selector] -> [Selector]
forall a b. (a -> b) -> [a] -> [b]
map Selector -> Selector
mapSel) [[Selector]]
sels
        mapSel :: Selector -> Selector
mapSel (Select mi :: Maybe Id
mi ty :: Type
ty p :: Partiality
p) = Maybe Id -> Type -> Partiality -> Selector
Select Maybe Id
mi (IdMap -> Type -> Type
mapType IdMap
im Type
ty) Partiality
p
        alts :: Set AltDefn
alts = (AltDefn -> AltDefn) -> Set AltDefn -> Set AltDefn
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map AltDefn -> AltDefn
mapAlt Set AltDefn
talts
        in GenKind -> Doc
printGenKind GenKind
k Doc -> Doc -> Doc
<+> String -> Doc
keyword String
typeS Doc -> Doc -> Doc
<+>
           [Doc] -> Doc
fsep [[Doc] -> Doc
fcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (TypeArg -> Doc) -> [TypeArg] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
parens (Doc -> Doc) -> (TypeArg -> Doc) -> TypeArg -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeArg -> Doc
forall a. Pretty a => a -> Doc
pretty) [TypeArg]
args
                , Doc
defn, [Doc] -> Doc
cat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate (Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
bar Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
space)
                ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (AltDefn -> Doc) -> [AltDefn] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map AltDefn -> Doc
printAltDefn ([AltDefn] -> [Doc]) -> [AltDefn] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Set AltDefn -> [AltDefn]
forall a. Set a -> [a]
Set.toList Set AltDefn
alts]

instance Pretty Sentence where
    pretty :: Sentence -> Doc
pretty s :: Sentence
s = case Sentence
s of
        Formula t :: Term
t -> (case Term
t of
          QuantifiedTerm Universal (_ : _) _ _ -> Doc -> Doc
forall a. a -> a
id
          _ -> Doc -> Doc
addBullet) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
t
        DatatypeSen ls :: [DataEntry]
ls -> [Doc] -> Doc
vcat ((DataEntry -> Doc) -> [DataEntry] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map DataEntry -> Doc
forall a. Pretty a => a -> Doc
pretty [DataEntry]
ls)
        ProgEqSen _ _ pe :: ProgEq
pe -> String -> Doc
keyword String
programS Doc -> Doc -> Doc
<+> ProgEq -> Doc
forall a. Pretty a => a -> Doc
pretty ProgEq
pe

delPreDefs :: Env -> Env
delPreDefs :: Env -> Env
delPreDefs e :: Env
e =
  let cm :: ClassMap
cm = Env -> ClassMap
classMap Env
e
      tm :: TypeMap
tm = Env -> TypeMap
typeMap Env
e
      ops :: Assumps
ops = Env -> Assumps
assumps Env
e
      ocm :: ClassMap
ocm = ClassMap -> ClassMap -> ClassMap
diffClassMap ClassMap
cm ClassMap
cpoMap
  in Env
e
  { classMap :: ClassMap
classMap = ClassMap
ocm
  , typeMap :: TypeMap
typeMap = ClassMap -> TypeMap -> TypeMap -> TypeMap
diffTypeMap ClassMap
ocm TypeMap
tm TypeMap
bTypes
  , assumps :: Assumps
assumps = ((Id, TypeScheme) -> Assumps -> Assumps)
-> Assumps -> [(Id, TypeScheme)] -> Assumps
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Id -> Assumps -> Assumps
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (Id -> Assumps -> Assumps)
-> ((Id, TypeScheme) -> Id)
-> (Id, TypeScheme)
-> Assumps
-> Assumps
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, TypeScheme) -> Id
forall a b. (a, b) -> a
fst) Assumps
ops [(Id, TypeScheme)]
bList }

getSuperClasses :: ClassMap -> [(Id, Kind)]
getSuperClasses :: ClassMap -> [(Id, Kind)]
getSuperClasses = ((Id, ClassInfo) -> [(Id, Kind)])
-> [(Id, ClassInfo)] -> [(Id, Kind)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
  ( \ (i :: Id
i, ci :: ClassInfo
ci) -> (Kind -> (Id, Kind)) -> [Kind] -> [(Id, Kind)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ s :: Kind
s -> (Id
i, Kind
s))
    ([Kind] -> [(Id, Kind)])
-> (Set Kind -> [Kind]) -> Set Kind -> [(Id, Kind)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList (Set Kind -> [(Id, Kind)]) -> Set Kind -> [(Id, Kind)]
forall a b. (a -> b) -> a -> b
$ Kind -> Set Kind -> Set Kind
forall a. Ord a => a -> Set a -> Set a
Set.delete (RawKind -> Kind
rawToKind (RawKind -> Kind) -> RawKind -> Kind
forall a b. (a -> b) -> a -> b
$ ClassInfo -> RawKind
rawKind ClassInfo
ci) (Set Kind -> Set Kind) -> Set Kind -> Set Kind
forall a b. (a -> b) -> a -> b
$ ClassInfo -> Set Kind
classKinds ClassInfo
ci)
  ([(Id, ClassInfo)] -> [(Id, Kind)])
-> (ClassMap -> [(Id, ClassInfo)]) -> ClassMap -> [(Id, Kind)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClassMap -> [(Id, ClassInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList

getSuperTypes :: TypeMap -> [(Id, Id)]
getSuperTypes :: TypeMap -> [(Id, Id)]
getSuperTypes = ((Id, TypeInfo) -> [(Id, Id)]) -> [(Id, TypeInfo)] -> [(Id, Id)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
  ( \ (i :: Id
i, ti :: TypeInfo
ti) -> (Id -> (Id, Id)) -> [Id] -> [(Id, Id)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ s :: Id
s -> (Id
i, Id
s))
    ([Id] -> [(Id, Id)]) -> (Set Id -> [Id]) -> Set Id -> [(Id, Id)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Set Id -> [(Id, Id)]) -> Set Id -> [(Id, Id)]
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Set Id
superTypes TypeInfo
ti)
  ([(Id, TypeInfo)] -> [(Id, Id)])
-> (TypeMap -> [(Id, TypeInfo)]) -> TypeMap -> [(Id, Id)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeMap -> [(Id, TypeInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList

getTypeKinds :: TypeMap -> [(Id, Kind)]
getTypeKinds :: TypeMap -> [(Id, Kind)]
getTypeKinds = ((Id, TypeInfo) -> [(Id, Kind)])
-> [(Id, TypeInfo)] -> [(Id, Kind)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
  ( \ (i :: Id
i, ti :: TypeInfo
ti) -> (Kind -> (Id, Kind)) -> [Kind] -> [(Id, Kind)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ k :: Kind
k -> (Id
i, Kind
k))
    ([Kind] -> [(Id, Kind)])
-> (Set Kind -> [Kind]) -> Set Kind -> [(Id, Kind)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList (Set Kind -> [(Id, Kind)]) -> Set Kind -> [(Id, Kind)]
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Set Kind
otherTypeKinds TypeInfo
ti)
  ([(Id, TypeInfo)] -> [(Id, Kind)])
-> (TypeMap -> [(Id, TypeInfo)]) -> TypeMap -> [(Id, Kind)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeMap -> [(Id, TypeInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList

getTypeAliases :: TypeMap -> [(Id, Type)]
getTypeAliases :: TypeMap -> [(Id, Type)]
getTypeAliases = ((Id, TypeInfo) -> [(Id, Type)] -> [(Id, Type)])
-> [(Id, Type)] -> [(Id, TypeInfo)] -> [(Id, Type)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
  ( \ (i :: Id
i, td :: TypeInfo
td) -> case TypeInfo -> TypeDefn
typeDefn TypeInfo
td of
    AliasTypeDefn ty :: Type
ty -> ((Id
i, Type
ty) (Id, Type) -> [(Id, Type)] -> [(Id, Type)]
forall a. a -> [a] -> [a]
:)
    _ -> [(Id, Type)] -> [(Id, Type)]
forall a. a -> a
id) [] ([(Id, TypeInfo)] -> [(Id, Type)])
-> (TypeMap -> [(Id, TypeInfo)]) -> TypeMap -> [(Id, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeMap -> [(Id, TypeInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList

instance Pretty Env where
    pretty :: Env -> Doc
pretty env :: Env
env = let
      d :: Env
d = Env -> Env
delPreDefs Env
env
      cm :: ClassMap
cm = Env -> ClassMap
classMap Env
d
      tm :: TypeMap
tm = Env -> TypeMap
typeMap Env
d
      tvs :: LocalTypeVars
tvs = Env -> LocalTypeVars
localTypeVars Env
d
      vs :: Map Id VarDefn
vs = Env -> Map Id VarDefn
localVars Env
d
      poMap :: Map Id (Set OpInfo, Set OpInfo)
poMap = (Set OpInfo -> (Set OpInfo, Set OpInfo))
-> Assumps -> Map Id (Set OpInfo, Set OpInfo)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((OpInfo -> Bool) -> Set OpInfo -> (Set OpInfo, Set OpInfo)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (OpDefn -> Bool
isPredOpDefn (OpDefn -> Bool) -> (OpInfo -> OpDefn) -> OpInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpInfo -> OpDefn
opDefn)) (Assumps -> Map Id (Set OpInfo, Set OpInfo))
-> Assumps -> Map Id (Set OpInfo, Set OpInfo)
forall a b. (a -> b) -> a -> b
$ Env -> Assumps
assumps Env
d
      pMap :: Assumps
pMap = ((Set OpInfo, Set OpInfo) -> Set OpInfo)
-> Map Id (Set OpInfo, Set OpInfo) -> Assumps
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Set OpInfo, Set OpInfo) -> Set OpInfo
forall a b. (a, b) -> a
fst Map Id (Set OpInfo, Set OpInfo)
poMap
      aoMap :: Assumps
aoMap = ((Set OpInfo, Set OpInfo) -> Set OpInfo)
-> Map Id (Set OpInfo, Set OpInfo) -> Assumps
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Set OpInfo, Set OpInfo) -> Set OpInfo
forall a b. (a, b) -> b
snd Map Id (Set OpInfo, Set OpInfo)
poMap
      foMap :: Map Id (Set OpInfo, Set OpInfo)
foMap = (Set OpInfo -> (Set OpInfo, Set OpInfo))
-> Assumps -> Map Id (Set OpInfo, Set OpInfo)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((OpInfo -> Bool) -> Set OpInfo -> (Set OpInfo, Set OpInfo)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (OpDefn -> Bool
isFunOpDefn (OpDefn -> Bool) -> (OpInfo -> OpDefn) -> OpInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpInfo -> OpDefn
opDefn)) Assumps
aoMap
      fMap :: Assumps
fMap = ((Set OpInfo, Set OpInfo) -> Set OpInfo)
-> Map Id (Set OpInfo, Set OpInfo) -> Assumps
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Set OpInfo, Set OpInfo) -> Set OpInfo
forall a b. (a, b) -> a
fst Map Id (Set OpInfo, Set OpInfo)
foMap
      oMap :: Assumps
oMap = ((Set OpInfo, Set OpInfo) -> Set OpInfo)
-> Map Id (Set OpInfo, Set OpInfo) -> Assumps
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Set OpInfo, Set OpInfo) -> Set OpInfo
forall a b. (a, b) -> b
snd Map Id (Set OpInfo, Set OpInfo)
foMap
      ltm :: [(Id, Kind)]
ltm = TypeMap -> [(Id, Kind)]
getTypeKinds TypeMap
tm
      stm :: [(Id, Id)]
stm = TypeMap -> [(Id, Id)]
getSuperTypes TypeMap
tm
      atm :: [(Id, Type)]
atm = TypeMap -> [(Id, Type)]
getTypeAliases TypeMap
tm
      scm :: [(Id, Kind)]
scm = ClassMap -> [(Id, Kind)]
getSuperClasses ClassMap
cm
      bas :: [Annotation]
bas = ((Id, Id) -> Annotation) -> [(Id, Id)] -> [Annotation]
forall a b. (a -> b) -> [a] -> [b]
map (\ (b :: Id
b, o :: Id
o) -> Annote_word -> Annote_text -> Range -> Annotation
Unparsed_anno (String -> Annote_word
Annote_word "binder")
             (String -> Annote_text
Line_anno (String -> Annote_text) -> String -> Annote_text
forall a b. (a -> b) -> a -> b
$ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ ", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
o) (Range -> Annotation) -> Range -> Annotation
forall a b. (a -> b) -> a -> b
$ Id -> Range
posOfId Id
b)
            ([(Id, Id)] -> [Annotation]) -> [(Id, Id)] -> [Annotation]
forall a b. (a -> b) -> a -> b
$ IdMap -> [(Id, Id)]
forall k a. Map k a -> [(k, a)]
Map.toList (IdMap -> [(Id, Id)]) -> IdMap -> [(Id, Id)]
forall a b. (a -> b) -> a -> b
$ Env -> IdMap
binders Env
d
      mkPlural :: String -> String
mkPlural s :: String
s = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ if String -> Char
forall a. [a] -> a
last String
s Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== 's' then "es" else "s"
      header2 :: [a] -> String -> Doc
header2 l :: [a]
l s :: String
s = String -> Doc
keyword (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ case [a]
l of
        _ : _ : _ -> String -> String
mkPlural String
s
        _ -> String
s
      header :: Map k a -> String -> Doc
header m :: Map k a
m s :: String
s = String -> Doc
keyword (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
        if Map k a -> Int
forall k a. Map k a -> Int
Map.size Map k a
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 2 then String
s else String -> String
mkPlural String
s
      in Bool -> Doc -> Doc
noPrint (ClassMap -> Bool
forall k a. Map k a -> Bool
Map.null ClassMap
cm) (ClassMap -> String -> Doc
forall k a. Map k a -> String -> Doc
header ClassMap
cm String
classS)
        Doc -> Doc -> Doc
$+$ ClassMap -> Doc
forall a b. (Pretty a, Ord a, Pretty b) => Map a b -> Doc
printMap0 ((ClassInfo -> ClassInfo) -> ClassMap -> ClassMap
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ( \ ci :: ClassInfo
ci -> ClassInfo
ci { classKinds :: Set Kind
classKinds = Set Kind
forall a. Set a
Set.empty }) ClassMap
cm)
        Doc -> Doc -> Doc
$+$ Bool -> Doc -> Doc
noPrint ([(Id, Kind)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Id, Kind)]
scm) ([(Id, Kind)] -> String -> Doc
forall a. [a] -> String -> Doc
header2 [(Id, Kind)]
scm String
classS)
        Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat (Doc -> [Doc] -> [Doc]
punctuate Doc
semi ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ ((Id, Kind) -> Doc) -> [(Id, Kind)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: Id
i, s :: Kind
s) ->
            Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i Doc -> Doc -> Doc
<+> String -> Doc
text String
lessS Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. Pretty a => a -> Doc
pretty Kind
s) [(Id, Kind)]
scm)
        Doc -> Doc -> Doc
$+$ Bool -> Doc -> Doc
noPrint ([(Id, Kind)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Id, Kind)]
ltm) ([(Id, Kind)] -> String -> Doc
forall a. [a] -> String -> Doc
header2 [(Id, Kind)]
ltm String
typeS)
        Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat (Doc -> [Doc] -> [Doc]
punctuate Doc
semi ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ ((Id, Kind) -> Doc) -> [(Id, Kind)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: Id
i, k :: Kind
k) ->
            Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. Pretty a => a -> Doc
pretty Kind
k) [(Id, Kind)]
ltm)
        Doc -> Doc -> Doc
$+$ Bool -> Doc -> Doc
noPrint ([(Id, Id)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Id, Id)]
stm) ([(Id, Id)] -> String -> Doc
forall a. [a] -> String -> Doc
header2 [(Id, Id)]
stm String
typeS)
        Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat (Doc -> [Doc] -> [Doc]
punctuate Doc
semi ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ ((Id, Id) -> Doc) -> [(Id, Id)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: Id
i, s :: Id
s) ->
            Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i Doc -> Doc -> Doc
<+> String -> Doc
text String
lessS Doc -> Doc -> Doc
<+> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
s) [(Id, Id)]
stm)
        Doc -> Doc -> Doc
$+$ Bool -> Doc -> Doc
noPrint ([(Id, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Id, Type)]
atm) ([(Id, Type)] -> String -> Doc
forall a. [a] -> String -> Doc
header2 [(Id, Type)]
atm String
typeS)
        Doc -> Doc -> Doc
$+$ [(Id, Type)] -> Doc
printAliasTypes [(Id, Type)]
atm
        Doc -> Doc -> Doc
$+$ Bool -> Doc -> Doc
noPrint (LocalTypeVars -> Bool
forall k a. Map k a -> Bool
Map.null LocalTypeVars
tvs) (LocalTypeVars -> String -> Doc
forall k a. Map k a -> String -> Doc
header LocalTypeVars
tvs String
varS)
        Doc -> Doc -> Doc
$+$ LocalTypeVars -> Doc
forall a b. (Pretty a, Ord a, Pretty b) => Map a b -> Doc
printMap0 LocalTypeVars
tvs
        Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ((Annotation -> Doc) -> [Annotation] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Annotation -> Doc
annoDoc [Annotation]
bas)
        Doc -> Doc -> Doc
$+$ Doc -> Doc -> Assumps -> Doc
forall k a.
(Pretty k, Pretty a) =>
Doc -> Doc -> Map k (Set a) -> Doc
printSetMap (String -> Doc
keyword String
opS) Doc
space Assumps
oMap
        Doc -> Doc -> Doc
$+$ Doc -> Doc -> Assumps -> Doc
forall k a.
(Pretty k, Pretty a) =>
Doc -> Doc -> Map k (Set a) -> Doc
printSetMap (String -> Doc
keyword String
predS) Doc
space Assumps
pMap
        Doc -> Doc -> Doc
$+$ Doc -> Doc -> Assumps -> Doc
forall k a.
(Pretty k, Pretty a) =>
Doc -> Doc -> Map k (Set a) -> Doc
printSetMap (String -> Doc
keyword String
functS) Doc
space Assumps
fMap
        Doc -> Doc -> Doc
$+$ Bool -> Doc -> Doc
noPrint (Map Id VarDefn -> Bool
forall k a. Map k a -> Bool
Map.null Map Id VarDefn
vs) (Map Id VarDefn -> String -> Doc
forall k a. Map k a -> String -> Doc
header Map Id VarDefn
vs String
varS)
        Doc -> Doc -> Doc
$+$ Map Id VarDefn -> Doc
forall a b. (Pretty a, Ord a, Pretty b) => Map a b -> Doc
printMap0 Map Id VarDefn
vs
        Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ((Named Sentence -> Doc) -> [Named Sentence] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Annoted Sentence -> Doc
forall a. Pretty a => a -> Doc
pretty (Annoted Sentence -> Doc)
-> (Named Sentence -> Annoted Sentence) -> Named Sentence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Sentence -> Annoted Sentence
forall s. Named s -> Annoted s
fromLabelledSen) ([Named Sentence] -> [Doc])
-> ([Named Sentence] -> [Named Sentence])
-> [Named Sentence]
-> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a]
reverse ([Named Sentence] -> [Doc]) -> [Named Sentence] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Env -> [Named Sentence]
sentences Env
d)
        Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ((Diagnosis -> Doc) -> [Diagnosis] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Diagnosis -> Doc
forall a. Pretty a => a -> Doc
pretty ([Diagnosis] -> [Doc])
-> ([Diagnosis] -> [Diagnosis]) -> [Diagnosis] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a]
reverse ([Diagnosis] -> [Doc]) -> [Diagnosis] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Env -> [Diagnosis]
envDiags Env
d)

mostSyms :: Env -> [Symbol]
mostSyms :: Env -> [Symbol]
mostSyms e :: Env
e = let
  d :: Env
d = Env -> Env
delPreDefs Env
e
  cm :: ClassMap
cm = Env -> ClassMap
classMap Env
d
  tm :: TypeMap
tm = Env -> TypeMap
typeMap Env
d
  in ((Id, ClassInfo) -> Symbol) -> [(Id, ClassInfo)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Id
i, k :: ClassInfo
k) -> Id -> RawKind -> Symbol
idToClassSymbol Id
i (RawKind -> Symbol) -> RawKind -> Symbol
forall a b. (a -> b) -> a -> b
$ ClassInfo -> RawKind
rawKind ClassInfo
k) (ClassMap -> [(Id, ClassInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList ClassMap
cm)
      [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ((Id, Kind) -> Symbol) -> [(Id, Kind)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Id
i, s :: Kind
s) -> Id -> SymbolType -> Symbol
Symbol Id
i (SymbolType -> Symbol) -> SymbolType -> Symbol
forall a b. (a -> b) -> a -> b
$ Kind -> SymbolType
SuperClassSymbol Kind
s) (ClassMap -> [(Id, Kind)]
getSuperClasses ClassMap
cm)
      [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ((Id, Kind) -> Symbol) -> [(Id, Kind)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Id
i, s :: Kind
s) -> Id -> SymbolType -> Symbol
Symbol Id
i (SymbolType -> Symbol) -> SymbolType -> Symbol
forall a b. (a -> b) -> a -> b
$ Kind -> SymbolType
TypeKindInstance Kind
s) (TypeMap -> [(Id, Kind)]
getTypeKinds TypeMap
tm)
      [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ((Id, Id) -> Symbol) -> [(Id, Id)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Id
i, s :: Id
s) -> Id -> SymbolType -> Symbol
Symbol Id
i (SymbolType -> Symbol) -> SymbolType -> Symbol
forall a b. (a -> b) -> a -> b
$ Id -> SymbolType
SuperTypeSymbol Id
s) (TypeMap -> [(Id, Id)]
getSuperTypes TypeMap
tm)
      [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ((Id, Type) -> Symbol) -> [(Id, Type)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Id
i, s :: Type
s) -> Id -> SymbolType -> Symbol
Symbol Id
i (SymbolType -> Symbol) -> SymbolType -> Symbol
forall a b. (a -> b) -> a -> b
$ Type -> SymbolType
TypeAliasSymbol Type
s) (TypeMap -> [(Id, Type)]
getTypeAliases TypeMap
tm)
      [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ((Id, Set OpInfo) -> [Symbol]) -> [(Id, Set OpInfo)] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (i :: Id
i, ts :: Set OpInfo
ts) ->
                    (OpInfo -> Symbol) -> [OpInfo] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (\ t :: OpInfo
t -> (if OpDefn -> Bool
isPredOpDefn (OpDefn -> Bool) -> OpDefn -> Bool
forall a b. (a -> b) -> a -> b
$ OpInfo -> OpDefn
opDefn OpInfo
t then
                           Id -> SymbolType -> Symbol
Symbol Id
i (SymbolType -> Symbol)
-> (TypeScheme -> SymbolType) -> TypeScheme -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeScheme -> SymbolType
PredAsItemType (TypeScheme -> SymbolType)
-> (TypeScheme -> TypeScheme) -> TypeScheme -> SymbolType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeScheme -> TypeScheme
unPredTypeScheme
                           else Id -> TypeScheme -> Symbol
idToOpSymbol Id
i) (TypeScheme -> Symbol) -> TypeScheme -> Symbol
forall a b. (a -> b) -> a -> b
$ OpInfo -> TypeScheme
opType OpInfo
t) ([OpInfo] -> [Symbol]) -> [OpInfo] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
ts)
             (Assumps -> [(Id, Set OpInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList (Assumps -> [(Id, Set OpInfo)]) -> Assumps -> [(Id, Set OpInfo)]
forall a b. (a -> b) -> a -> b
$ Env -> Assumps
assumps Env
d)

printAliasType :: Type -> Doc
printAliasType :: Type -> Doc
printAliasType ty :: Type
ty =
    let (args :: [TypeArg]
args, t :: Type
t) = Type -> ([TypeArg], Type)
getArgsAndType Type
ty in
    [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (TypeArg -> Doc) -> [TypeArg] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
parens (Doc -> Doc) -> (TypeArg -> Doc) -> TypeArg -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeArg -> Doc
forall a. Pretty a => a -> Doc
pretty) [TypeArg]
args [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Doc
text String
assignS, Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
t]

printAliasTypes :: [(Id, Type)] -> Doc
printAliasTypes :: [(Id, Type)] -> Doc
printAliasTypes = [Doc] -> Doc
vcat ([Doc] -> Doc) -> ([(Id, Type)] -> [Doc]) -> [(Id, Type)] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
semi ([Doc] -> [Doc])
-> ([(Id, Type)] -> [Doc]) -> [(Id, Type)] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
   ((Id, Type) -> Doc) -> [(Id, Type)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Id
i, ty :: Type
ty) -> [Doc] -> Doc
sep [Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i, Type -> Doc
printAliasType Type
ty])

getArgsAndType :: Type -> ([TypeArg], Type)
getArgsAndType :: Type -> ([TypeArg], Type)
getArgsAndType ty :: Type
ty = case Type
ty of
  TypeAbs arg :: TypeArg
arg t :: Type
t _ -> let (l :: [TypeArg]
l, r :: Type
r) = Type -> ([TypeArg], Type)
getArgsAndType Type
t in (TypeArg
arg TypeArg -> [TypeArg] -> [TypeArg]
forall a. a -> [a] -> [a]
: [TypeArg]
l, Type
r)
  _ -> ([], Type
ty)

printMap0 :: (Pretty a, Ord a, Pretty b) => Map.Map a b -> Doc
printMap0 :: Map a b -> Doc
printMap0 = (Doc -> Doc)
-> ([Doc] -> Doc) -> (Doc -> Doc -> Doc) -> Map a b -> Doc
forall a b.
(Pretty a, Pretty b) =>
(Doc -> Doc)
-> ([Doc] -> Doc) -> (Doc -> Doc -> Doc) -> Map a b -> Doc
printMap Doc -> Doc
forall a. a -> a
id ([Doc] -> Doc
vcat ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
semi) ((Doc -> Doc -> Doc) -> Map a b -> Doc)
-> (Doc -> Doc -> Doc) -> Map a b -> Doc
forall a b. (a -> b) -> a -> b
$ \ a :: Doc
a b :: Doc
b -> [Doc] -> Doc
fsep [Doc
a, Doc
b]

printMap1 :: (Pretty a, Ord a, Pretty b) => Map.Map a b -> Doc
printMap1 :: Map a b -> Doc
printMap1 = (Doc -> Doc)
-> ([Doc] -> Doc) -> (Doc -> Doc -> Doc) -> Map a b -> Doc
forall a b.
(Pretty a, Pretty b) =>
(Doc -> Doc)
-> ([Doc] -> Doc) -> (Doc -> Doc -> Doc) -> Map a b -> Doc
printMap Doc -> Doc
forall a. a -> a
id [Doc] -> Doc
vcat ((Doc -> Doc -> Doc) -> Map a b -> Doc)
-> (Doc -> Doc -> Doc) -> Map a b -> Doc
forall a b. (a -> b) -> a -> b
$ \ a :: Doc
a b :: Doc
b -> [Doc] -> Doc
fsep [Doc
a, Doc
mapsto, Doc
b]

instance Pretty Morphism where
  pretty :: Morphism -> Doc
pretty m :: Morphism
m =
      let tm :: IdMap
tm = Morphism -> IdMap
typeIdMap Morphism
m
          cm :: IdMap
cm = Morphism -> IdMap
classIdMap Morphism
m
          fm :: FunMap
fm = Morphism -> FunMap
funMap Morphism
m
          {- the types in funs are already mapped
          key und value types only differ wrt. partiality -}
          ds :: [Doc]
ds = ((Id, TypeScheme) -> (Id, TypeScheme) -> [Doc] -> [Doc])
-> [Doc] -> FunMap -> [Doc]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey ( \ (i :: Id
i, _) (j :: Id
j, t :: TypeScheme
t) ->
                ((Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i Doc -> Doc -> Doc
<+> Doc
mapsto Doc -> Doc -> Doc
<+>
                  Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
j Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> TypeScheme -> Doc
forall a. Pretty a => a -> Doc
pretty TypeScheme
t) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:))
               [] FunMap
fm
      in (if IdMap -> Bool
forall k a. Map k a -> Bool
Map.null IdMap
tm then Doc
empty
         else String -> Doc
keyword (String
typeS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS) Doc -> Doc -> Doc
<+> IdMap -> Doc
forall a b. (Pretty a, Ord a, Pretty b) => Map a b -> Doc
printMap1 IdMap
tm)
         Doc -> Doc -> Doc
$+$ (if IdMap -> Bool
forall k a. Map k a -> Bool
Map.null IdMap
cm then Doc
empty
         else String -> Doc
keyword (String
classS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS) Doc -> Doc -> Doc
<+> IdMap -> Doc
forall a b. (Pretty a, Ord a, Pretty b) => Map a b -> Doc
printMap1 IdMap
cm)
         Doc -> Doc -> Doc
$+$ (if FunMap -> Bool
forall k a. Map k a -> Bool
Map.null FunMap
fm then Doc
empty
             else String -> Doc
keyword (String
opS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS) Doc -> Doc -> Doc
<+> [Doc] -> Doc
sepByCommas [Doc]
ds)
         Doc -> Doc -> Doc
$+$ Doc
colon Doc -> Doc -> Doc
<+> Doc -> Doc
specBraces (Env -> Doc
forall a. Pretty a => a -> Doc
pretty (Env -> Doc) -> Env -> Doc
forall a b. (a -> b) -> a -> b
$ Morphism -> Env
msource Morphism
m)
                    Doc -> Doc -> Doc
$+$ Doc
mapsto
                    Doc -> Doc -> Doc
<+> Doc -> Doc
specBraces (Env -> Doc
forall a. Pretty a => a -> Doc
pretty (Env -> Doc) -> Env -> Doc
forall a b. (a -> b) -> a -> b
$ Morphism -> Env
mtarget Morphism
m)

instance Pretty Symbol where
    pretty :: Symbol -> Doc
pretty s :: Symbol
s = let ty :: SymbolType
ty = Symbol -> SymbolType
symType Symbol
s in
      SymbKind -> [()] -> Doc
forall a. SymbKind -> [a] -> Doc
printSK (SymbolType -> SymbKind
symbTypeToKind SymbolType
ty) [()] Doc -> Doc -> Doc
<+> Id -> Doc
forall a. Pretty a => a -> Doc
pretty (Symbol -> Id
symName Symbol
s) Doc -> Doc -> Doc
<+> case SymbolType
ty of
        SuperTypeSymbol sty :: Id
sty -> Doc
less Doc -> Doc -> Doc
<+> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
sty
        SuperClassSymbol k :: Kind
k -> Doc
less Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. Pretty a => a -> Doc
pretty Kind
k
        TypeAliasSymbol t :: Type
t -> Type -> Doc
printAliasType Type
t
        TypeKindInstance k :: Kind
k -> Doc
colon Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. Pretty a => a -> Doc
pretty Kind
k
        OpAsItemType sc :: TypeScheme
sc -> Doc
colon Doc -> Doc -> Doc
<+> TypeScheme -> Doc
forall a. Pretty a => a -> Doc
pretty TypeScheme
sc
        TypeAsItemType k :: RawKind
k -> Doc
colon Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. Pretty a => a -> Doc
pretty (RawKind -> Kind
rawToKind RawKind
k)
        ClassAsItemType k :: RawKind
k -> Doc
colon Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. Pretty a => a -> Doc
pretty (RawKind -> Kind
rawToKind RawKind
k)
        PredAsItemType sc :: TypeScheme
sc -> Doc
colon Doc -> Doc -> Doc
<+> TypeScheme -> Doc
forall a. Pretty a => a -> Doc
pretty TypeScheme
sc

instance Pretty RawSymbol where
  pretty :: RawSymbol -> Doc
pretty rs :: RawSymbol
rs = case RawSymbol
rs of
      AnID i :: Id
i -> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i
      AKindedId k :: SymbKind
k i :: Id
i -> SymbKind -> [Id] -> Doc
forall a. SymbKind -> [a] -> Doc
printSK SymbKind
k [Id
i] Doc -> Doc -> Doc
<+> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i
      ASymbol s :: Symbol
s -> Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
s

improveDiag :: (GetRange a, Pretty a) => a -> Diagnosis -> Diagnosis
improveDiag :: a -> Diagnosis -> Diagnosis
improveDiag v :: a
v d :: Diagnosis
d = Diagnosis
d
  { diagString :: String
diagString = let f :: String
f : l :: [String]
l = String -> [String]
lines (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ Diagnosis -> String
diagString Diagnosis
d in
      [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ " of '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String -> String
forall a. Pretty a => a -> String -> String
showDoc a
v "'") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
l
  , diagPos :: Range
diagPos = a -> Range
forall a. GetRange a => a -> Range
getRange a
v }

mergeMap :: (Ord a, GetRange a, Pretty a) => (b -> b -> Result b)
         -> Map.Map a b -> Map.Map a b -> Result (Map.Map a b)
mergeMap :: (b -> b -> Result b) -> Map a b -> Map a b -> Result (Map a b)
mergeMap f :: b -> b -> Result b
f m1 :: Map a b
m1 = (Map a b -> (a, b) -> Result (Map a b))
-> Map a b -> [(a, b)] -> Result (Map a b)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ( \ m :: Map a b
m (k :: a
k, v :: b
v) -> case a -> Map a b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
k Map a b
m of
    Nothing -> Map a b -> Result (Map a b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map a b -> Result (Map a b)) -> Map a b -> Result (Map a b)
forall a b. (a -> b) -> a -> b
$ a -> b -> Map a b -> Map a b
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
k b
v Map a b
m
    Just w :: b
w -> let
      Result ds :: [Diagnosis]
ds r :: Maybe (Map a b)
r = do
        b
u <- b -> b -> Result b
f b
w b
v
        Map a b -> Result (Map a b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map a b -> Result (Map a b)) -> Map a b -> Result (Map a b)
forall a b. (a -> b) -> a -> b
$ a -> b -> Map a b -> Map a b
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
k b
u Map a b
m
      in [Diagnosis] -> Maybe (Map a b) -> Result (Map a b)
forall a. [Diagnosis] -> Maybe a -> Result a
Result ((Diagnosis -> Diagnosis) -> [Diagnosis] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Diagnosis -> Diagnosis
forall a. (GetRange a, Pretty a) => a -> Diagnosis -> Diagnosis
improveDiag a
k) [Diagnosis]
ds) Maybe (Map a b)
r) Map a b
m1 ([(a, b)] -> Result (Map a b))
-> (Map a b -> [(a, b)]) -> Map a b -> Result (Map a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
Map.toList

mergeClassInfo :: ClassInfo -> ClassInfo -> Result ClassInfo
mergeClassInfo :: ClassInfo -> ClassInfo -> Result ClassInfo
mergeClassInfo c1 :: ClassInfo
c1 c2 :: ClassInfo
c2 = do
    RawKind
k <- String -> RawKind -> RawKind -> Result RawKind
forall (m :: * -> *).
MonadFail m =>
String -> RawKind -> RawKind -> m RawKind
minRawKind "class raw kind" (ClassInfo -> RawKind
rawKind ClassInfo
c1) (RawKind -> Result RawKind) -> RawKind -> Result RawKind
forall a b. (a -> b) -> a -> b
$ ClassInfo -> RawKind
rawKind ClassInfo
c2
    ClassInfo -> Result ClassInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (ClassInfo -> Result ClassInfo) -> ClassInfo -> Result ClassInfo
forall a b. (a -> b) -> a -> b
$ RawKind -> Set Kind -> ClassInfo
ClassInfo RawKind
k (Set Kind -> ClassInfo) -> Set Kind -> ClassInfo
forall a b. (a -> b) -> a -> b
$ Set Kind -> Set Kind -> Set Kind
forall a. Ord a => Set a -> Set a -> Set a
Set.union (ClassInfo -> Set Kind
classKinds ClassInfo
c1) (Set Kind -> Set Kind) -> Set Kind -> Set Kind
forall a b. (a -> b) -> a -> b
$ ClassInfo -> Set Kind
classKinds ClassInfo
c2

minimizeClassMap :: ClassMap -> ClassMap
minimizeClassMap :: ClassMap -> ClassMap
minimizeClassMap cm :: ClassMap
cm = (ClassInfo -> ClassInfo) -> ClassMap -> ClassMap
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ ci :: ClassInfo
ci -> ClassInfo
ci { classKinds :: Set Kind
classKinds =
                          ClassMap -> [Set Kind] -> Set Kind
keepMinKinds ClassMap
cm [ClassInfo -> Set Kind
classKinds ClassInfo
ci] }) ClassMap
cm

mergeClassMap :: ClassMap -> ClassMap -> Result ClassMap
mergeClassMap :: ClassMap -> ClassMap -> Result ClassMap
mergeClassMap c :: ClassMap
c = (ClassMap -> ClassMap) -> Result ClassMap -> Result ClassMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ClassMap -> ClassMap
minimizeClassMap (Result ClassMap -> Result ClassMap)
-> (ClassMap -> Result ClassMap) -> ClassMap -> Result ClassMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ClassInfo -> ClassInfo -> Result ClassInfo)
-> ClassMap -> ClassMap -> Result ClassMap
forall a b.
(Ord a, GetRange a, Pretty a) =>
(b -> b -> Result b) -> Map a b -> Map a b -> Result (Map a b)
mergeMap ClassInfo -> ClassInfo -> Result ClassInfo
mergeClassInfo ClassMap
c

addClassMap :: ClassMap -> ClassMap -> ClassMap
addClassMap :: ClassMap -> ClassMap -> ClassMap
addClassMap c :: ClassMap
c = ClassMap -> Maybe ClassMap -> ClassMap
forall a. a -> Maybe a -> a
fromMaybe (String -> ClassMap
forall a. HasCallStack => String -> a
error "addClassMap") (Maybe ClassMap -> ClassMap)
-> (ClassMap -> Maybe ClassMap) -> ClassMap -> ClassMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result ClassMap -> Maybe ClassMap
forall a. Result a -> Maybe a
maybeResult (Result ClassMap -> Maybe ClassMap)
-> (ClassMap -> Result ClassMap) -> ClassMap -> Maybe ClassMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClassMap -> ClassMap -> Result ClassMap
mergeClassMap ClassMap
c

addCpoMap :: ClassMap -> ClassMap
addCpoMap :: ClassMap -> ClassMap
addCpoMap = ClassMap -> ClassMap -> ClassMap
addClassMap ClassMap
cpoMap

diffClassMap :: ClassMap -> ClassMap -> ClassMap
diffClassMap :: ClassMap -> ClassMap -> ClassMap
diffClassMap c1 :: ClassMap
c1 c2 :: ClassMap
c2 =
  let ce :: ClassMap
ce = ClassMap -> ClassMap -> ClassMap
addClassMap ClassMap
c1 ClassMap
c2
  in (ClassInfo -> ClassInfo -> Maybe ClassInfo)
-> ClassMap -> ClassMap -> ClassMap
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith (ClassMap -> ClassInfo -> ClassInfo -> Maybe ClassInfo
diffClass ClassMap
ce) ClassMap
c1 ClassMap
c2

-- | compute difference of class infos
diffClass :: ClassMap -> ClassInfo -> ClassInfo -> Maybe ClassInfo
diffClass :: ClassMap -> ClassInfo -> ClassInfo -> Maybe ClassInfo
diffClass cm :: ClassMap
cm (ClassInfo r1 :: RawKind
r1 k1 :: Set Kind
k1) (ClassInfo _ k2 :: Set Kind
k2) =
    let ks :: Set Kind
ks = (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ k :: Kind
k -> Set Kind -> Bool
forall a. Set a -> Bool
Set.null (Set Kind -> Bool) -> Set Kind -> Bool
forall a b. (a -> b) -> a -> b
$
                  (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((Kind -> Kind -> Bool) -> Kind -> Kind -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ClassMap -> Kind -> Kind -> Bool
lesserKind ClassMap
cm) Kind
k) Set Kind
k2) Set Kind
k1
    in if Set Kind -> Bool
forall a. Set a -> Bool
Set.null Set Kind
ks then Maybe ClassInfo
forall a. Maybe a
Nothing else
           ClassInfo -> Maybe ClassInfo
forall a. a -> Maybe a
Just (ClassInfo -> Maybe ClassInfo) -> ClassInfo -> Maybe ClassInfo
forall a b. (a -> b) -> a -> b
$ RawKind -> Set Kind -> ClassInfo
ClassInfo RawKind
r1 Set Kind
ks

diffTypeMap :: ClassMap -> TypeMap -> TypeMap -> TypeMap
diffTypeMap :: ClassMap -> TypeMap -> TypeMap -> TypeMap
diffTypeMap = (TypeInfo -> TypeInfo -> Maybe TypeInfo)
-> TypeMap -> TypeMap -> TypeMap
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith ((TypeInfo -> TypeInfo -> Maybe TypeInfo)
 -> TypeMap -> TypeMap -> TypeMap)
-> (ClassMap -> TypeInfo -> TypeInfo -> Maybe TypeInfo)
-> ClassMap
-> TypeMap
-> TypeMap
-> TypeMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClassMap -> TypeInfo -> TypeInfo -> Maybe TypeInfo
diffType

-- | compute difference of type infos
diffType :: ClassMap -> TypeInfo -> TypeInfo -> Maybe TypeInfo
diffType :: ClassMap -> TypeInfo -> TypeInfo -> Maybe TypeInfo
diffType cm :: ClassMap
cm ti1 :: TypeInfo
ti1 ti2 :: TypeInfo
ti2 =
    let k1 :: Set Kind
k1 = TypeInfo -> Set Kind
otherTypeKinds TypeInfo
ti1
        k2 :: Set Kind
k2 = TypeInfo -> Set Kind
otherTypeKinds TypeInfo
ti2
        ks :: Set Kind
ks = (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ k :: Kind
k -> Set Kind -> Bool
forall a. Set a -> Bool
Set.null (Set Kind -> Bool) -> Set Kind -> Bool
forall a b. (a -> b) -> a -> b
$
                  (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((Kind -> Kind -> Bool) -> Kind -> Kind -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ClassMap -> Kind -> Kind -> Bool
lesserKind ClassMap
cm) Kind
k) Set Kind
k2) Set Kind
k1
        sups :: Set Id
sups = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (TypeInfo -> Set Id
superTypes TypeInfo
ti1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Set Id
superTypes TypeInfo
ti2
    in if Set Kind -> Bool
forall a. Set a -> Bool
Set.null Set Kind
ks Bool -> Bool -> Bool
&& Set Id -> Bool
forall a. Set a -> Bool
Set.null Set Id
sups then Maybe TypeInfo
forall a. Maybe a
Nothing else
       TypeInfo -> Maybe TypeInfo
forall a. a -> Maybe a
Just (TypeInfo -> Maybe TypeInfo) -> TypeInfo -> Maybe TypeInfo
forall a b. (a -> b) -> a -> b
$ TypeInfo
ti1 { otherTypeKinds :: Set Kind
otherTypeKinds = Set Kind
ks
                  , superTypes :: Set Id
superTypes = Set Id
sups }