{- |
Module      :  ./HasCASL/AsUtils.hs
Description :  some utilities for the abstract syntax
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

utility functions and computations of meaningful positions for
   various data types of the abstract syntax
-}

module HasCASL.AsUtils where

import HasCASL.As
import HasCASL.FoldType
import HasCASL.HToken

import Common.DocUtils
import Common.Id
import Common.Keywords
import Common.Parsec
import qualified Control.Monad.Fail as Fail

import qualified Data.Set as Set
import qualified Text.ParserCombinators.Parsec as P

-- | the string for the universe type
typeUniverseS :: String
typeUniverseS :: String
typeUniverseS = "Type"

-- | the id of the universe type
universeId :: Id
universeId :: Id
universeId = String -> Id
stringToId String
typeUniverseS

-- | the type universe
universe :: Kind
universe :: Kind
universe = Id -> Kind
forall a. a -> AnyKind a
ClassKind Id
universeId

-- | the type universe
universeWithRange :: Range -> Kind
universeWithRange :: Range -> Kind
universeWithRange = Id -> Kind
forall a. a -> AnyKind a
ClassKind (Id -> Kind) -> (Range -> Id) -> Range -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIMPLE_ID -> Id
simpleIdToId (SIMPLE_ID -> Id) -> (Range -> SIMPLE_ID) -> Range -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Range -> SIMPLE_ID
Token String
typeUniverseS

-- | the name for the Unit type
unitTypeS :: String
unitTypeS :: String
unitTypeS = "Unit"

-- | the identifier for the Unit type
unitTypeId :: Id
unitTypeId :: Id
unitTypeId = String -> Id
stringToId String
unitTypeS

-- | single step beta reduce type abstractions
redStep :: Type -> Maybe Type
redStep :: Type -> Maybe Type
redStep ty :: Type
ty = case Type
ty of
    TypeAppl t1 :: Type
t1 t2 :: Type
t2 -> case Type
t1 of
        TypeAbs (TypeArg _ _ _ _ c :: Int
c _ _) b :: Type
b _ -> Type -> Maybe Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$
            FoldTypeRec Type -> Type -> Type
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec Type
mapTypeRec
            { foldTypeName :: Type -> Id -> RawKind -> Int -> Type
foldTypeName = \ t :: Type
t _ _ n :: Int
n -> if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
c then Type
t2 else Type
t
            , foldTypeAbs :: Type -> TypeArg -> Type -> Range -> Type
foldTypeAbs = \ t :: Type
t v1 :: TypeArg
v1@(TypeArg _ _ _ _ n :: Int
n _ _) tb :: Type
tb p :: Range
p ->
                if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
c then Type
t else TypeArg -> Type -> Range -> Type
TypeAbs TypeArg
v1 Type
tb Range
p } Type
b
        ExpandedType _ t :: Type
t -> Type -> Maybe Type
redStep (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
TypeAppl Type
t Type
t2
        KindedType t :: Type
t _ _ -> Type -> Maybe Type
redStep (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
TypeAppl Type
t Type
t2
        _ -> do
          Type
r1 <- Type -> Maybe Type
redStep Type
t1
          Type -> Maybe Type
redStep (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
TypeAppl Type
r1 Type
t2
    ExpandedType e :: Type
e t :: Type
t -> (Type -> Type) -> Maybe Type -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type -> Type -> Type
ExpandedType Type
e) (Maybe Type -> Maybe Type) -> Maybe Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
redStep Type
t
    KindedType t :: Type
t k :: Set Kind
k ps :: Range
ps -> do
      Type
r <- Type -> Maybe Type
redStep Type
t
      Type -> Maybe Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> Set Kind -> Range -> Type
KindedType Type
r Set Kind
k Range
ps
    _ -> String -> Maybe Type
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "unreducible"

strippedType :: Type -> Type
strippedType :: Type -> Type
strippedType = FoldTypeRec Type -> Type -> Type
forall a. FoldTypeRec a -> Type -> a
foldType FoldTypeRec Type
mapTypeRec
    { foldTypeAppl :: Type -> Type -> Type -> Type
foldTypeAppl = \ trm :: Type
trm f :: Type
f a :: Type
a -> let t :: Type
t = Type -> Type -> Type
TypeAppl Type
f Type
a in
        case Type -> Maybe Type
redStep Type
trm of
          Nothing -> case Type
f of
            TypeName i :: Id
i _ 0
              | Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId -> Type
a
              | Id -> Bool
isArrow Id
i -> Type -> Type -> Type
TypeAppl (Arrow -> Type
toFunType Arrow
PFunArr) Type
a
            _ -> Type
t
          Just r :: Type
r -> Type -> Type
strippedType Type
r
    , foldTypeName :: Type -> Id -> RawKind -> Int -> Type
foldTypeName = \ _ i :: Id
i k :: RawKind
k v :: Int
v -> Id -> RawKind -> Int -> Type
TypeName (if Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 then Id
i else Id
typeId) RawKind
k Int
v
    , foldKindedType :: Type -> Type -> Set Kind -> Range -> Type
foldKindedType = \ _ t :: Type
t _ _ -> Type
t
    , foldExpandedType :: Type -> Type -> Type -> Type
foldExpandedType = \ _ _ t :: Type
t -> Type
t }

eqStrippedType :: Type -> Type -> Bool
eqStrippedType :: Type -> Type -> Bool
eqStrippedType t1 :: Type
t1 t2 :: Type
t2 = Type -> Type
strippedType Type
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type -> Type
strippedType Type
t2

-- | get top-level type constructor and its arguments and beta reduce
getTypeAppl :: Type -> (Type, [Type])
getTypeAppl :: Type -> (Type, [Type])
getTypeAppl = Bool -> Type -> (Type, [Type])
getTypeApplAux Bool
True

-- | get top-level type constructor and its arguments and beta reduce if True
getTypeApplAux :: Bool -> Type -> (Type, [Type])
getTypeApplAux :: Bool -> Type -> (Type, [Type])
getTypeApplAux b :: Bool
b ty :: Type
ty = let (t :: Type
t, args :: [Type]
args) = Type -> (Type, [Type])
getTyAppl Type
ty in (Type
t, [Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
args) where
    getTyAppl :: Type -> (Type, [Type])
getTyAppl typ :: Type
typ =
      case Type
typ of
        TypeAppl t1 :: Type
t1 t2 :: Type
t2 -> case Type -> Maybe Type
redStep Type
typ of
           Just r :: Type
r | Bool
b -> Type -> (Type, [Type])
getTyAppl Type
r
           _ -> let (t :: Type
t, args :: [Type]
args) = Type -> (Type, [Type])
getTyAppl Type
t1 in (Type
t, Type
t2 Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
args)
        ExpandedType _ te :: Type
te -> let (t :: Type
t, args :: [Type]
args) = Type -> (Type, [Type])
getTyAppl Type
te in case Type
t of
           TypeName {} -> (Type
t, [Type]
args)
           _ -> if [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args then (Type
typ, []) else (Type
t, [Type]
args)
        KindedType t :: Type
t _ _ -> Type -> (Type, [Type])
getTyAppl Type
t
        _ -> (Type
typ, [])

-- | the builtin function arrows
data Arrow = FunArr | PFunArr | ContFunArr | PContFunArr deriving (Arrow -> Arrow -> Bool
(Arrow -> Arrow -> Bool) -> (Arrow -> Arrow -> Bool) -> Eq Arrow
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Arrow -> Arrow -> Bool
$c/= :: Arrow -> Arrow -> Bool
== :: Arrow -> Arrow -> Bool
$c== :: Arrow -> Arrow -> Bool
Eq, Eq Arrow
Eq Arrow =>
(Arrow -> Arrow -> Ordering)
-> (Arrow -> Arrow -> Bool)
-> (Arrow -> Arrow -> Bool)
-> (Arrow -> Arrow -> Bool)
-> (Arrow -> Arrow -> Bool)
-> (Arrow -> Arrow -> Arrow)
-> (Arrow -> Arrow -> Arrow)
-> Ord Arrow
Arrow -> Arrow -> Bool
Arrow -> Arrow -> Ordering
Arrow -> Arrow -> Arrow
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Arrow -> Arrow -> Arrow
$cmin :: Arrow -> Arrow -> Arrow
max :: Arrow -> Arrow -> Arrow
$cmax :: Arrow -> Arrow -> Arrow
>= :: Arrow -> Arrow -> Bool
$c>= :: Arrow -> Arrow -> Bool
> :: Arrow -> Arrow -> Bool
$c> :: Arrow -> Arrow -> Bool
<= :: Arrow -> Arrow -> Bool
$c<= :: Arrow -> Arrow -> Bool
< :: Arrow -> Arrow -> Bool
$c< :: Arrow -> Arrow -> Bool
compare :: Arrow -> Arrow -> Ordering
$ccompare :: Arrow -> Arrow -> Ordering
$cp1Ord :: Eq Arrow
Ord)

instance Show Arrow where
    show :: Arrow -> String
show a :: Arrow
a = case Arrow
a of
        FunArr -> String
funS
        PFunArr -> String
pFun
        ContFunArr -> String
contFun
        PContFunArr -> String
pContFun

arrowIdRange :: Range -> Arrow -> Id
arrowIdRange :: Range -> Arrow -> Id
arrowIdRange r :: Range
r a :: Arrow
a = [SIMPLE_ID] -> Id
mkId ([SIMPLE_ID] -> Id) -> [SIMPLE_ID] -> Id
forall a b. (a -> b) -> a -> b
$ (String -> SIMPLE_ID) -> [String] -> [SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Range -> SIMPLE_ID
`Token` Range
r) [String
place, Arrow -> String
forall a. Show a => a -> String
show Arrow
a, String
place]

-- | construct an infix identifier for a function arrow
arrowId :: Arrow -> Id
arrowId :: Arrow -> Id
arrowId = Range -> Arrow -> Id
arrowIdRange Range
nullRange

-- | test for a function identifier
isArrow :: Id -> Bool
isArrow :: Id -> Bool
isArrow i :: Id
i = Id -> Bool
isPartialArrow Id
i Bool -> Bool -> Bool
|| Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Id
i ((Arrow -> Id) -> [Arrow] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map Arrow -> Id
arrowId [Arrow
FunArr, Arrow
ContFunArr])

-- | test for a partial function identifier
isPartialArrow :: Id -> Bool
isPartialArrow :: Id -> Bool
isPartialArrow i :: Id
i = Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Id
i ([Id] -> Bool) -> [Id] -> Bool
forall a b. (a -> b) -> a -> b
$ (Arrow -> Id) -> [Arrow] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map Arrow -> Id
arrowId [Arrow
PFunArr, Arrow
PContFunArr]

-- | construct a mixfix product identifier with n places
productId :: Int -> Range -> Id
productId :: Int -> Range -> Id
productId n :: Int
n r :: Range
r = if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 then
  [SIMPLE_ID] -> Id
mkId ([SIMPLE_ID] -> Id) -> [SIMPLE_ID] -> Id
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID
placeTok SIMPLE_ID -> [SIMPLE_ID] -> [SIMPLE_ID]
forall a. a -> [a] -> [a]
: [[SIMPLE_ID]] -> [SIMPLE_ID]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Int -> [SIMPLE_ID] -> [[SIMPLE_ID]]
forall a. Int -> a -> [a]
replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) [String -> Range -> SIMPLE_ID
Token String
prodS Range
r, SIMPLE_ID
placeTok])
  else String -> Id
forall a. HasCallStack => String -> a
error "productId"

-- | test for a product identifier
isProductId :: Id -> Bool
isProductId :: Id -> Bool
isProductId i :: Id
i = Id -> Int -> Bool
isProductIdWithArgs Id
i 0

-- | test for a product identifier
isProductIdWithArgs :: Id -> Int -> Bool
isProductIdWithArgs :: Id -> Int -> Bool
isProductIdWithArgs (Id ts :: [SIMPLE_ID]
ts cs :: [Id]
cs _) m :: Int
m = let n :: Int
n = [SIMPLE_ID] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SIMPLE_ID]
ts in
    [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
cs Bool -> Bool -> Bool
&& (if Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 then Int
m Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Int -> Int
forall a. Integral a => a -> a -> a
div (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) 2 else Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 2) Bool -> Bool -> Bool
&& [SIMPLE_ID] -> Bool
altPlaceProd [SIMPLE_ID]
ts
     where altPlaceProd :: [SIMPLE_ID] -> Bool
altPlaceProd l :: [SIMPLE_ID]
l = case [SIMPLE_ID]
l of
               [] -> Bool
False
               t :: SIMPLE_ID
t : r :: [SIMPLE_ID]
r -> SIMPLE_ID -> Bool
isPlace SIMPLE_ID
t Bool -> Bool -> Bool
&& [SIMPLE_ID] -> Bool
altProdPlace [SIMPLE_ID]
r
           altProdPlace :: [SIMPLE_ID] -> Bool
altProdPlace l :: [SIMPLE_ID]
l = case [SIMPLE_ID]
l of
               [] -> Bool
True
               t :: SIMPLE_ID
t : r :: [SIMPLE_ID]
r -> SIMPLE_ID -> String
tokStr SIMPLE_ID
t String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
prodS Bool -> Bool -> Bool
&& [SIMPLE_ID] -> Bool
altPlaceProd [SIMPLE_ID]
r

-- | map a kind and its variance
mapKindV :: (Variance -> Variance) -> (a -> b) -> AnyKind a -> AnyKind b
mapKindV :: (Variance -> Variance) -> (a -> b) -> AnyKind a -> AnyKind b
mapKindV g :: Variance -> Variance
g f :: a -> b
f k :: AnyKind a
k = case AnyKind a
k of
    ClassKind a :: a
a -> b -> AnyKind b
forall a. a -> AnyKind a
ClassKind (b -> AnyKind b) -> b -> AnyKind b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
a
    FunKind v :: Variance
v a :: AnyKind a
a b :: AnyKind a
b r :: Range
r -> Variance -> AnyKind b -> AnyKind b -> Range -> AnyKind b
forall a. Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
FunKind (Variance -> Variance
g Variance
v) ((Variance -> Variance) -> (a -> b) -> AnyKind a -> AnyKind b
forall a b.
(Variance -> Variance) -> (a -> b) -> AnyKind a -> AnyKind b
mapKindV Variance -> Variance
g a -> b
f AnyKind a
a) ((Variance -> Variance) -> (a -> b) -> AnyKind a -> AnyKind b
forall a b.
(Variance -> Variance) -> (a -> b) -> AnyKind a -> AnyKind b
mapKindV Variance -> Variance
g a -> b
f AnyKind a
b) Range
r

-- | map a kind and keep variance the same
mapKind :: (a -> b) -> AnyKind a -> AnyKind b
mapKind :: (a -> b) -> AnyKind a -> AnyKind b
mapKind = (Variance -> Variance) -> (a -> b) -> AnyKind a -> AnyKind b
forall a b.
(Variance -> Variance) -> (a -> b) -> AnyKind a -> AnyKind b
mapKindV Variance -> Variance
forall a. a -> a
id

-- | ignore variances of raw kinds
nonVarRawKind :: RawKind -> RawKind
nonVarRawKind :: RawKind -> RawKind
nonVarRawKind = (Variance -> Variance) -> (() -> ()) -> RawKind -> RawKind
forall a b.
(Variance -> Variance) -> (a -> b) -> AnyKind a -> AnyKind b
mapKindV (Variance -> Variance -> Variance
forall a b. a -> b -> a
const Variance
NonVar) () -> ()
forall a. a -> a
id

-- | compute raw kind (if class ids or no higher kinds)
toRaw :: Kind -> RawKind
toRaw :: Kind -> RawKind
toRaw = (Id -> ()) -> Kind -> RawKind
forall a b. (a -> b) -> AnyKind a -> AnyKind b
mapKind ((Id -> ()) -> Kind -> RawKind) -> (Id -> ()) -> Kind -> RawKind
forall a b. (a -> b) -> a -> b
$ () -> Id -> ()
forall a b. a -> b -> a
const ()

-- | the type universe as raw kind
rStar :: RawKind
rStar :: RawKind
rStar = () -> RawKind
forall a. a -> AnyKind a
ClassKind ()

-- | the Unit type (name)
unitType :: Type
unitType :: Type
unitType = Id -> Type
toType Id
unitTypeId

-- | the Unit type (name)
unitTypeWithRange :: Range -> Type
unitTypeWithRange :: Range -> Type
unitTypeWithRange = Id -> Type
toType (Id -> Type) -> (Range -> Id) -> Range -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIMPLE_ID -> Id
simpleIdToId (SIMPLE_ID -> Id) -> (Range -> SIMPLE_ID) -> Range -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Range -> SIMPLE_ID
Token String
unitTypeS

-- | the prefix name for lazy types
lazyTypeId :: Id
lazyTypeId :: Id
lazyTypeId = [SIMPLE_ID] -> Id
mkId [String -> SIMPLE_ID
mkSimpleId "?"]

-- | the kind of the lazy type constructor
coKind :: Kind
coKind :: Kind
coKind = Variance -> Kind -> Kind -> Range -> Kind
forall a. Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
FunKind Variance
CoVar Kind
universe Kind
universe Range
nullRange

-- | the lazy type constructor
lazyTypeConstr :: Type
lazyTypeConstr :: Type
lazyTypeConstr = Id -> RawKind -> Int -> Type
TypeName Id
lazyTypeId (Kind -> RawKind
toRaw Kind
coKind) 0

-- | make a type lazy
mkLazyType :: Type -> Type
mkLazyType :: Type -> Type
mkLazyType = Type -> Type -> Type
TypeAppl Type
lazyTypeConstr

-- | function type
mkFunArrType :: Type -> Arrow -> Type -> Type
mkFunArrType :: Type -> Arrow -> Type -> Type
mkFunArrType = Range -> Type -> Arrow -> Type -> Type
mkFunArrTypeWithRange Range
nullRange

mkFunArrTypeWithRange :: Range -> Type -> Arrow -> Type -> Type
mkFunArrTypeWithRange :: Range -> Type -> Arrow -> Type -> Type
mkFunArrTypeWithRange r :: Range
r t1 :: Type
t1 a :: Arrow
a t2 :: Type
t2 = Type -> [Type] -> Type
mkTypeAppl (Range -> Arrow -> Type
toFunTypeRange Range
r Arrow
a) [Type
t1, Type
t2]

-- | construct a product type
mkProductType :: [Type] -> Type
mkProductType :: [Type] -> Type
mkProductType ts :: [Type]
ts = [Type] -> Range -> Type
mkProductTypeWithRange [Type]
ts Range
nullRange

-- | construct a product type
mkProductTypeWithRange :: [Type] -> Range -> Type
mkProductTypeWithRange :: [Type] -> Range -> Type
mkProductTypeWithRange ts :: [Type]
ts r :: Range
r = case [Type]
ts of
    [] -> Type
unitType
    [t :: Type
t] -> Type
t
    _ -> let n :: Int
n = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts in
         Type -> [Type] -> Type
mkTypeAppl (Int -> Range -> Type
toProdType Int
n Range
r) [Type]
ts

-- | convert a type with unbound variables to a scheme
simpleTypeScheme :: Type -> TypeScheme
simpleTypeScheme :: Type -> TypeScheme
simpleTypeScheme t :: Type
t = [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [] Type
t Range
nullRange

{- | add the unit type as result type or convert a parsed empty tuple
   to the unit type -}
predType :: Range -> Type -> Type
predType :: Range -> Type -> Type
predType r :: Range
r t :: Type
t = case Type
t of
    BracketType Parens [] _ -> Type -> Type
mkLazyType (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Range -> Type
unitTypeWithRange Range
r
    _ -> Range -> Type -> Arrow -> Type -> Type
mkFunArrTypeWithRange Range
r Type
t Arrow
PFunArr (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Range -> Type
unitTypeWithRange Range
r

-- | change the type of the scheme to a 'predType'
predTypeScheme :: Range -> TypeScheme -> TypeScheme
predTypeScheme :: Range -> TypeScheme -> TypeScheme
predTypeScheme = (Type -> Type) -> TypeScheme -> TypeScheme
mapTypeOfScheme ((Type -> Type) -> TypeScheme -> TypeScheme)
-> (Range -> Type -> Type) -> Range -> TypeScheme -> TypeScheme
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Type -> Type
predType

-- | check for and remove predicate arrow
unPredType :: Type -> (Bool, Type)
unPredType :: Type -> (Bool, Type)
unPredType t :: Type
t = case Type -> (Type, [Type])
getTypeAppl Type
t of
    (TypeName at :: Id
at _ 0, [ty :: Type
ty, TypeName ut :: Id
ut (ClassKind _) 0])
        | Id
ut Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
unitTypeId Bool -> Bool -> Bool
&& Id
at Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Arrow -> Id
arrowId Arrow
PFunArr -> (Bool
True, Type
ty)
    (TypeName lt :: Id
lt _ 0, [TypeName ut :: Id
ut (ClassKind _) 0])
        | Id
ut Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
unitTypeId Bool -> Bool -> Bool
&& Id
lt Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
         (Bool
True, BracketKind -> [Type] -> Range -> Type
BracketType BracketKind
Parens [] Range
nullRange) -- for printing only
    _ -> (Bool
False, Type
t)

-- | test if type is a predicate type
isPredType :: Type -> Bool
isPredType :: Type -> Bool
isPredType = (Bool, Type) -> Bool
forall a b. (a, b) -> a
fst ((Bool, Type) -> Bool) -> (Type -> (Bool, Type)) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (Bool, Type)
unPredType

-- |  remove predicate arrow in a type scheme
unPredTypeScheme :: TypeScheme -> TypeScheme
unPredTypeScheme :: TypeScheme -> TypeScheme
unPredTypeScheme = (Type -> Type) -> TypeScheme -> TypeScheme
mapTypeOfScheme ((Bool, Type) -> Type
forall a b. (a, b) -> b
snd ((Bool, Type) -> Type) -> (Type -> (Bool, Type)) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (Bool, Type)
unPredType)

funKindWithRange3 :: Range -> Kind -> Kind -> Kind -> Kind
funKindWithRange3 :: Range -> Kind -> Kind -> Kind -> Kind
funKindWithRange3 r :: Range
r a :: Kind
a b :: Kind
b c :: Kind
c = Variance -> Kind -> Kind -> Range -> Kind
forall a. Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
FunKind Variance
ContraVar Kind
a (Variance -> Kind -> Kind -> Range -> Kind
forall a. Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
FunKind Variance
CoVar Kind
b Kind
c Range
r) Range
r

funKind3 :: Kind -> Kind -> Kind -> Kind
funKind3 :: Kind -> Kind -> Kind -> Kind
funKind3 = Range -> Kind -> Kind -> Kind -> Kind
funKindWithRange3 Range
nullRange

funKindWithRange :: Range -> Kind
funKindWithRange :: Range -> Kind
funKindWithRange r :: Range
r = let c :: Kind
c = Range -> Kind
universeWithRange Range
r in Range -> Kind -> Kind -> Kind -> Kind
funKindWithRange3 Range
r Kind
c Kind
c Kind
c

-- | the kind of the function type
funKind :: Kind
funKind :: Kind
funKind = Range -> Kind
funKindWithRange Range
nullRange

-- | construct higher order kind from arguments and result kind
mkFunKind :: Range -> [(Variance, AnyKind a)] -> AnyKind a -> AnyKind a
mkFunKind :: Range -> [(Variance, AnyKind a)] -> AnyKind a -> AnyKind a
mkFunKind r :: Range
r args :: [(Variance, AnyKind a)]
args res :: AnyKind a
res = ((Variance, AnyKind a) -> AnyKind a -> AnyKind a)
-> AnyKind a -> [(Variance, AnyKind a)] -> AnyKind a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ (v :: Variance
v, a :: AnyKind a
a) k :: AnyKind a
k -> Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
forall a. Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
FunKind Variance
v AnyKind a
a AnyKind a
k Range
r) AnyKind a
res [(Variance, AnyKind a)]
args

-- | the 'Kind' of the product type
prodKind1 :: Int -> Range -> Kind -> Kind
prodKind1 :: Int -> Range -> Kind -> Kind
prodKind1 n :: Int
n r :: Range
r c :: Kind
c =
    if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 then Range -> [(Variance, Kind)] -> Kind -> Kind
forall a.
Range -> [(Variance, AnyKind a)] -> AnyKind a -> AnyKind a
mkFunKind Range
r (Int -> (Variance, Kind) -> [(Variance, Kind)]
forall a. Int -> a -> [a]
replicate Int
n (Variance
CoVar, Kind
c)) Kind
c
    else String -> Kind
forall a. HasCallStack => String -> a
error "prodKind"

prodKind :: Int -> Range -> Kind
prodKind :: Int -> Range -> Kind
prodKind n :: Int
n r :: Range
r = Int -> Range -> Kind -> Kind
prodKind1 Int
n Range
r Kind
universe

-- | a type name with a universe kind
toType :: Id -> Type
toType :: Id -> Type
toType i :: Id
i = Id -> RawKind -> Int -> Type
TypeName Id
i RawKind
rStar 0

toFunTypeRange :: Range -> Arrow -> Type
toFunTypeRange :: Range -> Arrow -> Type
toFunTypeRange r :: Range
r a :: Arrow
a = Id -> RawKind -> Int -> Type
TypeName (Range -> Arrow -> Id
arrowIdRange Range
r Arrow
a) (Kind -> RawKind
toRaw (Kind -> RawKind) -> Kind -> RawKind
forall a b. (a -> b) -> a -> b
$ Range -> Kind
funKindWithRange Range
r) 0

-- | the type name for a function arrow
toFunType :: Arrow -> Type
toFunType :: Arrow -> Type
toFunType = Range -> Arrow -> Type
toFunTypeRange Range
nullRange

-- | the type name for a function arrow
toProdType :: Int -> Range -> Type
toProdType :: Int -> Range -> Type
toProdType n :: Int
n r :: Range
r = Id -> RawKind -> Int -> Type
TypeName (Int -> Range -> Id
productId Int
n Range
r) (Kind -> RawKind
toRaw (Kind -> RawKind) -> Kind -> RawKind
forall a b. (a -> b) -> a -> b
$ Int -> Range -> Kind
prodKind Int
n Range
r) 0

-- | the brackets as tokens with positions
mkBracketToken :: BracketKind -> Range -> [Token]
mkBracketToken :: BracketKind -> Range -> [SIMPLE_ID]
mkBracketToken k :: BracketKind
k ps :: Range
ps =
    (String -> SIMPLE_ID) -> [String] -> [SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> Range -> SIMPLE_ID) -> Range -> String -> SIMPLE_ID
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> Range -> SIMPLE_ID
Token Range
ps) ([String] -> [SIMPLE_ID]) -> [String] -> [SIMPLE_ID]
forall a b. (a -> b) -> a -> b
$ (\ (o :: String
o, c :: String
c) -> [String
o, String
c]) ((String, String) -> [String]) -> (String, String) -> [String]
forall a b. (a -> b) -> a -> b
$ BracketKind -> (String, String)
getBrackets BracketKind
k

-- | construct a tuple from non-singleton lists
mkTupleTerm :: [Term] -> Range -> Term
mkTupleTerm :: [Term] -> Range -> Term
mkTupleTerm ts :: [Term]
ts ps :: Range
ps = if [Term] -> Bool
forall a. [a] -> Bool
isSingle [Term]
ts then [Term] -> Term
forall a. [a] -> a
head [Term]
ts else [Term] -> Range -> Term
TupleTerm [Term]
ts Range
ps

-- | try to extract tuple arguments
getTupleArgs :: Term -> Maybe [Term]
getTupleArgs :: Term -> Maybe [Term]
getTupleArgs t :: Term
t = case Term
t of
    TypedTerm trm :: Term
trm qt :: TypeQual
qt _ _ -> case TypeQual
qt of
      InType -> Maybe [Term]
forall a. Maybe a
Nothing
      _ -> Term -> Maybe [Term]
getTupleArgs Term
trm
    TupleTerm ts :: [Term]
ts _ -> [Term] -> Maybe [Term]
forall a. a -> Maybe a
Just [Term]
ts
    _ -> Maybe [Term]
forall a. Maybe a
Nothing

{- | decompose an 'ApplTerm' into an application of an operation and a
     list of arguments -}
getAppl :: Term -> Maybe (Id, TypeScheme, [Term])
getAppl :: Term -> Maybe (Id, TypeScheme, [Term])
getAppl = ([Term] -> [Term])
-> Maybe (Id, TypeScheme, [Term]) -> Maybe (Id, TypeScheme, [Term])
forall c a b. (c -> c) -> Maybe (a, b, c) -> Maybe (a, b, c)
thrdM [Term] -> [Term]
forall a. [a] -> [a]
reverse (Maybe (Id, TypeScheme, [Term]) -> Maybe (Id, TypeScheme, [Term]))
-> (Term -> Maybe (Id, TypeScheme, [Term]))
-> Term
-> Maybe (Id, TypeScheme, [Term])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe (Id, TypeScheme, [Term])
getRevAppl where
    thrdM :: (c -> c) -> Maybe (a, b, c) -> Maybe (a, b, c)
    thrdM :: (c -> c) -> Maybe (a, b, c) -> Maybe (a, b, c)
thrdM f :: c -> c
f = ((a, b, c) -> (a, b, c)) -> Maybe (a, b, c) -> Maybe (a, b, c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ( \ (a :: a
a, b :: b
b, c :: c
c) -> (a
a, b
b, c -> c
f c
c))
    getRevAppl :: Term -> Maybe (Id, TypeScheme, [Term])
    getRevAppl :: Term -> Maybe (Id, TypeScheme, [Term])
getRevAppl t :: Term
t = case Term
t of
        TypedTerm trm :: Term
trm q :: TypeQual
q _ _ -> case TypeQual
q of
            InType -> Maybe (Id, TypeScheme, [Term])
forall a. Maybe a
Nothing
            _ -> Term -> Maybe (Id, TypeScheme, [Term])
getRevAppl Term
trm
        QualOp _ (PolyId i :: Id
i _ _) sc :: TypeScheme
sc _ _ _ -> (Id, TypeScheme, [Term]) -> Maybe (Id, TypeScheme, [Term])
forall a. a -> Maybe a
Just (Id
i, TypeScheme
sc, [])
        QualVar (VarDecl v :: Id
v ty :: Type
ty _ _) -> (Id, TypeScheme, [Term]) -> Maybe (Id, TypeScheme, [Term])
forall a. a -> Maybe a
Just (Id
v, Type -> TypeScheme
simpleTypeScheme Type
ty, [])
        ApplTerm t1 :: Term
t1 t2 :: Term
t2 _ -> ([Term] -> [Term])
-> Maybe (Id, TypeScheme, [Term]) -> Maybe (Id, TypeScheme, [Term])
forall c a b. (c -> c) -> Maybe (a, b, c) -> Maybe (a, b, c)
thrdM (Term
t2 Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:) (Maybe (Id, TypeScheme, [Term]) -> Maybe (Id, TypeScheme, [Term]))
-> Maybe (Id, TypeScheme, [Term]) -> Maybe (Id, TypeScheme, [Term])
forall a b. (a -> b) -> a -> b
$ Term -> Maybe (Id, TypeScheme, [Term])
getRevAppl Term
t1
        _ -> Maybe (Id, TypeScheme, [Term])
forall a. Maybe a
Nothing

-- | split the list of generic variables into values and type variables
splitVars :: [GenVarDecl] -> ([VarDecl], [TypeArg])
splitVars :: [GenVarDecl] -> ([VarDecl], [TypeArg])
splitVars l :: [GenVarDecl]
l = let f :: GenVarDecl -> ([VarDecl], [TypeArg]) -> ([VarDecl], [TypeArg])
f x :: GenVarDecl
x (vs :: [VarDecl]
vs, tvs :: [TypeArg]
tvs) =
                      case GenVarDecl
x of
                        GenVarDecl vd :: VarDecl
vd -> (VarDecl
vd VarDecl -> [VarDecl] -> [VarDecl]
forall a. a -> [a] -> [a]
: [VarDecl]
vs, [TypeArg]
tvs)
                        GenTypeVarDecl tv :: TypeArg
tv -> ([VarDecl]
vs, TypeArg
tv TypeArg -> [TypeArg] -> [TypeArg]
forall a. a -> [a] -> [a]
: [TypeArg]
tvs)
              in (GenVarDecl -> ([VarDecl], [TypeArg]) -> ([VarDecl], [TypeArg]))
-> ([VarDecl], [TypeArg]) -> [GenVarDecl] -> ([VarDecl], [TypeArg])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr GenVarDecl -> ([VarDecl], [TypeArg]) -> ([VarDecl], [TypeArg])
f ([], []) [GenVarDecl]
l


-- | extract bindings from an analysed pattern
extractVars :: Term -> [VarDecl]
extractVars :: Term -> [VarDecl]
extractVars pat :: Term
pat = case Term
pat of
    QualVar vd :: VarDecl
vd -> VarDecl -> [VarDecl]
getVd VarDecl
vd
    ApplTerm p1 :: Term
p1 p2 :: Term
p2 _ ->
         Term -> [VarDecl]
extractVars Term
p1 [VarDecl] -> [VarDecl] -> [VarDecl]
forall a. [a] -> [a] -> [a]
++ Term -> [VarDecl]
extractVars Term
p2
    TupleTerm pats :: [Term]
pats _ -> (Term -> [VarDecl]) -> [Term] -> [VarDecl]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Term -> [VarDecl]
extractVars [Term]
pats
    TypedTerm p :: Term
p _ _ _ -> Term -> [VarDecl]
extractVars Term
p
    AsPattern v :: VarDecl
v p2 :: Term
p2 _ -> VarDecl -> [VarDecl]
getVd VarDecl
v [VarDecl] -> [VarDecl] -> [VarDecl]
forall a. [a] -> [a] -> [a]
++ Term -> [VarDecl]
extractVars Term
p2
    ResolvedMixTerm _ _ pats :: [Term]
pats _ -> (Term -> [VarDecl]) -> [Term] -> [VarDecl]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Term -> [VarDecl]
extractVars [Term]
pats
    _ -> []
    where getVd :: VarDecl -> [VarDecl]
getVd vd :: VarDecl
vd@(VarDecl v :: Id
v _ _ _) = if Id -> ShowS
showId Id
v "" String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "_" then [] else [VarDecl
vd]

-- | construct term from id
mkOpTerm :: Id -> TypeScheme -> Term
mkOpTerm :: Id -> TypeScheme -> Term
mkOpTerm i :: Id
i sc :: TypeScheme
sc = OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
Op (Id -> [TypeArg] -> Range -> PolyId
PolyId Id
i [] Range
nullRange) TypeScheme
sc [] InstKind
Infer Range
nullRange

-- | bind a term
mkForall :: [GenVarDecl] -> Term -> Term
mkForall :: [GenVarDecl] -> Term -> Term
mkForall vl :: [GenVarDecl]
vl f :: Term
f = if [GenVarDecl] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [GenVarDecl]
vl then Term
f else Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm Quantifier
Universal [GenVarDecl]
vl Term
f Range
nullRange

-- | construct application with curried arguments
mkApplTerm :: Term -> [Term] -> Term
mkApplTerm :: Term -> [Term] -> Term
mkApplTerm = (Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ( \ t :: Term
t a :: Term
a -> Term -> Term -> Range -> Term
ApplTerm Term
t Term
a Range
nullRange)

-- | make function arrow partial after some arguments
addPartiality :: [a] -> Type -> Type
addPartiality :: [a] -> Type -> Type
addPartiality args :: [a]
args t :: Type
t = case [a]
args of
    [] -> Type -> Type
mkLazyType Type
t
    _ : rs :: [a]
rs -> case Type -> (Type, [Type])
getTypeAppl Type
t of
        (TypeName a :: Id
a _ _, [t1 :: Type
t1, t2 :: Type
t2]) | Id
a Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Arrow -> Id
arrowId Arrow
FunArr ->
            if [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
rs then case Type -> (Type, [Type])
getTypeAppl Type
t2 of
                (TypeName l :: Id
l _ _, [t3 :: Type
t3]) | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId
                   -> Type -> Arrow -> Type -> Type
mkFunArrType Type
t1 Arrow
PFunArr Type
t3
                _ -> Type -> Arrow -> Type -> Type
mkFunArrType Type
t1 Arrow
PFunArr Type
t2
            else Type -> Arrow -> Type -> Type
mkFunArrType Type
t1 Arrow
FunArr (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ [a] -> Type -> Type
forall a. [a] -> Type -> Type
addPartiality [a]
rs Type
t2
        _ -> String -> Type
forall a. HasCallStack => String -> a
error "addPartiality"

-- | convert a type argument to a type
typeArgToType :: TypeArg -> Type
typeArgToType :: TypeArg -> Type
typeArgToType (TypeArg i :: Id
i _ _ rk :: RawKind
rk c :: Int
c _ _) = Id -> RawKind -> Int -> Type
TypeName Id
i RawKind
rk Int
c

{- | convert a parameterized type identifier with a result raw kind
     to a type application -}
patToType :: Id -> [TypeArg] -> RawKind -> Type
patToType :: Id -> [TypeArg] -> RawKind -> Type
patToType i :: Id
i args :: [TypeArg]
args rk :: RawKind
rk =
    Type -> [Type] -> Type
mkTypeAppl (Id -> RawKind -> Int -> Type
TypeName Id
i ([TypeArg] -> RawKind -> RawKind
typeArgsListToRawKind [TypeArg]
args RawKind
rk) 0)
    ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (TypeArg -> Type) -> [TypeArg] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> Type
typeArgToType [TypeArg]
args

-- | create the (raw if True) kind from type arguments
typeArgsListToRawKind :: [TypeArg] -> RawKind -> RawKind
typeArgsListToRawKind :: [TypeArg] -> RawKind -> RawKind
typeArgsListToRawKind tArgs :: [TypeArg]
tArgs = Range -> [(Variance, RawKind)] -> RawKind -> RawKind
forall a.
Range -> [(Variance, AnyKind a)] -> AnyKind a -> AnyKind a
mkFunKind ([TypeArg] -> Range
forall a. GetRange a => a -> Range
getRange [TypeArg]
tArgs) ([(Variance, RawKind)] -> RawKind -> RawKind)
-> [(Variance, RawKind)] -> RawKind -> RawKind
forall a b. (a -> b) -> a -> b
$
    (TypeArg -> (Variance, RawKind))
-> [TypeArg] -> [(Variance, RawKind)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (TypeArg _ v :: Variance
v _ rk :: RawKind
rk _ _ _) -> (Variance
v, RawKind
rk)) [TypeArg]
tArgs

-- | create the kind from type arguments
typeArgsListToKind :: [TypeArg] -> Kind -> Kind
typeArgsListToKind :: [TypeArg] -> Kind -> Kind
typeArgsListToKind tArgs :: [TypeArg]
tArgs = Range -> [(Variance, Kind)] -> Kind -> Kind
forall a.
Range -> [(Variance, AnyKind a)] -> AnyKind a -> AnyKind a
mkFunKind ([TypeArg] -> Range
forall a. GetRange a => a -> Range
getRange [TypeArg]
tArgs) ([(Variance, Kind)] -> Kind -> Kind)
-> [(Variance, Kind)] -> Kind -> Kind
forall a b. (a -> b) -> a -> b
$
    (TypeArg -> (Variance, Kind)) -> [TypeArg] -> [(Variance, Kind)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (TypeArg _ v :: Variance
v ak :: VarKind
ak _ _ _ _) -> (Variance
v, VarKind -> Kind
toKind VarKind
ak)) [TypeArg]
tArgs

-- | get the type of a constructor with given curried argument types
getFunType :: Type -> Partiality -> [Type] -> Type
getFunType :: Type -> Partiality -> [Type] -> Type
getFunType rty :: Type
rty p :: Partiality
p ts :: [Type]
ts = (case Partiality
p of
    Total -> Type -> Type
forall a. a -> a
id
    Partial -> [Type] -> Type -> Type
forall a. [a] -> Type -> Type
addPartiality [Type]
ts)
    (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> Arrow -> Type -> Type
`mkFunArrType` Arrow
FunArr) Type
rty [Type]
ts

-- | get the type of a selector given the data type as first arguemnt
getSelType :: Type -> Partiality -> Type -> Type
getSelType :: Type -> Partiality -> Type -> Type
getSelType dt :: Type
dt p :: Partiality
p = (case Partiality
p of
    Partial -> [Type] -> Type -> Type
forall a. [a] -> Type -> Type
addPartiality [Type
dt]
    Total -> Type -> Type
forall a. a -> a
id) (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Arrow -> Type -> Type
mkFunArrType Type
dt Arrow
FunArr

-- | make type argument non-variant
nonVarTypeArg :: TypeArg -> TypeArg
nonVarTypeArg :: TypeArg -> TypeArg
nonVarTypeArg (TypeArg i :: Id
i _ vk :: VarKind
vk rk :: RawKind
rk c :: Int
c o :: SeparatorKind
o p :: Range
p) = Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
i Variance
NonVar VarKind
vk RawKind
rk Int
c SeparatorKind
o Range
p

-- | get the type variable
getTypeVar :: TypeArg -> Id
getTypeVar :: TypeArg -> Id
getTypeVar (TypeArg v :: Id
v _ _ _ _ _ _) = Id
v

-- | construct application left-associative
mkTypeAppl :: Type -> [Type] -> Type
mkTypeAppl :: Type -> [Type] -> Type
mkTypeAppl = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Type -> Type -> Type
TypeAppl

-- | get the kind of an analyzed type variable
toKind :: VarKind -> Kind
toKind :: VarKind -> Kind
toKind vk :: VarKind
vk = case VarKind
vk of
    VarKind k :: Kind
k -> Kind
k
    Downset t :: Type
t -> case Type
t of
        KindedType _ k :: Set Kind
k _ | Set Kind -> Int
forall a. Set a -> Int
Set.size Set Kind
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 -> Set Kind -> Kind
forall a. Set a -> a
Set.findMin Set Kind
k
        _ -> String -> Kind
forall a. HasCallStack => String -> a
error "toKind: Downset"
    MissingKind -> String -> Kind
forall a. HasCallStack => String -> a
error "toKind: Missing"

-- | try to reparse the pretty printed input as an identifier
reparseAsId :: Pretty a => a -> Maybe Id
reparseAsId :: a -> Maybe Id
reparseAsId t :: a
t = case Parsec String () Id -> String -> String -> Either ParseError Id
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
P.parse (Parsec String () Id
forall st. GenParser Char st Id
opId Parsec String () Id
-> ParsecT String () Identity () -> Parsec String () Id
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
P.eof) "" (String -> Either ParseError Id) -> String -> Either ParseError Id
forall a b. (a -> b) -> a -> b
$ a -> ShowS
forall a. Pretty a => a -> ShowS
showDoc a
t "" of
               Right x :: Id
x -> Id -> Maybe Id
forall a. a -> Maybe a
Just Id
x
               _ -> Maybe Id
forall a. Maybe a
Nothing

-- | generate a comparison string
expected :: Pretty a => a -> a -> String
expected :: a -> a -> String
expected a :: a
a b :: a
b =
    "\n  expected: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> ShowS
forall a. Pretty a => a -> ShowS
showDoc a
a
    "\n     found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> ShowS
forall a. Pretty a => a -> ShowS
showDoc a
b "\n"