{-# LANGUAGE PatternGuards, BangPatterns, RecordWildCards #-}
module Cryptol.TypeCheck.Solve
( simplifyAllConstraints
, proveImplication
, tryProveImplication
, proveModuleTopLevel
, defaultAndSimplify
, defaultReplExpr
) where
import Cryptol.Parser.Position(thing,emptyRange)
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Monad
import Cryptol.TypeCheck.Default
import Cryptol.TypeCheck.SimpType(tWidth)
import Cryptol.TypeCheck.Error(Error(..),Warning(..))
import Cryptol.TypeCheck.Subst
(apSubst, isEmptySubst, substToList,
emptySubst,Subst,(@@), Subst, listParamSubst)
import qualified Cryptol.TypeCheck.SimpleSolver as Simplify
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.Solver.Selector(tryHasGoal)
import Cryptol.TypeCheck.Solver.SMT(Solver,proveImp,isNumeric)
import Cryptol.TypeCheck.Solver.Improve(improveProp,improveProps)
import Cryptol.TypeCheck.Solver.Numeric.Interval
import Cryptol.Utils.Patterns(matchMaybe)
import Control.Applicative ((<|>))
import Control.Monad(mzero)
import Data.Containers.ListUtils (nubOrd)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set ( Set )
import qualified Data.Set as Set
import Data.List(partition)
import Data.Maybe(listToMaybe,fromMaybe)
quickSolverIO :: Ctxt -> [Goal] -> IO (Either Error (Subst,[Goal]))
quickSolverIO :: Ctxt -> [Goal] -> IO (Either Error (Subst, [Goal]))
quickSolverIO Ctxt
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (Subst
emptySubst, []))
quickSolverIO Ctxt
ctxt [Goal]
gs =
case Ctxt -> [Goal] -> Either Error (Subst, [Goal])
quickSolver Ctxt
ctxt [Goal]
gs of
Left Error
err -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left Error
err)
Right (Subst
su,[Goal]
gs') ->
do forall {m :: * -> *} {p}. Monad m => p -> m ()
msg ([Doc] -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP a => a -> Doc
pp forall b c a. (b -> c) -> (a -> b) -> a -> c
. Goal -> Type
goal) [Goal]
gs' forall a. [a] -> [a] -> [a]
++ [forall a. PP a => a -> Doc
pp Subst
su]))
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (Subst
su,[Goal]
gs'))
where
msg :: p -> m ()
msg p
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
quickSolver :: Ctxt
-> [Goal]
-> Either Error (Subst,[Goal])
quickSolver :: Ctxt -> [Goal] -> Either Error (Subst, [Goal])
quickSolver Ctxt
ctxt [Goal]
gs0 = Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
go Subst
emptySubst [] [Goal]
gs0
where
go :: Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
go Subst
su [] [] = forall a b. b -> Either a b
Right (Subst
su,[])
go Subst
su [Goal]
unsolved [] =
case forall a. Match a -> Maybe a
matchMaybe (Incompatible -> [Goal] -> Match (Either Error (Subst, [Goal]))
findImprovement Incompatible
noIncompatible [Goal]
unsolved) of
Maybe (Either Error (Subst, [Goal]))
Nothing -> forall a b. b -> Either a b
Right (Subst
su,[Goal]
unsolved)
Just Either Error (Subst, [Goal])
imp ->
case Either Error (Subst, [Goal])
imp of
Right (Subst
newSu, [Goal]
subs) ->
Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
go (Subst
newSu Subst -> Subst -> Subst
@@ Subst
su) [] ([Goal]
subs forall a. [a] -> [a] -> [a]
++ forall t. TVars t => Subst -> t -> t
apSubst Subst
newSu [Goal]
unsolved)
Left Error
err -> forall a b. a -> Either a b
Left Error
err
go Subst
su [Goal]
unsolved (Goal
g : [Goal]
gs)
| forall a. Ord a => a -> Set a -> Bool
Set.member (Goal -> Type
goal Goal
g) (Ctxt -> Set Type
saturatedAsmps Ctxt
ctxt) = Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
go Subst
su [Goal]
unsolved [Goal]
gs
go Subst
su [Goal]
unsolved (Goal
g : [Goal]
gs) =
case Ctxt -> Type -> Solved
Simplify.simplifyStep Ctxt
ctxt (Goal -> Type
goal Goal
g) of
Solved
Unsolvable -> forall a b. a -> Either a b
Left ([Goal] -> Error
UnsolvableGoals [Goal
g])
Solved
Unsolved -> Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
go Subst
su (Goal
g forall a. a -> [a] -> [a]
: [Goal]
unsolved) [Goal]
gs
SolvedIf [Type]
subs ->
let cvt :: Type -> Goal
cvt Type
x = Goal
g { goal :: Type
goal = Type
x }
in Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
go Subst
su [Goal]
unsolved (forall a b. (a -> b) -> [a] -> [b]
map Type -> Goal
cvt [Type]
subs forall a. [a] -> [a] -> [a]
++ [Goal]
gs)
findImprovement :: Incompatible -> [Goal] -> Match (Either Error (Subst, [Goal]))
findImprovement Incompatible
inc [] =
do let bad :: Map TVar (Goal, Goal)
bad = forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith (,) (Incompatible -> Map TVar Goal
integralTVars Incompatible
inc) (Incompatible -> Map TVar Goal
fracTVars Incompatible
inc)
case forall k a. Map k a -> Maybe (a, Map k a)
Map.minView Map TVar (Goal, Goal)
bad of
Just ((Goal
g1,Goal
g2),Map TVar (Goal, Goal)
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ [Goal] -> Error
UnsolvableGoals [Goal
g1,Goal
g2]
Maybe ((Goal, Goal), Map TVar (Goal, Goal))
Nothing -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
findImprovement Incompatible
inc (Goal
g : [Goal]
gs) =
do (Subst
su,[Type]
ps) <- Bool -> Ctxt -> Type -> Match (Subst, [Type])
improveProp Bool
False Ctxt
ctxt (Goal -> Type
goal Goal
g)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (Subst
su, [ Goal
g { goal :: Type
goal = Type
p } | Type
p <- [Type]
ps ]))
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
Incompatible -> [Goal] -> Match (Either Error (Subst, [Goal]))
findImprovement (Goal -> Incompatible -> Incompatible
addIncompatible Goal
g Incompatible
inc) [Goal]
gs
data Incompatible = Incompatible
{ Incompatible -> Map TVar Goal
integralTVars :: Map TVar Goal
, Incompatible -> Map TVar Goal
fracTVars :: Map TVar Goal
}
noIncompatible :: Incompatible
noIncompatible :: Incompatible
noIncompatible = Incompatible
{ integralTVars :: Map TVar Goal
integralTVars = forall k a. Map k a
Map.empty
, fracTVars :: Map TVar Goal
fracTVars = forall k a. Map k a
Map.empty
}
addIncompatible :: Goal -> Incompatible -> Incompatible
addIncompatible :: Goal -> Incompatible -> Incompatible
addIncompatible Goal
g Incompatible
i =
forall a. a -> Maybe a -> a
fromMaybe Incompatible
i forall a b. (a -> b) -> a -> b
$
do TVar
tv <- Type -> Maybe TVar
tIsVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Maybe Type
pIsIntegral (Goal -> Type
goal Goal
g)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Incompatible
i { integralTVars :: Map TVar Goal
integralTVars = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TVar
tv Goal
g (Incompatible -> Map TVar Goal
integralTVars Incompatible
i) }
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
do TVar
tv <- Type -> Maybe TVar
tIsVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Maybe Type
pIsField (Goal -> Type
goal Goal
g)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Incompatible
i { fracTVars :: Map TVar Goal
fracTVars = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TVar
tv Goal
g (Incompatible -> Map TVar Goal
fracTVars Incompatible
i) }
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
do (Type
_,Type
_,Type
_,Type
t) <- Type -> Maybe (Type, Type, Type, Type)
pIsFLiteral (Goal -> Type
goal Goal
g)
TVar
tv <- Type -> Maybe TVar
tIsVar Type
t
forall (f :: * -> *) a. Applicative f => a -> f a
pure Incompatible
i { fracTVars :: Map TVar Goal
fracTVars = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TVar
tv Goal
g (Incompatible -> Map TVar Goal
fracTVars Incompatible
i) }
defaultReplExpr :: Solver -> Expr -> Schema ->
IO (Maybe ([(TParam,Type)], Expr))
defaultReplExpr :: Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr))
defaultReplExpr Solver
sol Expr
expr Schema
sch =
do Maybe [(TParam, Type)]
mb <- Solver -> [TParam] -> [Type] -> IO (Maybe [(TParam, Type)])
defaultReplExpr' Solver
sol [TParam]
numVs [Type]
numPs
case Maybe [(TParam, Type)]
mb of
Maybe [(TParam, Type)]
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Just [(TParam, Type)]
numBinds -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
do let optss :: [[(TParam, Type)]]
optss = forall a b. (a -> b) -> [a] -> [b]
map TParam -> [(TParam, Type)]
tryDefVar [TParam]
otherVs
[(TParam, Type)]
su <- forall a. [a] -> Maybe a
listToMaybe
[ [(TParam, Type)]
binds | [(TParam, Type)]
nonSu <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[(TParam, Type)]]
optss
, let binds :: [(TParam, Type)]
binds = [(TParam, Type)]
nonSu forall a. [a] -> [a] -> [a]
++ [(TParam, Type)]
numBinds
, [(TParam, Type)] -> Bool
validate [(TParam, Type)]
binds ]
[Type]
tys <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TParam
v [(TParam, Type)]
su | TParam
v <- Schema -> [TParam]
sVars Schema
sch ]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TParam, Type)]
su, forall {t :: * -> *}. Foldable t => t Type -> Expr
appExpr [Type]
tys)
where
validate :: [(TParam, Type)] -> Bool
validate [(TParam, Type)]
binds =
let su :: Subst
su = [(TParam, Type)] -> Subst
listParamSubst [(TParam, Type)]
binds
in forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
pSplitAnd (forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Schema -> [Type]
sProps Schema
sch)))
([TParam]
numVs,[TParam]
otherVs) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (forall {t}. HasKind t => Kind -> t -> Bool
kindIs Kind
KNum) (Schema -> [TParam]
sVars Schema
sch)
([Type]
numPs,[Type]
otherPs) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Type -> Bool
isNumeric (Schema -> [Type]
sProps Schema
sch)
kindIs :: Kind -> t -> Bool
kindIs Kind
k t
x = forall t. HasKind t => t -> Kind
kindOf t
x forall a. Eq a => a -> a -> Bool
== Kind
k
gSet :: Goals
gSet = [Goal] -> Goals
goalsFromList
[ Goal { goal :: Type
goal = Type
p
, goalRange :: Range
goalRange = Range
emptyRange
, goalSource :: ConstraintSource
goalSource = ConstraintSource
CtDefaulting } | Type
p <- [Type]
otherPs ]
fLitGoals :: Map TVar (Maybe ((TVar, Type), Warning))
fLitGoals = Goals -> Map TVar (Maybe ((TVar, Type), Warning))
flitDefaultCandidates Goals
gSet
tryDefVar :: TParam -> [(TParam, Type)]
tryDefVar :: TParam -> [(TParam, Type)]
tryDefVar TParam
a
| Just Maybe ((TVar, Type), Warning)
m <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (TParam -> TVar
TVBound TParam
a) Map TVar (Maybe ((TVar, Type), Warning))
fLitGoals
= case Maybe ((TVar, Type), Warning)
m of
Just ((TVar
_,Type
t),Warning
_) -> [(TParam
a,Type
t)]
Maybe ((TVar, Type), Warning)
Nothing -> []
| Just Goal
gt <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (TParam -> TVar
TVBound TParam
a) (Goals -> Map TVar Goal
literalGoals Goals
gSet)
= let ok :: t -> Bool
ok t
p = Bool -> Bool
not (forall a. Ord a => a -> Set a -> Bool
Set.member (TParam -> TVar
TVBound TParam
a) (forall t. FVS t => t -> Set TVar
fvs t
p)) in
[ (TParam
a,Type
t) | Type
t <- [ Type
tInteger, Type -> Type
tWord (Type -> Type
tWidth (Goal -> Type
goal Goal
gt)) ]
, forall {t}. FVS t => t -> Bool
ok Type
t ]
| Bool
otherwise = [ (TParam
a,Type
t) | Type
t <- [Type
tInteger, Type
tRational, Type
tBit] ]
appExpr :: t Type -> Expr
appExpr t Type
tys = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr
e1 Type
_ -> Expr -> Expr
EProofApp Expr
e1)
(forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Type -> Expr
ETApp Expr
expr t Type
tys)
(Schema -> [Type]
sProps Schema
sch)
defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar],[Goal],Subst,[Warning],[Error])
defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error])
defaultAndSimplify [TVar]
as [Goal]
gs =
let ([TVar]
as1, [Goal]
gs1, Subst
su1, [Warning]
ws) = ([TVar], [Goal], Subst, [Warning])
defLit
([TVar]
as2, [Goal]
gs2, Subst
su2, [Error]
errs) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
improveByDefaultingWithPure [TVar]
as1 [Goal]
gs1
in ([TVar]
as2,[Goal]
gs2,Subst
su2 Subst -> Subst -> Subst
@@ Subst
su1, [Warning]
ws, [Error]
errs)
where
defLit :: ([TVar], [Goal], Subst, [Warning])
defLit
| Subst -> Bool
isEmptySubst Subst
su = forall {a}. ([TVar], [Goal], Subst, [a])
nope
| Bool
otherwise = case Ctxt -> [Goal] -> Either Error (Subst, [Goal])
quickSolver forall a. Monoid a => a
mempty (forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Goal]
gs) of
Left Error
_ -> forall {a}. ([TVar], [Goal], Subst, [a])
nope
Right (Subst
su1,[Goal]
gs1) -> ([TVar]
as1,[Goal]
gs1,Subst
su1Subst -> Subst -> Subst
@@Subst
su,[Warning]
ws)
where ([TVar]
as1,Subst
su,[Warning]
ws) = [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
defaultLiterals [TVar]
as [Goal]
gs
nope :: ([TVar], [Goal], Subst, [a])
nope = ([TVar]
as,[Goal]
gs,Subst
emptySubst,[])
simplifyAllConstraints :: InferM ()
simplifyAllConstraints :: InferM ()
simplifyAllConstraints =
do InferM ()
simpHasGoals
[Goal]
gs <- InferM [Goal]
getGoals
case [Goal]
gs of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
[Goal]
_ ->
case Ctxt -> [Goal] -> Either Error (Subst, [Goal])
quickSolver forall a. Monoid a => a
mempty [Goal]
gs of
Left Error
err -> Error -> InferM ()
recordError Error
err
Right (Subst
su,[Goal]
gs1) ->
do Subst -> InferM ()
extendSubst Subst
su
[Goal] -> InferM ()
addGoals [Goal]
gs1
simpHasGoals :: InferM ()
simpHasGoals :: InferM ()
simpHasGoals = Bool -> [HasGoal] -> [HasGoal] -> InferM ()
go Bool
False [] forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InferM [HasGoal]
getHasGoals
where
go :: Bool -> [HasGoal] -> [HasGoal] -> InferM ()
go Bool
_ [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
go Bool
True [HasGoal]
unsolved [] = Bool -> [HasGoal] -> [HasGoal] -> InferM ()
go Bool
False [] [HasGoal]
unsolved
go Bool
False [HasGoal]
unsolved [] = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ HasGoal -> InferM ()
addHasGoal [HasGoal]
unsolved
go Bool
changes [HasGoal]
unsolved (HasGoal
g : [HasGoal]
todo) =
do (Bool
ch,Bool
solved) <- HasGoal -> InferM (Bool, Bool)
tryHasGoal HasGoal
g
let changes' :: Bool
changes' = Bool
ch Bool -> Bool -> Bool
|| Bool
changes
unsolved' :: [HasGoal]
unsolved' = if Bool
solved then [HasGoal]
unsolved else HasGoal
g forall a. a -> [a] -> [a]
: [HasGoal]
unsolved
Bool
changes' seq :: forall a b. a -> b -> b
`seq` [HasGoal]
unsolved seq :: forall a b. a -> b -> b
`seq` Bool -> [HasGoal] -> [HasGoal] -> InferM ()
go Bool
changes' [HasGoal]
unsolved' [HasGoal]
todo
proveModuleTopLevel :: InferM ()
proveModuleTopLevel :: InferM ()
proveModuleTopLevel =
do InferM ()
simplifyAllConstraints
[Goal]
gs <- InferM [Goal]
getGoals
let vs :: [TVar]
vs = forall a. Set a -> [a]
Set.toList (forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV (forall t. FVS t => t -> Set TVar
fvs [Goal]
gs))
([TVar]
_,[Goal]
gs1,Subst
su1,[Warning]
ws,[Error]
errs) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error])
defaultAndSimplify [TVar]
vs [Goal]
gs
Subst -> InferM ()
extendSubst Subst
su1
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
[Located Type]
cs <- InferM [Located Type]
getParamConstraints
case [Located Type]
cs of
[] -> [Goal] -> InferM ()
addGoals [Goal]
gs1
[Located Type]
_ -> do Subst
su2 <- Bool -> Maybe Name -> [TParam] -> [Type] -> [Goal] -> InferM Subst
proveImplication Bool
False forall a. Maybe a
Nothing [] [] [Goal]
gs1
Subst -> InferM ()
extendSubst Subst
su2
proveImplication :: Bool -> Maybe Name ->
[TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication :: Bool -> Maybe Name -> [TParam] -> [Type] -> [Goal] -> InferM Subst
proveImplication Bool
dedupErrs Maybe Name
lnam [TParam]
as [Type]
ps [Goal]
gs =
do Set TVar
evars <- InferM (Set TVar)
varsWithAsmps
Solver
solver <- InferM Solver
getSolver
[TParam]
extraAs <- (forall a b. (a -> b) -> [a] -> [b]
map ModTParam -> TParam
mtpParam forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
Map.elems) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM (Map Name ModTParam)
getParamTypes
[Type]
extra <- forall a b. (a -> b) -> [a] -> [b]
map forall a. Located a -> a
thing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM [Located Type]
getParamConstraints
(Either [Error] [Warning]
mbErr,Subst
su) <- forall a. IO a -> InferM a
io (Solver
-> Bool
-> Maybe Name
-> Set TVar
-> [TParam]
-> [Type]
-> [Goal]
-> IO (Either [Error] [Warning], Subst)
proveImplicationIO Solver
solver Bool
dedupErrs Maybe Name
lnam Set TVar
evars
([TParam]
extraAs forall a. [a] -> [a] -> [a]
++ [TParam]
as) ([Type]
extra forall a. [a] -> [a] -> [a]
++ [Type]
ps) [Goal]
gs)
case Either [Error] [Warning]
mbErr of
Right [Warning]
ws -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Warning -> InferM ()
recordWarning [Warning]
ws
Left [Error]
errs -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Error -> InferM ()
recordError [Error]
errs
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
su
tryProveImplication ::
Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Bool
tryProveImplication :: Maybe Name -> [TParam] -> [Type] -> [Goal] -> InferM Bool
tryProveImplication Maybe Name
lnam [TParam]
as [Type]
ps [Goal]
gs =
do Set TVar
evars <- InferM (Set TVar)
varsWithAsmps
Solver
solver <- InferM Solver
getSolver
[TParam]
extraAs <- (forall a b. (a -> b) -> [a] -> [b]
map ModTParam -> TParam
mtpParam forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
Map.elems) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM (Map Name ModTParam)
getParamTypes
[Type]
extra <- forall a b. (a -> b) -> [a] -> [b]
map forall a. Located a -> a
thing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM [Located Type]
getParamConstraints
(Either [Error] [Warning]
mbErr,Subst
_su) <- forall a. IO a -> InferM a
io (Solver
-> Bool
-> Maybe Name
-> Set TVar
-> [TParam]
-> [Type]
-> [Goal]
-> IO (Either [Error] [Warning], Subst)
proveImplicationIO Solver
solver Bool
False Maybe Name
lnam Set TVar
evars
([TParam]
extraAs forall a. [a] -> [a] -> [a]
++ [TParam]
as) ([Type]
extra forall a. [a] -> [a] -> [a]
++ [Type]
ps) [Goal]
gs)
case Either [Error] [Warning]
mbErr of
Left {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
Right {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
proveImplicationIO :: Solver
-> Bool
-> Maybe Name
-> Set TVar
-> [TParam]
-> [Prop]
-> [Goal]
-> IO (Either [Error] [Warning], Subst)
proveImplicationIO :: Solver
-> Bool
-> Maybe Name
-> Set TVar
-> [TParam]
-> [Type]
-> [Goal]
-> IO (Either [Error] [Warning], Subst)
proveImplicationIO Solver
_ Bool
_ Maybe Name
_ Set TVar
_ [TParam]
_ [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right [], Subst
emptySubst)
proveImplicationIO Solver
s Bool
dedupErrs Maybe Name
f Set TVar
varsInEnv [TParam]
ps [Type]
asmps0 [Goal]
gs0 =
do let ctxt :: Ctxt
ctxt = [Type] -> Ctxt
buildSolverCtxt [Type]
asmps
Either Error (Subst, [Goal])
res <- Ctxt -> [Goal] -> IO (Either Error (Subst, [Goal]))
quickSolverIO Ctxt
ctxt [Goal]
gs
case Either Error (Subst, [Goal])
res of
Left Error
erro -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left [Error
erro], Subst
emptySubst)
Right (Subst
su,[]) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right [], Subst
su)
Right (Subst
su,[Goal]
gs1) ->
do [Goal]
gs2 <- Solver -> [Type] -> [Goal] -> IO [Goal]
proveImp Solver
s [Type]
asmps [Goal]
gs1
case [Goal]
gs2 of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right [], Subst
su)
[Goal]
gs3 ->
do let free :: [TVar]
free = forall a. (a -> Bool) -> [a] -> [a]
filter TVar -> Bool
isFreeTV
forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList
forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
Set.difference (forall t. FVS t => t -> Set TVar
fvs (forall a b. (a -> b) -> [a] -> [b]
map Goal -> Type
goal [Goal]
gs3)) Set TVar
varsInEnv
case [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error])
defaultAndSimplify [TVar]
free [Goal]
gs3 of
([TVar]
_,[Goal]
_,Subst
newSu,[Warning]
_,[Error]
errs)
| Subst -> Bool
isEmptySubst Subst
newSu ->
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left ([Goal] -> Error
err [Goal]
gs3forall a. a -> [a] -> [a]
:[Error]
errs), Subst
su)
([TVar]
_,[Goal]
newGs,Subst
newSu,[Warning]
ws,[Error]
errs) ->
do let su1 :: Subst
su1 = Subst
newSu Subst -> Subst -> Subst
@@ Subst
su
(Either [Error] [Warning]
res1,Subst
su2) <- Solver
-> Bool
-> Maybe Name
-> Set TVar
-> [TParam]
-> [Type]
-> [Goal]
-> IO (Either [Error] [Warning], Subst)
proveImplicationIO Solver
s Bool
dedupErrs Maybe Name
f Set TVar
varsInEnv [TParam]
ps
(forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 [Type]
asmps0) [Goal]
newGs
let su3 :: Subst
su3 = Subst
su2 Subst -> Subst -> Subst
@@ Subst
su1
case Either [Error] [Warning]
res1 of
Left [Error]
bad -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left ([Error]
bad forall a. [a] -> [a] -> [a]
++ [Error]
errs), Subst
su3)
Right [Warning]
ws1
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Error]
errs -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right ([Warning]
wsforall a. [a] -> [a] -> [a]
++[Warning]
ws1),Subst
su3)
| Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left [Error]
errs, Subst
su3)
where
err :: [Goal] -> Error
err [Goal]
us = Error -> Error
cleanupError
forall a b. (a -> b) -> a -> b
$ DelayedCt -> Error
UnsolvedDelayedCt
forall a b. (a -> b) -> a -> b
$ DelayedCt { dctSource :: Maybe Name
dctSource = Maybe Name
f
, dctForall :: [TParam]
dctForall = [TParam]
ps
, dctAsmps :: [Type]
dctAsmps = [Type]
asmps0
, dctGoals :: [Goal]
dctGoals = if Bool
dedupErrs then forall a. Ord a => [a] -> [a]
nubOrd [Goal]
us else [Goal]
us
}
asmps1 :: [Type]
asmps1 = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
pSplitAnd [Type]
asmps0
([Type]
asmps,[Goal]
gs) =
let gs1 :: [Goal]
gs1 = [ Goal
g { goal :: Type
goal = Type
p } | Goal
g <- [Goal]
gs0, Type
p <- Type -> [Type]
pSplitAnd (Goal -> Type
goal Goal
g)
, forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Type
p [Type]
asmps1 ]
in case forall a. Match a -> Maybe a
matchMaybe (Bool -> Ctxt -> [Type] -> Match (Subst, [Type])
improveProps Bool
True forall a. Monoid a => a
mempty [Type]
asmps1) of
Maybe (Subst, [Type])
Nothing -> ([Type]
asmps1,[Goal]
gs1)
Just (Subst
newSu,[Type]
newAsmps) ->
( [ TVar -> Type
TVar TVar
x Type -> Type -> Type
=#= Type
t | (TVar
x,Type
t) <- Subst -> [(TVar, Type)]
substToList Subst
newSu ]
forall a. [a] -> [a] -> [a]
++ [Type]
newAsmps
, [ Goal
g { goal :: Type
goal = forall t. TVars t => Subst -> t -> t
apSubst Subst
newSu (Goal -> Type
goal Goal
g) } | Goal
g <- [Goal]
gs1 ]
)
cleanupError :: Error -> Error
cleanupError :: Error -> Error
cleanupError Error
err =
case Error
err of
UnsolvedDelayedCt DelayedCt
d ->
let noInferVars :: Goal -> Bool
noInferVars = forall a. Set a -> Bool
Set.null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. FVS t => t -> Set TVar
fvs forall b c a. (b -> c) -> (a -> b) -> a -> c
. Goal -> Type
goal
without :: [Goal]
without = forall a. (a -> Bool) -> [a] -> [a]
filter Goal -> Bool
noInferVars (DelayedCt -> [Goal]
dctGoals DelayedCt
d)
in DelayedCt -> Error
UnsolvedDelayedCt forall a b. (a -> b) -> a -> b
$
if Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Goal]
without) then DelayedCt
d { dctGoals :: [Goal]
dctGoals = [Goal]
without } else DelayedCt
d
Error
_ -> Error
err
buildSolverCtxt :: [Prop] -> Ctxt
buildSolverCtxt :: [Type] -> Ctxt
buildSolverCtxt [Type]
ps0 =
let ps :: Set Type
ps = Set Type -> [Type] -> Set Type
saturateProps forall a. Monoid a => a
mempty [Type]
ps0
ivals :: Map TVar Interval
ivals = Map TVar Interval -> [Type] -> Map TVar Interval
assumptionIntervals forall a. Monoid a => a
mempty (forall a. Set a -> [a]
Set.toList Set Type
ps)
in SolverCtxt
{ intervals :: Map TVar Interval
intervals = Map TVar Interval
ivals
, saturatedAsmps :: Set Type
saturatedAsmps = Set Type
ps
}
where
saturateProps :: Set Type -> [Type] -> Set Type
saturateProps Set Type
gs [] = Set Type
gs
saturateProps Set Type
gs (Type
p:[Type]
ps)
| forall a. Ord a => a -> Set a -> Bool
Set.member Type
p Set Type
gs = Set Type -> [Type] -> Set Type
saturateProps Set Type
gs [Type]
ps
| Just (Type
n,Type
_) <- Type -> Maybe (Type, Type)
pIsLiteral Type
p =
let gs' :: Set Type
gs' = forall a. Ord a => [a] -> Set a
Set.fromList [Type
p, Type -> Type
pFin Type
n] forall a. Semigroup a => a -> a -> a
<> Set Type
gs
in Set Type -> [Type] -> Set Type
saturateProps Set Type
gs' [Type]
ps
| Bool
otherwise =
let gs' :: Set Type
gs' = forall a. a -> Set a
Set.singleton Type
p forall a. Semigroup a => a -> a -> a
<> Type -> Set Type
superclassSet Type
p forall a. Semigroup a => a -> a -> a
<> Set Type
gs
in Set Type -> [Type] -> Set Type
saturateProps Set Type
gs' [Type]
ps
assumptionIntervals :: Map TVar Interval -> [Type] -> Map TVar Interval
assumptionIntervals Map TVar Interval
as [Type]
ps =
case Map TVar Interval -> [Type] -> IntervalUpdate
computePropIntervals Map TVar Interval
as [Type]
ps of
IntervalUpdate
NoChange -> Map TVar Interval
as
InvalidInterval {} -> Map TVar Interval
as
NewIntervals Map TVar Interval
bs -> forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map TVar Interval
bs Map TVar Interval
as