{-# LANGUAGE Safe #-}

module Cryptol.TypeCheck.Default where

import qualified Data.Set as Set
import           Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe(mapMaybe, isJust)
import Data.List((\\),nub)
import Control.Monad(guard,mzero)

import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.SimpType(tMax)
import Cryptol.TypeCheck.Error(Warning(..), Error(..))
import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,uncheckedSingleSubst)
import Cryptol.TypeCheck.InferTypes(Goal,goal,Goals(..),goalsFromList)
import Cryptol.TypeCheck.Solver.SMT(Solver,tryGetModel,shrinkModel)
import Cryptol.Utils.Panic(panic)

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

-- | We default constraints of the form @Literal t a@ and @FLiteral m n r a@.
--
--   For @Literal t a@ we examine the context of constraints on the type @a@
--   to decide how to default.  If @Logic a@ is required,
--   we cannot do any defaulting.  Otherwise, we default
--   to either @Integer@ or @Rational@.  In particular, if
--   we need to satisfy the @Field a@, constraint, we choose
--   @Rational@ and otherwise we choose @Integer@.
--
--   For @FLiteral t a@ we always default to @Rational@.
defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
defaultLiterals [TVar]
as [Goal]
gs = let ([(TVar, Prop)]
binds,[Warning]
warns) = [((TVar, Prop), Warning)] -> ([(TVar, Prop)], [Warning])
forall a b. [(a, b)] -> ([a], [b])
unzip ((TVar -> Maybe ((TVar, Prop), Warning))
-> [TVar] -> [((TVar, Prop), Warning)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TVar -> Maybe ((TVar, Prop), Warning)
tryDefVar [TVar]
as)
                        in ([TVar]
as [TVar] -> [TVar] -> [TVar]
forall a. Eq a => [a] -> [a] -> [a]
\\ ((TVar, Prop) -> TVar) -> [(TVar, Prop)] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Prop) -> TVar
forall a b. (a, b) -> a
fst [(TVar, Prop)]
binds, [(TVar, Prop)] -> Subst
listSubst [(TVar, Prop)]
binds, [Warning]
warns)
  where
  gSet :: Goals
gSet = [Goal] -> Goals
goalsFromList [Goal]
gs
  allProps :: Set Prop
allProps = Goals -> Set Prop
saturatedPropSet Goals
gSet
  has :: (Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
p TVar
a  = Prop -> Set Prop -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Prop -> Prop
p (TVar -> Prop
TVar TVar
a)) Set Prop
allProps

  isLiteralGoal :: TVar -> Bool
isLiteralGoal TVar
a = Maybe Goal -> Bool
forall a. Maybe a -> Bool
isJust (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)) Bool -> Bool -> Bool
||
                    Maybe Goal -> Bool
forall a. Maybe a -> Bool
isJust (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
literalLessThanGoals Goals
gSet))
  tryDefVar :: TVar -> Maybe ((TVar, Prop), Warning)
tryDefVar TVar
a =
    -- If there is an `FLiteral` constraint we use that for defaulting.
    case 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 TVar
a (Goals -> Map TVar (Maybe ((TVar, Prop), Warning))
flitDefaultCandidates Goals
gSet) of
      Just Maybe ((TVar, Prop), Warning)
m -> Maybe ((TVar, Prop), Warning)
m

      -- Otherwise we try to use a `Literal`
      Maybe (Maybe ((TVar, Prop), Warning))
Nothing
        | TVar -> Bool
isLiteralGoal TVar
a -> do
           Prop
defT <- if (Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
pLogic TVar
a then Maybe Prop
forall a. Maybe a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                   else if (Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
pField TVar
a Bool -> Bool -> Bool
&& Bool -> Bool
not ((Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
pIntegral TVar
a)
                          then Prop -> Maybe Prop
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
tRational
                   else if Bool -> Bool
not ((Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
pField TVar
a) then Prop -> Maybe Prop
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
tInteger
                   else Maybe Prop
forall a. Maybe a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
           let d :: TVarInfo
d    = TVar -> TVarInfo
tvInfo TVar
a
               w :: Warning
w    = TVarInfo -> Prop -> Warning
DefaultingTo TVarInfo
d Prop
defT
           Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member TVar
a (Prop -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Prop
defT)))  -- Currently shouldn't happen
                                                  -- but future proofing.
           -- XXX: Make sure that `defT` has only variables that `a` is allowed
           -- to depend on
           ((TVar, Prop), Warning) -> Maybe ((TVar, Prop), Warning)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((TVar
a,Prop
defT),Warning
w)

        | Bool
otherwise -> Maybe ((TVar, Prop), Warning)
forall a. Maybe a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

flitDefaultCandidates :: Goals -> Map TVar (Maybe ((TVar,Type),Warning))
flitDefaultCandidates :: Goals -> Map TVar (Maybe ((TVar, Prop), Warning))
flitDefaultCandidates Goals
gs =
  [(TVar, Maybe ((TVar, Prop), Warning))]
-> Map TVar (Maybe ((TVar, Prop), Warning))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ((Goal -> Maybe (TVar, Maybe ((TVar, Prop), Warning)))
-> [Goal] -> [(TVar, Maybe ((TVar, Prop), Warning))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Goal -> Maybe (TVar, Maybe ((TVar, Prop), Warning))
forall {m :: * -> *}.
(Monad m, Alternative m) =>
Goal -> Maybe (TVar, m ((TVar, Prop), Warning))
flitCandidate (Set Goal -> [Goal]
forall a. Set a -> [a]
Set.toList (Goals -> Set Goal
goalSet Goals
gs)))
  where
  allProps :: Set Prop
allProps = Goals -> Set Prop
saturatedPropSet Goals
gs
  has :: (Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
p TVar
a  = Prop -> Set Prop -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Prop -> Prop
p (TVar -> Prop
TVar TVar
a)) Set Prop
allProps

  flitCandidate :: Goal -> Maybe (TVar, m ((TVar, Prop), Warning))
flitCandidate Goal
g =
    do (Prop
_,Prop
_,Prop
_,Prop
x) <- Prop -> Maybe (Prop, Prop, Prop, Prop)
pIsFLiteral (Goal -> Prop
goal Goal
g)
       TVar
a         <- Prop -> Maybe TVar
tIsVar Prop
x
       (TVar, m ((TVar, Prop), Warning))
-> Maybe (TVar, m ((TVar, Prop), Warning))
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TVar
a, do Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not ((Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
pLogic TVar
a) Bool -> Bool -> Bool
&& Bool -> Bool
not ((Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
pIntegral TVar
a))
                   let defT :: Prop
defT = Prop
tRational
                   let w :: Warning
w    = TVarInfo -> Prop -> Warning
DefaultingTo (TVar -> TVarInfo
tvInfo TVar
a) Prop
defT
                   ((TVar, Prop), Warning) -> m ((TVar, Prop), Warning)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((TVar
a,Prop
defT),Warning
w))


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

-- This is what we use to avoid ambiguity when generalizing.

{- If a variable, `a`, is:
    1. Of kind KNum
    2. Generic (i.e., does not appear in the environment)
    3. It appears only in constraints but not in the resulting type
       (i.e., it is not on the RHS of =>)
    4. It (say, the variable 'a') appears only in constraints like this:
        3.1 `a >= t` with (`a` not in `fvs t`)
        3.2 in the `s` of `fin s`

  Then we replace `a` with `max(t1 .. tn)` where the `ts`
  are from the constraints `a >= t`.

  If `t1 .. tn` is empty, then we replace `a` with 0.

  This function assumes that 1-3 have been checked, and implements the rest.
  So, given some variables and constraints that are about to be generalized,
  we return:
      1. a new (same or smaller) set of variables to quantify,
      2. a new set of constraints,
      3. a substitution which indicates what got defaulted.
-}





improveByDefaultingWithPure :: [TVar] -> [Goal] ->
    ( [TVar]    -- non-defaulted
    , [Goal]    -- new constraints
    , Subst     -- improvements from defaulting
    , [Error]   -- width defaulting errors
    )
improveByDefaultingWithPure :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
improveByDefaultingWithPure [TVar]
as [Goal]
ps =
  Map TVar ([(Prop, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify ([(TVar, ([(Prop, Goal)], Set TVar))]
-> Map TVar ([(Prop, Goal)], Set TVar)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (TVar
a,([],Set TVar
forall a. Set a
Set.empty)) | TVar
a <- [TVar]
as ]) [] [] [Goal]
ps

  where
  -- leq: candidate definitions (i.e. of the form x >= t, x `notElem` fvs t)
  --      for each of these, we keep the list of `t`, and the free vars in them.
  -- fins: all `fin` constraints
  -- others: any other constraints
  classify :: Map TVar ([(Prop, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify Map TVar ([(Prop, Goal)], Set TVar)
leqs [Goal]
fins [Goal]
others [] =
    let -- First, we use the `leqs` to choose some definitions.
        ([(TVar, Prop)]
defs, [Goal]
newOthers)  = [(TVar, Prop)]
-> [Goal]
-> Set TVar
-> [(TVar, ([(Prop, Goal)], Set TVar))]
-> ([(TVar, Prop)], [Goal])
forall {b}.
TVars b =>
[(TVar, Prop)]
-> [b]
-> Set TVar
-> [(TVar, ([(Prop, b)], Set TVar))]
-> ([(TVar, Prop)], [b])
select [] [] ([Goal] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs [Goal]
others) (Map TVar ([(Prop, Goal)], Set TVar)
-> [(TVar, ([(Prop, Goal)], Set TVar))]
forall k a. Map k a -> [(k, a)]
Map.toList Map TVar ([(Prop, Goal)], Set TVar)
leqs)
        su :: Subst
su                 = [(TVar, Prop)] -> Subst
listSubst [(TVar, Prop)]
defs
        names :: Set TVar
names              = Subst -> Set TVar
substBinds Subst
su
        mkErr :: (TVar, Prop) -> Error
mkErr (TVar
x,Prop
t) =
          case TVar
x of
            TVFree Int
_ Kind
_ Set TParam
_ TVarInfo
d
              | Just Integer
0 <- Prop -> Maybe Integer
tIsNum Prop
t -> TVarInfo -> Maybe Prop -> Error
AmbiguousSize TVarInfo
d Maybe Prop
forall a. Maybe a
Nothing
              | Bool
otherwise -> TVarInfo -> Maybe Prop -> Error
AmbiguousSize TVarInfo
d (Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
t)
            TVBound {} -> String -> [String] -> Error
forall a. HasCallStack => String -> [String] -> a
panic String
"Crypto.TypeCheck.Infer"
                 [ String
"tryDefault attempted to default a quantified variable."
                 ]

    in ( [ TVar
a | TVar
a <- [TVar]
as, Bool -> Bool
not (TVar
a TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
names) ]
       , [Goal]
newOthers [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ [Goal]
others [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ [Goal] -> [Goal]
forall a. Eq a => [a] -> [a]
nub (Subst -> [Goal] -> [Goal]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Goal]
fins)
       , Subst
su
       , ((TVar, Prop) -> Error) -> [(TVar, Prop)] -> [Error]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Prop) -> Error
mkErr [(TVar, Prop)]
defs
       )


  classify Map TVar ([(Prop, Goal)], Set TVar)
leqs [Goal]
fins [Goal]
others (Goal
prop : [Goal]
more) =
      case Prop -> Prop
tNoUser (Goal -> Prop
goal Goal
prop) of

        -- We found a `fin` constraint.
        TCon (PC PC
PFin) [ Prop
_ ] -> Map TVar ([(Prop, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify Map TVar ([(Prop, Goal)], Set TVar)
leqs (Goal
prop Goal -> [Goal] -> [Goal]
forall a. a -> [a] -> [a]
: [Goal]
fins) [Goal]
others [Goal]
more

        -- Things of the form: x >= T(x) are not defaulted.
        TCon (PC PC
PGeq) [ TVar TVar
x, Prop
t ]
          | TVar
x TVar -> [TVar] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TVar]
as Bool -> Bool -> Bool
&& TVar
x TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set TVar
freeRHS ->
           Map TVar ([(Prop, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify Map TVar ([(Prop, Goal)], Set TVar)
leqs' [Goal]
fins [Goal]
others [Goal]
more
           where freeRHS :: Set TVar
freeRHS = Prop -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Prop
t
                 add :: ([a], Set a) -> ([a], Set a) -> ([a], Set a)
add ([a]
xs1,Set a
vs1) ([a]
xs2,Set a
vs2) = ([a]
xs1 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
xs2, Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set a
vs1 Set a
vs2)
                 leqs' :: Map TVar ([(Prop, Goal)], Set TVar)
leqs' = (([(Prop, Goal)], Set TVar)
 -> ([(Prop, Goal)], Set TVar) -> ([(Prop, Goal)], Set TVar))
-> TVar
-> ([(Prop, Goal)], Set TVar)
-> Map TVar ([(Prop, Goal)], Set TVar)
-> Map TVar ([(Prop, Goal)], Set TVar)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith ([(Prop, Goal)], Set TVar)
-> ([(Prop, Goal)], Set TVar) -> ([(Prop, Goal)], Set TVar)
forall {a} {a}.
Ord a =>
([a], Set a) -> ([a], Set a) -> ([a], Set a)
add TVar
x ([(Prop
t,Goal
prop)],Set TVar
freeRHS) Map TVar ([(Prop, Goal)], Set TVar)
leqs

        Prop
_ -> Map TVar ([(Prop, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify Map TVar ([(Prop, Goal)], Set TVar)
leqs [Goal]
fins (Goal
prop Goal -> [Goal] -> [Goal]
forall a. a -> [a] -> [a]
: [Goal]
others) [Goal]
more


  -- Pickout which variables may be defaulted and how.
    -- XXX: simpType t
  select :: [(TVar, Prop)]
-> [b]
-> Set TVar
-> [(TVar, ([(Prop, b)], Set TVar))]
-> ([(TVar, Prop)], [b])
select [(TVar, Prop)]
yes [b]
no Set TVar
_ [] = ([ (TVar
x, Prop
t) | (TVar
x,Prop
t) <- [(TVar, Prop)]
yes ] ,[b]
no)
  select [(TVar, Prop)]
yes [b]
no Set TVar
otherFree ((TVar
x,([(Prop, b)]
rhsG,Set TVar
vs)) : [(TVar, ([(Prop, b)], Set TVar))]
more) =
    [(TVar, Prop)]
-> [b]
-> Set TVar
-> [(TVar, ([(Prop, b)], Set TVar))]
-> ([(TVar, Prop)], [b])
select [(TVar, Prop)]
newYes [b]
newNo Set TVar
newFree [(TVar, ([(Prop, b)], Set TVar))]
newMore

    where
    ([Prop]
ts,[b]
gs) = [(Prop, b)] -> ([Prop], [b])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Prop, b)]
rhsG

    -- `x` selected only if appears nowehere else.
    -- this includes other candidates for defaulting.
    ([(TVar, Prop)]
newYes,[b]
newNo,Set TVar
newFree,[(TVar, ([(Prop, b)], Set TVar))]
newMore)

        -- Mentioned in other constraints, definately not defaultable.
        | TVar
x TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
otherFree = ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
noDefaulting

        | Bool
otherwise =
            let deps :: [TVar]
deps = [ TVar
y | (TVar
y,([(Prop, b)]
_,Set TVar
yvs)) <- [(TVar, ([(Prop, b)], Set TVar))]
more, TVar
x TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
yvs ]
                recs :: [TVar]
recs = (TVar -> Bool) -> [TVar] -> [TVar]
forall a. (a -> Bool) -> [a] -> [a]
filter (TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
vs) [TVar]
deps
            in if Bool -> Bool
not ([TVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TVar]
recs) Bool -> Bool -> Bool
|| TVar -> Bool
isBoundTV TVar
x -- x >= S(y), y >= T(x)
                                 then ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
noDefaulting

                                  -- x >= S,    y >= T(x)   or
                                  -- x >= S(y), y >= S
                                  else ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
yesDefaulting

        where
        noDefaulting :: ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
noDefaulting = ( [(TVar, Prop)]
yes, [b]
gs [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ [b]
no, Set TVar
vs Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set TVar
otherFree, [(TVar, ([(Prop, b)], Set TVar))]
more )

        yesDefaulting :: ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
yesDefaulting =
          let ty :: Prop
ty  = case [Prop]
ts of
                      [] -> Int -> Prop
forall a. Integral a => a -> Prop
tNum (Int
0::Int)
                      [Prop]
_  -> (Prop -> Prop -> Prop) -> [Prop] -> Prop
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Prop -> Prop -> Prop
tMax [Prop]
ts
              su1 :: Subst
su1 = TVar -> Prop -> Subst
uncheckedSingleSubst TVar
x Prop
ty
          in ( (TVar
x,Prop
ty) (TVar, Prop) -> [(TVar, Prop)] -> [(TVar, Prop)]
forall a. a -> [a] -> [a]
: [ (TVar
y,Subst -> Prop -> Prop
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 Prop
t) | (TVar
y,Prop
t) <- [(TVar, Prop)]
yes ]
             , [b]
no         -- We know that `x` does not appear here
             , Set TVar
otherFree  -- We know that `x` did not appear here either

             -- No need to update the `vs` because we've already
             -- checked that there are no recursive dependencies.
             , [ (TVar
y, (Subst -> [(Prop, b)] -> [(Prop, b)]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 [(Prop, b)]
ts1, Set TVar
vs1)) | (TVar
y,([(Prop, b)]
ts1,Set TVar
vs1)) <- [(TVar, ([(Prop, b)], Set TVar))]
more ]
             )


{- | Try to pick a reasonable instantiation for an expression with
the given type.  This is useful when we do evaluation at the REPL.
The resulting types should satisfy the constraints of the schema.
The parameters should be all of numeric kind, and the props should als
be numeric -}
defaultReplExpr' :: Solver -> [TParam] -> [Prop] -> IO (Maybe [ (TParam,Type) ])
defaultReplExpr' :: Solver -> [TParam] -> [Prop] -> IO (Maybe [(TParam, Prop)])
defaultReplExpr' Solver
sol [TParam]
as [Prop]
props =
  do let params :: [TVar]
params = (TParam -> TVar) -> [TParam] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar [TParam]
as
     Maybe [(TVar, Nat')]
mb <- Solver -> [TVar] -> [Prop] -> IO (Maybe [(TVar, Nat')])
tryGetModel Solver
sol [TVar]
params [Prop]
props
     case Maybe [(TVar, Nat')]
mb of
       Maybe [(TVar, Nat')]
Nothing -> Maybe [(TParam, Prop)] -> IO (Maybe [(TParam, Prop)])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [(TParam, Prop)]
forall a. Maybe a
Nothing
       Just [(TVar, Nat')]
mdl0 ->
         do [(TVar, Nat')]
mdl <- Solver -> [TVar] -> [Prop] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
shrinkModel Solver
sol [TVar]
params [Prop]
props [(TVar, Nat')]
mdl0
            let su :: Subst
su = [(TVar, Prop)] -> Subst
listSubst [ (TVar
x, Nat' -> Prop
tNat' Nat'
n) | (TVar
x,Nat'
n) <- [(TVar, Nat')]
mdl ]
            Maybe [(TParam, Prop)] -> IO (Maybe [(TParam, Prop)])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [(TParam, Prop)] -> IO (Maybe [(TParam, Prop)]))
-> Maybe [(TParam, Prop)] -> IO (Maybe [(TParam, Prop)])
forall a b. (a -> b) -> a -> b
$
              do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ([Prop] -> Bool
forall a. [a] -> 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 [Prop]
props)))
                 [Prop]
tys <- (TVar -> Maybe Prop) -> [TVar] -> Maybe [Prop]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Subst -> TVar -> Maybe Prop
forall {m :: * -> *}.
(Monad m, Alternative m) =>
Subst -> TVar -> m Prop
bindParam Subst
su) [TVar]
params
                 [(TParam, Prop)] -> Maybe [(TParam, Prop)]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TParam] -> [Prop] -> [(TParam, Prop)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TParam]
as [Prop]
tys)
  where
  bindParam :: Subst -> TVar -> m Prop
bindParam Subst
su TVar
tp =
    do let ty :: Prop
ty  = TVar -> Prop
TVar TVar
tp
           ty' :: Prop
ty' = Subst -> Prop -> Prop
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Prop
ty
       Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Prop
ty Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
/= Prop
ty')
       Prop -> m Prop
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
ty'