{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Infer
( checkE
, checkSigB
, inferModule
, inferBinds
, inferDs
)
where
import Cryptol.ModuleSystem.Name (asPrim,lookupPrimDecl,nameLoc)
import Cryptol.Parser.Position
import qualified Cryptol.Parser.AST as P
import qualified Cryptol.ModuleSystem.Exports as P
import Cryptol.TypeCheck.AST hiding (tSub,tMul,tExp)
import Cryptol.TypeCheck.Monad
import Cryptol.TypeCheck.Error
import Cryptol.TypeCheck.Solve
import Cryptol.TypeCheck.SimpType(tMul)
import Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
checkPropSyn,checkNewtype,
checkParameterType,
checkPrimType,
checkParameterConstraints)
import Cryptol.TypeCheck.Instantiate
import Cryptol.TypeCheck.Depends
import Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),isEmptySubst)
import Cryptol.TypeCheck.Solver.InfNat(genLog)
import Cryptol.Utils.Ident
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.PP
import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Set as Set
import Data.List(foldl',sortBy)
import Data.Either(partitionEithers)
import Data.Maybe(mapMaybe,isJust, fromMaybe)
import Data.List(partition,find)
import Data.Graph(SCC(..))
import Data.Traversable(forM)
import Control.Monad(zipWithM,unless,foldM)
inferModule :: P.Module Name -> InferM Module
inferModule :: Module Name -> InferM Module
inferModule m :: Module Name
m =
[TopDecl Name] -> ([DeclGroup] -> InferM Module) -> InferM Module
forall d a.
FromDecl d =>
[d] -> ([DeclGroup] -> InferM a) -> InferM a
inferDs (Module Name -> [TopDecl Name]
forall name. Module name -> [TopDecl name]
P.mDecls Module Name
m) (([DeclGroup] -> InferM Module) -> InferM Module)
-> ([DeclGroup] -> InferM Module) -> InferM Module
forall a b. (a -> b) -> a -> b
$ \ds1 :: [DeclGroup]
ds1 ->
do InferM ()
proveModuleTopLevel
Map Name (DefLoc, TySyn)
ts <- InferM (Map Name (DefLoc, TySyn))
getTSyns
Map Name (DefLoc, Newtype)
nts <- InferM (Map Name (DefLoc, Newtype))
getNewtypes
Map Name (DefLoc, AbstractType)
ats <- InferM (Map Name (DefLoc, AbstractType))
getAbstractTypes
Map Name ModTParam
pTs <- InferM (Map Name ModTParam)
getParamTypes
[Located Prop]
pCs <- InferM [Located Prop]
getParamConstraints
Map Name ModVParam
pFuns <- InferM (Map Name ModVParam)
getParamFuns
Module -> InferM Module
forall (m :: * -> *) a. Monad m => a -> m a
return $WModule :: ModName
-> ExportSpec Name
-> [Import]
-> Map Name TySyn
-> Map Name Newtype
-> Map Name AbstractType
-> Map Name ModTParam
-> [Located Prop]
-> Map Name ModVParam
-> [DeclGroup]
-> Module
Module { mName :: ModName
mName = Located ModName -> ModName
forall a. Located a -> a
thing (Module Name -> Located ModName
forall name. Module name -> Located ModName
P.mName Module Name
m)
, mExports :: ExportSpec Name
mExports = Module Name -> ExportSpec Name
forall name. Ord name => Module name -> ExportSpec name
P.modExports Module Name
m
, mImports :: [Import]
mImports = (Located Import -> Import) -> [Located Import] -> [Import]
forall a b. (a -> b) -> [a] -> [b]
map Located Import -> Import
forall a. Located a -> a
thing (Module Name -> [Located Import]
forall name. Module name -> [Located Import]
P.mImports Module Name
m)
, mTySyns :: Map Name TySyn
mTySyns = ((DefLoc, TySyn) -> Maybe TySyn)
-> Map Name (DefLoc, TySyn) -> Map Name TySyn
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe (DefLoc, TySyn) -> Maybe TySyn
forall a. (DefLoc, a) -> Maybe a
onlyLocal Map Name (DefLoc, TySyn)
ts
, mNewtypes :: Map Name Newtype
mNewtypes = ((DefLoc, Newtype) -> Maybe Newtype)
-> Map Name (DefLoc, Newtype) -> Map Name Newtype
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe (DefLoc, Newtype) -> Maybe Newtype
forall a. (DefLoc, a) -> Maybe a
onlyLocal Map Name (DefLoc, Newtype)
nts
, mPrimTypes :: Map Name AbstractType
mPrimTypes = ((DefLoc, AbstractType) -> Maybe AbstractType)
-> Map Name (DefLoc, AbstractType) -> Map Name AbstractType
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe (DefLoc, AbstractType) -> Maybe AbstractType
forall a. (DefLoc, a) -> Maybe a
onlyLocal Map Name (DefLoc, AbstractType)
ats
, mParamTypes :: Map Name ModTParam
mParamTypes = Map Name ModTParam
pTs
, mParamConstraints :: [Located Prop]
mParamConstraints = [Located Prop]
pCs
, mParamFuns :: Map Name ModVParam
mParamFuns = Map Name ModVParam
pFuns
, mDecls :: [DeclGroup]
mDecls = [DeclGroup]
ds1
}
where
onlyLocal :: (DefLoc, a) -> Maybe a
onlyLocal (IsLocal, x :: a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
onlyLocal (IsExternal, _) = Maybe a
forall a. Maybe a
Nothing
mkPrim :: String -> InferM (P.Expr Name)
mkPrim :: String -> InferM (Expr Name)
mkPrim str :: String
str =
do Name
nm <- String -> InferM Name
mkPrim' String
str
Expr Name -> InferM (Expr Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Expr Name
forall n. n -> Expr n
P.EVar Name
nm)
mkPrim' :: String -> InferM Name
mkPrim' :: String -> InferM Name
mkPrim' str :: String
str =
do PrimMap
prims <- InferM PrimMap
getPrimMap
Name -> InferM Name
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> PrimMap -> Name
lookupPrimDecl (String -> Ident
packIdent String
str) PrimMap
prims)
desugarLiteral :: Bool -> P.Literal -> InferM (P.Expr Name)
desugarLiteral :: Bool -> Literal -> InferM (Expr Name)
desugarLiteral fixDec :: Bool
fixDec lit :: Literal
lit =
do Range
l <- InferM Range
curRange
Expr Name
numberPrim <- String -> InferM (Expr Name)
mkPrim "number"
let named :: (String, Type name) -> TypeInst name
named (x :: String
x,y :: Type name
y) = Named (Type name) -> TypeInst name
forall name. Named (Type name) -> TypeInst name
P.NamedInst
Named :: forall a. Located Ident -> a -> Named a
P.Named { name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type name
value = Type name
y }
number :: [(String, Type Name)] -> Expr Name
number fs :: [(String, Type Name)]
fs = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
numberPrim (((String, Type Name) -> TypeInst Name)
-> [(String, Type Name)] -> [TypeInst Name]
forall a b. (a -> b) -> [a] -> [b]
map (String, Type Name) -> TypeInst Name
forall name. (String, Type name) -> TypeInst name
named [(String, Type Name)]
fs)
tBits :: Integer -> Type n
tBits n :: Integer
n = Type n -> Type n -> Type n
forall n. Type n -> Type n -> Type n
P.TSeq (Integer -> Type n
forall n. Integer -> Type n
P.TNum Integer
n) Type n
forall n. Type n
P.TBit
Expr Name -> InferM (Expr Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr Name -> InferM (Expr Name))
-> Expr Name -> InferM (Expr Name)
forall a b. (a -> b) -> a -> b
$ case Literal
lit of
P.ECNum num :: Integer
num info :: NumInfo
info ->
[(String, Type Name)] -> Expr Name
number ([(String, Type Name)] -> Expr Name)
-> [(String, Type Name)] -> Expr Name
forall a b. (a -> b) -> a -> b
$ [ ("val", Integer -> Type Name
forall n. Integer -> Type n
P.TNum Integer
num) ] [(String, Type Name)]
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. [a] -> [a] -> [a]
++ case NumInfo
info of
P.BinLit n :: Int
n -> [ ("rep", Integer -> Type Name
forall n. Integer -> Type n
tBits (1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)) ]
P.OctLit n :: Int
n -> [ ("rep", Integer -> Type Name
forall n. Integer -> Type n
tBits (3 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)) ]
P.HexLit n :: Int
n -> [ ("rep", Integer -> Type Name
forall n. Integer -> Type n
tBits (4 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)) ]
P.CharLit -> [ ("rep", Integer -> Type Name
forall n. Integer -> Type n
tBits (8 :: Integer)) ]
P.DecLit
| Bool
fixDec -> if Integer
num Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0
then [ ("rep", Integer -> Type Name
forall n. Integer -> Type n
tBits 0)]
else case Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
num 2 of
Just (x :: Integer
x,_) -> [ ("rep", Integer -> Type Name
forall n. Integer -> Type n
tBits (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1)) ]
_ -> []
| Bool
otherwise -> [ ]
P.PolyLit _n :: Int
_n -> [ ("rep", Type Name -> Type Name -> Type Name
forall n. Type n -> Type n -> Type n
P.TSeq Type Name
forall n. Type n
P.TWild Type Name
forall n. Type n
P.TBit) ]
P.ECString s :: String
s ->
Expr Name -> Type Name -> Expr Name
forall n. Expr n -> Type n -> Expr n
P.ETyped ([Expr Name] -> Expr Name
forall n. [Expr n] -> Expr n
P.EList [ Literal -> Expr Name
forall n. Literal -> Expr n
P.ELit (Integer -> NumInfo -> Literal
P.ECNum (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c))
NumInfo
P.CharLit) | Char
c <- String
s ])
(Type Name -> Type Name -> Type Name
forall n. Type n -> Type n -> Type n
P.TSeq Type Name
forall n. Type n
P.TWild (Type Name -> Type Name -> Type Name
forall n. Type n -> Type n -> Type n
P.TSeq (Integer -> Type Name
forall n. Integer -> Type n
P.TNum 8) Type Name
forall n. Type n
P.TBit))
appTys :: P.Expr Name -> [TypeArg] -> Type -> InferM Expr
appTys :: Expr Name -> [TypeArg] -> Prop -> InferM Expr
appTys expr :: Expr Name
expr ts :: [TypeArg]
ts tGoal :: Prop
tGoal =
case Expr Name
expr of
P.EVar x :: Name
x ->
do VarType
res <- Name -> InferM VarType
lookupVar Name
x
(e' :: Expr
e',t :: Prop
t) <- case VarType
res of
ExtVar s :: Schema
s -> Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Prop)
instantiateWith Name
x (Name -> Expr
EVar Name
x) Schema
s [TypeArg]
ts
CurSCC e :: Expr
e t :: Prop
t -> do [TypeArg] -> InferM ()
checkNoParams [TypeArg]
ts
(Expr, Prop) -> InferM (Expr, Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e,Prop
t)
Prop -> Prop -> InferM ()
checkHasType Prop
t Prop
tGoal
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'
P.ELit l :: Literal
l -> do Expr Name
e <- Bool -> Literal -> InferM (Expr Name)
desugarLiteral Bool
False Literal
l
Expr Name -> [TypeArg] -> Prop -> InferM Expr
appTys Expr Name
e [TypeArg]
ts Prop
tGoal
P.EAppT e :: Expr Name
e fs :: [TypeInst Name]
fs -> Expr Name -> [TypeArg] -> Prop -> InferM Expr
appTys Expr Name
e ((TypeInst Name -> TypeArg) -> [TypeInst Name] -> [TypeArg]
forall a b. (a -> b) -> [a] -> [b]
map TypeInst Name -> TypeArg
uncheckedTypeArg [TypeInst Name]
fs [TypeArg] -> [TypeArg] -> [TypeArg]
forall a. [a] -> [a] -> [a]
++ [TypeArg]
ts) Prop
tGoal
P.EWhere e :: Expr Name
e ds :: [Decl Name]
ds ->
[Decl Name] -> ([DeclGroup] -> InferM Expr) -> InferM Expr
forall d a.
FromDecl d =>
[d] -> ([DeclGroup] -> InferM a) -> InferM a
inferDs [Decl Name]
ds (([DeclGroup] -> InferM Expr) -> InferM Expr)
-> ([DeclGroup] -> InferM Expr) -> InferM Expr
forall a b. (a -> b) -> a -> b
$ \ds1 :: [DeclGroup]
ds1 -> do Expr
e1 <- Expr Name -> [TypeArg] -> Prop -> InferM Expr
appTys Expr Name
e [TypeArg]
ts Prop
tGoal
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> [DeclGroup] -> Expr
EWhere Expr
e1 [DeclGroup]
ds1)
P.ELocated e :: Expr Name
e r :: Range
r ->
Range -> InferM Expr -> InferM Expr
forall a. Range -> InferM a -> InferM a
inRange Range
r (Expr Name -> [TypeArg] -> Prop -> InferM Expr
appTys Expr Name
e [TypeArg]
ts Prop
tGoal)
P.ENeg {} -> InferM Expr
mono
P.EComplement {} -> InferM Expr
mono
P.EGenerate {} -> InferM Expr
mono
P.ETuple {} -> InferM Expr
mono
P.ERecord {} -> InferM Expr
mono
P.EUpd {} -> InferM Expr
mono
P.ESel {} -> InferM Expr
mono
P.EList {} -> InferM Expr
mono
P.EFromTo {} -> InferM Expr
mono
P.EInfFrom {} -> InferM Expr
mono
P.EComp {} -> InferM Expr
mono
P.EApp {} -> InferM Expr
mono
P.EIf {} -> InferM Expr
mono
P.ETyped {} -> InferM Expr
mono
P.ETypeVal {} -> InferM Expr
mono
P.EFun {} -> InferM Expr
mono
P.ESplit {} -> InferM Expr
mono
P.EParens e :: Expr Name
e -> Expr Name -> [TypeArg] -> Prop -> InferM Expr
appTys Expr Name
e [TypeArg]
ts Prop
tGoal
P.EInfix a :: Expr Name
a op :: Located Name
op _ b :: Expr Name
b -> Expr Name -> [TypeArg] -> Prop -> InferM Expr
appTys (Name -> Expr Name
forall n. n -> Expr n
P.EVar (Located Name -> Name
forall a. Located a -> a
thing Located Name
op) Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
a Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
b) [TypeArg]
ts Prop
tGoal
where mono :: InferM Expr
mono = do Expr
e' <- Expr Name -> Prop -> InferM Expr
checkE Expr Name
expr Prop
tGoal
[TypeArg] -> InferM ()
checkNoParams [TypeArg]
ts
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'
checkNoParams :: [TypeArg] -> InferM ()
checkNoParams :: [TypeArg] -> InferM ()
checkNoParams ts :: [TypeArg]
ts =
case [TypeArg]
pos of
p :: TypeArg
p : _ -> do Range
r <- case TypeArg -> MaybeCheckedType
tyArgType TypeArg
p of
Unchecked t :: Type Name
t | Just r :: Range
r <- Type Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Type Name
t -> Range -> InferM Range
forall (f :: * -> *) a. Applicative f => a -> f a
pure Range
r
_ -> InferM Range
curRange
Range -> InferM () -> InferM ()
forall a. Range -> InferM a -> InferM a
inRange Range
r (Error -> InferM ()
recordError Error
TooManyPositionalTypeParams)
_ -> (TypeArg -> InferM ()) -> [TypeArg] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TypeArg -> InferM ()
badNamed [TypeArg]
named
where
badNamed :: TypeArg -> InferM ()
badNamed l :: TypeArg
l =
case TypeArg -> Maybe (Located Ident)
tyArgName TypeArg
l of
Just i :: Located Ident
i -> Error -> InferM ()
recordError (Located Ident -> Error
UndefinedTypeParameter Located Ident
i)
Nothing -> () -> InferM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(named :: [TypeArg]
named,pos :: [TypeArg]
pos) = (TypeArg -> Bool) -> [TypeArg] -> ([TypeArg], [TypeArg])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Maybe (Located Ident) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Located Ident) -> Bool)
-> (TypeArg -> Maybe (Located Ident)) -> TypeArg -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeArg -> Maybe (Located Ident)
tyArgName) [TypeArg]
ts
checkTypeOfKind :: P.Type Name -> Kind -> InferM Type
checkTypeOfKind :: Type Name -> Kind -> InferM Prop
checkTypeOfKind ty :: Type Name
ty k :: Kind
k = Type Name -> Maybe Kind -> InferM Prop
checkType Type Name
ty (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
k)
checkE :: P.Expr Name -> Type -> InferM Expr
checkE :: Expr Name -> Prop -> InferM Expr
checkE expr :: Expr Name
expr tGoal :: Prop
tGoal =
case Expr Name
expr of
P.EVar x :: Name
x ->
do VarType
res <- Name -> InferM VarType
lookupVar Name
x
(e' :: Expr
e',t :: Prop
t) <- case VarType
res of
ExtVar s :: Schema
s -> Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Prop)
instantiateWith Name
x (Name -> Expr
EVar Name
x) Schema
s []
CurSCC e :: Expr
e t :: Prop
t -> (Expr, Prop) -> InferM (Expr, Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Prop
t)
Prop -> Prop -> InferM ()
checkHasType Prop
t Prop
tGoal
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'
P.ENeg e :: Expr Name
e ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim "negate"
Expr Name -> Prop -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e) Prop
tGoal
P.EComplement e :: Expr Name
e ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim "complement"
Expr Name -> Prop -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e) Prop
tGoal
P.EGenerate e :: Expr Name
e ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim "generate"
Expr Name -> Prop -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e) Prop
tGoal
P.ELit l :: Literal
l@(P.ECNum _ P.DecLit) ->
do Expr Name
e <- Bool -> Literal -> InferM (Expr Name)
desugarLiteral Bool
False Literal
l
Range
loc <- InferM Range
curRange
let arg :: TypeArg
arg = TypeArg :: Maybe (Located Ident) -> MaybeCheckedType -> TypeArg
TypeArg { tyArgName :: Maybe (Located Ident)
tyArgName = Located Ident -> Maybe (Located Ident)
forall a. a -> Maybe a
Just (Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
loc (String -> Ident
packIdent "rep"))
, tyArgType :: MaybeCheckedType
tyArgType = Prop -> MaybeCheckedType
Checked Prop
tGoal
}
Expr Name -> [TypeArg] -> Prop -> InferM Expr
appTys Expr Name
e [TypeArg
arg] Prop
tGoal
P.ELit l :: Literal
l -> (Expr Name -> Prop -> InferM Expr
`checkE` Prop
tGoal) (Expr Name -> InferM Expr) -> InferM (Expr Name) -> InferM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Bool -> Literal -> InferM (Expr Name)
desugarLiteral Bool
False Literal
l
P.ETuple es :: [Expr Name]
es ->
do [Prop]
etys <- Int -> Prop -> InferM [Prop]
expectTuple ([Expr Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr Name]
es) Prop
tGoal
[Expr]
es' <- (Expr Name -> Prop -> InferM Expr)
-> [Expr Name] -> [Prop] -> InferM [Expr]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Expr Name -> Prop -> InferM Expr
checkE [Expr Name]
es [Prop]
etys
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Expr
ETuple [Expr]
es')
P.ERecord fs :: [Named (Expr Name)]
fs ->
do (ns :: [Ident]
ns,es :: [Expr Name]
es,ts :: [Prop]
ts) <- [(Ident, Expr Name, Prop)] -> ([Ident], [Expr Name], [Prop])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 ([(Ident, Expr Name, Prop)] -> ([Ident], [Expr Name], [Prop]))
-> InferM [(Ident, Expr Name, Prop)]
-> InferM ([Ident], [Expr Name], [Prop])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` [Named (Expr Name)] -> Prop -> InferM [(Ident, Expr Name, Prop)]
forall a. [Named a] -> Prop -> InferM [(Ident, a, Prop)]
expectRec [Named (Expr Name)]
fs Prop
tGoal
[Expr]
es' <- (Expr Name -> Prop -> InferM Expr)
-> [Expr Name] -> [Prop] -> InferM [Expr]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Expr Name -> Prop -> InferM Expr
checkE [Expr Name]
es [Prop]
ts
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Ident, Expr)] -> Expr
ERec ([Ident] -> [Expr] -> [(Ident, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
ns [Expr]
es'))
P.EUpd x :: Maybe (Expr Name)
x fs :: [UpdField Name]
fs -> Maybe (Expr Name) -> [UpdField Name] -> Prop -> InferM Expr
checkRecUpd Maybe (Expr Name)
x [UpdField Name]
fs Prop
tGoal
P.ESel e :: Expr Name
e l :: Selector
l ->
do Prop
t <- TVarSource -> Kind -> InferM Prop
newType (Selector -> TVarSource
selSrc Selector
l) Kind
KType
Expr
e' <- Expr Name -> Prop -> InferM Expr
checkE Expr Name
e Prop
t
HasGoalSln
f <- Selector -> Prop -> Prop -> InferM HasGoalSln
newHasGoal Selector
l Prop
t Prop
tGoal
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (HasGoalSln -> Expr -> Expr
hasDoSelect HasGoalSln
f Expr
e')
P.EList [] ->
do (len :: Prop
len,a :: Prop
a) <- Prop -> InferM (Prop, Prop)
expectSeq Prop
tGoal
Int -> Prop -> InferM ()
expectFin 0 Prop
len
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Prop -> Expr
EList [] Prop
a)
P.EList es :: [Expr Name]
es ->
do (len :: Prop
len,a :: Prop
a) <- Prop -> InferM (Prop, Prop)
expectSeq Prop
tGoal
Int -> Prop -> InferM ()
expectFin ([Expr Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr Name]
es) Prop
len
[Expr]
es' <- (Expr Name -> InferM Expr) -> [Expr Name] -> InferM [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Expr Name -> Prop -> InferM Expr
`checkE` Prop
a) [Expr Name]
es
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Prop -> Expr
EList [Expr]
es' Prop
a)
P.EFromTo t1 :: Type Name
t1 mbt2 :: Maybe (Type Name)
mbt2 t3 :: Type Name
t3 mety :: Maybe (Type Name)
mety ->
do Range
l <- InferM Range
curRange
let fs0 :: [(String, Type Name)]
fs0 =
case Maybe (Type Name)
mety of
Just ety :: Type Name
ety -> [("a", Type Name
ety)]
Nothing -> []
let (c :: String
c,fs :: [(String, Type Name)]
fs) =
case Maybe (Type Name)
mbt2 of
Nothing ->
("fromTo", ("last", Type Name
t3) (String, Type Name)
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. a -> [a] -> [a]
: [(String, Type Name)]
fs0)
Just t2 :: Type Name
t2 ->
("fromThenTo", ("next",Type Name
t2) (String, Type Name)
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. a -> [a] -> [a]
: ("last",Type Name
t3) (String, Type Name)
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. a -> [a] -> [a]
: [(String, Type Name)]
fs0)
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
c
let e' :: Expr Name
e' = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[ Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst Named :: forall a. Located Ident -> a -> Named a
P.Named { name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
| (x :: String
x,y :: Type Name
y) <- ("first",Type Name
t1) (String, Type Name)
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. a -> [a] -> [a]
: [(String, Type Name)]
fs
]
Expr Name -> Prop -> InferM Expr
checkE Expr Name
e' Prop
tGoal
P.EInfFrom e1 :: Expr Name
e1 Nothing ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim "infFrom"
Expr Name -> Prop -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e1) Prop
tGoal
P.EInfFrom e1 :: Expr Name
e1 (Just e2 :: Expr Name
e2) ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim "infFromThen"
Expr Name -> Prop -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e1) Expr Name
e2) Prop
tGoal
P.EComp e :: Expr Name
e mss :: [[Match Name]]
mss ->
do (mss' :: [[Match]]
mss', dss :: [Map Name (Located Prop)]
dss, ts :: [Prop]
ts) <- [([Match], Map Name (Located Prop), Prop)]
-> ([[Match]], [Map Name (Located Prop)], [Prop])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 ([([Match], Map Name (Located Prop), Prop)]
-> ([[Match]], [Map Name (Located Prop)], [Prop]))
-> InferM [([Match], Map Name (Located Prop), Prop)]
-> InferM ([[Match]], [Map Name (Located Prop)], [Prop])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Int
-> [Match Name] -> InferM ([Match], Map Name (Located Prop), Prop))
-> [Int]
-> [[Match Name]]
-> InferM [([Match], Map Name (Located Prop), Prop)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Int
-> [Match Name] -> InferM ([Match], Map Name (Located Prop), Prop)
inferCArm [ 1 .. ] [[Match Name]]
mss
(len :: Prop
len,a :: Prop
a) <- Prop -> InferM (Prop, Prop)
expectSeq Prop
tGoal
ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtComprehension ([Prop] -> InferM ()) -> InferM [Prop] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Prop -> Prop -> InferM [Prop]
unify Prop
len (Prop -> InferM [Prop]) -> InferM Prop -> InferM [Prop]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Prop] -> InferM Prop
smallest [Prop]
ts
Map Name (Located Prop)
ds <- [Map Name (Located Prop)] -> InferM (Map Name (Located Prop))
forall a. [Map Name (Located a)] -> InferM (Map Name (Located a))
combineMaps [Map Name (Located Prop)]
dss
Expr
e' <- Map Name (Located Prop) -> InferM Expr -> InferM Expr
forall a. Map Name (Located Prop) -> InferM a -> InferM a
withMonoTypes Map Name (Located Prop)
ds (Expr Name -> Prop -> InferM Expr
checkE Expr Name
e Prop
a)
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop -> Prop -> Expr -> [[Match]] -> Expr
EComp Prop
len Prop
a Expr
e' [[Match]]
mss')
P.EAppT e :: Expr Name
e fs :: [TypeInst Name]
fs -> Expr Name -> [TypeArg] -> Prop -> InferM Expr
appTys Expr Name
e ((TypeInst Name -> TypeArg) -> [TypeInst Name] -> [TypeArg]
forall a b. (a -> b) -> [a] -> [b]
map TypeInst Name -> TypeArg
uncheckedTypeArg [TypeInst Name]
fs) Prop
tGoal
P.EApp fun :: Expr Name
fun@(Expr Name -> Expr Name
forall t. AddLoc t => t -> t
dropLoc -> P.EApp (Expr Name -> Expr Name
forall t. AddLoc t => t -> t
dropLoc -> P.EVar c :: Name
c) _)
arg :: Expr Name
arg@(Expr Name -> Expr Name
forall t. AddLoc t => t -> t
dropLoc -> P.ELit l :: Literal
l)
| Just n :: Ident
n <- Name -> Maybe Ident
asPrim Name
c
, Ident
n Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (String -> Ident) -> [String] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map String -> Ident
packIdent [ "<<", ">>", "<<<", ">>>" , "@", "!" ] ->
do Expr Name
newArg <- do Expr Name
l1 <- Bool -> Literal -> InferM (Expr Name)
desugarLiteral Bool
True Literal
l
Expr Name -> InferM (Expr Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr Name -> InferM (Expr Name))
-> Expr Name -> InferM (Expr Name)
forall a b. (a -> b) -> a -> b
$ case Expr Name
arg of
P.ELocated _ pos :: Range
pos -> Expr Name -> Range -> Expr Name
forall n. Expr n -> Range -> Expr n
P.ELocated Expr Name
l1 Range
pos
_ -> Expr Name
l1
Expr Name -> Prop -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
fun Expr Name
newArg) Prop
tGoal
P.EApp e1 :: Expr Name
e1 e2 :: Expr Name
e2 ->
do Prop
t1 <- TVarSource -> Kind -> InferM Prop
newType (Maybe Int -> TVarSource
TypeOfArg Maybe Int
forall a. Maybe a
Nothing) Kind
KType
Expr
e1' <- Expr Name -> Prop -> InferM Expr
checkE Expr Name
e1 (Prop -> Prop -> Prop
tFun Prop
t1 Prop
tGoal)
Expr
e2' <- Expr Name -> Prop -> InferM Expr
checkE Expr Name
e2 Prop
t1
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
EApp Expr
e1' Expr
e2')
P.EIf e1 :: Expr Name
e1 e2 :: Expr Name
e2 e3 :: Expr Name
e3 ->
do Expr
e1' <- Expr Name -> Prop -> InferM Expr
checkE Expr Name
e1 Prop
tBit
Expr
e2' <- Expr Name -> Prop -> InferM Expr
checkE Expr Name
e2 Prop
tGoal
Expr
e3' <- Expr Name -> Prop -> InferM Expr
checkE Expr Name
e3 Prop
tGoal
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
EIf Expr
e1' Expr
e2' Expr
e3')
P.EWhere e :: Expr Name
e ds :: [Decl Name]
ds ->
[Decl Name] -> ([DeclGroup] -> InferM Expr) -> InferM Expr
forall d a.
FromDecl d =>
[d] -> ([DeclGroup] -> InferM a) -> InferM a
inferDs [Decl Name]
ds (([DeclGroup] -> InferM Expr) -> InferM Expr)
-> ([DeclGroup] -> InferM Expr) -> InferM Expr
forall a b. (a -> b) -> a -> b
$ \ds1 :: [DeclGroup]
ds1 -> do Expr
e1 <- Expr Name -> Prop -> InferM Expr
checkE Expr Name
e Prop
tGoal
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> [DeclGroup] -> Expr
EWhere Expr
e1 [DeclGroup]
ds1)
P.ETyped e :: Expr Name
e t :: Type Name
t ->
do Prop
tSig <- Type Name -> Kind -> InferM Prop
checkTypeOfKind Type Name
t Kind
KType
Expr
e' <- Expr Name -> Prop -> InferM Expr
checkE Expr Name
e Prop
tSig
Prop -> Prop -> InferM ()
checkHasType Prop
tSig Prop
tGoal
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'
P.ETypeVal t :: Type Name
t ->
do Range
l <- InferM Range
curRange
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim "number"
Expr Name -> Prop -> InferM Expr
checkE (Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst
Named :: forall a. Located Ident -> a -> Named a
P.Named { name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent "val")
, value :: Type Name
value = Type Name
t }]) Prop
tGoal
P.EFun ps :: [Pattern Name]
ps e :: Expr Name
e -> Doc -> [Pattern Name] -> Expr Name -> Prop -> InferM Expr
checkFun (String -> Doc
text "anonymous function") [Pattern Name]
ps Expr Name
e Prop
tGoal
P.ELocated e :: Expr Name
e r :: Range
r -> Range -> InferM Expr -> InferM Expr
forall a. Range -> InferM a -> InferM a
inRange Range
r (Expr Name -> Prop -> InferM Expr
checkE Expr Name
e Prop
tGoal)
P.ESplit e :: Expr Name
e ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim "splitAt"
Expr Name -> Prop -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e) Prop
tGoal
P.EInfix a :: Expr Name
a op :: Located Name
op _ b :: Expr Name
b -> Expr Name -> Prop -> InferM Expr
checkE (Name -> Expr Name
forall n. n -> Expr n
P.EVar (Located Name -> Name
forall a. Located a -> a
thing Located Name
op) Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
a Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
b) Prop
tGoal
P.EParens e :: Expr Name
e -> Expr Name -> Prop -> InferM Expr
checkE Expr Name
e Prop
tGoal
selSrc :: P.Selector -> TVarSource
selSrc :: Selector -> TVarSource
selSrc l :: Selector
l = case Selector
l of
RecordSel la :: Ident
la _ -> Ident -> TVarSource
TypeOfRecordField Ident
la
TupleSel n :: Int
n _ -> Int -> TVarSource
TypeOfTupleField Int
n
ListSel _ _ -> TVarSource
TypeOfSeqElement
checkRecUpd :: Maybe (P.Expr Name) -> [ P.UpdField Name ] -> Type -> InferM Expr
checkRecUpd :: Maybe (Expr Name) -> [UpdField Name] -> Prop -> InferM Expr
checkRecUpd mb :: Maybe (Expr Name)
mb fs :: [UpdField Name]
fs tGoal :: Prop
tGoal =
case Maybe (Expr Name)
mb of
Nothing ->
do Name
r <- Ident -> InferM Name
newParamName (String -> Ident
packIdent "r")
let p :: Pattern Name
p = Located Name -> Pattern Name
forall n. Located n -> Pattern n
P.PVar $WLocated :: forall a. Range -> a -> Located a
Located { srcRange :: Range
srcRange = Name -> Range
nameLoc Name
r, thing :: Name
thing = Name
r }
fe :: Expr Name
fe = [Pattern Name] -> Expr Name -> Expr Name
forall n. [Pattern n] -> Expr n -> Expr n
P.EFun [Pattern Name
p] (Maybe (Expr Name) -> [UpdField Name] -> Expr Name
forall n. Maybe (Expr n) -> [UpdField n] -> Expr n
P.EUpd (Expr Name -> Maybe (Expr Name)
forall a. a -> Maybe a
Just (Name -> Expr Name
forall n. n -> Expr n
P.EVar Name
r)) [UpdField Name]
fs)
Expr Name -> Prop -> InferM Expr
checkE Expr Name
fe Prop
tGoal
Just e :: Expr Name
e ->
do Expr
e1 <- Expr Name -> Prop -> InferM Expr
checkE Expr Name
e Prop
tGoal
(Expr -> UpdField Name -> InferM Expr)
-> Expr -> [UpdField Name] -> InferM Expr
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Expr -> UpdField Name -> InferM Expr
doUpd Expr
e1 [UpdField Name]
fs
where
doUpd :: Expr -> UpdField Name -> InferM Expr
doUpd e :: Expr
e (P.UpdField how :: UpdHow
how sels :: [Located Selector]
sels v :: Expr Name
v) =
case [Located Selector]
sels of
[l :: Located Selector
l] ->
case UpdHow
how of
P.UpdSet ->
do Prop
ft <- TVarSource -> Kind -> InferM Prop
newType (Selector -> TVarSource
selSrc Selector
s) Kind
KType
Expr
v1 <- Expr Name -> Prop -> InferM Expr
checkE Expr Name
v Prop
ft
HasGoalSln
d <- Selector -> Prop -> Prop -> InferM HasGoalSln
newHasGoal Selector
s Prop
tGoal Prop
ft
Expr -> InferM Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasGoalSln -> Expr -> Expr -> Expr
hasDoSet HasGoalSln
d Expr
e Expr
v1)
P.UpdFun ->
do Prop
ft <- TVarSource -> Kind -> InferM Prop
newType (Selector -> TVarSource
selSrc Selector
s) Kind
KType
Expr
v1 <- Expr Name -> Prop -> InferM Expr
checkE Expr Name
v (Prop -> Prop -> Prop
tFun Prop
ft Prop
ft)
HasGoalSln
d <- Selector -> Prop -> Prop -> InferM HasGoalSln
newHasGoal Selector
s Prop
tGoal Prop
ft
Name
tmp <- Ident -> InferM Name
newParamName (String -> Ident
packIdent "rf")
let e' :: Expr
e' = Name -> Expr
EVar Name
tmp
Expr -> InferM Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> InferM Expr) -> Expr -> InferM Expr
forall a b. (a -> b) -> a -> b
$ HasGoalSln -> Expr -> Expr -> Expr
hasDoSet HasGoalSln
d Expr
e' (Expr -> Expr -> Expr
EApp Expr
v1 (HasGoalSln -> Expr -> Expr
hasDoSelect HasGoalSln
d Expr
e'))
Expr -> [DeclGroup] -> Expr
`EWhere`
[ Decl -> DeclGroup
NonRecursive
$WDecl :: Name
-> Schema
-> DeclDef
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe String
-> Decl
Decl { dName :: Name
dName = Name
tmp
, dSignature :: Schema
dSignature = Prop -> Schema
tMono Prop
tGoal
, dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr Expr
e
, dPragmas :: [Pragma]
dPragmas = []
, dInfix :: Bool
dInfix = Bool
False
, dFixity :: Maybe Fixity
dFixity = Maybe Fixity
forall a. Maybe a
Nothing
, dDoc :: Maybe String
dDoc = Maybe String
forall a. Maybe a
Nothing
} ]
where s :: Selector
s = Located Selector -> Selector
forall a. Located a -> a
thing Located Selector
l
_ -> String -> [String] -> InferM Expr
forall a. HasCallStack => String -> [String] -> a
panic "checkRecUpd/doUpd" [ "Expected exactly 1 field label"
, "Got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Located Selector] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Located Selector]
sels)
]
expectSeq :: Type -> InferM (Type,Type)
expectSeq :: Prop -> InferM (Prop, Prop)
expectSeq ty :: Prop
ty =
case Prop
ty of
TUser _ _ ty' :: Prop
ty' ->
Prop -> InferM (Prop, Prop)
expectSeq Prop
ty'
TCon (TC TCSeq) [a :: Prop
a,b :: Prop
b] ->
(Prop, Prop) -> InferM (Prop, Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
a,Prop
b)
TVar _ ->
do tys :: (Prop, Prop)
tys@(a :: Prop
a,b :: Prop
b) <- InferM (Prop, Prop)
genTys
ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType ([Prop] -> InferM ()) -> InferM [Prop] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Prop -> Prop -> InferM [Prop]
unify Prop
ty (Prop -> Prop -> Prop
tSeq Prop
a Prop
b)
(Prop, Prop) -> InferM (Prop, Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop, Prop)
tys
_ ->
do tys :: (Prop, Prop)
tys@(a :: Prop
a,b :: Prop
b) <- InferM (Prop, Prop)
genTys
Error -> InferM ()
recordError (Prop -> Prop -> Error
TypeMismatch Prop
ty (Prop -> Prop -> Prop
tSeq Prop
a Prop
b))
(Prop, Prop) -> InferM (Prop, Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop, Prop)
tys
where
genTys :: InferM (Prop, Prop)
genTys =
do Prop
a <- TVarSource -> Kind -> InferM Prop
newType TVarSource
LenOfSeq Kind
KNum
Prop
b <- TVarSource -> Kind -> InferM Prop
newType TVarSource
TypeOfSeqElement Kind
KType
(Prop, Prop) -> InferM (Prop, Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
a,Prop
b)
expectTuple :: Int -> Type -> InferM [Type]
expectTuple :: Int -> Prop -> InferM [Prop]
expectTuple n :: Int
n ty :: Prop
ty =
case Prop
ty of
TUser _ _ ty' :: Prop
ty' ->
Int -> Prop -> InferM [Prop]
expectTuple Int
n Prop
ty'
TCon (TC (TCTuple n' :: Int
n')) tys :: [Prop]
tys | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n' ->
[Prop] -> InferM [Prop]
forall (m :: * -> *) a. Monad m => a -> m a
return [Prop]
tys
TVar _ ->
do [Prop]
tys <- InferM [Prop]
genTys
ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType ([Prop] -> InferM ()) -> InferM [Prop] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Prop -> Prop -> InferM [Prop]
unify Prop
ty ([Prop] -> Prop
tTuple [Prop]
tys)
[Prop] -> InferM [Prop]
forall (m :: * -> *) a. Monad m => a -> m a
return [Prop]
tys
_ ->
do [Prop]
tys <- InferM [Prop]
genTys
Error -> InferM ()
recordError (Prop -> Prop -> Error
TypeMismatch Prop
ty ([Prop] -> Prop
tTuple [Prop]
tys))
[Prop] -> InferM [Prop]
forall (m :: * -> *) a. Monad m => a -> m a
return [Prop]
tys
where
genTys :: InferM [Prop]
genTys =[Int] -> (Int -> InferM Prop) -> InferM [Prop]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ 0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1 ] ((Int -> InferM Prop) -> InferM [Prop])
-> (Int -> InferM Prop) -> InferM [Prop]
forall a b. (a -> b) -> a -> b
$ \ i :: Int
i -> TVarSource -> Kind -> InferM Prop
newType (Int -> TVarSource
TypeOfTupleField Int
i) Kind
KType
expectRec :: [P.Named a] -> Type -> InferM [(Ident,a,Type)]
expectRec :: [Named a] -> Prop -> InferM [(Ident, a, Prop)]
expectRec fs :: [Named a]
fs ty :: Prop
ty =
case Prop
ty of
TUser _ _ ty' :: Prop
ty' ->
[Named a] -> Prop -> InferM [(Ident, a, Prop)]
forall a. [Named a] -> Prop -> InferM [(Ident, a, Prop)]
expectRec [Named a]
fs Prop
ty'
TRec ls :: [(Ident, Prop)]
ls | Just tys :: [(Ident, a, Prop)]
tys <- ((Ident, Prop) -> Maybe (Ident, a, Prop))
-> [(Ident, Prop)] -> Maybe [(Ident, a, Prop)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Ident, Prop) -> Maybe (Ident, a, Prop)
forall c. (Ident, c) -> Maybe (Ident, a, c)
checkField [(Ident, Prop)]
ls ->
[(Ident, a, Prop)] -> InferM [(Ident, a, Prop)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Ident, a, Prop)]
tys
_ ->
do (tys :: [(Ident, Prop)]
tys,res :: [(Ident, a, Prop)]
res) <- InferM ([(Ident, Prop)], [(Ident, a, Prop)])
genTys
case Prop
ty of
TVar TVFree{} -> do [Prop]
ps <- Prop -> Prop -> InferM [Prop]
unify Prop
ty ([(Ident, Prop)] -> Prop
TRec [(Ident, Prop)]
tys)
ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType [Prop]
ps
_ -> Error -> InferM ()
recordError (Prop -> Prop -> Error
TypeMismatch Prop
ty ([(Ident, Prop)] -> Prop
TRec [(Ident, Prop)]
tys))
[(Ident, a, Prop)] -> InferM [(Ident, a, Prop)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Ident, a, Prop)]
res
where
checkField :: (Ident, c) -> Maybe (Ident, a, c)
checkField (n :: Ident
n,t :: c
t) =
do Named a
f <- (Named a -> Bool) -> [Named a] -> Maybe (Named a)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\f :: Named a
f -> Located Ident -> Ident
forall a. Located a -> a
thing (Named a -> Located Ident
forall a. Named a -> Located Ident
P.name Named a
f) Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
n) [Named a]
fs
(Ident, a, c) -> Maybe (Ident, a, c)
forall (m :: * -> *) a. Monad m => a -> m a
return (Located Ident -> Ident
forall a. Located a -> a
thing (Named a -> Located Ident
forall a. Named a -> Located Ident
P.name Named a
f), Named a -> a
forall a. Named a -> a
P.value Named a
f, c
t)
genTys :: InferM ([(Ident, Prop)], [(Ident, a, Prop)])
genTys =
do [(Ident, a, Prop)]
res <- [Named a]
-> (Named a -> InferM (Ident, a, Prop))
-> InferM [(Ident, a, Prop)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Named a]
fs ((Named a -> InferM (Ident, a, Prop)) -> InferM [(Ident, a, Prop)])
-> (Named a -> InferM (Ident, a, Prop))
-> InferM [(Ident, a, Prop)]
forall a b. (a -> b) -> a -> b
$ \ f :: Named a
f ->
do let field :: Ident
field = Located Ident -> Ident
forall a. Located a -> a
thing (Named a -> Located Ident
forall a. Named a -> Located Ident
P.name Named a
f)
Prop
t <- TVarSource -> Kind -> InferM Prop
newType (Ident -> TVarSource
TypeOfRecordField Ident
field) Kind
KType
(Ident, a, Prop) -> InferM (Ident, a, Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident
field, Named a -> a
forall a. Named a -> a
P.value Named a
f, Prop
t)
let (ls :: [Ident]
ls,_,ts :: [Prop]
ts) = [(Ident, a, Prop)] -> ([Ident], [a], [Prop])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [(Ident, a, Prop)]
res
([(Ident, Prop)], [(Ident, a, Prop)])
-> InferM ([(Ident, Prop)], [(Ident, a, Prop)])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Ident] -> [Prop] -> [(Ident, Prop)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
ls [Prop]
ts, [(Ident, a, Prop)]
res)
expectFin :: Int -> Type -> InferM ()
expectFin :: Int -> Prop -> InferM ()
expectFin n :: Int
n ty :: Prop
ty =
case Prop
ty of
TUser _ _ ty' :: Prop
ty' ->
Int -> Prop -> InferM ()
expectFin Int
n Prop
ty'
TCon (TC (TCNum n' :: Integer
n')) [] | Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n' ->
() -> InferM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
_ ->
do ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType ([Prop] -> InferM ()) -> InferM [Prop] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Prop -> Prop -> InferM [Prop]
unify Prop
ty (Int -> Prop
forall a. Integral a => a -> Prop
tNum Int
n)
expectFun :: Int -> Type -> InferM ([Type],Type)
expectFun :: Int -> Prop -> InferM ([Prop], Prop)
expectFun = [Prop] -> Int -> Prop -> InferM ([Prop], Prop)
go []
where
go :: [Prop] -> Int -> Prop -> InferM ([Prop], Prop)
go tys :: [Prop]
tys arity :: Int
arity ty :: Prop
ty
| Int
arity Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 =
case Prop
ty of
TUser _ _ ty' :: Prop
ty' ->
[Prop] -> Int -> Prop -> InferM ([Prop], Prop)
go [Prop]
tys Int
arity Prop
ty'
TCon (TC TCFun) [a :: Prop
a,b :: Prop
b] ->
[Prop] -> Int -> Prop -> InferM ([Prop], Prop)
go (Prop
aProp -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
:[Prop]
tys) (Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) Prop
b
_ ->
do [Prop]
args <- Int -> InferM [Prop]
genArgs Int
arity
Prop
res <- TVarSource -> Kind -> InferM Prop
newType TVarSource
TypeOfRes Kind
KType
case Prop
ty of
TVar TVFree{} -> do [Prop]
ps <- Prop -> Prop -> InferM [Prop]
unify Prop
ty ((Prop -> Prop -> Prop) -> Prop -> [Prop] -> Prop
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Prop -> Prop
tFun Prop
res [Prop]
args)
ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType [Prop]
ps
_ -> Error -> InferM ()
recordError (Prop -> Prop -> Error
TypeMismatch Prop
ty ((Prop -> Prop -> Prop) -> Prop -> [Prop] -> Prop
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Prop -> Prop
tFun Prop
res [Prop]
args))
([Prop], Prop) -> InferM ([Prop], Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Prop] -> [Prop]
forall a. [a] -> [a]
reverse [Prop]
tys [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
args, Prop
res)
| Bool
otherwise =
([Prop], Prop) -> InferM ([Prop], Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Prop] -> [Prop]
forall a. [a] -> [a]
reverse [Prop]
tys, Prop
ty)
genArgs :: Int -> InferM [Prop]
genArgs arity :: Int
arity = [Int] -> (Int -> InferM Prop) -> InferM [Prop]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ 1 .. Int
arity ] ((Int -> InferM Prop) -> InferM [Prop])
-> (Int -> InferM Prop) -> InferM [Prop]
forall a b. (a -> b) -> a -> b
$
\ ix :: Int
ix -> TVarSource -> Kind -> InferM Prop
newType (Maybe Int -> TVarSource
TypeOfArg (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
ix)) Kind
KType
checkHasType :: Type -> Type -> InferM ()
checkHasType :: Prop -> Prop -> InferM ()
checkHasType inferredType :: Prop
inferredType givenType :: Prop
givenType =
do [Prop]
ps <- Prop -> Prop -> InferM [Prop]
unify Prop
givenType Prop
inferredType
case [Prop]
ps of
[] -> () -> InferM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
_ -> ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType [Prop]
ps
checkFun :: Doc -> [P.Pattern Name] -> P.Expr Name -> Type -> InferM Expr
checkFun :: Doc -> [Pattern Name] -> Expr Name -> Prop -> InferM Expr
checkFun _ [] e :: Expr Name
e tGoal :: Prop
tGoal = Expr Name -> Prop -> InferM Expr
checkE Expr Name
e Prop
tGoal
checkFun desc :: Doc
desc ps :: [Pattern Name]
ps e :: Expr Name
e tGoal :: Prop
tGoal =
InferM Expr -> InferM Expr
forall a. InferM a -> InferM a
inNewScope (InferM Expr -> InferM Expr) -> InferM Expr -> InferM Expr
forall a b. (a -> b) -> a -> b
$
do let descs :: [Doc]
descs = [ String -> Doc
text "type of" Doc -> Doc -> Doc
<+> Int -> Doc
forall a. (Integral a, Show a, Eq a) => a -> Doc
ordinal Int
n Doc -> Doc -> Doc
<+> String -> Doc
text "argument"
Doc -> Doc -> Doc
<+> String -> Doc
text "of" Doc -> Doc -> Doc
<+> Doc
desc | Int
n <- [ 1 :: Int .. ] ]
(tys :: [Prop]
tys,tRes :: Prop
tRes) <- Int -> Prop -> InferM ([Prop], Prop)
expectFun ([Pattern Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern Name]
ps) Prop
tGoal
[Located Name]
largs <- [InferM (Located Name)] -> InferM [Located Name]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((Doc -> Pattern Name -> Prop -> InferM (Located Name))
-> [Doc] -> [Pattern Name] -> [Prop] -> [InferM (Located Name)]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Doc -> Pattern Name -> Prop -> InferM (Located Name)
checkP [Doc]
descs [Pattern Name]
ps [Prop]
tys)
let ds :: Map Name (Located Prop)
ds = [(Name, Located Prop)] -> Map Name (Located Prop)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Located Name -> Name
forall a. Located a -> a
thing Located Name
x, Located Name
x { thing :: Prop
thing = Prop
t }) | (x :: Located Name
x,t :: Prop
t) <- [Located Name] -> [Prop] -> [(Located Name, Prop)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Located Name]
largs [Prop]
tys ]
Expr
e1 <- Map Name (Located Prop) -> InferM Expr -> InferM Expr
forall a. Map Name (Located Prop) -> InferM a -> InferM a
withMonoTypes Map Name (Located Prop)
ds (Expr Name -> Prop -> InferM Expr
checkE Expr Name
e Prop
tRes)
let args :: [(Name, Prop)]
args = [ (Located Name -> Name
forall a. Located a -> a
thing Located Name
x, Prop
t) | (x :: Located Name
x,t :: Prop
t) <- [Located Name] -> [Prop] -> [(Located Name, Prop)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Located Name]
largs [Prop]
tys ]
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, Prop) -> Expr -> Expr) -> Expr -> [(Name, Prop)] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(x :: Name
x,t :: Prop
t) b :: Expr
b -> Name -> Prop -> Expr -> Expr
EAbs Name
x Prop
t Expr
b) Expr
e1 [(Name, Prop)]
args)
smallest :: [Type] -> InferM Type
smallest :: [Prop] -> InferM Prop
smallest [] = TVarSource -> Kind -> InferM Prop
newType TVarSource
LenOfSeq Kind
KNum
smallest [t :: Prop
t] = Prop -> InferM Prop
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
t
smallest ts :: [Prop]
ts = do Prop
a <- TVarSource -> Kind -> InferM Prop
newType TVarSource
LenOfSeq Kind
KNum
ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtComprehension [ Prop
a Prop -> Prop -> Prop
=#= (Prop -> Prop -> Prop) -> [Prop] -> Prop
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Prop -> Prop -> Prop
tMin [Prop]
ts ]
Prop -> InferM Prop
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
a
checkP :: Doc -> P.Pattern Name -> Type -> InferM (Located Name)
checkP :: Doc -> Pattern Name -> Prop -> InferM (Located Name)
checkP desc :: Doc
desc p :: Pattern Name
p tGoal :: Prop
tGoal =
do (x :: Name
x, t :: Located Prop
t) <- Doc -> Pattern Name -> InferM (Name, Located Prop)
inferP Doc
desc Pattern Name
p
[Prop]
ps <- Prop -> Prop -> InferM [Prop]
unify Prop
tGoal (Located Prop -> Prop
forall a. Located a -> a
thing Located Prop
t)
let rng :: Range
rng = Range -> Maybe Range -> Range
forall a. a -> Maybe a -> a
fromMaybe Range
emptyRange (Maybe Range -> Range) -> Maybe Range -> Range
forall a b. (a -> b) -> a -> b
$ Pattern Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Pattern Name
p
let mkErr :: Prop -> InferM ()
mkErr = Error -> InferM ()
recordError (Error -> InferM ()) -> (Prop -> Error) -> Prop -> InferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [Goal] -> Error
UnsolvedGoals Bool
False ([Goal] -> Error) -> (Prop -> [Goal]) -> Prop -> Error
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Goal -> [Goal] -> [Goal]
forall a. a -> [a] -> [a]
:[])
(Goal -> [Goal]) -> (Prop -> Goal) -> Prop -> [Goal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstraintSource -> Range -> Prop -> Goal
Goal (Doc -> ConstraintSource
CtPattern Doc
desc) Range
rng
(Prop -> InferM ()) -> [Prop] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Prop -> InferM ()
mkErr [Prop]
ps
Located Name -> InferM (Located Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Range -> Name -> Located Name
forall a. Range -> a -> Located a
Located (Located Prop -> Range
forall a. Located a -> Range
srcRange Located Prop
t) Name
x)
inferP :: Doc -> P.Pattern Name -> InferM (Name, Located Type)
inferP :: Doc -> Pattern Name -> InferM (Name, Located Prop)
inferP desc :: Doc
desc pat :: Pattern Name
pat =
case Pattern Name
pat of
P.PVar x0 :: Located Name
x0 ->
do Prop
a <- Range -> InferM Prop -> InferM Prop
forall a. Range -> InferM a -> InferM a
inRange (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
x0) (TVarSource -> Kind -> InferM Prop
newType (Name -> TVarSource
DefinitionOf (Located Name -> Name
forall a. Located a -> a
thing Located Name
x0)) Kind
KType)
(Name, Located Prop) -> InferM (Name, Located Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return (Located Name -> Name
forall a. Located a -> a
thing Located Name
x0, Located Name
x0 { thing :: Prop
thing = Prop
a })
P.PTyped p :: Pattern Name
p t :: Type Name
t ->
do Prop
tSig <- Type Name -> Kind -> InferM Prop
checkTypeOfKind Type Name
t Kind
KType
Located Name
ln <- Doc -> Pattern Name -> Prop -> InferM (Located Name)
checkP Doc
desc Pattern Name
p Prop
tSig
(Name, Located Prop) -> InferM (Name, Located Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return (Located Name -> Name
forall a. Located a -> a
thing Located Name
ln, Located Name
ln { thing :: Prop
thing = Prop
tSig })
_ -> String -> [String] -> InferM (Name, Located Prop)
forall a. String -> [String] -> a
tcPanic "inferP" [ "Unexpected pattern:", Pattern Name -> String
forall a. Show a => a -> String
show Pattern Name
pat ]
inferMatch :: P.Match Name -> InferM (Match, Name, Located Type, Type)
inferMatch :: Match Name -> InferM (Match, Name, Located Prop, Prop)
inferMatch (P.Match p :: Pattern Name
p e :: Expr Name
e) =
do (x :: Name
x,t :: Located Prop
t) <- Doc -> Pattern Name -> InferM (Name, Located Prop)
inferP (String -> Doc
text "a value bound by a generator in a comprehension") Pattern Name
p
Prop
n <- TVarSource -> Kind -> InferM Prop
newType TVarSource
LenOfCompGen Kind
KNum
Expr
e' <- Expr Name -> Prop -> InferM Expr
checkE Expr Name
e (Prop -> Prop -> Prop
tSeq Prop
n (Located Prop -> Prop
forall a. Located a -> a
thing Located Prop
t))
(Match, Name, Located Prop, Prop)
-> InferM (Match, Name, Located Prop, Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Prop -> Prop -> Expr -> Match
From Name
x Prop
n (Located Prop -> Prop
forall a. Located a -> a
thing Located Prop
t) Expr
e', Name
x, Located Prop
t, Prop
n)
inferMatch (P.MatchLet b :: Bind Name
b)
| Bind Name -> Bool
forall name. Bind name -> Bool
P.bMono Bind Name
b =
do let rng :: Range
rng = Located Name -> Range
forall a. Located a -> Range
srcRange (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
Prop
a <- Range -> InferM Prop -> InferM Prop
forall a. Range -> InferM a -> InferM a
inRange Range
rng (TVarSource -> Kind -> InferM Prop
newType (Name -> TVarSource
DefinitionOf (Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b))) Kind
KType)
Decl
b1 <- Bind Name -> Prop -> InferM Decl
checkMonoB Bind Name
b Prop
a
(Match, Name, Located Prop, Prop)
-> InferM (Match, Name, Located Prop, Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Match
Let Decl
b1, Decl -> Name
dName Decl
b1, Range -> Prop -> Located Prop
forall a. Range -> a -> Located a
Located (Located Name -> Range
forall a. Located a -> Range
srcRange (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)) Prop
a, Int -> Prop
forall a. Integral a => a -> Prop
tNum (1::Int))
| Bool
otherwise = String -> [String] -> InferM (Match, Name, Located Prop, Prop)
forall a. String -> [String] -> a
tcPanic "inferMatch"
[ "Unexpected polymorphic match let:", Bind Name -> String
forall a. Show a => a -> String
show Bind Name
b ]
inferCArm :: Int -> [P.Match Name] -> InferM
( [Match]
, Map Name (Located Type)
, Type
)
inferCArm :: Int
-> [Match Name] -> InferM ([Match], Map Name (Located Prop), Prop)
inferCArm _ [] = String
-> [String] -> InferM ([Match], Map Name (Located Prop), Prop)
forall a. HasCallStack => String -> [String] -> a
panic "inferCArm" [ "Empty comprehension arm" ]
inferCArm _ [m :: Match Name
m] =
do (m1 :: Match
m1, x :: Name
x, t :: Located Prop
t, n :: Prop
n) <- Match Name -> InferM (Match, Name, Located Prop, Prop)
inferMatch Match Name
m
([Match], Map Name (Located Prop), Prop)
-> InferM ([Match], Map Name (Located Prop), Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Match
m1], Name -> Located Prop -> Map Name (Located Prop)
forall k a. k -> a -> Map k a
Map.singleton Name
x Located Prop
t, Prop
n)
inferCArm armNum :: Int
armNum (m :: Match Name
m : ms :: [Match Name]
ms) =
do (m1 :: Match
m1, x :: Name
x, t :: Located Prop
t, n :: Prop
n) <- Match Name -> InferM (Match, Name, Located Prop, Prop)
inferMatch Match Name
m
(ms' :: [Match]
ms', ds :: Map Name (Located Prop)
ds, n' :: Prop
n') <- (Name, Located Prop)
-> InferM ([Match], Map Name (Located Prop), Prop)
-> InferM ([Match], Map Name (Located Prop), Prop)
forall a. (Name, Located Prop) -> InferM a -> InferM a
withMonoType (Name
x,Located Prop
t) (Int
-> [Match Name] -> InferM ([Match], Map Name (Located Prop), Prop)
inferCArm Int
armNum [Match Name]
ms)
ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtComprehension [ Prop -> Prop
pFin Prop
n' ]
([Match], Map Name (Located Prop), Prop)
-> InferM ([Match], Map Name (Located Prop), Prop)
forall (m :: * -> *) a. Monad m => a -> m a
return (Match
m1 Match -> [Match] -> [Match]
forall a. a -> [a] -> [a]
: [Match]
ms', (Located Prop -> Located Prop -> Located Prop)
-> Name
-> Located Prop
-> Map Name (Located Prop)
-> Map Name (Located Prop)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (\_ old :: Located Prop
old -> Located Prop
old) Name
x Located Prop
t Map Name (Located Prop)
ds, Prop -> Prop -> Prop
tMul Prop
n Prop
n')
inferBinds :: Bool -> Bool -> [P.Bind Name] -> InferM [Decl]
inferBinds :: Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferBinds isTopLevel :: Bool
isTopLevel isRec :: Bool
isRec binds :: [Bind Name]
binds =
do
Bool
monoBinds <- InferM Bool
getMonoBinds
let (sigs :: [Bind Name]
sigs,noSigs :: [Bind Name]
noSigs) = (Bind Name -> Bool) -> [Bind Name] -> ([Bind Name], [Bind Name])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Maybe (Schema Name) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Schema Name) -> Bool)
-> (Bind Name -> Maybe (Schema Name)) -> Bind Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bind Name -> Maybe (Schema Name)
forall name. Bind name -> Maybe (Schema name)
P.bSignature) [Bind Name]
binds
monos :: [Bind Name]
monos = [Bind Name]
sigs [Bind Name] -> [Bind Name] -> [Bind Name]
forall a. [a] -> [a] -> [a]
++ [ Bind Name
b { bMono :: Bool
P.bMono = Bool
True } | Bind Name
b <- [Bind Name]
noSigs ]
binds' :: [Bind Name]
binds' | (Bind Name -> Bool) -> [Bind Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Bind Name -> Bool
forall name. Bind name -> Bool
P.bMono [Bind Name]
binds = [Bind Name]
monos
| Bool
monoBinds Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
isTopLevel = [Bind Name]
monos
| Bool
otherwise = [Bind Name]
binds
check :: Map Name Expr -> InferM ([Decl], [Decl])
check exprMap :: Map Name Expr
exprMap =
do (newEnv :: [(Name, VarType)]
newEnv,todos :: [Either (InferM Decl) (InferM Decl)]
todos) <- [((Name, VarType), Either (InferM Decl) (InferM Decl))]
-> ([(Name, VarType)], [Either (InferM Decl) (InferM Decl)])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((Name, VarType), Either (InferM Decl) (InferM Decl))]
-> ([(Name, VarType)], [Either (InferM Decl) (InferM Decl)]))
-> InferM [((Name, VarType), Either (InferM Decl) (InferM Decl))]
-> InferM ([(Name, VarType)], [Either (InferM Decl) (InferM Decl)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Bind Name
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl)))
-> [Bind Name]
-> InferM [((Name, VarType), Either (InferM Decl) (InferM Decl))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Map Name Expr
-> Bind Name
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
guessType Map Name Expr
exprMap) [Bind Name]
binds'
let otherEnv :: [(Name, VarType)]
otherEnv = ((Name, VarType) -> Bool) -> [(Name, VarType)] -> [(Name, VarType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name, VarType) -> Bool
forall a. (a, VarType) -> Bool
isExt [(Name, VarType)]
newEnv
let (sigsAndMonos :: [InferM Decl]
sigsAndMonos,noSigGen :: [InferM Decl]
noSigGen) = [Either (InferM Decl) (InferM Decl)]
-> ([InferM Decl], [InferM Decl])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either (InferM Decl) (InferM Decl)]
todos
let prepGen :: InferM ([Decl], [Goal])
prepGen = InferM [Decl] -> InferM ([Decl], [Goal])
forall a. InferM a -> InferM (a, [Goal])
collectGoals
(InferM [Decl] -> InferM ([Decl], [Goal]))
-> InferM [Decl] -> InferM ([Decl], [Goal])
forall a b. (a -> b) -> a -> b
$ do [Decl]
bs <- [InferM Decl] -> InferM [Decl]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [InferM Decl]
noSigGen
InferM ()
simplifyAllConstraints
[Decl] -> InferM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return [Decl]
bs
if Bool
isRec
then
do (bs1 :: [Decl]
bs1,cs :: [Goal]
cs) <- [(Name, VarType)]
-> InferM ([Decl], [Goal]) -> InferM ([Decl], [Goal])
forall a. [(Name, VarType)] -> InferM a -> InferM a
withVarTypes [(Name, VarType)]
newEnv InferM ([Decl], [Goal])
prepGen
[Decl]
genCs <- [(Name, VarType)] -> InferM [Decl] -> InferM [Decl]
forall a. [(Name, VarType)] -> InferM a -> InferM a
withVarTypes [(Name, VarType)]
otherEnv ([Decl] -> [Goal] -> InferM [Decl]
generalize [Decl]
bs1 [Goal]
cs)
let newEnv' :: [(Name, VarType)]
newEnv' = (Decl -> (Name, VarType)) -> [Decl] -> [(Name, VarType)]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> (Name, VarType)
toExt [Decl]
bs1 [(Name, VarType)] -> [(Name, VarType)] -> [(Name, VarType)]
forall a. [a] -> [a] -> [a]
++ [(Name, VarType)]
otherEnv
[Decl]
done <- [(Name, VarType)] -> InferM [Decl] -> InferM [Decl]
forall a. [(Name, VarType)] -> InferM a -> InferM a
withVarTypes [(Name, VarType)]
newEnv' ([InferM Decl] -> InferM [Decl]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [InferM Decl]
sigsAndMonos)
([Decl], [Decl]) -> InferM ([Decl], [Decl])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl]
done,[Decl]
genCs)
else
do [Decl]
done <- [InferM Decl] -> InferM [Decl]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [InferM Decl]
sigsAndMonos
(bs1 :: [Decl]
bs1, cs :: [Goal]
cs) <- InferM ([Decl], [Goal])
prepGen
[Decl]
genCs <- [Decl] -> [Goal] -> InferM [Decl]
generalize [Decl]
bs1 [Goal]
cs
([Decl], [Decl]) -> InferM ([Decl], [Decl])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl]
done,[Decl]
genCs)
rec
let exprMap :: Map Name Expr
exprMap = [(Name, Expr)] -> Map Name Expr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ((Decl -> (Name, Expr)) -> [Decl] -> [(Name, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> (Name, Expr)
monoUse [Decl]
genBs)
(doneBs :: [Decl]
doneBs, genBs :: [Decl]
genBs) <- Map Name Expr -> InferM ([Decl], [Decl])
check Map Name Expr
exprMap
InferM ()
simplifyAllConstraints
[Decl] -> InferM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl]
doneBs [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ [Decl]
genBs)
where
toExt :: Decl -> (Name, VarType)
toExt d :: Decl
d = (Decl -> Name
dName Decl
d, Schema -> VarType
ExtVar (Decl -> Schema
dSignature Decl
d))
isExt :: (a, VarType) -> Bool
isExt (_,y :: VarType
y) = case VarType
y of
ExtVar _ -> Bool
True
_ -> Bool
False
monoUse :: Decl -> (Name, Expr)
monoUse d :: Decl
d = (Name
x, Expr
withQs)
where
x :: Name
x = Decl -> Name
dName Decl
d
as :: [TParam]
as = Schema -> [TParam]
sVars (Decl -> Schema
dSignature Decl
d)
qs :: [Prop]
qs = Schema -> [Prop]
sProps (Decl -> Schema
dSignature Decl
d)
appT :: Expr -> TParam -> Expr
appT e :: Expr
e a :: TParam
a = Expr -> Prop -> Expr
ETApp Expr
e (TVar -> Prop
TVar (TParam -> TVar
tpVar TParam
a))
appP :: Expr -> p -> Expr
appP e :: Expr
e _ = Expr -> Expr
EProofApp Expr
e
withTys :: Expr
withTys = (Expr -> TParam -> Expr) -> Expr -> [TParam] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Expr -> TParam -> Expr
appT (Name -> Expr
EVar Name
x) [TParam]
as
withQs :: Expr
withQs = (Expr -> Prop -> Expr) -> Expr -> [Prop] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Expr -> Prop -> Expr
forall p. Expr -> p -> Expr
appP Expr
withTys [Prop]
qs
guessType :: Map Name Expr -> P.Bind Name ->
InferM ( (Name, VarType)
, Either (InferM Decl)
(InferM Decl)
)
guessType :: Map Name Expr
-> Bind Name
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
guessType exprMap :: Map Name Expr
exprMap b :: Bind Name
b@(P.Bind { .. }) =
case Maybe (Schema Name)
bSignature of
Just s :: Schema Name
s ->
do (Schema, [Goal])
s1 <- AllowWildCards -> Schema Name -> InferM (Schema, [Goal])
checkSchema AllowWildCards
AllowWildCards Schema Name
s
((Name, VarType), Either (InferM Decl) (InferM Decl))
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
name, Schema -> VarType
ExtVar ((Schema, [Goal]) -> Schema
forall a b. (a, b) -> a
fst (Schema, [Goal])
s1)), InferM Decl -> Either (InferM Decl) (InferM Decl)
forall a b. a -> Either a b
Left (Bind Name -> (Schema, [Goal]) -> InferM Decl
checkSigB Bind Name
b (Schema, [Goal])
s1))
Nothing
| Bool
bMono ->
do Prop
t <- TVarSource -> Kind -> InferM Prop
newType (Name -> TVarSource
DefinitionOf Name
name) Kind
KType
let schema :: Schema
schema = [TParam] -> [Prop] -> Prop -> Schema
Forall [] [] Prop
t
((Name, VarType), Either (InferM Decl) (InferM Decl))
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
name, Schema -> VarType
ExtVar Schema
schema), InferM Decl -> Either (InferM Decl) (InferM Decl)
forall a b. a -> Either a b
Left (Bind Name -> Prop -> InferM Decl
checkMonoB Bind Name
b Prop
t))
| Bool
otherwise ->
do Prop
t <- TVarSource -> Kind -> InferM Prop
newType (Name -> TVarSource
DefinitionOf Name
name) Kind
KType
let noWay :: a
noWay = String -> [String] -> a
forall a. String -> [String] -> a
tcPanic "guessType" [ "Missing expression for:" ,
Name -> String
forall a. Show a => a -> String
show Name
name ]
expr :: Expr
expr = Expr -> Name -> Map Name Expr -> Expr
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Expr
forall a. a
noWay Name
name Map Name Expr
exprMap
((Name, VarType), Either (InferM Decl) (InferM Decl))
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
name, Expr -> Prop -> VarType
CurSCC Expr
expr Prop
t), InferM Decl -> Either (InferM Decl) (InferM Decl)
forall a b. b -> Either a b
Right (Bind Name -> Prop -> InferM Decl
checkMonoB Bind Name
b Prop
t))
where
name :: Name
name = Located Name -> Name
forall a. Located a -> a
thing Located Name
bName
generalize :: [Decl] -> [Goal] -> InferM [Decl]
generalize :: [Decl] -> [Goal] -> InferM [Decl]
generalize [] gs0 :: [Goal]
gs0 =
do [Goal] -> InferM ()
addGoals [Goal]
gs0
[Decl] -> InferM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return []
generalize bs0 :: [Decl]
bs0 gs0 :: [Goal]
gs0 =
do
[Goal]
gs <- [Goal] -> InferM [Goal]
applySubstGoals [Goal]
gs0
[Decl]
bs <- [Decl] -> (Decl -> InferM Decl) -> InferM [Decl]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Decl]
bs0 ((Decl -> InferM Decl) -> InferM [Decl])
-> (Decl -> InferM Decl) -> InferM [Decl]
forall a b. (a -> b) -> a -> b
$ \b :: Decl
b -> do Schema
s <- Schema -> InferM Schema
forall t. TVars t => t -> InferM t
applySubst (Decl -> Schema
dSignature Decl
b)
Decl -> InferM Decl
forall (m :: * -> *) a. Monad m => a -> m a
return Decl
b { dSignature :: Schema
dSignature = Schema
s }
let goalFVS :: Goal -> Set TVar
goalFVS g :: Goal
g = (TVar -> Bool) -> Set TVar -> Set TVar
forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV (Set TVar -> Set TVar) -> Set TVar -> Set TVar
forall a b. (a -> b) -> a -> b
$ Prop -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (Prop -> Set TVar) -> Prop -> Set TVar
forall a b. (a -> b) -> a -> b
$ Goal -> Prop
goal Goal
g
inGoals :: Set TVar
inGoals = [Set TVar] -> Set TVar
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set TVar] -> Set TVar) -> [Set TVar] -> Set TVar
forall a b. (a -> b) -> a -> b
$ (Goal -> Set TVar) -> [Goal] -> [Set TVar]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Set TVar
goalFVS [Goal]
gs
inSigs :: Set TVar
inSigs = (TVar -> Bool) -> Set TVar -> Set TVar
forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV (Set TVar -> Set TVar) -> Set TVar -> Set TVar
forall a b. (a -> b) -> a -> b
$ [Schema] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs ([Schema] -> Set TVar) -> [Schema] -> Set TVar
forall a b. (a -> b) -> a -> b
$ (Decl -> Schema) -> [Decl] -> [Schema]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> Schema
dSignature [Decl]
bs
candidates :: Set TVar
candidates = (Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set TVar
inGoals Set TVar
inSigs)
Set TVar
asmpVs <- InferM (Set TVar)
varsWithAsmps
let gen0 :: Set TVar
gen0 = Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set TVar
candidates Set TVar
asmpVs
stays :: Goal -> Bool
stays g :: Goal
g = (TVar -> Bool) -> [TVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
gen0) ([TVar] -> Bool) -> [TVar] -> Bool
forall a b. (a -> b) -> a -> b
$ Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (Set TVar -> [TVar]) -> Set TVar -> [TVar]
forall a b. (a -> b) -> a -> b
$ Goal -> Set TVar
goalFVS Goal
g
(here0 :: [Goal]
here0,later :: [Goal]
later) = (Goal -> Bool) -> [Goal] -> ([Goal], [Goal])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Goal -> Bool
stays [Goal]
gs
[Goal] -> InferM ()
addGoals [Goal]
later
let maybeAmbig :: [TVar]
maybeAmbig = Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set TVar
gen0 Set TVar
inSigs)
let (as0 :: [TVar]
as0,here1 :: [Goal]
here1,defSu :: Subst
defSu,ws :: [Warning]
ws) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
defaultAndSimplify [TVar]
maybeAmbig [Goal]
here0
Subst -> InferM ()
extendSubst Subst
defSu
(Warning -> InferM ()) -> [Warning] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Warning -> InferM ()
recordWarning [Warning]
ws
let here :: [Prop]
here = (Goal -> Prop) -> [Goal] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Prop
goal [Goal]
here1
let as :: [TVar]
as = (TVar -> TVar -> Ordering) -> [TVar] -> [TVar]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy TVar -> TVar -> Ordering
forall t t. (HasKind t, HasKind t) => t -> t -> Ordering
numFst
([TVar] -> [TVar]) -> [TVar] -> [TVar]
forall a b. (a -> b) -> a -> b
$ [TVar]
as0 [TVar] -> [TVar] -> [TVar]
forall a. [a] -> [a] -> [a]
++ Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set TVar
inSigs Set TVar
asmpVs)
asPs :: [TParam]
asPs = [ $WTParam :: Int -> Kind -> TPFlavor -> TVarInfo -> TParam
TParam { tpUnique :: Int
tpUnique = Int
x, tpKind :: Kind
tpKind = Kind
k, tpFlav :: TPFlavor
tpFlav = Maybe Name -> TPFlavor
TPOther Maybe Name
forall a. Maybe a
Nothing
, tpInfo :: TVarInfo
tpInfo = TVarInfo
i } | TVFree x :: Int
x k :: Kind
k _ i :: TVarInfo
i <- [TVar]
as ]
Subst
totSu <- InferM Subst
getSubst
let
su :: Subst
su = [(TVar, Prop)] -> Subst
listSubst ([TVar] -> [Prop] -> [(TVar, Prop)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TVar]
as ((TParam -> Prop) -> [TParam] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (TVar -> Prop
TVar (TVar -> Prop) -> (TParam -> TVar) -> TParam -> Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
tpVar) [TParam]
asPs)) Subst -> Subst -> Subst
@@ Subst
totSu
qs :: [Prop]
qs = (Prop -> [Prop]) -> [Prop] -> [Prop]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Prop -> [Prop]
pSplitAnd (Prop -> [Prop]) -> (Prop -> Prop) -> Prop -> [Prop]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> Prop -> Prop
forall t. TVars t => Subst -> t -> t
apSubst Subst
su) [Prop]
here
genE :: Expr -> Expr
genE e :: Expr
e = (TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs ((Prop -> Expr -> Expr) -> Expr -> [Prop] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Expr -> Expr
EProofAbs (Subst -> Expr -> Expr
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e) [Prop]
qs) [TParam]
asPs
genB :: Decl -> Decl
genB d :: Decl
d = Decl
d { dDefinition :: DeclDef
dDefinition = case Decl -> DeclDef
dDefinition Decl
d of
DExpr e :: Expr
e -> Expr -> DeclDef
DExpr (Expr -> Expr
genE Expr
e)
DPrim -> DeclDef
DPrim
, dSignature :: Schema
dSignature = [TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
asPs [Prop]
qs
(Prop -> Schema) -> Prop -> Schema
forall a b. (a -> b) -> a -> b
$ Subst -> Prop -> Prop
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Prop -> Prop) -> Prop -> Prop
forall a b. (a -> b) -> a -> b
$ Schema -> Prop
sType (Schema -> Prop) -> Schema -> Prop
forall a b. (a -> b) -> a -> b
$ Decl -> Schema
dSignature Decl
d
}
[Decl] -> InferM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Decl -> Decl) -> [Decl] -> [Decl]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> Decl
genB [Decl]
bs)
where
numFst :: t -> t -> Ordering
numFst x :: t
x y :: t
y = case (t -> Kind
forall t. HasKind t => t -> Kind
kindOf t
x, t -> Kind
forall t. HasKind t => t -> Kind
kindOf t
y) of
(KNum, KNum) -> Ordering
EQ
(KNum, _) -> Ordering
LT
(_,KNum) -> Ordering
GT
_ -> Ordering
EQ
checkMonoB :: P.Bind Name -> Type -> InferM Decl
checkMonoB :: Bind Name -> Prop -> InferM Decl
checkMonoB b :: Bind Name
b t :: Prop
t =
Maybe Range -> InferM Decl -> InferM Decl
forall a. Maybe Range -> InferM a -> InferM a
inRangeMb (Bind Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b) (InferM Decl -> InferM Decl) -> InferM Decl -> InferM Decl
forall a b. (a -> b) -> a -> b
$
case Located (BindDef Name) -> BindDef Name
forall a. Located a -> a
thing (Bind Name -> Located (BindDef Name)
forall name. Bind name -> Located (BindDef name)
P.bDef Bind Name
b) of
P.DPrim -> String -> [String] -> InferM Decl
forall a. HasCallStack => String -> [String] -> a
panic "checkMonoB" ["Primitive with no signature?"]
P.DExpr e :: Expr Name
e ->
do Expr
e1 <- Doc -> [Pattern Name] -> Expr Name -> Prop -> InferM Expr
checkFun (Name -> Doc
forall a. PP a => a -> Doc
pp (Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b))) (Bind Name -> [Pattern Name]
forall name. Bind name -> [Pattern name]
P.bParams Bind Name
b) Expr Name
e Prop
t
let f :: Name
f = Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
Decl -> InferM Decl
forall (m :: * -> *) a. Monad m => a -> m a
return $WDecl :: Name
-> Schema
-> DeclDef
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe String
-> Decl
Decl { dName :: Name
dName = Name
f
, dSignature :: Schema
dSignature = [TParam] -> [Prop] -> Prop -> Schema
Forall [] [] Prop
t
, dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr Expr
e1
, dPragmas :: [Pragma]
dPragmas = Bind Name -> [Pragma]
forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
, dInfix :: Bool
dInfix = Bind Name -> Bool
forall name. Bind name -> Bool
P.bInfix Bind Name
b
, dFixity :: Maybe Fixity
dFixity = Bind Name -> Maybe Fixity
forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
, dDoc :: Maybe String
dDoc = Bind Name -> Maybe String
forall name. Bind name -> Maybe String
P.bDoc Bind Name
b
}
checkSigB :: P.Bind Name -> (Schema,[Goal]) -> InferM Decl
checkSigB :: Bind Name -> (Schema, [Goal]) -> InferM Decl
checkSigB b :: Bind Name
b (Forall as :: [TParam]
as asmps0 :: [Prop]
asmps0 t0 :: Prop
t0, validSchema :: [Goal]
validSchema) = case Located (BindDef Name) -> BindDef Name
forall a. Located a -> a
thing (Bind Name -> Located (BindDef Name)
forall name. Bind name -> Located (BindDef name)
P.bDef Bind Name
b) of
P.DPrim ->
do Decl -> InferM Decl
forall (m :: * -> *) a. Monad m => a -> m a
return $WDecl :: Name
-> Schema
-> DeclDef
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe String
-> Decl
Decl { dName :: Name
dName = Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
, dSignature :: Schema
dSignature = [TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as [Prop]
asmps0 Prop
t0
, dDefinition :: DeclDef
dDefinition = DeclDef
DPrim
, dPragmas :: [Pragma]
dPragmas = Bind Name -> [Pragma]
forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
, dInfix :: Bool
dInfix = Bind Name -> Bool
forall name. Bind name -> Bool
P.bInfix Bind Name
b
, dFixity :: Maybe Fixity
dFixity = Bind Name -> Maybe Fixity
forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
, dDoc :: Maybe String
dDoc = Bind Name -> Maybe String
forall name. Bind name -> Maybe String
P.bDoc Bind Name
b
}
P.DExpr e0 :: Expr Name
e0 ->
Maybe Range -> InferM Decl -> InferM Decl
forall a. Maybe Range -> InferM a -> InferM a
inRangeMb (Bind Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b) (InferM Decl -> InferM Decl) -> InferM Decl -> InferM Decl
forall a b. (a -> b) -> a -> b
$
[TParam] -> InferM Decl -> InferM Decl
forall a. [TParam] -> InferM a -> InferM a
withTParams [TParam]
as (InferM Decl -> InferM Decl) -> InferM Decl -> InferM Decl
forall a b. (a -> b) -> a -> b
$
do (e1 :: Expr
e1,cs0 :: [Goal]
cs0) <- InferM Expr -> InferM (Expr, [Goal])
forall a. InferM a -> InferM (a, [Goal])
collectGoals (InferM Expr -> InferM (Expr, [Goal]))
-> InferM Expr -> InferM (Expr, [Goal])
forall a b. (a -> b) -> a -> b
$
do Expr
e1 <- Doc -> [Pattern Name] -> Expr Name -> Prop -> InferM Expr
checkFun (Name -> Doc
forall a. PP a => a -> Doc
pp (Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b))) (Bind Name -> [Pattern Name]
forall name. Bind name -> [Pattern name]
P.bParams Bind Name
b) Expr Name
e0 Prop
t0
[Goal] -> InferM ()
addGoals [Goal]
validSchema
() <- InferM ()
simplifyAllConstraints
Expr -> InferM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e1
[Goal]
cs <- [Goal] -> InferM [Goal]
applySubstGoals [Goal]
cs0
let findKeep :: Set a -> [a] -> [(a, Set a)] -> ([a], [a])
findKeep vs :: Set a
vs keep :: [a]
keep todo :: [(a, Set a)]
todo =
let stays :: (a, Set a) -> Bool
stays (_,cvs :: Set a
cvs) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set a -> Bool
forall a. Set a -> Bool
Set.null (Set a -> Bool) -> Set a -> Bool
forall a b. (a -> b) -> a -> b
$ Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set a
vs Set a
cvs
(yes :: [(a, Set a)]
yes,perhaps :: [(a, Set a)]
perhaps) = ((a, Set a) -> Bool)
-> [(a, Set a)] -> ([(a, Set a)], [(a, Set a)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (a, Set a) -> Bool
forall a. (a, Set a) -> Bool
stays [(a, Set a)]
todo
(stayPs :: [a]
stayPs,newVars :: [Set a]
newVars) = [(a, Set a)] -> ([a], [Set a])
forall a b. [(a, b)] -> ([a], [b])
unzip [(a, Set a)]
yes
in case [a]
stayPs of
[] -> ([a]
keep,((a, Set a) -> a) -> [(a, Set a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, Set a) -> a
forall a b. (a, b) -> a
fst [(a, Set a)]
todo)
_ -> Set a -> [a] -> [(a, Set a)] -> ([a], [a])
findKeep ([Set a] -> Set a
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (Set a
vsSet a -> [Set a] -> [Set a]
forall a. a -> [a] -> [a]
:[Set a]
newVars)) ([a]
stayPs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
keep) [(a, Set a)]
perhaps
let (stay :: [Goal]
stay,leave :: [Goal]
leave) = Set TVar -> [Goal] -> [(Goal, Set TVar)] -> ([Goal], [Goal])
forall a a. Ord a => Set a -> [a] -> [(a, Set a)] -> ([a], [a])
findKeep ([TVar] -> Set TVar
forall a. Ord a => [a] -> Set a
Set.fromList ((TParam -> TVar) -> [TParam] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar [TParam]
as)) []
[ (Goal
c, Goal -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Goal
c) | Goal
c <- [Goal]
cs ]
[Goal] -> InferM ()
addGoals [Goal]
leave
[Prop]
asmps1 <- [Prop] -> InferM [Prop]
applySubstPreds [Prop]
asmps0
Subst
su <- Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication (Name -> Maybe Name
forall a. a -> Maybe a
Just (Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b))) [TParam]
as [Prop]
asmps1 [Goal]
stay
Subst -> InferM ()
extendSubst Subst
su
let asmps :: [Prop]
asmps = (Prop -> [Prop]) -> [Prop] -> [Prop]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Prop -> [Prop]
pSplitAnd (Subst -> [Prop] -> [Prop]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Prop]
asmps1)
Prop
t <- Prop -> InferM Prop
forall t. TVars t => t -> InferM t
applySubst Prop
t0
Expr
e2 <- Expr -> InferM Expr
forall t. TVars t => t -> InferM t
applySubst Expr
e1
Decl -> InferM Decl
forall (m :: * -> *) a. Monad m => a -> m a
return $WDecl :: Name
-> Schema
-> DeclDef
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe String
-> Decl
Decl
{ dName :: Name
dName = Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
, dSignature :: Schema
dSignature = [TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as [Prop]
asmps Prop
t
, dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr ((TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs ((Prop -> Expr -> Expr) -> Expr -> [Prop] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Expr -> Expr
EProofAbs Expr
e2 [Prop]
asmps) [TParam]
as)
, dPragmas :: [Pragma]
dPragmas = Bind Name -> [Pragma]
forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
, dInfix :: Bool
dInfix = Bind Name -> Bool
forall name. Bind name -> Bool
P.bInfix Bind Name
b
, dFixity :: Maybe Fixity
dFixity = Bind Name -> Maybe Fixity
forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
, dDoc :: Maybe String
dDoc = Bind Name -> Maybe String
forall name. Bind name -> Maybe String
P.bDoc Bind Name
b
}
inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a
inferDs :: [d] -> ([DeclGroup] -> InferM a) -> InferM a
inferDs ds :: [d]
ds continue :: [DeclGroup] -> InferM a
continue = [TyDecl] -> InferM a
checkTyDecls ([TyDecl] -> InferM a) -> InferM [TyDecl] -> InferM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TyDecl] -> InferM [TyDecl]
orderTyDecls ((d -> Maybe TyDecl) -> [d] -> [TyDecl]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe d -> Maybe TyDecl
forall d. FromDecl d => d -> Maybe TyDecl
toTyDecl [d]
ds)
where
isTopLevel :: Bool
isTopLevel = d -> Bool
forall d. FromDecl d => d -> Bool
isTopDecl ([d] -> d
forall a. [a] -> a
head [d]
ds)
checkTyDecls :: [TyDecl] -> InferM a
checkTyDecls (AT t :: ParameterType Name
t mbD :: Maybe String
mbD : ts :: [TyDecl]
ts) =
do ModTParam
t1 <- ParameterType Name -> Maybe String -> InferM ModTParam
checkParameterType ParameterType Name
t Maybe String
mbD
ModTParam -> InferM a -> InferM a
forall a. ModTParam -> InferM a -> InferM a
withParamType ModTParam
t1 ([TyDecl] -> InferM a
checkTyDecls [TyDecl]
ts)
checkTyDecls (TS t :: TySyn Name
t mbD :: Maybe String
mbD : ts :: [TyDecl]
ts) =
do TySyn
t1 <- TySyn Name -> Maybe String -> InferM TySyn
checkTySyn TySyn Name
t Maybe String
mbD
TySyn -> InferM a -> InferM a
forall a. TySyn -> InferM a -> InferM a
withTySyn TySyn
t1 ([TyDecl] -> InferM a
checkTyDecls [TyDecl]
ts)
checkTyDecls (PS t :: PropSyn Name
t mbD :: Maybe String
mbD : ts :: [TyDecl]
ts) =
do TySyn
t1 <- PropSyn Name -> Maybe String -> InferM TySyn
checkPropSyn PropSyn Name
t Maybe String
mbD
TySyn -> InferM a -> InferM a
forall a. TySyn -> InferM a -> InferM a
withTySyn TySyn
t1 ([TyDecl] -> InferM a
checkTyDecls [TyDecl]
ts)
checkTyDecls (NT t :: Newtype Name
t mbD :: Maybe String
mbD : ts :: [TyDecl]
ts) =
do Newtype
t1 <- Newtype Name -> Maybe String -> InferM Newtype
checkNewtype Newtype Name
t Maybe String
mbD
Newtype -> InferM a -> InferM a
forall a. Newtype -> InferM a -> InferM a
withNewtype Newtype
t1 ([TyDecl] -> InferM a
checkTyDecls [TyDecl]
ts)
checkTyDecls (PT p :: PrimType Name
p mbD :: Maybe String
mbD : ts :: [TyDecl]
ts) =
do AbstractType
p1 <- PrimType Name -> Maybe String -> InferM AbstractType
checkPrimType PrimType Name
p Maybe String
mbD
AbstractType -> InferM a -> InferM a
forall a. AbstractType -> InferM a -> InferM a
withPrimType AbstractType
p1 ([TyDecl] -> InferM a
checkTyDecls [TyDecl]
ts)
checkTyDecls [] =
do [Located Prop]
cs <- [Located (Prop Name)] -> InferM [Located Prop]
checkParameterConstraints ((d -> [Located (Prop Name)]) -> [d] -> [Located (Prop Name)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap d -> [Located (Prop Name)]
forall d. FromDecl d => d -> [Located (Prop Name)]
toParamConstraints [d]
ds)
[Located Prop] -> InferM a -> InferM a
forall a. [Located Prop] -> InferM a -> InferM a
withParameterConstraints [Located Prop]
cs (InferM a -> InferM a) -> InferM a -> InferM a
forall a b. (a -> b) -> a -> b
$
do [ModVParam]
xs <- (ParameterFun Name -> InferM ModVParam)
-> [ParameterFun Name] -> InferM [ModVParam]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ParameterFun Name -> InferM ModVParam
checkParameterFun ((d -> Maybe (ParameterFun Name)) -> [d] -> [ParameterFun Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe d -> Maybe (ParameterFun Name)
forall d. FromDecl d => d -> Maybe (ParameterFun Name)
toParamFun [d]
ds)
[ModVParam] -> InferM a -> InferM a
forall a. [ModVParam] -> InferM a -> InferM a
withParamFuns [ModVParam]
xs (InferM a -> InferM a) -> InferM a -> InferM a
forall a b. (a -> b) -> a -> b
$ [DeclGroup] -> [SCC (Bind Name)] -> InferM a
checkBinds [] ([SCC (Bind Name)] -> InferM a) -> [SCC (Bind Name)] -> InferM a
forall a b. (a -> b) -> a -> b
$ [Bind Name] -> [SCC (Bind Name)]
orderBinds ([Bind Name] -> [SCC (Bind Name)])
-> [Bind Name] -> [SCC (Bind Name)]
forall a b. (a -> b) -> a -> b
$ (d -> Maybe (Bind Name)) -> [d] -> [Bind Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe d -> Maybe (Bind Name)
forall d. FromDecl d => d -> Maybe (Bind Name)
toBind [d]
ds
checkParameterFun :: ParameterFun Name -> InferM ModVParam
checkParameterFun x :: ParameterFun Name
x =
do (s :: Schema
s,gs :: [Goal]
gs) <- AllowWildCards -> Schema Name -> InferM (Schema, [Goal])
checkSchema AllowWildCards
NoWildCards (ParameterFun Name -> Schema Name
forall name. ParameterFun name -> Schema name
P.pfSchema ParameterFun Name
x)
Subst
su <- Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication (Name -> Maybe Name
forall a. a -> Maybe a
Just (Located Name -> Name
forall a. Located a -> a
thing (ParameterFun Name -> Located Name
forall name. ParameterFun name -> Located name
P.pfName ParameterFun Name
x)))
(Schema -> [TParam]
sVars Schema
s) (Schema -> [Prop]
sProps Schema
s) [Goal]
gs
Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Subst -> Bool
isEmptySubst Subst
su) (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
String -> [String] -> InferM ()
forall a. HasCallStack => String -> [String] -> a
panic "checkParameterFun" ["Subst not empty??"]
let n :: Name
n = Located Name -> Name
forall a. Located a -> a
thing (ParameterFun Name -> Located Name
forall name. ParameterFun name -> Located name
P.pfName ParameterFun Name
x)
ModVParam -> InferM ModVParam
forall (m :: * -> *) a. Monad m => a -> m a
return ModVParam :: Name -> Schema -> Maybe String -> Maybe Fixity -> ModVParam
ModVParam { mvpName :: Name
mvpName = Name
n
, mvpType :: Schema
mvpType = Schema
s
, mvpDoc :: Maybe String
mvpDoc = ParameterFun Name -> Maybe String
forall name. ParameterFun name -> Maybe String
P.pfDoc ParameterFun Name
x
, mvpFixity :: Maybe Fixity
mvpFixity = ParameterFun Name -> Maybe Fixity
forall name. ParameterFun name -> Maybe Fixity
P.pfFixity ParameterFun Name
x
}
checkBinds :: [DeclGroup] -> [SCC (Bind Name)] -> InferM a
checkBinds decls :: [DeclGroup]
decls (CyclicSCC bs :: [Bind Name]
bs : more :: [SCC (Bind Name)]
more) =
do [Decl]
bs1 <- Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferBinds Bool
isTopLevel Bool
True [Bind Name]
bs
(Decl -> InferM a -> InferM a) -> InferM a -> [Decl] -> InferM a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\b :: Decl
b m :: InferM a
m -> Name -> Schema -> InferM a -> InferM a
forall a. Name -> Schema -> InferM a -> InferM a
withVar (Decl -> Name
dName Decl
b) (Decl -> Schema
dSignature Decl
b) InferM a
m)
([DeclGroup] -> [SCC (Bind Name)] -> InferM a
checkBinds ([Decl] -> DeclGroup
Recursive [Decl]
bs1 DeclGroup -> [DeclGroup] -> [DeclGroup]
forall a. a -> [a] -> [a]
: [DeclGroup]
decls) [SCC (Bind Name)]
more)
[Decl]
bs1
checkBinds decls :: [DeclGroup]
decls (AcyclicSCC c :: Bind Name
c : more :: [SCC (Bind Name)]
more) =
do ~[b :: Decl
b] <- Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferBinds Bool
isTopLevel Bool
False [Bind Name
c]
Name -> Schema -> InferM a -> InferM a
forall a. Name -> Schema -> InferM a -> InferM a
withVar (Decl -> Name
dName Decl
b) (Decl -> Schema
dSignature Decl
b) (InferM a -> InferM a) -> InferM a -> InferM a
forall a b. (a -> b) -> a -> b
$
[DeclGroup] -> [SCC (Bind Name)] -> InferM a
checkBinds (Decl -> DeclGroup
NonRecursive Decl
b DeclGroup -> [DeclGroup] -> [DeclGroup]
forall a. a -> [a] -> [a]
: [DeclGroup]
decls) [SCC (Bind Name)]
more
checkBinds decls :: [DeclGroup]
decls [] = [DeclGroup] -> InferM a
continue ([DeclGroup] -> [DeclGroup]
forall a. [a] -> [a]
reverse [DeclGroup]
decls)
tcPanic :: String -> [String] -> a
tcPanic :: String -> [String] -> a
tcPanic l :: String
l msg :: [String]
msg = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic ("[TypeCheck] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l) [String]
msg