TypeRel.hs revision b87efd3db0d2dc41615ea28669faf80fc1b48d56
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder{- |
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederModule : $Header$
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederDescription : compute subtype dependencies
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederLicense : GPLv2 or higher
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederMaintainer : Christian.Maeder@dfki.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : experimental
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedercompute subtype dependencies
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-}
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedermodule HasCASL.TypeRel where
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport HasCASL.As
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport HasCASL.AsUtils
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport HasCASL.ClassAna
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport HasCASL.Le
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport HasCASL.Builtin
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport HasCASL.DataAna
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport HasCASL.MinType
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Common.Id
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Common.AS_Annotation
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport qualified Common.Lib.Rel as Rel
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport qualified Data.Map as Map
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport qualified Data.Set as Set
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Data.Maybe
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedertypeRel :: TypeMap -> Rel.Rel Id
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedertypeRel = Rel.transReduce . Rel.irreflex . Rel.transClosure
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder . Map.foldWithKey ( \ i ti r ->
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Set.fold (Rel.insert i) r $ superTypes ti) Rel.empty
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedergetRawKind :: TypeMap -> Id -> RawKind
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedergetRawKind tm i = typeKind $
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Map.findWithDefault (error $ showId i " not found in type map") i tm
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | make a polymorphic function from a to b
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedermkInjOrProjType :: Arrow -> TypeScheme
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedermkInjOrProjType arr =
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder TypeScheme [aTypeArg, bTypeArg] (mkFunArrType aType arr bType) nullRange
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederinjType :: TypeScheme
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederinjType = mkInjOrProjType FunArr
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederprojType :: TypeScheme
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederprojType = mkInjOrProjType PFunArr
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedermkInjOrProj :: Arrow -> Set.Set OpInfo
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedermkInjOrProj arr = Set.singleton OpInfo
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder { opType = mkInjOrProjType arr
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , opAttrs = Set.empty
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , opDefn = NoOpDefn Fun }
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersubtRelName :: Id
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersubtRelName = mkId [genToken "subt"]
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersubtRelType :: TypeScheme
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersubtRelType = TypeScheme [aTypeArg, bTypeArg]
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (mkFunArrType (mkProductType [aType, bType]) PFunArr unitType) nullRange
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersubtRel :: Set.Set OpInfo
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersubtRel = Set.singleton OpInfo
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder { opType = subtRelType
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , opAttrs = Set.empty
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , opDefn = NoOpDefn Fun }
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersubtAxioms :: TypeMap -> [Named Sentence]
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersubtAxioms tm =
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder let tr = typeRel tm in
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder if Rel.null tr then [] else subtReflex : subtTrans : subtInjProj : injTrans
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder : map (subtAx tm) (Rel.toList tr)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedernr :: Range
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedernr = nullRange
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedergetKindAppl :: RawKind -> [Variance]
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedergetKindAppl rk = case rk of
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder ClassKind () -> []
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder FunKind v _ r _ -> v : getKindAppl r
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedermkTypeArg :: Id -> Int -> TypeArg
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedermkTypeArg i c = TypeArg i NonVar (VarKind universe) rStar c Other nr
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersubtAx :: TypeMap -> (Id, Id) -> Named Sentence
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersubtAx tm (i1, i2) = let
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder findType i = Map.findWithDefault
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (Map.findWithDefault (error "TypeRel.subtAx") i bTypes) i tm
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder e1 = findType i1
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder e2 = findType i2
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder txt = shows i1 "_<_" ++ show i2
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder l1 = getKindAppl $ typeKind e1
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder l2 = getKindAppl $ typeKind e2
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder l3 = zipWith minVariance l1 l2
l4 = foldr (\ v (((tl, vl), pl), fl) ->
let c = length pl + 1
a = simpleIdToId $ genNumVar "a" c
ta = mkTypeArg a (- (length tl + 1))
b = simpleIdToId $ genNumVar "b" c
tb = mkTypeArg b (- (length tl + 2))
x = stringToId $ 'x' : show c
y = stringToId $ 'y' : show c
tx = typeArgToType ta
ty = typeArgToType tb
vx = mkVarDecl x tx
vy = mkVarDecl y ty
in (case v of
NonVar -> ((ta : tl, vx : vl), (tx, tx) : pl)
_ -> (([ta, tb] ++ tl, [vx, vy] ++ vl), (tx, ty) : pl)
, case v of
CoVar -> mkSubtTerm tx ty vx vy : fl
ContraVar -> mkSubtTerm ty tx vy vx : fl
_ -> fl)) ((([], []), []), []) l3
(args, fs) = l4
(gens, acts) = args
(act1, act2) = unzip acts
(tyargs, vargs) = gens
t1 = mkTypeAppl (toType i1) act1
t2 = mkTypeAppl (toType i2) act2
x1 = stringToId "x"
x2 = stringToId "y"
v1 = mkVarDecl x1 t1
v2 = mkVarDecl x2 t2
in makeNamed ("ga_subt_" ++ txt) $ Formula
$ mkForall (map GenTypeVarDecl tyargs
++ map GenVarDecl (vargs ++ [v1, v2]))
$ (if null fs then id else
mkLogTerm implId nr (foldr1 (mkLogTerm andId nr) fs))
$ mkSubtTerm t1 t2 v1 v2
mkSubtTerm :: Type -> Type -> VarDecl -> VarDecl -> Term
mkSubtTerm t1 t2 v1 v2 = mkTerm subtRelName subtRelType [t1, t2] nr
$ TupleTerm [QualVar v1, QualVar v2] nr
subtReflex :: Named Sentence
subtReflex = let
v1 = mkVarDecl (stringToId "x") aType
v2 = mkVarDecl (stringToId "y") aType
in makeNamed "ga_subt_reflexive" $ Formula
$ mkForall (GenTypeVarDecl aTypeArg : map GenVarDecl [v1, v2])
$ mkSubtTerm aType aType v1 v2
subtTrans :: Named Sentence
subtTrans = let
v1 = mkVarDecl (stringToId "x") aType
v2 = mkVarDecl (stringToId "y") bType
v3 = mkVarDecl (stringToId "z") cType
in makeNamed "ga_subt_transitive" $ Formula
$ mkForall (map GenTypeVarDecl [aTypeArg, bTypeArg, cTypeArg]
++ map GenVarDecl [v1, v2, v3])
$ mkLogTerm implId nr
(mkLogTerm andId nr
(mkSubtTerm aType bType v1 v2)
$ mkSubtTerm bType cType v2 v3)
$ mkSubtTerm aType cType v1 v3
mkInjTerm :: Type -> Type -> Term -> Term
mkInjTerm t1 t2 = mkTerm injName injType [t1, t2] nr
mkInjEq :: Type -> Type -> VarDecl -> VarDecl -> Term
mkInjEq t1 t2 v1 v2 =
mkEqTerm eqId t2 nr (QualVar v2)
$ mkInjTerm t1 t2 $ QualVar v1
subtInjProj :: Named Sentence
subtInjProj = let
v1 = mkVarDecl (stringToId "x") aType
v2 = mkVarDecl (stringToId "y") bType
in makeNamed "ga_subt_inj_proj" $ Formula
$ mkForall (map GenTypeVarDecl [aTypeArg, bTypeArg]
++ map GenVarDecl [v1, v2])
$ mkLogTerm implId nr
(mkSubtTerm aType bType v1 v2)
$ mkLogTerm eqvId nr (mkInjEq aType bType v1 v2)
$ mkEqTerm eqId aType nr (QualVar v1)
$ mkTerm projName projType [bType, aType] nr
$ QualVar v2
injTrans :: Named Sentence
injTrans = let
v1 = mkVarDecl (stringToId "x") aType
v2 = mkVarDecl (stringToId "y") bType
v3 = mkVarDecl (stringToId "z") cType
in makeNamed "ga_inj_transitive" $ Formula
$ mkForall (map GenTypeVarDecl [aTypeArg, bTypeArg, cTypeArg]
++ map GenVarDecl [v1, v2, v3])
$ mkLogTerm implId nr
(mkLogTerm andId nr (mkSubtTerm aType bType v1 v2)
$ mkLogTerm andId nr (mkSubtTerm bType cType v2 v3)
$ mkInjEq aType bType v1 v2)
$ mkLogTerm eqvId nr (mkInjEq aType cType v1 v3)
$ mkInjEq bType cType v2 v3
monos :: Env -> [Named Sentence]
monos e = concatMap (makeMonos e) . Map.toList $ assumps e
makeMonos :: Env -> (Id, Set.Set OpInfo) -> [Named Sentence]
makeMonos e (i, s) = makeEquivMonos e i . map opType $ Set.toList s
makeEquivMonos :: Env -> Id -> [TypeScheme] -> [Named Sentence]
makeEquivMonos e i l = case l of
[] -> []
t : r -> mapMaybe (makeEquivMono e i t) r ++ makeEquivMonos e i r
makeEquivMono :: Env -> Id -> TypeScheme -> TypeScheme -> Maybe (Named Sentence)
makeEquivMono e i s1 s2 = case getCommonSupertype e s1 s2 of
Just (ty1, l1, ty2, l2, args, nTy) ->
Just $ makeNamed "ga_monotonicity"
$ Formula $ mkForall (map GenTypeVarDecl args)
$ mkEqTerm eqId nTy nr
(mkInjTerm ty1 nTy
$ QualOp Op (PolyId i [] nr) s1 l1 UserGiven nr)
$ mkInjTerm ty2 nTy
$ QualOp Op (PolyId i [] nr) s2 l2 UserGiven nr
Nothing -> Nothing