{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE BlockArguments #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Redundant <$>" #-}
{-# HLINT ignore "Redundant <&>" #-}
module Cryptol.TypeCheck.Infer
( checkE
, checkSigB
, inferTopModule
, inferBinds
, checkTopDecls
)
where
import Data.Text(Text)
import qualified Data.Text as Text
import Cryptol.ModuleSystem.Name (lookupPrimDecl,nameLoc, nameIdent)
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,
checkPropGuards)
import Cryptol.TypeCheck.Instantiate
import Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),isEmptySubst)
import Cryptol.TypeCheck.Unify(rootPath)
import Cryptol.TypeCheck.Module
import Cryptol.TypeCheck.FFI
import Cryptol.TypeCheck.FFI.FFIType
import Cryptol.Utils.Ident
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.RecordMap
import Cryptol.IR.TraverseNames(mapNames)
import Cryptol.Utils.PP (pp)
import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Set as Set
import Data.List(foldl', sortBy, groupBy, partition)
import Data.Either(partitionEithers)
import Data.Maybe(isJust, fromMaybe, mapMaybe)
import Data.Ratio(numerator,denominator)
import Data.Traversable(forM)
import Data.Function(on)
import Control.Monad(zipWithM, unless, foldM, forM_, mplus, zipWithM,
unless, foldM, forM_, mplus, when)
inferTopModule :: P.Module Name -> InferM TCTopEntity
inferTopModule :: Module Name -> InferM TCTopEntity
inferTopModule Module Name
m =
case forall mname name. ModuleG mname name -> ModuleDefinition name
P.mDef Module Name
m of
P.NormalModule [TopDecl Name]
ds ->
do ModName -> ExportSpec Name -> InferM ()
newModuleScope (forall a. Located a -> a
thing (forall mname name. ModuleG mname name -> Located mname
P.mName Module Name
m)) (forall name. Ord name => [TopDecl name] -> ExportSpec name
P.exportedDecls [TopDecl Name]
ds)
[TopDecl Name] -> InferM ()
checkTopDecls [TopDecl Name]
ds
InferM ()
proveModuleTopLevel
InferM TCTopEntity
endModule
P.FunctorInstance Located (ImpName Name)
f ModuleInstanceArgs Name
as ModuleInstance Name
inst ->
do Maybe TCTopEntity
mb <- Located (ImpName Name)
-> Located (ImpName Name)
-> ModuleInstanceArgs Name
-> ModuleInstance Name
-> Maybe Text
-> InferM (Maybe TCTopEntity)
doFunctorInst (forall name. ModName -> ImpName name
P.ImpTop forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall mname name. ModuleG mname name -> Located mname
P.mName Module Name
m) Located (ImpName Name)
f ModuleInstanceArgs Name
as ModuleInstance Name
inst forall a. Maybe a
Nothing
case Maybe TCTopEntity
mb of
Just TCTopEntity
mo -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TCTopEntity
mo
Maybe TCTopEntity
Nothing -> forall a. HasCallStack => String -> [String] -> a
panic String
"inferModule" [String
"Didnt' get a module"]
P.InterfaceModule Signature Name
sig ->
do ModName -> InferM ()
newTopSignatureScope (forall a. Located a -> a
thing (forall mname name. ModuleG mname name -> Located mname
P.mName Module Name
m))
Signature Name -> InferM ()
checkSignature Signature Name
sig
InferM TCTopEntity
endTopSignature
mkPrim :: String -> InferM (P.Expr Name)
mkPrim :: String -> InferM (Expr Name)
mkPrim String
str =
do Name
nm <- String -> InferM Name
mkPrim' String
str
forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Expr n
P.EVar Name
nm)
mkPrim' :: String -> InferM Name
mkPrim' :: String -> InferM Name
mkPrim' String
str =
do PrimMap
prims <- InferM PrimMap
getPrimMap
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimIdent -> PrimMap -> Name
lookupPrimDecl (Text -> PrimIdent
prelPrim (String -> Text
Text.pack String
str)) PrimMap
prims)
desugarLiteral :: P.Literal -> InferM (P.Expr Name)
desugarLiteral :: Literal -> InferM (Expr Name)
desugarLiteral Literal
lit =
do Range
l <- InferM Range
curRange
Expr Name
numberPrim <- String -> InferM (Expr Name)
mkPrim String
"number"
Expr Name
fracPrim <- String -> InferM (Expr Name)
mkPrim String
"fraction"
let named :: (String, Type name) -> TypeInst name
named (String
x,Type name
y) = forall name. Named (Type name) -> TypeInst name
P.NamedInst
P.Named { name :: Located Ident
name = 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 [(String, Type Name)]
fs = forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
numberPrim (forall a b. (a -> b) -> [a] -> [b]
map forall {name}. (String, Type name) -> TypeInst name
named [(String, Type Name)]
fs)
tBits :: Integer -> Type n
tBits Integer
n = forall n. Type n -> Type n -> Type n
P.TSeq (forall n. Integer -> Type n
P.TNum Integer
n) forall n. Type n
P.TBit
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Literal
lit of
P.ECNum Integer
num NumInfo
info ->
[(String, Type Name)] -> Expr Name
number forall a b. (a -> b) -> a -> b
$ [ (String
"val", forall n. Integer -> Type n
P.TNum Integer
num) ] forall a. [a] -> [a] -> [a]
++ case NumInfo
info of
P.BinLit Text
_ Int
n -> [ (String
"rep", forall n. Integer -> Type n
tBits (Integer
1 forall a. Num a => a -> a -> a
* forall a. Integral a => a -> Integer
toInteger Int
n)) ]
P.OctLit Text
_ Int
n -> [ (String
"rep", forall n. Integer -> Type n
tBits (Integer
3 forall a. Num a => a -> a -> a
* forall a. Integral a => a -> Integer
toInteger Int
n)) ]
P.HexLit Text
_ Int
n -> [ (String
"rep", forall n. Integer -> Type n
tBits (Integer
4 forall a. Num a => a -> a -> a
* forall a. Integral a => a -> Integer
toInteger Int
n)) ]
P.DecLit Text
_ -> [ ]
P.PolyLit Int
_n -> [ (String
"rep", forall n. Type n -> Type n -> Type n
P.TSeq forall n. Type n
P.TWild forall n. Type n
P.TBit) ]
P.ECFrac Rational
fr FracInfo
info ->
let arg :: (Rational -> Integer) -> TypeInst name
arg Rational -> Integer
f = forall name. Type name -> TypeInst name
P.PosInst (forall n. Integer -> Type n
P.TNum (Rational -> Integer
f Rational
fr))
rnd :: TypeInst name
rnd = forall name. Type name -> TypeInst name
P.PosInst (forall n. Integer -> Type n
P.TNum (case FracInfo
info of
P.DecFrac Text
_ -> Integer
0
P.BinFrac Text
_ -> Integer
1
P.OctFrac Text
_ -> Integer
1
P.HexFrac Text
_ -> Integer
1))
in forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
fracPrim [ forall {name}. (Rational -> Integer) -> TypeInst name
arg forall a. Ratio a -> a
numerator, forall {name}. (Rational -> Integer) -> TypeInst name
arg forall a. Ratio a -> a
denominator, forall {name}. TypeInst name
rnd ]
P.ECChar Char
c ->
[(String, Type Name)] -> Expr Name
number [ (String
"val", forall n. Integer -> Type n
P.TNum (forall a. Integral a => a -> Integer
toInteger (forall a. Enum a => a -> Int
fromEnum Char
c)))
, (String
"rep", forall n. Integer -> Type n
tBits (Integer
8 :: Integer)) ]
P.ECString String
s ->
forall n. Expr n -> Type n -> Expr n
P.ETyped (forall n. [Expr n] -> Expr n
P.EList [ forall n. Literal -> Expr n
P.ELit (Char -> Literal
P.ECChar Char
c) | Char
c <- String
s ])
(forall n. Type n -> Type n -> Type n
P.TSeq forall n. Type n
P.TWild (forall n. Type n -> Type n -> Type n
P.TSeq (forall n. Integer -> Type n
P.TNum Integer
8) forall n. Type n
P.TBit))
appTys :: P.Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys :: Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
expr [TypeArg]
ts TypeWithSource
tGoal =
case Expr Name
expr of
P.EVar Name
x ->
do VarType
res <- Name -> InferM VarType
lookupVar Name
x
(Expr
e',Prop
t) <- case VarType
res of
ExtVar Schema
s -> Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Prop)
instantiateWith Name
x (Name -> Expr
EVar Name
x) Schema
s [TypeArg]
ts
CurSCC Expr
e Prop
t -> do [TypeArg] -> InferM ()
checkNoParams [TypeArg]
ts
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e,Prop
t)
Prop -> TypeWithSource -> InferM ()
checkHasType Prop
t TypeWithSource
tGoal
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'
P.ELit Literal
l -> do Expr Name
e <- Literal -> InferM (Expr Name)
desugarLiteral Literal
l
Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg]
ts TypeWithSource
tGoal
P.EAppT Expr Name
e [TypeInst Name]
fs -> Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e (forall a b. (a -> b) -> [a] -> [b]
map TypeInst Name -> TypeArg
uncheckedTypeArg [TypeInst Name]
fs forall a. [a] -> [a] -> [a]
++ [TypeArg]
ts) TypeWithSource
tGoal
P.EWhere Expr Name
e [Decl Name]
ds ->
do (Expr
e1,[DeclGroup]
ds1) <- forall a. [Decl Name] -> InferM a -> InferM (a, [DeclGroup])
checkLocalDecls [Decl Name]
ds (Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg]
ts TypeWithSource
tGoal)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> [DeclGroup] -> Expr
EWhere Expr
e1 [DeclGroup]
ds1)
P.ELocated Expr Name
e Range
r ->
do Expr
e' <- forall a. Range -> InferM a -> InferM a
inRange Range
r (Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg]
ts TypeWithSource
tGoal)
Bool
cs <- InferM Bool
getCallStacks
if Bool
cs then forall (f :: * -> *) a. Applicative f => a -> f a
pure (Range -> Expr -> Expr
ELocated Range
r Expr
e') else forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e'
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.EFromToBy {} -> InferM Expr
mono
P.EFromToDownBy {} -> InferM Expr
mono
P.EFromToLessThan {} -> 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.EPrefix {} -> InferM Expr
mono
P.EParens Expr Name
e -> Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg]
ts TypeWithSource
tGoal
P.EInfix Expr Name
a Located Name
op Fixity
_ Expr Name
b -> Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys (forall n. n -> Expr n
P.EVar (forall a. Located a -> a
thing Located Name
op) forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
a forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
b) [TypeArg]
ts TypeWithSource
tGoal
where mono :: InferM Expr
mono = do Expr
e' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
expr TypeWithSource
tGoal
[TypeArg] -> InferM ()
checkNoParams [TypeArg]
ts
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'
checkNoParams :: [TypeArg] -> InferM ()
checkNoParams :: [TypeArg] -> InferM ()
checkNoParams [TypeArg]
ts =
case [TypeArg]
pos of
TypeArg
p : [TypeArg]
_ -> do Range
r <- case TypeArg -> MaybeCheckedType
tyArgType TypeArg
p of
Unchecked Type Name
t | Just Range
r <- forall t. HasLoc t => t -> Maybe Range
getLoc Type Name
t -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Range
r
MaybeCheckedType
_ -> InferM Range
curRange
forall a. Range -> InferM a -> InferM a
inRange Range
r (Error -> InferM ()
recordError Error
TooManyPositionalTypeParams)
[TypeArg]
_ -> 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 TypeArg
l =
case TypeArg -> Maybe (Located Ident)
tyArgName TypeArg
l of
Just Located Ident
i -> Error -> InferM ()
recordError (Located Ident -> Error
UndefinedTypeParameter Located Ident
i)
Maybe (Located Ident)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
([TypeArg]
named,[TypeArg]
pos) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (forall a. Maybe a -> Bool
isJust 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 Type Name
ty Kind
k = Type Name -> Maybe Kind -> InferM Prop
checkType Type Name
ty (forall a. a -> Maybe a
Just Kind
k)
checkE :: P.Expr Name -> TypeWithSource -> InferM Expr
checkE :: Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
expr TypeWithSource
tGoal =
case Expr Name
expr of
P.EVar Name
x ->
do VarType
res <- Name -> InferM VarType
lookupVar Name
x
(Expr
e',Prop
t) <- case VarType
res of
ExtVar Schema
s -> Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Prop)
instantiateWith Name
x (Name -> Expr
EVar Name
x) Schema
s []
CurSCC Expr
e Prop
t -> forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Prop
t)
Prop -> TypeWithSource -> InferM ()
checkHasType Prop
t TypeWithSource
tGoal
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'
P.EGenerate Expr Name
e ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"generate"
Expr Name -> TypeWithSource -> InferM Expr
checkE (forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e) TypeWithSource
tGoal
P.ELit l :: Literal
l@(P.ECNum Integer
_ (P.DecLit Text
_)) ->
do Expr Name
e <- Literal -> InferM (Expr Name)
desugarLiteral Literal
l
Range
loc <- InferM Range
curRange
let arg :: TypeArg
arg = TypeArg { tyArgName :: Maybe (Located Ident)
tyArgName = forall a. a -> Maybe a
Just (forall a. Range -> a -> Located a
Located Range
loc (String -> Ident
packIdent String
"rep"))
, tyArgType :: MaybeCheckedType
tyArgType = Prop -> MaybeCheckedType
Checked (TypeWithSource -> Prop
twsType TypeWithSource
tGoal)
}
Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg
arg] TypeWithSource
tGoal
P.ELit Literal
l -> (Expr Name -> TypeWithSource -> InferM Expr
`checkE` TypeWithSource
tGoal) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Literal -> InferM (Expr Name)
desugarLiteral Literal
l
P.ETuple [Expr Name]
es ->
do [Prop]
etys <- Int -> TypeWithSource -> InferM [Prop]
expectTuple (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr Name]
es) TypeWithSource
tGoal
let mkTGoal :: Int -> Prop -> t -> TypeWithSource
mkTGoal Int
n Prop
t t
e = Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
t (Int -> TypeSource
TypeOfTupleField Int
n) (forall t. HasLoc t => t -> Maybe Range
getLoc t
e)
[Expr]
es' <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Expr Name -> TypeWithSource -> InferM Expr
checkE [Expr Name]
es (forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 forall {t}. HasLoc t => Int -> Prop -> t -> TypeWithSource
mkTGoal [Int
1..] [Prop]
etys [Expr Name]
es)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Expr
ETuple [Expr]
es')
P.ERecord Rec (Expr Name)
fs ->
do RecordMap Ident (Expr Name, Prop)
es <- forall a.
RecordMap Ident (Range, a)
-> TypeWithSource -> InferM (RecordMap Ident (a, Prop))
expectRec Rec (Expr Name)
fs TypeWithSource
tGoal
let checkField :: Ident -> (Expr Name, Prop) -> InferM Expr
checkField Ident
f (Expr Name
e,Prop
t) =
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
t (Ident -> TypeSource
TypeOfRecordField Ident
f) (forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e))
RecordMap Ident Expr
es' <- forall (t :: * -> *) a b c.
Applicative t =>
(a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
traverseRecordMap Ident -> (Expr Name, Prop) -> InferM Expr
checkField RecordMap Ident (Expr Name, Prop)
es
forall (m :: * -> *) a. Monad m => a -> m a
return (RecordMap Ident Expr -> Expr
ERec RecordMap Ident Expr
es')
P.EUpd Maybe (Expr Name)
x [UpdField Name]
fs -> Maybe (Expr Name)
-> [UpdField Name] -> TypeWithSource -> InferM Expr
checkRecUpd Maybe (Expr Name)
x [UpdField Name]
fs TypeWithSource
tGoal
P.ESel Expr Name
e Selector
l ->
do let src :: TypeSource
src = Selector -> TypeSource
selSrc Selector
l
Prop
t <- TypeSource -> Kind -> InferM Prop
newType TypeSource
src Kind
KType
Expr
e' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
t TypeSource
src (forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
expr))
HasGoalSln
f <- Selector -> Prop -> Prop -> InferM HasGoalSln
newHasGoal Selector
l Prop
t (TypeWithSource -> Prop
twsType TypeWithSource
tGoal)
forall (m :: * -> *) a. Monad m => a -> m a
return (HasGoalSln -> Expr -> Expr
hasDoSelect HasGoalSln
f Expr
e')
P.EList [] ->
do (Prop
len,Prop
a) <- TypeWithSource -> InferM (Prop, Prop)
expectSeq TypeWithSource
tGoal
Int -> TypeWithSource -> InferM ()
expectFin Int
0 (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
len TypeSource
LenOfSeq (forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
expr))
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Prop -> Expr
EList [] Prop
a)
P.EList [Expr Name]
es ->
do (Prop
len,Prop
a) <- TypeWithSource -> InferM (Prop, Prop)
expectSeq TypeWithSource
tGoal
Int -> TypeWithSource -> InferM ()
expectFin (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr Name]
es) (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
len TypeSource
LenOfSeq (forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
expr))
let checkElem :: Expr Name -> InferM Expr
checkElem Expr Name
e = Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
a TypeSource
TypeOfSeqElement (forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e))
[Expr]
es' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Expr Name -> InferM Expr
checkElem [Expr Name]
es
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Prop -> Expr
EList [Expr]
es' Prop
a)
P.EFromToBy Bool
isStrict Type Name
t1 Type Name
t2 Type Name
t3 Maybe (Type Name)
mety
| Bool
isStrict ->
do Range
l <- InferM Range
curRange
let fs :: [(String, Type Name)]
fs = [(String
"first",Type Name
t1),(String
"bound",Type Name
t2),(String
"stride",Type Name
t3)] forall a. [a] -> [a] -> [a]
++
case Maybe (Type Name)
mety of
Just Type Name
ety -> [(String
"a",Type Name
ety)]
Maybe (Type Name)
Nothing -> []
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToByLessThan"
let e' :: Expr Name
e' = forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[ forall name. Named (Type name) -> TypeInst name
P.NamedInst P.Named{ name :: Located Ident
name = forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
| (String
x,Type Name
y) <- [(String, Type Name)]
fs
]
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal
| Bool
otherwise ->
do Range
l <- InferM Range
curRange
let fs :: [(String, Type Name)]
fs = [(String
"first",Type Name
t1),(String
"last",Type Name
t2),(String
"stride",Type Name
t3)] forall a. [a] -> [a] -> [a]
++
case Maybe (Type Name)
mety of
Just Type Name
ety -> [(String
"a",Type Name
ety)]
Maybe (Type Name)
Nothing -> []
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToBy"
let e' :: Expr Name
e' = forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[ forall name. Named (Type name) -> TypeInst name
P.NamedInst P.Named{ name :: Located Ident
name = forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
| (String
x,Type Name
y) <- [(String, Type Name)]
fs
]
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal
P.EFromToDownBy Bool
isStrict Type Name
t1 Type Name
t2 Type Name
t3 Maybe (Type Name)
mety
| Bool
isStrict ->
do Range
l <- InferM Range
curRange
let fs :: [(String, Type Name)]
fs = [(String
"first",Type Name
t1),(String
"bound",Type Name
t2),(String
"stride",Type Name
t3)] forall a. [a] -> [a] -> [a]
++
case Maybe (Type Name)
mety of
Just Type Name
ety -> [(String
"a",Type Name
ety)]
Maybe (Type Name)
Nothing -> []
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToDownByGreaterThan"
let e' :: Expr Name
e' = forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[ forall name. Named (Type name) -> TypeInst name
P.NamedInst P.Named{ name :: Located Ident
name = forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
| (String
x,Type Name
y) <- [(String, Type Name)]
fs
]
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal
| Bool
otherwise ->
do Range
l <- InferM Range
curRange
let fs :: [(String, Type Name)]
fs = [(String
"first",Type Name
t1),(String
"last",Type Name
t2),(String
"stride",Type Name
t3)] forall a. [a] -> [a] -> [a]
++
case Maybe (Type Name)
mety of
Just Type Name
ety -> [(String
"a",Type Name
ety)]
Maybe (Type Name)
Nothing -> []
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToDownBy"
let e' :: Expr Name
e' = forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[ forall name. Named (Type name) -> TypeInst name
P.NamedInst P.Named{ name :: Located Ident
name = forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
| (String
x,Type Name
y) <- [(String, Type Name)]
fs
]
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal
P.EFromToLessThan Type Name
t1 Type Name
t2 Maybe (Type Name)
mety ->
do Range
l <- InferM Range
curRange
let fs0 :: [(String, Type Name)]
fs0 =
case Maybe (Type Name)
mety of
Just Type Name
ety -> [(String
"a", Type Name
ety)]
Maybe (Type Name)
Nothing -> []
let fs :: [(String, Type Name)]
fs = [(String
"first", Type Name
t1), (String
"bound", Type Name
t2)] forall a. [a] -> [a] -> [a]
++ [(String, Type Name)]
fs0
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToLessThan"
let e' :: Expr Name
e' = forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[ forall name. Named (Type name) -> TypeInst name
P.NamedInst P.Named { name :: Located Ident
name = forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
| (String
x,Type Name
y) <- [(String, Type Name)]
fs
]
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal
P.EFromTo Type Name
t1 Maybe (Type Name)
mbt2 Type Name
t3 Maybe (Type Name)
mety ->
do Range
l <- InferM Range
curRange
let fs0 :: [(String, Type Name)]
fs0 =
case Maybe (Type Name)
mety of
Just Type Name
ety -> [(String
"a", Type Name
ety)]
Maybe (Type Name)
Nothing -> []
let (String
c,[(String, Type Name)]
fs) =
case Maybe (Type Name)
mbt2 of
Maybe (Type Name)
Nothing ->
(String
"fromTo", (String
"last", Type Name
t3) forall a. a -> [a] -> [a]
: [(String, Type Name)]
fs0)
Just Type Name
t2 ->
(String
"fromThenTo", (String
"next",Type Name
t2) forall a. a -> [a] -> [a]
: (String
"last",Type Name
t3) forall a. a -> [a] -> [a]
: [(String, Type Name)]
fs0)
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
c
let e' :: Expr Name
e' = forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[ forall name. Named (Type name) -> TypeInst name
P.NamedInst P.Named { name :: Located Ident
name = forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
| (String
x,Type Name
y) <- (String
"first",Type Name
t1) forall a. a -> [a] -> [a]
: [(String, Type Name)]
fs
]
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal
P.EInfFrom Expr Name
e1 Maybe (Expr Name)
Nothing ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"infFrom"
Expr Name -> TypeWithSource -> InferM Expr
checkE (forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e1) TypeWithSource
tGoal
P.EInfFrom Expr Name
e1 (Just Expr Name
e2) ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"infFromThen"
Expr Name -> TypeWithSource -> InferM Expr
checkE (forall n. Expr n -> Expr n -> Expr n
P.EApp (forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e1) Expr Name
e2) TypeWithSource
tGoal
P.EComp Expr Name
e [[Match Name]]
mss ->
do ([[Match]]
mss', [Map Name (Located Prop)]
dss, [Prop]
ts) <- forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` 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 [ Int
1 .. ] [[Match Name]]
mss
(Prop
len,Prop
a) <- TypeWithSource -> InferM (Prop, Prop)
expectSeq TypeWithSource
tGoal
Prop
inferred <- [Prop] -> InferM Prop
smallest [Prop]
ts
[Prop]
ctrs <- TypeWithSource -> Prop -> InferM [Prop]
unify (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
len TypeSource
LenOfSeq (forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
expr)) Prop
inferred
ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtComprehension [Prop]
ctrs
Map Name (Located Prop)
ds <- forall {m :: * -> *} {k} {a}.
(Monad m, Show k, Ord k) =>
[Map k (Located a)] -> m (Map k (Located a))
combineMaps [Map Name (Located Prop)]
dss
Expr
e' <- forall a. Map Name (Located Prop) -> InferM a -> InferM a
withMonoTypes Map Name (Located Prop)
ds (Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e
(Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
a TypeSource
TypeOfSeqElement (forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e)))
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop -> Prop -> Expr -> [[Match]] -> Expr
EComp Prop
len Prop
a Expr
e' [[Match]]
mss')
where
combineMaps :: [Map k (Located a)] -> m (Map k (Located a))
combineMaps [Map k (Located a)]
ms = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(k, [Range])]
bad
then forall (m :: * -> *) a. Monad m => a -> m a
return (forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions [Map k (Located a)]
ms)
else forall a. HasCallStack => String -> [String] -> a
panic String
"combineMaps" forall a b. (a -> b) -> a -> b
$ String
"Multiple definitions"
forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [(k, [Range])]
bad
where
bad :: [(k, [Range])]
bad = do Map k (Located a)
m <- [Map k (Located a)]
ms
[Located k] -> [(k, [Range])]
duplicates [ Located a
a { thing :: k
thing = k
x } | (k
x,Located a
a) <- forall k a. Map k a -> [(k, a)]
Map.toList Map k (Located a)
m ]
duplicates :: [Located k] -> [(k, [Range])]
duplicates = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {a}. [Located a] -> Maybe (a, [Range])
multiple
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a. Located a -> a
thing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a. Located a -> a
thing)
where
multiple :: [Located a] -> Maybe (a, [Range])
multiple xs :: [Located a]
xs@(Located a
x : Located a
_ : [Located a]
_) = forall a. a -> Maybe a
Just (forall a. Located a -> a
thing Located a
x, forall a b. (a -> b) -> [a] -> [b]
map forall a. Located a -> Range
srcRange [Located a]
xs)
multiple [Located a]
_ = forall a. Maybe a
Nothing
P.EAppT Expr Name
e [TypeInst Name]
fs -> Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e (forall a b. (a -> b) -> [a] -> [b]
map TypeInst Name -> TypeArg
uncheckedTypeArg [TypeInst Name]
fs) TypeWithSource
tGoal
P.EApp Expr Name
e1 Expr Name
e2 ->
do let argSrc :: TypeSource
argSrc = ArgDescr -> TypeSource
TypeOfArg ArgDescr
noArgDescr
Prop
t1 <- TypeSource -> Kind -> InferM Prop
newType TypeSource
argSrc Kind
KType
Expr
e1' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e1
(Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource (Prop -> Prop -> Prop
tFun Prop
t1 (TypeWithSource -> Prop
twsType TypeWithSource
tGoal)) TypeSource
FunApp (forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e1))
Expr
e2' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e2 (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
t1 TypeSource
argSrc (forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e2))
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
EApp Expr
e1' Expr
e2')
P.EIf Expr Name
e1 Expr Name
e2 Expr Name
e3 ->
do Expr
e1' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e1 (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
tBit TypeSource
TypeOfIfCondExpr (forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e1))
Expr
e2' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e2 TypeWithSource
tGoal
Expr
e3' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e3 TypeWithSource
tGoal
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
EIf Expr
e1' Expr
e2' Expr
e3')
P.EWhere Expr Name
e [Decl Name]
ds ->
do (Expr
e1,[DeclGroup]
ds1) <- forall a. [Decl Name] -> InferM a -> InferM (a, [DeclGroup])
checkLocalDecls [Decl Name]
ds (Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> [DeclGroup] -> Expr
EWhere Expr
e1 [DeclGroup]
ds1)
P.ETyped Expr Name
e Type Name
t ->
do Prop
tSig <- Type Name -> Kind -> InferM Prop
checkTypeOfKind Type Name
t Kind
KType
Expr
e' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
tSig TypeSource
TypeFromUserAnnotation (forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
expr))
Prop -> TypeWithSource -> InferM ()
checkHasType Prop
tSig TypeWithSource
tGoal
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'
P.ETypeVal Type Name
t ->
do Range
l <- InferM Range
curRange
Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"number"
Expr Name -> TypeWithSource -> InferM Expr
checkE (forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
[forall name. Named (Type name) -> TypeInst name
P.NamedInst
P.Named { name :: Located Ident
name = forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
"val")
, value :: Type Name
value = Type Name
t }]) TypeWithSource
tGoal
P.EFun FunDesc Name
desc [Pattern Name]
ps Expr Name
e -> FunDesc Name
-> [Pattern Name] -> Expr Name -> TypeWithSource -> InferM Expr
checkFun FunDesc Name
desc [Pattern Name]
ps Expr Name
e TypeWithSource
tGoal
P.ELocated Expr Name
e Range
r ->
do Expr
e' <- forall a. Range -> InferM a -> InferM a
inRange Range
r (Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal)
Bool
cs <- InferM Bool
getCallStacks
if Bool
cs then forall (f :: * -> *) a. Applicative f => a -> f a
pure (Range -> Expr -> Expr
ELocated Range
r Expr
e') else forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e'
P.ESplit Expr Name
e ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"splitAt"
Expr Name -> TypeWithSource -> InferM Expr
checkE (forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e) TypeWithSource
tGoal
P.EInfix Expr Name
a Located Name
op Fixity
_ Expr Name
b -> Expr Name -> TypeWithSource -> InferM Expr
checkE (forall n. n -> Expr n
P.EVar (forall a. Located a -> a
thing Located Name
op) forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
a forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
b) TypeWithSource
tGoal
P.EPrefix PrefixOp
op Expr Name
e ->
do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim case PrefixOp
op of
PrefixOp
P.PrefixNeg -> String
"negate"
PrefixOp
P.PrefixComplement -> String
"complement"
Expr Name -> TypeWithSource -> InferM Expr
checkE (forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e) TypeWithSource
tGoal
P.EParens Expr Name
e -> Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal
checkRecUpd ::
Maybe (P.Expr Name) -> [ P.UpdField Name ] -> TypeWithSource -> InferM Expr
checkRecUpd :: Maybe (Expr Name)
-> [UpdField Name] -> TypeWithSource -> InferM Expr
checkRecUpd Maybe (Expr Name)
mb [UpdField Name]
fs TypeWithSource
tGoal =
case Maybe (Expr Name)
mb of
Maybe (Expr Name)
Nothing ->
do Name
r <- Namespace -> Ident -> InferM Name
newLocalName Namespace
NSValue (String -> Ident
packIdent String
"r")
let p :: Pattern Name
p = forall n. Located n -> Pattern n
P.PVar Located { srcRange :: Range
srcRange = Name -> Range
nameLoc Name
r, thing :: Name
thing = Name
r }
fe :: Expr Name
fe = forall n. FunDesc n -> [Pattern n] -> Expr n -> Expr n
P.EFun forall n. FunDesc n
P.emptyFunDesc [Pattern Name
p] (forall n. Maybe (Expr n) -> [UpdField n] -> Expr n
P.EUpd (forall a. a -> Maybe a
Just (forall n. n -> Expr n
P.EVar Name
r)) [UpdField Name]
fs)
Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
fe TypeWithSource
tGoal
Just Expr Name
e ->
do Expr
e1 <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal
forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Expr, Maybe Range) -> UpdField Name -> InferM (Expr, Maybe Range)
doUpd (Expr
e1, forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e) [UpdField Name]
fs
where
doUpd :: (Expr, Maybe Range) -> UpdField Name -> InferM (Expr, Maybe Range)
doUpd (Expr
e,Maybe Range
eloc) (P.UpdField UpdHow
how [Located Selector]
sels Expr Name
v) =
case [Located Selector]
sels of
[Located Selector
l] ->
case UpdHow
how of
UpdHow
P.UpdSet ->
do let src :: TypeSource
src = Selector -> TypeSource
selSrc Selector
s
Prop
ft <- TypeSource -> Kind -> InferM Prop
newType TypeSource
src Kind
KType
Expr
v1 <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
v (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
ft TypeSource
src Maybe Range
eloc)
HasGoalSln
d <- Selector -> Prop -> Prop -> InferM HasGoalSln
newHasGoal Selector
s (TypeWithSource -> Prop
twsType TypeWithSource
tGoal) Prop
ft
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasGoalSln -> Expr -> Expr -> Expr
hasDoSet HasGoalSln
d Expr
e Expr
v1, Maybe Range
eloc Maybe Range -> Maybe Range -> Maybe Range
`rCombMaybe` forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
v)
UpdHow
P.UpdFun ->
do let src :: TypeSource
src = Selector -> TypeSource
selSrc Selector
s
Prop
ft <- TypeSource -> Kind -> InferM Prop
newType TypeSource
src Kind
KType
Expr
v1 <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
v (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource (Prop -> Prop -> Prop
tFun Prop
ft Prop
ft) TypeSource
src Maybe Range
eloc)
HasGoalSln
d <- Selector -> Prop -> Prop -> InferM HasGoalSln
newHasGoal Selector
s (TypeWithSource -> Prop
twsType TypeWithSource
tGoal) Prop
ft
Name
tmp <- Namespace -> Ident -> InferM Name
newLocalName Namespace
NSValue (String -> Ident
packIdent String
"rf")
let e' :: Expr
e' = Name -> Expr
EVar Name
tmp
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( 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
Decl { dName :: Name
dName = Name
tmp
, dSignature :: Schema
dSignature = Prop -> Schema
tMono (TypeWithSource -> Prop
twsType TypeWithSource
tGoal)
, dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr Expr
e
, dPragmas :: [Pragma]
dPragmas = []
, dInfix :: Bool
dInfix = Bool
False
, dFixity :: Maybe Fixity
dFixity = forall a. Maybe a
Nothing
, dDoc :: Maybe Text
dDoc = forall a. Maybe a
Nothing
} ]
, Maybe Range
eloc Maybe Range -> Maybe Range -> Maybe Range
`rCombMaybe` forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
v )
where s :: Selector
s = forall a. Located a -> a
thing Located Selector
l
[Located Selector]
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"checkRecUpd/doUpd" [ String
"Expected exactly 1 field label"
, String
"Got: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Located Selector]
sels)
]
expectSeq :: TypeWithSource -> InferM (Type,Type)
expectSeq :: TypeWithSource -> InferM (Prop, Prop)
expectSeq tGoal :: TypeWithSource
tGoal@(WithSource Prop
ty TypeSource
src Maybe Range
rng) =
case Prop
ty of
TUser Name
_ [Prop]
_ Prop
ty' ->
TypeWithSource -> InferM (Prop, Prop)
expectSeq (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
ty' TypeSource
src Maybe Range
rng)
TCon (TC TC
TCSeq) [Prop
a,Prop
b] ->
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
a,Prop
b)
TVar TVar
_ ->
do tys :: (Prop, Prop)
tys@(Prop
a,Prop
b) <- InferM (Prop, Prop)
genTys
ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeWithSource -> Prop -> InferM [Prop]
unify TypeWithSource
tGoal (Prop -> Prop -> Prop
tSeq Prop
a Prop
b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop, Prop)
tys
Prop
_ ->
do tys :: (Prop, Prop)
tys@(Prop
a,Prop
b) <- InferM (Prop, Prop)
genTys
Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
rng (TypeSource -> Path -> Prop -> Prop -> Error
TypeMismatch TypeSource
src Path
rootPath Prop
ty (Prop -> Prop -> Prop
tSeq Prop
a Prop
b))
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop, Prop)
tys
where
genTys :: InferM (Prop, Prop)
genTys =
do Prop
a <- TypeSource -> Kind -> InferM Prop
newType TypeSource
LenOfSeq Kind
KNum
Prop
b <- TypeSource -> Kind -> InferM Prop
newType TypeSource
TypeOfSeqElement Kind
KType
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
a,Prop
b)
expectTuple :: Int -> TypeWithSource -> InferM [Type]
expectTuple :: Int -> TypeWithSource -> InferM [Prop]
expectTuple Int
n tGoal :: TypeWithSource
tGoal@(WithSource Prop
ty TypeSource
src Maybe Range
rng) =
case Prop
ty of
TUser Name
_ [Prop]
_ Prop
ty' ->
Int -> TypeWithSource -> InferM [Prop]
expectTuple Int
n (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
ty' TypeSource
src Maybe Range
rng)
TCon (TC (TCTuple Int
n')) [Prop]
tys | Int
n forall a. Eq a => a -> a -> Bool
== Int
n' ->
forall (m :: * -> *) a. Monad m => a -> m a
return [Prop]
tys
TVar TVar
_ ->
do [Prop]
tys <- InferM [Prop]
genTys
ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeWithSource -> Prop -> InferM [Prop]
unify TypeWithSource
tGoal ([Prop] -> Prop
tTuple [Prop]
tys)
forall (m :: * -> *) a. Monad m => a -> m a
return [Prop]
tys
Prop
_ ->
do [Prop]
tys <- InferM [Prop]
genTys
Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
rng (TypeSource -> Path -> Prop -> Prop -> Error
TypeMismatch TypeSource
src Path
rootPath Prop
ty ([Prop] -> Prop
tTuple [Prop]
tys))
forall (m :: * -> *) a. Monad m => a -> m a
return [Prop]
tys
where
genTys :: InferM [Prop]
genTys =forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ Int
0 .. Int
n forall a. Num a => a -> a -> a
- Int
1 ] forall a b. (a -> b) -> a -> b
$ \ Int
i -> TypeSource -> Kind -> InferM Prop
newType (Int -> TypeSource
TypeOfTupleField Int
i) Kind
KType
expectRec ::
RecordMap Ident (Range, a) ->
TypeWithSource ->
InferM (RecordMap Ident (a, Type))
expectRec :: forall a.
RecordMap Ident (Range, a)
-> TypeWithSource -> InferM (RecordMap Ident (a, Prop))
expectRec RecordMap Ident (Range, a)
fs tGoal :: TypeWithSource
tGoal@(WithSource Prop
ty TypeSource
src Maybe Range
rng) =
case Prop
ty of
TUser Name
_ [Prop]
_ Prop
ty' ->
forall a.
RecordMap Ident (Range, a)
-> TypeWithSource -> InferM (RecordMap Ident (a, Prop))
expectRec RecordMap Ident (Range, a)
fs (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
ty' TypeSource
src Maybe Range
rng)
TRec RecordMap Ident Prop
ls
| Right RecordMap Ident (a, Prop)
r <- forall a b c d.
Ord a =>
(a -> b -> c -> d)
-> RecordMap a b
-> RecordMap a c
-> Either (Either a a) (RecordMap a d)
zipRecords (\Ident
_ (Range
_rng,a
v) Prop
t -> (a
v,Prop
t)) RecordMap Ident (Range, a)
fs RecordMap Ident Prop
ls -> forall (f :: * -> *) a. Applicative f => a -> f a
pure RecordMap Ident (a, Prop)
r
Prop
_ ->
do RecordMap Ident (a, Prop)
res <- forall (t :: * -> *) a b c.
Applicative t =>
(a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
traverseRecordMap
(\Ident
nm (Range
_rng,a
v) ->
do Prop
t <- TypeSource -> Kind -> InferM Prop
newType (Ident -> TypeSource
TypeOfRecordField Ident
nm) Kind
KType
forall (m :: * -> *) a. Monad m => a -> m a
return (a
v, Prop
t))
RecordMap Ident (Range, a)
fs
let tys :: RecordMap Ident Prop
tys = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd RecordMap Ident (a, Prop)
res
case Prop
ty of
TVar TVFree{} -> do [Prop]
ps <- TypeWithSource -> Prop -> InferM [Prop]
unify TypeWithSource
tGoal (RecordMap Ident Prop -> Prop
TRec RecordMap Ident Prop
tys)
ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType [Prop]
ps
Prop
_ -> Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
rng (TypeSource -> Path -> Prop -> Prop -> Error
TypeMismatch TypeSource
src Path
rootPath Prop
ty (RecordMap Ident Prop -> Prop
TRec RecordMap Ident Prop
tys))
forall (m :: * -> *) a. Monad m => a -> m a
return RecordMap Ident (a, Prop)
res
expectFin :: Int -> TypeWithSource -> InferM ()
expectFin :: Int -> TypeWithSource -> InferM ()
expectFin Int
n tGoal :: TypeWithSource
tGoal@(WithSource Prop
ty TypeSource
src Maybe Range
rng) =
case Prop
ty of
TUser Name
_ [Prop]
_ Prop
ty' ->
Int -> TypeWithSource -> InferM ()
expectFin Int
n (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
ty' TypeSource
src Maybe Range
rng)
TCon (TC (TCNum Integer
n')) [] | forall a. Integral a => a -> Integer
toInteger Int
n forall a. Eq a => a -> a -> Bool
== Integer
n' ->
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Prop
_ -> ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeWithSource -> Prop -> InferM [Prop]
unify TypeWithSource
tGoal (forall a. Integral a => a -> Prop
tNum Int
n)
expectFun :: Maybe Name -> Int -> TypeWithSource -> InferM ([Type],Type)
expectFun :: Maybe Name -> Int -> TypeWithSource -> InferM ([Prop], Prop)
expectFun Maybe Name
mbN Int
n (WithSource Prop
ty0 TypeSource
src Maybe Range
rng) = [Prop] -> Int -> Prop -> InferM ([Prop], Prop)
go [] Int
n Prop
ty0
where
go :: [Prop] -> Int -> Prop -> InferM ([Prop], Prop)
go [Prop]
tys Int
arity Prop
ty
| Int
arity forall a. Ord a => a -> a -> Bool
> Int
0 =
case Prop
ty of
TUser Name
_ [Prop]
_ Prop
ty' ->
[Prop] -> Int -> Prop -> InferM ([Prop], Prop)
go [Prop]
tys Int
arity Prop
ty'
TCon (TC TC
TCFun) [Prop
a,Prop
b] ->
[Prop] -> Int -> Prop -> InferM ([Prop], Prop)
go (Prop
aforall a. a -> [a] -> [a]
:[Prop]
tys) (Int
arity forall a. Num a => a -> a -> a
- Int
1) Prop
b
Prop
_ ->
do [Prop]
args <- Int -> InferM [Prop]
genArgs Int
arity
Prop
res <- TypeSource -> Kind -> InferM Prop
newType TypeSource
TypeOfRes Kind
KType
case Prop
ty of
TVar TVFree{} ->
do [Prop]
ps <- TypeWithSource -> Prop -> InferM [Prop]
unify (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
ty TypeSource
src Maybe Range
rng) (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
Prop
_ -> Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
rng
(TypeSource -> Path -> Prop -> Prop -> Error
TypeMismatch TypeSource
src Path
rootPath Prop
ty (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Prop -> Prop
tFun Prop
res [Prop]
args))
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> [a]
reverse [Prop]
tys forall a. [a] -> [a] -> [a]
++ [Prop]
args, Prop
res)
| Bool
otherwise =
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> [a]
reverse [Prop]
tys, Prop
ty)
genArgs :: Int -> InferM [Prop]
genArgs Int
arity = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ Int
1 .. Int
arity ] forall a b. (a -> b) -> a -> b
$
\ Int
ix -> TypeSource -> Kind -> InferM Prop
newType (ArgDescr -> TypeSource
TypeOfArg (Maybe Name -> Maybe Int -> ArgDescr
ArgDescr Maybe Name
mbN (forall a. a -> Maybe a
Just Int
ix))) Kind
KType
checkHasType :: Type -> TypeWithSource -> InferM ()
checkHasType :: Prop -> TypeWithSource -> InferM ()
checkHasType Prop
inferredType TypeWithSource
tGoal =
do [Prop]
ps <- TypeWithSource -> Prop -> InferM [Prop]
unify TypeWithSource
tGoal Prop
inferredType
case [Prop]
ps of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
[Prop]
_ -> ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType [Prop]
ps
checkFun ::
P.FunDesc Name -> [P.Pattern Name] ->
P.Expr Name -> TypeWithSource -> InferM Expr
checkFun :: FunDesc Name
-> [Pattern Name] -> Expr Name -> TypeWithSource -> InferM Expr
checkFun FunDesc Name
_ [] Expr Name
e TypeWithSource
tGoal = Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal
checkFun (P.FunDesc Maybe Name
fun Int
offset) [Pattern Name]
ps Expr Name
e TypeWithSource
tGoal =
forall a. InferM a -> InferM a
inNewScope
do let descs :: [TypeSource]
descs = [ ArgDescr -> TypeSource
TypeOfArg (Maybe Name -> Maybe Int -> ArgDescr
ArgDescr Maybe Name
fun (forall a. a -> Maybe a
Just Int
n)) | Int
n <- [ Int
1 forall a. Num a => a -> a -> a
+ Int
offset .. ] ]
([Prop]
tys,Prop
tRes) <- Maybe Name -> Int -> TypeWithSource -> InferM ([Prop], Prop)
expectFun Maybe Name
fun (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern Name]
ps) TypeWithSource
tGoal
let srcs :: [TypeWithSource]
srcs = forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource [Prop]
tys [TypeSource]
descs (forall a b. (a -> b) -> [a] -> [b]
map forall t. HasLoc t => t -> Maybe Range
getLoc [Pattern Name]
ps)
[Located Name]
largs <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Pattern Name -> TypeWithSource -> InferM (Located Name)
checkP [Pattern Name]
ps [TypeWithSource]
srcs)
let ds :: Map Name (Located Prop)
ds = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (forall a. Located a -> a
thing Located Name
x, Located Name
x { thing :: Prop
thing = Prop
t }) | (Located Name
x,Prop
t) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Located Name]
largs [Prop]
tys ]
Expr
e1 <- forall a. Map Name (Located Prop) -> InferM a -> InferM a
withMonoTypes Map Name (Located Prop)
ds
(Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
tRes TypeSource
TypeOfRes (TypeWithSource -> Maybe Range
twsRange TypeWithSource
tGoal)))
let args :: [(Name, Prop)]
args = [ (forall a. Located a -> a
thing Located Name
x, Prop
t) | (Located Name
x,Prop
t) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Located Name]
largs [Prop]
tys ]
forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Name
x,Prop
t) 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 [] = TypeSource -> Kind -> InferM Prop
newType TypeSource
LenOfSeq Kind
KNum
smallest [Prop
t] = forall (m :: * -> *) a. Monad m => a -> m a
return Prop
t
smallest [Prop]
ts = do Prop
a <- TypeSource -> Kind -> InferM Prop
newType TypeSource
LenOfSeq Kind
KNum
ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtComprehension [ Prop
a Prop -> Prop -> Prop
=#= forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Prop -> Prop -> Prop
tMin [Prop]
ts ]
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
a
checkP :: P.Pattern Name -> TypeWithSource -> InferM (Located Name)
checkP :: Pattern Name -> TypeWithSource -> InferM (Located Name)
checkP Pattern Name
p tGoal :: TypeWithSource
tGoal@(WithSource Prop
_ TypeSource
src Maybe Range
rng0) =
do (Name
x, Located Prop
t) <- Pattern Name -> InferM (Name, Located Prop)
inferP Pattern Name
p
[Prop]
ps <- TypeWithSource -> Prop -> InferM [Prop]
unify TypeWithSource
tGoal (forall a. Located a -> a
thing Located Prop
t)
let rngMb :: Maybe Range
rngMb = forall t. HasLoc t => t -> Maybe Range
getLoc Pattern Name
p forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe Range
rng0
rng :: Range
rng = forall a. a -> Maybe a -> a
fromMaybe Range
emptyRange Maybe Range
rngMb
let mkErr :: Prop -> InferM ()
mkErr = Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
rngMb forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Goal] -> Error
UnsolvedGoals forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstraintSource -> Range -> Prop -> Goal
Goal (TypeSource -> ConstraintSource
CtPattern TypeSource
src) Range
rng
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Prop -> InferM ()
mkErr [Prop]
ps
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Range -> a -> Located a
Located (forall a. Located a -> Range
srcRange Located Prop
t) Name
x)
inferP :: P.Pattern Name -> InferM (Name, Located Type)
inferP :: Pattern Name -> InferM (Name, Located Prop)
inferP Pattern Name
pat =
case Pattern Name
pat of
P.PVar Located Name
x0 ->
do Prop
a <- forall a. Range -> InferM a -> InferM a
inRange (forall a. Located a -> Range
srcRange Located Name
x0) (TypeSource -> Kind -> InferM Prop
newType (Name -> TypeSource
DefinitionOf (forall a. Located a -> a
thing Located Name
x0)) Kind
KType)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Located a -> a
thing Located Name
x0, Located Name
x0 { thing :: Prop
thing = Prop
a })
P.PTyped Pattern Name
p Type Name
t ->
do Prop
tSig <- Type Name -> Kind -> InferM Prop
checkTypeOfKind Type Name
t Kind
KType
Located Name
ln <- Pattern Name -> TypeWithSource -> InferM (Located Name)
checkP Pattern Name
p (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
tSig TypeSource
TypeFromUserAnnotation (forall t. HasLoc t => t -> Maybe Range
getLoc Type Name
t))
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Located a -> a
thing Located Name
ln, Located Name
ln { thing :: Prop
thing = Prop
tSig })
Pattern Name
_ -> forall a. String -> [String] -> a
tcPanic String
"inferP" [ String
"Unexpected pattern:", 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 Pattern Name
p Expr Name
e) =
do (Name
x,Located Prop
t) <- Pattern Name -> InferM (Name, Located Prop)
inferP Pattern Name
p
Prop
n <- TypeSource -> Kind -> InferM Prop
newType TypeSource
LenOfCompGen Kind
KNum
Expr
e' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource (Prop -> Prop -> Prop
tSeq Prop
n (forall a. Located a -> a
thing Located Prop
t)) TypeSource
GeneratorOfListComp
(forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e))
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Prop -> Prop -> Expr -> Match
From Name
x Prop
n (forall a. Located a -> a
thing Located Prop
t) Expr
e', Name
x, Located Prop
t, Prop
n)
inferMatch (P.MatchLet Bind Name
b)
| forall name. Bind name -> Bool
P.bMono Bind Name
b =
do let rng :: Range
rng = forall a. Located a -> Range
srcRange (forall name. Bind name -> Located name
P.bName Bind Name
b)
Prop
a <- forall a. Range -> InferM a -> InferM a
inRange Range
rng (TypeSource -> Kind -> InferM Prop
newType (Name -> TypeSource
DefinitionOf (forall a. Located a -> a
thing (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
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Match
Let Decl
b1, Decl -> Name
dName Decl
b1, forall a. Range -> a -> Located a
Located (forall a. Located a -> Range
srcRange (forall name. Bind name -> Located name
P.bName Bind Name
b)) Prop
a, forall a. Integral a => a -> Prop
tNum (Int
1::Int))
| Bool
otherwise = forall a. String -> [String] -> a
tcPanic String
"inferMatch"
[ String
"Unexpected polymorphic match let:", 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 Int
_ [] = forall a. HasCallStack => String -> [String] -> a
panic String
"inferCArm" [ String
"Empty comprehension arm" ]
inferCArm Int
_ [Match Name
m] =
do (Match
m1, Name
x, Located Prop
t, Prop
n) <- Match Name -> InferM (Match, Name, Located Prop, Prop)
inferMatch Match Name
m
forall (m :: * -> *) a. Monad m => a -> m a
return ([Match
m1], forall k a. k -> a -> Map k a
Map.singleton Name
x Located Prop
t, Prop
n)
inferCArm Int
armNum (Match Name
m : [Match Name]
ms) =
do (Match
m1, Name
x, Located Prop
t, Prop
n) <- Match Name -> InferM (Match, Name, Located Prop, Prop)
inferMatch Match Name
m
([Match]
ms', Map Name (Located Prop)
ds, Prop
n') <- 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' ]
forall (m :: * -> *) a. Monad m => a -> m a
return (Match
m1 forall a. a -> [a] -> [a]
: [Match]
ms', forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (\Located Prop
_ 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 Bool
isTopLevel Bool
isRec [Bind Name]
binds =
do
Bool
monoBinds <- InferM Bool
getMonoBinds
let ([Bind Name]
sigs,[Bind Name]
noSigs) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name. Bind name -> Maybe (Schema name)
P.bSignature) [Bind Name]
binds
monos :: [Bind Name]
monos = [Bind Name]
sigs forall a. [a] -> [a] -> [a]
++ [ Bind Name
b { bMono :: Bool
P.bMono = Bool
True } | Bind Name
b <- [Bind Name]
noSigs ]
binds' :: [Bind Name]
binds' | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any 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 Map Name Expr
exprMap =
do ([(Name, VarType)]
newEnv,[Either (InferM Decl) (InferM Decl)]
todos) <- forall a b. [(a, b)] -> ([a], [b])
unzip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` 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 = forall a. (a -> Bool) -> [a] -> [a]
filter forall {a}. (a, VarType) -> Bool
isExt [(Name, VarType)]
newEnv
let ([InferM Decl]
sigsAndMonos,[InferM Decl]
noSigGen) = forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either (InferM Decl) (InferM Decl)]
todos
let prepGen :: InferM ([Decl], [Goal])
prepGen = forall a. InferM a -> InferM (a, [Goal])
collectGoals
forall a b. (a -> b) -> a -> b
$ do [Decl]
bs <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [InferM Decl]
noSigGen
InferM ()
simplifyAllConstraints
forall (m :: * -> *) a. Monad m => a -> m a
return [Decl]
bs
if Bool
isRec
then
do ([Decl]
bs1,[Goal]
cs) <- forall a. [(Name, VarType)] -> InferM a -> InferM a
withVarTypes [(Name, VarType)]
newEnv InferM ([Decl], [Goal])
prepGen
[Decl]
genCs <- 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' = forall a b. (a -> b) -> [a] -> [b]
map Decl -> (Name, VarType)
toExt [Decl]
bs1 forall a. [a] -> [a] -> [a]
++ [(Name, VarType)]
otherEnv
[Decl]
done <- forall a. [(Name, VarType)] -> InferM a -> InferM a
withVarTypes [(Name, VarType)]
newEnv' (forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [InferM Decl]
sigsAndMonos)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl]
done,[Decl]
genCs)
else
do [Decl]
done <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [InferM Decl]
sigsAndMonos
([Decl]
bs1, [Goal]
cs) <- InferM ([Decl], [Goal])
prepGen
[Decl]
genCs <- [Decl] -> [Goal] -> InferM [Decl]
generalize [Decl]
bs1 [Goal]
cs
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl]
done,[Decl]
genCs)
Bool -> [Bind Name] -> [Bind Name] -> InferM ()
checkNumericConstraintGuardsOK Bool
isTopLevel [Bind Name]
sigs [Bind Name]
noSigs
rec
let exprMap :: Map Name Expr
exprMap = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. (a -> b) -> [a] -> [b]
map Decl -> (Name, Expr)
monoUse [Decl]
genBs)
([Decl]
doneBs, [Decl]
genBs) <- Map Name Expr -> InferM ([Decl], [Decl])
check Map Name Expr
exprMap
InferM ()
simplifyAllConstraints
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl]
doneBs forall a. [a] -> [a] -> [a]
++ [Decl]
genBs)
where
toExt :: Decl -> (Name, VarType)
toExt Decl
d = (Decl -> Name
dName Decl
d, Schema -> VarType
ExtVar (Decl -> Schema
dSignature Decl
d))
isExt :: (a, VarType) -> Bool
isExt (a
_,VarType
y) = case VarType
y of
ExtVar Schema
_ -> Bool
True
VarType
_ -> Bool
False
monoUse :: Decl -> (Name, Expr)
monoUse 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 Expr
e TParam
a = Expr -> Prop -> Expr
ETApp Expr
e (TVar -> Prop
TVar (TParam -> TVar
tpVar TParam
a))
appP :: Expr -> p -> Expr
appP Expr
e p
_ = Expr -> Expr
EProofApp Expr
e
withTys :: Expr
withTys = 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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall {p}. Expr -> p -> Expr
appP Expr
withTys [Prop]
qs
checkNumericConstraintGuardsOK ::
Bool -> [P.Bind Name] -> [P.Bind Name] -> InferM ()
checkNumericConstraintGuardsOK :: Bool -> [Bind Name] -> [Bind Name] -> InferM ()
checkNumericConstraintGuardsOK Bool
isTopLevel [Bind Name]
haveSig [Bind Name]
noSig =
do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
isTopLevel
(forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Ident -> Error) -> Bind Name -> InferM ()
mkErr Ident -> Error
NestedConstraintGuard) [Bind Name]
withGuards)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Bind Name]
withGuards)
(forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Ident -> Error) -> Bind Name -> InferM ()
mkErr Ident -> Error
DeclarationRequiresSignatureCtrGrd) [Bind Name]
noSig)
where
mkErr :: (Ident -> Error) -> Bind Name -> InferM ()
mkErr Ident -> Error
f Bind Name
b =
do let nm :: Located Name
nm = forall name. Bind name -> Located name
P.bName Bind Name
b
forall a. Range -> InferM a -> InferM a
inRange (forall a. Located a -> Range
srcRange Located Name
nm) (Error -> InferM ()
recordError (Ident -> Error
f (Name -> Ident
nameIdent (forall a. Located a -> a
thing Located Name
nm))))
withGuards :: [Bind Name]
withGuards = forall a. (a -> Bool) -> [a] -> [a]
filter forall name. Bind name -> Bool
hasConstraintGuards [Bind Name]
haveSig
hasConstraintGuards :: Bind name -> Bool
hasConstraintGuards Bind name
b =
case forall a. Located a -> a
thing (forall name. Bind name -> Located (BindDef name)
P.bDef Bind name
b) of
P.DPropGuards {} -> Bool
True
BindDef name
_ -> Bool
False
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 Map Name Expr
exprMap b :: Bind Name
b@(P.Bind { Bool
[Pattern Name]
[Pragma]
Maybe Text
Maybe Fixity
Maybe (Schema Name)
Located Name
Located (BindDef Name)
ExportType
bExport :: forall name. Bind name -> ExportType
bDoc :: forall name. Bind name -> Maybe Text
bPragmas :: forall name. Bind name -> [Pragma]
bFixity :: forall name. Bind name -> Maybe Fixity
bInfix :: forall name. Bind name -> Bool
bParams :: forall name. Bind name -> [Pattern name]
bExport :: ExportType
bDoc :: Maybe Text
bMono :: Bool
bPragmas :: [Pragma]
bFixity :: Maybe Fixity
bInfix :: Bool
bSignature :: Maybe (Schema Name)
bDef :: Located (BindDef Name)
bParams :: [Pattern Name]
bName :: Located Name
bDef :: forall name. Bind name -> Located (BindDef name)
bSignature :: forall name. Bind name -> Maybe (Schema name)
bName :: forall name. Bind name -> Located name
bMono :: forall name. Bind name -> Bool
.. }) =
case Maybe (Schema Name)
bSignature of
Just Schema Name
s ->
do let wildOk :: AllowWildCards
wildOk = case forall a. Located a -> a
thing Located (BindDef Name)
bDef of
P.DForeign {} -> AllowWildCards
NoWildCards
BindDef Name
P.DPrim -> AllowWildCards
NoWildCards
P.DExpr {} -> AllowWildCards
AllowWildCards
P.DPropGuards {} -> AllowWildCards
NoWildCards
(Schema, [Goal])
s1 <- AllowWildCards -> Schema Name -> InferM (Schema, [Goal])
checkSchema AllowWildCards
wildOk Schema Name
s
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
name, Schema -> VarType
ExtVar (forall a b. (a, b) -> a
fst (Schema, [Goal])
s1)), forall a b. a -> Either a b
Left (Bind Name -> (Schema, [Goal]) -> InferM Decl
checkSigB Bind Name
b (Schema, [Goal])
s1))
Maybe (Schema Name)
Nothing
| Bool
bMono ->
do Prop
t <- TypeSource -> Kind -> InferM Prop
newType (Name -> TypeSource
DefinitionOf Name
name) Kind
KType
let schema :: Schema
schema = [TParam] -> [Prop] -> Prop -> Schema
Forall [] [] Prop
t
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
name, Schema -> VarType
ExtVar Schema
schema), forall a b. a -> Either a b
Left (Bind Name -> Prop -> InferM Decl
checkMonoB Bind Name
b Prop
t))
| Bool
otherwise ->
do Prop
t <- TypeSource -> Kind -> InferM Prop
newType (Name -> TypeSource
DefinitionOf Name
name) Kind
KType
let noWay :: a
noWay = forall a. String -> [String] -> a
tcPanic String
"guessType" [ String
"Missing expression for:" ,
forall a. Show a => a -> String
show Name
name ]
expr :: Expr
expr = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall {a}. a
noWay Name
name Map Name Expr
exprMap
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
name, Expr -> Prop -> VarType
CurSCC Expr
expr Prop
t), forall a b. b -> Either a b
Right (Bind Name -> Prop -> InferM Decl
checkMonoB Bind Name
b Prop
t))
where
name :: Name
name = forall a. Located a -> a
thing Located Name
bName
generalize :: [Decl] -> [Goal] -> InferM [Decl]
generalize :: [Decl] -> [Goal] -> InferM [Decl]
generalize [] [Goal]
gs0 =
do [Goal] -> InferM ()
addGoals [Goal]
gs0
forall (m :: * -> *) a. Monad m => a -> m a
return []
generalize [Decl]
bs0 [Goal]
gs0 =
do
[Goal]
gs <- [Goal] -> InferM [Goal]
applySubstGoals [Goal]
gs0
[Decl]
bs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Decl]
bs0 forall a b. (a -> b) -> a -> b
$ \Decl
b -> do Schema
s <- forall t. TVars t => t -> InferM t
applySubst (Decl -> Schema
dSignature Decl
b)
forall (m :: * -> *) a. Monad m => a -> m a
return Decl
b { dSignature :: Schema
dSignature = Schema
s }
let goalFVS :: Goal -> Set TVar
goalFVS Goal
g = forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV forall a b. (a -> b) -> a -> b
$ forall t. FVS t => t -> Set TVar
fvs forall a b. (a -> b) -> a -> b
$ Goal -> Prop
goal Goal
g
inGoals :: Set TVar
inGoals = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Goal -> Set TVar
goalFVS [Goal]
gs
inSigs :: Set TVar
inSigs = forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV forall a b. (a -> b) -> a -> b
$ forall t. FVS t => t -> Set TVar
fvs forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Decl -> Schema
dSignature [Decl]
bs
candidates :: Set TVar
candidates = (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 = forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set TVar
candidates Set TVar
asmpVs
stays :: Goal -> Bool
stays Goal
g = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
gen0) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Goal -> Set TVar
goalFVS Goal
g
([Goal]
here0,[Goal]
later) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Goal -> Bool
stays [Goal]
gs
[Goal] -> InferM ()
addGoals [Goal]
later
let maybeAmbig :: [TVar]
maybeAmbig = forall a. Set a -> [a]
Set.toList (forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set TVar
gen0 Set TVar
inSigs)
let ([TVar]
as0,[Goal]
here1,Subst
defSu,[Warning]
ws,[Error]
errs) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error])
defaultAndSimplify [TVar]
maybeAmbig [Goal]
here0
Subst -> InferM ()
extendSubst Subst
defSu
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Warning -> InferM ()
recordWarning [Warning]
ws
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Error -> InferM ()
recordError [Error]
errs
let here :: [Prop]
here = forall a b. (a -> b) -> [a] -> [b]
map Goal -> Prop
goal [Goal]
here1
let as :: [TVar]
as = forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy forall {t} {t}. (HasKind t, HasKind t) => t -> t -> Ordering
numFst
forall a b. (a -> b) -> a -> b
$ [TVar]
as0 forall a. [a] -> [a] -> [a]
++ forall a. Set a -> [a]
Set.toList (forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set TVar
inSigs Set TVar
asmpVs)
asPs :: [TParam]
asPs = [ TParam { tpUnique :: Int
tpUnique = Int
x
, tpKind :: Kind
tpKind = Kind
k
, tpFlav :: TPFlavor
tpFlav = TPFlavor
TPUnifyVar
, tpInfo :: TVarInfo
tpInfo = TVarInfo
i
}
| TVFree Int
x Kind
k Set TParam
_ TVarInfo
i <- [TVar]
as
]
Subst
totSu <- InferM Subst
getSubst
let
su :: Subst
su = [(TVar, Prop)] -> Subst
listSubst (forall a b. [a] -> [b] -> [(a, b)]
zip [TVar]
as (forall a b. (a -> b) -> [a] -> [b]
map (TVar -> Prop
TVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
tpVar) [TParam]
asPs)) Subst -> Subst -> Subst
@@ Subst
totSu
qs :: [Prop]
qs = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Prop -> [Prop]
pSplitAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. TVars t => Subst -> t -> t
apSubst Subst
su) [Prop]
here
genE :: Expr -> Expr
genE Expr
e = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Expr -> Expr
EProofAbs (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e) [Prop]
qs) [TParam]
asPs
genB :: Decl -> Decl
genB Decl
d = Decl
d { dDefinition :: DeclDef
dDefinition = case Decl -> DeclDef
dDefinition Decl
d of
DExpr Expr
e -> Expr -> DeclDef
DExpr (Expr -> Expr
genE Expr
e)
DeclDef
DPrim -> DeclDef
DPrim
DForeign FFIFunType
t -> FFIFunType -> DeclDef
DForeign FFIFunType
t
, dSignature :: Schema
dSignature = [TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
asPs [Prop]
qs
forall a b. (a -> b) -> a -> b
$ forall t. TVars t => Subst -> t -> t
apSubst Subst
su forall a b. (a -> b) -> a -> b
$ Schema -> Prop
sType forall a b. (a -> b) -> a -> b
$ Decl -> Schema
dSignature Decl
d
}
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map Decl -> Decl
genB [Decl]
bs)
where
numFst :: t -> t -> Ordering
numFst t
x t
y = case (forall t. HasKind t => t -> Kind
kindOf t
x, forall t. HasKind t => t -> Kind
kindOf t
y) of
(Kind
KNum, Kind
KNum) -> Ordering
EQ
(Kind
KNum, Kind
_) -> Ordering
LT
(Kind
_,Kind
KNum) -> Ordering
GT
(Kind, Kind)
_ -> Ordering
EQ
checkMonoB :: P.Bind Name -> Type -> InferM Decl
checkMonoB :: Bind Name -> Prop -> InferM Decl
checkMonoB Bind Name
b Prop
t =
forall a. Maybe Range -> InferM a -> InferM a
inRangeMb (forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b) forall a b. (a -> b) -> a -> b
$
case forall a. Located a -> a
thing (forall name. Bind name -> Located (BindDef name)
P.bDef Bind Name
b) of
BindDef Name
P.DPrim -> forall a. HasCallStack => String -> [String] -> a
panic String
"checkMonoB" [String
"Primitive with no signature?"]
BindDef Name
P.DForeign -> forall a. HasCallStack => String -> [String] -> a
panic String
"checkMonoB" [String
"Foreign with no signature?"]
P.DExpr Expr Name
e ->
do let nm :: Name
nm = forall a. Located a -> a
thing (forall name. Bind name -> Located name
P.bName Bind Name
b)
let tGoal :: TypeWithSource
tGoal = Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
t (Name -> TypeSource
DefinitionOf Name
nm) (forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b)
Expr
e1 <- FunDesc Name
-> [Pattern Name] -> Expr Name -> TypeWithSource -> InferM Expr
checkFun (forall n. Maybe n -> Int -> FunDesc n
P.FunDesc (forall a. a -> Maybe a
Just Name
nm) Int
0) (forall name. Bind name -> [Pattern name]
P.bParams Bind Name
b) Expr Name
e TypeWithSource
tGoal
let f :: Name
f = forall a. Located a -> a
thing (forall name. Bind name -> Located name
P.bName Bind Name
b)
forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
, dInfix :: Bool
dInfix = forall name. Bind name -> Bool
P.bInfix Bind Name
b
, dFixity :: Maybe Fixity
dFixity = forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
, dDoc :: Maybe Text
dDoc = forall name. Bind name -> Maybe Text
P.bDoc Bind Name
b
}
P.DPropGuards [PropGuardCase Name]
_ ->
forall a. String -> [String] -> a
tcPanic String
"checkMonoB"
[ String
"Used constraint guards without a signature at "
, forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PP a => a -> Doc
pp forall a b. (a -> b) -> a -> b
$ forall name. Bind name -> Located name
P.bName Bind Name
b ]
checkSigB :: P.Bind Name -> (Schema,[Goal]) -> InferM Decl
checkSigB :: Bind Name -> (Schema, [Goal]) -> InferM Decl
checkSigB Bind Name
b (Forall [TParam]
as [Prop]
asmps0 Prop
t0, [Goal]
validSchema) =
let name :: Name
name = forall a. Located a -> a
thing (forall name. Bind name -> Located name
P.bName Bind Name
b) in
case forall a. Located a -> a
thing (forall name. Bind name -> Located (BindDef name)
P.bDef Bind Name
b) of
BindDef Name
P.DPrim ->
forall (m :: * -> *) a. Monad m => a -> m a
return Decl
{ dName :: Name
dName = Name
name
, dSignature :: Schema
dSignature = [TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as [Prop]
asmps0 Prop
t0
, dDefinition :: DeclDef
dDefinition = DeclDef
DPrim
, dPragmas :: [Pragma]
dPragmas = forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
, dInfix :: Bool
dInfix = forall name. Bind name -> Bool
P.bInfix Bind Name
b
, dFixity :: Maybe Fixity
dFixity = forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
, dDoc :: Maybe Text
dDoc = forall name. Bind name -> Maybe Text
P.bDoc Bind Name
b
}
BindDef Name
P.DForeign -> do
let loc :: Maybe Range
loc = forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b
name' :: Name
name' = forall a. Located a -> a
thing forall a b. (a -> b) -> a -> b
$ forall name. Bind name -> Located name
P.bName Bind Name
b
src :: TypeSource
src = Name -> TypeSource
DefinitionOf Name
name'
forall a. Maybe Range -> InferM a -> InferM a
inRangeMb Maybe Range
loc do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [TParam]
as \TParam
a ->
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TParam -> Kind
tpKind TParam
a forall a. Eq a => a -> a -> Bool
/= Kind
KNum) forall a b. (a -> b) -> a -> b
$
Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
loc forall a b. (a -> b) -> a -> b
$ TypeSource -> TParam -> Kind -> Error
UnsupportedFFIKind TypeSource
src TParam
a forall a b. (a -> b) -> a -> b
$ TParam -> Kind
tpKind TParam
a
forall a. [TParam] -> InferM a -> InferM a
withTParams [TParam]
as do
FFIFunType
ffiFunType <-
case Schema -> Either FFITypeError ([Prop], FFIFunType)
toFFIFunType ([TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as [Prop]
asmps0 Prop
t0) of
Right ([Prop]
props, FFIFunType
ffiFunType) -> FFIFunType
ffiFunType forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do
[Goal]
ffiGoals <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (ConstraintSource -> Prop -> InferM Goal
newGoal (Name -> ConstraintSource
CtFFI Name
name')) [Prop]
props
Bool -> Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication Bool
True (forall a. a -> Maybe a
Just Name
name') [TParam]
as [Prop]
asmps0 forall a b. (a -> b) -> a -> b
$
[Goal]
validSchema forall a. [a] -> [a] -> [a]
++ [Goal]
ffiGoals
Left FFITypeError
err -> do
Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
loc forall a b. (a -> b) -> a -> b
$ TypeSource -> FFITypeError -> Error
UnsupportedFFIType TypeSource
src FFITypeError
err
forall (f :: * -> *) a. Applicative f => a -> f a
pure FFIFunType
{ ffiTParams :: [TParam]
ffiTParams = [TParam]
as, ffiArgTypes :: [FFIType]
ffiArgTypes = []
, ffiRetType :: FFIType
ffiRetType = [FFIType] -> FFIType
FFITuple [] }
forall (f :: * -> *) a. Applicative f => a -> f a
pure Decl { dName :: Name
dName = forall a. Located a -> a
thing (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 = FFIFunType -> DeclDef
DForeign FFIFunType
ffiFunType
, dPragmas :: [Pragma]
dPragmas = forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
, dInfix :: Bool
dInfix = forall name. Bind name -> Bool
P.bInfix Bind Name
b
, dFixity :: Maybe Fixity
dFixity = forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
, dDoc :: Maybe Text
dDoc = forall name. Bind name -> Maybe Text
P.bDoc Bind Name
b
}
P.DExpr Expr Name
e0 ->
forall a. Maybe Range -> InferM a -> InferM a
inRangeMb (forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b) forall a b. (a -> b) -> a -> b
$
forall a. [TParam] -> InferM a -> InferM a
withTParams [TParam]
as forall a b. (a -> b) -> a -> b
$ do
(Prop
t, [Prop]
asmps, Expr
e2) <- [Prop] -> [Prop] -> Expr Name -> InferM (Prop, [Prop], Expr)
checkBindDefExpr [] [Prop]
asmps0 Expr Name
e0
forall (m :: * -> *) a. Monad m => a -> m a
return Decl
{ dName :: Name
dName = Name
name
, dSignature :: Schema
dSignature = [TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as [Prop]
asmps Prop
t
, dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs (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 = forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
, dInfix :: Bool
dInfix = forall name. Bind name -> Bool
P.bInfix Bind Name
b
, dFixity :: Maybe Fixity
dFixity = forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
, dDoc :: Maybe Text
dDoc = forall name. Bind name -> Maybe Text
P.bDoc Bind Name
b
}
P.DPropGuards [PropGuardCase Name]
cases0 ->
forall a. Maybe Range -> InferM a -> InferM a
inRangeMb (forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b) forall a b. (a -> b) -> a -> b
$
forall a. [TParam] -> InferM a -> InferM a
withTParams [TParam]
as forall a b. (a -> b) -> a -> b
$ do
[Prop]
asmps1 <- [Prop] -> InferM [Prop]
applySubstPreds [Prop]
asmps0
Prop
t1 <- forall t. TVars t => t -> InferM t
applySubst Prop
t0
[([Prop], Expr)]
cases1 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PropGuardCase Name -> InferM ([Prop], Expr)
checkPropGuardCase [PropGuardCase Name]
cases0
Bool
exh <- Located Name -> [TParam] -> [Prop] -> [[Prop]] -> InferM Bool
checkExhaustive (forall name. Bind name -> Located name
P.bName Bind Name
b) [TParam]
as [Prop]
asmps1 (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [([Prop], Expr)]
cases1)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
exh forall a b. (a -> b) -> a -> b
$
Warning -> InferM ()
recordWarning (Name -> Warning
NonExhaustivePropGuards Name
name)
let schema :: Schema
schema = [TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as [Prop]
asmps1 Prop
t1
forall (m :: * -> *) a. Monad m => a -> m a
return Decl
{ dName :: Name
dName = Name
name
, dSignature :: Schema
dSignature = Schema
schema
, dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr
(forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs
(forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Expr -> Expr
EProofAbs
([([Prop], Expr)] -> Prop -> Expr
EPropGuards [([Prop], Expr)]
cases1 Prop
t1)
[Prop]
asmps1)
[TParam]
as)
, dPragmas :: [Pragma]
dPragmas = forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
, dInfix :: Bool
dInfix = forall name. Bind name -> Bool
P.bInfix Bind Name
b
, dFixity :: Maybe Fixity
dFixity = forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
, dDoc :: Maybe Text
dDoc = forall name. Bind name -> Maybe Text
P.bDoc Bind Name
b
}
where
checkBindDefExpr ::
[Prop] -> [Prop] -> P.Expr Name -> InferM (Type, [Prop], Expr)
checkBindDefExpr :: [Prop] -> [Prop] -> Expr Name -> InferM (Prop, [Prop], Expr)
checkBindDefExpr [Prop]
asmpsSign [Prop]
asmps1 Expr Name
e0 = do
(Expr
e1,[Goal]
cs0) <- forall a. InferM a -> InferM (a, [Goal])
collectGoals forall a b. (a -> b) -> a -> b
$ do
let nm :: Name
nm = forall a. Located a -> a
thing (forall name. Bind name -> Located name
P.bName Bind Name
b)
tGoal :: TypeWithSource
tGoal = Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
t0 (Name -> TypeSource
DefinitionOf Name
nm) (forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b)
Expr
e1 <- FunDesc Name
-> [Pattern Name] -> Expr Name -> TypeWithSource -> InferM Expr
checkFun (forall n. Maybe n -> Int -> FunDesc n
P.FunDesc (forall a. a -> Maybe a
Just Name
nm) Int
0) (forall name. Bind name -> [Pattern name]
P.bParams Bind Name
b) Expr Name
e0 TypeWithSource
tGoal
[Goal] -> InferM ()
addGoals [Goal]
validSchema
() <- InferM ()
simplifyAllConstraints
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e1
[Prop]
asmps2 <- [Prop] -> InferM [Prop]
applySubstPreds [Prop]
asmps1
[Goal]
cs <- [Goal] -> InferM [Goal]
applySubstGoals [Goal]
cs0
let findKeep :: Set a -> [a] -> [(a, Set a)] -> ([a], [a])
findKeep Set a
vs [a]
keep [(a, Set a)]
todo =
let stays :: (a, Set a) -> Bool
stays (a
_,Set a
cvs) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Set a -> Bool
Set.null forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set a
vs Set a
cvs
([(a, Set a)]
yes,[(a, Set a)]
perhaps) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition forall {a}. (a, Set a) -> Bool
stays [(a, Set a)]
todo
([a]
stayPs,[Set a]
newVars) = forall a b. [(a, b)] -> ([a], [b])
unzip [(a, Set a)]
yes
in case [a]
stayPs of
[] -> ([a]
keep,forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(a, Set a)]
todo)
[a]
_ -> Set a -> [a] -> [(a, Set a)] -> ([a], [a])
findKeep (forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (Set a
vsforall a. a -> [a] -> [a]
:[Set a]
newVars)) ([a]
stayPs forall a. [a] -> [a] -> [a]
++ [a]
keep) [(a, Set a)]
perhaps
let
stickyVars :: Set TVar
stickyVars = forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar [TParam]
as) forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall t. FVS t => t -> Set TVar
fvs [Prop]
asmps2
([Goal]
stay,[Goal]
leave) = forall {a} {a}. Ord a => Set a -> [a] -> [(a, Set a)] -> ([a], [a])
findKeep Set TVar
stickyVars []
[ (Goal
c, forall t. FVS t => t -> Set TVar
fvs Goal
c) | Goal
c <- [Goal]
cs ]
[Goal] -> InferM ()
addGoals [Goal]
leave
Subst
su <- Bool -> Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication Bool
True (forall a. a -> Maybe a
Just (forall a. Located a -> a
thing (forall name. Bind name -> Located name
P.bName Bind Name
b))) [TParam]
as ([Prop]
asmpsSign forall a. Semigroup a => a -> a -> a
<> [Prop]
asmps2) [Goal]
stay
Subst -> InferM ()
extendSubst Subst
su
let asmps :: [Prop]
asmps = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Prop -> [Prop]
pSplitAnd (forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Prop]
asmps2)
Prop
t <- forall t. TVars t => t -> InferM t
applySubst Prop
t0
Expr
e2 <- forall t. TVars t => t -> InferM t
applySubst Expr
e1
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop
t, [Prop]
asmps, Expr
e2)
checkExhaustive :: Located Name -> [TParam] -> [Prop] -> [[Prop]] -> InferM Bool
checkExhaustive :: Located Name -> [TParam] -> [Prop] -> [[Prop]] -> InferM Bool
checkExhaustive Located Name
name [TParam]
as [Prop]
asmps [[Prop]]
guards =
case forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy forall {t :: * -> *} {t :: * -> *} {a} {a}.
(Foldable t, Foldable t) =>
t a -> t a -> Ordering
cmpByLonger [[Prop]]
guards of
[] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
[Prop]
longest : [[Prop]]
rest -> [[Prop]] -> [Goal] -> InferM Bool
doGoals ([[Prop]] -> [[Prop]]
theAlts [[Prop]]
rest) (forall a b. (a -> b) -> [a] -> [b]
map Prop -> Goal
toGoal [Prop]
longest)
where
cmpByLonger :: t a -> t a -> Ordering
cmpByLonger t a
props1 t a
props2 = forall a. Ord a => a -> a -> Ordering
compare (forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
props2) (forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
props1)
theAlts :: [[Prop]] -> [[Prop]]
theAlts :: [[Prop]] -> [[Prop]]
theAlts = forall a b. (a -> b) -> [a] -> [b]
map forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map [Prop] -> [[Prop]]
chooseNeg
chooseNeg :: [Prop] -> [[Prop]]
chooseNeg [Prop]
ps =
case [Prop]
ps of
[] -> []
Prop
p : [Prop]
qs -> (Prop -> [Prop]
pNegNumeric Prop
p forall a. [a] -> [a] -> [a]
++ [Prop]
qs) forall a. a -> [a] -> [a]
: [ Prop
p forall a. a -> [a] -> [a]
: [Prop]
alts | [Prop]
alts <- [Prop] -> [[Prop]]
chooseNeg [Prop]
qs ]
doGoals :: [[Prop]] -> [Goal] -> InferM Bool
doGoals [[Prop]]
todo [Goal]
gs =
case [[Prop]]
todo of
[] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
[Prop]
alt : [[Prop]]
more ->
do Bool
ok <- [Prop] -> [Goal] -> InferM Bool
canProve ([Prop]
asmps forall a. [a] -> [a] -> [a]
++ [Prop]
alt) [Goal]
gs
if Bool
ok then [[Prop]] -> [Goal] -> InferM Bool
doGoals [[Prop]]
more [Goal]
gs
else forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
toGoal :: Prop -> Goal
toGoal :: Prop -> Goal
toGoal Prop
prop =
Goal
{ goalSource :: ConstraintSource
goalSource = Name -> ConstraintSource
CtPropGuardsExhaustive (forall a. Located a -> a
thing Located Name
name)
, goalRange :: Range
goalRange = forall a. Located a -> Range
srcRange Located Name
name
, goal :: Prop
goal = Prop
prop
}
canProve :: [Prop] -> [Goal] -> InferM Bool
canProve :: [Prop] -> [Goal] -> InferM Bool
canProve [Prop]
asmps' [Goal]
goals =
Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Bool
tryProveImplication (forall a. a -> Maybe a
Just (forall a. Located a -> a
thing Located Name
name)) [TParam]
as [Prop]
asmps' [Goal]
goals
checkPropGuardCase :: P.PropGuardCase Name -> InferM ([Prop],Expr)
checkPropGuardCase :: PropGuardCase Name -> InferM ([Prop], Expr)
checkPropGuardCase (P.PropGuardCase [Located (Prop Name)]
guards Expr Name
e0) =
do [Prop]
ps <- [Located (Prop Name)] -> InferM [Prop]
checkPropGuards [Located (Prop Name)]
guards
[Prop]
tys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type Name -> Maybe Kind -> InferM Prop
`checkType` forall a. Maybe a
Nothing) [Type Name]
ts
let rhsTs :: Expr
rhsTs = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Prop -> Expr
ETApp (Expr Name -> Expr
getV Expr Name
eV) [Prop]
tys
rhsPs :: Expr
rhsPs = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr
e Prop
_p -> Expr -> Expr
EProofApp Expr
e) Expr
rhsTs [Prop]
ps
rhs :: Expr
rhs = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp Expr
rhsPs (forall a b. (a -> b) -> [a] -> [b]
map Expr Name -> Expr
getV [Expr Name]
es)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Prop]
ps,Expr
rhs)
where
(Expr Name
e1,[Expr Name]
es) = forall n. Expr n -> (Expr n, [Expr n])
P.asEApps Expr Name
e0
(Expr Name
eV,[Type Name]
ts) = case Expr Name
e1 of
P.EAppT Expr Name
ex1 [TypeInst Name]
tis -> (Expr Name
ex1, forall a b. (a -> b) -> [a] -> [b]
map forall {name}. TypeInst name -> Type name
getT [TypeInst Name]
tis)
Expr Name
_ -> (Expr Name
e1, [])
getV :: Expr Name -> Expr
getV Expr Name
ex =
case Expr Name
ex of
P.EVar Name
x -> Name -> Expr
EVar Name
x
Expr Name
_ -> forall {a}. String -> a
bad String
"Expression is not a variable."
getT :: TypeInst name -> Type name
getT TypeInst name
ti =
case TypeInst name
ti of
P.PosInst Type name
t -> Type name
t
P.NamedInst {} -> forall {a}. String -> a
bad String
"Unexpeceted NamedInst"
bad :: String -> a
bad String
msg = forall a. HasCallStack => String -> [String] -> a
panic String
"checkPropGuardCase" [String
msg]
checkLocalDecls :: [P.Decl Name] -> InferM a -> InferM (a,[DeclGroup])
checkLocalDecls :: forall a. [Decl Name] -> InferM a -> InferM (a, [DeclGroup])
checkLocalDecls [Decl Name]
ds0 InferM a
k =
do InferM ()
newLocalScope
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Decl Name]
ds0 \Decl Name
d -> Bool -> Decl Name -> Maybe Text -> InferM ()
checkDecl Bool
False Decl Name
d forall a. Maybe a
Nothing
a
a <- InferM a
k
([DeclGroup]
ds,Map Name TySyn
_tySyns) <- InferM ([DeclGroup], Map Name TySyn)
endLocalScope
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a,[DeclGroup]
ds)
checkTopDecls :: [P.TopDecl Name] -> InferM ()
checkTopDecls :: [TopDecl Name] -> InferM ()
checkTopDecls = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TopDecl Name -> InferM ()
checkTopDecl
where
checkTopDecl :: TopDecl Name -> InferM ()
checkTopDecl TopDecl Name
decl =
case TopDecl Name
decl of
P.Decl TopLevel (Decl Name)
tl -> Bool -> Decl Name -> Maybe Text -> InferM ()
checkDecl Bool
True (forall a. TopLevel a -> a
P.tlValue TopLevel (Decl Name)
tl) (forall a. Located a -> a
thing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (Decl Name)
tl)
P.TDNewtype TopLevel (Newtype Name)
tl ->
do Newtype
t <- Newtype Name -> Maybe Text -> InferM Newtype
checkNewtype (forall a. TopLevel a -> a
P.tlValue TopLevel (Newtype Name)
tl) (forall a. Located a -> a
thing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (Newtype Name)
tl)
Newtype -> InferM ()
addNewtype Newtype
t
P.DPrimType TopLevel (PrimType Name)
tl ->
do AbstractType
t <- PrimType Name -> Maybe Text -> InferM AbstractType
checkPrimType (forall a. TopLevel a -> a
P.tlValue TopLevel (PrimType Name)
tl) (forall a. Located a -> a
thing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (PrimType Name)
tl)
AbstractType -> InferM ()
addPrimType AbstractType
t
P.DInterfaceConstraint Maybe Text
_ Located [Prop Name]
cs ->
forall a. Range -> InferM a -> InferM a
inRange (forall a. Located a -> Range
srcRange Located [Prop Name]
cs)
do [Located Prop]
cs1 <- [Located (Prop Name)] -> InferM [Located Prop]
checkParameterConstraints [ Located [Prop Name]
cs { thing :: Prop Name
thing = Prop Name
c } | Prop Name
c <- forall a. Located a -> a
thing Located [Prop Name]
cs ]
[Located Prop] -> InferM ()
addParameterConstraints [Located Prop]
cs1
P.DModule TopLevel (NestedModule Name)
tl ->
forall a. InferM a -> InferM a
selectorScope
case forall mname name. ModuleG mname name -> ModuleDefinition name
P.mDef ModuleG Name Name
m of
P.NormalModule [TopDecl Name]
ds ->
do Name -> Maybe Text -> ExportSpec Name -> InferM ()
newSubmoduleScope (forall a. Located a -> a
thing (forall mname name. ModuleG mname name -> Located mname
P.mName ModuleG Name Name
m))
(forall a. Located a -> a
thing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (NestedModule Name)
tl)
(forall name. Ord name => [TopDecl name] -> ExportSpec name
P.exportedDecls [TopDecl Name]
ds)
[TopDecl Name] -> InferM ()
checkTopDecls [TopDecl Name]
ds
InferM ()
proveModuleTopLevel
InferM ()
endSubmodule
P.FunctorInstance Located (ImpName Name)
f ModuleInstanceArgs Name
as ModuleInstance Name
inst ->
do let doc :: Maybe Text
doc = forall a. Located a -> a
thing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (NestedModule Name)
tl
Maybe TCTopEntity
_ <- Located (ImpName Name)
-> Located (ImpName Name)
-> ModuleInstanceArgs Name
-> ModuleInstance Name
-> Maybe Text
-> InferM (Maybe TCTopEntity)
doFunctorInst (forall name. name -> ImpName name
P.ImpNested forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall mname name. ModuleG mname name -> Located mname
P.mName ModuleG Name Name
m) Located (ImpName Name)
f ModuleInstanceArgs Name
as ModuleInstance Name
inst Maybe Text
doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
P.InterfaceModule Signature Name
sig ->
do let doc :: Maybe Text
doc = forall a. Located a -> a
P.thing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (NestedModule Name)
tl
forall a. Range -> InferM a -> InferM a
inRange (forall a. Located a -> Range
srcRange (forall mname name. ModuleG mname name -> Located mname
P.mName ModuleG Name Name
m))
do Name -> Maybe Text -> InferM ()
newSignatureScope (forall a. Located a -> a
thing (forall mname name. ModuleG mname name -> Located mname
P.mName ModuleG Name Name
m)) Maybe Text
doc
Signature Name -> InferM ()
checkSignature Signature Name
sig
InferM ()
endSignature
where P.NestedModule ModuleG Name Name
m = forall a. TopLevel a -> a
P.tlValue TopLevel (NestedModule Name)
tl
P.DModParam ModParam Name
p ->
forall a. Range -> InferM a -> InferM a
inRange (forall a. Located a -> Range
srcRange (forall name. ModParam name -> Located (ImpName name)
P.mpSignature ModParam Name
p))
do let binds :: ModuleInstance Name
binds = forall name. ModParam name -> Map name name
P.mpRenaming ModParam Name
p
suMap :: ModuleInstance Name
suMap = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name
y,Name
x) | (Name
x,Name
y) <- forall k a. Map k a -> [(k, a)]
Map.toList ModuleInstance Name
binds ]
actualName :: Name -> Name
actualName Name
x = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Name
x Name
x ModuleInstance Name
suMap
ModParamNames
ips <- ImpName Name -> InferM ModParamNames
lookupSignature (forall a. Located a -> a
thing (forall name. ModParam name -> Located (ImpName name)
P.mpSignature ModParam Name
p))
let actualTys :: [ModTParam]
actualTys = [ forall t. TraverseNames t => (Name -> Name) -> t -> t
mapNames Name -> Name
actualName ModTParam
mp
| ModTParam
mp <- forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
ips) ]
actualTS :: [TySyn]
actualTS = [ forall t. TraverseNames t => (Name -> Name) -> t -> t
mapNames Name -> Name
actualName TySyn
ts
| TySyn
ts <- forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name TySyn
mpnTySyn ModParamNames
ips)
]
actualCtrs :: [Located Prop]
actualCtrs = [ forall t. TraverseNames t => (Name -> Name) -> t -> t
mapNames Name -> Name
actualName Located Prop
prop
| Located Prop
prop <- ModParamNames -> [Located Prop]
mpnConstraints ModParamNames
ips ]
actualVals :: [ModVParam]
actualVals = [ forall t. TraverseNames t => (Name -> Name) -> t -> t
mapNames Name -> Name
actualName ModVParam
vp
| ModVParam
vp <- forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
ips) ]
param :: ModParam
param =
ModParam
{ mpName :: Ident
mpName = forall name. ModParam name -> Ident
P.mpName ModParam Name
p
, mpIface :: ImpName Name
mpIface = forall a. Located a -> a
thing (forall name. ModParam name -> Located (ImpName name)
P.mpSignature ModParam Name
p)
, mpQual :: Maybe ModName
mpQual = forall name. ModParam name -> Maybe ModName
P.mpAs ModParam Name
p
, mpParameters :: ModParamNames
mpParameters =
ModParamNames
{ mpnTypes :: Map Name ModTParam
mpnTypes = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (ModTParam -> Name
mtpName ModTParam
tp, ModTParam
tp)
| ModTParam
tp <- [ModTParam]
actualTys ]
, mpnTySyn :: Map Name TySyn
mpnTySyn = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (TySyn -> Name
tsName TySyn
ts, TySyn
ts)
| TySyn
ts <- [TySyn]
actualTS ]
, mpnConstraints :: [Located Prop]
mpnConstraints = [Located Prop]
actualCtrs
, mpnFuns :: Map Name ModVParam
mpnFuns = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (ModVParam -> Name
mvpName ModVParam
vp, ModVParam
vp)
| ModVParam
vp <- [ModVParam]
actualVals ]
, mpnDoc :: Maybe Text
mpnDoc = forall a. Located a -> a
thing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall name. ModParam name -> Maybe (Located Text)
P.mpDoc ModParam Name
p
}
}
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ModTParam -> InferM ()
addParamType [ModTParam]
actualTys
[Located Prop] -> InferM ()
addParameterConstraints [Located Prop]
actualCtrs
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ModVParam -> InferM ()
addParamFun [ModVParam]
actualVals
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TySyn -> InferM ()
addTySyn [TySyn]
actualTS
ModParam -> InferM ()
addModParam ModParam
param
P.DImport {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
P.Include {} -> forall {a}. String -> a
bad String
"Include"
P.DParamDecl {} -> forall {a}. String -> a
bad String
"DParamDecl"
bad :: String -> a
bad String
x = forall a. HasCallStack => String -> [String] -> a
panic String
"checkTopDecl" [ String
x ]
checkSignature :: P.Signature Name -> InferM ()
checkSignature :: Signature Name -> InferM ()
checkSignature Signature Name
sig =
do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall name. Signature name -> [ParameterType name]
P.sigTypeParams Signature Name
sig) \ParameterType Name
pt ->
ModTParam -> InferM ()
addParamType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ParameterType Name -> InferM ModTParam
checkParameterType ParameterType Name
pt
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SigDecl Name -> InferM ()
checkSigDecl (forall name. Signature name -> [SigDecl name]
P.sigDecls Signature Name
sig)
[Located Prop] -> InferM ()
addParameterConstraints forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
[Located (Prop Name)] -> InferM [Located Prop]
checkParameterConstraints (forall name. Signature name -> [Located (Prop name)]
P.sigConstraints Signature Name
sig)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall name. Signature name -> [ParameterFun name]
P.sigFunParams Signature Name
sig) \ParameterFun Name
f ->
ModVParam -> InferM ()
addParamFun forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ParameterFun Name -> InferM ModVParam
checkParameterFun ParameterFun Name
f
InferM ()
proveModuleTopLevel
checkSigDecl :: P.SigDecl Name -> InferM ()
checkSigDecl :: SigDecl Name -> InferM ()
checkSigDecl SigDecl Name
decl =
case SigDecl Name
decl of
P.SigTySyn TySyn Name
ts Maybe Text
mbD ->
TySyn -> InferM ()
addTySyn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TySyn Name -> Maybe Text -> InferM TySyn
checkTySyn TySyn Name
ts Maybe Text
mbD
P.SigPropSyn PropSyn Name
ps Maybe Text
mbD ->
TySyn -> InferM ()
addTySyn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< PropSyn Name -> Maybe Text -> InferM TySyn
checkPropSyn PropSyn Name
ps Maybe Text
mbD
checkDecl :: Bool -> P.Decl Name -> Maybe Text -> InferM ()
checkDecl :: Bool -> Decl Name -> Maybe Text -> InferM ()
checkDecl Bool
isTopLevel Decl Name
d Maybe Text
mbDoc =
case Decl Name
d of
P.DBind Bind Name
c ->
do ~[Decl
b] <- Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferBinds Bool
isTopLevel Bool
False [Bind Name
c]
DeclGroup -> InferM ()
addDecls (Decl -> DeclGroup
NonRecursive Decl
b)
P.DRec [Bind Name]
bs ->
do [Decl]
bs1 <- Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferBinds Bool
isTopLevel Bool
True [Bind Name]
bs
DeclGroup -> InferM ()
addDecls ([Decl] -> DeclGroup
Recursive [Decl]
bs1)
P.DType TySyn Name
t ->
do TySyn
t1 <- TySyn Name -> Maybe Text -> InferM TySyn
checkTySyn TySyn Name
t Maybe Text
mbDoc
TySyn -> InferM ()
addTySyn TySyn
t1
P.DProp PropSyn Name
t ->
do TySyn
t1 <- PropSyn Name -> Maybe Text -> InferM TySyn
checkPropSyn PropSyn Name
t Maybe Text
mbDoc
TySyn -> InferM ()
addTySyn TySyn
t1
P.DLocated Decl Name
d' Range
r -> forall a. Range -> InferM a -> InferM a
inRange Range
r (Bool -> Decl Name -> Maybe Text -> InferM ()
checkDecl Bool
isTopLevel Decl Name
d' Maybe Text
mbDoc)
P.DSignature {} -> forall {a}. String -> a
bad String
"DSignature"
P.DFixity {} -> forall {a}. String -> a
bad String
"DFixity"
P.DPragma {} -> forall {a}. String -> a
bad String
"DPragma"
P.DPatBind {} -> forall {a}. String -> a
bad String
"DPatBind"
where
bad :: String -> a
bad String
x = forall a. HasCallStack => String -> [String] -> a
panic String
"checkDecl" [String
x]
checkParameterFun :: P.ParameterFun Name -> InferM ModVParam
checkParameterFun :: ParameterFun Name -> InferM ModVParam
checkParameterFun ParameterFun Name
x =
do (Schema
s,[Goal]
gs) <- AllowWildCards -> Schema Name -> InferM (Schema, [Goal])
checkSchema AllowWildCards
NoWildCards (forall name. ParameterFun name -> Schema name
P.pfSchema ParameterFun Name
x)
Subst
su <- Bool -> Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication Bool
False (forall a. a -> Maybe a
Just (forall a. Located a -> a
thing (forall name. ParameterFun name -> Located name
P.pfName ParameterFun Name
x)))
(Schema -> [TParam]
sVars Schema
s) (Schema -> [Prop]
sProps Schema
s) [Goal]
gs
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Subst -> Bool
isEmptySubst Subst
su) forall a b. (a -> b) -> a -> b
$
forall a. HasCallStack => String -> [String] -> a
panic String
"checkParameterFun" [String
"Subst not empty??"]
let n :: Name
n = forall a. Located a -> a
thing (forall name. ParameterFun name -> Located name
P.pfName ParameterFun Name
x)
forall (m :: * -> *) a. Monad m => a -> m a
return ModVParam { mvpName :: Name
mvpName = Name
n
, mvpType :: Schema
mvpType = Schema
s
, mvpDoc :: Maybe Text
mvpDoc = forall name. ParameterFun name -> Maybe Text
P.pfDoc ParameterFun Name
x
, mvpFixity :: Maybe Fixity
mvpFixity = forall name. ParameterFun name -> Maybe Fixity
P.pfFixity ParameterFun Name
x
}
tcPanic :: String -> [String] -> a
tcPanic :: forall a. String -> [String] -> a
tcPanic String
l [String]
msg = forall a. HasCallStack => String -> [String] -> a
panic (String
"[TypeCheck] " forall a. [a] -> [a] -> [a]
++ String
l) [String]
msg