db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiuCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

1ac3b05a1cf2b8169242608c0884ec2fab5a4f29Felix Gabriel ManceMaintainer : maeder@tzi.de

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiuStability : experimental

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiuPortability : portable

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuconstraint resolution

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu-}

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiumodule HasCASL.Constrain where

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuimport HasCASL.Unify

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuimport HasCASL.As

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuimport HasCASL.AsUtils

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuimport HasCASL.Le

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuimport HasCASL.TypeAna

1ac3b05a1cf2b8169242608c0884ec2fab5a4f29Felix Gabriel Manceimport HasCASL.ClassAna

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuimport qualified Common.Lib.Set as Set

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuimport qualified Common.Lib.Map as Map

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuimport qualified Common.Lib.Rel as Rel

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuimport Common.Lib.State

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuimport Common.PrettyPrint

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuimport Common.Lib.Pretty

1ac3b05a1cf2b8169242608c0884ec2fab5a4f29Felix Gabriel Manceimport Common.Keywords

1ac3b05a1cf2b8169242608c0884ec2fab5a4f29Felix Gabriel Manceimport Common.Id

45e34c7696f9dd6163686ff6798b33a126590fa2Felix Gabriel Manceimport Common.Result

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuimport Data.List

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuimport Data.Maybe

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiudata Constrain = Kinding Type Kind

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu | Subtyping Type Type

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu deriving (Eq, Ord, Show)

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuinstance PrettyPrint Constrain where

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu printText0 ga c = case c of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Kinding ty k -> printText0 ga ty <+> colon

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu <+> printText0 ga k

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Subtyping t1 t2 -> printText0 ga t1 <+> text lessS

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu <+> printText0 ga t2

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuinstance PosItem Constrain where

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu getRange c = case c of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Kinding ty _ -> getRange ty

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Subtyping t1 t2 -> getRange t1 `appRange` getRange t2

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiutype Constraints = Set.Set Constrain

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiunoC :: Constraints

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiunoC = Set.empty

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiujoinC :: Constraints -> Constraints -> Constraints

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiujoinC = Set.union

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiuinsertC :: Constrain -> Constraints -> Constraints

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiuinsertC c = case c of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Subtyping t1 t2 -> if t1 == t2 then id else Set.insert c

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Kinding _ k -> if k == star then id else Set.insert c

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiusubstC :: Subst -> Constraints -> Constraints

0a65899b09e78455a94af9128455f6613441ab71cmaedersubstC s = Set.fold (insertC . ( \ c -> case c of

0a65899b09e78455a94af9128455f6613441ab71cmaeder Kinding ty k -> Kinding (subst s ty) k

0a65899b09e78455a94af9128455f6613441ab71cmaeder Subtyping t1 t2 -> Subtyping (subst s t1) $ subst s t2)) noC

0a65899b09e78455a94af9128455f6613441ab71cmaeder

0a65899b09e78455a94af9128455f6613441ab71cmaedersimplify :: TypeEnv -> Constraints -> ([Diagnosis], Constraints)

0a65899b09e78455a94af9128455f6613441ab71cmaedersimplify te rs =

0a65899b09e78455a94af9128455f6613441ab71cmaeder if Set.null rs then ([], noC)

e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder else let (r, rt) = Set.deleteFindMin rs

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Result ds m = entail te r

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (es, cs) = simplify te rt

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu in (ds ++ es, case m of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Just _ -> cs

45e34c7696f9dd6163686ff6798b33a126590fa2Felix Gabriel Mance Nothing -> insertC r cs)

e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder

e24ad3f655daa60ddabe690e4b11de3187996c16cmaederentail :: Monad m => TypeEnv -> Constrain -> m ()

e24ad3f655daa60ddabe690e4b11de3187996c16cmaederentail te p =

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu do is <- byInst te p

1ac3b05a1cf2b8169242608c0884ec2fab5a4f29Felix Gabriel Mance mapM_ (entail te) $ Set.toList is

e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder

e24ad3f655daa60ddabe690e4b11de3187996c16cmaederbyInst :: Monad m => TypeEnv -> Constrain -> m Constraints

e24ad3f655daa60ddabe690e4b11de3187996c16cmaederbyInst te c = let cm = classMap te in case c of

e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder Kinding ty k -> case ty of

1ac3b05a1cf2b8169242608c0884ec2fab5a4f29Felix Gabriel Mance ExpandedType _ t -> byInst te $ Kinding t k

45e34c7696f9dd6163686ff6798b33a126590fa2Felix Gabriel Mance _ -> if k == star then return noC else case k of

45e34c7696f9dd6163686ff6798b33a126590fa2Felix Gabriel Mance ExtKind ek _ _ -> byInst te (Kinding ty ek)

e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder ClassKind _ -> let (topTy, args) = getTypeAppl ty in

e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder case topTy of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu TypeName i _ _ -> let Result _ mk = getIdKind te i in

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu case mk of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Nothing -> fail $ "remaining variable '"

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu ++ showPretty i "'"

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Just ((_, ks), _) -> do

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu if null args then

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu if any ( \ j -> lesserKind cm j k) ks

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu then return noC

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu else fail $ "constrain '" ++

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu showPretty c "' is unprovable"

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu ++ "\n known kinds are: " ++

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu showPretty ks ""

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu else do

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu let kas = concatMap ( \ j ->

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu getKindAppl cm j args) ks

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu newKs <- dom cm k kas

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu return $ Set.fromList $ zipWith Kinding args newKs

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu _ -> error "byInst: unexpected Type"

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu _ -> error "byInst: unexpected Kind"

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Subtyping t1 t2 -> if lesserType te t1 t2 then return noC

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu else fail ("unable to prove: " ++ showPretty t1 " < "

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu ++ showPretty t2 "")

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiumaxKind :: ClassMap -> Kind -> Kind -> Maybe Kind

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiumaxKind cm k1 k2 = if lesserKind cm k1 k2 then Just k1 else

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu if lesserKind cm k2 k1 then Just k2 else Nothing

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiumaxKinds :: ClassMap -> [Kind] -> Maybe Kind

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiumaxKinds cm l = case l of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu [] -> Nothing

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu [k] -> Just k

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu [k1, k2] -> maxKind cm k1 k2

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu k1 : k2 : ks -> case maxKind cm k1 k2 of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Just k -> maxKinds cm (k : ks)

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Nothing -> do k <- maxKinds cm (k2 : ks)

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu maxKind cm k1 k

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiumaxKindss :: ClassMap -> [[Kind]] -> Maybe [Kind]

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiumaxKindss cm l = let margs = map (maxKinds cm) $ transpose l in

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu if all isJust margs then Just $ map fromJust margs

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu else Nothing

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiudom :: Monad m => ClassMap -> Kind -> [([Kind], Kind)] -> m [Kind]

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiudom cm k ks =

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu let fks = filter ( \ (_, rk) -> lesserKind cm rk k ) ks

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu margs = maxKindss cm $ map fst fks

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu in if null fks then fail ("class not found " ++ showPretty k "")

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu else case margs of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Nothing -> fail "dom: maxKind"

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Just args -> if any ((args ==) . fst) fks then return args

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu else fail "dom: not coregular"

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiufreshTypeVarT :: Type -> State Int Type

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiufreshTypeVarT t =

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu do (var, c) <- freshVar $ posOfType t

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu return $ TypeName var (rawKindOfType t) c

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiufreshVarsT :: [Type] -> State Int [Type]

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiufreshVarsT l = mapM freshTypeVarT l

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiutoPairState :: State Int a -> State (Int, b) a

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiutoPairState p =

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu do (a, b) <- get

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu let (r, c) = runState p a

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu put (c, b)

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu return r

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiuaddSubst :: Subst -> State (Int, Subst) ()

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiuaddSubst s = do

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (c, o) <- get

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu put (c, compSubst o s)

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuswap :: (a, b) -> (b, a)

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiuswap (a, b) = (b, a)

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiusubstPairList :: Subst -> [(Type, Type)] -> [(Type, Type)]

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiusubstPairList s = map ( \ (a, b) -> (subst s a, subst s b))

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu-- pre: shapeMatch succeeds

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiushapeMgu :: TypeEnv -> [(Type, Type)] -> State (Int, Subst) [(Type, Type)]

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiushapeMgu te cs =

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu let (atoms, structs) = partition ( \ p -> case p of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (TypeName _ _ _, TypeName _ _ _) -> True

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu _ -> False) cs

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu in if null structs then return atoms else

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu let p@(t1, t2) = head structs

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu tl = tail structs

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu rest = tl ++ atoms

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu in case p of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (ExpandedType _ t, _) -> shapeMgu te $ (t, t2) : rest

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (_, ExpandedType _ t) -> shapeMgu te $ (t1, t) : rest

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (LazyType t _, _) -> shapeMgu te $ (t, t2) : rest

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (_, LazyType t _) -> shapeMgu te $ (t1, t) : rest

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

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

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (ProductType _ _, _) -> shapeMgu te $ (convertType t1, t2) : rest

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (_, ProductType _ _) -> shapeMgu te $ (t1, convertType t2) : rest

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (FunType _ _ _ _, _) -> shapeMgu te $ (convertType t1, t2) : rest

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (_, FunType _ _ _ _) -> shapeMgu te $ (t1, convertType t2) : rest

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (TypeName _ _ v1, TypeAppl f a) -> if (v1 > 0) then do

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu vf <- toPairState $ freshTypeVarT f

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu va <- toPairState $ freshTypeVarT a

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

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu addSubst s

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

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu FunKind (ExtKind _ CoVar _) _ _ -> [(va, a)]

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu FunKind (ExtKind _ ContraVar _) _ _ -> [(a, va)]

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

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu else error ("shapeMgu1: " ++ showPretty t1 " < " ++ showPretty t2 "")

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (_, TypeName _ _ _) -> do ats <- shapeMgu te ((t2, t1) : map swap rest)

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu return $ map swap ats

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (TypeAppl f1 a1, TypeAppl f2 a2) ->

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu shapeMgu te $ (f1, f2) : case (rawKindOfType f1, rawKindOfType f2) of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (FunKind (ExtKind _ CoVar _) _ _,

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu FunKind (ExtKind _ CoVar _) _ _) -> (a1, a2) : rest

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (FunKind (ExtKind _ ContraVar _) _ _,

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu FunKind (ExtKind _ ContraVar _) _ _) -> (a2, a1) : rest

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu _ -> (a1, a2) : (a2, a1) : rest

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu _ -> error ("shapeMgu2: " ++ showPretty t1 " < " ++ showPretty t2 "")

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiuzipC :: Kind -> (Type, Type) -> [(Type, Type)]

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiuzipC k p = let q = swap p in case k of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu ExtKind _ CoVar _ -> [p]

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu ExtKind _ ContraVar _ -> [q]

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu _ -> [p,q]

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiushapeUnify :: TypeEnv -> [(Type, Type)] -> State Int (Subst, [(Type, Type)])

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiushapeUnify te l = do

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu c <- get

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

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu put n

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu return (s, r)

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiugetRawKindAppl :: Kind -> [a] -> (Kind, [Kind])

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiugetRawKindAppl k args = if null args then (k, []) else

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu case k of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu FunKind k1 k2 _ -> let (rk, ks) = getRawKindAppl k2 (tail args)

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu in (rk, k1 : ks)

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu ExtKind ek _ _ -> getRawKindAppl ek args

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu _ -> error ("getRawKindAppl " ++ show k)

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu-- input an atomized constraint list

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiucollapser :: Rel.Rel Type -> Result Subst

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiucollapser r =

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu let t = Rel.sccOfClosure r

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

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu TypeName _ _ n -> n==0

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu _ -> error "collapser")) t

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu ws = filter (\ p -> Set.size (fst p) > 1) ks

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu in if null ws then

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

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu if Set.null cs then

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu extendSubst s $ Set.deleteFindMin vs

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

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu else Result

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (map ( \ (cs, _) ->

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu let (c1, rs) = Set.deleteFindMin cs

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu c2 = Set.findMin rs

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu in Diag Hint ("contradicting type inclusions for '"

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu ++ showPretty c1 "' and '"

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu ++ showPretty c2 "'") nullRange) ws) Nothing

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiuextendSubst :: Subst -> (Type, Set.Set Type) -> Subst

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

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Map.insert n t) s vs

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu-- | partition into qualification and subtyping constraints

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiupartitionC :: Constraints -> (Constraints, Constraints)

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiupartitionC = Set.partition ( \ c -> case c of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Kinding _ _ -> True

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu Subtyping _ _ -> False)

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu-- | convert subtypings constrains to a pair list

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiutoListC :: Constraints -> [(Type, Type)]

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

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiushapeMatchPairList :: TypeMap -> [(Type, Type)] -> Result Subst

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiushapeMatchPairList tm l = case l of

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu [] -> return eps

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu (t1, t2) : rt -> do

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu s1 <- shapeMatch tm t1 t2

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu s2 <- shapeMatchPairList tm $ substPairList s1 rt

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu return $ compSubst s1 s2

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiushapeRel :: TypeEnv -> Constraints

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

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae BungiushapeRel te cs =

db5856552a51bade5696f529676181752cad6a9fFrancisc Nicolae Bungiu 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)

ExpandedType _ t2 -> monotonic te v t2

KindedType tk _ _ -> monotonic te v tk

LazyType tl _ -> monotonic te v tl

_ -> let (top, args) = getTypeAppl t in case top of

TypeName _ k _ ->

let ks = snd $ getRawKindAppl k args

(bs1, bs2) = unzip $ zipWith ( \ rk a ->

let (b1, b2) = monotonic te v a

in case rk of

ExtKind _ CoVar _ -> (b1, b2)

ExtKind _ ContraVar _ -> (b2, b1)

_ -> (b1 && b2, b1 && b2)) ks args

in (and bs1, and bs2)

_ -> error "monotonic"

-- | 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, _) -> 1 == Set.size

(Rel.predecessors r $

TypeName n rk i)

_ -> False) vs

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

(_, True) -> 1 == Set.size

(Rel.succs r $

TypeName n rk i)

_ -> False) vs

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

(True, True) -> 1 < Set.size

(Rel.succs r $

TypeName n rk i)

_ -> False) vs

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

(True, True) -> 1 < Set.size

(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.fromAscList $ map ( \ (i, (n, rk)) ->

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

TypeName n rk i)) monos

else Map.fromAscList $ 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 ->

foldr (Rel.insert (TypeName t (typeKind ti) 0)) r

[ ty | ty@(TypeName _ _ _) <-

superTypes ti ]) Rel.empty