5620N/A{- |

5620N/AModule : $Header$

5620N/ADescription : compute subtype dependencies

5620N/ACopyright : (c) Christian Maeder and Uni Bremen 2003-2005

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

5620N/A

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

5620N/AStability : experimental

5620N/APortability : portable

5620N/A

5620N/Acompute subtype dependencies

5620N/A-}

5620N/A

5620N/Amodule HasCASL.TypeRel where

5620N/A

5620N/Aimport HasCASL.As

5620N/Aimport HasCASL.AsUtils

5620N/Aimport HasCASL.ClassAna

5620N/Aimport HasCASL.Le

5620N/Aimport HasCASL.Builtin

5620N/Aimport HasCASL.DataAna

5620N/Aimport HasCASL.MinType

5620N/A

5620N/Aimport Common.Id

5620N/Aimport Common.AS_Annotation

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

5620N/A

5620N/Aimport qualified Data.Map as Map

5620N/Aimport qualified Data.Set as Set

5620N/Aimport Data.Maybe

5620N/A

5620N/AtypeRel :: TypeMap -> Rel.Rel Id

5620N/AtypeRel = Rel.transReduce . Rel.irreflex . Rel.transClosure

5620N/A . Map.foldrWithKey ( \ i ti r ->

5620N/A Set.fold (Rel.insert i) r $ superTypes ti) Rel.empty

5620N/A

5620N/AgetRawKind :: TypeMap -> Id -> RawKind

5620N/AgetRawKind tm i = typeKind $

5620N/A Map.findWithDefault (error $ showId i " not found in type map") i tm

5620N/A

5620N/A-- | make a polymorphic function from a to b

5620N/AmkInjOrProjType :: Arrow -> TypeScheme

5620N/AmkInjOrProjType arr =

5620N/A TypeScheme [aTypeArg, bTypeArg] (mkFunArrType aType arr bType) nullRange

5620N/A

5620N/AinjType :: TypeScheme

5620N/AinjType = mkInjOrProjType FunArr

5620N/A

5620N/AprojType :: TypeScheme

5620N/AprojType = mkInjOrProjType PFunArr

5620N/A

5620N/AmkInjOrProj :: Arrow -> Set.Set OpInfo

5620N/AmkInjOrProj arr = Set.singleton OpInfo

5620N/A { opType = mkInjOrProjType arr

5620N/A , opAttrs = Set.empty

5620N/A , opDefn = NoOpDefn Fun }

5620N/A

5620N/AsubtRelName :: Id

5620N/AsubtRelName = mkId [genToken "subt"]

5620N/A

5620N/AsubtRelType :: TypeScheme

5620N/AsubtRelType = TypeScheme [aTypeArg, bTypeArg]

5620N/A (mkFunArrType (mkProductType [aType, bType]) PFunArr unitType) nullRange

5620N/A

5620N/AsubtRel :: Set.Set OpInfo

5620N/AsubtRel = Set.singleton OpInfo

5620N/A { opType = subtRelType

5620N/A , opAttrs = Set.empty

5620N/A , opDefn = NoOpDefn Fun }

5620N/A

5620N/AsubtAxioms :: TypeMap -> [Named Sentence]

5620N/AsubtAxioms tm =

5620N/A let tr = typeRel tm in

5620N/A if Rel.null tr then [] else subtReflex : subtTrans : subtInjProj : injTrans

5620N/A : map (subtAx tm) (Rel.toList tr)

5620N/A

5620N/Anr :: Range

5620N/Anr = nullRange

5620N/A

5620N/AgetKindAppl :: RawKind -> [Variance]

5620N/AgetKindAppl rk = case rk of

5620N/A ClassKind () -> []

5620N/A FunKind v _ r _ -> v : getKindAppl r

5620N/A

5620N/AmkTypeArg :: Id -> Int -> TypeArg

5620N/AmkTypeArg i c = TypeArg i NonVar (VarKind universe) rStar c Other nr

5620N/A

5620N/AsubtAx :: TypeMap -> (Id, Id) -> Named Sentence

5620N/AsubtAx tm (i1, i2) = let

5620N/A findType i = Map.findWithDefault

5620N/A (Map.findWithDefault (error "TypeRel.subtAx") i bTypes) i tm

5620N/A e1 = findType i1

5620N/A e2 = findType i2

5620N/A txt = shows i1 "_<_" ++ show i2

5620N/A l1 = getKindAppl $ typeKind e1

5620N/A l2 = getKindAppl $ typeKind e2

5620N/A l3 = zipWith minVariance l1 l2

5620N/A l4 = foldr (\ v (((tl, vl), pl), fl) ->

5620N/A let c = length pl + 1

5620N/A a = simpleIdToId $ genNumVar "a" c

5620N/A ta = mkTypeArg a (- (length tl + 1))

5620N/A b = simpleIdToId $ genNumVar "b" c

5620N/A tb = mkTypeArg b (- (length tl + 2))

5620N/A x = stringToId $ 'x' : show c

5620N/A y = stringToId $ 'y' : show c

5620N/A tx = typeArgToType ta

5620N/A ty = typeArgToType tb

5620N/A vx = mkVarDecl x tx

5620N/A vy = mkVarDecl y ty

5620N/A in (case v of

5620N/A NonVar -> ((ta : tl, vx : vl), (tx, tx) : pl)

5620N/A _ -> (([ta, tb] ++ tl, [vx, vy] ++ vl), (tx, ty) : pl)

5620N/A , case v of

5620N/A CoVar -> mkSubtTerm tx ty vx vy : fl

5620N/A ContraVar -> mkSubtTerm ty tx vy vx : fl

5620N/A _ -> fl)) ((([], []), []), []) l3

5620N/A (args, fs) = l4

5620N/A (gens, acts) = args

5620N/A (act1, act2) = unzip acts

5620N/A (tyargs, vargs) = gens

5620N/A t1 = mkTypeAppl (toType i1) act1

5620N/A t2 = mkTypeAppl (toType i2) act2

5620N/A x1 = stringToId "x"

5620N/A x2 = stringToId "y"

5620N/A v1 = mkVarDecl x1 t1

5620N/A v2 = mkVarDecl x2 t2

5620N/A in makeNamed ("ga_subt_" ++ txt) $ Formula

5620N/A $ mkForall (map GenTypeVarDecl tyargs

5620N/A ++ map GenVarDecl (vargs ++ [v1, v2]))

5620N/A $ (if null fs then id else

5620N/A mkLogTerm implId nr (foldr1 (mkLogTerm andId nr) fs))

5620N/A $ mkSubtTerm t1 t2 v1 v2

5620N/A

5620N/AmkSubtTerm :: Type -> Type -> VarDecl -> VarDecl -> Term

5620N/AmkSubtTerm t1 t2 v1 v2 = mkTerm subtRelName subtRelType [t1, t2] nr

5620N/A $ TupleTerm [QualVar v1, QualVar v2] nr

5620N/A

5620N/AsubtReflex :: Named Sentence

5620N/AsubtReflex = let

5620N/A v1 = mkVarDecl (stringToId "x") aType

5620N/A v2 = mkVarDecl (stringToId "y") aType

5620N/A in makeNamed "ga_subt_reflexive" $ Formula

5620N/A $ mkForall (GenTypeVarDecl aTypeArg : map GenVarDecl [v1, v2])

5620N/A $ mkSubtTerm aType aType v1 v2

5620N/A

5620N/AsubtTrans :: Named Sentence

5620N/AsubtTrans = let

5620N/A v1 = mkVarDecl (stringToId "x") aType

5620N/A v2 = mkVarDecl (stringToId "y") bType

5620N/A v3 = mkVarDecl (stringToId "z") cType

5620N/A in makeNamed "ga_subt_transitive" $ Formula

5620N/A $ mkForall (map GenTypeVarDecl [aTypeArg, bTypeArg, cTypeArg]

5620N/A ++ map GenVarDecl [v1, v2, v3])

5620N/A $ mkLogTerm implId nr

5620N/A (mkLogTerm andId nr

5620N/A (mkSubtTerm aType bType v1 v2)

5620N/A $ mkSubtTerm bType cType v2 v3)

5620N/A $ mkSubtTerm aType cType v1 v3

5620N/A

5620N/AmkInjTerm :: Type -> Type -> Term -> Term

5620N/AmkInjTerm t1 t2 = mkTerm injName injType [t1, t2] nr

5620N/A

5620N/AmkInjEq :: Type -> Type -> VarDecl -> VarDecl -> Term

5620N/AmkInjEq t1 t2 v1 v2 =

5620N/A mkEqTerm eqId t2 nr (QualVar v2)

5620N/A $ mkInjTerm t1 t2 $ QualVar v1

5620N/A

5620N/AsubtInjProj :: Named Sentence

5620N/AsubtInjProj = let

5620N/A v1 = mkVarDecl (stringToId "x") aType

5620N/A v2 = mkVarDecl (stringToId "y") bType

5620N/A in makeNamed "ga_subt_inj_proj" $ Formula

5620N/A $ mkForall (map GenTypeVarDecl [aTypeArg, bTypeArg]

5620N/A ++ map GenVarDecl [v1, v2])

5620N/A $ mkLogTerm implId nr

5620N/A (mkSubtTerm aType bType v1 v2)

5620N/A $ mkLogTerm eqvId nr (mkInjEq aType bType v1 v2)

5620N/A $ mkEqTerm eqId aType nr (QualVar v1)

5620N/A $ mkTerm projName projType [bType, aType] nr

5620N/A $ QualVar v2

5620N/A

5620N/AinjTrans :: Named Sentence

5620N/AinjTrans = let

5620N/A v1 = mkVarDecl (stringToId "x") aType

5620N/A v2 = mkVarDecl (stringToId "y") bType

5620N/A v3 = mkVarDecl (stringToId "z") cType

5620N/A in makeNamed "ga_inj_transitive" $ Formula

5620N/A $ mkForall (map GenTypeVarDecl [aTypeArg, bTypeArg, cTypeArg]

5620N/A ++ map GenVarDecl [v1, v2, v3])

5620N/A $ mkLogTerm implId nr

5620N/A (mkLogTerm andId nr (mkSubtTerm aType bType v1 v2)

5620N/A $ mkLogTerm andId nr (mkSubtTerm bType cType v2 v3)

5620N/A $ mkInjEq aType bType v1 v2)

5620N/A $ mkLogTerm eqvId nr (mkInjEq aType cType v1 v3)

5620N/A $ mkInjEq bType cType v2 v3

5620N/A

5620N/Amonos :: Env -> [Named Sentence]

5620N/Amonos e = concatMap (makeMonos e) . Map.toList $ assumps e

5620N/A

5620N/AmakeMonos :: Env -> (Id, Set.Set OpInfo) -> [Named Sentence]

5620N/AmakeMonos e (i, s) = makeEquivMonos e i . map opType $ Set.toList s

5620N/A

5620N/AmakeEquivMonos :: Env -> Id -> [TypeScheme] -> [Named Sentence]

5620N/AmakeEquivMonos e i l = case l of

5620N/A [] -> []

5620N/A t : r -> mapMaybe (makeEquivMono e i t) r ++ makeEquivMonos e i r

5620N/A

5620N/AmakeEquivMono :: Env -> Id -> TypeScheme -> TypeScheme -> Maybe (Named Sentence)

5620N/AmakeEquivMono e i s1 s2 = case getCommonSupertype e s1 s2 of

5620N/A Just (ty1, l1, ty2, l2, args, nTy) ->

5620N/A Just $ makeNamed "ga_monotonicity"

5620N/A $ Formula $ mkForall (map GenTypeVarDecl args)

5620N/A $ mkEqTerm eqId nTy nr

5620N/A (mkInjTerm ty1 nTy

5620N/A $ QualOp Op (PolyId i [] nr) s1 l1 UserGiven nr)

5620N/A $ mkInjTerm ty2 nTy

5620N/A $ QualOp Op (PolyId i [] nr) s2 l2 UserGiven nr

5620N/A Nothing -> Nothing

5620N/A