MinType.hs revision 3bffe0f10ad93403e36288a1a4a92d50356956b5
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederModule : $Header$
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederDescription : choose a minimal type for overloaded terms
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederCopyright : (c) Christian Maeder and Uni Bremen 2003
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederMaintainer : Christian.Maeder@dfki.de
d31090850b029162859d0aedf45bae2a83d7b673Jonathan von SchroederStability : experimental
d31090850b029162859d0aedf45bae2a83d7b673Jonathan von SchroederPortability : portable
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederchoose a minimal type
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroedermodule HasCASL.MinType (q2p, typeNub, haveCommonSupertype) where
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederimport qualified Data.Set as Set
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederimport qualified Data.Map as Map
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederimport qualified Common.Lib.Rel as Rel
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroederq2p :: (a, b, c, d) -> (c, d)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroederq2p (_, _, c, d) = (c,d)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von SchroedertypeNub :: Env -> (a -> (Type, Term)) -> [a] -> [a]
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von SchroedertypeNub e f = let
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder comp (ty1, t1) (ty2, t2) = eqTerm e t1 t2 &&
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder lesserType e ty1 ty2
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder lt a b = comp (f a) (f b)
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von SchroedereqTerm :: Env -> Term -> Term -> Bool
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroedereqTerm e t1 t2 = case (t1, t2) of
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder (TypedTerm t _ _ _, _) -> eqTerm e t t2
19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von Schroeder (_, TypedTerm t _ _ _) -> eqTerm e t1 t
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder (QualVar (VarDecl v1 _s1 _ _), QualVar (VarDecl v2 _s2 _ _)) ->
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder (QualOp _ i1 s1 _ _ _, QualOp _ i2 s2 _ _ _) -> i1 == i2
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroeder && haveCommonSupertype e s1 s2
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder (ApplTerm tf1 ta1 _, ApplTerm tf2 ta2 _) ->
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder eqTerm e tf1 tf2 && eqTerm e ta1 ta2
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder (TupleTerm ts1 _, TupleTerm ts2 _) ->
f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroeder length ts1 == length ts2 && and (zipWith (eqTerm e) ts1 ts2)
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder (QuantifiedTerm q1 vs1 f1 _, QuantifiedTerm q2 vs2 f2 _) ->
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder (q1, vs1) == (q2, vs2) && eqTerm e f1 f2
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder (LambdaTerm ps1 p1 f1 _, LambdaTerm ps2 p2 f2 _) ->
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder and (zipWith (eqTerm e) ps1 ps2) && p1 == p2 && eqTerm e f1 f2
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder && length ps1 == length ps2
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder (CaseTerm f1 e1 _, CaseTerm f2 e2 _) ->
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder eqTerm e f1 f2 && length e1 == length e2
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder && and (zipWith (eqProgEq e) e1 e2)
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder (LetTerm _ e1 f1 _, LetTerm _ e2 f2 _) ->
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder eqTerm e f1 f2 && length e1 == length e2
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder && and (zipWith (eqProgEq e) e1 e2)
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroedereqProgEq :: Env -> ProgEq -> ProgEq -> Bool
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroedereqProgEq e (ProgEq p1 t1 _) (ProgEq p2 t2 _) = eqTerm e p1 p2 && eqTerm e t1 t2
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von SchroederaddToEnv :: (Type, VarKind) -> Env -> Env
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von SchroederaddToEnv (ty, vk) e = case ty of
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder TypeName i rk c | c > 0 ->
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder execState (addLocalTypeVar False (TypeVarDefn NonVar vk rk c) i) e
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von SchroederhaveCommonSupertype :: Env -> TypeScheme -> TypeScheme -> Bool
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von SchroederhaveCommonSupertype e s1 s2 =
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder evalState (toEnvState $ haveCommonSupertypeE e s1 s2) e
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von SchroederhaveCommonSupertypeE :: Env -> TypeScheme -> TypeScheme -> State Int Bool
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von SchroederhaveCommonSupertypeE eIn s1 s2 = do
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder (t1, l1) <- freshInst s1
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder (t2, l2) <- freshInst s2
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder cst <- mkSingleSubst (genName "commonSupertype", rStar)
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder let cs = Set.fromList [Subtyping t1 cst, Subtyping t2 cst]
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder e = foldr addToEnv eIn $ l1 ++ l2
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder Result _ mr <- shapeRelAndSimplify False e cs (Just cst)
f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroeder return $ case mr of
d40eeef0175161a089443ba027dcb635ed11a1bdJonathan von Schroeder Nothing -> False
d40eeef0175161a089443ba027dcb635ed11a1bdJonathan von Schroeder Just (_, rcs) -> let (qs, subC) = partitionC rcs
d40eeef0175161a089443ba027dcb635ed11a1bdJonathan von Schroeder && reduceCommonSubtypes (Rel.transClosure $ fromTypeMap $ typeMap e)
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von SchroederreduceCommonSubtypes :: Rel.Rel Type -> [(Type, Type)] -> Bool
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von SchroederreduceCommonSubtypes e l = let
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder mygroup = groupBy ( \ (a, b) (c, d) -> case (a, b, d) of
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder (TypeName _ _ n, TypeName _ _ 0, TypeName _ _ 0)
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder -> n > 0 && a == c
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder mypart = partition ( \ s -> case s of
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder [] -> error "reduceCommonSubtypes1"
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder (csubts, rest) = mypart $ mygroup l
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder swap = map $ \ (a, b) -> (b, a)
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder (csuperts, rest2) = mypart $ mygroup $ sort $ swap (concat rest)
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder mkPair s = case s of
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder (a, _) : _ -> (a, map snd s)
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder _ -> error "reduceCommonSubtypes2"
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder in null (concat rest2) && and (map (commonSubtype e True . mkPair) csubts)
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder && and (map (commonSubtype e False . mkPair) csuperts)
19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von SchroedercommonSubtype :: Rel.Rel Type -> Bool -> (Type, [Type]) -> Bool
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroedercommonSubtype e b (a, l) = case l of
4cd542a7f4e378ab5a36b49da804b258442b13f9Jonathan von Schroeder let c1 = commonSubtype e b (a, c : r)
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroeder c2 = commonSubtype e b (a, d : r)
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder in commonSubtypeId e b c d && (c1 || c2)
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder || any ( \ f -> commonSubtypeId e b c f
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder && commonSubtypeId e b d f) r
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder _ -> error "commonSubtype"
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von SchroedercommonSubtypeId :: Rel.Rel Type -> Bool -> Type -> Type -> Bool
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von SchroedercommonSubtypeId e b c d = let tm = Rel.toMap e in
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder $ Map.filter ( \ s -> Set.member c s && Set.member d s) tm