{- |

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 (_, _, c, d) = (c, d)

typeNub :: Env -> (a -> (Type, Term)) -> [a] -> [a]

typeNub e f = let

comp (ty1, t1) (ty2, t2) = eqTerm e t1 t2 &&

lesserType e ty1 ty2

lt a b = comp (f a) (f b)

in keepMins lt

eqTerm :: Env -> Term -> Term -> Bool

eqTerm e t1 t2 = case (t1, t2) of

(TypedTerm t _ _ _, _) -> eqTerm e t t2

(_, TypedTerm t _ _ _) -> eqTerm e t1 t

(QualVar (VarDecl v1 _s1 _ _), QualVar (VarDecl v2 _s2 _ _)) ->

v1 == v2

(QualOp _ i1 s1 _ _ _, QualOp _ i2 s2 _ _ _) -> i1 == i2

&& haveCommonSupertype e s1 s2

(ApplTerm tf1 ta1 _, ApplTerm tf2 ta2 _) ->

eqTerm e tf1 tf2 && eqTerm e ta1 ta2

(TupleTerm ts1 _, TupleTerm ts2 _) ->

length ts1 == length ts2 && and (zipWith (eqTerm e) ts1 ts2)

(QuantifiedTerm q1 vs1 f1 _, QuantifiedTerm q2 vs2 f2 _) ->

(q1, vs1) == (q2, vs2) && eqTerm e f1 f2

(LambdaTerm ps1 p1 f1 _, LambdaTerm ps2 p2 f2 _) ->

and (zipWith (eqTerm e) ps1 ps2) && p1 == p2 && eqTerm e f1 f2

&& length ps1 == length ps2

(CaseTerm f1 e1 _, CaseTerm f2 e2 _) ->

eqTerm e f1 f2 && length e1 == length e2

&& and (zipWith (eqProgEq e) e1 e2)

(LetTerm _ e1 f1 _, LetTerm _ e2 f2 _) ->

eqTerm e f1 f2 && length e1 == length e2

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