-- |
-- Module      :  Cryptol.TypeCheck.Solve
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE PatternGuards, BangPatterns, RecordWildCards #-}
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Solve
  ( simplifyAllConstraints
  , proveImplication
  , proveModuleTopLevel
  , defaultAndSimplify
  , defaultReplExpr
  ) where

import           Cryptol.Parser.Position(thing,emptyRange)
import           Cryptol.TypeCheck.PP -- (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.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
_ [] = Either Error (Subst, [Goal]) -> IO (Either Error (Subst, [Goal]))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Subst, [Goal]) -> Either Error (Subst, [Goal])
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 -> Either Error (Subst, [Goal]) -> IO (Either Error (Subst, [Goal]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Error -> Either Error (Subst, [Goal])
forall a b. a -> Either a b
Left Error
err)
    Right (Subst
su,[Goal]
gs') ->
      do Doc -> IO ()
forall (m :: * -> *) p. Monad m => p -> m ()
msg ([Doc] -> Doc
vcat ((Goal -> Doc) -> [Goal] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Prop -> Doc
forall a. PP a => a -> Doc
pp (Prop -> Doc) -> (Goal -> Prop) -> Goal -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Goal -> Prop
goal) [Goal]
gs' [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Subst -> Doc
forall a. PP a => a -> Doc
pp Subst
su]))
         Either Error (Subst, [Goal]) -> IO (Either Error (Subst, [Goal]))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Subst, [Goal]) -> Either Error (Subst, [Goal])
forall a b. b -> Either a b
Right (Subst
su,[Goal]
gs'))
  where
  msg :: p -> m ()
msg p
_ = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
{-
  shAsmps = case [ pp x <+> text "in" <+> ppInterval i |
               (x,i) <- Map.toList ctxt ] of
              [] -> text ""
              xs -> text "ASMPS:" $$ nest 2 (vcat xs $$ text "===")
  msg d = putStrLn $ show (
             text "quickSolver:" $$ nest 2 (vcat
                [ shAsmps
                , vcat (map (pp.goal) gs)
                , text "==>"
                , d
                ])) -- -}

quickSolver :: Ctxt   -- ^ Facts we can know
            -> [Goal] -- ^ Need to solve these
            -> Either Error (Subst,[Goal])
            -- ^ Left: contradicting goals,
            --   Right: inferred types, unsolved goals.
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 [] [] = (Subst, [Goal]) -> Either Error (Subst, [Goal])
forall a b. b -> Either a b
Right (Subst
su,[])

  go Subst
su [Goal]
unsolved [] =
    case Match (Either Error (Subst, [Goal]))
-> Maybe (Either Error (Subst, [Goal]))
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 -> (Subst, [Goal]) -> Either Error (Subst, [Goal])
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 [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ Subst -> [Goal] -> [Goal]
forall t. TVars t => Subst -> t -> t
apSubst Subst
newSu [Goal]
unsolved)
          Left Error
err -> Error -> Either Error (Subst, [Goal])
forall a b. a -> Either a b
Left Error
err

  go Subst
su [Goal]
unsolved (Goal
g : [Goal]
gs)
    | Prop -> Set Prop -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Goal -> Prop
goal Goal
g) (Ctxt -> Set Prop
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 -> Prop -> Solved
Simplify.simplifyStep Ctxt
ctxt (Goal -> Prop
goal Goal
g) of
      Solved
Unsolvable          -> Error -> Either Error (Subst, [Goal])
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 Goal -> [Goal] -> [Goal]
forall a. a -> [a] -> [a]
: [Goal]
unsolved) [Goal]
gs
      SolvedIf [Prop]
subs       ->
        let cvt :: Prop -> Goal
cvt Prop
x = Goal
g { goal :: Prop
goal = Prop
x }
        in Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
go Subst
su [Goal]
unsolved ((Prop -> Goal) -> [Prop] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Goal
cvt [Prop]
subs [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ [Goal]
gs)

  -- Probably better to find more than one.
  findImprovement :: Incompatible -> [Goal] -> Match (Either Error (Subst, [Goal]))
findImprovement Incompatible
inc [] =
    do let bad :: Map TVar (Goal, Goal)
bad = (Goal -> Goal -> (Goal, Goal))
-> Map TVar Goal -> Map TVar Goal -> Map TVar (Goal, Goal)
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 Map TVar (Goal, Goal)
-> Maybe ((Goal, Goal), Map TVar (Goal, Goal))
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)
_) -> Either Error (Subst, [Goal])
-> Match (Either Error (Subst, [Goal]))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Error (Subst, [Goal])
 -> Match (Either Error (Subst, [Goal])))
-> Either Error (Subst, [Goal])
-> Match (Either Error (Subst, [Goal]))
forall a b. (a -> b) -> a -> b
$ Error -> Either Error (Subst, [Goal])
forall a b. a -> Either a b
Left (Error -> Either Error (Subst, [Goal]))
-> Error -> Either Error (Subst, [Goal])
forall a b. (a -> b) -> a -> b
$ [Goal] -> Error
UnsolvableGoals [Goal
g1,Goal
g2]
         Maybe ((Goal, Goal), Map TVar (Goal, Goal))
Nothing -> Match (Either Error (Subst, [Goal]))
forall (m :: * -> *) a. MonadPlus m => m a
mzero

  findImprovement Incompatible
inc (Goal
g : [Goal]
gs) =
    do (Subst
su,[Prop]
ps) <- Bool -> Ctxt -> Prop -> Match (Subst, [Prop])
improveProp Bool
False Ctxt
ctxt (Goal -> Prop
goal Goal
g)
       Either Error (Subst, [Goal])
-> Match (Either Error (Subst, [Goal]))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Subst, [Goal]) -> Either Error (Subst, [Goal])
forall a b. b -> Either a b
Right (Subst
su, [ Goal
g { goal :: Prop
goal = Prop
p } | Prop
p <- [Prop]
ps ]))
    Match (Either Error (Subst, [Goal]))
-> Match (Either Error (Subst, [Goal]))
-> Match (Either Error (Subst, [Goal]))
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


--------------------------------------------------------------------------------
-- Look for type variable with incompatible constraints

data Incompatible = Incompatible
  { Incompatible -> Map TVar Goal
integralTVars :: Map TVar Goal    -- ^ Integral a
  , Incompatible -> Map TVar Goal
fracTVars     :: Map TVar Goal    -- ^ Field a or FLiteral 
  }

noIncompatible :: Incompatible
noIncompatible :: Incompatible
noIncompatible = Incompatible :: Map TVar Goal -> Map TVar Goal -> Incompatible
Incompatible
  { integralTVars :: Map TVar Goal
integralTVars = Map TVar Goal
forall k a. Map k a
Map.empty
  , fracTVars :: Map TVar Goal
fracTVars     = Map TVar Goal
forall k a. Map k a
Map.empty
  }

addIncompatible :: Goal -> Incompatible -> Incompatible
addIncompatible :: Goal -> Incompatible -> Incompatible
addIncompatible Goal
g Incompatible
i =
  Incompatible -> Maybe Incompatible -> Incompatible
forall a. a -> Maybe a -> a
fromMaybe Incompatible
i (Maybe Incompatible -> Incompatible)
-> Maybe Incompatible -> Incompatible
forall a b. (a -> b) -> a -> b
$
  do TVar
tv <- Prop -> Maybe TVar
tIsVar (Prop -> Maybe TVar) -> Maybe Prop -> Maybe TVar
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Prop -> Maybe Prop
pIsIntegral (Goal -> Prop
goal Goal
g)
     Incompatible -> Maybe Incompatible
forall (f :: * -> *) a. Applicative f => a -> f a
pure Incompatible
i { integralTVars :: Map TVar Goal
integralTVars = TVar -> Goal -> Map TVar Goal -> Map TVar Goal
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) }
  Maybe Incompatible -> Maybe Incompatible -> Maybe Incompatible
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  do TVar
tv <- Prop -> Maybe TVar
tIsVar (Prop -> Maybe TVar) -> Maybe Prop -> Maybe TVar
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Prop -> Maybe Prop
pIsField (Goal -> Prop
goal Goal
g)
     Incompatible -> Maybe Incompatible
forall (f :: * -> *) a. Applicative f => a -> f a
pure Incompatible
i { fracTVars :: Map TVar Goal
fracTVars = TVar -> Goal -> Map TVar Goal -> Map TVar Goal
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) }
  Maybe Incompatible -> Maybe Incompatible -> Maybe Incompatible
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  do (Prop
_,Prop
_,Prop
_,Prop
t) <- Prop -> Maybe (Prop, Prop, Prop, Prop)
pIsFLiteral (Goal -> Prop
goal Goal
g)
     TVar
tv        <- Prop -> Maybe TVar
tIsVar Prop
t
     Incompatible -> Maybe Incompatible
forall (f :: * -> *) a. Applicative f => a -> f a
pure Incompatible
i { fracTVars :: Map TVar Goal
fracTVars = TVar -> Goal -> Map TVar Goal -> Map TVar Goal
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, Prop)], Expr))
defaultReplExpr Solver
sol Expr
expr Schema
sch =
  do Maybe [(TParam, Prop)]
mb <- Solver -> [TParam] -> [Prop] -> IO (Maybe [(TParam, Prop)])
defaultReplExpr' Solver
sol [TParam]
numVs [Prop]
numPs
     case Maybe [(TParam, Prop)]
mb of
       Maybe [(TParam, Prop)]
Nothing -> Maybe ([(TParam, Prop)], Expr)
-> IO (Maybe ([(TParam, Prop)], Expr))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([(TParam, Prop)], Expr)
forall a. Maybe a
Nothing
       Just [(TParam, Prop)]
numBinds -> Maybe ([(TParam, Prop)], Expr)
-> IO (Maybe ([(TParam, Prop)], Expr))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(TParam, Prop)], Expr)
 -> IO (Maybe ([(TParam, Prop)], Expr)))
-> Maybe ([(TParam, Prop)], Expr)
-> IO (Maybe ([(TParam, Prop)], Expr))
forall a b. (a -> b) -> a -> b
$
         do let optss :: [[(TParam, Prop)]]
optss = (TParam -> [(TParam, Prop)]) -> [TParam] -> [[(TParam, Prop)]]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> [(TParam, Prop)]
tryDefVar [TParam]
otherVs
            [(TParam, Prop)]
su    <- [[(TParam, Prop)]] -> Maybe [(TParam, Prop)]
forall a. [a] -> Maybe a
listToMaybe
                       [ [(TParam, Prop)]
binds | [(TParam, Prop)]
nonSu <- [[(TParam, Prop)]] -> [[(TParam, Prop)]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[(TParam, Prop)]]
optss
                               , let binds :: [(TParam, Prop)]
binds = [(TParam, Prop)]
nonSu [(TParam, Prop)] -> [(TParam, Prop)] -> [(TParam, Prop)]
forall a. [a] -> [a] -> [a]
++ [(TParam, Prop)]
numBinds
                               , [(TParam, Prop)] -> Bool
validate [(TParam, Prop)]
binds ]
            [Prop]
tys <- [Maybe Prop] -> Maybe [Prop]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ TParam -> [(TParam, Prop)] -> Maybe Prop
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TParam
v [(TParam, Prop)]
su | TParam
v <- Schema -> [TParam]
sVars Schema
sch ]
            ([(TParam, Prop)], Expr) -> Maybe ([(TParam, Prop)], Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TParam, Prop)]
su, [Prop] -> Expr
forall (t :: * -> *). Foldable t => t Prop -> Expr
appExpr [Prop]
tys)

  where
  validate :: [(TParam, Prop)] -> Bool
validate [(TParam, Prop)]
binds =
    let su :: Subst
su = [(TParam, Prop)] -> Subst
listParamSubst [(TParam, Prop)]
binds
    in [Prop] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((Prop -> [Prop]) -> [Prop] -> [Prop]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Prop -> [Prop]
pSplitAnd (Subst -> [Prop] -> [Prop]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Schema -> [Prop]
sProps Schema
sch)))

  ([TParam]
numVs,[TParam]
otherVs) = (TParam -> Bool) -> [TParam] -> ([TParam], [TParam])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Kind -> TParam -> Bool
forall t. HasKind t => Kind -> t -> Bool
kindIs Kind
KNum) (Schema -> [TParam]
sVars Schema
sch)
  ([Prop]
numPs,[Prop]
otherPs) = (Prop -> Bool) -> [Prop] -> ([Prop], [Prop])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Prop -> Bool
isNumeric (Schema -> [Prop]
sProps Schema
sch)


  kindIs :: Kind -> t -> Bool
kindIs Kind
k t
x = t -> Kind
forall t. HasKind t => t -> Kind
kindOf t
x Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k

  gSet :: Goals
gSet  = [Goal] -> Goals
goalsFromList
           [ Goal :: ConstraintSource -> Range -> Prop -> Goal
Goal { goal :: Prop
goal = Prop
p
                  , goalRange :: Range
goalRange = Range
emptyRange
                  , goalSource :: ConstraintSource
goalSource = ConstraintSource
CtDefaulting } | Prop
p <- [Prop]
otherPs ]

  fLitGoals :: Map TVar (Maybe ((TVar, Prop), Warning))
fLitGoals = Goals -> Map TVar (Maybe ((TVar, Prop), Warning))
flitDefaultCandidates Goals
gSet

  tryDefVar :: TParam -> [(TParam, Type)]
  tryDefVar :: TParam -> [(TParam, Prop)]
tryDefVar TParam
a
    -- REPL defaulting for floating-point literals
    | Just Maybe ((TVar, Prop), Warning)
m <- TVar
-> Map TVar (Maybe ((TVar, Prop), Warning))
-> Maybe (Maybe ((TVar, Prop), Warning))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (TParam -> TVar
TVBound TParam
a) Map TVar (Maybe ((TVar, Prop), Warning))
fLitGoals
    = case Maybe ((TVar, Prop), Warning)
m of
        Just ((TVar
_,Prop
t),Warning
_) -> [(TParam
a,Prop
t)]
        Maybe ((TVar, Prop), Warning)
Nothing        -> []

    -- REPL defaulting for integer literals
    | Just Goal
gt <- TVar -> Map TVar Goal -> Maybe Goal
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 (TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (TParam -> TVar
TVBound TParam
a) (t -> Set TVar
forall t. FVS t => t -> Set TVar
fvs t
p)) in
      [ (TParam
a,Prop
t) | Prop
t <- [ Prop
tInteger, Prop -> Prop
tWord (Prop -> Prop
tWidth (Goal -> Prop
goal Goal
gt)) ]
              , Prop -> Bool
forall t. FVS t => t -> Bool
ok Prop
t ]

    -- REPL defaulting for variables unconstrained by a literal constraint
    | Bool
otherwise = [ (TParam
a,Prop
t) | Prop
t <- [Prop
tInteger, Prop
tRational, Prop
tBit] ]

  appExpr :: t Prop -> Expr
appExpr t Prop
tys = (Expr -> Prop -> Expr) -> Expr -> [Prop] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr
e1 Prop
_ -> Expr -> Expr
EProofApp Expr
e1)
                      ((Expr -> Prop -> Expr) -> Expr -> t Prop -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Prop -> Expr
ETApp Expr
expr t Prop
tys)
                      (Schema -> [Prop]
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 = ([TVar], [Goal], Subst, [Warning])
forall a. ([TVar], [Goal], Subst, [a])
nope
    | Bool
otherwise       = case Ctxt -> [Goal] -> Either Error (Subst, [Goal])
quickSolver Ctxt
forall a. Monoid a => a
mempty (Subst -> [Goal] -> [Goal]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Goal]
gs) of
                          Left Error
_ -> ([TVar], [Goal], Subst, [Warning])
forall a. ([TVar], [Goal], Subst, [a])
nope -- hm?
                          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
       [] -> () -> InferM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       [Goal]
_ ->
        case Ctxt -> [Goal] -> Either Error (Subst, [Goal])
quickSolver Ctxt
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

-- | Simplify @Has@ constraints as much as possible.
simpHasGoals :: InferM ()
simpHasGoals :: InferM ()
simpHasGoals = Bool -> [HasGoal] -> [HasGoal] -> InferM ()
go Bool
False [] ([HasGoal] -> InferM ()) -> InferM [HasGoal] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InferM [HasGoal]
getHasGoals
  where
  go :: Bool -> [HasGoal] -> [HasGoal] -> InferM ()
go Bool
_     []       []  = () -> InferM ()
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 []  = (HasGoal -> InferM ()) -> [HasGoal] -> InferM ()
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 HasGoal -> [HasGoal] -> [HasGoal]
forall a. a -> [a] -> [a]
: [HasGoal]
unsolved
       Bool
changes' Bool -> InferM () -> InferM ()
`seq` [HasGoal]
unsolved [HasGoal] -> InferM () -> InferM ()
`seq` Bool -> [HasGoal] -> [HasGoal] -> InferM ()
go Bool
changes' [HasGoal]
unsolved' [HasGoal]
todo


-- | Try to clean-up any left-over constraints after we've checked everything
-- in a module.  Typically these are either trivial things, or constraints
-- on the module's type parameters.
proveModuleTopLevel :: InferM ()
proveModuleTopLevel :: InferM ()
proveModuleTopLevel =
  do InferM ()
simplifyAllConstraints
     [Goal]
gs <- InferM [Goal]
getGoals
     let vs :: [TVar]
vs = Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList ((TVar -> Bool) -> Set TVar -> Set TVar
forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV ([Goal] -> Set TVar
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
     (Warning -> InferM ()) -> [Warning] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Warning -> InferM ()
recordWarning [Warning]
ws
     (Error -> InferM ()) -> [Error] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Error -> InferM ()
recordError [Error]
errs

     [Located Prop]
cs <- InferM [Located Prop]
getParamConstraints
     case [Located Prop]
cs of
       [] -> [Goal] -> InferM ()
addGoals [Goal]
gs1
       [Located Prop]
_  -> do Subst
su2 <- Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication Maybe Name
forall a. Maybe a
Nothing [] [] [Goal]
gs1
                Subst -> InferM ()
extendSubst Subst
su2

-- | Prove an implication, and return any improvements that we computed.
-- Records errors, if any of the goals couldn't be solved.
proveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication Maybe Name
lnam [TParam]
as [Prop]
ps [Goal]
gs =
  do Set TVar
evars <- InferM (Set TVar)
varsWithAsmps
     Solver
solver <- InferM Solver
getSolver

     [TParam]
extraAs <- ((ModTParam -> TParam) -> [ModTParam] -> [TParam]
forall a b. (a -> b) -> [a] -> [b]
map ModTParam -> TParam
mtpParam ([ModTParam] -> [TParam])
-> (Map Name ModTParam -> [ModTParam])
-> Map Name ModTParam
-> [TParam]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name ModTParam -> [ModTParam]
forall k a. Map k a -> [a]
Map.elems) (Map Name ModTParam -> [TParam])
-> InferM (Map Name ModTParam) -> InferM [TParam]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM (Map Name ModTParam)
getParamTypes
     [Prop]
extra   <- (Located Prop -> Prop) -> [Located Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Located Prop -> Prop
forall a. Located a -> a
thing ([Located Prop] -> [Prop])
-> InferM [Located Prop] -> InferM [Prop]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM [Located Prop]
getParamConstraints

     (Either [Error] [Warning]
mbErr,Subst
su) <- IO (Either [Error] [Warning], Subst)
-> InferM (Either [Error] [Warning], Subst)
forall a. IO a -> InferM a
io (Solver
-> Maybe Name
-> Set TVar
-> [TParam]
-> [Prop]
-> [Goal]
-> IO (Either [Error] [Warning], Subst)
proveImplicationIO Solver
solver Maybe Name
lnam Set TVar
evars
                            ([TParam]
extraAs [TParam] -> [TParam] -> [TParam]
forall a. [a] -> [a] -> [a]
++ [TParam]
as) ([Prop]
extra [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
ps) [Goal]
gs)
     case Either [Error] [Warning]
mbErr of
       Right [Warning]
ws  -> (Warning -> InferM ()) -> [Warning] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Warning -> InferM ()
recordWarning [Warning]
ws
       Left [Error]
errs -> (Error -> InferM ()) -> [Error] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Error -> InferM ()
recordError [Error]
errs
     Subst -> InferM Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
su


proveImplicationIO :: Solver
                   -> Maybe Name     -- ^ Checking this function
                   -> Set TVar -- ^ These appear in the env., and we should
                               -- not try to default them
                   -> [TParam] -- ^ Type parameters
                   -> [Prop]   -- ^ Assumed constraint
                   -> [Goal]   -- ^ Collected constraints
                   -> IO (Either [Error] [Warning], Subst)
proveImplicationIO :: Solver
-> Maybe Name
-> Set TVar
-> [TParam]
-> [Prop]
-> [Goal]
-> IO (Either [Error] [Warning], Subst)
proveImplicationIO Solver
_   Maybe Name
_     Set TVar
_         [TParam]
_  [] [] = (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Warning] -> Either [Error] [Warning]
forall a b. b -> Either a b
Right [], Subst
emptySubst)
proveImplicationIO Solver
s Maybe Name
f Set TVar
varsInEnv [TParam]
ps [Prop]
asmps0 [Goal]
gs0 =
  do let ctxt :: Ctxt
ctxt = [Prop] -> Ctxt
buildSolverCtxt [Prop]
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 -> (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Error] -> Either [Error] [Warning]
forall a b. a -> Either a b
Left [Error
erro], Subst
emptySubst)
       Right (Subst
su,[]) -> (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Warning] -> Either [Error] [Warning]
forall a b. b -> Either a b
Right [], Subst
su)
       Right (Subst
su,[Goal]
gs1) ->
         do [Goal]
gs2 <- Solver -> [Prop] -> [Goal] -> IO [Goal]
proveImp Solver
s [Prop]
asmps [Goal]
gs1
            case [Goal]
gs2 of
              [] -> (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Warning] -> Either [Error] [Warning]
forall a b. b -> Either a b
Right [], Subst
su)
              [Goal]
gs3 ->
                do let free :: [TVar]
free = (TVar -> Bool) -> [TVar] -> [TVar]
forall a. (a -> Bool) -> [a] -> [a]
filter TVar -> Bool
isFreeTV
                            ([TVar] -> [TVar]) -> [TVar] -> [TVar]
forall a b. (a -> b) -> a -> b
$ Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList
                            (Set TVar -> [TVar]) -> Set TVar -> [TVar]
forall a b. (a -> b) -> a -> b
$ Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference ([Prop] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs ((Goal -> Prop) -> [Goal] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Prop
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 ->
                                 (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Error] -> Either [Error] [Warning]
forall a b. a -> Either a b
Left ([Goal] -> Error
err [Goal]
gs3Error -> [Error] -> [Error]
forall a. a -> [a] -> [a]
:[Error]
errs), Subst
su) -- XXX: Old?
                     ([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
-> Maybe Name
-> Set TVar
-> [TParam]
-> [Prop]
-> [Goal]
-> IO (Either [Error] [Warning], Subst)
proveImplicationIO Solver
s Maybe Name
f Set TVar
varsInEnv [TParam]
ps
                                                 (Subst -> [Prop] -> [Prop]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 [Prop]
asmps0) [Goal]
newGs
                          let su3 :: Subst
su3 = Subst
su2 Subst -> Subst -> Subst
@@ Subst
su1
                          case Either [Error] [Warning]
res1 of
                            Left [Error]
bad -> (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Error] -> Either [Error] [Warning]
forall a b. a -> Either a b
Left ([Error]
bad [Error] -> [Error] -> [Error]
forall a. [a] -> [a] -> [a]
++ [Error]
errs), Subst
su3)
                            Right [Warning]
ws1
                              | [Error] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Error]
errs -> (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Warning] -> Either [Error] [Warning]
forall a b. b -> Either a b
Right ([Warning]
ws[Warning] -> [Warning] -> [Warning]
forall a. [a] -> [a] -> [a]
++[Warning]
ws1),Subst
su3)
                              | Bool
otherwise -> (Either [Error] [Warning], Subst)
-> IO (Either [Error] [Warning], Subst)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Error] -> Either [Error] [Warning]
forall a b. a -> Either a b
Left [Error]
errs, Subst
su3)
  where
  err :: [Goal] -> Error
err [Goal]
us = Error -> Error
cleanupError
           (Error -> Error) -> Error -> Error
forall a b. (a -> b) -> a -> b
$ DelayedCt -> Error
UnsolvedDelayedCt
           (DelayedCt -> Error) -> DelayedCt -> Error
forall a b. (a -> b) -> a -> b
$ DelayedCt :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> DelayedCt
DelayedCt { dctSource :: Maybe Name
dctSource = Maybe Name
f
                       , dctForall :: [TParam]
dctForall = [TParam]
ps
                       , dctAsmps :: [Prop]
dctAsmps  = [Prop]
asmps0
                       , dctGoals :: [Goal]
dctGoals  = [Goal]
us
                       }


  asmps1 :: [Prop]
asmps1 = (Prop -> [Prop]) -> [Prop] -> [Prop]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Prop -> [Prop]
pSplitAnd [Prop]
asmps0
  ([Prop]
asmps,[Goal]
gs) =
     let gs1 :: [Goal]
gs1 = [ Goal
g { goal :: Prop
goal = Prop
p } | Goal
g <- [Goal]
gs0, Prop
p <- Prop -> [Prop]
pSplitAnd (Goal -> Prop
goal Goal
g)
                                , Prop -> [Prop] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Prop
p [Prop]
asmps1 ]
     in case Match (Subst, [Prop]) -> Maybe (Subst, [Prop])
forall a. Match a -> Maybe a
matchMaybe (Bool -> Ctxt -> [Prop] -> Match (Subst, [Prop])
improveProps Bool
True Ctxt
forall a. Monoid a => a
mempty [Prop]
asmps1) of
          Maybe (Subst, [Prop])
Nothing -> ([Prop]
asmps1,[Goal]
gs1)
          Just (Subst
newSu,[Prop]
newAsmps) ->
             ( [ TVar -> Prop
TVar TVar
x Prop -> Prop -> Prop
=#= Prop
t | (TVar
x,Prop
t) <- Subst -> [(TVar, Prop)]
substToList Subst
newSu ]
               [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
newAsmps
             , [ Goal
g { goal :: Prop
goal = Subst -> Prop -> Prop
forall t. TVars t => Subst -> t -> t
apSubst Subst
newSu (Goal -> Prop
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 = Set TVar -> Bool
forall a. Set a -> Bool
Set.null (Set TVar -> Bool) -> (Goal -> Set TVar) -> Goal -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TVar -> Bool) -> Set TVar -> Set TVar
forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV (Set TVar -> Set TVar) -> (Goal -> Set TVar) -> Goal -> Set TVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (Prop -> Set TVar) -> (Goal -> Prop) -> Goal -> Set TVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Goal -> Prop
goal
          without :: [Goal]
without = (Goal -> Bool) -> [Goal] -> [Goal]
forall a. (a -> Bool) -> [a] -> [a]
filter Goal -> Bool
noInferVars (DelayedCt -> [Goal]
dctGoals DelayedCt
d)
      in DelayedCt -> Error
UnsolvedDelayedCt (DelayedCt -> Error) -> DelayedCt -> Error
forall a b. (a -> b) -> a -> b
$
            if Bool -> Bool
not ([Goal] -> Bool
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 :: [Prop] -> Ctxt
buildSolverCtxt [Prop]
ps0 =
  let ps :: Set Prop
ps = Set Prop -> [Prop] -> Set Prop
saturateProps Set Prop
forall a. Monoid a => a
mempty [Prop]
ps0
      ivals :: Map TVar Interval
ivals = Map TVar Interval -> [Prop] -> Map TVar Interval
assumptionIntervals Map TVar Interval
forall a. Monoid a => a
mempty (Set Prop -> [Prop]
forall a. Set a -> [a]
Set.toList Set Prop
ps)
   in SolverCtxt :: Map TVar Interval -> Set Prop -> Ctxt
SolverCtxt
      { intervals :: Map TVar Interval
intervals = Map TVar Interval
ivals
      , saturatedAsmps :: Set Prop
saturatedAsmps = Set Prop
ps
      }

 where
 saturateProps :: Set Prop -> [Prop] -> Set Prop
saturateProps Set Prop
gs [] = Set Prop
gs
 saturateProps Set Prop
gs (Prop
p:[Prop]
ps)
   | Prop -> Set Prop -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Prop
p Set Prop
gs = Set Prop -> [Prop] -> Set Prop
saturateProps Set Prop
gs [Prop]
ps
   | Just (Prop
n,Prop
_) <- Prop -> Maybe (Prop, Prop)
pIsLiteral Prop
p =
       let gs' :: Set Prop
gs' = [Prop] -> Set Prop
forall a. Ord a => [a] -> Set a
Set.fromList [Prop
p, Prop -> Prop
pFin Prop
n] Set Prop -> Set Prop -> Set Prop
forall a. Semigroup a => a -> a -> a
<> Set Prop
gs
        in Set Prop -> [Prop] -> Set Prop
saturateProps Set Prop
gs' [Prop]
ps
   | Bool
otherwise =
        let gs' :: Set Prop
gs' = Prop -> Set Prop
forall a. a -> Set a
Set.singleton Prop
p Set Prop -> Set Prop -> Set Prop
forall a. Semigroup a => a -> a -> a
<> Prop -> Set Prop
superclassSet Prop
p Set Prop -> Set Prop -> Set Prop
forall a. Semigroup a => a -> a -> a
<> Set Prop
gs
         in Set Prop -> [Prop] -> Set Prop
saturateProps Set Prop
gs' [Prop]
ps

 assumptionIntervals :: Map TVar Interval -> [Prop] -> Map TVar Interval
assumptionIntervals Map TVar Interval
as [Prop]
ps =
   case Map TVar Interval -> [Prop] -> IntervalUpdate
computePropIntervals Map TVar Interval
as [Prop]
ps of
     IntervalUpdate
NoChange -> Map TVar Interval
as
     InvalidInterval {} -> Map TVar Interval
as -- XXX: say something
     NewIntervals Map TVar Interval
bs -> Map TVar Interval -> Map TVar Interval -> Map TVar Interval
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map TVar Interval
bs Map TVar Interval
as