{- |
Module      :  ./HasCASL/FoldType.hs
Description :  fold functions for types
Copyright   :  (c) Christian Maeder and Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

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

folding types
-}

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

-- | recursively substitute type alias names within a type
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 }

-- | the type name components of a type
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 = \ _ _ -> [] }

-- | uninstantiate, non-generalized, unknown type variables
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