66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{- |

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederModule : $Header$

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederMaintainer : maeder@tzi.de

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederStability : experimental

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederPortability : portable

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederconstraint resolution

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder-}

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule HasCASL.Constrain

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder ( Constraints

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder , Constrain(..)

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder , noC

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder , substC

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder , joinC

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder , insertC

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , shapeRel

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder , monoSubsts

08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder , fromTypeMap

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder , simplify

712f5e5ca1c3a5cfdd28518154ecf2dd0994cdb5Christian Maeder ) where

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder

f71a8dcf94fd9eb3c9800e16dcdc5e5ff74e5c22Christian Maederimport HasCASL.Unify

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.As

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maederimport HasCASL.AsUtils

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport HasCASL.Le

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport HasCASL.PrintLe()

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport HasCASL.TypeAna

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport HasCASL.ClassAna

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederimport qualified Data.Set as Set

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederimport qualified Data.Map as Map

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport qualified Common.Lib.Rel as Rel

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Common.Lib.State

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Common.Id

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maederimport Common.Result

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport Common.Doc

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.DocUtils

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Control.Exception(assert)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Data.List

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Data.Maybe

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder{- utils for singleton sets that could also be part of "Data.Set". These

fb50920e621bfc152c19147cb52077ff06b3526bChristian Maederfunctions rely on 'Data.Set.size' being computable in constant time and

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maederwould need to be rewritten for set implementations with a size

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederfunction that is only linear. -}

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder-- | /O(1)/ test if the set's size is one

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederisSingleton :: Set.Set a -> Bool

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederisSingleton s = Set.size s == 1

fb50920e621bfc152c19147cb52077ff06b3526bChristian Maeder

fb50920e621bfc152c19147cb52077ff06b3526bChristian Maeder-- | /O(1)/ test if the set's size is greater one

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederhasMany :: Set.Set a -> Bool

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederhasMany s = Set.size s > 1

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederdata Constrain = Kinding Type Kind

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder | Subtyping Type Type

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder deriving (Eq, Ord, Show)

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederinstance Pretty Constrain where

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder pretty c = case c of

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder Kinding ty k -> pretty $ KindedType ty k nullRange

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder Subtyping t1 t2 -> fsep [pretty t1, less <+> pretty t2]

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederinstance PosItem Constrain where

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder getRange c = case c of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Kinding ty _ -> getRange ty

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Subtyping t1 t2 -> getRange t1 `appRange` getRange t2

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maedertype Constraints = Set.Set Constrain

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedernoC :: Constraints

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedernoC = Set.empty

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian MaederjoinC :: Constraints -> Constraints -> Constraints

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian MaederjoinC = Set.union

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian MaederinsertC :: Constrain -> Constraints -> Constraints

628310b42327ad76ce471caf0dde6563d6fa6307Christian MaederinsertC c = case c of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Subtyping t1 t2 -> if t1 == t2 then id else Set.insert c

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Kinding _ k -> if k == universe then id else Set.insert c

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedersubstC :: Subst -> Constraints -> Constraints

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedersubstC s = Set.fold (insertC . ( \ c -> case c of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Kinding ty k -> Kinding (subst s ty) k

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Subtyping t1 t2 -> Subtyping (subst s t1) $ subst s t2)) noC

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maedersimplify :: TypeEnv -> Constraints -> ([Diagnosis], Constraints)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maedersimplify te rs =

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder if Set.null rs then ([], noC)

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder else let (r, rt) = Set.deleteFindMin rs

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder Result ds m = entail te r

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder (es, cs) = simplify te rt

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder in (ds ++ es, case m of

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder Just _ -> cs

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder Nothing -> insertC r cs)

f0742398d4587242b1a115de113cd17f63dcb6d0Christian Maeder

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederentail :: Monad m => TypeEnv -> Constrain -> m ()

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederentail te p =

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder do is <- byInst te p

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder mapM_ (entail te) $ Set.toList is

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaederbyInst :: Monad m => TypeEnv -> Constrain -> m Constraints

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederbyInst te c = let cm = classMap te in case c of

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder Kinding ty k -> if k == universe then

c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian Maeder assert (rawKindOfType ty == ClassKind ())

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder $ return noC else

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder let Result _ds mk = inferKinds (Just True) ty te in

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder case mk of

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder Nothing -> fail $ "constrain '" ++

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder showDoc c "' is unprovable"

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder Just ((_, ks), _) -> if any ( \ j -> lesserKind cm j k) ks

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder then return noC

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder else fail $ "constrain '" ++

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder showDoc c "' is unprovable"

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder ++ "\n known kinds are: " ++

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder concat (intersperse ", " $

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder map (flip showDoc "") ks)

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder Subtyping t1 t2 -> if lesserType te t1 t2 then return noC

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder else fail ("unable to prove: " ++ showDoc t1 " < "

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ++ showDoc t2 "")

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederfreshTypeVarT :: Type -> State Int Type

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederfreshTypeVarT t =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do (var, c) <- freshVar $ getRange t

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder return $ TypeName var (rawKindOfType t) c

772abb916b994ad9461ddb11c88829251c5ac87aChristian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaedertoPairState :: State Int a -> State (Int, b) a

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaedertoPairState p =

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder do (a, b) <- get

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder let (r, c) = runState p a

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder put (c, b)

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder return r

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederaddSubst :: Subst -> State (Int, Subst) ()

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederaddSubst s = do

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder (c, o) <- get

08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder put (c, compSubst o s)

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederswap :: (a, b) -> (b, a)

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederswap (a, b) = (b, a)

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedersubstPairList :: Subst -> [(Type, Type)] -> [(Type, Type)]

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedersubstPairList s = map ( \ (a, b) -> (subst s a, subst s b))

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder-- pre: shapeMatch succeeds

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaedershapeMgu :: TypeEnv -> [(Type, Type)] -> State (Int, Subst) [(Type, Type)]

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaedershapeMgu te cs =

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder let (atoms, structs) = partition ( \ p -> case p of

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (TypeName _ _ _, TypeName _ _ _) -> True

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder _ -> False) cs

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder in if null structs then return atoms else

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder let (t1, t2) = head structs

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder tl = tail structs

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder rest = tl ++ atoms

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder in case (t1, t2) of

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (ExpandedType _ t, _) -> shapeMgu te $ (t, t2) : rest

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder (_, ExpandedType _ t) -> shapeMgu te $ (t1, t) : rest

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (TypeAppl (TypeName l _ _) t, _) | l == lazyTypeId ->

shapeMgu te $ (t, t2) : rest

(_, TypeAppl (TypeName l _ _) t) | l == lazyTypeId ->

shapeMgu te $ (t1, t) : rest

(KindedType t _ _, _) -> shapeMgu te $ (t, t2) : rest

(_, KindedType t _ _) -> shapeMgu te $ (t1, t) : rest

(TypeName _ _ v1, TypeAppl f a) ->

if hasRedex t2 then shapeMgu te $ (t1, redStep t2) : rest else

if v1 > 0 then do

vf <- toPairState $ freshTypeVarT f

va <- toPairState $ freshTypeVarT a

let s = Map.singleton v1 (TypeAppl vf va)

addSubst s

shapeMgu te $ (vf, f) : (case rawKindOfType vf of

FunKind CoVar _ _ _ -> [(va, a)]

FunKind ContraVar _ _ _ -> [(a, va)]

_ -> [(a, va), (va, a)]) ++ substPairList s rest

else error ("shapeMgu1: " ++ showDoc t1 " < " ++ showDoc t2 "")

(TypeName _ _ v1, TypeAbs _ _ _) -> if v1 > 0 then do

let s = Map.singleton v1 t2

addSubst s

shapeMgu te $ substPairList s rest

else error ("shapeMgu1: " ++ showDoc t1 " < " ++ showDoc t2 "")

(_, TypeName _ _ _) -> do

ats <- shapeMgu te ((t2, t1) : map swap rest)

return $ map swap ats

(TypeAppl f1 a1, TypeAppl f2 a2) -> let

Result _ ms1 = if hasRedex t1 then

shapeMatch (typeMap te) (redStep t1) t2 else fail "shapeMatch1"

Result _ ms2 = if hasRedex t2 then

shapeMatch (typeMap te) t1 (redStep t2) else fail "shapeMatch2"

res = shapeMgu te $ (f1, f2) :

case (rawKindOfType f1, rawKindOfType f2) of

(FunKind CoVar _ _ _,

FunKind CoVar _ _ _) -> (a1, a2) : rest

(FunKind ContraVar _ _ _,

FunKind ContraVar _ _ _) -> (a2, a1) : rest

_ -> (a1, a2) : (a2, a1) : rest

in case ms1 of

Nothing -> case ms2 of

Nothing -> res

Just _ -> shapeMgu te $ (t1, redStep t2) : rest

Just _ -> shapeMgu te $ (redStep t1, t2) : rest

_ -> if t1 == t2 then shapeMgu te rest else

error ("shapeMgu2: " ++ showDoc t1 " < " ++ showDoc t2 "")

shapeUnify :: TypeEnv -> [(Type, Type)] -> State Int (Subst, [(Type, Type)])

shapeUnify te l = do

c <- get

let (r, (n, s)) = runState (shapeMgu te l) (c, eps)

put n

return (s, r)

-- input an atomized constraint list

collapser :: Rel.Rel Type -> Result Subst

collapser r =

let t = Rel.sccOfClosure r

ks = map (Set.partition ( \ e -> case e of

TypeName _ _ n -> n==0

_ -> error "collapser")) t

ws = filter (hasMany . fst) ks

in if null ws then

return $ foldr ( \ (cs, vs) s ->

if Set.null cs then

extendSubst s $ Set.deleteFindMin vs

else extendSubst s (Set.findMin cs, vs)) eps ks

else Result

(map ( \ (cs, _) ->

let (c1, rs) = Set.deleteFindMin cs

c2 = Set.findMin rs

in Diag Hint ("contradicting type inclusions for '"

++ showDoc c1 "' and '"

++ showDoc c2 "'") nullRange) ws) Nothing

extendSubst :: Subst -> (Type, Set.Set Type) -> Subst

extendSubst s (t, vs) = Set.fold ( \ (TypeName _ _ n) ->

Map.insert n t) s vs

-- | partition into qualification and subtyping constraints

partitionC :: Constraints -> (Constraints, Constraints)

partitionC = Set.partition ( \ c -> case c of

Kinding _ _ -> True

Subtyping _ _ -> False)

-- | convert subtypings constrains to a pair list

toListC :: Constraints -> [(Type, Type)]

toListC l = [ (t1, t2) | Subtyping t1 t2 <- Set.toList l ]

shapeMatchPairList :: TypeMap -> [(Type, Type)] -> Result Subst

shapeMatchPairList tm l = case l of

[] -> return eps

(t1, t2) : rt -> do

s1 <- shapeMatch tm t1 t2

s2 <- shapeMatchPairList tm $ substPairList s1 rt

return $ compSubst s1 s2

shapeRel :: TypeEnv -> Constraints

-> State Int (Result (Subst, Constraints, Rel.Rel Type))

shapeRel te cs =

let (qs, subS) = partitionC cs

subL = toListC subS

in case shapeMatchPairList (typeMap te) subL of

Result ds Nothing -> return $ Result ds Nothing

_ -> do (s1, atoms) <- shapeUnify te subL

let r = Rel.transClosure $ Rel.fromList atoms

es = Map.foldWithKey ( \ t1 st l1 ->

case t1 of

TypeName _ _ 0 -> Set.fold ( \ t2 l2 ->

case t2 of

TypeName _ _ 0 -> if lesserType te t1 t2

then l2 else (t1, t2) : l2

_ -> l2) l1 st

_ -> l1) [] $ Rel.toMap r

return $ if null es then

case collapser r of

Result ds Nothing -> Result ds Nothing

Result _ (Just s2) ->

let s = compSubst s1 s2

in return (s, substC s qs,

Rel.fromList $ substPairList s2 atoms)

else Result (map ( \ (t1, t2) ->

mkDiag Hint "rejected" $

Subtyping t1 t2) es) Nothing

-- | compute monotonicity of a type variable

monotonic :: TypeEnv -> Int -> Type -> (Bool, Bool)

monotonic te v t =

case t of

TypeName _ _ i -> (True, i /= v)

TypeAppl t1 t2 ->

if hasRedex t then monotonic te v $ redStep t else let

(a1, a2) = monotonic te v t2

(f1, f2) = monotonic te v t1

in case rawKindOfType t1 of

FunKind CoVar _ _ _ -> (f1 && a1, f2 && a2)

FunKind ContraVar _ _ _ -> (f1 && a2, f2 && a1)

_ -> (f1 && a1 && a2, f2 && a1 && a2)

_ -> monotonic te v (stripType "monotonic" t)

-- | find monotonicity based instantiation

monoSubst :: TypeEnv -> Rel.Rel Type -> Type -> Subst

monoSubst te r t =

let varSet = Set.fromList . leaves (> 0)

vs = Set.toList $ Set.union (varSet t) $ Set.unions $ map varSet

$ Set.toList $ Rel.nodes r

monos = filter ( \ (i, (n, rk)) -> case monotonic te i t of

(True, _) -> isSingleton

(Rel.predecessors r $

TypeName n rk i)

_ -> False) vs

antis = filter ( \ (i, (n, rk)) -> case monotonic te i t of

(_, True) -> isSingleton

(Rel.succs r $

TypeName n rk i)

_ -> False) vs

resta = filter ( \ (i, (n, rk)) -> case monotonic te i t of

(True, True) -> hasMany $

Rel.succs r $ TypeName n rk i

_ -> False) vs

restb = filter ( \ (i, (n, rk)) -> case monotonic te i t of

(True, True) -> hasMany $

Rel.predecessors r $ TypeName n rk i

_ -> False) vs

in if null antis then

if null monos then

if null resta then

if null restb then eps else

let (i, (n, rk)) = head restb

tn = TypeName n rk i

s = Rel.predecessors r tn

sl = Set.delete tn $ foldl1 Set.intersection

$ map (Rel.succs r)

$ Set.toList s

in Map.singleton i $ Set.findMin $ if Set.null sl then s

else sl

else let (i, (n, rk)) = head resta

tn = TypeName n rk i

s = Rel.succs r tn

sl = Set.delete tn $ foldl1 Set.intersection

$ map (Rel.predecessors r)

$ Set.toList s

in Map.singleton i $ Set.findMin $ if Set.null sl then s

else sl

else Map.fromDistinctAscList $ map ( \ (i, (n, rk)) ->

(i, Set.findMin $ Rel.predecessors r $

TypeName n rk i)) monos

else Map.fromDistinctAscList $ map ( \ (i, (n, rk)) ->

(i, Set.findMin $ Rel.succs r $

TypeName n rk i)) antis

monoSubsts :: TypeEnv -> Rel.Rel Type -> Type -> Subst

monoSubsts te r t =

let s = monoSubst te (Rel.transReduce $ Rel.irreflex r) t in

if Map.null s then s else

compSubst s $

monoSubsts te (Rel.transClosure $ Rel.map (subst s) r)

$ subst s t

fromTypeMap :: TypeMap -> Rel.Rel Type

fromTypeMap = Map.foldWithKey (\ t ti r -> let k = typeKind ti in

Set.fold ( \ j -> Rel.insert (TypeName t k 0)

$ TypeName j k 0) r

$ superTypes ti) Rel.empty