{- |
Module      :  ./HasCASL/MinType.hs
Description :  choose a minimal type for overloaded terms
Copyright   :  (c) Christian Maeder and Uni Bremen 2003
License     :  GPLv2 or higher, see LICENSE.txt

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

choose a minimal type
-}

module HasCASL.MinType
  ( q2p
  , typeNub
  , haveCommonSupertype
  , getCommonSupertype
  ) where

import HasCASL.As
import HasCASL.FoldType
import HasCASL.Le
import HasCASL.AsUtils
import HasCASL.TypeAna
import HasCASL.Unify
import HasCASL.Constrain

import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Common.Lib.Rel as Rel
import Common.DocUtils
import Common.Id
import Common.Result
import Common.Lib.State
import Common.Utils

import Data.List as List
import Data.Maybe

q2p :: (a, b, c, d) -> (c, d)
q2p :: (a, b, c, d) -> (c, d)
q2p (_, _, c :: c
c, d :: d
d) = (c
c, d
d)

typeNub :: Env -> (a -> (Type, Term)) -> [a] -> [a]
typeNub :: Env -> (a -> (Type, Term)) -> [a] -> [a]
typeNub e :: Env
e f :: a -> (Type, Term)
f = let
    comp :: (Type, Term) -> (Type, Term) -> Bool
comp (ty1 :: Type
ty1, t1 :: Term
t1) (ty2 :: Type
ty2, t2 :: Term
t2) = Env -> Term -> Term -> Bool
eqTerm Env
e Term
t1 Term
t2 Bool -> Bool -> Bool
&&
                               Env -> Type -> Type -> Bool
lesserType Env
e Type
ty1 Type
ty2
    lt :: a -> a -> Bool
lt a :: a
a b :: a
b = (Type, Term) -> (Type, Term) -> Bool
comp (a -> (Type, Term)
f a
a) (a -> (Type, Term)
f a
b)
    in (a -> a -> Bool) -> [a] -> [a]
forall a. (a -> a -> Bool) -> [a] -> [a]
keepMins a -> a -> Bool
lt

eqTerm :: Env -> Term -> Term -> Bool
eqTerm :: Env -> Term -> Term -> Bool
eqTerm e :: Env
e t1 :: Term
t1 t2 :: Term
t2 = case (Term
t1, Term
t2) of
     (TypedTerm t :: Term
t _ _ _, _) -> Env -> Term -> Term -> Bool
eqTerm Env
e Term
t Term
t2
     (_, TypedTerm t :: Term
t _ _ _) -> Env -> Term -> Term -> Bool
eqTerm Env
e Term
t1 Term
t
     (QualVar (VarDecl v1 :: Id
v1 _s1 :: Type
_s1 _ _), QualVar (VarDecl v2 :: Id
v2 _s2 :: Type
_s2 _ _)) ->
         Id
v1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
v2
     (QualOp _ i1 :: PolyId
i1 s1 :: TypeScheme
s1 _ _ _, QualOp _ i2 :: PolyId
i2 s2 :: TypeScheme
s2 _ _ _) -> PolyId
i1 PolyId -> PolyId -> Bool
forall a. Eq a => a -> a -> Bool
== PolyId
i2
         Bool -> Bool -> Bool
&& Env -> TypeScheme -> TypeScheme -> Bool
haveCommonSupertype Env
e TypeScheme
s1 TypeScheme
s2
     (ApplTerm tf1 :: Term
tf1 ta1 :: Term
ta1 _, ApplTerm tf2 :: Term
tf2 ta2 :: Term
ta2 _) ->
         Env -> Term -> Term -> Bool
eqTerm Env
e Term
tf1 Term
tf2 Bool -> Bool -> Bool
&& Env -> Term -> Term -> Bool
eqTerm Env
e Term
ta1 Term
ta2
     (TupleTerm ts1 :: [Term]
ts1 _, TupleTerm ts2 :: [Term]
ts2 _) ->
         [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ts1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ts2 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Term -> Term -> Bool) -> [Term] -> [Term] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Env -> Term -> Term -> Bool
eqTerm Env
e) [Term]
ts1 [Term]
ts2)
     (QuantifiedTerm q1 :: Quantifier
q1 vs1 :: [GenVarDecl]
vs1 f1 :: Term
f1 _, QuantifiedTerm q2 :: Quantifier
q2 vs2 :: [GenVarDecl]
vs2 f2 :: Term
f2 _) ->
         (Quantifier
q1, [GenVarDecl]
vs1) (Quantifier, [GenVarDecl]) -> (Quantifier, [GenVarDecl]) -> Bool
forall a. Eq a => a -> a -> Bool
== (Quantifier
q2, [GenVarDecl]
vs2) Bool -> Bool -> Bool
&& Env -> Term -> Term -> Bool
eqTerm Env
e Term
f1 Term
f2
     (LambdaTerm ps1 :: [Term]
ps1 p1 :: Partiality
p1 f1 :: Term
f1 _, LambdaTerm ps2 :: [Term]
ps2 p2 :: Partiality
p2 f2 :: Term
f2 _) ->
          [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Term -> Term -> Bool) -> [Term] -> [Term] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Env -> Term -> Term -> Bool
eqTerm Env
e) [Term]
ps1 [Term]
ps2) Bool -> Bool -> Bool
&& Partiality
p1 Partiality -> Partiality -> Bool
forall a. Eq a => a -> a -> Bool
== Partiality
p2 Bool -> Bool -> Bool
&& Env -> Term -> Term -> Bool
eqTerm Env
e Term
f1 Term
f2
          Bool -> Bool -> Bool
&& [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ps1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ps2
     (CaseTerm f1 :: Term
f1 e1 :: [ProgEq]
e1 _, CaseTerm f2 :: Term
f2 e2 :: [ProgEq]
e2 _) ->
         Env -> Term -> Term -> Bool
eqTerm Env
e Term
f1 Term
f2 Bool -> Bool -> Bool
&& [ProgEq] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ProgEq]
e1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [ProgEq] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ProgEq]
e2
         Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((ProgEq -> ProgEq -> Bool) -> [ProgEq] -> [ProgEq] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Env -> ProgEq -> ProgEq -> Bool
eqProgEq Env
e) [ProgEq]
e1 [ProgEq]
e2)
     (LetTerm _ e1 :: [ProgEq]
e1 f1 :: Term
f1 _, LetTerm _ e2 :: [ProgEq]
e2 f2 :: Term
f2 _) ->
         Env -> Term -> Term -> Bool
eqTerm Env
e Term
f1 Term
f2 Bool -> Bool -> Bool
&& [ProgEq] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ProgEq]
e1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [ProgEq] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ProgEq]
e2
         Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((ProgEq -> ProgEq -> Bool) -> [ProgEq] -> [ProgEq] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Env -> ProgEq -> ProgEq -> Bool
eqProgEq Env
e) [ProgEq]
e1 [ProgEq]
e2)
     _ -> Bool
False

eqProgEq :: Env -> ProgEq -> ProgEq -> Bool
eqProgEq :: Env -> ProgEq -> ProgEq -> Bool
eqProgEq e :: Env
e (ProgEq p1 :: Term
p1 t1 :: Term
t1 _) (ProgEq p2 :: Term
p2 t2 :: Term
t2 _) = Env -> Term -> Term -> Bool
eqTerm Env
e Term
p1 Term
p2 Bool -> Bool -> Bool
&& Env -> Term -> Term -> Bool
eqTerm Env
e Term
t1 Term
t2

addToEnv :: (Type, VarKind) -> Env -> Env
addToEnv :: (Type, VarKind) -> Env -> Env
addToEnv (ty :: Type
ty, vk :: VarKind
vk) e :: Env
e = case Type
ty of
    TypeName i :: Id
i rk :: RawKind
rk c :: Int
c | Int
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 ->
        State Env () -> Env -> Env
forall s a. State s a -> s -> s
execState (Bool -> TypeVarDefn -> Id -> State Env ()
addLocalTypeVar Bool
False (Variance -> VarKind -> RawKind -> Int -> TypeVarDefn
TypeVarDefn Variance
NonVar VarKind
vk RawKind
rk Int
c) Id
i) Env
e
    _ -> Env
e

haveCommonSupertype :: Env -> TypeScheme -> TypeScheme -> Bool
haveCommonSupertype :: Env -> TypeScheme -> TypeScheme -> Bool
haveCommonSupertype e :: Env
e s :: TypeScheme
s = Maybe TypeTriple -> Bool
forall a. Maybe a -> Bool
isJust (Maybe TypeTriple -> Bool)
-> (TypeScheme -> Maybe TypeTriple) -> TypeScheme -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> TypeScheme -> TypeScheme -> Maybe TypeTriple
getCommonSupertype Env
e TypeScheme
s

getCommonSupertype :: Env -> TypeScheme -> TypeScheme -> Maybe TypeTriple
getCommonSupertype :: Env -> TypeScheme -> TypeScheme -> Maybe TypeTriple
getCommonSupertype e :: Env
e s1 :: TypeScheme
s1 s2 :: TypeScheme
s2 =
    State Env (Maybe TypeTriple) -> Env -> Maybe TypeTriple
forall s a. State s a -> s -> a
evalState (State Int (Maybe TypeTriple) -> State Env (Maybe TypeTriple)
forall a. State Int a -> State Env a
toEnvState (State Int (Maybe TypeTriple) -> State Env (Maybe TypeTriple))
-> State Int (Maybe TypeTriple) -> State Env (Maybe TypeTriple)
forall a b. (a -> b) -> a -> b
$ Env -> TypeScheme -> TypeScheme -> State Int (Maybe TypeTriple)
haveCommonSupertypeE Env
e TypeScheme
s1 TypeScheme
s2) Env
e

type TypeTriple = (Type, [Type], Type, [Type], [TypeArg], Type)

haveCommonSupertypeE :: Env -> TypeScheme -> TypeScheme
  -> State Int (Maybe TypeTriple)
haveCommonSupertypeE :: Env -> TypeScheme -> TypeScheme -> State Int (Maybe TypeTriple)
haveCommonSupertypeE eIn :: Env
eIn s1 :: TypeScheme
s1 s2 :: TypeScheme
s2 = do
    (t1 :: Type
t1, l1 :: [(Type, VarKind)]
l1) <- TypeScheme -> State Int (Type, [(Type, VarKind)])
freshInst TypeScheme
s1
    (t2 :: Type
t2, l2 :: [(Type, VarKind)]
l2) <- TypeScheme -> State Int (Type, [(Type, VarKind)])
freshInst TypeScheme
s2
    Type
cst <- (Id, RawKind) -> State Int Type
mkSingleSubst (String -> Id
genName "commonSupertype", RawKind
rStar)
    let cs :: Set Constrain
cs = [Constrain] -> Set Constrain
forall a. Ord a => [a] -> Set a
Set.fromList [Type -> Type -> Constrain
Subtyping Type
t1 Type
cst, Type -> Type -> Constrain
Subtyping Type
t2 Type
cst]
        e :: Env
e = ((Type, VarKind) -> Env -> Env) -> Env -> [(Type, VarKind)] -> Env
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type, VarKind) -> Env -> Env
addToEnv Env
eIn ([(Type, VarKind)] -> Env) -> [(Type, VarKind)] -> Env
forall a b. (a -> b) -> a -> b
$ (Type
cst, Kind -> VarKind
VarKind Kind
universe) (Type, VarKind) -> [(Type, VarKind)] -> [(Type, VarKind)]
forall a. a -> [a] -> [a]
: [(Type, VarKind)]
l1 [(Type, VarKind)] -> [(Type, VarKind)] -> [(Type, VarKind)]
forall a. [a] -> [a] -> [a]
++ [(Type, VarKind)]
l2
    Result _ mr :: Maybe (Subst, Set Constrain)
mr <- Bool
-> Env
-> Set Constrain
-> Maybe Type
-> State Int (Result (Subst, Set Constrain))
shapeRelAndSimplify Bool
False Env
e Set Constrain
cs (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
cst)
    Maybe TypeTriple -> State Int (Maybe TypeTriple)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeTriple -> State Int (Maybe TypeTriple))
-> Maybe TypeTriple -> State Int (Maybe TypeTriple)
forall a b. (a -> b) -> a -> b
$ case Maybe (Subst, Set Constrain)
mr of
      Nothing -> Maybe TypeTriple
forall a. Maybe a
Nothing
      Just (sbst :: Subst
sbst, rcs :: Set Constrain
rcs) -> let (qs :: Set Constrain
qs, subC :: Set Constrain
subC) = Set Constrain -> (Set Constrain, Set Constrain)
partitionC Set Constrain
rcs
        in case Rel Type -> [(Type, Type)] -> Maybe Subst
reduceCommonSubtypes
               (Rel Type -> Rel Type
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel Type -> Rel Type) -> Rel Type -> Rel Type
forall a b. (a -> b) -> a -> b
$ TypeMap -> Rel Type
fromTypeMap (TypeMap -> Rel Type) -> TypeMap -> Rel Type
forall a b. (a -> b) -> a -> b
$ Env -> TypeMap
typeMap Env
e)
               (Set Constrain -> [(Type, Type)]
toListC Set Constrain
subC) of
             Just msb :: Subst
msb | Set Constrain -> Bool
forall a. Set a -> Bool
Set.null Set Constrain
qs -> let
               doSubst :: Type -> Type
doSubst = Subst -> Type -> Type
subst (Subst -> Type -> Type) -> Subst -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Subst -> Subst -> Subst
compSubst Subst
sbst Subst
msb
               [ty :: Type
ty, ty1 :: Type
ty1, ty2 :: Type
ty2] = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
doSubst [Type
cst, Type
t1, Type
t2]
               fvs :: [(Int, (Id, RawKind))]
fvs = ([(Int, (Id, RawKind))]
 -> [(Int, (Id, RawKind))] -> [(Int, (Id, RawKind))])
-> [[(Int, (Id, RawKind))]] -> [(Int, (Id, RawKind))]
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 [(Int, (Id, RawKind))]
-> [(Int, (Id, RawKind))] -> [(Int, (Id, RawKind))]
forall a. Eq a => [a] -> [a] -> [a]
List.union ([[(Int, (Id, RawKind))]] -> [(Int, (Id, RawKind))])
-> [[(Int, (Id, RawKind))]] -> [(Int, (Id, RawKind))]
forall a b. (a -> b) -> a -> b
$ (Type -> [(Int, (Id, RawKind))])
-> [Type] -> [[(Int, (Id, RawKind))]]
forall a b. (a -> b) -> [a] -> [b]
map Type -> [(Int, (Id, RawKind))]
freeTVars [Type
ty1, Type
ty2, Type
ty]
               svs :: [(Int, (Id, RawKind))]
svs = ((Int, (Id, RawKind)) -> (Int, (Id, RawKind)) -> Ordering)
-> [(Int, (Id, RawKind))] -> [(Int, (Id, RawKind))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Int, (Id, RawKind)) -> (Int, (Id, RawKind)) -> Ordering
forall a b b. Ord a => (a, b) -> (a, b) -> Ordering
comp [(Int, (Id, RawKind))]
fvs
               comp :: (a, b) -> (a, b) -> Ordering
comp a :: (a, b)
a b :: (a, b)
b = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ((a, b) -> a
forall a b. (a, b) -> a
fst (a, b)
a) (a -> Ordering) -> a -> Ordering
forall a b. (a -> b) -> a -> b
$ (a, b) -> a
forall a b. (a, b) -> a
fst (a, b)
b
               tvs :: LocalTypeVars
tvs = Env -> LocalTypeVars
localTypeVars Env
e
               newArgs :: [TypeArg]
newArgs = ((Int, (Id, RawKind)) -> TypeArg)
-> [(Int, (Id, RawKind))] -> [TypeArg]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (_, (i :: Id
i, _)) -> case Id -> LocalTypeVars -> Maybe TypeVarDefn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i LocalTypeVars
tvs of
                  Nothing -> String -> TypeArg
forall a. HasCallStack => String -> a
error (String -> TypeArg) -> String -> TypeArg
forall a b. (a -> b) -> a -> b
$ "generalizeS " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Id, Type) -> String
forall a. Show a => a -> String
show (Id
i, Type
ty)
                      String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (TypeScheme, TypeScheme) -> String -> String
forall a. Pretty a => a -> String -> String
showDoc (TypeScheme
s1, TypeScheme
s2) ""
                  Just (TypeVarDefn v :: Variance
v vk :: VarKind
vk rk :: RawKind
rk c :: Int
c) ->
                      Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
i Variance
v VarKind
vk RawKind
rk Int
c SeparatorKind
Other Range
nullRange) [(Int, (Id, RawKind))]
svs
               genArgs :: Type -> Type
genArgs = [TypeArg] -> Type -> Type
generalize [TypeArg]
newArgs
               [gty :: Type
gty, gty1 :: Type
gty1, gty2 :: Type
gty2] = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
genArgs [Type
ty, Type
ty1, Type
ty2]
               gl1 :: [Type]
gl1 = ((Type, VarKind) -> Type) -> [(Type, VarKind)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Type
genArgs (Type -> Type)
-> ((Type, VarKind) -> Type) -> (Type, VarKind) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
doSubst (Type -> Type)
-> ((Type, VarKind) -> Type) -> (Type, VarKind) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, VarKind) -> Type
forall a b. (a, b) -> a
fst) [(Type, VarKind)]
l1
               gl2 :: [Type]
gl2 = ((Type, VarKind) -> Type) -> [(Type, VarKind)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Type
genArgs (Type -> Type)
-> ((Type, VarKind) -> Type) -> (Type, VarKind) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
doSubst (Type -> Type)
-> ((Type, VarKind) -> Type) -> (Type, VarKind) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, VarKind) -> Type
forall a b. (a, b) -> a
fst) [(Type, VarKind)]
l2
               in TypeTriple -> Maybe TypeTriple
forall a. a -> Maybe a
Just (Type
gty1, [Type]
gl1, Type
gty2, [Type]
gl2, [TypeArg] -> [TypeArg]
genTypeArgs [TypeArg]
newArgs, Type
gty)
             _ -> Maybe TypeTriple
forall a. Maybe a
Nothing

reduceCommonSubtypes :: Rel.Rel Type -> [(Type, Type)] -> Maybe Subst
reduceCommonSubtypes :: Rel Type -> [(Type, Type)] -> Maybe Subst
reduceCommonSubtypes e :: Rel Type
e l :: [(Type, Type)]
l = let
    mygroup :: [(Type, Type)] -> [[(Type, Type)]]
mygroup = ((Type, Type) -> (Type, Type) -> Bool)
-> [(Type, Type)] -> [[(Type, Type)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy ( \ (a :: Type
a, b :: Type
b) (c :: Type
c, d :: Type
d) -> case (Type
a, Type
b, Type
d) of
                  (TypeName _ _ n :: Int
n, TypeName _ _ 0, TypeName _ _ 0)
                      -> Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 Bool -> Bool -> Bool
&& Type
a Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
c
                  _ -> Bool
False)
    mypart :: [[a]] -> ([[a]], [[a]])
mypart = ([a] -> Bool) -> [[a]] -> ([[a]], [[a]])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ( \ s :: [a]
s -> case [a]
s of
                         [] -> String -> Bool
forall a. HasCallStack => String -> a
error "reduceCommonSubtypes1"
                         [_] -> Bool
False
                         _ -> Bool
True)
    (csubts :: [[(Type, Type)]]
csubts, rest :: [[(Type, Type)]]
rest) = [[(Type, Type)]] -> ([[(Type, Type)]], [[(Type, Type)]])
forall a. [[a]] -> ([[a]], [[a]])
mypart ([[(Type, Type)]] -> ([[(Type, Type)]], [[(Type, Type)]]))
-> [[(Type, Type)]] -> ([[(Type, Type)]], [[(Type, Type)]])
forall a b. (a -> b) -> a -> b
$ [(Type, Type)] -> [[(Type, Type)]]
mygroup [(Type, Type)]
l
    swap :: [(b, a)] -> [(a, b)]
swap = ((b, a) -> (a, b)) -> [(b, a)] -> [(a, b)]
forall a b. (a -> b) -> [a] -> [b]
map (((b, a) -> (a, b)) -> [(b, a)] -> [(a, b)])
-> ((b, a) -> (a, b)) -> [(b, a)] -> [(a, b)]
forall a b. (a -> b) -> a -> b
$ \ (a :: b
a, b :: a
b) -> (a
b, b
a)
    (csuperts :: [[(Type, Type)]]
csuperts, rest2 :: [[(Type, Type)]]
rest2) = [[(Type, Type)]] -> ([[(Type, Type)]], [[(Type, Type)]])
forall a. [[a]] -> ([[a]], [[a]])
mypart ([[(Type, Type)]] -> ([[(Type, Type)]], [[(Type, Type)]]))
-> [[(Type, Type)]] -> ([[(Type, Type)]], [[(Type, Type)]])
forall a b. (a -> b) -> a -> b
$ [(Type, Type)] -> [[(Type, Type)]]
mygroup ([(Type, Type)] -> [[(Type, Type)]])
-> [(Type, Type)] -> [[(Type, Type)]]
forall a b. (a -> b) -> a -> b
$ [(Type, Type)] -> [(Type, Type)]
forall a. Ord a => [a] -> [a]
sort ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ [(Type, Type)] -> [(Type, Type)]
forall b a. [(b, a)] -> [(a, b)]
swap ([[(Type, Type)]] -> [(Type, Type)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Type, Type)]]
rest)
    mkPair :: [(a, b)] -> (a, [b])
mkPair s :: [(a, b)]
s = case [(a, b)]
s of
          (a :: a
a, _) : _ -> (a
a, ((a, b) -> b) -> [(a, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> b
forall a b. (a, b) -> b
snd [(a, b)]
s)
          _ -> String -> (a, [b])
forall a. HasCallStack => String -> a
error "reduceCommonSubtypes2"
    subM :: Maybe [(Int, Type)]
subM = ([(Type, Type)] -> Maybe (Int, Type))
-> [[(Type, Type)]] -> Maybe [(Int, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Rel Type -> Bool -> (Type, [Type]) -> Maybe (Int, Type)
commonSubtype Rel Type
e Bool
True ((Type, [Type]) -> Maybe (Int, Type))
-> ([(Type, Type)] -> (Type, [Type]))
-> [(Type, Type)]
-> Maybe (Int, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Type, Type)] -> (Type, [Type])
forall a b. [(a, b)] -> (a, [b])
mkPair) [[(Type, Type)]]
csubts
    superM :: Maybe [(Int, Type)]
superM = ([(Type, Type)] -> Maybe (Int, Type))
-> [[(Type, Type)]] -> Maybe [(Int, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Rel Type -> Bool -> (Type, [Type]) -> Maybe (Int, Type)
commonSubtype Rel Type
e Bool
False ((Type, [Type]) -> Maybe (Int, Type))
-> ([(Type, Type)] -> (Type, [Type]))
-> [(Type, Type)]
-> Maybe (Int, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Type, Type)] -> (Type, [Type])
forall a b. [(a, b)] -> (a, [b])
mkPair) [[(Type, Type)]]
csuperts
    in case ([[(Type, Type)]] -> [(Type, Type)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Type, Type)]]
rest2, Maybe [(Int, Type)]
subM, Maybe [(Int, Type)]
superM) of
      ([], Just l1 :: [(Int, Type)]
l1, Just l2 :: [(Int, Type)]
l2) -> Subst -> Maybe Subst
forall a. a -> Maybe a
Just (Subst -> Maybe Subst) -> Subst -> Maybe Subst
forall a b. (a -> b) -> a -> b
$ [(Int, Type)] -> Subst
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Type)] -> Subst) -> [(Int, Type)] -> Subst
forall a b. (a -> b) -> a -> b
$ [(Int, Type)]
l1 [(Int, Type)] -> [(Int, Type)] -> [(Int, Type)]
forall a. [a] -> [a] -> [a]
++ [(Int, Type)]
l2
      _ -> Maybe Subst
forall a. Maybe a
Nothing

commonSubtype :: Rel.Rel Type -> Bool -> (Type, [Type]) -> Maybe (Int, Type)
commonSubtype :: Rel Type -> Bool -> (Type, [Type]) -> Maybe (Int, Type)
commonSubtype trel :: Rel Type
trel b :: Bool
b (ty :: Type
ty, l :: [Type]
l) =
  let tySet :: Set Type
tySet = (Set Type -> Set Type -> Set Type) -> [Set Type] -> Set Type
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Set Type -> Set Type -> Set Type
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
         ([Set Type] -> Set Type) -> [Set Type] -> Set Type
forall a b. (a -> b) -> a -> b
$ (Type -> Set Type) -> [Type] -> [Set Type]
forall a b. (a -> b) -> [a] -> [b]
map (if Bool
b then Rel Type -> Type -> Set Type
forall a. Ord a => Rel a -> a -> Set a
Rel.predecessors Rel Type
trel else Rel Type -> Type -> Set Type
forall a. Ord a => Rel a -> a -> Set a
Rel.succs Rel Type
trel) [Type]
l
  in case Type
ty of
    TypeName _ _ n :: Int
n | Bool -> Bool
not (Set Type -> Bool
forall a. Set a -> Bool
Set.null Set Type
tySet) Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0
      -> (Int, Type) -> Maybe (Int, Type)
forall a. a -> Maybe a
Just (Int
n, Set Type -> Type
forall a. Set a -> a
Set.findMin Set Type
tySet)
    _ -> Maybe (Int, Type)
forall a. Maybe a
Nothing