{- |
    Module      :  $Header$
    Description :  Type computation of Curry expressions
    Copyright   :  (c) 2003 - 2006 Wolfgang Lux
                       2014 - 2015 Jan Tikovsky
                       2016        Finn Teegen
    License     :  BSD-3-clause

    Maintainer  :  bjp@informatik.uni-kiel.de
    Stability   :  experimental
    Portability :  portable

    After the compiler has attributed patterns and expressions with type
    information during type inference, it is straightforward to recompute
    the type of every pattern and expression. Since all annotated types
    are monomorphic, there is no need to instantiate any variables or
    perform any (non-trivial) unifications.
-}

module Base.Typing
  ( Typeable (..)
  , withType, matchType
  , bindDecls, bindDecl, bindPatterns, bindPattern, declVars, patternVars
  ) where

import Data.List (nub)
import Data.Maybe (fromMaybe)

import Curry.Base.Ident
import Curry.Syntax

import Base.Messages (internalError)
import Base.Types
import Base.TypeSubst
import Base.Utils (fst3)

import Env.Value

class Typeable a where
  typeOf :: a -> Type

instance Typeable Type where
  typeOf :: Type -> Type
typeOf = Type -> Type
forall a. a -> a
id

instance Typeable PredType where
  typeOf :: PredType -> Type
typeOf = PredType -> Type
unpredType

instance Typeable a => Typeable (Rhs a) where
  typeOf :: Rhs a -> Type
typeOf (SimpleRhs  _ e :: Expression a
e _ ) = Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e
  typeOf (GuardedRhs _ es :: [CondExpr a]
es _) = [Type] -> Type
forall a. [a] -> a
head [Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e | CondExpr _ _ e :: Expression a
e <- [CondExpr a]
es]

instance Typeable a => Typeable (Pattern a) where
  typeOf :: Pattern a -> Type
typeOf (LiteralPattern _ a :: a
a _) = a -> Type
forall a. Typeable a => a -> Type
typeOf a
a
  typeOf (NegativePattern _ a :: a
a _) = a -> Type
forall a. Typeable a => a -> Type
typeOf a
a
  typeOf (VariablePattern _ a :: a
a _) = a -> Type
forall a. Typeable a => a -> Type
typeOf a
a
  typeOf (ConstructorPattern _ a :: a
a _ _) = a -> Type
forall a. Typeable a => a -> Type
typeOf a
a
  typeOf (InfixPattern _ a :: a
a _ _ _) = a -> Type
forall a. Typeable a => a -> Type
typeOf a
a
  typeOf (ParenPattern _ t :: Pattern a
t) = Pattern a -> Type
forall a. Typeable a => a -> Type
typeOf Pattern a
t
  typeOf (RecordPattern _ a :: a
a _ _) = a -> Type
forall a. Typeable a => a -> Type
typeOf a
a
  typeOf (TuplePattern _ ts :: [Pattern a]
ts) = [Type] -> Type
tupleType ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Pattern a -> Type) -> [Pattern a] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Pattern a -> Type
forall a. Typeable a => a -> Type
typeOf [Pattern a]
ts
  typeOf (ListPattern _ a :: a
a _) = a -> Type
forall a. Typeable a => a -> Type
typeOf a
a
  typeOf (AsPattern _ _ t :: Pattern a
t) = Pattern a -> Type
forall a. Typeable a => a -> Type
typeOf Pattern a
t
  typeOf (LazyPattern _ t :: Pattern a
t) = Pattern a -> Type
forall a. Typeable a => a -> Type
typeOf Pattern a
t
  typeOf (FunctionPattern _ a :: a
a _ _) = a -> Type
forall a. Typeable a => a -> Type
typeOf a
a
  typeOf (InfixFuncPattern _ a :: a
a _ _ _) = a -> Type
forall a. Typeable a => a -> Type
typeOf a
a

instance Typeable a => Typeable (Expression a) where
  typeOf :: Expression a -> Type
typeOf (Literal _ a :: a
a _) = a -> Type
forall a. Typeable a => a -> Type
typeOf a
a
  typeOf (Variable _ a :: a
a _) = a -> Type
forall a. Typeable a => a -> Type
typeOf a
a
  typeOf (Constructor _ a :: a
a _) = a -> Type
forall a. Typeable a => a -> Type
typeOf a
a
  typeOf (Paren _ e :: Expression a
e) = Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e
  typeOf (Typed _ e :: Expression a
e _) = Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e
  typeOf (Record _ a :: a
a _ _) = a -> Type
forall a. Typeable a => a -> Type
typeOf a
a
  typeOf (RecordUpdate _ e :: Expression a
e _) = Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e
  typeOf (Tuple _ es :: [Expression a]
es) = [Type] -> Type
tupleType ((Expression a -> Type) -> [Expression a] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Expression a -> Type
forall a. Typeable a => a -> Type
typeOf [Expression a]
es)
  typeOf (List _ a :: a
a _) = a -> Type
forall a. Typeable a => a -> Type
typeOf a
a
  typeOf (ListCompr _ e :: Expression a
e _) = Type -> Type
listType (Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e)
  typeOf (EnumFrom _ e :: Expression a
e) = Type -> Type
listType (Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e)
  typeOf (EnumFromThen _ e :: Expression a
e _) = Type -> Type
listType (Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e)
  typeOf (EnumFromTo _ e :: Expression a
e _) = Type -> Type
listType (Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e)
  typeOf (EnumFromThenTo _ e :: Expression a
e _ _) = Type -> Type
listType (Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e)
  typeOf (UnaryMinus _ e :: Expression a
e) = Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e
  typeOf (Apply _ e :: Expression a
e _) = case Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e of
    TypeArrow _ ty :: Type
ty -> Type
ty
    _ -> String -> Type
forall a. String -> a
internalError "Base.Typing.typeOf: application"
  typeOf (InfixApply _ _ op :: InfixOp a
op _) = case Expression a -> Type
forall a. Typeable a => a -> Type
typeOf (InfixOp a -> Expression a
forall a. InfixOp a -> Expression a
infixOp InfixOp a
op) of
    TypeArrow _ (TypeArrow _ ty :: Type
ty) -> Type
ty
    _ -> String -> Type
forall a. String -> a
internalError "Base.Typing.typeOf: infix application"
  typeOf (LeftSection _ _ op :: InfixOp a
op) = case Expression a -> Type
forall a. Typeable a => a -> Type
typeOf (InfixOp a -> Expression a
forall a. InfixOp a -> Expression a
infixOp InfixOp a
op) of
    TypeArrow _ ty :: Type
ty -> Type
ty
    _ -> String -> Type
forall a. String -> a
internalError "Base.Typing.typeOf: left section"
  typeOf (RightSection _ op :: InfixOp a
op _) = case Expression a -> Type
forall a. Typeable a => a -> Type
typeOf (InfixOp a -> Expression a
forall a. InfixOp a -> Expression a
infixOp InfixOp a
op) of
    TypeArrow ty1 :: Type
ty1 (TypeArrow _ ty2 :: Type
ty2) -> Type -> Type -> Type
TypeArrow Type
ty1 Type
ty2
    _ -> String -> Type
forall a. String -> a
internalError "Base.Typing.typeOf: right section"
  typeOf (Lambda _ ts :: [Pattern a]
ts e :: Expression a
e) = (Pattern a -> Type -> Type) -> Type -> [Pattern a] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> Type -> Type
TypeArrow (Type -> Type -> Type)
-> (Pattern a -> Type) -> Pattern a -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern a -> Type
forall a. Typeable a => a -> Type
typeOf) (Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e) [Pattern a]
ts
  typeOf (Let _ _ e :: Expression a
e) = Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e
  typeOf (Do _ _ e :: Expression a
e) = Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e
  typeOf (IfThenElse _ _ e :: Expression a
e _) = Expression a -> Type
forall a. Typeable a => a -> Type
typeOf Expression a
e
  typeOf (Case _ _ _ as :: [Alt a]
as) = Alt a -> Type
forall a. Typeable a => a -> Type
typeOf (Alt a -> Type) -> Alt a -> Type
forall a b. (a -> b) -> a -> b
$ [Alt a] -> Alt a
forall a. [a] -> a
head [Alt a]
as

instance Typeable a => Typeable (Alt a) where
  typeOf :: Alt a -> Type
typeOf (Alt _ _ rhs :: Rhs a
rhs) = Rhs a -> Type
forall a. Typeable a => a -> Type
typeOf Rhs a
rhs

-- When inlining variable and function definitions, the compiler must
-- eventually update the type annotations of the inlined expression. To
-- that end, the variable or function's annotated type and the type of
-- the inlined expression must be unified. Since the program is type
-- correct, this unification is just a simple one way matching where we
-- only need to match the type variables in the inlined expression's type
-- with the corresponding types in the variable or function's annotated
-- type.

withType :: (Functor f, Typeable (f Type)) => Type -> f Type -> f Type
withType :: Type -> f Type -> f Type
withType ty :: Type
ty e :: f Type
e = (Type -> Type) -> f Type -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TypeSubst -> Type -> Type
forall a. SubstType a => TypeSubst -> a -> a
subst (Type -> Type -> TypeSubst -> TypeSubst
matchType (f Type -> Type
forall a. Typeable a => a -> Type
typeOf f Type
e) Type
ty TypeSubst
forall a b. Subst a b
idSubst)) f Type
e

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
$ "Base.Typing.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) (TypeConstructor tc2 :: QualIdent
tc2)
  | 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
forall a. a -> a
id
matchType' (TypeConstrained _ tv1 :: Int
tv1) (TypeConstrained _ tv2 :: Int
tv2)
  | Int
tv1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
tv2 = (TypeSubst -> TypeSubst) -> Maybe (TypeSubst -> TypeSubst)
forall a. a -> Maybe a
Just TypeSubst -> TypeSubst
forall a. a -> a
id
matchType' (TypeApply ty11 :: Type
ty11 ty12 :: Type
ty12) (TypeApply ty21 :: Type
ty21 ty22 :: Type
ty22) =
  ((TypeSubst -> TypeSubst) -> TypeSubst -> TypeSubst)
-> Maybe (TypeSubst -> TypeSubst) -> Maybe (TypeSubst -> TypeSubst)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((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) (Type -> Type -> Maybe (TypeSubst -> TypeSubst)
matchType' Type
ty11 Type
ty21)
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' (TypeApply ty11 :: Type
ty11 ty12 :: Type
ty12) (TypeArrow ty21 :: Type
ty21 ty22 :: Type
ty22) =
  ((TypeSubst -> TypeSubst) -> TypeSubst -> TypeSubst)
-> Maybe (TypeSubst -> TypeSubst) -> Maybe (TypeSubst -> TypeSubst)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((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)
       (Type -> Type -> Maybe (TypeSubst -> TypeSubst)
matchType' Type
ty11 (Type -> Type -> Type
TypeApply (QualIdent -> Type
TypeConstructor QualIdent
qArrowId) Type
ty21))
matchType' (TypeArrow ty11 :: Type
ty11 ty12 :: Type
ty12) (TypeApply ty21 :: Type
ty21 ty22 :: Type
ty22) =
  ((TypeSubst -> TypeSubst) -> TypeSubst -> TypeSubst)
-> Maybe (TypeSubst -> TypeSubst) -> Maybe (TypeSubst -> TypeSubst)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((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)
       (Type -> Type -> Maybe (TypeSubst -> TypeSubst)
matchType' (Type -> Type -> Type
TypeApply (QualIdent -> Type
TypeConstructor QualIdent
qArrowId) Type
ty11) Type
ty21)
matchType' (TypeForall _ ty1 :: Type
ty1) (TypeForall _ ty2 :: Type
ty2) = Type -> Type -> Maybe (TypeSubst -> TypeSubst)
matchType' Type
ty1 Type
ty2
matchType' (TypeForall _ ty1 :: Type
ty1) ty2 :: Type
ty2 = Type -> Type -> Maybe (TypeSubst -> TypeSubst)
matchType' Type
ty1 Type
ty2
matchType' ty1 :: Type
ty1 (TypeForall _ ty2 :: Type
ty2) = Type -> Type -> Maybe (TypeSubst -> TypeSubst)
matchType' Type
ty1 Type
ty2
matchType' _ _ = Maybe (TypeSubst -> TypeSubst)
forall a. Maybe a
Nothing

-- The functions 'bindDecls', 'bindDecl', 'bindPatterns' and 'bindPattern'
-- augment the value environment with the types of the entities defined in
-- local declaration groups and patterns, respectively, using the types from
-- their type annotations.

bindDecls :: (Eq t, Typeable t, ValueType t) => [Decl t] -> ValueEnv -> ValueEnv
bindDecls :: [Decl t] -> ValueEnv -> ValueEnv
bindDecls = (ValueEnv -> [Decl t] -> ValueEnv)
-> [Decl t] -> ValueEnv -> ValueEnv
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((ValueEnv -> [Decl t] -> ValueEnv)
 -> [Decl t] -> ValueEnv -> ValueEnv)
-> (ValueEnv -> [Decl t] -> ValueEnv)
-> [Decl t]
-> ValueEnv
-> ValueEnv
forall a b. (a -> b) -> a -> b
$ (Decl t -> ValueEnv -> ValueEnv)
-> ValueEnv -> [Decl t] -> ValueEnv
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Decl t -> ValueEnv -> ValueEnv
forall t.
(Eq t, Typeable t, ValueType t) =>
Decl t -> ValueEnv -> ValueEnv
bindDecl

bindDecl :: (Eq t, Typeable t, ValueType t) => Decl t -> ValueEnv -> ValueEnv
bindDecl :: Decl t -> ValueEnv -> ValueEnv
bindDecl d :: Decl t
d vEnv :: ValueEnv
vEnv = [(Ident, Int, t)] -> ValueEnv -> ValueEnv
forall t. ValueType t => [(Ident, Int, t)] -> ValueEnv -> ValueEnv
bindLocalVars (((Ident, Int, t) -> Bool) -> [(Ident, Int, t)] -> [(Ident, Int, t)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Ident, Int, t) -> Bool
forall b c. (Ident, b, c) -> Bool
unbound ([(Ident, Int, t)] -> [(Ident, Int, t)])
-> [(Ident, Int, t)] -> [(Ident, Int, t)]
forall a b. (a -> b) -> a -> b
$ Decl t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Decl t -> [(Ident, Int, t)]
declVars Decl t
d) ValueEnv
vEnv
  where unbound :: (Ident, b, c) -> Bool
unbound v :: (Ident, b, c)
v = [ValueInfo] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([ValueInfo] -> Bool) -> [ValueInfo] -> Bool
forall a b. (a -> b) -> a -> b
$ Ident -> ValueEnv -> [ValueInfo]
lookupValue ((Ident, b, c) -> Ident
forall a b c. (a, b, c) -> a
fst3 (Ident, b, c)
v) ValueEnv
vEnv

bindPatterns :: (Eq t, Typeable t, ValueType t) => [Pattern t] -> ValueEnv
             -> ValueEnv
bindPatterns :: [Pattern t] -> ValueEnv -> ValueEnv
bindPatterns = (ValueEnv -> [Pattern t] -> ValueEnv)
-> [Pattern t] -> ValueEnv -> ValueEnv
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((ValueEnv -> [Pattern t] -> ValueEnv)
 -> [Pattern t] -> ValueEnv -> ValueEnv)
-> (ValueEnv -> [Pattern t] -> ValueEnv)
-> [Pattern t]
-> ValueEnv
-> ValueEnv
forall a b. (a -> b) -> a -> b
$ (Pattern t -> ValueEnv -> ValueEnv)
-> ValueEnv -> [Pattern t] -> ValueEnv
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Pattern t -> ValueEnv -> ValueEnv
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> ValueEnv -> ValueEnv
bindPattern

bindPattern :: (Eq t, Typeable t, ValueType t) => Pattern t -> ValueEnv
            -> ValueEnv
bindPattern :: Pattern t -> ValueEnv -> ValueEnv
bindPattern t :: Pattern t
t vEnv :: ValueEnv
vEnv = [(Ident, Int, t)] -> ValueEnv -> ValueEnv
forall t. ValueType t => [(Ident, Int, t)] -> ValueEnv -> ValueEnv
bindLocalVars (((Ident, Int, t) -> Bool) -> [(Ident, Int, t)] -> [(Ident, Int, t)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Ident, Int, t) -> Bool
forall b c. (Ident, b, c) -> Bool
unbound ([(Ident, Int, t)] -> [(Ident, Int, t)])
-> [(Ident, Int, t)] -> [(Ident, Int, t)]
forall a b. (a -> b) -> a -> b
$ Pattern t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> [(Ident, Int, t)]
patternVars Pattern t
t) ValueEnv
vEnv
  where unbound :: (Ident, b, c) -> Bool
unbound v :: (Ident, b, c)
v = [ValueInfo] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([ValueInfo] -> Bool) -> [ValueInfo] -> Bool
forall a b. (a -> b) -> a -> b
$ Ident -> ValueEnv -> [ValueInfo]
lookupValue ((Ident, b, c) -> Ident
forall a b c. (a, b, c) -> a
fst3 (Ident, b, c)
v) ValueEnv
vEnv

declVars :: (Eq t, Typeable t, ValueType t) => Decl t -> [(Ident, Int, t)]
declVars :: Decl t -> [(Ident, Int, t)]
declVars (InfixDecl        _ _ _ _) = []
declVars (TypeSig            _ _ _) = []
declVars (FunctionDecl  _ ty :: t
ty f :: Ident
f eqs :: [Equation t]
eqs) = [(Ident
f, Equation t -> Int
forall a. Equation a -> Int
eqnArity (Equation t -> Int) -> Equation t -> Int
forall a b. (a -> b) -> a -> b
$ [Equation t] -> Equation t
forall a. [a] -> a
head [Equation t]
eqs, t
ty)]
declVars (PatternDecl        _ t :: Pattern t
t _) = Pattern t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> [(Ident, Int, t)]
patternVars Pattern t
t
declVars (FreeDecl            _ vs :: [Var t]
vs) = [(Ident
v, 0, t
ty) | Var ty :: t
ty v :: Ident
v <- [Var t]
vs]
declVars _                          = String -> [(Ident, Int, t)]
forall a. String -> a
internalError "Base.Typing.declVars"

patternVars :: (Eq t, Typeable t, ValueType t) => Pattern t -> [(Ident, Int, t)]
patternVars :: Pattern t -> [(Ident, Int, t)]
patternVars (LiteralPattern         _ _ _) = []
patternVars (NegativePattern        _ _ _) = []
patternVars (VariablePattern       _ ty :: t
ty v :: Ident
v) = [(Ident
v, 0, t
ty)]
patternVars (ConstructorPattern  _ _ _ ts :: [Pattern t]
ts) = (Pattern t -> [(Ident, Int, t)])
-> [Pattern t] -> [(Ident, Int, t)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pattern t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> [(Ident, Int, t)]
patternVars [Pattern t]
ts
patternVars (InfixPattern     _ _ t1 :: Pattern t
t1 _ t2 :: Pattern t
t2) = Pattern t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> [(Ident, Int, t)]
patternVars Pattern t
t1 [(Ident, Int, t)] -> [(Ident, Int, t)] -> [(Ident, Int, t)]
forall a. [a] -> [a] -> [a]
++ Pattern t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> [(Ident, Int, t)]
patternVars Pattern t
t2
patternVars (ParenPattern             _ t :: Pattern t
t) = Pattern t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> [(Ident, Int, t)]
patternVars Pattern t
t
patternVars (RecordPattern       _ _ _ fs :: [Field (Pattern t)]
fs) =
  [[(Ident, Int, t)]] -> [(Ident, Int, t)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Pattern t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> [(Ident, Int, t)]
patternVars Pattern t
t | Field _ _ t :: Pattern t
t <- [Field (Pattern t)]
fs]
patternVars (TuplePattern            _ ts :: [Pattern t]
ts) = (Pattern t -> [(Ident, Int, t)])
-> [Pattern t] -> [(Ident, Int, t)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pattern t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> [(Ident, Int, t)]
patternVars [Pattern t]
ts
patternVars (ListPattern           _ _ ts :: [Pattern t]
ts) = (Pattern t -> [(Ident, Int, t)])
-> [Pattern t] -> [(Ident, Int, t)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pattern t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> [(Ident, Int, t)]
patternVars [Pattern t]
ts
patternVars (AsPattern              _ v :: Ident
v t :: Pattern t
t) =
  (Ident
v, 0, Type -> t
forall t. ValueType t => Type -> t
toValueType (Type -> t) -> Type -> t
forall a b. (a -> b) -> a -> b
$ Pattern t -> Type
forall a. Typeable a => a -> Type
typeOf Pattern t
t) (Ident, Int, t) -> [(Ident, Int, t)] -> [(Ident, Int, t)]
forall a. a -> [a] -> [a]
: Pattern t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> [(Ident, Int, t)]
patternVars Pattern t
t
patternVars (LazyPattern              _ t :: Pattern t
t) = Pattern t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> [(Ident, Int, t)]
patternVars Pattern t
t
patternVars (FunctionPattern     _ _ _ ts :: [Pattern t]
ts) = [(Ident, Int, t)] -> [(Ident, Int, t)]
forall a. Eq a => [a] -> [a]
nub ([(Ident, Int, t)] -> [(Ident, Int, t)])
-> [(Ident, Int, t)] -> [(Ident, Int, t)]
forall a b. (a -> b) -> a -> b
$ (Pattern t -> [(Ident, Int, t)])
-> [Pattern t] -> [(Ident, Int, t)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pattern t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> [(Ident, Int, t)]
patternVars [Pattern t]
ts
patternVars (InfixFuncPattern _ _ t1 :: Pattern t
t1 _ t2 :: Pattern t
t2) =
  [(Ident, Int, t)] -> [(Ident, Int, t)]
forall a. Eq a => [a] -> [a]
nub ([(Ident, Int, t)] -> [(Ident, Int, t)])
-> [(Ident, Int, t)] -> [(Ident, Int, t)]
forall a b. (a -> b) -> a -> b
$ Pattern t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> [(Ident, Int, t)]
patternVars Pattern t
t1 [(Ident, Int, t)] -> [(Ident, Int, t)] -> [(Ident, Int, t)]
forall a. [a] -> [a] -> [a]
++ Pattern t -> [(Ident, Int, t)]
forall t.
(Eq t, Typeable t, ValueType t) =>
Pattern t -> [(Ident, Int, t)]
patternVars Pattern t
t2