{-# LANGUAGE CPP #-}
module Transformations.CaseCompletion (completeCase) where
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative ((<$>), (<*>))
#endif
import qualified Control.Monad.State as S (State, evalState, gets, modify)
import Data.List (find)
import Data.Maybe (fromMaybe, listToMaybe)
import Curry.Base.Ident
import qualified Curry.Syntax as CS
import Base.CurryTypes (toType)
import Base.Expr
import Base.Messages (internalError)
import Base.Types ( boolType, charType, floatType
, intType, listType
)
import Base.Subst
import Env.Interface (InterfaceEnv, lookupInterface)
import Transformations.CurryToIL (transType)
import Transformations.Dictionary (qImplMethodId)
import IL
completeCase :: InterfaceEnv -> Module -> Module
completeCase :: InterfaceEnv -> Module -> Module
completeCase iEnv :: InterfaceEnv
iEnv mdl :: Module
mdl@(Module mid :: ModuleIdent
mid is :: [ModuleIdent]
is ds :: [Decl]
ds) = ModuleIdent -> [ModuleIdent] -> [Decl] -> Module
Module ModuleIdent
mid [ModuleIdent]
is [Decl]
ds'
where ds' :: [Decl]
ds'= State CCState [Decl] -> CCState -> [Decl]
forall s a. State s a -> s -> a
S.evalState ((Decl -> StateT CCState Identity Decl)
-> [Decl] -> State CCState [Decl]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Decl -> StateT CCState Identity Decl
ccDecl [Decl]
ds) (Module -> InterfaceEnv -> Int -> CCState
CCState Module
mdl InterfaceEnv
iEnv 0)
data CCState = CCState
{ CCState -> Module
modul :: Module
, CCState -> InterfaceEnv
interfaceEnv :: InterfaceEnv
, CCState -> Int
nextId :: Int
}
type CCM a = S.State CCState a
getModule :: CCM Module
getModule :: CCM Module
getModule = (CCState -> Module) -> CCM Module
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets CCState -> Module
modul
getInterfaceEnv :: CCM InterfaceEnv
getInterfaceEnv :: CCM InterfaceEnv
getInterfaceEnv = (CCState -> InterfaceEnv) -> CCM InterfaceEnv
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets CCState -> InterfaceEnv
interfaceEnv
freshIdent :: CCM Ident
freshIdent :: CCM Ident
freshIdent = do
Int
nid <- (CCState -> Int) -> StateT CCState Identity Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets CCState -> Int
nextId
(CCState -> CCState) -> StateT CCState Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
S.modify ((CCState -> CCState) -> StateT CCState Identity ())
-> (CCState -> CCState) -> StateT CCState Identity ()
forall a b. (a -> b) -> a -> b
$ \s :: CCState
s -> CCState
s { nextId :: Int
nextId = Int -> Int
forall a. Enum a => a -> a
succ Int
nid }
Ident -> CCM Ident
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> CCM Ident) -> Ident -> CCM Ident
forall a b. (a -> b) -> a -> b
$ String -> Ident
mkIdent (String -> Ident) -> String -> Ident
forall a b. (a -> b) -> a -> b
$ "_#comp" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
nid
ccDecl :: Decl -> CCM Decl
ccDecl :: Decl -> StateT CCState Identity Decl
ccDecl dd :: Decl
dd@(DataDecl _ _ _) = Decl -> StateT CCState Identity Decl
forall (m :: * -> *) a. Monad m => a -> m a
return Decl
dd
ccDecl edd :: Decl
edd@(ExternalDataDecl _ _) = Decl -> StateT CCState Identity Decl
forall (m :: * -> *) a. Monad m => a -> m a
return Decl
edd
ccDecl (FunctionDecl qid :: QualIdent
qid vs :: [(Type, Ident)]
vs ty :: Type
ty e :: Expression
e) = QualIdent -> [(Type, Ident)] -> Type -> Expression -> Decl
FunctionDecl QualIdent
qid [(Type, Ident)]
vs Type
ty (Expression -> Decl)
-> StateT CCState Identity Expression
-> StateT CCState Identity Decl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> StateT CCState Identity Expression
ccExpr Expression
e
ccDecl ed :: Decl
ed@(ExternalDecl _ _) = Decl -> StateT CCState Identity Decl
forall (m :: * -> *) a. Monad m => a -> m a
return Decl
ed
ccExpr :: Expression -> CCM Expression
ccExpr :: Expression -> StateT CCState Identity Expression
ccExpr l :: Expression
l@(Literal _ _) = Expression -> StateT CCState Identity Expression
forall (m :: * -> *) a. Monad m => a -> m a
return Expression
l
ccExpr v :: Expression
v@(Variable _ _) = Expression -> StateT CCState Identity Expression
forall (m :: * -> *) a. Monad m => a -> m a
return Expression
v
ccExpr f :: Expression
f@(Function _ _ _) = Expression -> StateT CCState Identity Expression
forall (m :: * -> *) a. Monad m => a -> m a
return Expression
f
ccExpr c :: Expression
c@(Constructor _ _ _) = Expression -> StateT CCState Identity Expression
forall (m :: * -> *) a. Monad m => a -> m a
return Expression
c
ccExpr (Apply e1 :: Expression
e1 e2 :: Expression
e2) = Expression -> Expression -> Expression
Apply (Expression -> Expression -> Expression)
-> StateT CCState Identity Expression
-> StateT CCState Identity (Expression -> Expression)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> StateT CCState Identity Expression
ccExpr Expression
e1 StateT CCState Identity (Expression -> Expression)
-> StateT CCState Identity Expression
-> StateT CCState Identity Expression
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> StateT CCState Identity Expression
ccExpr Expression
e2
ccExpr (Case ea :: Eval
ea e :: Expression
e bs :: [Alt]
bs) = do
Expression
e' <- Expression -> StateT CCState Identity Expression
ccExpr Expression
e
[Alt]
bs' <- (Alt -> StateT CCState Identity Alt)
-> [Alt] -> StateT CCState Identity [Alt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Alt -> StateT CCState Identity Alt
ccAlt [Alt]
bs
Eval -> Expression -> [Alt] -> StateT CCState Identity Expression
ccCase Eval
ea Expression
e' [Alt]
bs'
ccExpr (Or e1 :: Expression
e1 e2 :: Expression
e2) = Expression -> Expression -> Expression
Or (Expression -> Expression -> Expression)
-> StateT CCState Identity Expression
-> StateT CCState Identity (Expression -> Expression)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> StateT CCState Identity Expression
ccExpr Expression
e1 StateT CCState Identity (Expression -> Expression)
-> StateT CCState Identity Expression
-> StateT CCState Identity Expression
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> StateT CCState Identity Expression
ccExpr Expression
e2
ccExpr (Exist v :: Ident
v ty :: Type
ty e :: Expression
e) = Ident -> Type -> Expression -> Expression
Exist Ident
v Type
ty (Expression -> Expression)
-> StateT CCState Identity Expression
-> StateT CCState Identity Expression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> StateT CCState Identity Expression
ccExpr Expression
e
ccExpr (Let b :: Binding
b e :: Expression
e) = Binding -> Expression -> Expression
Let (Binding -> Expression -> Expression)
-> StateT CCState Identity Binding
-> StateT CCState Identity (Expression -> Expression)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binding -> StateT CCState Identity Binding
ccBinding Binding
b StateT CCState Identity (Expression -> Expression)
-> StateT CCState Identity Expression
-> StateT CCState Identity Expression
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> StateT CCState Identity Expression
ccExpr Expression
e
ccExpr (Letrec bs :: [Binding]
bs e :: Expression
e) = [Binding] -> Expression -> Expression
Letrec ([Binding] -> Expression -> Expression)
-> StateT CCState Identity [Binding]
-> StateT CCState Identity (Expression -> Expression)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Binding -> StateT CCState Identity Binding)
-> [Binding] -> StateT CCState Identity [Binding]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Binding -> StateT CCState Identity Binding
ccBinding [Binding]
bs StateT CCState Identity (Expression -> Expression)
-> StateT CCState Identity Expression
-> StateT CCState Identity Expression
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> StateT CCState Identity Expression
ccExpr Expression
e
ccExpr (Typed e :: Expression
e ty :: Type
ty) = (Expression -> Type -> Expression)
-> Type -> Expression -> Expression
forall a b c. (a -> b -> c) -> b -> a -> c
flip Expression -> Type -> Expression
Typed Type
ty (Expression -> Expression)
-> StateT CCState Identity Expression
-> StateT CCState Identity Expression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> StateT CCState Identity Expression
ccExpr Expression
e
ccAlt :: Alt -> CCM Alt
ccAlt :: Alt -> StateT CCState Identity Alt
ccAlt (Alt p :: ConstrTerm
p e :: Expression
e) = ConstrTerm -> Expression -> Alt
Alt ConstrTerm
p (Expression -> Alt)
-> StateT CCState Identity Expression
-> StateT CCState Identity Alt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> StateT CCState Identity Expression
ccExpr Expression
e
ccBinding :: Binding -> CCM Binding
ccBinding :: Binding -> StateT CCState Identity Binding
ccBinding (Binding v :: Ident
v e :: Expression
e) = Ident -> Expression -> Binding
Binding Ident
v (Expression -> Binding)
-> StateT CCState Identity Expression
-> StateT CCState Identity Binding
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> StateT CCState Identity Expression
ccExpr Expression
e
ccCase :: Eval -> Expression -> [Alt] -> CCM Expression
ccCase :: Eval -> Expression -> [Alt] -> StateT CCState Identity Expression
ccCase Flex e :: Expression
e alts :: [Alt]
alts = Expression -> StateT CCState Identity Expression
forall (m :: * -> *) a. Monad m => a -> m a
return (Expression -> StateT CCState Identity Expression)
-> Expression -> StateT CCState Identity Expression
forall a b. (a -> b) -> a -> b
$ Eval -> Expression -> [Alt] -> Expression
Case Eval
Flex Expression
e [Alt]
alts
ccCase Rigid _ [] = String -> StateT CCState Identity Expression
forall a. String -> a
internalError (String -> StateT CCState Identity Expression)
-> String -> StateT CCState Identity Expression
forall a b. (a -> b) -> a -> b
$ "CaseCompletion.ccCase: "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ "empty alternative list"
ccCase Rigid e :: Expression
e as :: [Alt]
as@(Alt p :: ConstrTerm
p _:_) = case ConstrTerm
p of
ConstructorPattern _ _ _ -> Eval -> Expression -> [Alt] -> StateT CCState Identity Expression
completeConsAlts Eval
Rigid Expression
e [Alt]
as
LiteralPattern _ _ -> Eval -> Expression -> [Alt] -> StateT CCState Identity Expression
completeLitAlts Eval
Rigid Expression
e [Alt]
as
VariablePattern _ _ -> Expression -> [Alt] -> StateT CCState Identity Expression
completeVarAlts Expression
e [Alt]
as
completeConsAlts :: Eval -> Expression -> [Alt] -> CCM Expression
completeConsAlts :: Eval -> Expression -> [Alt] -> StateT CCState Identity Expression
completeConsAlts ea :: Eval
ea ce :: Expression
ce alts :: [Alt]
alts = do
Module
mdl <- CCM Module
getModule
InterfaceEnv
menv <- CCM InterfaceEnv
getInterfaceEnv
[ConstrTerm]
complPats <- ((QualIdent, [Type]) -> StateT CCState Identity ConstrTerm)
-> [(QualIdent, [Type])] -> StateT CCState Identity [ConstrTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (QualIdent, [Type]) -> StateT CCState Identity ConstrTerm
genPat ([(QualIdent, [Type])] -> StateT CCState Identity [ConstrTerm])
-> [(QualIdent, [Type])] -> StateT CCState Identity [ConstrTerm]
forall a b. (a -> b) -> a -> b
$ Module -> InterfaceEnv -> [QualIdent] -> [(QualIdent, [Type])]
getComplConstrs Module
mdl InterfaceEnv
menv
[ QualIdent
c | (Alt (ConstructorPattern _ c :: QualIdent
c _) _) <- [Alt]
consAlts ]
Ident
v <- CCM Ident
freshIdent
Ident
w <- CCM Ident
freshIdent
Expression -> StateT CCState Identity Expression
forall (m :: * -> *) a. Monad m => a -> m a
return (Expression -> StateT CCState Identity Expression)
-> Expression -> StateT CCState Identity Expression
forall a b. (a -> b) -> a -> b
$ case ([ConstrTerm]
complPats, Ident -> Maybe Expression
defaultAlt Ident
v) of
(_:_, Just e' :: Expression
e') -> Ident
-> Expression -> Ident -> Expression -> [ConstrTerm] -> Expression
bindDefVar Ident
v Expression
ce Ident
w Expression
e' [ConstrTerm]
complPats
_ -> Eval -> Expression -> [Alt] -> Expression
Case Eval
ea Expression
ce [Alt]
consAlts
where
consAlts :: [Alt]
consAlts = [ Alt
a | a :: Alt
a@(Alt (ConstructorPattern _ _ _) _) <- [Alt]
alts ]
dataTy :: Type
dataTy = let TypeConstructor qid :: QualIdent
qid tys :: [Type]
tys = Type
patTy
in QualIdent -> [Type] -> Type
TypeConstructor QualIdent
qid ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Int -> Type) -> [Int] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Type
TypeVariable [0 .. [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]
patTy :: Type
patTy = let Alt pat :: ConstrTerm
pat _ = [Alt] -> Alt
forall a. [a] -> a
head [Alt]
consAlts in ConstrTerm -> Type
forall a. Typeable a => a -> Type
typeOf ConstrTerm
pat
tySubst :: TypeSubst
tySubst = Type -> Type -> TypeSubst -> TypeSubst
matchType Type
dataTy Type
patTy TypeSubst
forall a b. Subst a b
idSubst
genPat :: (QualIdent, [Type]) -> StateT CCState Identity ConstrTerm
genPat (qid :: QualIdent
qid, tys :: [Type]
tys) = Type -> QualIdent -> [(Type, Ident)] -> ConstrTerm
ConstructorPattern Type
patTy QualIdent
qid ([(Type, Ident)] -> ConstrTerm)
-> StateT CCState Identity [(Type, Ident)]
-> StateT CCState Identity ConstrTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(Type -> StateT CCState Identity (Type, Ident))
-> [Type] -> StateT CCState Identity [(Type, Ident)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ty' :: Type
ty' -> CCM Ident
freshIdent CCM Ident
-> (Ident -> StateT CCState Identity (Type, Ident))
-> StateT CCState Identity (Type, Ident)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \v :: Ident
v -> (Type, Ident) -> StateT CCState Identity (Type, Ident)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty', Ident
v)) (TypeSubst -> [Type] -> [Type]
forall a. SubstType a => TypeSubst -> a -> a
subst TypeSubst
tySubst [Type]
tys)
defaultAlt :: Ident -> Maybe Expression
defaultAlt v :: Ident
v = [Expression] -> Maybe Expression
forall a. [a] -> Maybe a
listToMaybe [ Ident -> Expression -> Expression -> Expression
replaceVar Ident
x (Type -> Ident -> Expression
Variable Type
ty Ident
v) Expression
e
| Alt (VariablePattern ty :: Type
ty x :: Ident
x) e :: Expression
e <- [Alt]
alts ]
bindDefVar :: Ident
-> Expression -> Ident -> Expression -> [ConstrTerm] -> Expression
bindDefVar v :: Ident
v e :: Expression
e w :: Ident
w e' :: Expression
e' ps :: [ConstrTerm]
ps
| Ident
v Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Expression -> [Ident]
forall e. Expr e => e -> [Ident]
fv Expression
e' = Ident -> Expression -> Expression -> Expression
mkBinding Ident
v Expression
e (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Expression -> Ident -> Expression -> [ConstrTerm] -> Expression
mkCase (Type -> Ident -> Expression
Variable (Expression -> Type
forall a. Typeable a => a -> Type
typeOf Expression
e) Ident
v) Ident
w Expression
e' [ConstrTerm]
ps
| Bool
otherwise = Expression -> Ident -> Expression -> [ConstrTerm] -> Expression
mkCase Expression
e Ident
w Expression
e' [ConstrTerm]
ps
mkCase :: Expression -> Ident -> Expression -> [ConstrTerm] -> Expression
mkCase e :: Expression
e w :: Ident
w e' :: Expression
e' ps :: [ConstrTerm]
ps = case [ConstrTerm]
ps of
[p :: ConstrTerm
p] -> Eval -> Expression -> [Alt] -> Expression
Case Eval
ea Expression
e ([Alt]
consAlts [Alt] -> [Alt] -> [Alt]
forall a. [a] -> [a] -> [a]
++ [ConstrTerm -> Expression -> Alt
Alt ConstrTerm
p Expression
e'])
_ -> Ident -> Expression -> Expression -> Expression
mkBinding Ident
w Expression
e'
(Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Eval -> Expression -> [Alt] -> Expression
Case Eval
ea Expression
e ([Alt]
consAlts [Alt] -> [Alt] -> [Alt]
forall a. [a] -> [a] -> [a]
++ [ConstrTerm -> Expression -> Alt
Alt ConstrTerm
p (Type -> Ident -> Expression
Variable (Expression -> Type
forall a. Typeable a => a -> Type
typeOf Expression
e') Ident
w) | ConstrTerm
p <- [ConstrTerm]
ps])
completeLitAlts :: Eval -> Expression -> [Alt] -> CCM Expression
completeLitAlts :: Eval -> Expression -> [Alt] -> StateT CCState Identity Expression
completeLitAlts ea :: Eval
ea ce :: Expression
ce alts :: [Alt]
alts = do
Ident
x <- CCM Ident
freshIdent
Expression -> StateT CCState Identity Expression
forall (m :: * -> *) a. Monad m => a -> m a
return (Expression -> StateT CCState Identity Expression)
-> Expression -> StateT CCState Identity Expression
forall a b. (a -> b) -> a -> b
$ Ident -> Expression -> Expression -> Expression
mkBinding Ident
x Expression
ce (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Ident -> [Alt] -> Expression
nestedCases Ident
x [Alt]
alts
where
nestedCases :: Ident -> [Alt] -> Expression
nestedCases _ [] = Type -> Expression
failedExpr (Alt -> Type
forall a. Typeable a => a -> Type
typeOf (Alt -> Type) -> Alt -> Type
forall a b. (a -> b) -> a -> b
$ [Alt] -> Alt
forall a. [a] -> a
head [Alt]
alts)
nestedCases x :: Ident
x (Alt p :: ConstrTerm
p ae :: Expression
ae : as :: [Alt]
as) = case ConstrTerm
p of
LiteralPattern ty :: Type
ty l :: Literal
l -> Eval -> Expression -> [Alt] -> Expression
Case Eval
ea (Type -> Ident -> Expression
Variable Type
ty Ident
x Expression -> Expression -> Expression
`eqExpr` Type -> Literal -> Expression
Literal Type
ty Literal
l)
[ ConstrTerm -> Expression -> Alt
Alt ConstrTerm
truePatt Expression
ae
, ConstrTerm -> Expression -> Alt
Alt ConstrTerm
falsePatt (Ident -> [Alt] -> Expression
nestedCases Ident
x [Alt]
as)
]
VariablePattern ty :: Type
ty v :: Ident
v -> Ident -> Expression -> Expression -> Expression
replaceVar Ident
v (Type -> Ident -> Expression
Variable Type
ty Ident
x) Expression
ae
_ -> String -> Expression
forall a. String -> a
internalError "CaseCompletion.completeLitAlts: illegal alternative"
completeVarAlts :: Expression -> [Alt] -> CCM Expression
completeVarAlts :: Expression -> [Alt] -> StateT CCState Identity Expression
completeVarAlts _ [] = String -> StateT CCState Identity Expression
forall a. String -> a
internalError (String -> StateT CCState Identity Expression)
-> String -> StateT CCState Identity Expression
forall a b. (a -> b) -> a -> b
$
"CaseCompletion.completeVarAlts: empty alternative list"
completeVarAlts ce :: Expression
ce (Alt p :: ConstrTerm
p ae :: Expression
ae : _) = case ConstrTerm
p of
VariablePattern _ x :: Ident
x -> Expression -> StateT CCState Identity Expression
forall (m :: * -> *) a. Monad m => a -> m a
return (Expression -> StateT CCState Identity Expression)
-> Expression -> StateT CCState Identity Expression
forall a b. (a -> b) -> a -> b
$ Ident -> Expression -> Expression -> Expression
mkBinding Ident
x Expression
ce Expression
ae
_ -> String -> StateT CCState Identity Expression
forall a. String -> a
internalError (String -> StateT CCState Identity Expression)
-> String -> StateT CCState Identity Expression
forall a b. (a -> b) -> a -> b
$
"CaseCompletion.completeVarAlts: variable pattern expected"
mkBinding :: Ident -> Expression -> Expression -> Expression
mkBinding :: Ident -> Expression -> Expression -> Expression
mkBinding v :: Ident
v e :: Expression
e e' :: Expression
e' = case Expression
e of
Variable _ _ -> Ident -> Expression -> Expression -> Expression
replaceVar Ident
v Expression
e Expression
e'
_ -> Binding -> Expression -> Expression
Let (Ident -> Expression -> Binding
Binding Ident
v Expression
e) Expression
e'
replaceVar :: Ident -> Expression -> Expression -> Expression
replaceVar :: Ident -> Expression -> Expression -> Expression
replaceVar v :: Ident
v e :: Expression
e x :: Expression
x@(Variable _ w :: Ident
w)
| Ident
v Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
w = Expression
e
| Bool
otherwise = Expression
x
replaceVar v :: Ident
v e :: Expression
e (Apply e1 :: Expression
e1 e2 :: Expression
e2)
= Expression -> Expression -> Expression
Apply (Ident -> Expression -> Expression -> Expression
replaceVar Ident
v Expression
e Expression
e1) (Ident -> Expression -> Expression -> Expression
replaceVar Ident
v Expression
e Expression
e2)
replaceVar v :: Ident
v e :: Expression
e (Case ev :: Eval
ev e' :: Expression
e' bs :: [Alt]
bs)
= Eval -> Expression -> [Alt] -> Expression
Case Eval
ev (Ident -> Expression -> Expression -> Expression
replaceVar Ident
v Expression
e Expression
e') ((Alt -> Alt) -> [Alt] -> [Alt]
forall a b. (a -> b) -> [a] -> [b]
map (Ident -> Expression -> Alt -> Alt
replaceVarInAlt Ident
v Expression
e) [Alt]
bs)
replaceVar v :: Ident
v e :: Expression
e (Or e1 :: Expression
e1 e2 :: Expression
e2)
= Expression -> Expression -> Expression
Or (Ident -> Expression -> Expression -> Expression
replaceVar Ident
v Expression
e Expression
e1) (Ident -> Expression -> Expression -> Expression
replaceVar Ident
v Expression
e Expression
e2)
replaceVar v :: Ident
v e :: Expression
e (Exist w :: Ident
w ty :: Type
ty e' :: Expression
e')
| Ident
v Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
w = Ident -> Type -> Expression -> Expression
Exist Ident
w Type
ty Expression
e'
| Bool
otherwise = Ident -> Type -> Expression -> Expression
Exist Ident
w Type
ty (Ident -> Expression -> Expression -> Expression
replaceVar Ident
v Expression
e Expression
e')
replaceVar v :: Ident
v e :: Expression
e (Let b :: Binding
b e' :: Expression
e')
| Ident
v Ident -> Binding -> Bool
`occursInBinding` Binding
b = Binding -> Expression -> Expression
Let Binding
b Expression
e'
| Bool
otherwise = Binding -> Expression -> Expression
Let (Ident -> Expression -> Binding -> Binding
replaceVarInBinding Ident
v Expression
e Binding
b)
(Ident -> Expression -> Expression -> Expression
replaceVar Ident
v Expression
e Expression
e')
replaceVar v :: Ident
v e :: Expression
e (Letrec bs :: [Binding]
bs e' :: Expression
e')
| (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Ident -> Binding -> Bool
occursInBinding Ident
v) [Binding]
bs = [Binding] -> Expression -> Expression
Letrec [Binding]
bs Expression
e'
| Bool
otherwise = [Binding] -> Expression -> Expression
Letrec ((Binding -> Binding) -> [Binding] -> [Binding]
forall a b. (a -> b) -> [a] -> [b]
map (Ident -> Expression -> Binding -> Binding
replaceVarInBinding Ident
v Expression
e) [Binding]
bs)
(Ident -> Expression -> Expression -> Expression
replaceVar Ident
v Expression
e Expression
e')
replaceVar _ _ e' :: Expression
e' = Expression
e'
replaceVarInAlt :: Ident -> Expression -> Alt -> Alt
replaceVarInAlt :: Ident -> Expression -> Alt -> Alt
replaceVarInAlt v :: Ident
v e :: Expression
e (Alt p :: ConstrTerm
p e' :: Expression
e')
| Ident
v Ident -> ConstrTerm -> Bool
`occursInPattern` ConstrTerm
p = ConstrTerm -> Expression -> Alt
Alt ConstrTerm
p Expression
e'
| Bool
otherwise = ConstrTerm -> Expression -> Alt
Alt ConstrTerm
p (Ident -> Expression -> Expression -> Expression
replaceVar Ident
v Expression
e Expression
e')
replaceVarInBinding :: Ident -> Expression -> Binding -> Binding
replaceVarInBinding :: Ident -> Expression -> Binding -> Binding
replaceVarInBinding v :: Ident
v e :: Expression
e (Binding w :: Ident
w e' :: Expression
e')
| Ident
v Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
w = Ident -> Expression -> Binding
Binding Ident
w Expression
e'
| Bool
otherwise = Ident -> Expression -> Binding
Binding Ident
w (Ident -> Expression -> Expression -> Expression
replaceVar Ident
v Expression
e Expression
e')
occursInPattern :: Ident -> ConstrTerm -> Bool
occursInPattern :: Ident -> ConstrTerm -> Bool
occursInPattern v :: Ident
v (VariablePattern _ w :: Ident
w) = Ident
v Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
w
occursInPattern v :: Ident
v (ConstructorPattern _ _ vs :: [(Type, Ident)]
vs) = Ident
v Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Type, Ident) -> Ident) -> [(Type, Ident)] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Ident) -> Ident
forall a b. (a, b) -> b
snd [(Type, Ident)]
vs
occursInPattern _ _ = Bool
False
occursInBinding :: Ident -> Binding -> Bool
occursInBinding :: Ident -> Binding -> Bool
occursInBinding v :: Ident
v (Binding w :: Ident
w _) = Ident
v Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
w
failedExpr :: Type -> Expression
failedExpr :: Type -> Expression
failedExpr ty :: Type
ty = Type -> QualIdent -> Int -> Expression
Function Type
ty (ModuleIdent -> Ident -> QualIdent
qualifyWith ModuleIdent
preludeMIdent (String -> Ident
mkIdent "failed")) 0
eqExpr :: Expression -> Expression -> Expression
eqExpr :: Expression -> Expression -> Expression
eqExpr e1 :: Expression
e1 e2 :: Expression
e2 = Expression -> Expression -> Expression
Apply (Expression -> Expression -> Expression
Apply (Type -> QualIdent -> Int -> Expression
Function Type
eqTy QualIdent
eq 2) Expression
e1) Expression
e2
where eq :: QualIdent
eq = ModuleIdent -> QualIdent -> Type -> Ident -> QualIdent
qImplMethodId ModuleIdent
preludeMIdent QualIdent
qEqId Type
ty (Ident -> QualIdent) -> Ident -> QualIdent
forall a b. (a -> b) -> a -> b
$ String -> Ident
mkIdent "=="
ty :: Type
ty = case Expression
e2 of
Literal _ l :: Literal
l -> case Literal
l of
Char _ -> Type
charType
Int _ -> Type
intType
Float _ -> Type
floatType
_ -> String -> Type
forall a. String -> a
internalError "CaseCompletion.eqExpr: no literal"
ty' :: Type
ty' = Type -> Type
transType Type
ty
eqTy :: Type
eqTy = Type -> Type -> Type
TypeArrow Type
ty' (Type -> Type -> Type
TypeArrow Type
ty' Type
boolType')
truePatt :: ConstrTerm
truePatt :: ConstrTerm
truePatt = Type -> QualIdent -> [(Type, Ident)] -> ConstrTerm
ConstructorPattern Type
boolType' QualIdent
qTrueId []
falsePatt :: ConstrTerm
falsePatt :: ConstrTerm
falsePatt = Type -> QualIdent -> [(Type, Ident)] -> ConstrTerm
ConstructorPattern Type
boolType' QualIdent
qFalseId []
boolType' :: Type
boolType' :: Type
boolType' = Type -> Type
transType Type
boolType
getComplConstrs :: Module -> InterfaceEnv -> [QualIdent] -> [(QualIdent, [Type])]
getComplConstrs :: Module -> InterfaceEnv -> [QualIdent] -> [(QualIdent, [Type])]
getComplConstrs _ _ []
= String -> [(QualIdent, [Type])]
forall a. String -> a
internalError "CaseCompletion.getComplConstrs: empty constructor list"
getComplConstrs (Module mid :: ModuleIdent
mid _ ds :: [Decl]
ds) menv :: InterfaceEnv
menv cs :: [QualIdent]
cs@(c :: QualIdent
c:_)
| QualIdent
c QualIdent -> [QualIdent] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QualIdent
qNilId, QualIdent
qConsId] = [QualIdent] -> [(QualIdent, [Type])] -> [(QualIdent, [Type])]
complementary [QualIdent]
cs
[(QualIdent
qNilId, []), (QualIdent
qConsId, [Int -> Type
TypeVariable 0, Type -> Type
transType (Type -> Type
listType Type
boolType)])]
| ModuleIdent
mid' ModuleIdent -> ModuleIdent -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleIdent
mid = [QualIdent] -> [Decl] -> [(QualIdent, [Type])]
getCCFromDecls [QualIdent]
cs [Decl]
ds
| Bool
otherwise = [(QualIdent, [Type])]
-> (Interface -> [(QualIdent, [Type])])
-> Maybe Interface
-> [(QualIdent, [Type])]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (ModuleIdent -> [QualIdent] -> Interface -> [(QualIdent, [Type])]
getCCFromIDecls ModuleIdent
mid' [QualIdent]
cs)
(ModuleIdent -> InterfaceEnv -> Maybe Interface
lookupInterface ModuleIdent
mid' InterfaceEnv
menv)
where mid' :: ModuleIdent
mid' = ModuleIdent -> Maybe ModuleIdent -> ModuleIdent
forall a. a -> Maybe a -> a
fromMaybe ModuleIdent
mid (QualIdent -> Maybe ModuleIdent
qidModule QualIdent
c)
getCCFromDecls :: [QualIdent] -> [Decl] -> [(QualIdent, [Type])]
getCCFromDecls :: [QualIdent] -> [Decl] -> [(QualIdent, [Type])]
getCCFromDecls cs :: [QualIdent]
cs ds :: [Decl]
ds = [QualIdent] -> [(QualIdent, [Type])] -> [(QualIdent, [Type])]
complementary [QualIdent]
cs [(QualIdent, [Type])]
cinfos
where
cinfos :: [(QualIdent, [Type])]
cinfos = (ConstrDecl -> (QualIdent, [Type]))
-> [ConstrDecl] -> [(QualIdent, [Type])]
forall a b. (a -> b) -> [a] -> [b]
map ConstrDecl -> (QualIdent, [Type])
constrInfo
([ConstrDecl] -> [(QualIdent, [Type])])
-> [ConstrDecl] -> [(QualIdent, [Type])]
forall a b. (a -> b) -> a -> b
$ [ConstrDecl]
-> (Decl -> [ConstrDecl]) -> Maybe Decl -> [ConstrDecl]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Decl -> [ConstrDecl]
extractConstrDecls ((Decl -> Bool) -> [Decl] -> Maybe Decl
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Decl -> QualIdent -> Bool
`declares` [QualIdent] -> QualIdent
forall a. [a] -> a
head [QualIdent]
cs) [Decl]
ds)
decl :: Decl
decl declares :: Decl -> QualIdent -> Bool
`declares` qid :: QualIdent
qid = case Decl
decl of
DataDecl _ _ cs' :: [ConstrDecl]
cs' -> (ConstrDecl -> Bool) -> [ConstrDecl] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (ConstrDecl -> QualIdent -> Bool
`declaresConstr` QualIdent
qid) [ConstrDecl]
cs'
_ -> Bool
False
declaresConstr :: ConstrDecl -> QualIdent -> Bool
declaresConstr (ConstrDecl cid :: QualIdent
cid _) qid :: QualIdent
qid = QualIdent
cid QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
qid
extractConstrDecls :: Decl -> [ConstrDecl]
extractConstrDecls (DataDecl _ _ cs' :: [ConstrDecl]
cs') = [ConstrDecl]
cs'
extractConstrDecls _ = []
constrInfo :: ConstrDecl -> (QualIdent, [Type])
constrInfo (ConstrDecl cid :: QualIdent
cid tys :: [Type]
tys) = (QualIdent
cid, [Type]
tys)
getCCFromIDecls :: ModuleIdent -> [QualIdent] -> CS.Interface
-> [(QualIdent, [Type])]
getCCFromIDecls :: ModuleIdent -> [QualIdent] -> Interface -> [(QualIdent, [Type])]
getCCFromIDecls mid :: ModuleIdent
mid cs :: [QualIdent]
cs (CS.Interface _ _ ds :: [IDecl]
ds) = [QualIdent] -> [(QualIdent, [Type])] -> [(QualIdent, [Type])]
complementary [QualIdent]
cs [(QualIdent, [Type])]
cinfos
where
cinfos :: [(QualIdent, [Type])]
cinfos = (([Ident], ConstrDecl) -> (QualIdent, [Type]))
-> [([Ident], ConstrDecl)] -> [(QualIdent, [Type])]
forall a b. (a -> b) -> [a] -> [b]
map (([Ident] -> ConstrDecl -> (QualIdent, [Type]))
-> ([Ident], ConstrDecl) -> (QualIdent, [Type])
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Ident] -> ConstrDecl -> (QualIdent, [Type])
constrInfo)
([([Ident], ConstrDecl)] -> [(QualIdent, [Type])])
-> [([Ident], ConstrDecl)] -> [(QualIdent, [Type])]
forall a b. (a -> b) -> a -> b
$ [([Ident], ConstrDecl)]
-> (IDecl -> [([Ident], ConstrDecl)])
-> Maybe IDecl
-> [([Ident], ConstrDecl)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] IDecl -> [([Ident], ConstrDecl)]
extractConstrDecls ((IDecl -> Bool) -> [IDecl] -> Maybe IDecl
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (IDecl -> QualIdent -> Bool
`declares` [QualIdent] -> QualIdent
forall a. [a] -> a
head [QualIdent]
cs) [IDecl]
ds)
decl :: IDecl
decl declares :: IDecl -> QualIdent -> Bool
`declares` qid :: QualIdent
qid = case IDecl
decl of
CS.IDataDecl _ _ _ _ cs' :: [ConstrDecl]
cs' _ -> (ConstrDecl -> Bool) -> [ConstrDecl] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (ConstrDecl -> QualIdent -> Bool
`declaresConstr` QualIdent
qid) [ConstrDecl]
cs'
CS.INewtypeDecl _ _ _ _ nc :: NewConstrDecl
nc _ -> QualIdent -> NewConstrDecl -> Bool
isNewConstrDecl QualIdent
qid NewConstrDecl
nc
_ -> Bool
False
declaresConstr :: ConstrDecl -> QualIdent -> Bool
declaresConstr (CS.ConstrDecl _ cid :: Ident
cid _) qid :: QualIdent
qid = QualIdent -> Ident
unqualify QualIdent
qid Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cid
declaresConstr (CS.ConOpDecl _ _ oid :: Ident
oid _) qid :: QualIdent
qid = QualIdent -> Ident
unqualify QualIdent
qid Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
oid
declaresConstr (CS.RecordDecl _ cid :: Ident
cid _) qid :: QualIdent
qid = QualIdent -> Ident
unqualify QualIdent
qid Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cid
isNewConstrDecl :: QualIdent -> NewConstrDecl -> Bool
isNewConstrDecl qid :: QualIdent
qid (CS.NewConstrDecl _ cid :: Ident
cid _) = QualIdent -> Ident
unqualify QualIdent
qid Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cid
isNewConstrDecl qid :: QualIdent
qid (CS.NewRecordDecl _ cid :: Ident
cid _) = QualIdent -> Ident
unqualify QualIdent
qid Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cid
extractConstrDecls :: IDecl -> [([Ident], ConstrDecl)]
extractConstrDecls (CS.IDataDecl _ _ _ vs :: [Ident]
vs cs' :: [ConstrDecl]
cs' _) = [[Ident]] -> [ConstrDecl] -> [([Ident], ConstrDecl)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Ident] -> [[Ident]]
forall a. a -> [a]
repeat [Ident]
vs) [ConstrDecl]
cs'
extractConstrDecls _ = []
constrInfo :: [Ident] -> ConstrDecl -> (QualIdent, [Type])
constrInfo vs :: [Ident]
vs (CS.ConstrDecl _ cid :: Ident
cid tys :: [TypeExpr]
tys) =
(ModuleIdent -> Ident -> QualIdent
qualifyWith ModuleIdent
mid Ident
cid, (TypeExpr -> Type) -> [TypeExpr] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ([Ident] -> TypeExpr -> Type
transType' [Ident]
vs) [TypeExpr]
tys)
constrInfo vs :: [Ident]
vs (CS.ConOpDecl _ ty1 :: TypeExpr
ty1 oid :: Ident
oid ty2 :: TypeExpr
ty2) =
(ModuleIdent -> Ident -> QualIdent
qualifyWith ModuleIdent
mid Ident
oid, (TypeExpr -> Type) -> [TypeExpr] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ([Ident] -> TypeExpr -> Type
transType' [Ident]
vs) [TypeExpr
ty1, TypeExpr
ty2])
constrInfo vs :: [Ident]
vs (CS.RecordDecl _ cid :: Ident
cid fs :: [FieldDecl]
fs) =
( ModuleIdent -> Ident -> QualIdent
qualifyWith ModuleIdent
mid Ident
cid
, [[Ident] -> TypeExpr -> Type
transType' [Ident]
vs TypeExpr
ty | CS.FieldDecl _ ls :: [Ident]
ls ty :: TypeExpr
ty <- [FieldDecl]
fs, Ident
_ <- [Ident]
ls]
)
transType' :: [Ident] -> TypeExpr -> Type
transType' vs :: [Ident]
vs = Type -> Type
transType (Type -> Type) -> (TypeExpr -> Type) -> TypeExpr -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Ident] -> TypeExpr -> Type
toType [Ident]
vs
complementary :: [QualIdent] -> [(QualIdent, [Type])] -> [(QualIdent, [Type])]
complementary :: [QualIdent] -> [(QualIdent, [Type])] -> [(QualIdent, [Type])]
complementary known :: [QualIdent]
known others :: [(QualIdent, [Type])]
others = ((QualIdent, [Type]) -> Bool)
-> [(QualIdent, [Type])] -> [(QualIdent, [Type])]
forall a. (a -> Bool) -> [a] -> [a]
filter ((QualIdent -> [QualIdent] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [QualIdent]
known) (QualIdent -> Bool)
-> ((QualIdent, [Type]) -> QualIdent)
-> (QualIdent, [Type])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QualIdent, [Type]) -> QualIdent
forall a b. (a, b) -> a
fst) [(QualIdent, [Type])]
others
type TypeSubst = Subst Int Type
class SubstType a where
subst :: TypeSubst -> a -> a
instance SubstType a => SubstType [a] where
subst :: TypeSubst -> [a] -> [a]
subst sigma :: TypeSubst
sigma = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (TypeSubst -> a -> a
forall a. SubstType a => TypeSubst -> a -> a
subst TypeSubst
sigma)
instance SubstType Type where
subst :: TypeSubst -> Type -> Type
subst sigma :: TypeSubst
sigma (TypeConstructor q :: QualIdent
q tys :: [Type]
tys) = QualIdent -> [Type] -> Type
TypeConstructor QualIdent
q ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ TypeSubst -> [Type] -> [Type]
forall a. SubstType a => TypeSubst -> a -> a
subst TypeSubst
sigma [Type]
tys
subst sigma :: TypeSubst
sigma (TypeVariable tv :: Int
tv) = (Int -> Type)
-> (TypeSubst -> Type -> Type) -> TypeSubst -> Int -> Type
forall v e.
Ord v =>
(v -> e) -> (Subst v e -> e -> e) -> Subst v e -> v -> e
substVar' Int -> Type
TypeVariable TypeSubst -> Type -> Type
forall a. SubstType a => TypeSubst -> a -> a
subst TypeSubst
sigma Int
tv
subst sigma :: TypeSubst
sigma (TypeArrow ty1 :: Type
ty1 ty2 :: Type
ty2) = Type -> Type -> Type
TypeArrow (TypeSubst -> Type -> Type
forall a. SubstType a => TypeSubst -> a -> a
subst TypeSubst
sigma Type
ty1) (TypeSubst -> Type -> Type
forall a. SubstType a => TypeSubst -> a -> a
subst TypeSubst
sigma Type
ty2)
subst _ (TypeForall _ _) =
String -> Type
forall a. String -> a
internalError "Transformations.CaseCompletion.SubstType.Type.subst"
matchType :: Type -> Type -> TypeSubst -> TypeSubst
matchType :: Type -> Type -> TypeSubst -> TypeSubst
matchType ty1 :: Type
ty1 ty2 :: Type
ty2 = (TypeSubst -> TypeSubst)
-> Maybe (TypeSubst -> TypeSubst) -> TypeSubst -> TypeSubst
forall a. a -> Maybe a -> a
fromMaybe TypeSubst -> TypeSubst
forall a. a
noMatch (Type -> Type -> Maybe (TypeSubst -> TypeSubst)
matchType' Type
ty1 Type
ty2)
where
noMatch :: a
noMatch = String -> a
forall a. String -> a
internalError (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "Transformations.CaseCompletion.matchType: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
Int -> Type -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec 11 Type
ty1 " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Type -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec 11 Type
ty2 ""
matchType' :: Type -> Type -> Maybe (TypeSubst -> TypeSubst)
matchType' :: Type -> Type -> Maybe (TypeSubst -> TypeSubst)
matchType' (TypeVariable tv :: Int
tv) ty :: Type
ty
| Type
ty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Type
TypeVariable Int
tv = (TypeSubst -> TypeSubst) -> Maybe (TypeSubst -> TypeSubst)
forall a. a -> Maybe a
Just TypeSubst -> TypeSubst
forall a. a -> a
id
| Bool
otherwise = (TypeSubst -> TypeSubst) -> Maybe (TypeSubst -> TypeSubst)
forall a. a -> Maybe a
Just (Int -> Type -> TypeSubst -> TypeSubst
forall v e. Ord v => v -> e -> Subst v e -> Subst v e
bindSubst Int
tv Type
ty)
matchType' (TypeConstructor tc1 :: QualIdent
tc1 tys1 :: [Type]
tys1) (TypeConstructor tc2 :: QualIdent
tc2 tys2 :: [Type]
tys2)
| QualIdent
tc1 QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
tc2 = (TypeSubst -> TypeSubst) -> Maybe (TypeSubst -> TypeSubst)
forall a. a -> Maybe a
Just ((TypeSubst -> TypeSubst) -> Maybe (TypeSubst -> TypeSubst))
-> (TypeSubst -> TypeSubst) -> Maybe (TypeSubst -> TypeSubst)
forall a b. (a -> b) -> a -> b
$ ((Type, Type)
-> (TypeSubst -> TypeSubst) -> TypeSubst -> TypeSubst)
-> (TypeSubst -> TypeSubst)
-> [(Type, Type)]
-> TypeSubst
-> TypeSubst
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(ty1 :: Type
ty1, ty2 :: Type
ty2) -> (Type -> Type -> TypeSubst -> TypeSubst
matchType Type
ty1 Type
ty2 (TypeSubst -> TypeSubst)
-> (TypeSubst -> TypeSubst) -> TypeSubst -> TypeSubst
forall b c a. (b -> c) -> (a -> b) -> a -> c
.)) TypeSubst -> TypeSubst
forall a. a -> a
id ([(Type, Type)] -> TypeSubst -> TypeSubst)
-> [(Type, Type)] -> TypeSubst -> TypeSubst
forall a b. (a -> b) -> a -> b
$ [(Type, Type)]
tys
where tys :: [(Type, Type)]
tys = [Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
tys1 [Type]
tys2
matchType' (TypeArrow ty11 :: Type
ty11 ty12 :: Type
ty12) (TypeArrow ty21 :: Type
ty21 ty22 :: Type
ty22) =
(TypeSubst -> TypeSubst) -> Maybe (TypeSubst -> TypeSubst)
forall a. a -> Maybe a
Just (Type -> Type -> TypeSubst -> TypeSubst
matchType Type
ty11 Type
ty21 (TypeSubst -> TypeSubst)
-> (TypeSubst -> TypeSubst) -> TypeSubst -> TypeSubst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type -> TypeSubst -> TypeSubst
matchType Type
ty12 Type
ty22)
matchType' _ _ = Maybe (TypeSubst -> TypeSubst)
forall a. Maybe a
Nothing