{- |
Module      :  ./HasCASL/TypeRel.hs
Description :  compute subtype dependencies
Copyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

compute subtype dependencies
-}

module HasCASL.TypeRel where

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.ClassAna
import HasCASL.Le
import HasCASL.Builtin
import HasCASL.DataAna
import HasCASL.MinType
import HasCASL.Merge

import Common.Id
import Common.AS_Annotation
import qualified Common.Lib.Rel as Rel

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe

typeRel :: TypeMap -> Rel.Rel Id
typeRel :: TypeMap -> Rel Id
typeRel = Rel Id -> Rel Id
forall a. Ord a => Rel a -> Rel a
Rel.transReduce (Rel Id -> Rel Id) -> (TypeMap -> Rel Id) -> TypeMap -> Rel Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel Id -> Rel Id
forall a. Ord a => Rel a -> Rel a
Rel.irreflex (Rel Id -> Rel Id) -> (TypeMap -> Rel Id) -> TypeMap -> Rel Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel Id -> Rel Id
forall a. Ord a => Rel a -> Rel a
Rel.transClosure
  (Rel Id -> Rel Id) -> (TypeMap -> Rel Id) -> TypeMap -> Rel Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id -> TypeInfo -> Rel Id -> Rel Id) -> Rel Id -> TypeMap -> Rel Id
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey ( \ i :: Id
i ti :: TypeInfo
ti r :: Rel Id
r ->
    (Id -> Rel Id -> Rel Id) -> Rel Id -> Set Id -> Rel Id
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Id -> Id -> Rel Id -> Rel Id
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertPair Id
i) Rel Id
r (Set Id -> Rel Id) -> Set Id -> Rel Id
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Set Id
superTypes TypeInfo
ti) Rel Id
forall a. Rel a
Rel.empty

getRawKind :: TypeMap -> Id -> RawKind
getRawKind :: TypeMap -> Id -> RawKind
getRawKind tm :: TypeMap
tm i :: Id
i = TypeInfo -> RawKind
typeKind (TypeInfo -> RawKind) -> TypeInfo -> RawKind
forall a b. (a -> b) -> a -> b
$
    TypeInfo -> Id -> TypeMap -> TypeInfo
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> TypeInfo
forall a. HasCallStack => [Char] -> a
error ([Char] -> TypeInfo) -> [Char] -> TypeInfo
forall a b. (a -> b) -> a -> b
$ Id -> ShowS
showId Id
i " not found in type map") Id
i TypeMap
tm

-- | make a polymorphic function from a to b
mkInjOrProjType :: Arrow -> TypeScheme
mkInjOrProjType :: Arrow -> TypeScheme
mkInjOrProjType arr :: Arrow
arr =
    [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg
aTypeArg, TypeArg
bTypeArg] (Type -> Arrow -> Type -> Type
mkFunArrType Type
aType Arrow
arr Type
bType) Range
nullRange

injType :: TypeScheme
injType :: TypeScheme
injType = Arrow -> TypeScheme
mkInjOrProjType Arrow
FunArr

projType :: TypeScheme
projType :: TypeScheme
projType = Arrow -> TypeScheme
mkInjOrProjType Arrow
PFunArr

mkInjOrProj :: Arrow -> Set.Set OpInfo
mkInjOrProj :: Arrow -> Set OpInfo
mkInjOrProj arr :: Arrow
arr = OpInfo -> Set OpInfo
forall a. a -> Set a
Set.singleton OpInfo :: TypeScheme -> Set OpAttr -> OpDefn -> OpInfo
OpInfo
    { opType :: TypeScheme
opType = Arrow -> TypeScheme
mkInjOrProjType Arrow
arr
    , opAttrs :: Set OpAttr
opAttrs = Set OpAttr
forall a. Set a
Set.empty
    , opDefn :: OpDefn
opDefn = OpBrand -> OpDefn
NoOpDefn OpBrand
Fun }

subtRelName :: Id
subtRelName :: Id
subtRelName = [Token] -> Id
mkId [[Char] -> Token
genToken "subt"]

subtRelType :: TypeScheme
subtRelType :: TypeScheme
subtRelType = [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg
aTypeArg, TypeArg
bTypeArg]
  (Type -> Arrow -> Type -> Type
mkFunArrType ([Type] -> Type
mkProductType [Type
aType, Type
bType]) Arrow
PFunArr Type
unitType) Range
nullRange

subtRel :: Set.Set OpInfo
subtRel :: Set OpInfo
subtRel = OpInfo -> Set OpInfo
forall a. a -> Set a
Set.singleton OpInfo :: TypeScheme -> Set OpAttr -> OpDefn -> OpInfo
OpInfo
    { opType :: TypeScheme
opType = TypeScheme
subtRelType
    , opAttrs :: Set OpAttr
opAttrs = Set OpAttr
forall a. Set a
Set.empty
    , opDefn :: OpDefn
opDefn = OpBrand -> OpDefn
NoOpDefn OpBrand
Fun }

varRel :: Rel.Rel Id -> TypeMap -> Rel.Rel Id
varRel :: Rel Id -> TypeMap -> Rel Id
varRel r :: Rel Id
r =
  (Id -> Rel Id -> Rel Id) -> Rel Id -> [Id] -> Rel Id
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ i :: Id
i -> Id -> Id -> Rel Id -> Rel Id
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertPair Id
i Id
i) Rel Id
r ([Id] -> Rel Id) -> (TypeMap -> [Id]) -> TypeMap -> Rel Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeMap -> [Id]
forall k a. Map k a -> [k]
Map.keys
  (TypeMap -> [Id]) -> (TypeMap -> TypeMap) -> TypeMap -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeInfo -> Bool) -> TypeMap -> TypeMap
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter ((Variance -> Bool) -> [Variance] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Variance -> [Variance] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Variance
CoVar, Variance
ContraVar]) ([Variance] -> Bool)
-> (TypeInfo -> [Variance]) -> TypeInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawKind -> [Variance]
getKindAppl (RawKind -> [Variance])
-> (TypeInfo -> RawKind) -> TypeInfo -> [Variance]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeInfo -> RawKind
typeKind)

subtAxioms :: TypeMap -> [Named Sentence]
subtAxioms :: TypeMap -> [Named Sentence]
subtAxioms tm0 :: TypeMap
tm0 =
  let tm :: TypeMap
tm = ClassMap -> TypeMap -> TypeMap
addUnit ClassMap
cpoMap TypeMap
tm0
      tr :: Rel Id
tr = Rel Id -> TypeMap -> Rel Id
varRel (TypeMap -> Rel Id
typeRel TypeMap
tm) TypeMap
tm in
  if Rel Id -> Bool
forall a. Rel a -> Bool
Rel.nullKeys (Rel Id -> Bool) -> Rel Id -> Bool
forall a b. (a -> b) -> a -> b
$ TypeMap -> Rel Id
typeRel TypeMap
tm0 then [] else
  Named Sentence
subtReflex Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: Named Sentence
subtTrans Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: Named Sentence
subtInjProj Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: Named Sentence
injTrans Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: Named Sentence
idInj
  Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: ((Id, Id) -> Named Sentence) -> [(Id, Id)] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map (TypeMap -> (Id, Id) -> Named Sentence
subtAx TypeMap
tm) (Rel Id -> [(Id, Id)]
forall a. Rel a -> [(a, a)]
Rel.toList Rel Id
tr)

nr :: Range
nr :: Range
nr = Range
nullRange

getKindAppl :: RawKind -> [Variance]
getKindAppl :: RawKind -> [Variance]
getKindAppl rk :: RawKind
rk = case RawKind
rk of
  ClassKind () -> []
  FunKind v :: Variance
v _ r :: RawKind
r _ -> Variance
v Variance -> [Variance] -> [Variance]
forall a. a -> [a] -> [a]
: RawKind -> [Variance]
getKindAppl RawKind
r

mkTypeArg :: Id -> Int -> TypeArg
mkTypeArg :: Id -> Int -> TypeArg
mkTypeArg i :: Id
i c :: Int
c = Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
i Variance
NonVar (Kind -> VarKind
VarKind Kind
universe) RawKind
rStar Int
c SeparatorKind
Other Range
nr

subtAx :: TypeMap -> (Id, Id) -> Named Sentence
subtAx :: TypeMap -> (Id, Id) -> Named Sentence
subtAx tm :: TypeMap
tm (i1 :: Id
i1, i2 :: Id
i2) = let
    findType :: Id -> TypeInfo
findType i :: Id
i = TypeInfo -> Id -> TypeMap -> TypeInfo
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
      (TypeInfo -> Id -> TypeMap -> TypeInfo
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> TypeInfo
forall a. HasCallStack => [Char] -> a
error "TypeRel.subtAx") Id
i TypeMap
bTypes) Id
i TypeMap
tm
    e1 :: TypeInfo
e1 = Id -> TypeInfo
findType Id
i1
    e2 :: TypeInfo
e2 = Id -> TypeInfo
findType Id
i2
    txt :: [Char]
txt = Id -> ShowS
forall a. Show a => a -> ShowS
shows Id
i1 "_<_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> [Char]
forall a. Show a => a -> [Char]
show Id
i2
    l1 :: [Variance]
l1 = RawKind -> [Variance]
getKindAppl (RawKind -> [Variance]) -> RawKind -> [Variance]
forall a b. (a -> b) -> a -> b
$ TypeInfo -> RawKind
typeKind TypeInfo
e1
    l2 :: [Variance]
l2 = RawKind -> [Variance]
getKindAppl (RawKind -> [Variance]) -> RawKind -> [Variance]
forall a b. (a -> b) -> a -> b
$ TypeInfo -> RawKind
typeKind TypeInfo
e2
    l3 :: [Variance]
l3 = (Variance -> Variance -> Variance)
-> [Variance] -> [Variance] -> [Variance]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Variance -> Variance -> Variance
minVariance [Variance]
l1 [Variance]
l2
    l4 :: ((([TypeArg], [VarDecl]), [(Type, Type)]), [Term])
l4 = (Variance
 -> ((([TypeArg], [VarDecl]), [(Type, Type)]), [Term])
 -> ((([TypeArg], [VarDecl]), [(Type, Type)]), [Term]))
-> ((([TypeArg], [VarDecl]), [(Type, Type)]), [Term])
-> [Variance]
-> ((([TypeArg], [VarDecl]), [(Type, Type)]), [Term])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ v :: Variance
v (((tl :: [TypeArg]
tl, vl :: [VarDecl]
vl), pl :: [(Type, Type)]
pl), fl :: [Term]
fl) ->
            let c :: Int
c = [(Type, Type)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Type, Type)]
pl Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
                a :: Id
a = Token -> Id
simpleIdToId (Token -> Id) -> Token -> Id
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> Token
genNumVar "a" Int
c
                ta :: TypeArg
ta = Id -> Int -> TypeArg
mkTypeArg Id
a (- ([TypeArg] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg]
tl Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1))
                b :: Id
b = Token -> Id
simpleIdToId (Token -> Id) -> Token -> Id
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> Token
genNumVar "b" Int
c
                tb :: TypeArg
tb = Id -> Int -> TypeArg
mkTypeArg Id
b (- ([TypeArg] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg]
tl Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 2))
                x :: Id
x = [Char] -> Id
stringToId ([Char] -> Id) -> [Char] -> Id
forall a b. (a -> b) -> a -> b
$ 'x' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> [Char]
forall a. Show a => a -> [Char]
show Int
c
                y :: Id
y = [Char] -> Id
stringToId ([Char] -> Id) -> [Char] -> Id
forall a b. (a -> b) -> a -> b
$ 'y' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> [Char]
forall a. Show a => a -> [Char]
show Int
c
                tx :: Type
tx = TypeArg -> Type
typeArgToType TypeArg
ta
                ty :: Type
ty = TypeArg -> Type
typeArgToType TypeArg
tb
                vx :: VarDecl
vx = Id -> Type -> VarDecl
mkVarDecl Id
x Type
tx
                vy :: VarDecl
vy = Id -> Type -> VarDecl
mkVarDecl Id
y Type
ty
            in (case Variance
v of
                  NonVar -> ((TypeArg
ta TypeArg -> [TypeArg] -> [TypeArg]
forall a. a -> [a] -> [a]
: [TypeArg]
tl, VarDecl
vx VarDecl -> [VarDecl] -> [VarDecl]
forall a. a -> [a] -> [a]
: [VarDecl]
vl), (Type
tx, Type
tx) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
pl)
                  _ -> (([TypeArg
ta, TypeArg
tb] [TypeArg] -> [TypeArg] -> [TypeArg]
forall a. [a] -> [a] -> [a]
++ [TypeArg]
tl, [VarDecl
vx, VarDecl
vy] [VarDecl] -> [VarDecl] -> [VarDecl]
forall a. [a] -> [a] -> [a]
++ [VarDecl]
vl), (Type
tx, Type
ty) (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
forall a. a -> [a] -> [a]
: [(Type, Type)]
pl)
               , case Variance
v of
                   CoVar -> Type -> Type -> VarDecl -> VarDecl -> Term
mkSubtTerm Type
tx Type
ty VarDecl
vx VarDecl
vy Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
fl
                   ContraVar -> Type -> Type -> VarDecl -> VarDecl -> Term
mkSubtTerm Type
ty Type
tx VarDecl
vy VarDecl
vx Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
fl
                   _ -> [Term]
fl)) ((([], []), []), []) [Variance]
l3
    (args :: (([TypeArg], [VarDecl]), [(Type, Type)])
args, fs :: [Term]
fs) = ((([TypeArg], [VarDecl]), [(Type, Type)]), [Term])
l4
    (gens :: ([TypeArg], [VarDecl])
gens, acts :: [(Type, Type)]
acts) = (([TypeArg], [VarDecl]), [(Type, Type)])
args
    (act1 :: [Type]
act1, act2 :: [Type]
act2) = [(Type, Type)] -> ([Type], [Type])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Type, Type)]
acts
    (tyargs :: [TypeArg]
tyargs, vargs :: [VarDecl]
vargs) = ([TypeArg], [VarDecl])
gens
    t1 :: Type
t1 = Type -> [Type] -> Type
mkTypeAppl (Id -> Type
toType Id
i1) [Type]
act1
    t2 :: Type
t2 = Type -> [Type] -> Type
mkTypeAppl (Id -> Type
toType Id
i2) [Type]
act2
    x1 :: Id
x1 = [Char] -> Id
stringToId "x"
    x2 :: Id
x2 = [Char] -> Id
stringToId "y"
    v1 :: VarDecl
v1 = Id -> Type -> VarDecl
mkVarDecl Id
x1 Type
t1
    v2 :: VarDecl
v2 = Id -> Type -> VarDecl
mkVarDecl Id
x2 Type
t2
    in [Char] -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_subt_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
txt) (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
Formula
         (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> Term -> Term
mkForall ((TypeArg -> GenVarDecl) -> [TypeArg] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> GenVarDecl
GenTypeVarDecl [TypeArg]
tyargs
                     [GenVarDecl] -> [GenVarDecl] -> [GenVarDecl]
forall a. [a] -> [a] -> [a]
++ (VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl ([VarDecl]
vargs [VarDecl] -> [VarDecl] -> [VarDecl]
forall a. [a] -> [a] -> [a]
++ [VarDecl
v1, VarDecl
v2]))
           (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ (if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
fs then Term -> Term
forall a. a -> a
id else
             Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nr ((Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
nr) [Term]
fs))
               (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type -> VarDecl -> VarDecl -> Term
mkSubtTerm Type
t1 Type
t2 VarDecl
v1 VarDecl
v2

mkSubtTerm :: Type -> Type -> VarDecl -> VarDecl -> Term
mkSubtTerm :: Type -> Type -> VarDecl -> VarDecl -> Term
mkSubtTerm t1 :: Type
t1 t2 :: Type
t2 v1 :: VarDecl
v1 v2 :: VarDecl
v2 = Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm Id
subtRelName TypeScheme
subtRelType [Type
t1, Type
t2] Range
nr
  (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Range -> Term
TupleTerm [VarDecl -> Term
QualVar VarDecl
v1, VarDecl -> Term
QualVar VarDecl
v2] Range
nr

subtReflex :: Named Sentence
subtReflex :: Named Sentence
subtReflex = let
  v1 :: VarDecl
v1 = Id -> Type -> VarDecl
mkVarDecl ([Char] -> Id
stringToId "x") Type
aType
  v2 :: VarDecl
v2 = Id -> Type -> VarDecl
mkVarDecl ([Char] -> Id
stringToId "y") Type
aType
  in [Char] -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "ga_subt_reflexive" (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
Formula
       (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> Term -> Term
mkForall (TypeArg -> GenVarDecl
GenTypeVarDecl TypeArg
aTypeArg GenVarDecl -> [GenVarDecl] -> [GenVarDecl]
forall a. a -> [a] -> [a]
: (VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl
v1, VarDecl
v2])
         (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type -> VarDecl -> VarDecl -> Term
mkSubtTerm Type
aType Type
aType VarDecl
v1 VarDecl
v2

xa :: VarDecl
xa :: VarDecl
xa = Id -> Type -> VarDecl
mkVarDecl ([Char] -> Id
stringToId "x") Type
aType

yb :: VarDecl
yb :: VarDecl
yb = Id -> Type -> VarDecl
mkVarDecl ([Char] -> Id
stringToId "y") Type
bType

zc :: VarDecl
zc :: VarDecl
zc = Id -> Type -> VarDecl
mkVarDecl ([Char] -> Id
stringToId "z") Type
cType

xaToZc :: [GenVarDecl]
xaToZc :: [GenVarDecl]
xaToZc = (TypeArg -> GenVarDecl) -> [TypeArg] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> GenVarDecl
GenTypeVarDecl [TypeArg
aTypeArg, TypeArg
bTypeArg, TypeArg
cTypeArg]
  [GenVarDecl] -> [GenVarDecl] -> [GenVarDecl]
forall a. [a] -> [a] -> [a]
++ (VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl
xa, VarDecl
yb, VarDecl
zc]

subtTrans :: Named Sentence
subtTrans :: Named Sentence
subtTrans = [Char] -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "ga_subt_transitive" (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
Formula
     (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> Term -> Term
mkForall [GenVarDecl]
xaToZc
     (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nr
        (Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
nr
         (Type -> Type -> VarDecl -> VarDecl -> Term
mkSubtTerm Type
aType Type
bType VarDecl
xa VarDecl
yb)
         (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type -> VarDecl -> VarDecl -> Term
mkSubtTerm Type
bType Type
cType VarDecl
yb VarDecl
zc)
        (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type -> VarDecl -> VarDecl -> Term
mkSubtTerm Type
aType Type
cType VarDecl
xa VarDecl
zc

mkInjTerm :: Type -> Type -> Term -> Term
mkInjTerm :: Type -> Type -> Term -> Term
mkInjTerm t1 :: Type
t1 t2 :: Type
t2 = Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm Id
injName TypeScheme
injType [Type
t1, Type
t2] Range
nr

mkInjEq :: Type -> Type -> VarDecl -> VarDecl -> Term
mkInjEq :: Type -> Type -> VarDecl -> VarDecl -> Term
mkInjEq t1 :: Type
t1 t2 :: Type
t2 v1 :: VarDecl
v1 v2 :: VarDecl
v2 =
   Id -> Type -> Range -> Term -> Term -> Term
mkEqTerm Id
eqId Type
t2 Range
nr (VarDecl -> Term
QualVar VarDecl
v2)
          (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Term -> Term
mkInjTerm Type
t1 Type
t2 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ VarDecl -> Term
QualVar VarDecl
v1

subtInjProj :: Named Sentence
subtInjProj :: Named Sentence
subtInjProj = [Char] -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "ga_subt_inj_proj" (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
Formula
     (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> Term -> Term
mkForall ((TypeArg -> GenVarDecl) -> [TypeArg] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> GenVarDecl
GenTypeVarDecl [TypeArg
aTypeArg, TypeArg
bTypeArg]
                 [GenVarDecl] -> [GenVarDecl] -> [GenVarDecl]
forall a. [a] -> [a] -> [a]
++ (VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl
xa, VarDecl
yb])
     (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nr
        (Type -> Type -> VarDecl -> VarDecl -> Term
mkSubtTerm Type
aType Type
bType VarDecl
xa VarDecl
yb)
       (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
nr (Type -> Type -> VarDecl -> VarDecl -> Term
mkInjEq Type
aType Type
bType VarDecl
xa VarDecl
yb)
        (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Type -> Range -> Term -> Term -> Term
mkEqTerm Id
eqId Type
aType Range
nr (VarDecl -> Term
QualVar VarDecl
xa)
          (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm Id
projName TypeScheme
projType [Type
bType, Type
aType] Range
nr
            (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ VarDecl -> Term
QualVar VarDecl
yb

injTrans :: Named Sentence
injTrans :: Named Sentence
injTrans = [Char] -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "ga_inj_transitive" (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
Formula
     (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> Term -> Term
mkForall [GenVarDecl]
xaToZc
     (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nr
        (Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
nr (Type -> Type -> VarDecl -> VarDecl -> Term
mkSubtTerm Type
aType Type
bType VarDecl
xa VarDecl
yb)
          (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
nr (Type -> Type -> VarDecl -> VarDecl -> Term
mkSubtTerm Type
bType Type
cType VarDecl
yb VarDecl
zc)
            (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type -> VarDecl -> VarDecl -> Term
mkInjEq Type
aType Type
bType VarDecl
xa VarDecl
yb)
       (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
nr (Type -> Type -> VarDecl -> VarDecl -> Term
mkInjEq Type
aType Type
cType VarDecl
xa VarDecl
zc)
           (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type -> VarDecl -> VarDecl -> Term
mkInjEq Type
bType Type
cType VarDecl
yb VarDecl
zc

idInj :: Named Sentence
idInj :: Named Sentence
idInj = [Char] -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "ga_inj_identity"
  (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
Formula (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> Term -> Term
mkForall [TypeArg -> GenVarDecl
GenTypeVarDecl TypeArg
aTypeArg, VarDecl -> GenVarDecl
GenVarDecl VarDecl
xa]
  (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type -> VarDecl -> VarDecl -> Term
mkInjEq Type
aType Type
aType VarDecl
xa VarDecl
xa

monos :: Env -> [Named Sentence]
monos :: Env -> [Named Sentence]
monos e :: Env
e = ((Id, Set OpInfo) -> [Named Sentence])
-> [(Id, Set OpInfo)] -> [Named Sentence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env -> (Id, Set OpInfo) -> [Named Sentence]
makeMonos Env
e) ([(Id, Set OpInfo)] -> [Named Sentence])
-> (Map Id (Set OpInfo) -> [(Id, Set OpInfo)])
-> Map Id (Set OpInfo)
-> [Named Sentence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Id (Set OpInfo) -> [(Id, Set OpInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Id (Set OpInfo) -> [Named Sentence])
-> Map Id (Set OpInfo) -> [Named Sentence]
forall a b. (a -> b) -> a -> b
$ Env -> Map Id (Set OpInfo)
assumps Env
e

makeMonos :: Env -> (Id, Set.Set OpInfo) -> [Named Sentence]
makeMonos :: Env -> (Id, Set OpInfo) -> [Named Sentence]
makeMonos e :: Env
e (i :: Id
i, s :: Set OpInfo
s) = Env -> Id -> [TypeScheme] -> [Named Sentence]
makeEquivMonos Env
e Id
i ([TypeScheme] -> [Named Sentence])
-> ([OpInfo] -> [TypeScheme]) -> [OpInfo] -> [Named Sentence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OpInfo -> TypeScheme) -> [OpInfo] -> [TypeScheme]
forall a b. (a -> b) -> [a] -> [b]
map OpInfo -> TypeScheme
opType ([OpInfo] -> [Named Sentence]) -> [OpInfo] -> [Named Sentence]
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
s

makeEquivMonos :: Env -> Id -> [TypeScheme] -> [Named Sentence]
makeEquivMonos :: Env -> Id -> [TypeScheme] -> [Named Sentence]
makeEquivMonos e :: Env
e i :: Id
i l :: [TypeScheme]
l = case [TypeScheme]
l of
  [] -> []
  t :: TypeScheme
t : r :: [TypeScheme]
r -> (TypeScheme -> Maybe (Named Sentence))
-> [TypeScheme] -> [Named Sentence]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Env -> Id -> TypeScheme -> TypeScheme -> Maybe (Named Sentence)
makeEquivMono Env
e Id
i TypeScheme
t) [TypeScheme]
r [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ Env -> Id -> [TypeScheme] -> [Named Sentence]
makeEquivMonos Env
e Id
i [TypeScheme]
r

mkTypedTerm :: Term -> Type -> Range -> Term
mkTypedTerm :: Term -> Type -> Range -> Term
mkTypedTerm t :: Term
t = Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
t TypeQual
OfType

mkTypedEqTerm :: Id -> Type -> Range -> Term -> Term -> Term
mkTypedEqTerm :: Id -> Type -> Range -> Term -> Term -> Term
mkTypedEqTerm i :: Id
i s :: Type
s r :: Range
r t1 :: Term
t1 t2 :: Term
t2 =
  Id -> Type -> Range -> Term -> Term -> Term
mkEqTerm Id
i Type
s Range
r (Term -> Type -> Range -> Term
mkTypedTerm Term
t1 Type
s Range
r) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Type -> Range -> Term
mkTypedTerm Term
t2 Type
s Range
r

makeEquivMono :: Env -> Id -> TypeScheme -> TypeScheme -> Maybe (Named Sentence)
makeEquivMono :: Env -> Id -> TypeScheme -> TypeScheme -> Maybe (Named Sentence)
makeEquivMono e :: Env
e i :: Id
i s1 :: TypeScheme
s1 s2 :: TypeScheme
s2 = case Env -> TypeScheme -> TypeScheme -> Maybe TypeTriple
getCommonSupertype Env
e TypeScheme
s1 TypeScheme
s2 of
  Just (ty1 :: Type
ty1, l1 :: [Type]
l1, ty2 :: Type
ty2, l2 :: [Type]
l2, args :: [TypeArg]
args, nTy :: Type
nTy) ->
    Named Sentence -> Maybe (Named Sentence)
forall a. a -> Maybe a
Just (Named Sentence -> Maybe (Named Sentence))
-> Named Sentence -> Maybe (Named Sentence)
forall a b. (a -> b) -> a -> b
$ [Char] -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "ga_monotonicity"
         (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
Formula (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> Term -> Term
mkForall ((TypeArg -> GenVarDecl) -> [TypeArg] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> GenVarDecl
GenTypeVarDecl [TypeArg]
args)
           (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Type -> Range -> Term -> Term -> Term
mkTypedEqTerm Id
eqId Type
nTy Range
nr
           (Type -> Type -> Term -> Term
mkInjTerm Type
ty1 Type
nTy
             (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
Op (Id -> [TypeArg] -> Range -> PolyId
PolyId Id
i [] Range
nr) TypeScheme
s1 [Type]
l1 InstKind
UserGiven Range
nr)
           (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Term -> Term
mkInjTerm Type
ty2 Type
nTy
             (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
Op (Id -> [TypeArg] -> Range -> PolyId
PolyId Id
i [] Range
nr) TypeScheme
s2 [Type]
l2 InstKind
UserGiven Range
nr
  Nothing -> Maybe (Named Sentence)
forall a. Maybe a
Nothing