2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann{- |

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannModule : $Header$

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannMaintainer : maeder@tzi.de

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannStability : experimental

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannPortability : portable

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannconstraint resolution

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann-}

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannmodule HasCASL.Constrain where

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport HasCASL.Unify

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport HasCASL.As

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport HasCASL.AsUtils

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport HasCASL.Le

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport HasCASL.TypeAna

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport HasCASL.ClassAna

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport qualified Common.Lib.Set as Set

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport qualified Common.Lib.Map as Map

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport qualified Common.Lib.Rel as Rel

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport Common.Lib.State

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport Common.Id

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport Common.Result

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport Common.Doc

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport Control.Exception(assert)

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport Data.List

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannimport Data.Maybe

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanndata Constrain = Kinding Type Kind

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann | Subtyping Type Type

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann deriving (Eq, Ord, Show)

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanninstance Pretty Constrain where

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann pretty c = case c of

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Kinding ty k -> fsep [pretty ty, colon, pretty k]

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Subtyping t1 t2 -> fsep [pretty t1, less, pretty t2]

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanninstance PosItem Constrain where

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann getRange c = case c of

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Kinding ty _ -> getRange ty

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Subtyping t1 t2 -> getRange t1 `appRange` getRange t2

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmanntype Constraints = Set.Set Constrain

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannnoC :: Constraints

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannnoC = Set.empty

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannjoinC :: Constraints -> Constraints -> Constraints

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannjoinC = Set.union

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmanninsertC :: Constrain -> Constraints -> Constraints

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmanninsertC c = case c of

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Subtyping t1 t2 -> if t1 == t2 then id else Set.insert c

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Kinding _ k -> if k == universe then id else Set.insert c

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannsubstC :: Subst -> Constraints -> Constraints

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannsubstC s = Set.fold (insertC . ( \ c -> case c of

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Kinding ty k -> Kinding (subst s ty) k

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Subtyping t1 t2 -> Subtyping (subst s t1) $ subst s t2)) noC

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannsimplify :: TypeEnv -> Constraints -> ([Diagnosis], Constraints)

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannsimplify te rs =

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann if Set.null rs then ([], noC)

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann else let (r, rt) = Set.deleteFindMin rs

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Result ds m = entail te r

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann (es, cs) = simplify te rt

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann in (ds ++ es, case m of

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Just _ -> cs

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Nothing -> insertC r cs)

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannentail :: Monad m => TypeEnv -> Constrain -> m ()

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannentail te p =

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann do is <- byInst te p

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann mapM_ (entail te) $ Set.toList is

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannbyInst :: Monad m => TypeEnv -> Constrain -> m Constraints

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannbyInst te c = let cm = classMap te in case c of

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Kinding ty k -> if k == universe then

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann assert (rawKindOfType ty == ClassKind ())

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann $ return noC else

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann let Result _ds mk = inferKinds (Just True) ty te in

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann case mk of

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Nothing -> fail $ "constrain '" ++

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann showPretty c "' is unprovable"

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Just ((_, ks), _) -> if any ( \ j -> lesserKind cm j k) ks

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann then return noC

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann else fail $ "constrain '" ++

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann showPretty c "' is unprovable"

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann ++ "\n known kinds are: " ++

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann concat (intersperse ", " $

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann map (flip showPretty "") ks)

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Subtyping t1 t2 -> if lesserType te t1 t2 then return noC

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann else fail ("unable to prove: " ++ showPretty t1 " < "

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann ++ showPretty t2 "")

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannfreshTypeVarT :: Type -> State Int Type

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannfreshTypeVarT t =

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann do (var, c) <- freshVar $ getRange t

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann return $ TypeName var (rawKindOfType t) c

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannfreshVarsT :: [Type] -> State Int [Type]

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannfreshVarsT l = mapM freshTypeVarT l

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmanntoPairState :: State Int a -> State (Int, b) a

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmanntoPairState p =

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann do (a, b) <- get

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann let (r, c) = runState p a

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann put (c, b)

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann return r

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannaddSubst :: Subst -> State (Int, Subst) ()

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannaddSubst s = do

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann (c, o) <- get

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann put (c, compSubst o s)

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannswap :: (a, b) -> (b, a)

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannswap (a, b) = (b, a)

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannsubstPairList :: Subst -> [(Type, Type)] -> [(Type, Type)]

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannsubstPairList s = map ( \ (a, b) -> (subst s a, subst s b))

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann-- pre: shapeMatch succeeds

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannshapeMgu :: TypeEnv -> [(Type, Type)] -> State (Int, Subst) [(Type, Type)]

2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannshapeMgu te cs =

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann let (atoms, structs) = partition ( \ p -> case p of

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann (TypeName _ _ _, TypeName _ _ _) -> True

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann _ -> False) cs

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann in if null structs then return atoms else

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann let p@(t1, t2) = head structs

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann tl = tail structs

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann rest = tl ++ atoms

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann in case p of

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann (ExpandedType _ t, _) -> shapeMgu te $ (t, t2) : rest

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann (_, ExpandedType _ t) -> shapeMgu te $ (t1, t) : rest

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

2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann 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 (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: " ++ showPretty t1 " < " ++ showPretty t2 "")

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

return $ map swap ats

(TypeAppl f1 a1, TypeAppl f2 a2) ->

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

_ -> error ("shapeMgu2: " ++ showPretty t1 " < " ++ showPretty 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 (\ p -> Set.compareSize 1 (fst p) == LT) 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 '"

++ showPretty c1 "' and '"

++ showPretty 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 -> 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 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, _) -> Set.isSingleton

(Rel.predecessors r $

TypeName n rk i)

_ -> False) vs

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

(_, True) -> Set.isSingleton

(Rel.succs r $

TypeName n rk i)

_ -> False) vs

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

(True, True) -> Set.compareSize 1

(Rel.succs r $

TypeName n rk i) == LT

_ -> False) vs

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

(True, True) -> Set.compareSize 1

(Rel.predecessors r $

TypeName n rk i) == LT

_ -> 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