2155N/A{- |

2155N/AModule : $Header$

2155N/ADescription : choose a minimal type for overloaded terms

2155N/ACopyright : (c) Christian Maeder and Uni Bremen 2003

2155N/ALicense : GPLv2 or higher, see LICENSE.txt

2155N/A

2155N/AMaintainer : Christian.Maeder@dfki.de

2155N/AStability : experimental

2155N/APortability : portable

2155N/A

2155N/Achoose a minimal type

2155N/A-}

2155N/A

2155N/Amodule HasCASL.MinType

2155N/A ( q2p

2155N/A , typeNub

2155N/A , haveCommonSupertype

2155N/A , getCommonSupertype

2155N/A ) where

2155N/A

2155N/Aimport HasCASL.As

2155N/Aimport HasCASL.FoldType

2155N/Aimport HasCASL.Le

2155N/Aimport HasCASL.AsUtils

2155N/Aimport HasCASL.TypeAna

2155N/Aimport HasCASL.Unify

2155N/Aimport HasCASL.Constrain

2155N/A

2155N/Aimport qualified Data.Set as Set

2155N/Aimport qualified Data.Map as Map

2155N/Aimport qualified Common.Lib.Rel as Rel

2155N/Aimport Common.DocUtils

2155N/Aimport Common.Id

2155N/Aimport Common.Result

2155N/Aimport Common.Lib.State

2155N/Aimport Common.Utils

2155N/A

2155N/Aimport Data.List as List

2155N/Aimport Data.Maybe

2155N/A

2155N/Aq2p :: (a, b, c, d) -> (c, d)

2155N/Aq2p (_, _, c, d) = (c,d)

2155N/A

2155N/AtypeNub :: Env -> (a -> (Type, Term)) -> [a] -> [a]

2155N/AtypeNub e f = let

2155N/A comp (ty1, t1) (ty2, t2) = eqTerm e t1 t2 &&

2155N/A lesserType e ty1 ty2

2155N/A lt a b = comp (f a) (f b)

2155N/A in keepMins lt

2155N/A

2155N/AeqTerm :: Env -> Term -> Term -> Bool

2155N/AeqTerm e t1 t2 = case (t1, t2) of

2155N/A (TypedTerm t _ _ _, _) -> eqTerm e t t2

2155N/A (_, TypedTerm t _ _ _) -> eqTerm e t1 t

2155N/A (QualVar (VarDecl v1 _s1 _ _), QualVar (VarDecl v2 _s2 _ _)) ->

2155N/A v1 == v2

2155N/A (QualOp _ i1 s1 _ _ _, QualOp _ i2 s2 _ _ _) -> i1 == i2

2155N/A && haveCommonSupertype e s1 s2

2155N/A (ApplTerm tf1 ta1 _, ApplTerm tf2 ta2 _) ->

2155N/A eqTerm e tf1 tf2 && eqTerm e ta1 ta2

2155N/A (TupleTerm ts1 _, TupleTerm ts2 _) ->

2155N/A length ts1 == length ts2 && and (zipWith (eqTerm e) ts1 ts2)

2155N/A (QuantifiedTerm q1 vs1 f1 _, QuantifiedTerm q2 vs2 f2 _) ->

2155N/A (q1, vs1) == (q2, vs2) && eqTerm e f1 f2

2155N/A (LambdaTerm ps1 p1 f1 _, LambdaTerm ps2 p2 f2 _) ->

2155N/A and (zipWith (eqTerm e) ps1 ps2) && p1 == p2 && eqTerm e f1 f2

2155N/A && length ps1 == length ps2

2155N/A (CaseTerm f1 e1 _, CaseTerm f2 e2 _) ->

2155N/A eqTerm e f1 f2 && length e1 == length e2

2155N/A && and (zipWith (eqProgEq e) e1 e2)

2155N/A (LetTerm _ e1 f1 _, LetTerm _ e2 f2 _) ->

2155N/A eqTerm e f1 f2 && length e1 == length e2

2155N/A && and (zipWith (eqProgEq e) e1 e2)

_ -> False

eqProgEq :: Env -> ProgEq -> ProgEq -> Bool

eqProgEq e (ProgEq p1 t1 _) (ProgEq p2 t2 _) = eqTerm e p1 p2 && eqTerm e t1 t2

addToEnv :: (Type, VarKind) -> Env -> Env

addToEnv (ty, vk) e = case ty of

TypeName i rk c | c > 0 ->

execState (addLocalTypeVar False (TypeVarDefn NonVar vk rk c) i) e

_ -> e

haveCommonSupertype :: Env -> TypeScheme -> TypeScheme -> Bool

haveCommonSupertype e s = isJust . getCommonSupertype e s

getCommonSupertype :: Env -> TypeScheme -> TypeScheme -> Maybe TypeTriple

getCommonSupertype e s1 s2 =

evalState (toEnvState $ haveCommonSupertypeE e s1 s2) e

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

haveCommonSupertypeE :: Env -> TypeScheme -> TypeScheme

-> State Int (Maybe TypeTriple)

haveCommonSupertypeE eIn s1 s2 = do

(t1, l1) <- freshInst s1

(t2, l2) <- freshInst s2

cst <- mkSingleSubst (genName "commonSupertype", rStar)

let cs = Set.fromList [Subtyping t1 cst, Subtyping t2 cst]

e = foldr addToEnv eIn $ (cst, VarKind universe) : l1 ++ l2

Result _ mr <- shapeRelAndSimplify False e cs (Just cst)

return $ case mr of

Nothing -> Nothing

Just (sbst, rcs) -> let (qs, subC) = partitionC rcs

in case reduceCommonSubtypes

(Rel.transClosure $ fromTypeMap $ typeMap e)

(toListC subC) of

Just msb | Set.null qs -> let

doSubst = subst $ compSubst sbst msb

[ty, ty1, ty2] = map doSubst [cst, t1, t2]

fvs = foldr1 List.union $ map freeTVars [ty1, ty2, ty]

svs = sortBy comp fvs

comp a b = compare (fst a) $ fst b

tvs = localTypeVars e

newArgs = map ( \ (_, (i, _)) -> case Map.lookup i tvs of

Nothing -> error $ "generalizeS " ++ show (i, ty)

++ "\n" ++ showDoc (s1, s2) ""

Just (TypeVarDefn v vk rk c) ->

TypeArg i v vk rk c Other nullRange) svs

genArgs = generalize newArgs

[gty, gty1, gty2] = map genArgs [ty, ty1, ty2]

gl1 = map (genArgs . doSubst . fst) l1

gl2 = map (genArgs . doSubst . fst) l2

in Just (gty1, gl1, gty2, gl2, genTypeArgs newArgs, gty)

_ -> Nothing

reduceCommonSubtypes :: Rel.Rel Type -> [(Type, Type)] -> Maybe Subst

reduceCommonSubtypes e l = let

mygroup = groupBy ( \ (a, b) (c, d) -> case (a, b, d) of

(TypeName _ _ n, TypeName _ _ 0, TypeName _ _ 0)

-> n > 0 && a == c

_ -> False)

mypart = partition ( \ s -> case s of

[] -> error "reduceCommonSubtypes1"

[_] -> False

_ -> True)

(csubts, rest) = mypart $ mygroup l

swap = map $ \ (a, b) -> (b, a)

(csuperts, rest2) = mypart $ mygroup $ sort $ swap (concat rest)

mkPair s = case s of

(a, _) : _ -> (a, map snd s)

_ -> error "reduceCommonSubtypes2"

subM = mapM (commonSubtype e True . mkPair) csubts

superM = mapM (commonSubtype e False . mkPair) csuperts

in case (concat rest2, subM, superM) of

([], Just l1, Just l2) -> Just $ Map.fromList $ l1 ++ l2

_ -> Nothing

commonSubtype :: Rel.Rel Type -> Bool -> (Type, [Type]) -> Maybe (Int, Type)

commonSubtype trel b (ty, l) =

let tySet = foldl1 Set.intersection

$ map (if b then Rel.predecessors trel else Rel.succs trel) l

in case ty of

TypeName _ _ n | not (Set.null tySet) && n > 0

-> Just (n, Set.findMin tySet)

_ -> Nothing