module HasCASL.FoldType where
import HasCASL.As
import Common.Id
import qualified Data.Set as Set
import Data.List as List
data FoldTypeRec a = FoldTypeRec
{ FoldTypeRec a -> Type -> Id -> RawKind -> Int -> a
foldTypeName :: Type -> Id -> RawKind -> Int -> a
, FoldTypeRec a -> Type -> a -> a -> a
foldTypeAppl :: Type -> a -> a -> a
, FoldTypeRec a -> Type -> a -> a -> a
foldExpandedType :: Type -> a -> a -> a
, FoldTypeRec a -> Type -> TypeArg -> a -> Range -> a
foldTypeAbs :: Type -> TypeArg -> a -> Range -> a
, FoldTypeRec a -> Type -> a -> Set Kind -> Range -> a
foldKindedType :: Type -> a -> Set.Set Kind -> Range -> a
, FoldTypeRec a -> Type -> Token -> a
foldTypeToken :: Type -> Token -> a
, FoldTypeRec a -> Type -> BracketKind -> [a] -> Range -> a
foldBracketType :: Type -> BracketKind -> [a] -> Range -> a
, FoldTypeRec a -> Type -> [a] -> a
foldMixfixType :: Type -> [a] -> a }
mapTypeRec :: FoldTypeRec Type
mapTypeRec :: FoldTypeRec Type
mapTypeRec = FoldTypeRec :: forall a.
(Type -> Id -> RawKind -> Int -> a)
-> (Type -> a -> a -> a)
-> (Type -> a -> a -> a)
-> (Type -> TypeArg -> a -> Range -> a)
-> (Type -> a -> Set Kind -> Range -> a)
-> (Type -> Token -> a)
-> (Type -> BracketKind -> [a] -> Range -> a)
-> (Type -> [a] -> a)
-> FoldTypeRec a
FoldTypeRec
{ foldTypeName :: Type -> Id -> RawKind -> Int -> Type
foldTypeName = (Id -> RawKind -> Int -> Type)
-> Type -> Id -> RawKind -> Int -> Type
forall a b. a -> b -> a
const Id -> RawKind -> Int -> Type
TypeName
, foldTypeAppl :: Type -> Type -> Type -> Type
foldTypeAppl = (Type -> Type -> Type) -> Type -> Type -> Type -> Type
forall a b. a -> b -> a
const Type -> Type -> Type
TypeAppl
, foldExpandedType :: Type -> Type -> Type -> Type
foldExpandedType = (Type -> Type -> Type) -> Type -> Type -> Type -> Type
forall a b. a -> b -> a
const Type -> Type -> Type
ExpandedType
, foldTypeAbs :: Type -> TypeArg -> Type -> Range -> Type
foldTypeAbs = (TypeArg -> Type -> Range -> Type)
-> Type -> TypeArg -> Type -> Range -> Type
forall a b. a -> b -> a
const TypeArg -> Type -> Range -> Type
TypeAbs
, foldKindedType :: Type -> Type -> Set Kind -> Range -> Type
foldKindedType = (Type -> Set Kind -> Range -> Type)
-> Type -> Type -> Set Kind -> Range -> Type
forall a b. a -> b -> a
const Type -> Set Kind -> Range -> Type
KindedType
, foldTypeToken :: Type -> Token -> Type
foldTypeToken = (Token -> Type) -> Type -> Token -> Type
forall a b. a -> b -> a
const Token -> Type
TypeToken
, foldBracketType :: Type -> BracketKind -> [Type] -> Range -> Type
foldBracketType = (BracketKind -> [Type] -> Range -> Type)
-> Type -> BracketKind -> [Type] -> Range -> Type
forall a b. a -> b -> a
const BracketKind -> [Type] -> Range -> Type
BracketType
, foldMixfixType :: Type -> [Type] -> Type
foldMixfixType = ([Type] -> Type) -> Type -> [Type] -> Type
forall a b. a -> b -> a
const [Type] -> Type
MixfixType }
foldType :: FoldTypeRec a -> Type -> a
foldType :: FoldTypeRec a -> Type -> a
foldType r :: FoldTypeRec a
r t :: Type
t = case Type
t of
TypeName i :: Id
i k :: RawKind
k c :: Int
c -> FoldTypeRec a -> Type -> Id -> RawKind -> Int -> a
forall a. FoldTypeRec a -> Type -> Id -> RawKind -> Int -> a
foldTypeName FoldTypeRec a
r Type
t Id
i RawKind
k Int
c
TypeAppl t1 :: Type
t1 t2 :: Type
t2 -> FoldTypeRec a -> Type -> a -> a -> a
forall a. FoldTypeRec a -> Type -> a -> a -> a
foldTypeAppl FoldTypeRec a
r Type
t (FoldTypeRec a -> Type -> a
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec a
r Type
t1) (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ FoldTypeRec a -> Type -> a
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec a
r Type
t2
ExpandedType t1 :: Type
t1 t2 :: Type
t2 -> FoldTypeRec a -> Type -> a -> a -> a
forall a. FoldTypeRec a -> Type -> a -> a -> a
foldExpandedType FoldTypeRec a
r Type
t (FoldTypeRec a -> Type -> a
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec a
r Type
t1) (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ FoldTypeRec a -> Type -> a
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec a
r Type
t2
TypeAbs a :: TypeArg
a ty :: Type
ty p :: Range
p -> FoldTypeRec a -> Type -> TypeArg -> a -> Range -> a
forall a. FoldTypeRec a -> Type -> TypeArg -> a -> Range -> a
foldTypeAbs FoldTypeRec a
r Type
t TypeArg
a (FoldTypeRec a -> Type -> a
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec a
r Type
ty) Range
p
KindedType ty :: Type
ty ks :: Set Kind
ks p :: Range
p -> FoldTypeRec a -> Type -> a -> Set Kind -> Range -> a
forall a. FoldTypeRec a -> Type -> a -> Set Kind -> Range -> a
foldKindedType FoldTypeRec a
r Type
t (FoldTypeRec a -> Type -> a
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec a
r Type
ty) Set Kind
ks Range
p
TypeToken tok :: Token
tok -> FoldTypeRec a -> Type -> Token -> a
forall a. FoldTypeRec a -> Type -> Token -> a
foldTypeToken FoldTypeRec a
r Type
t Token
tok
BracketType k :: BracketKind
k ts :: [Type]
ts p :: Range
p -> FoldTypeRec a -> Type -> BracketKind -> [a] -> Range -> a
forall a. FoldTypeRec a -> Type -> BracketKind -> [a] -> Range -> a
foldBracketType FoldTypeRec a
r Type
t BracketKind
k ((Type -> a) -> [Type] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (FoldTypeRec a -> Type -> a
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec a
r) [Type]
ts) Range
p
MixfixType ts :: [Type]
ts -> FoldTypeRec a -> Type -> [a] -> a
forall a. FoldTypeRec a -> Type -> [a] -> a
foldMixfixType FoldTypeRec a
r Type
t ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ (Type -> a) -> [Type] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (FoldTypeRec a -> Type -> a
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec a
r) [Type]
ts
replAlias :: (Id -> RawKind -> Int -> Type) -> Type -> Type
replAlias :: (Id -> RawKind -> Int -> Type) -> Type -> Type
replAlias m :: Id -> RawKind -> Int -> Type
m = FoldTypeRec Type -> Type -> Type
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec Type
mapTypeRec
{ foldTypeName :: Type -> Id -> RawKind -> Int -> Type
foldTypeName = (Id -> RawKind -> Int -> Type)
-> Type -> Id -> RawKind -> Int -> Type
forall a b. a -> b -> a
const Id -> RawKind -> Int -> Type
m
, foldExpandedType :: Type -> Type -> Type -> Type
foldExpandedType = \ et :: Type
et r1 :: Type
r1 r2 :: Type
r2 -> case (Type
et, Type
r1) of
(ExpandedType t1 :: Type
t1@(TypeName {}) _, ExpandedType t3 :: Type
t3 _) | Type
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t3 ->
Type -> Type -> Type
ExpandedType Type
t1 Type
r2
_ -> Type -> Type -> Type
ExpandedType Type
r1 Type
r2 }
leaves :: (Int -> Bool) -> Type -> [(Int, (Id, RawKind))]
leaves :: (Int -> Bool) -> Type -> [(Int, (Id, RawKind))]
leaves b :: Int -> Bool
b = FoldTypeRec [(Int, (Id, RawKind))]
-> Type -> [(Int, (Id, RawKind))]
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec :: forall a.
(Type -> Id -> RawKind -> Int -> a)
-> (Type -> a -> a -> a)
-> (Type -> a -> a -> a)
-> (Type -> TypeArg -> a -> Range -> a)
-> (Type -> a -> Set Kind -> Range -> a)
-> (Type -> Token -> a)
-> (Type -> BracketKind -> [a] -> Range -> a)
-> (Type -> [a] -> a)
-> FoldTypeRec a
FoldTypeRec
{ foldTypeName :: Type -> Id -> RawKind -> Int -> [(Int, (Id, RawKind))]
foldTypeName = \ _ i :: Id
i k :: RawKind
k c :: Int
c -> [(Int
c, (Id
i, RawKind
k)) | Int -> Bool
b Int
c]
, foldTypeAppl :: Type
-> [(Int, (Id, RawKind))]
-> [(Int, (Id, RawKind))]
-> [(Int, (Id, RawKind))]
foldTypeAppl = ([(Int, (Id, RawKind))]
-> [(Int, (Id, RawKind))] -> [(Int, (Id, RawKind))])
-> Type
-> [(Int, (Id, RawKind))]
-> [(Int, (Id, RawKind))]
-> [(Int, (Id, RawKind))]
forall a b. a -> b -> a
const [(Int, (Id, RawKind))]
-> [(Int, (Id, RawKind))] -> [(Int, (Id, RawKind))]
forall a. Eq a => [a] -> [a] -> [a]
List.union
, foldExpandedType :: Type
-> [(Int, (Id, RawKind))]
-> [(Int, (Id, RawKind))]
-> [(Int, (Id, RawKind))]
foldExpandedType = \ _ _ t2 :: [(Int, (Id, RawKind))]
t2 -> [(Int, (Id, RawKind))]
t2
, foldTypeAbs :: Type
-> TypeArg
-> [(Int, (Id, RawKind))]
-> Range
-> [(Int, (Id, RawKind))]
foldTypeAbs = \ _ (TypeArg i :: Id
i _ _ r :: RawKind
r c :: Int
c _ _) ty :: [(Int, (Id, RawKind))]
ty _ ->
(Int, (Id, RawKind))
-> [(Int, (Id, RawKind))] -> [(Int, (Id, RawKind))]
forall a. Eq a => a -> [a] -> [a]
List.delete (Int
c, (Id
i, RawKind
r)) [(Int, (Id, RawKind))]
ty
, foldKindedType :: Type
-> [(Int, (Id, RawKind))]
-> Set Kind
-> Range
-> [(Int, (Id, RawKind))]
foldKindedType = \ _ ty :: [(Int, (Id, RawKind))]
ty _ _ -> [(Int, (Id, RawKind))]
ty
, foldTypeToken :: Type -> Token -> [(Int, (Id, RawKind))]
foldTypeToken = \ _ _ -> []
, foldBracketType :: Type
-> BracketKind
-> [[(Int, (Id, RawKind))]]
-> Range
-> [(Int, (Id, RawKind))]
foldBracketType = \ _ _ _ _ -> []
, foldMixfixType :: Type -> [[(Int, (Id, RawKind))]] -> [(Int, (Id, RawKind))]
foldMixfixType = \ _ _ -> [] }
freeTVars :: Type -> [(Int, (Id, RawKind))]
freeTVars :: Type -> [(Int, (Id, RawKind))]
freeTVars = (Int -> Bool) -> Type -> [(Int, (Id, RawKind))]
leaves (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0)
freeTVarIds :: Type -> [Id]
freeTVarIds :: Type -> [Id]
freeTVarIds = ((Int, (Id, RawKind)) -> Id) -> [(Int, (Id, RawKind))] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map ((Id, RawKind) -> Id
forall a b. (a, b) -> a
fst ((Id, RawKind) -> Id)
-> ((Int, (Id, RawKind)) -> (Id, RawKind))
-> (Int, (Id, RawKind))
-> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (Id, RawKind)) -> (Id, RawKind)
forall a b. (a, b) -> b
snd) ([(Int, (Id, RawKind))] -> [Id])
-> (Type -> [(Int, (Id, RawKind))]) -> Type -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [(Int, (Id, RawKind))]
freeTVars