{- |
Module      :  ./HasCASL/TypeMixAna.hs
Description :  manually resolve mixfix type applications
Copyright   :  (c) Christian Maeder and Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

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

analyse mixfix types

-}

module HasCASL.TypeMixAna (mkTypeConstrAppl) where

import HasCASL.As
import HasCASL.Le
import HasCASL.AsUtils
import HasCASL.PrintAs ()
import Common.DocUtils
import Common.Id
import Common.Result
import qualified Data.Set as Set

-- | resolve parsed mixfix type to type applications with dummy kinds
mkTypeConstrAppl :: Env -> Type -> Result Type
mkTypeConstrAppl :: Env -> Type -> Result Type
mkTypeConstrAppl = ApplMode -> Env -> Type -> Result Type
mkTypeConstrAppls ApplMode
TopLevel

-- | construct application differently for left and right arguments
data ApplMode = TopLevel | OnlyArg

-- | manual mixfix resolution of parsed types
mkTypeConstrAppls :: ApplMode -> Env -> Type -> Result Type
mkTypeConstrAppls :: ApplMode -> Env -> Type -> Result Type
mkTypeConstrAppls m :: ApplMode
m e :: Env
e ty :: Type
ty = case Type
ty of
    TypeName {} -> Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
    TypeToken tt :: Token
tt -> Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Result Type) -> Type -> Result Type
forall a b. (a -> b) -> a -> b
$ Id -> Type
toType (Id -> Type) -> Id -> Type
forall a b. (a -> b) -> a -> b
$ Token -> Id
simpleIdToId Token
tt
    BracketType b :: BracketKind
b ts :: [Type]
ts ps :: Range
ps -> do
       [Type]
args <- (Type -> Result Type) -> [Type] -> Result [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ApplMode -> Env -> Type -> Result Type
mkTypeConstrAppls ApplMode
m Env
e) [Type]
ts
       case BracketKind
b of
         Squares -> () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
hint () ("a non-compound list: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Type
ty "") Range
ps
         _ -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       case [Type]
args of
         [] -> Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Result Type) -> Type -> Result Type
forall a b. (a -> b) -> a -> b
$ case BracketKind
b of
             Parens -> Type
unitType
             _ -> Id -> Type
toType (Id -> Type) -> Id -> Type
forall a b. (a -> b) -> a -> b
$ [Token] -> Id
mkId ([Token] -> Id) -> [Token] -> Id
forall a b. (a -> b) -> a -> b
$ BracketKind -> Range -> [Token]
mkBracketToken BracketKind
b Range
ps
         [x :: Type
x] -> Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Result Type) -> Type -> Result Type
forall a b. (a -> b) -> a -> b
$ case BracketKind
b of
             Parens -> Type
x
             _ -> let
                 [o :: Token
o, c :: Token
c] = BracketKind -> Range -> [Token]
mkBracketToken BracketKind
b Range
ps
                 t :: Type
t = Id -> RawKind -> Int -> Type
TypeName ([Token] -> Id
mkId [Token
o, String -> Range -> Token
Token String
place Range
ps, Token
c])
                     (Kind -> RawKind
toRaw Kind
coKind) 0
                 in if Type -> Bool
isPlaceType ([Type] -> Type
forall a. [a] -> a
head [Type]
ts) then Type
t else Type -> Type -> Type
TypeAppl Type
t Type
x
         _ -> String -> Type -> Result Type
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "illegal type" Type
ty
    MixfixType l :: [Type]
l -> case Env -> [Type] -> [Type]
mkCompoundTypeIds Env
e [Type]
l of
         f :: Type
f : a :: [Type]
a -> do
           Type
newF <- ApplMode -> Env -> Type -> Result Type
mkTypeConstrAppls ApplMode
TopLevel Env
e Type
f
           [Type]
nA <- (Type -> Result Type) -> [Type] -> Result [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ApplMode -> Env -> Type -> Result Type
mkTypeConstrAppls ApplMode
OnlyArg Env
e) [Type]
a
           Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Result Type) -> Type -> Result Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Type) -> [Type] -> Type
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Type -> Type -> Type
TypeAppl ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ Type
newF Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
nA
         [] -> String -> Result Type
forall a. HasCallStack => String -> a
error "mkTypeConstrAppl (MixfixType [])"
    KindedType t :: Type
t k :: Set Kind
k p :: Range
p -> do
       Type
newT <- ApplMode -> Env -> Type -> Result Type
mkTypeConstrAppls ApplMode
m Env
e Type
t
       Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Result Type) -> Type -> Result Type
forall a b. (a -> b) -> a -> b
$ Type -> Set Kind -> Range -> Type
KindedType Type
newT Set Kind
k Range
p
    _ -> case Type -> (Type, [Type])
getTypeAppl Type
ty of
       (top :: Type
top@(TypeName i :: Id
i _ _), ts :: [Type]
ts) -> let n :: Int
n = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts in
           if Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then do
           Type
newT <- ApplMode -> Env -> Type -> Result Type
mkTypeConstrAppls ApplMode
TopLevel Env
e (Type -> Result Type) -> Type -> Result Type
forall a b. (a -> b) -> a -> b
$ [Type] -> Type
forall a. [a] -> a
head [Type]
ts
           Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Result Type) -> Type -> Result Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
mkLazyType Type
newT
           else if Id -> Int -> Bool
isProductIdWithArgs Id
i Int
n then
             if (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
isPlaceType [Type]
ts then
                Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
top else do
                [Type]
mTs <- (Type -> Result Type) -> [Type] -> Result [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ApplMode -> Env -> Type -> Result Type
mkTypeConstrAppls ApplMode
TopLevel Env
e) [Type]
ts
                Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Result Type) -> Type -> Result Type
forall a b. (a -> b) -> a -> b
$ [Type] -> Range -> Type
mkProductTypeWithRange [Type]
mTs (Range -> Type) -> Range -> Type
forall a b. (a -> b) -> a -> b
$ Id -> Range
posOfId Id
i
           else if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 2 Bool -> Bool -> Bool
&& Id -> Bool
isArrow Id
i then
                if (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
isPlaceType [Type]
ts then
                Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
top else do
                [Type]
mTs <- (Type -> Result Type) -> [Type] -> Result [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ApplMode -> Env -> Type -> Result Type
mkTypeConstrAppls ApplMode
TopLevel Env
e) [Type]
ts
                Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Result Type) -> Type -> Result Type
forall a b. (a -> b) -> a -> b
$ Type -> [Type] -> Type
mkTypeAppl Type
top [Type]
mTs
           else String -> Result Type
forall a. HasCallStack => String -> a
error "mkTypeConstrAppls"
       _ -> String -> Result Type
forall a. HasCallStack => String -> a
error (String -> Result Type) -> String -> Result Type
forall a b. (a -> b) -> a -> b
$ "mkTypeConstrAppls " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Type
ty "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty

mkCompoundTypeIds :: Env -> [Type] -> [Type]
mkCompoundTypeIds :: Env -> [Type] -> [Type]
mkCompoundTypeIds e :: Env
e l :: [Type]
l = case [Type]
l of
    a :: Type
a@(TypeToken t :: Token
t) : b :: Type
b@(BracketType Squares as :: [Type]
as ps :: Range
ps) : r :: [Type]
r ->
        let mis :: Maybe [Id]
mis = (Type -> Maybe Id) -> [Type] -> Maybe [Id]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> Maybe Id
forall a. Pretty a => a -> Maybe Id
reparseAsId [Type]
as in
        case Maybe [Id]
mis of
          Just cs :: [Id]
cs | [Id] -> Set [Id] -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member [Id]
cs (Set [Id] -> Bool) -> Set [Id] -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> Set [Id]
getCompoundLists Env
e ->
           Id -> Type
toType ([Token] -> [Id] -> Range -> Id
Id [Token
t] [Id]
cs Range
ps) Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Env -> [Type] -> [Type]
mkCompoundTypeIds Env
e [Type]
r
          _ -> Type
a Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Type
b Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Env -> [Type] -> [Type]
mkCompoundTypeIds Env
e [Type]
r
    a :: Type
a : r :: [Type]
r -> Type
a Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Env -> [Type] -> [Type]
mkCompoundTypeIds Env
e [Type]
r
    [] -> []

isPlaceType :: Type -> Bool
isPlaceType :: Type -> Bool
isPlaceType ty :: Type
ty = case Type
ty of
    TypeToken t :: Token
t -> Token -> Bool
isPlace Token
t
    _ -> Bool
False