-- |
-- 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.PP (text,vcat,(<+>))
import           Cryptol.Utils.Patterns(matchMaybe)

import           Control.Applicative ((<|>))
import           Control.Monad(mzero)
import qualified Data.Map as Map
import           Data.Set ( Set )
import qualified Data.Set as Set
import           Data.List(partition)
import           Data.Maybe(listToMaybe)





quickSolverIO :: Ctxt -> [Goal] -> IO (Either Goal (Subst,[Goal]))
quickSolverIO :: Ctxt -> [Goal] -> IO (Either Goal (Subst, [Goal]))
quickSolverIO _ [] = Either Goal (Subst, [Goal]) -> IO (Either Goal (Subst, [Goal]))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Subst, [Goal]) -> Either Goal (Subst, [Goal])
forall a b. b -> Either a b
Right (Subst
emptySubst, []))
quickSolverIO ctxt :: Ctxt
ctxt gs :: [Goal]
gs =
  case Ctxt -> [Goal] -> Either Goal (Subst, [Goal])
quickSolver Ctxt
ctxt [Goal]
gs of
    Left err :: Goal
err ->
      do Doc -> IO ()
forall (m :: * -> *) p. Monad m => p -> m ()
msg (String -> Doc
text "Contradiction:" Doc -> Doc -> Doc
<+> Prop -> Doc
forall a. PP a => a -> Doc
pp (Goal -> Prop
goal Goal
err))
         Either Goal (Subst, [Goal]) -> IO (Either Goal (Subst, [Goal]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Goal -> Either Goal (Subst, [Goal])
forall a b. a -> Either a b
Left Goal
err)
    Right (su :: Subst
su,gs' :: [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 Goal (Subst, [Goal]) -> IO (Either Goal (Subst, [Goal]))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Subst, [Goal]) -> Either Goal (Subst, [Goal])
forall a b. b -> Either a b
Right (Subst
su,[Goal]
gs'))
  where
  msg :: p -> m ()
msg _ = () -> 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 Goal (Subst,[Goal])
            -- ^ Left: contradicting goals,
            --   Right: inferred types, unsolved goals.
quickSolver :: Ctxt -> [Goal] -> Either Goal (Subst, [Goal])
quickSolver ctxt :: Ctxt
ctxt gs0 :: [Goal]
gs0 = Subst -> [Goal] -> [Goal] -> Either Goal (Subst, [Goal])
go Subst
emptySubst [] [Goal]
gs0
  where
  go :: Subst -> [Goal] -> [Goal] -> Either Goal (Subst, [Goal])
go su :: Subst
su [] [] = (Subst, [Goal]) -> Either Goal (Subst, [Goal])
forall a b. b -> Either a b
Right (Subst
su,[])

  go su :: Subst
su unsolved :: [Goal]
unsolved [] =
    case Match (Subst, [Goal]) -> Maybe (Subst, [Goal])
forall a. Match a -> Maybe a
matchMaybe ([Goal] -> Match (Subst, [Goal])
findImprovement [Goal]
unsolved) of
      Nothing            -> (Subst, [Goal]) -> Either Goal (Subst, [Goal])
forall a b. b -> Either a b
Right (Subst
su,[Goal]
unsolved)
      Just (newSu :: Subst
newSu, subs :: [Goal]
subs) -> Subst -> [Goal] -> [Goal] -> Either Goal (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)

  go su :: Subst
su unsolved :: [Goal]
unsolved (g :: Goal
g : gs :: [Goal]
gs) =
    case Ctxt -> Prop -> Solved
Simplify.simplifyStep Ctxt
ctxt (Goal -> Prop
goal Goal
g) of
      Unsolvable _        -> Goal -> Either Goal (Subst, [Goal])
forall a b. a -> Either a b
Left Goal
g
      Unsolved            -> Subst -> [Goal] -> [Goal] -> Either Goal (Subst, [Goal])
go Subst
su (Goal
g Goal -> [Goal] -> [Goal]
forall a. a -> [a] -> [a]
: [Goal]
unsolved) [Goal]
gs
      SolvedIf subs :: [Prop]
subs       ->
        let cvt :: Prop -> Goal
cvt x :: Prop
x = Goal
g { goal :: Prop
goal = Prop
x }
        in Subst -> [Goal] -> [Goal] -> Either Goal (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 :: [Goal] -> Match (Subst, [Goal])
findImprovement []       = Match (Subst, [Goal])
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  findImprovement (g :: Goal
g : gs :: [Goal]
gs) =
    do (su :: Subst
su,ps :: [Prop]
ps) <- Bool -> Ctxt -> Prop -> Match (Subst, [Prop])
improveProp Bool
False Ctxt
ctxt (Goal -> Prop
goal Goal
g)
       (Subst, [Goal]) -> Match (Subst, [Goal])
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
su, [ Goal
g { goal :: Prop
goal = Prop
p } | Prop
p <- [Prop]
ps ])
    Match (Subst, [Goal])
-> Match (Subst, [Goal]) -> Match (Subst, [Goal])
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Goal] -> Match (Subst, [Goal])
findImprovement [Goal]
gs





--------------------------------------------------------------------------------


defaultReplExpr :: Solver -> Expr -> Schema ->
                    IO (Maybe ([(TParam,Type)], Expr))

defaultReplExpr :: Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Prop)], Expr))
defaultReplExpr sol :: Solver
sol expr :: Expr
expr sch :: 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
       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 numBinds :: [(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 [[(TParam, Prop)]]
optss <- (TParam -> Maybe [(TParam, Prop)])
-> [TParam] -> Maybe [[(TParam, Prop)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TParam -> Maybe [(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 binds :: [(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)))

  (numVs :: [TParam]
numVs,otherVs :: [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)
  (numPs :: [Prop]
numPs,otherPs :: [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 k :: Kind
k x :: 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 ]

  tryDefVar :: TParam -> Maybe [(TParam, Prop)]
tryDefVar a :: TParam
a =
    do let a' :: TVar
a' = TParam -> TVar
TVBound TParam
a
       Goal
gt <- TVar -> Map TVar Goal -> Maybe Goal
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TVar
a' (Goals -> Map TVar Goal
literalGoals Goals
gSet)
       let ok :: t -> Bool
ok p :: t
p = Bool -> Bool
not (TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member TVar
a' (t -> Set TVar
forall t. FVS t => t -> Set TVar
fvs t
p))
       [(TParam, Prop)] -> Maybe [(TParam, Prop)]
forall (m :: * -> *) a. Monad m => a -> m a
return [ (TParam
a,Prop
t) | Prop
t <- [ Prop
tInteger, Prop
tBit, Prop -> Prop
tWord (Prop -> Prop
tWidth (Goal -> Prop
goal Goal
gt)) ]
                      , Prop -> Bool
forall t. FVS t => t -> Bool
ok Prop
t ]


  appExpr :: t Prop -> Expr
appExpr tys :: t Prop
tys = (Expr -> Prop -> Expr) -> Expr -> [Prop] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\e1 :: Expr
e1 _ -> 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])
defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
defaultAndSimplify as :: [TVar]
as gs :: [Goal]
gs =
  let (as1 :: [TVar]
as1, gs1 :: [Goal]
gs1, su1 :: Subst
su1, ws1 :: [Warning]
ws1) = ([TVar], [Goal], Subst, [Warning])
defLit
      (as2 :: [TVar]
as2, gs2 :: [Goal]
gs2, su2 :: Subst
su2, ws2 :: [Warning]
ws2) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
improveByDefaultingWithPure [TVar]
as1 [Goal]
gs1
  in ([TVar]
as2,[Goal]
gs2,Subst
su2 Subst -> Subst -> Subst
@@ Subst
su1, [Warning]
ws1 [Warning] -> [Warning] -> [Warning]
forall a. [a] -> [a] -> [a]
++ [Warning]
ws2)
  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 Goal (Subst, [Goal])
quickSolver Ctxt
forall k a. Map k a
Map.empty (Subst -> [Goal] -> [Goal]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Goal]
gs) of
                          Left _ -> ([TVar], [Goal], Subst, [Warning])
forall a. ([TVar], [Goal], Subst, [a])
nope -- hm?
                          Right (su1 :: Subst
su1,gs1 :: [Goal]
gs1) -> ([TVar]
as1,[Goal]
gs1,Subst
su1Subst -> Subst -> Subst
@@Subst
su,[Warning]
ws)
    where (as1 :: [TVar]
as1,su :: Subst
su,ws :: [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 ()
       _ ->
        case Ctxt -> [Goal] -> Either Goal (Subst, [Goal])
quickSolver Ctxt
forall k a. Map k a
Map.empty [Goal]
gs of
          Left badG :: Goal
badG      -> Error -> InferM ()
recordError (Bool -> [Goal] -> Error
UnsolvedGoals Bool
True [Goal
badG])
          Right (su :: Subst
su,gs1 :: [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 _     []       []  = () -> InferM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  go True  unsolved :: [HasGoal]
unsolved []  = Bool -> [HasGoal] -> [HasGoal] -> InferM ()
go Bool
False [] [HasGoal]
unsolved
  go False unsolved :: [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 changes :: Bool
changes unsolved :: [HasGoal]
unsolved (g :: HasGoal
g : todo :: [HasGoal]
todo) =
    do (ch :: Bool
ch,solved :: 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 ()
forall a b. a -> b -> b
`seq` [HasGoal]
unsolved [HasGoal] -> InferM () -> InferM ()
forall a b. a -> b -> b
`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))
         (_,gs1 :: [Goal]
gs1,su1 :: Subst
su1,ws :: [Warning]
ws) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
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

     [Located Prop]
cs <- InferM [Located Prop]
getParamConstraints
     case [Located Prop]
cs of
       [] -> [Goal] -> InferM ()
addGoals [Goal]
gs1
       _  -> 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 lnam :: Maybe Name
lnam as :: [TParam]
as ps :: [Prop]
ps gs :: [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

     (mbErr :: Either Error [Warning]
mbErr,su :: 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 ws :: [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 err :: Error
err -> Error -> InferM ()
recordError Error
err
     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 _   _     _         _  [] [] = (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 s :: Solver
s f :: Maybe Name
f varsInEnv :: Set TVar
varsInEnv ps :: [TParam]
ps asmps0 :: [Prop]
asmps0 gs0 :: [Goal]
gs0 =
  do let ctxt :: Ctxt
ctxt = Ctxt -> [Prop] -> Ctxt
assumptionIntervals Ctxt
forall k a. Map k a
Map.empty [Prop]
asmps
     Either Goal (Subst, [Goal])
res <- Ctxt -> [Goal] -> IO (Either Goal (Subst, [Goal]))
quickSolverIO Ctxt
ctxt [Goal]
gs
     case Either Goal (Subst, [Goal])
res of
       Left bad :: Goal
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 (Bool -> [Goal] -> Error
UnsolvedGoals Bool
True [Goal
bad]), Subst
emptySubst)
       Right (su :: 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 (su :: Subst
su,gs1 :: [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)
              gs3 :: [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])
defaultAndSimplify [TVar]
free [Goal]
gs3 of
                     (_,_,newSu :: Subst
newSu,_)
                        | Subst -> Bool
isEmptySubst Subst
newSu ->
                                 (Either Error [Warning], Subst)
-> IO (Either Error [Warning], Subst)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Goal] -> Either Error [Warning]
forall b. [Goal] -> Either Error b
err [Goal]
gs3, Subst
su) -- XXX: Old?
                     (_,newGs :: [Goal]
newGs,newSu :: Subst
newSu,ws :: [Warning]
ws) ->
                       do let su1 :: Subst
su1 = Subst
newSu Subst -> Subst -> Subst
@@ Subst
su
                          (res1 :: Either Error [Warning]
res1,su2 :: 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 bad :: 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, Subst
su3)
                            Right ws1 :: [Warning]
ws1 -> (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)
  where
  err :: [Goal] -> Either Error b
err us :: [Goal]
us =  Error -> Either Error b
forall a b. a -> Either a b
Left (Error -> Either Error b) -> Error -> Either Error b
forall a b. (a -> b) -> a -> b
$ 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
  (asmps :: [Prop]
asmps,gs :: [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 k a. Map k a
Map.empty [Prop]
asmps1) of
          Nothing -> ([Prop]
asmps1,[Goal]
gs1)
          Just (newSu :: Subst
newSu,newAsmps :: [Prop]
newAsmps) ->
             ( [ TVar -> Prop
TVar TVar
x Prop -> Prop -> Prop
=#= Prop
t | (x :: TVar
x,t :: 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 err :: Error
err =
  case Error
err of
    UnsolvedDelayedCt d :: 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
err



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