{-# LANGUAGE PatternGuards #-}
module GF.Compile.TypeCheck.Concrete( checkLType, inferLType, computeLType, ppType ) where
import Prelude hiding ((<>))
import GF.Infra.CheckM
import GF.Data.Operations
import GF.Grammar
import GF.Grammar.Lookup
import GF.Grammar.Predef
import GF.Grammar.PatternMatch
import GF.Grammar.Lockfield (isLockLabel, lockRecType, unlockRecord)
import GF.Compile.TypeCheck.Primitives
import Data.List
import Control.Monad
import GF.Text.Pretty
computeLType :: SourceGrammar -> Context -> Type -> Check Type
computeLType :: SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr Context
g0 Type
t = Context -> Type -> Check Type
comp (Context -> Context
forall a. [a] -> [a]
reverse [(BindType
b,Ident
x, Ident -> Type
Vr Ident
x) | (BindType
b,Ident
x,Type
_) <- Context
g0] Context -> Context -> Context
forall a. [a] -> [a] -> [a]
++ Context
g0) Type
t
where
comp :: Context -> Type -> Check Type
comp Context
g Type
ty = case Type
ty of
Type
_ | Just Int
_ <- Type -> Maybe Int
isTypeInts Type
ty -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
| Type -> Bool
isPredefConstant Type
ty -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
Q (ModuleName
m,Ident
ident) -> Doc -> Check Type -> Check Type
forall a. Doc -> Check a -> Check a
checkIn ([Char]
"module" [Char] -> ModuleName -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> ModuleName
m) (Check Type -> Check Type) -> Check Type -> Check Type
forall a b. (a -> b) -> a -> b
$ do
Type
ty' <- SourceGrammar -> (ModuleName, Ident) -> Check Type
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> (ModuleName, Ident) -> m Type
lookupResDef SourceGrammar
gr (ModuleName
m,Ident
ident)
if Type
ty' Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
ty then Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty else Context -> Type -> Check Type
comp Context
g Type
ty'
AdHocOverload [Type]
ts -> do
Maybe (Type, Type)
over <- SourceGrammar
-> Context -> Maybe Type -> Type -> Check (Maybe (Type, Type))
getOverload SourceGrammar
gr Context
g (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
typeType) Type
t
case Maybe (Type, Type)
over of
Just (Type
tr,Type
_) -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
tr
Maybe (Type, Type)
_ -> Doc -> Check Type
forall a. Doc -> Check a
checkError ([Char]
"unresolved overloading of constants" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Qualified Integer
0 Type
t)
Vr Ident
ident -> Ident -> Context -> Check Type
checkLookup Ident
ident Context
g
App Type
f Type
a -> do
Type
f' <- Context -> Type -> Check Type
comp Context
g Type
f
Type
a' <- Context -> Type -> Check Type
comp Context
g Type
a
case Type
f' of
Abs BindType
b Ident
x Type
t -> Context -> Type -> Check Type
comp ((BindType
b,Ident
x,Type
a')(BindType, Ident, Type) -> Context -> Context
forall a. a -> [a] -> [a]
:Context
g) Type
t
Type
_ -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
App Type
f' Type
a'
Prod BindType
bt Ident
x Type
a Type
b -> do
Type
a' <- Context -> Type -> Check Type
comp Context
g Type
a
Type
b' <- Context -> Type -> Check Type
comp ((BindType
bt,Ident
x,Ident -> Type
Vr Ident
x) (BindType, Ident, Type) -> Context -> Context
forall a. a -> [a] -> [a]
: Context
g) Type
b
Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ BindType -> Ident -> Type -> Type -> Type
Prod BindType
bt Ident
x Type
a' Type
b'
Abs BindType
bt Ident
x Type
b -> do
Type
b' <- Context -> Type -> Check Type
comp ((BindType
bt,Ident
x,Ident -> Type
Vr Ident
x)(BindType, Ident, Type) -> Context -> Context
forall a. a -> [a] -> [a]
:Context
g) Type
b
Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ BindType -> Ident -> Type -> Type
Abs BindType
bt Ident
x Type
b'
Let (Ident
x,(Maybe Type
_,Type
a)) Type
b -> Context -> Type -> Check Type
comp ((BindType
Explicit,Ident
x,Type
a)(BindType, Ident, Type) -> Context -> Context
forall a. a -> [a] -> [a]
:Context
g) Type
b
ExtR Type
r Type
s -> do
Type
r' <- Context -> Type -> Check Type
comp Context
g Type
r
Type
s' <- Context -> Type -> Check Type
comp Context
g Type
s
case (Type
r',Type
s') of
(RecType [Labelling]
rs, RecType [Labelling]
ss) -> Type -> Type -> Check Type
forall (m :: * -> *). ErrorMonad m => Type -> Type -> m Type
plusRecType Type
r' Type
s' Check Type -> (Type -> Check Type) -> Check Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Context -> Type -> Check Type
comp Context
g
(Type, Type)
_ -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
ExtR Type
r' Type
s'
RecType [Labelling]
fs -> do
let fs' :: [Labelling]
fs' = [Labelling] -> [Labelling]
forall a. [(Label, a)] -> [(Label, a)]
sortRec [Labelling]
fs
([Labelling] -> Type) -> Check [Labelling] -> Check Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Labelling] -> Type
RecType (Check [Labelling] -> Check Type)
-> Check [Labelling] -> Check Type
forall a b. (a -> b) -> a -> b
$ (Type -> Check Type) -> [Labelling] -> Check [Labelling]
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> [(a, b)] -> m [(a, c)]
mapPairsM (Context -> Type -> Check Type
comp Context
g) [Labelling]
fs'
ELincat Ident
c Type
t -> do
Type
t' <- Context -> Type -> Check Type
comp Context
g Type
t
Ident -> Type -> Check Type
forall (m :: * -> *). ErrorMonad m => Ident -> Type -> m Type
lockRecType Ident
c Type
t'
Type
_ | Type
ty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
typeTok -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
typeStr
Type
_ -> (Type -> Check Type) -> Type -> Check Type
forall (m :: * -> *). Monad m => (Type -> m Type) -> Type -> m Type
composOp (Context -> Type -> Check Type
comp Context
g) Type
ty
inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
inferLType :: SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
trm = case Type
trm of
Q (ModuleName
m,Ident
ident) | ModuleName -> Bool
isPredef ModuleName
m -> Type -> Check Type -> Check (Type, Type)
termWith Type
trm (Check Type -> Check (Type, Type))
-> Check Type -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ case Ident -> Maybe Type
typPredefined Ident
ident of
Just Type
ty -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
Maybe Type
Nothing -> Doc -> Check Type
forall a. Doc -> Check a
checkError ([Char]
"unknown in Predef:" [Char] -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
ident)
Q (ModuleName, Ident)
ident -> [Check (Type, Type)] -> Check (Type, Type)
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks [
Type -> Check Type -> Check (Type, Type)
termWith Type
trm (Check Type -> Check (Type, Type))
-> Check Type -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ SourceGrammar -> (ModuleName, Ident) -> Check Type
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> (ModuleName, Ident) -> m Type
lookupResType SourceGrammar
gr (ModuleName, Ident)
ident Check Type -> (Type -> Check Type) -> Check Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr Context
g
,
SourceGrammar -> (ModuleName, Ident) -> Check Type
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> (ModuleName, Ident) -> m Type
lookupResDef SourceGrammar
gr (ModuleName, Ident)
ident Check Type -> (Type -> Check (Type, Type)) -> Check (Type, Type)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g
,
Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError ([Char]
"cannot infer type of constant" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
trm)
]
QC (ModuleName
m,Ident
ident) | ModuleName -> Bool
isPredef ModuleName
m -> Type -> Check Type -> Check (Type, Type)
termWith Type
trm (Check Type -> Check (Type, Type))
-> Check Type -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ case Ident -> Maybe Type
typPredefined Ident
ident of
Just Type
ty -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
Maybe Type
Nothing -> Doc -> Check Type
forall a. Doc -> Check a
checkError ([Char]
"unknown in Predef:" [Char] -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
ident)
QC (ModuleName, Ident)
ident -> [Check (Type, Type)] -> Check (Type, Type)
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks [
Type -> Check Type -> Check (Type, Type)
termWith Type
trm (Check Type -> Check (Type, Type))
-> Check Type -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ SourceGrammar -> (ModuleName, Ident) -> Check Type
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> (ModuleName, Ident) -> m Type
lookupResType SourceGrammar
gr (ModuleName, Ident)
ident Check Type -> (Type -> Check Type) -> Check Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr Context
g
,
SourceGrammar -> (ModuleName, Ident) -> Check Type
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> (ModuleName, Ident) -> m Type
lookupResDef SourceGrammar
gr (ModuleName, Ident)
ident Check Type -> (Type -> Check (Type, Type)) -> Check (Type, Type)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g
,
Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError ([Char]
"cannot infer type of canonical constant" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
trm)
]
Vr Ident
ident -> Type -> Check Type -> Check (Type, Type)
termWith Type
trm (Check Type -> Check (Type, Type))
-> Check Type -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ Ident -> Context -> Check Type
checkLookup Ident
ident Context
g
Typed Type
e Type
t -> do
Type
t' <- SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr Context
g Type
t
SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
e Type
t'
AdHocOverload [Type]
ts -> do
Maybe (Type, Type)
over <- SourceGrammar
-> Context -> Maybe Type -> Type -> Check (Maybe (Type, Type))
getOverload SourceGrammar
gr Context
g Maybe Type
forall a. Maybe a
Nothing Type
trm
case Maybe (Type, Type)
over of
Just (Type, Type)
trty -> (Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type, Type)
trty
Maybe (Type, Type)
_ -> Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError ([Char]
"unresolved overloading of constants" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Qualified Integer
0 Type
trm)
App Type
f Type
a -> do
Maybe (Type, Type)
over <- SourceGrammar
-> Context -> Maybe Type -> Type -> Check (Maybe (Type, Type))
getOverload SourceGrammar
gr Context
g Maybe Type
forall a. Maybe a
Nothing Type
trm
case Maybe (Type, Type)
over of
Just (Type, Type)
trty -> (Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type, Type)
trty
Maybe (Type, Type)
_ -> do
(Type
f',Type
fty) <- SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
f
Type
fty' <- SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr Context
g Type
fty
case Type
fty' of
Prod BindType
bt Ident
z Type
arg Type
val -> do
Type
a' <- Context -> Type -> Type -> Check Type
justCheck Context
g Type
a Type
arg
Type
ty <- if Ident -> Bool
isWildIdent Ident
z
then Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
val
else Context -> Type -> Check Type
substituteLType [(BindType
bt,Ident
z,Type
a')] Type
val
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
App Type
f' Type
a',Type
ty)
Type
_ ->
let term :: Doc
term = TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
f
funName :: Doc
funName = [Char] -> Doc
forall a. Pretty a => a -> Doc
pp ([Char] -> Doc) -> (Doc -> [Char]) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Char]] -> [Char]
forall a. [a] -> a
head ([[Char]] -> [Char]) -> (Doc -> [[Char]]) -> Doc -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[Char]]
words ([Char] -> [[Char]]) -> (Doc -> [Char]) -> Doc -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Doc -> [Char]
forall a. Pretty a => a -> [Char]
render (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
term
in Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError ([Char]
"A function type is expected for" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Doc
term Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Char]
"instead of type" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Type -> Doc
ppType Type
fty Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
[Char]
"\n ** Maybe you gave too many arguments to" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Doc
funName Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Char]
"\n")
S Type
f Type
x -> do
(Type
f', Type
fty) <- SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
f
case Type
fty of
Table Type
arg Type
val -> do
Type
x'<- Context -> Type -> Type -> Check Type
justCheck Context
g Type
x Type
arg
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
S Type
f' Type
x', Type
val)
Type
_ -> Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError ([Char]
"table lintype expected for the table in" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$ Int -> Doc -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 (TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
trm))
P Type
t Label
i -> do
(Type
t',Type
ty) <- SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
t
Type
ty' <- SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr Context
g Type
ty
let tr2 :: Type
tr2 = Type -> Label -> Type
P Type
t' Label
i
Type -> Check Type -> Check (Type, Type)
termWith Type
tr2 (Check Type -> Check (Type, Type))
-> Check Type -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ case Type
ty' of
RecType [Labelling]
ts -> case Label -> [Labelling] -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Label
i [Labelling]
ts of
Maybe Type
Nothing -> Doc -> Check Type
forall a. Doc -> Check a
checkError ([Char]
"unknown label" [Char] -> Label -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Label
i Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Char]
"in" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$ Int -> Doc -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 (TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
ty'))
Just Type
x -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
x
Type
_ -> Doc -> Check Type
forall a. Doc -> Check a
checkError ([Char]
"record type expected for:" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
t Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
[Char]
" instead of the inferred:" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
ty')
R [Assign]
r -> do
let ([Label]
ls,[(Maybe Type, Type)]
fs) = [Assign] -> ([Label], [(Maybe Type, Type)])
forall a b. [(a, b)] -> ([a], [b])
unzip [Assign]
r
[(Maybe Type, Type)]
fsts <- ((Maybe Type, Type) -> Check (Maybe Type, Type))
-> [(Maybe Type, Type)] -> Check [(Maybe Type, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe Type, Type) -> Check (Maybe Type, Type)
inferM [(Maybe Type, Type)]
fs
let ts :: [Type]
ts = [Type
ty | (Just Type
ty,Type
_) <- [(Maybe Type, Type)]
fsts]
Doc -> Bool -> Check ()
checkCond ([Char]
"cannot infer type of record" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$ Int -> Doc -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 (TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
trm)) ([Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [(Maybe Type, Type)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Maybe Type, Type)]
fsts)
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type, Type) -> Check (Type, Type))
-> (Type, Type) -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ ([Assign] -> Type
R ([Label] -> [(Maybe Type, Type)] -> [Assign]
forall a b. [a] -> [b] -> [(a, b)]
zip [Label]
ls [(Maybe Type, Type)]
fsts), [Labelling] -> Type
RecType ([Label] -> [Type] -> [Labelling]
forall a b. [a] -> [b] -> [(a, b)]
zip [Label]
ls [Type]
ts))
T (TTyped Type
arg) [Case]
pts -> do
(Type
_,Type
val) <- [Check (Type, Type)] -> Check (Type, Type)
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks ([Check (Type, Type)] -> Check (Type, Type))
-> [Check (Type, Type)] -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ (Case -> Check (Type, Type)) -> [Case] -> [Check (Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Type -> Case -> Check (Type, Type)
inferCase (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
arg)) [Case]
pts
SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
trm (Type -> Type -> Type
Table Type
arg Type
val)
T (TComp Type
arg) [Case]
pts -> do
(Type
_,Type
val) <- [Check (Type, Type)] -> Check (Type, Type)
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks ([Check (Type, Type)] -> Check (Type, Type))
-> [Check (Type, Type)] -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ (Case -> Check (Type, Type)) -> [Case] -> [Check (Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Type -> Case -> Check (Type, Type)
inferCase (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
arg)) [Case]
pts
SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
trm (Type -> Type -> Type
Table Type
arg Type
val)
T TInfo
ti [Case]
pts -> do
let pts' :: [Case]
pts' = [Case
pt | pt :: Case
pt@(Patt
p,Type
_) <- [Case]
pts, Patt -> Bool
isConstPatt Patt
p]
case [Case]
pts' of
[] -> Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError ([Char]
"cannot infer table type of" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
trm)
[Case]
_ -> do
(Type
arg,Type
val) <- [Check (Type, Type)] -> Check (Type, Type)
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks ([Check (Type, Type)] -> Check (Type, Type))
-> [Check (Type, Type)] -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ (Case -> Check (Type, Type)) -> [Case] -> [Check (Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Type -> Case -> Check (Type, Type)
inferCase Maybe Type
forall a. Maybe a
Nothing) [Case]
pts'
SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
trm (Type -> Type -> Type
Table Type
arg Type
val)
V Type
arg [Type]
pts -> do
(Type
_,Type
val) <- [Check (Type, Type)] -> Check (Type, Type)
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks ([Check (Type, Type)] -> Check (Type, Type))
-> [Check (Type, Type)] -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ (Type -> Check (Type, Type)) -> [Type] -> [Check (Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g) [Type]
pts
SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
trm (Type -> Type -> Type
Table Type
arg Type
val)
K [Char]
s -> do
if Char -> [Char] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
' ' [Char]
s
then do
let ss :: Type
ss = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
C Type
Empty (([Char] -> Type) -> [[Char]] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> Type
K ([Char] -> [[Char]]
words [Char]
s))
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ss, Type
typeStr)
else (Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
trm, Type
typeStr)
EInt Int
i -> (Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
trm, Type
typeInt)
EFloat Double
i -> (Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
trm, Type
typeFloat)
Type
Empty -> (Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
trm, Type
typeStr)
C Type
s1 Type
s2 ->
(Type -> Check Type)
-> (Type -> Type -> Type)
-> Type
-> Type
-> Type
-> Check (Type, Type)
check2 ((Type -> Type -> Check Type) -> Type -> Type -> Check Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Context -> Type -> Type -> Check Type
justCheck Context
g) Type
typeStr) Type -> Type -> Type
C Type
s1 Type
s2 Type
typeStr
Glue Type
s1 Type
s2 ->
(Type -> Check Type)
-> (Type -> Type -> Type)
-> Type
-> Type
-> Type
-> Check (Type, Type)
check2 ((Type -> Type -> Check Type) -> Type -> Type -> Check Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Context -> Type -> Type -> Check Type
justCheck Context
g) Type
typeStr) Type -> Type -> Type
Glue Type
s1 Type
s2 Type
typeStr
Strs (Cn Ident
c : [Type]
ts) | Ident
c Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cConflict -> do
Doc -> Check ()
checkWarn ([Char]
"unresolved constant, could be any of" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Doc] -> Doc
forall a. Pretty a => [a] -> Doc
hcat ((Type -> Doc) -> [Type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0) [Type]
ts))
SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g ([Type] -> Type
forall a. [a] -> a
head [Type]
ts)
Strs [Type]
ts -> do
[Type]
ts' <- (Type -> Check Type) -> [Type] -> Check [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\Type
t -> Context -> Type -> Type -> Check Type
justCheck Context
g Type
t Type
typeStr) [Type]
ts
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> Type
Strs [Type]
ts', Type
typeStrs)
Alts Type
t [(Type, Type)]
aa -> do
Type
t' <- Context -> Type -> Type -> Check Type
justCheck Context
g Type
t Type
typeStr
[(Type, Type)]
aa' <- (((Type, Type) -> Check (Type, Type))
-> [(Type, Type)] -> Check [(Type, Type)])
-> [(Type, Type)]
-> ((Type, Type) -> Check (Type, Type))
-> Check [(Type, Type)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Type, Type) -> Check (Type, Type))
-> [(Type, Type)] -> Check [(Type, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [(Type, Type)]
aa (\ (Type
c,Type
v) -> do
Type
c' <- Context -> Type -> Type -> Check Type
justCheck Context
g Type
c Type
typeStr
Type
v' <- [Check Type] -> Check Type
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks ([Check Type] -> Check Type) -> [Check Type] -> Check Type
forall a b. (a -> b) -> a -> b
$ (Type -> Check Type) -> [Type] -> [Check Type]
forall a b. (a -> b) -> [a] -> [b]
map (Context -> Type -> Type -> Check Type
justCheck Context
g Type
v) [Type
typeStrs, Type -> Type
EPattType Type
typeStr]
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
c',Type
v'))
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> [(Type, Type)] -> Type
Alts Type
t' [(Type, Type)]
aa', Type
typeStr)
RecType [Labelling]
r -> do
let ([Label]
ls,[Type]
ts) = [Labelling] -> ([Label], [Type])
forall a b. [(a, b)] -> ([a], [b])
unzip [Labelling]
r
[Type]
ts' <- (Type -> Check Type) -> [Type] -> Check [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Type -> Type -> Check Type) -> Type -> Type -> Check Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Context -> Type -> Type -> Check Type
justCheck Context
g) Type
typeType) [Type]
ts
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Labelling] -> Type
RecType ([Label] -> [Type] -> [Labelling]
forall a b. [a] -> [b] -> [(a, b)]
zip [Label]
ls [Type]
ts'), Type
typeType)
ExtR Type
r Type
s -> do
let r1 :: Type
r1 = Type
r
(Type
r',Type
rT) <- SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
r1
Type
rT' <- SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr Context
g Type
rT
(Type
s',Type
sT) <- SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
s
Type
sT' <- SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr Context
g Type
sT
let trm' :: Type
trm' = Type -> Type -> Type
ExtR Type
r' Type
s'
case (Type
rT', Type
sT') of
(RecType [Labelling]
rs, RecType [Labelling]
ss) -> do
let rt :: Type
rt = [Labelling] -> Type
RecType ([Labelling
field | field :: Labelling
field@(Label
l,Type
_) <- [Labelling]
rs, Label -> [Label] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Label
l ((Labelling -> Label) -> [Labelling] -> [Label]
forall a b. (a -> b) -> [a] -> [b]
map Labelling -> Label
forall a b. (a, b) -> a
fst [Labelling]
ss)] [Labelling] -> [Labelling] -> [Labelling]
forall a. [a] -> [a] -> [a]
++ [Labelling]
ss)
SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
trm' Type
rt
(Type, Type)
_ | Type
rT' Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
typeType Bool -> Bool -> Bool
&& Type
sT' Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
typeType -> do
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
trm', Type
typeType)
(Type, Type)
_ -> Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError ([Char]
"records or record types expected in" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
trm)
Sort Ident
_ ->
Type -> Check Type -> Check (Type, Type)
termWith Type
trm (Check Type -> Check (Type, Type))
-> Check Type -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
typeType
Prod BindType
bt Ident
x Type
a Type
b -> do
Type
a' <- Context -> Type -> Type -> Check Type
justCheck Context
g Type
a Type
typeType
Type
b' <- Context -> Type -> Type -> Check Type
justCheck ((BindType
bt,Ident
x,Type
a')(BindType, Ident, Type) -> Context -> Context
forall a. a -> [a] -> [a]
:Context
g) Type
b Type
typeType
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (BindType -> Ident -> Type -> Type -> Type
Prod BindType
bt Ident
x Type
a' Type
b', Type
typeType)
Table Type
p Type
t -> do
Type
p' <- Context -> Type -> Type -> Check Type
justCheck Context
g Type
p Type
typeType
Type
t' <- Context -> Type -> Type -> Check Type
justCheck Context
g Type
t Type
typeType
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type, Type) -> Check (Type, Type))
-> (Type, Type) -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Type
Table Type
p' Type
t', Type
typeType)
FV [Type]
vs -> do
(Type
_,Type
ty) <- [Check (Type, Type)] -> Check (Type, Type)
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks ([Check (Type, Type)] -> Check (Type, Type))
-> [Check (Type, Type)] -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ (Type -> Check (Type, Type)) -> [Type] -> [Check (Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g) [Type]
vs
SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
trm Type
ty
EPattType Type
ty -> do
Type
ty' <- Context -> Type -> Type -> Check Type
justCheck Context
g Type
ty Type
typeType
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type
EPattType Type
ty',Type
typeType)
EPatt Patt
p -> do
Type
ty <- Patt -> Check Type
inferPatt Patt
p
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
trm, Type -> Type
EPattType Type
ty)
ELin Ident
c Type
trm -> do
(Type
trm',Type
ty) <- SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
trm
Type
ty' <- Ident -> Type -> Check Type
forall (m :: * -> *). ErrorMonad m => Ident -> Type -> m Type
lockRecType Ident
c Type
ty
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type, Type) -> Check (Type, Type))
-> (Type, Type) -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ (Ident -> Type -> Type
ELin Ident
c Type
trm', Type
ty')
Type
_ -> Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError ([Char]
"cannot infer lintype of" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
trm)
where
isPredef :: ModuleName -> Bool
isPredef ModuleName
m = ModuleName -> [ModuleName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ModuleName
m [ModuleName
cPredef,ModuleName
cPredefAbs]
justCheck :: Context -> Type -> Type -> Check Type
justCheck Context
g Type
ty Type
te = SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
ty Type
te Check (Type, Type) -> ((Type, Type) -> Check Type) -> Check Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type)
-> ((Type, Type) -> Type) -> (Type, Type) -> Check Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, Type) -> Type
forall a b. (a, b) -> a
fst
inferM :: (Maybe Type, Type) -> Check (Maybe Type, Type)
inferM (Maybe Type
mty, Type
t) = do
(Type
t', Type
ty') <- case Maybe Type
mty of
Just Type
ty -> SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
t Type
ty
Maybe Type
_ -> SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
t
(Maybe Type, Type) -> Check (Maybe Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty',Type
t')
inferCase :: Maybe Type -> Case -> Check (Type, Type)
inferCase Maybe Type
mty (Patt
patt,Type
term) = do
Type
arg <- Check Type -> (Type -> Check Type) -> Maybe Type -> Check Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Patt -> Check Type
inferPatt Patt
patt) Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
mty
Context
cont <- SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext SourceGrammar
gr Context
g Type
arg Patt
patt
(Type
_,Type
val) <- SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr (Context -> Context
forall a. [a] -> [a]
reverse Context
cont Context -> Context -> Context
forall a. [a] -> [a] -> [a]
++ Context
g) Type
term
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
arg,Type
val)
isConstPatt :: Patt -> Bool
isConstPatt Patt
p = case Patt
p of
PC Ident
_ [Patt]
ps -> Bool
True
PP (ModuleName, Ident)
_ [Patt]
ps -> Bool
True
PR [(Label, Patt)]
ps -> ((Label, Patt) -> Bool) -> [(Label, Patt)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Patt -> Bool
isConstPatt (Patt -> Bool) -> ((Label, Patt) -> Patt) -> (Label, Patt) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Label, Patt) -> Patt
forall a b. (a, b) -> b
snd) [(Label, Patt)]
ps
PT Type
_ Patt
p -> Patt -> Bool
isConstPatt Patt
p
PString [Char]
_ -> Bool
True
PInt Int
_ -> Bool
True
PFloat Double
_ -> Bool
True
Patt
PChar -> Bool
True
PChars [Char]
_ -> Bool
True
PSeq Patt
p Patt
q -> Patt -> Bool
isConstPatt Patt
p Bool -> Bool -> Bool
&& Patt -> Bool
isConstPatt Patt
q
PAlt Patt
p Patt
q -> Patt -> Bool
isConstPatt Patt
p Bool -> Bool -> Bool
&& Patt -> Bool
isConstPatt Patt
q
PRep Patt
p -> Patt -> Bool
isConstPatt Patt
p
PNeg Patt
p -> Patt -> Bool
isConstPatt Patt
p
PAs Ident
_ Patt
p -> Patt -> Bool
isConstPatt Patt
p
Patt
_ -> Bool
False
inferPatt :: Patt -> Check Type
inferPatt Patt
p = case Patt
p of
PP (ModuleName
q,Ident
c) [Patt]
ps | ModuleName
q ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
/= ModuleName
cPredef -> (Type -> Type) -> Check Type -> Check Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Type -> Type
valTypeCnc (SourceGrammar -> (ModuleName, Ident) -> Check Type
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> (ModuleName, Ident) -> m Type
lookupResType SourceGrammar
gr (ModuleName
q,Ident
c))
PAs Ident
_ Patt
p -> Patt -> Check Type
inferPatt Patt
p
PNeg Patt
p -> Patt -> Check Type
inferPatt Patt
p
PAlt Patt
p Patt
q -> [Check Type] -> Check Type
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks [Patt -> Check Type
inferPatt Patt
p, Patt -> Check Type
inferPatt Patt
q]
PSeq Patt
_ Patt
_ -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Type
typeStr
PRep Patt
_ -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Type
typeStr
Patt
PChar -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Type
typeStr
PChars [Char]
_ -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Type
typeStr
Patt
_ -> SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g (Patt -> Type
patt2term Patt
p) Check (Type, Type) -> ((Type, Type) -> Check Type) -> Check Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type)
-> ((Type, Type) -> Type) -> (Type, Type) -> Check Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, Type) -> Type
forall a b. (a, b) -> b
snd
getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
getOverload :: SourceGrammar
-> Context -> Maybe Type -> Type -> Check (Maybe (Type, Type))
getOverload SourceGrammar
gr Context
g Maybe Type
mt Type
ot = case Type -> (Type, [Type])
appForm Type
ot of
(f :: Type
f@(Q (ModuleName, Ident)
c), [Type]
ts) -> case SourceGrammar
-> (ModuleName, Ident) -> Err [([Type], (Type, Type))]
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> (ModuleName, Ident) -> m [([Type], (Type, Type))]
lookupOverload SourceGrammar
gr (ModuleName, Ident)
c of
Ok [([Type], (Type, Type))]
typs -> do
[(Type, Type)]
ttys <- (Type -> Check (Type, Type)) -> [Type] -> Check [(Type, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g) [Type]
ts
(Type, Type)
v <- Type
-> [([Type], (Type, Type))] -> [(Type, Type)] -> Check (Type, Type)
matchOverload Type
f [([Type], (Type, Type))]
typs [(Type, Type)]
ttys
Maybe (Type, Type) -> Check (Maybe (Type, Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Type, Type) -> Check (Maybe (Type, Type)))
-> Maybe (Type, Type) -> Check (Maybe (Type, Type))
forall a b. (a -> b) -> a -> b
$ (Type, Type) -> Maybe (Type, Type)
forall a. a -> Maybe a
Just (Type, Type)
v
Err [([Type], (Type, Type))]
_ -> Maybe (Type, Type) -> Check (Maybe (Type, Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Type, Type)
forall a. Maybe a
Nothing
(AdHocOverload cs :: [Type]
cs@(Type
f:[Type]
_), [Type]
ts) -> do
let typs :: [([Type], (Type, Type))]
typs = (Type -> [([Type], (Type, Type))])
-> [Type] -> [([Type], (Type, Type))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [([Type], (Type, Type))]
collectOverloads [Type]
cs
[(Type, Type)]
ttys <- (Type -> Check (Type, Type)) -> [Type] -> Check [(Type, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g) [Type]
ts
(Type, Type)
v <- Type
-> [([Type], (Type, Type))] -> [(Type, Type)] -> Check (Type, Type)
matchOverload Type
f [([Type], (Type, Type))]
typs [(Type, Type)]
ttys
Maybe (Type, Type) -> Check (Maybe (Type, Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Type, Type) -> Check (Maybe (Type, Type)))
-> Maybe (Type, Type) -> Check (Maybe (Type, Type))
forall a b. (a -> b) -> a -> b
$ (Type, Type) -> Maybe (Type, Type)
forall a. a -> Maybe a
Just (Type, Type)
v
(Type, [Type])
_ -> Maybe (Type, Type) -> Check (Maybe (Type, Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Type, Type)
forall a. Maybe a
Nothing
where
collectOverloads :: Type -> [([Type], (Type, Type))]
collectOverloads tr :: Type
tr@(Q (ModuleName, Ident)
c) = case SourceGrammar
-> (ModuleName, Ident) -> Err [([Type], (Type, Type))]
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> (ModuleName, Ident) -> m [([Type], (Type, Type))]
lookupOverload SourceGrammar
gr (ModuleName, Ident)
c of
Ok [([Type], (Type, Type))]
typs -> [([Type], (Type, Type))]
typs
Err [([Type], (Type, Type))]
_ -> case SourceGrammar -> (ModuleName, Ident) -> Err Type
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> (ModuleName, Ident) -> m Type
lookupResType SourceGrammar
gr (ModuleName, Ident)
c of
Ok Type
ty -> let (Context
args,Type
val) = Type -> (Context, Type)
typeFormCnc Type
ty in [(((BindType, Ident, Type) -> Type) -> Context -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (\(BindType
b,Ident
x,Type
t) -> Type
t) Context
args,(Type
val,Type
tr))]
Err Type
_ -> []
collectOverloads Type
_ = []
matchOverload :: Type
-> [([Type], (Type, Type))] -> [(Type, Type)] -> Check (Type, Type)
matchOverload Type
f [([Type], (Type, Type))]
typs [(Type, Type)]
ttys = do
let ([Type]
tts,[Type]
tys) = [(Type, Type)] -> ([Type], [Type])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Type, Type)]
ttys
let vfs :: [(([Type], Type, Type), Bool)]
vfs = [Type]
-> [([Type], (Type, Type))] -> [(([Type], Type, Type), Bool)]
forall c.
[Type] -> [([Type], (Type, c))] -> [(([Type], Type, c), Bool)]
lookupOverloadInstance [Type]
tys [([Type], (Type, Type))]
typs
let matches :: [(([Type], Type, Type), Bool)]
matches = [(([Type], Type, Type), Bool)
vf | vf :: (([Type], Type, Type), Bool)
vf@(([Type]
_,Type
v,Type
_),Bool
_) <- [(([Type], Type, Type), Bool)]
vfs, Maybe Type -> Type -> Bool
matchVal Maybe Type
mt Type
v]
let showTypes :: [Type] -> Doc
showTypes [Type]
ty = [Doc] -> Doc
forall a. Pretty a => [a] -> Doc
hsep ((Type -> Doc) -> [Type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Doc
ppType [Type]
ty)
let (Doc
stys,[Doc]
styps) = ([Type] -> Doc
showTypes [Type]
tys, [[Type] -> Doc
showTypes [Type]
ty | ([Type]
ty,(Type, Type)
_) <- [([Type], (Type, Type))]
typs])
let (Doc
stysError,[Doc]
stypsError) = if [Char] -> [[Char]] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (Doc -> [Char]
forall a. Pretty a => a -> [Char]
render Doc
stys) ((Doc -> [Char]) -> [Doc] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> [Char]
forall a. Pretty a => a -> [Char]
render [Doc]
styps)
then ([Doc] -> Doc
forall a. Pretty a => [a] -> Doc
hsep ((Type -> Doc) -> [Type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0) [Type]
tys), [[Doc] -> Doc
forall a. Pretty a => [a] -> Doc
hsep ((Type -> Doc) -> [Type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0) [Type]
ty) | ([Type]
ty,(Type, Type)
_) <- [([Type], (Type, Type))]
typs])
else (Doc
stys,[Doc]
styps)
case ([([Type], Type, Type)
vf | (([Type], Type, Type)
vf,Bool
True) <- [(([Type], Type, Type), Bool)]
matches],[([Type], Type, Type)
vf | (([Type], Type, Type)
vf,Bool
False) <- [(([Type], Type, Type), Bool)]
matches]) of
([([Type]
_,Type
val,Type
fun)],[([Type], Type, Type)]
_) -> (Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> [Type] -> Type
mkApp Type
fun [Type]
tts, Type
val)
([],[([Type]
pre,Type
val,Type
fun)]) -> do
Doc -> Check ()
checkWarn (Doc -> Check ()) -> Doc -> Check ()
forall a b. (a -> b) -> a -> b
$ [Char]
"ignoring lock fields in resolving" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
ot Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
[Char]
"for" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
Int -> Doc -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 ([Type] -> Doc
showTypes [Type]
tys) Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
[Char]
"using" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
Int -> Doc -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 ([Type] -> Doc
showTypes [Type]
pre)
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> [Type] -> Type
mkApp Type
fun [Type]
tts, Type
val)
([],[]) -> do
Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError (Doc -> Check (Type, Type)) -> Doc -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ [Char]
"no overload instance of" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Qualified Integer
0 Type
f Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
Doc -> (Type -> Doc) -> Maybe Type -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty (\Type
x -> [Char]
"with value type" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Type -> Doc
ppType Type
x) Maybe Type
mt Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
[Char]
"for argument list" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
Int -> Doc -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 Doc
stysError Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
[Char]
"among alternatives" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
Int -> Doc -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 ([Doc] -> Doc
forall a. Pretty a => [a] -> Doc
vcat [Doc]
stypsError)
([([Type], Type, Type)]
vfs1,[([Type], Type, Type)]
vfs2) -> case ([([Type], Type, Type)] -> [(Type, Type)]
forall a b. [(a, Type, b)] -> [(Type, b)]
noProds [([Type], Type, Type)]
vfs1,[([Type], Type, Type)] -> [(Type, Type)]
forall a b. [(a, Type, b)] -> [(Type, b)]
noProds [([Type], Type, Type)]
vfs2) of
([(Type
val,Type
fun)],[(Type, Type)]
_) -> do
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> [Type] -> Type
mkApp Type
fun [Type]
tts, Type
val)
([],[(Type
val,Type
fun)]) -> do
Doc -> Check ()
checkWarn ([Char]
"ignoring lock fields in resolving" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
ot)
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> [Type] -> Type
mkApp Type
fun [Type]
tts, Type
val)
([(Type, Type)]
nps1,[(Type, Type)]
nps2) -> do
Doc -> Check ()
checkWarn (Doc -> Check ()) -> Doc -> Check ()
forall a b. (a -> b) -> a -> b
$ [Char]
"ambiguous overloading of" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
f Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+>
[Char]
"resolved by selecting the first of the alternatives" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
Int -> Doc -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 ([Doc] -> Doc
forall a. Pretty a => [a] -> Doc
vcat [TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Qualified Integer
0 Type
fun | ([Type]
_,Type
ty,Type
fun) <- [([Type], Type, Type)]
vfs1 [([Type], Type, Type)]
-> [([Type], Type, Type)] -> [([Type], Type, Type)]
forall a. [a] -> [a] -> [a]
++ if [([Type], Type, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Type], Type, Type)]
vfs1 then [([Type], Type, Type)]
vfs2 else []])
case [(Type -> [Type] -> Type
mkApp Type
fun [Type]
tts,Type
val) | (Type
val,Type
fun) <- [(Type, Type)]
nps1 [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++ [(Type, Type)]
nps2] of
[] -> Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError (Doc -> Check (Type, Type)) -> Doc -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ [Char]
"no alternatives left when resolving" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
f
(Type, Type)
h:[(Type, Type)]
_ -> (Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type, Type)
h
matchVal :: Maybe Type -> Type -> Bool
matchVal Maybe Type
mt Type
v = Maybe Type -> [Maybe Type] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Maybe Type
mt [Maybe Type
forall a. Maybe a
Nothing,Type -> Maybe Type
forall a. a -> Maybe a
Just Type
v,Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Type
unlocked Type
v)]
unlocked :: Type -> Type
unlocked Type
v = case Type
v of
RecType [Labelling]
fs -> [Labelling] -> Type
RecType ([Labelling] -> Type) -> [Labelling] -> Type
forall a b. (a -> b) -> a -> b
$ (Labelling -> Bool) -> [Labelling] -> [Labelling]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Labelling -> Bool) -> Labelling -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label -> Bool
isLockLabel (Label -> Bool) -> (Labelling -> Label) -> Labelling -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Labelling -> Label
forall a b. (a, b) -> a
fst) ([Labelling] -> [Labelling]
forall a. [(Label, a)] -> [(Label, a)]
sortRec [Labelling]
fs)
Type
_ -> Type
v
lookupOverloadInstance :: [Type] -> [([Type], (Type, c))] -> [(([Type], Type, c), Bool)]
lookupOverloadInstance [Type]
tys [([Type], (Type, c))]
typs =
[(([Type]
pre,[Type] -> Type -> Type
mkFunType [Type]
rest Type
val, c
t),Bool
isExact) |
let lt :: Int
lt = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys,
([Type]
ty,(Type
val,c
t)) <- [([Type], (Type, c))]
typs, [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ty Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
lt,
let ([Type]
pre,[Type]
rest) = Int -> [Type] -> ([Type], [Type])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
lt [Type]
ty,
let isExact :: Bool
isExact = [Type]
pre [Type] -> [Type] -> Bool
forall a. Eq a => a -> a -> Bool
== [Type]
tys,
Bool
isExact Bool -> Bool -> Bool
|| (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
unlocked [Type]
pre [Type] -> [Type] -> Bool
forall a. Eq a => a -> a -> Bool
== (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
unlocked [Type]
tys
]
noProds :: [(a, Type, b)] -> [(Type, b)]
noProds [(a, Type, b)]
vfs = [(Type
v,b
f) | (a
_,Type
v,b
f) <- [(a, Type, b)]
vfs, Type -> Bool
noProd Type
v]
noProd :: Type -> Bool
noProd Type
ty = case Type
ty of
Prod BindType
_ Ident
_ Type
_ Type
_ -> Bool
False
Type
_ -> Bool
True
checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
checkLType :: SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
trm Type
typ0 = do
Type
typ <- SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr Context
g Type
typ0
case Type
trm of
Abs BindType
bt Ident
x Type
c -> do
case Type
typ of
Prod BindType
bt' Ident
z Type
a Type
b -> do
(Type
c',Type
b') <- if Ident -> Bool
isWildIdent Ident
z
then SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr ((BindType
bt,Ident
x,Type
a)(BindType, Ident, Type) -> Context -> Context
forall a. a -> [a] -> [a]
:Context
g) Type
c Type
b
else do Type
b' <- Doc -> Check Type -> Check Type
forall a. Doc -> Check a -> Check a
checkIn ([Char] -> Doc
forall a. Pretty a => a -> Doc
pp [Char]
"abs") (Check Type -> Check Type) -> Check Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Context -> Type -> Check Type
substituteLType [(BindType
bt',Ident
z,Ident -> Type
Vr Ident
x)] Type
b
SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr ((BindType
bt,Ident
x,Type
a)(BindType, Ident, Type) -> Context -> Context
forall a. a -> [a] -> [a]
:Context
g) Type
c Type
b'
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type, Type) -> Check (Type, Type))
-> (Type, Type) -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ (BindType -> Ident -> Type -> Type
Abs BindType
bt Ident
x Type
c', BindType -> Ident -> Type -> Type -> Type
Prod BindType
bt' Ident
z Type
a Type
b')
Type
_ -> Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError (Doc -> Check (Type, Type)) -> Doc -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ [Char]
"function type expected instead of" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Type -> Doc
ppType Type
typ Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
[Char]
"\n ** Double-check that the type signature of the operation" Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
[Char]
"matches the number of arguments given to it.\n"
App Type
f Type
a -> do
Maybe (Type, Type)
over <- SourceGrammar
-> Context -> Maybe Type -> Type -> Check (Maybe (Type, Type))
getOverload SourceGrammar
gr Context
g (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
typ) Type
trm
case Maybe (Type, Type)
over of
Just (Type, Type)
trty -> (Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type, Type)
trty
Maybe (Type, Type)
_ -> do
(Type
trm',Type
ty') <- SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
trm
Type -> Check Type -> Check (Type, Type)
termWith Type
trm' (Check Type -> Check (Type, Type))
-> Check Type -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ SourceGrammar -> Context -> Type -> Type -> Type -> Check Type
checkEqLType SourceGrammar
gr Context
g Type
typ Type
ty' Type
trm'
AdHocOverload [Type]
ts -> do
Maybe (Type, Type)
over <- SourceGrammar
-> Context -> Maybe Type -> Type -> Check (Maybe (Type, Type))
getOverload SourceGrammar
gr Context
g Maybe Type
forall a. Maybe a
Nothing Type
trm
case Maybe (Type, Type)
over of
Just (Type, Type)
trty -> (Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type, Type)
trty
Maybe (Type, Type)
_ -> Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError ([Char]
"unresolved overloading of constants" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Qualified Integer
0 Type
trm)
Q (ModuleName, Ident)
_ -> do
Maybe (Type, Type)
over <- SourceGrammar
-> Context -> Maybe Type -> Type -> Check (Maybe (Type, Type))
getOverload SourceGrammar
gr Context
g (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
typ) Type
trm
case Maybe (Type, Type)
over of
Just (Type, Type)
trty -> (Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type, Type)
trty
Maybe (Type, Type)
_ -> do
(Type
trm',Type
ty') <- SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
trm
Type -> Check Type -> Check (Type, Type)
termWith Type
trm' (Check Type -> Check (Type, Type))
-> Check Type -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ SourceGrammar -> Context -> Type -> Type -> Type -> Check Type
checkEqLType SourceGrammar
gr Context
g Type
typ Type
ty' Type
trm'
T TInfo
_ [] ->
Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError ([Char]
"found empty table in type" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
typ)
T TInfo
_ [Case]
cs -> case Type
typ of
Table Type
arg Type
val -> do
case SourceGrammar -> Type -> Err [Type]
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> Type -> m [Type]
allParamValues SourceGrammar
gr Type
arg of
Ok [Type]
vs -> do
let ps0 :: [Patt]
ps0 = (Case -> Patt) -> [Case] -> [Patt]
forall a b. (a -> b) -> [a] -> [b]
map Case -> Patt
forall a b. (a, b) -> a
fst [Case]
cs
[Patt]
ps <- [Patt] -> [Type] -> Check [Patt]
forall (m :: * -> *). ErrorMonad m => [Patt] -> [Type] -> m [Patt]
testOvershadow [Patt]
ps0 [Type]
vs
if [Patt] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Patt]
ps
then () -> Check ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else Doc -> Check ()
checkWarn ([Char]
"patterns never reached:" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
Int -> Doc -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 ([Doc] -> Doc
forall a. Pretty a => [a] -> Doc
vcat ((Patt -> Doc) -> [Patt] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (TermPrintQual -> Integer -> Patt -> Doc
forall a. (Num a, Ord a) => TermPrintQual -> a -> Patt -> Doc
ppPatt TermPrintQual
Unqualified Integer
0) [Patt]
ps)))
Err [Type]
_ -> () -> Check ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
[Case]
cs' <- (Case -> Check Case) -> [Case] -> Check [Case]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> Type -> Case -> Check Case
checkCase Type
arg Type
val) [Case]
cs
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TInfo -> [Case] -> Type
T (Type -> TInfo
TTyped Type
arg) [Case]
cs', Type
typ)
Type
_ -> Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError (Doc -> Check (Type, Type)) -> Doc -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ [Char]
"table type expected for table instead of" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$ Int -> Doc -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 (Type -> Doc
ppType Type
typ)
V Type
arg0 [Type]
vs ->
case Type
typ of
Table Type
arg1 Type
val ->
do Type
arg' <- SourceGrammar -> Context -> Type -> Type -> Type -> Check Type
checkEqLType SourceGrammar
gr Context
g Type
arg0 Type
arg1 Type
trm
[Type]
vs1 <- SourceGrammar -> Type -> Check [Type]
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> Type -> m [Type]
allParamValues SourceGrammar
gr Type
arg1
if [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
vs1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
vs
then () -> Check ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else Doc -> Check ()
forall a. Doc -> Check a
checkError (Doc -> Check ()) -> Doc -> Check ()
forall a b. (a -> b) -> a -> b
$ [Char]
"wrong number of values in table" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
trm
[Type]
vs' <- ((Type, Type) -> Type) -> [(Type, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Type) -> Type
forall a b. (a, b) -> a
fst ([(Type, Type)] -> [Type]) -> Check [(Type, Type)] -> Check [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` [Check (Type, Type)] -> Check [(Type, Type)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
v Type
val|Type
v<-[Type]
vs]
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> [Type] -> Type
V Type
arg' [Type]
vs',Type
typ)
R [Assign]
r -> case Type
typ of
RecType [Labelling]
rr -> do
[Assign]
fsts <- (Labelling -> Check Assign) -> [Labelling] -> Check [Assign]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Assign] -> Labelling -> Check Assign
checkM [Assign]
r) [Labelling]
rr
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type, Type) -> Check (Type, Type))
-> (Type, Type) -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ ([Assign] -> Type
R [Assign]
fsts, Type
typ)
Type
_ -> Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError ([Char]
"record type expected in type checking instead of" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$ Int -> Doc -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 (TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
typ))
ExtR Type
r Type
s -> case Type
typ of
Type
_ | Type
typ Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
typeType -> do
Type
trm' <- SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr Context
g Type
trm
case Type
trm' of
RecType [Labelling]
_ -> Type -> Check Type -> Check (Type, Type)
termWith Type
trm' (Check Type -> Check (Type, Type))
-> Check Type -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
typeType
ExtR (Vr Ident
_) (RecType [Labelling]
_) -> Type -> Check Type -> Check (Type, Type)
termWith Type
trm' (Check Type -> Check (Type, Type))
-> Check Type -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
typeType
Type
_ -> Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError ([Char]
"invalid record type extension" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Int -> Doc -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 (TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
trm))
RecType [Labelling]
rr -> do
[Label]
ll2 <- case Type
s of
R [Assign]
ss -> [Label] -> Check [Label]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Label] -> Check [Label]) -> [Label] -> Check [Label]
forall a b. (a -> b) -> a -> b
$ (Assign -> Label) -> [Assign] -> [Label]
forall a b. (a -> b) -> [a] -> [b]
map Assign -> Label
forall a b. (a, b) -> a
fst [Assign]
ss
Type
_ -> do
(Type
s',Type
typ2) <- SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
s
case Type
typ2 of
RecType [Labelling]
ss -> [Label] -> Check [Label]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Label] -> Check [Label]) -> [Label] -> Check [Label]
forall a b. (a -> b) -> a -> b
$ (Labelling -> Label) -> [Labelling] -> [Label]
forall a b. (a -> b) -> [a] -> [b]
map Labelling -> Label
forall a b. (a, b) -> a
fst [Labelling]
ss
Type
_ -> Doc -> Check [Label]
forall a. Doc -> Check a
checkError ([Char]
"cannot get labels from" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$ Int -> Doc -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 (TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
typ2))
let ll1 :: [Label]
ll1 = [Label
l | (Label
l,Type
_) <- [Labelling]
rr, Label -> [Label] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Label
l [Label]
ll2]
let r1 :: Type
r1 = Type
r
(Type
r',Type
_) <- SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
r1 ([Labelling] -> Type
RecType [Labelling
field | field :: Labelling
field@(Label
l,Type
_) <- [Labelling]
rr, Label -> [Label] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Label
l [Label]
ll1])
(Type
s',Type
_) <- SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
s ([Labelling] -> Type
RecType [Labelling
field | field :: Labelling
field@(Label
l,Type
_) <- [Labelling]
rr, Label -> [Label] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Label
l [Label]
ll2])
let rec :: Type
rec = [Assign] -> Type
R ([(Label
l,(Maybe Type
forall a. Maybe a
Nothing,Type -> Label -> Type
P Type
r' Label
l)) | Label
l <- [Label]
ll1] [Assign] -> [Assign] -> [Assign]
forall a. [a] -> [a] -> [a]
++ [(Label
l,(Maybe Type
forall a. Maybe a
Nothing,Type -> Label -> Type
P Type
s' Label
l)) | Label
l <- [Label]
ll2])
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
rec, Type
typ)
ExtR Type
ty Type
ex -> do
Type
r' <- Context -> Type -> Type -> Check Type
justCheck Context
g Type
r Type
ty
Type
s' <- Context -> Type -> Type -> Check Type
justCheck Context
g Type
s Type
ex
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type, Type) -> Check (Type, Type))
-> (Type, Type) -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Type
ExtR Type
r' Type
s', Type
typ)
Type
_ -> Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError ([Char]
"record extension not meaningful for" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
typ)
FV [Type]
vs -> do
[(Type, Type)]
ttys <- (Type -> Check (Type, Type)) -> [Type] -> Check [(Type, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Type -> Type -> Check (Type, Type))
-> Type -> Type -> Check (Type, Type)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g) Type
typ) [Type]
vs
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> Type
FV (((Type, Type) -> Type) -> [(Type, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Type) -> Type
forall a b. (a, b) -> a
fst [(Type, Type)]
ttys), Type
typ)
S Type
tab Type
arg -> [Check (Type, Type)] -> Check (Type, Type)
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks [ do
(Type
tab',Type
ty) <- SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
tab
Type
ty' <- SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr Context
g Type
ty
case Type
ty' of
Table Type
p Type
t -> do
(Type
arg',Type
val) <- SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
arg Type
p
SourceGrammar -> Context -> Type -> Type -> Type -> Check Type
checkEqLType SourceGrammar
gr Context
g Type
typ Type
t Type
trm
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
S Type
tab' Type
arg', Type
t)
Type
_ -> Doc -> Check (Type, Type)
forall a. Doc -> Check a
checkError ([Char]
"table type expected for applied table instead of" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Type -> Doc
ppType Type
ty')
, do
(Type
arg',Type
ty) <- SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
arg
Type
ty' <- SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr Context
g Type
ty
(Type
tab',Type
_) <- SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
tab (Type -> Type -> Type
Table Type
ty' Type
typ)
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
S Type
tab' Type
arg', Type
typ)
]
Let (Ident
x,(Maybe Type
mty,Type
def)) Type
body -> case Maybe Type
mty of
Just Type
ty -> do
(Type
ty0,Type
_) <- SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
ty Type
typeType
(Type
def',Type
ty') <- SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
def Type
ty0
Type
body' <- Context -> Type -> Type -> Check Type
justCheck ((BindType
Explicit,Ident
x,Type
ty')(BindType, Ident, Type) -> Context -> Context
forall a. a -> [a] -> [a]
:Context
g) Type
body Type
typ
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Ident, (Maybe Type, Type)) -> Type -> Type
Let (Ident
x,(Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty',Type
def')) Type
body', Type
typ)
Maybe Type
_ -> do
(Type
def',Type
ty) <- SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
def
SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g ((Ident, (Maybe Type, Type)) -> Type -> Type
Let (Ident
x,(Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty,Type
def')) Type
body) Type
typ
ELin Ident
c Type
tr -> do
Type
tr1 <- Ident -> Type -> Check Type
forall (m :: * -> *). Monad m => Ident -> Type -> m Type
unlockRecord Ident
c Type
tr
SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
tr1 Type
typ
Type
_ -> do
(Type
trm',Type
ty') <- SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr Context
g Type
trm
Type -> Check Type -> Check (Type, Type)
termWith Type
trm' (Check Type -> Check (Type, Type))
-> Check Type -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ SourceGrammar -> Context -> Type -> Type -> Type -> Check Type
checkEqLType SourceGrammar
gr Context
g Type
typ Type
ty' Type
trm'
where
justCheck :: Context -> Type -> Type -> Check Type
justCheck Context
g Type
ty Type
te = SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
ty Type
te Check (Type, Type) -> ((Type, Type) -> Check Type) -> Check Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type)
-> ((Type, Type) -> Type) -> (Type, Type) -> Check Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, Type) -> Type
forall a b. (a, b) -> a
fst
checkM :: [Assign] -> Labelling -> Check Assign
checkM [Assign]
rms (Label
l,Type
ty) = case Label -> [Assign] -> Maybe (Maybe Type, Type)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Label
l [Assign]
rms of
Just (Just Type
ty0,Type
t) -> do
SourceGrammar -> Context -> Type -> Type -> Type -> Check Type
checkEqLType SourceGrammar
gr Context
g Type
ty Type
ty0 Type
t
(Type
t',Type
ty') <- SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
t Type
ty
Assign -> Check Assign
forall (m :: * -> *) a. Monad m => a -> m a
return (Label
l,(Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty',Type
t'))
Just (Maybe Type
_,Type
t) -> do
(Type
t',Type
ty') <- SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
t Type
ty
Assign -> Check Assign
forall (m :: * -> *) a. Monad m => a -> m a
return (Label
l,(Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty',Type
t'))
Maybe (Maybe Type, Type)
_ -> Doc -> Check Assign
forall a. Doc -> Check a
checkError (Doc -> Check Assign) -> Doc -> Check Assign
forall a b. (a -> b) -> a -> b
$
if Label -> Bool
isLockLabel Label
l
then let cat :: [Char]
cat = Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
drop Int
5 (Ident -> [Char]
showIdent (Label -> Ident
label2ident Label
l))
in TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 ([Assign] -> Type
R [Assign]
rms) Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Char]
"is not in the lincat of" Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Char]
cat Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<>
[Char]
"; try wrapping it with lin" Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Char]
cat
else [Char]
"cannot find value for label" [Char] -> Label -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Label
l Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Char]
"in" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 ([Assign] -> Type
R [Assign]
rms)
checkCase :: Type -> Type -> Case -> Check Case
checkCase Type
arg Type
val (Patt
p,Type
t) = do
Context
cont <- SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext SourceGrammar
gr Context
g Type
arg Patt
p
Type
t' <- Context -> Type -> Type -> Check Type
justCheck (Context -> Context
forall a. [a] -> [a]
reverse Context
cont Context -> Context -> Context
forall a. [a] -> [a] -> [a]
++ Context
g) Type
t Type
val
Case -> Check Case
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt
p,Type
t')
pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext SourceGrammar
env Context
g Type
typ Patt
p = case Patt
p of
PV Ident
x -> Context -> Check Context
forall (m :: * -> *) a. Monad m => a -> m a
return [(BindType
Explicit,Ident
x,Type
typ)]
PP (ModuleName
q,Ident
c) [Patt]
ps | ModuleName
q ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
/= ModuleName
cPredef -> do
Type
t <- SourceGrammar -> (ModuleName, Ident) -> Check Type
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> (ModuleName, Ident) -> m Type
lookupResType SourceGrammar
env (ModuleName
q,Ident
c)
let (Context
cont,Type
v) = Type -> (Context, Type)
typeFormCnc Type
t
Doc -> Bool -> Check ()
checkCond ([Char]
"wrong number of arguments for constructor in" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Patt -> Doc
forall a. (Num a, Ord a) => TermPrintQual -> a -> Patt -> Doc
ppPatt TermPrintQual
Unqualified Integer
0 Patt
p)
(Context -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Context
cont Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Patt] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Patt]
ps)
SourceGrammar -> Context -> Type -> Type -> Type -> Check Type
checkEqLType SourceGrammar
env Context
g Type
typ Type
v (Patt -> Type
patt2term Patt
p)
(((BindType, Ident, Type), Patt) -> Check Context)
-> [((BindType, Ident, Type), Patt)] -> Check [Context]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\((BindType
_,Ident
_,Type
ty),Patt
p) -> SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext SourceGrammar
env Context
g Type
ty Patt
p) (Context -> [Patt] -> [((BindType, Ident, Type), Patt)]
forall a b. [a] -> [b] -> [(a, b)]
zip Context
cont [Patt]
ps) Check [Context] -> ([Context] -> Check Context) -> Check Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Context -> Check Context
forall (m :: * -> *) a. Monad m => a -> m a
return (Context -> Check Context)
-> ([Context] -> Context) -> [Context] -> Check Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Context] -> Context
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
PR [(Label, Patt)]
r -> do
Type
typ' <- SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
env Context
g Type
typ
case Type
typ' of
RecType [Labelling]
t -> do
let pts :: [(Type, Patt)]
pts = [(Type
ty,Patt
tr) | (Label
l,Patt
tr) <- [(Label, Patt)]
r, Just Type
ty <- [Label -> [Labelling] -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Label
l [Labelling]
t]]
((Type, Patt) -> Check Context)
-> [(Type, Patt)] -> Check [Context]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Type -> Patt -> Check Context) -> (Type, Patt) -> Check Context
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext SourceGrammar
env Context
g)) [(Type, Patt)]
pts Check [Context] -> ([Context] -> Check Context) -> Check Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Context -> Check Context
forall (m :: * -> *) a. Monad m => a -> m a
return (Context -> Check Context)
-> ([Context] -> Context) -> [Context] -> Check Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Context] -> Context
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
Type
_ -> Doc -> Check Context
forall a. Doc -> Check a
checkError ([Char]
"record type expected for pattern instead of" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
typ')
PT Type
t Patt
p' -> do
SourceGrammar -> Context -> Type -> Type -> Type -> Check Type
checkEqLType SourceGrammar
env Context
g Type
typ Type
t (Patt -> Type
patt2term Patt
p')
SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext SourceGrammar
env Context
g Type
typ Patt
p'
PAs Ident
x Patt
p -> do
Context
g' <- SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext SourceGrammar
env Context
g Type
typ Patt
p
Context -> Check Context
forall (m :: * -> *) a. Monad m => a -> m a
return ((BindType
Explicit,Ident
x,Type
typ)(BindType, Ident, Type) -> Context -> Context
forall a. a -> [a] -> [a]
:Context
g')
PAlt Patt
p' Patt
q -> do
Context
g1 <- SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext SourceGrammar
env Context
g Type
typ Patt
p'
Context
g2 <- SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext SourceGrammar
env Context
g Type
typ Patt
q
let pts :: [Ident]
pts = [Ident] -> [Ident]
forall a. Eq a => [a] -> [a]
nub ([Ident
x | pt :: (BindType, Ident, Type)
pt@(BindType
_,Ident
x,Type
_) <- Context
g1, (BindType, Ident, Type) -> Context -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem (BindType, Ident, Type)
pt Context
g2] [Ident] -> [Ident] -> [Ident]
forall a. [a] -> [a] -> [a]
++ [Ident
x | pt :: (BindType, Ident, Type)
pt@(BindType
_,Ident
x,Type
_) <- Context
g2, (BindType, Ident, Type) -> Context -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem (BindType, Ident, Type)
pt Context
g1])
Doc -> Bool -> Check ()
checkCond
([Char]
"incompatible bindings of" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+>
[Ident] -> Doc
forall a. Pretty a => [a] -> Doc
fsep [Ident]
pts Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+>
[Char]
"in pattern alterantives" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Patt -> Doc
forall a. (Num a, Ord a) => TermPrintQual -> a -> Patt -> Doc
ppPatt TermPrintQual
Unqualified Integer
0 Patt
p) ([Ident] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ident]
pts)
Context -> Check Context
forall (m :: * -> *) a. Monad m => a -> m a
return Context
g1
PSeq Patt
p Patt
q -> do
Context
g1 <- SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext SourceGrammar
env Context
g Type
typ Patt
p
Context
g2 <- SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext SourceGrammar
env Context
g Type
typ Patt
q
Context -> Check Context
forall (m :: * -> *) a. Monad m => a -> m a
return (Context -> Check Context) -> Context -> Check Context
forall a b. (a -> b) -> a -> b
$ Context
g1 Context -> Context -> Context
forall a. [a] -> [a] -> [a]
++ Context
g2
PRep Patt
p' -> Type -> Patt -> Check Context
forall a. Type -> Patt -> Check [a]
noBind Type
typeStr Patt
p'
PNeg Patt
p' -> Type -> Patt -> Check Context
forall a. Type -> Patt -> Check [a]
noBind Type
typ Patt
p'
Patt
_ -> Context -> Check Context
forall (m :: * -> *) a. Monad m => a -> m a
return []
where
noBind :: Type -> Patt -> Check [a]
noBind Type
typ Patt
p' = do
Context
co <- SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext SourceGrammar
env Context
g Type
typ Patt
p'
if Bool -> Bool
not (Context -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Context
co)
then Doc -> Check ()
checkWarn ([Char]
"no variable bound inside pattern" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Patt -> Doc
forall a. (Num a, Ord a) => TermPrintQual -> a -> Patt -> Doc
ppPatt TermPrintQual
Unqualified Integer
0 Patt
p)
Check () -> Check [a] -> Check [a]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [a] -> Check [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
else [a] -> Check [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
checkEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check Type
checkEqLType :: SourceGrammar -> Context -> Type -> Type -> Type -> Check Type
checkEqLType SourceGrammar
gr Context
g Type
t Type
u Type
trm = do
(Bool
b,Type
t',Type
u',[Char]
s) <- SourceGrammar
-> Context
-> Type
-> Type
-> Type
-> Check (Bool, Type, Type, [Char])
checkIfEqLType SourceGrammar
gr Context
g Type
t Type
u Type
trm
case Bool
b of
Bool
True -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t'
Bool
False ->
let inferredType :: Doc
inferredType = TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Qualified Integer
0 Type
u
expectedType :: Doc
expectedType = TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Qualified Integer
0 Type
t
term :: Doc
term = TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
trm
funName :: Doc
funName = [Char] -> Doc
forall a. Pretty a => a -> Doc
pp ([Char] -> Doc) -> (Doc -> [Char]) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Char]] -> [Char]
forall a. [a] -> a
head ([[Char]] -> [Char]) -> (Doc -> [[Char]]) -> Doc -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[Char]]
words ([Char] -> [[Char]]) -> (Doc -> [Char]) -> Doc -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Doc -> [Char]
forall a. Pretty a => a -> [Char]
render (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
term
helpfulMsg :: Doc
helpfulMsg =
case (Doc -> Int
arrows Doc
inferredType, Doc -> Int
arrows Doc
expectedType) of
(Int
0,Int
0) -> [Char] -> Doc
forall a. Pretty a => a -> Doc
pp [Char]
""
(Int, Int)
_ -> [Char]
"\n **" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+>
if Doc
expectedType Doc -> Doc -> Bool
`isLessApplied` Doc
inferredType
then [Char]
"Maybe you gave too few arguments to" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Doc
funName
else [Char] -> Doc
forall a. Pretty a => a -> Doc
pp [Char]
"Double-check that type signature and number of arguments match."
in Doc -> Check Type
forall a. Doc -> Check a
checkError (Doc -> Check Type) -> Doc -> Check Type
forall a b. (a -> b) -> a -> b
$ [Char]
s [Char] -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Char]
"type of" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Doc
term Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
[Char]
"expected:" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Doc
expectedType Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
[Char]
"inferred:" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Doc
inferredType Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
Doc
helpfulMsg
where
arrows :: Doc -> Int
arrows :: Doc -> Int
arrows = [[Char]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([[Char]] -> Int) -> (Doc -> [[Char]]) -> Doc -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> Bool) -> [[Char]] -> [[Char]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
==[Char]
"->") ([[Char]] -> [[Char]]) -> (Doc -> [[Char]]) -> Doc -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[Char]]
words ([Char] -> [[Char]]) -> (Doc -> [Char]) -> Doc -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Char]
forall a. Pretty a => a -> [Char]
render
isLessApplied :: Doc -> Doc -> Bool
isLessApplied :: Doc -> Doc -> Bool
isLessApplied Doc
t Doc
u = Doc -> Int
arrows Doc
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Doc -> Int
arrows Doc
u
checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
checkIfEqLType :: SourceGrammar
-> Context
-> Type
-> Type
-> Type
-> Check (Bool, Type, Type, [Char])
checkIfEqLType SourceGrammar
gr Context
g Type
t Type
u Type
trm = do
Type
t' <- SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr Context
g Type
t
Type
u' <- SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr Context
g Type
u
case Type
t' Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
u' Bool -> Bool -> Bool
|| [(Ident, Ident)] -> Type -> Type -> Bool
alpha [] Type
t' Type
u' of
Bool
True -> (Bool, Type, Type, [Char]) -> Check (Bool, Type, Type, [Char])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True,Type
t',Type
u',[])
Bool
_ -> case [(Ident, Ident)] -> Type -> Type -> Err [Label]
missingLock [] Type
t' Type
u' of
Ok [Label]
lo -> do
Doc -> Check ()
checkWarn (Doc -> Check ()) -> Doc -> Check ()
forall a b. (a -> b) -> a -> b
$ [Char]
"missing lock field" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Label] -> Doc
forall a. Pretty a => [a] -> Doc
fsep [Label]
lo
(Bool, Type, Type, [Char]) -> Check (Bool, Type, Type, [Char])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True,Type
t',Type
u',[])
Bad [Char]
s -> (Bool, Type, Type, [Char]) -> Check (Bool, Type, Type, [Char])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False,Type
t',Type
u',[Char]
s)
where
alpha :: [(Ident, Ident)] -> Type -> Type -> Bool
alpha [(Ident, Ident)]
g Type
t Type
u = case (Type
t,Type
u) of
(Type
_,Type
u) | Type
u Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
typeError -> Bool
True
(Prod BindType
_ Ident
x Type
a Type
b, Prod BindType
_ Ident
y Type
c Type
d) -> [(Ident, Ident)] -> Type -> Type -> Bool
alpha [(Ident, Ident)]
g Type
c Type
a Bool -> Bool -> Bool
&& [(Ident, Ident)] -> Type -> Type -> Bool
alpha ((Ident
x,Ident
y)(Ident, Ident) -> [(Ident, Ident)] -> [(Ident, Ident)]
forall a. a -> [a] -> [a]
:[(Ident, Ident)]
g) Type
b Type
d
(RecType [Labelling]
rs, RecType [Labelling]
ts) -> (Labelling -> Bool) -> [Labelling] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ (Label
l,Type
a) ->
(Labelling -> Bool) -> [Labelling] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ (Label
k,Type
b) -> Label
l Label -> Label -> Bool
forall a. Eq a => a -> a -> Bool
== Label
k Bool -> Bool -> Bool
&& [(Ident, Ident)] -> Type -> Type -> Bool
alpha [(Ident, Ident)]
g Type
a Type
b) [Labelling]
ts) [Labelling]
rs
(ExtR Type
r Type
s, ExtR Type
r' Type
s') -> [(Ident, Ident)] -> Type -> Type -> Bool
alpha [(Ident, Ident)]
g Type
r Type
r' Bool -> Bool -> Bool
&& [(Ident, Ident)] -> Type -> Type -> Bool
alpha [(Ident, Ident)]
g Type
s Type
s'
(ExtR Type
r Type
s, Type
t) -> [(Ident, Ident)] -> Type -> Type -> Bool
alpha [(Ident, Ident)]
g Type
r Type
t Bool -> Bool -> Bool
|| [(Ident, Ident)] -> Type -> Type -> Bool
alpha [(Ident, Ident)]
g Type
s Type
t
(Type
t,Type
u) | Just Int
m <- Type -> Maybe Int
isTypeInts Type
t, Just Int
n <- Type -> Maybe Int
isTypeInts Type
u -> Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n
| Just Int
_ <- Type -> Maybe Int
isTypeInts Type
t, Type
u Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
typeInt -> Bool
True
| Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
typeInt, Just Int
_ <- Type -> Maybe Int
isTypeInts Type
u -> Bool
True
(Q (ModuleName
m,Ident
a), Q (ModuleName
n,Ident
b)) | Ident
a Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
b -> ModuleName -> [ModuleName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ModuleName
m (SourceGrammar -> ModuleName -> [ModuleName]
allExtendsPlus SourceGrammar
gr ModuleName
n)
Bool -> Bool -> Bool
|| ModuleName -> [ModuleName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ModuleName
n (SourceGrammar -> ModuleName -> [ModuleName]
allExtendsPlus SourceGrammar
gr ModuleName
m)
Bool -> Bool -> Bool
|| ModuleName
m ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
n
(QC (ModuleName
m,Ident
a), QC (ModuleName
n,Ident
b)) | Ident
a Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
b -> ModuleName -> [ModuleName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ModuleName
m (SourceGrammar -> ModuleName -> [ModuleName]
allExtendsPlus SourceGrammar
gr ModuleName
n)
Bool -> Bool -> Bool
|| ModuleName -> [ModuleName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ModuleName
n (SourceGrammar -> ModuleName -> [ModuleName]
allExtendsPlus SourceGrammar
gr ModuleName
m)
(QC (ModuleName
m,Ident
a), Q (ModuleName
n,Ident
b)) | Ident
a Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
b -> ModuleName -> [ModuleName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ModuleName
m (SourceGrammar -> ModuleName -> [ModuleName]
allExtendsPlus SourceGrammar
gr ModuleName
n)
Bool -> Bool -> Bool
|| ModuleName -> [ModuleName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ModuleName
n (SourceGrammar -> ModuleName -> [ModuleName]
allExtendsPlus SourceGrammar
gr ModuleName
m)
(Q (ModuleName
m,Ident
a), QC (ModuleName
n,Ident
b)) | Ident
a Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
b -> ModuleName -> [ModuleName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ModuleName
m (SourceGrammar -> ModuleName -> [ModuleName]
allExtendsPlus SourceGrammar
gr ModuleName
n)
Bool -> Bool -> Bool
|| ModuleName -> [ModuleName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ModuleName
n (SourceGrammar -> ModuleName -> [ModuleName]
allExtendsPlus SourceGrammar
gr ModuleName
m)
(Table Type
a Type
b, Table Type
c Type
d) -> [(Ident, Ident)] -> Type -> Type -> Bool
alpha [(Ident, Ident)]
g Type
c Type
a Bool -> Bool -> Bool
&& [(Ident, Ident)] -> Type -> Type -> Bool
alpha [(Ident, Ident)]
g Type
b Type
d
(Vr Ident
x, Vr Ident
y) -> Ident
x Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
y Bool -> Bool -> Bool
|| (Ident, Ident) -> [(Ident, Ident)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (Ident
x,Ident
y) [(Ident, Ident)]
g Bool -> Bool -> Bool
|| (Ident, Ident) -> [(Ident, Ident)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (Ident
y,Ident
x) [(Ident, Ident)]
g
(Type, Type)
_ -> Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
u
Bool -> Bool -> Bool
|| Type -> [Type] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Type
t [Type]
sTypes Bool -> Bool -> Bool
&& Type -> [Type] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Type
u [Type]
sTypes
Bool -> Bool -> Bool
|| (Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
typeType Bool -> Bool -> Bool
&& Type
u Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
typePType)
Bool -> Bool -> Bool
|| (Type
u Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
typeType Bool -> Bool -> Bool
&& Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
typePType)
missingLock :: [(Ident, Ident)] -> Type -> Type -> Err [Label]
missingLock [(Ident, Ident)]
g Type
t Type
u = case (Type
t,Type
u) of
(RecType [Labelling]
rs, RecType [Labelling]
ts) ->
let
ls :: [Label]
ls = [Label
l | (Label
l,Type
a) <- [Labelling]
rs,
Bool -> Bool
not ((Labelling -> Bool) -> [Labelling] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ (Label
k,Type
b) -> [(Ident, Ident)] -> Type -> Type -> Bool
alpha [(Ident, Ident)]
g Type
a Type
b Bool -> Bool -> Bool
&& Label
l Label -> Label -> Bool
forall a. Eq a => a -> a -> Bool
== Label
k) [Labelling]
ts)]
([Label]
locks,[Label]
others) = (Label -> Bool) -> [Label] -> ([Label], [Label])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Label -> Bool
isLockLabel [Label]
ls
in case [Label]
others of
Label
_:[Label]
_ -> [Char] -> Err [Label]
forall a. [Char] -> Err a
Bad ([Char] -> Err [Label]) -> [Char] -> Err [Label]
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Pretty a => a -> [Char]
render ([Char]
"missing record fields:" [Char] -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Doc] -> Doc
forall a. Pretty a => [a] -> Doc
fsep (Char -> [Label] -> [Doc]
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> [a2] -> [Doc]
punctuate Char
',' ([Label]
others)))
[Label]
_ -> [Label] -> Err [Label]
forall (m :: * -> *) a. Monad m => a -> m a
return [Label]
locks
(Prod BindType
_ Ident
x Type
a Type
b, Prod BindType
_ Ident
y Type
c Type
d) -> do
[Label]
ls1 <- [(Ident, Ident)] -> Type -> Type -> Err [Label]
missingLock [(Ident, Ident)]
g Type
c Type
a
[Label]
ls2 <- [(Ident, Ident)] -> Type -> Type -> Err [Label]
missingLock [(Ident, Ident)]
g Type
b Type
d
[Label] -> Err [Label]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Label] -> Err [Label]) -> [Label] -> Err [Label]
forall a b. (a -> b) -> a -> b
$ [Label]
ls1 [Label] -> [Label] -> [Label]
forall a. [a] -> [a] -> [a]
++ [Label]
ls2
(Type, Type)
_ -> [Char] -> Err [Label]
forall a. [Char] -> Err a
Bad [Char]
""
sTypes :: [Type]
sTypes = [Type
typeStr, Type
typeTok, Type
typeString]
substituteLType :: Context -> Type -> Check Type
substituteLType :: Context -> Type -> Check Type
substituteLType Context
g Type
t = case Type
t of
Vr Ident
x -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Type -> (Type -> Type) -> Maybe Type -> Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Type
t Type -> Type
forall a. a -> a
id (Maybe Type -> Type) -> Maybe Type -> Type
forall a b. (a -> b) -> a -> b
$ Ident -> [(Ident, Type)] -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ident
x [(Ident
x,Type
t) | (BindType
_,Ident
x,Type
t) <- Context
g]
Type
_ -> (Type -> Check Type) -> Type -> Check Type
forall (m :: * -> *). Monad m => (Type -> m Type) -> Type -> m Type
composOp (Context -> Type -> Check Type
substituteLType Context
g) Type
t
termWith :: Term -> Check Type -> Check (Term, Type)
termWith :: Type -> Check Type -> Check (Type, Type)
termWith Type
t Check Type
ct = do
Type
ty <- Check Type
ct
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t,Type
ty)
check2 :: (Term -> Check Term) -> (Term -> Term -> Term) ->
Term -> Term -> Type -> Check (Term,Type)
check2 :: (Type -> Check Type)
-> (Type -> Type -> Type)
-> Type
-> Type
-> Type
-> Check (Type, Type)
check2 Type -> Check Type
chk Type -> Type -> Type
con Type
a Type
b Type
t = do
Type
a' <- Type -> Check Type
chk Type
a
Type
b' <- Type -> Check Type
chk Type
b
(Type, Type) -> Check (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
con Type
a' Type
b', Type
t)
ppType :: Type -> Doc
ppType :: Type -> Doc
ppType Type
ty =
case Type
ty of
RecType [Labelling]
fs -> case (Label -> Bool) -> [Label] -> [Label]
forall a. (a -> Bool) -> [a] -> [a]
filter Label -> Bool
isLockLabel ([Label] -> [Label]) -> [Label] -> [Label]
forall a b. (a -> b) -> a -> b
$ (Labelling -> Label) -> [Labelling] -> [Label]
forall a b. (a -> b) -> [a] -> [b]
map Labelling -> Label
forall a b. (a, b) -> a
fst [Labelling]
fs of
[Label
lock] -> [Char] -> Doc
forall a. Pretty a => a -> Doc
pp (Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
drop Int
5 (Ident -> [Char]
showIdent (Label -> Ident
label2ident Label
lock)))
[Label]
_ -> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
ty
Prod BindType
_ Ident
x Type
a Type
b -> Type -> Doc
ppType Type
a Doc -> [Char] -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Char]
"->" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Type -> Doc
ppType Type
b
Type
_ -> TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Type
ty
checkLookup :: Ident -> Context -> Check Type
checkLookup :: Ident -> Context -> Check Type
checkLookup Ident
x Context
g =
case [Type
ty | (BindType
b,Ident
y,Type
ty) <- Context
g, Ident
x Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
y] of
[] -> Doc -> Check Type
forall a. Doc -> Check a
checkError ([Char]
"unknown variable" [Char] -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
x)
(Type
ty:[Type]
_) -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty