{-# LANGUAGE PatternGuards #-}
module GF.Compile.TypeCheck.Concrete( checkLType, inferLType, computeLType, ppType ) where
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint

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 ---- shouldn't be needed
      | Type -> Bool
isPredefConstant Type
ty     -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty ---- shouldn't be needed

    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' --- is this necessary to test?

    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 -- never needed to compute!

    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' ---- locking to be removed AR 20/6/2009

    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

-- the underlying algorithms

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  -- tries to guess: good in oper type inference
     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)
----       PInt k : _ -> return $ Ints $ max [i | PInt i <- pts']
       [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
--   return (trm, Table arg val) -- old, caused issue 68
     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))
          ----- removed irritating warning AR 24/5/2008
          ----- checkWarn ("token \"" ++ s ++
          -----              "\" converted to token list" ++ prt ss)
          (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 ---- typeTok

---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
   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

---     over <- getOverload gr g Nothing r
---     let r1 = maybe r fst over
     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) -- select types of later fields
         SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr Context
g Type
trm' Type
rt ---- return (trm', 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 --- check p partype!
     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
---     checkIfComplexVariantType trm ty
     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 ---- lookup c; remove lock AR 20/6/2009
     (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

   -- for record fields, which may be typed
   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 --- all isConstPatt ps
     PP (ModuleName, Ident)
_ [Patt]
ps -> Bool
True --- all isConstPatt ps
     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

-- type inference: Nothing, type checking: Just t
-- the latter permits matching with value type
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     --- the function name f is only used in error messages
       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
_ = [] --- constructors QC

   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])

     -- to avoid strange error msg e.g. in case of unmatch record extension, show whole types if needed AR 28/1/2013
     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)

----- unsafely exclude irritating warning AR 24/5/2008
-----           checkWarn $ "overloading of" +++ prt f +++
-----             "resolved by excluding partial applications:" ++++
-----             unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]

--- now forgiving ambiguity with a warning AR 1/2/2014
--  This gives ad hoc overloading the same behaviour as the choice of the first match in renaming did before.
--  But it also gives a chance to ambiguous overloadings that were banned before.
         ([(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
<+>
                  ----     "with argument types" <+> hsep (map (ppTerm Qualified 0) tys) $$
                           [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
   ---- TODO: accept subtypes
   ---- TODO: use a trie
   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 () -- happens with variable types
        [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 --- why needed? because inference may be too difficult
       RecType [Labelling]
rr -> do
       --let (ls,_) = unzip rr        -- labels of expected type
         [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   -- check that they are found in the record
         (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)       -- normalize record

       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
                                      -- ext t = t ** ...
           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]

---         over <- getOverload gr g Nothing r --- this would solve #66 but fail ParadigmsAra. AR 6/7/2020
---         let r1 = maybe r fst over
         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) --- is this all? it assumes the same division in trm and 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
---      checkIfComplexVariantType trm typ
      (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) --- 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  -- tries to infer type of local constant
        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
{-
   recParts rr t = (RecType rr1,RecType rr2) where
     (rr1,rr2) = partition (flip elem (map fst t) . fst) rr
-}
   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 ---- why this /=? AR 6/1/2006
    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]]
        ----- checkWarn $ prt p ++++ show pts ----- debug
        ((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 -- must be g1 == g2
  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 [] ---- check types!
 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]
"" -- None of the types is a function
              (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
$$ -- ppqType t u $$
                            [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
$$ -- ppqType u t
                            Doc
helpfulMsg
  where
    -- count the number of arrows in the prettyprinted term
    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

    -- If prettyprinted type t has fewer arrows then prettyprinted type u,
    -- then t is "less applied", and we can print out more helpful error msg.
    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',[])
    -- forgive missing lock fields by only generating a warning.
    --- better: use a flag to forgive? (AR 31/1/2006)
    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

   -- check that u is a subtype of t
   --- quick hack version of TC.eqVal
   alpha :: [(Ident, Ident)] -> Type -> Type -> Bool
alpha [(Ident, Ident)]
g Type
t Type
u = case (Type
t,Type
u) of

     -- error (the empty type!) is subtype of any other type
     (Type
_,Type
u) | Type
u Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
typeError -> Bool
True

     -- contravariance
     (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

     -- record subtyping
     (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

     -- the following say that Ints n is a subset of Int and of Ints m >= n
     -- But why does it also allow Int as a subtype of Ints m? /TH 2014-04-04
     (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 ---- check size!
           | Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
typeInt,           Just Int
_ <- Type -> Maybe Int
isTypeInts Type
u -> Bool
True ---- why this ???? AR 11/12/2005

     ---- this should be made in Rename
     (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 --- for Predef
     (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)

     -- contravariance
     (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
     --- the following should be one-way coercions only. AR 4/1/2001
                                  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
     -- contravariance
     (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]

-- auxiliaries

-- | light-weight substitution for dep. types
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)

-- | compositional check\/infer of binary operations
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)

-- printing a type with a lock field lock_C as C
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
{-
ppqType :: Type -> Type -> Doc
ppqType t u = case (ppType t, ppType u) of
  (pt,pu) | render pt == render pu -> ppTerm Qualified 0 t
  (pt,_) -> pt
-}
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