-- |
-- Module      :  Cryptol.TypeCheck.InferTypes
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
--
-- This module contains types used during type inference.

{-# LANGUAGE Safe #-}

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.TypeCheck.InferTypes where

import           Control.Monad(guard)

import           Cryptol.Parser.Position
import           Cryptol.ModuleSystem.Name (asPrim,nameLoc)
import           Cryptol.TypeCheck.AST
import           Cryptol.TypeCheck.PP
import           Cryptol.TypeCheck.Subst
import           Cryptol.TypeCheck.TypePat
import           Cryptol.TypeCheck.SimpType(tMax)
import           Cryptol.Utils.Ident (PrimIdent(..), preludeName)
import           Cryptol.Utils.Panic(panic)
import           Cryptol.Utils.Misc(anyJust)

import           Data.Set ( Set )
import qualified Data.Set as Set
import           Data.Map ( Map )
import qualified Data.Map as Map

import GHC.Generics (Generic)
import Control.DeepSeq

data SolverConfig = SolverConfig
  { SolverConfig -> FilePath
solverPath    :: FilePath   -- ^ The SMT solver to invoke
  , SolverConfig -> [FilePath]
solverArgs    :: [String]   -- ^ Additional arguments to pass to the solver
  , SolverConfig -> Int
solverVerbose :: Int        -- ^ How verbose to be when type-checking
  , SolverConfig -> [FilePath]
solverPreludePath :: [FilePath]
    -- ^ Look for the solver prelude in these locations.
  } deriving (Int -> SolverConfig -> ShowS
[SolverConfig] -> ShowS
SolverConfig -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [SolverConfig] -> ShowS
$cshowList :: [SolverConfig] -> ShowS
show :: SolverConfig -> FilePath
$cshow :: SolverConfig -> FilePath
showsPrec :: Int -> SolverConfig -> ShowS
$cshowsPrec :: Int -> SolverConfig -> ShowS
Show, forall x. Rep SolverConfig x -> SolverConfig
forall x. SolverConfig -> Rep SolverConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SolverConfig x -> SolverConfig
$cfrom :: forall x. SolverConfig -> Rep SolverConfig x
Generic, SolverConfig -> ()
forall a. (a -> ()) -> NFData a
rnf :: SolverConfig -> ()
$crnf :: SolverConfig -> ()
NFData)


-- | A default configuration for using Z3, where
--   the solver prelude is expected to be found
--   in the given search path.
defaultSolverConfig :: [FilePath] -> SolverConfig
defaultSolverConfig :: [FilePath] -> SolverConfig
defaultSolverConfig [FilePath]
searchPath =
  SolverConfig
  { solverPath :: FilePath
solverPath = FilePath
"z3"
  , solverArgs :: [FilePath]
solverArgs = [ FilePath
"-smt2", FilePath
"-in" ]
  , solverVerbose :: Int
solverVerbose = Int
0
  , solverPreludePath :: [FilePath]
solverPreludePath = [FilePath]
searchPath
  }

-- | The types of variables in the environment.
data VarType = ExtVar Schema
               -- ^ Known type

             | CurSCC {- LAZY -} Expr Type
               {- ^ Part of current SCC.  The expression will replace the
               variable, after we are done with the SCC.  In this way a
               variable that gets generalized is replaced with an appropriate
               instantiation of itself. -}

data Goals = Goals
  { Goals -> Set Goal
goalSet :: Set Goal
    -- ^ A bunch of goals, not including the ones in 'literalGoals'.

  , Goals -> Set Prop
saturatedPropSet :: Set Prop
    -- ^ The set of nonliteral goals, saturated by all superclass implications

  , Goals -> Map TVar Goal
literalGoals :: Map TVar LitGoal
    -- ^ An entry @(a,t)@ corresponds to @Literal t a@.

  , Goals -> Map TVar Goal
literalLessThanGoals :: Map TVar LitGoal
    -- ^ An entry @(a,t)@ corresponds to @LiteralLessThan t a@.

  } deriving (Int -> Goals -> ShowS
[Goals] -> ShowS
Goals -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [Goals] -> ShowS
$cshowList :: [Goals] -> ShowS
show :: Goals -> FilePath
$cshow :: Goals -> FilePath
showsPrec :: Int -> Goals -> ShowS
$cshowsPrec :: Int -> Goals -> ShowS
Show)

-- | This abuses the type 'Goal' a bit. The 'goal' field contains
-- only the numeric part of the Literal constraint.  For example,
-- @(a, Goal { goal = t })@ representats the goal for @Literal t a@
type LitGoal = Goal

litGoalToGoal :: (TVar,LitGoal) -> Goal
litGoalToGoal :: (TVar, Goal) -> Goal
litGoalToGoal (TVar
a,Goal
g) = Goal
g { goal :: Prop
goal = Prop -> Prop -> Prop
pLiteral (Goal -> Prop
goal Goal
g) (TVar -> Prop
TVar TVar
a) }

goalToLitGoal :: Goal -> Maybe (TVar,LitGoal)
goalToLitGoal :: Goal -> Maybe (TVar, Goal)
goalToLitGoal Goal
g =
  do (Prop
tn,TVar
a) <- forall a. Match a -> Maybe a
matchMaybe forall a b. (a -> b) -> a -> b
$ do (Prop
tn,Prop
b) <- Pat Prop (Prop, Prop)
aLiteral (Goal -> Prop
goal Goal
g)
                               TVar
a      <- Pat Prop TVar
aTVar Prop
b
                               forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
tn,TVar
a)
     forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
a, Goal
g { goal :: Prop
goal = Prop
tn })


litLessThanGoalToGoal :: (TVar,LitGoal) -> Goal
litLessThanGoalToGoal :: (TVar, Goal) -> Goal
litLessThanGoalToGoal (TVar
a,Goal
g) = Goal
g { goal :: Prop
goal = Prop -> Prop -> Prop
pLiteralLessThan (Goal -> Prop
goal Goal
g) (TVar -> Prop
TVar TVar
a) }

goalToLitLessThanGoal :: Goal -> Maybe (TVar,LitGoal)
goalToLitLessThanGoal :: Goal -> Maybe (TVar, Goal)
goalToLitLessThanGoal Goal
g =
  do (Prop
tn,TVar
a) <- forall a. Match a -> Maybe a
matchMaybe forall a b. (a -> b) -> a -> b
$ do (Prop
tn,Prop
b) <- Pat Prop (Prop, Prop)
aLiteralLessThan (Goal -> Prop
goal Goal
g)
                               TVar
a      <- Pat Prop TVar
aTVar Prop
b
                               forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
tn,TVar
a)
     forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
a, Goal
g { goal :: Prop
goal = Prop
tn })


emptyGoals :: Goals
emptyGoals :: Goals
emptyGoals  =
  Goals
  { goalSet :: Set Goal
goalSet = forall a. Set a
Set.empty
  , saturatedPropSet :: Set Prop
saturatedPropSet = forall a. Set a
Set.empty
  , literalGoals :: Map TVar Goal
literalGoals = forall k a. Map k a
Map.empty
  , literalLessThanGoals :: Map TVar Goal
literalLessThanGoals = forall k a. Map k a
Map.empty
  }

nullGoals :: Goals -> Bool
nullGoals :: Goals -> Bool
nullGoals Goals
gs =
  forall a. Set a -> Bool
Set.null (Goals -> Set Goal
goalSet Goals
gs) Bool -> Bool -> Bool
&&
  forall k a. Map k a -> Bool
Map.null (Goals -> Map TVar Goal
literalGoals Goals
gs) Bool -> Bool -> Bool
&&
  forall k a. Map k a -> Bool
Map.null (Goals -> Map TVar Goal
literalLessThanGoals Goals
gs)

fromGoals :: Goals -> [Goal]
fromGoals :: Goals -> [Goal]
fromGoals Goals
gs = forall a b. (a -> b) -> [a] -> [b]
map (TVar, Goal) -> Goal
litGoalToGoal (forall k a. Map k a -> [(k, a)]
Map.toList (Goals -> Map TVar Goal
literalGoals Goals
gs)) forall a. [a] -> [a] -> [a]
++
               forall a b. (a -> b) -> [a] -> [b]
map (TVar, Goal) -> Goal
litLessThanGoalToGoal (forall k a. Map k a -> [(k, a)]
Map.toList (Goals -> Map TVar Goal
literalLessThanGoals Goals
gs)) forall a. [a] -> [a] -> [a]
++
               forall a. Set a -> [a]
Set.toList (Goals -> Set Goal
goalSet Goals
gs)

goalsFromList :: [Goal] -> Goals
goalsFromList :: [Goal] -> Goals
goalsFromList = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Goal -> Goals -> Goals
insertGoal Goals
emptyGoals

insertGoal :: Goal -> Goals -> Goals
insertGoal :: Goal -> Goals -> Goals
insertGoal Goal
g Goals
gls
  | Just (TVar
a,Goal
newG) <- Goal -> Maybe (TVar, Goal)
goalToLitGoal Goal
g =
       -- XXX: here we are arbitrarily using the info of the first goal,
       -- which could lead to a confusing location for a constraint.
       let jn :: Goal -> Goal -> Goal
jn Goal
g1 Goal
g2 = Goal
g1 { goal :: Prop
goal = Prop -> Prop -> Prop
tMax (Goal -> Prop
goal Goal
g1) (Goal -> Prop
goal Goal
g2) } in
       Goals
gls { literalGoals :: Map TVar Goal
literalGoals = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Goal -> Goal -> Goal
jn TVar
a Goal
newG (Goals -> Map TVar Goal
literalGoals Goals
gls)
           , saturatedPropSet :: Set Prop
saturatedPropSet = forall a. Ord a => a -> Set a -> Set a
Set.insert (Prop -> Prop
pFin (TVar -> Prop
TVar TVar
a)) (Goals -> Set Prop
saturatedPropSet Goals
gls)
           }

  | Just (TVar
a,Goal
newG) <- Goal -> Maybe (TVar, Goal)
goalToLitLessThanGoal Goal
g =
       let jn :: Goal -> Goal -> Goal
jn Goal
g1 Goal
g2 = Goal
g1 { goal :: Prop
goal = Prop -> Prop -> Prop
tMax (Goal -> Prop
goal Goal
g1) (Goal -> Prop
goal Goal
g2) } in
       Goals
gls { literalLessThanGoals :: Map TVar Goal
literalLessThanGoals = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Goal -> Goal -> Goal
jn TVar
a Goal
newG (Goals -> Map TVar Goal
literalLessThanGoals Goals
gls)
           }

  -- If the goal is already implied by some other goal, skip it
  | forall a. Ord a => a -> Set a -> Bool
Set.member (Goal -> Prop
goal Goal
g) (Goals -> Set Prop
saturatedPropSet Goals
gls) = Goals
gls

  -- Otherwise, it is not already implied, add it and saturate
  | Bool
otherwise =
       Goals
gls { goalSet :: Set Goal
goalSet = Set Goal
gs', saturatedPropSet :: Set Prop
saturatedPropSet = Set Prop
sps'  }

       where
       ips :: Set Prop
ips  = Prop -> Set Prop
superclassSet (Goal -> Prop
goal Goal
g)
       igs :: Set Goal
igs  = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\Prop
p -> Goal
g{ goal :: Prop
goal = Prop
p}) Set Prop
ips

       -- remove all the goals that are implied by ips
       gs' :: Set Goal
gs'  = forall a. Ord a => a -> Set a -> Set a
Set.insert Goal
g (forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Goals -> Set Goal
goalSet Goals
gls) Set Goal
igs)

       -- add the goal and all its implied toals to the saturated set
       sps' :: Set Prop
sps' = forall a. Ord a => a -> Set a -> Set a
Set.insert (Goal -> Prop
goal Goal
g) (forall a. Ord a => Set a -> Set a -> Set a
Set.union (Goals -> Set Prop
saturatedPropSet Goals
gls) Set Prop
ips)


-- | Something that we need to find evidence for.
data Goal = Goal
  { Goal -> ConstraintSource
goalSource :: ConstraintSource  -- ^ What it is about
  , Goal -> Range
goalRange  :: Range             -- ^ Part of source code that caused goal
  , Goal -> Prop
goal       :: Prop              -- ^ What needs to be proved
  } deriving (Int -> Goal -> ShowS
[Goal] -> ShowS
Goal -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [Goal] -> ShowS
$cshowList :: [Goal] -> ShowS
show :: Goal -> FilePath
$cshow :: Goal -> FilePath
showsPrec :: Int -> Goal -> ShowS
$cshowsPrec :: Int -> Goal -> ShowS
Show, forall x. Rep Goal x -> Goal
forall x. Goal -> Rep Goal x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Goal x -> Goal
$cfrom :: forall x. Goal -> Rep Goal x
Generic, Goal -> ()
forall a. (a -> ()) -> NFData a
rnf :: Goal -> ()
$crnf :: Goal -> ()
NFData)

instance Eq Goal where
  Goal
x == :: Goal -> Goal -> Bool
== Goal
y = Goal -> Prop
goal Goal
x forall a. Eq a => a -> a -> Bool
== Goal -> Prop
goal Goal
y

instance Ord Goal where
  compare :: Goal -> Goal -> Ordering
compare Goal
x Goal
y = forall a. Ord a => a -> a -> Ordering
compare (Goal -> Prop
goal Goal
x) (Goal -> Prop
goal Goal
y)

data HasGoal = HasGoal
  { HasGoal -> Int
hasName :: !Int -- ^ This is the "name" of the constraint,
                    -- used to find the solution for ellaboration.
  , HasGoal -> Goal
hasGoal :: Goal
  } deriving Int -> HasGoal -> ShowS
[HasGoal] -> ShowS
HasGoal -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [HasGoal] -> ShowS
$cshowList :: [HasGoal] -> ShowS
show :: HasGoal -> FilePath
$cshow :: HasGoal -> FilePath
showsPrec :: Int -> HasGoal -> ShowS
$cshowsPrec :: Int -> HasGoal -> ShowS
Show


-- | A solution for a 'HasGoal'
data HasGoalSln = HasGoalSln
  { HasGoalSln -> Expr -> Expr
hasDoSelect :: Expr -> Expr
    -- ^ Select a specific field from the input expsression.

  , HasGoalSln -> Expr -> Expr -> Expr
hasDoSet    :: Expr -> Expr -> Expr
    -- ^ Set a field of the first expression to the second expression
  }


-- | Delayed implication constraints, arising from user-specified type sigs.
data DelayedCt = DelayedCt
  { DelayedCt -> Maybe Name
dctSource :: Maybe Name   -- ^ Signature that gave rise to this constraint
                              -- Nothing means module top-level
  , DelayedCt -> [TParam]
dctForall :: [TParam]
  , DelayedCt -> [Prop]
dctAsmps  :: [Prop]
  , DelayedCt -> [Goal]
dctGoals  :: [Goal]
  } deriving (Int -> DelayedCt -> ShowS
[DelayedCt] -> ShowS
DelayedCt -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [DelayedCt] -> ShowS
$cshowList :: [DelayedCt] -> ShowS
show :: DelayedCt -> FilePath
$cshow :: DelayedCt -> FilePath
showsPrec :: Int -> DelayedCt -> ShowS
$cshowsPrec :: Int -> DelayedCt -> ShowS
Show, forall x. Rep DelayedCt x -> DelayedCt
forall x. DelayedCt -> Rep DelayedCt x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DelayedCt x -> DelayedCt
$cfrom :: forall x. DelayedCt -> Rep DelayedCt x
Generic, DelayedCt -> ()
forall a. (a -> ()) -> NFData a
rnf :: DelayedCt -> ()
$crnf :: DelayedCt -> ()
NFData)

-- | Information about how a constraint came to be, used in error reporting.
data ConstraintSource
  = CtComprehension       -- ^ Computing shape of list comprehension
  | CtSplitPat            -- ^ Use of a split pattern
  | CtTypeSig             -- ^ A type signature in a pattern or expression
  | CtInst Expr           -- ^ Instantiation of this expression
  | CtSelector
  | CtExactType
  | CtEnumeration
  | CtDefaulting          -- ^ Just defaulting on the command line
  | CtPartialTypeFun Name -- ^ Use of a partial type function.
  | CtImprovement
  | CtPattern TypeSource  -- ^ Constraints arising from type-checking patterns
  | CtModuleInstance Range -- ^ Instantiating a parametrized module
  | CtPropGuardsExhaustive Name -- ^ Checking that a use of prop guards is exhastive
  | CtFFI Name            -- ^ Constraints on a foreign declaration required
                          --   by the FFI (e.g. sequences must be finite)
    deriving (Int -> ConstraintSource -> ShowS
[ConstraintSource] -> ShowS
ConstraintSource -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [ConstraintSource] -> ShowS
$cshowList :: [ConstraintSource] -> ShowS
show :: ConstraintSource -> FilePath
$cshow :: ConstraintSource -> FilePath
showsPrec :: Int -> ConstraintSource -> ShowS
$cshowsPrec :: Int -> ConstraintSource -> ShowS
Show, forall x. Rep ConstraintSource x -> ConstraintSource
forall x. ConstraintSource -> Rep ConstraintSource x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ConstraintSource x -> ConstraintSource
$cfrom :: forall x. ConstraintSource -> Rep ConstraintSource x
Generic, ConstraintSource -> ()
forall a. (a -> ()) -> NFData a
rnf :: ConstraintSource -> ()
$crnf :: ConstraintSource -> ()
NFData)

selSrc :: Selector -> TypeSource
selSrc :: Selector -> TypeSource
selSrc Selector
l = case Selector
l of
             RecordSel Ident
la Maybe [Ident]
_ -> Ident -> TypeSource
TypeOfRecordField Ident
la
             TupleSel Int
n Maybe Int
_   -> Int -> TypeSource
TypeOfTupleField Int
n
             ListSel Int
_ Maybe Int
_    -> TypeSource
TypeOfSeqElement





instance TVars ConstraintSource where
  apSubst :: Subst -> ConstraintSource -> ConstraintSource
apSubst Subst
su ConstraintSource
src =
    case ConstraintSource
src of
      ConstraintSource
CtComprehension -> ConstraintSource
src
      ConstraintSource
CtSplitPat      -> ConstraintSource
src
      ConstraintSource
CtTypeSig       -> ConstraintSource
src
      CtInst Expr
e        -> Expr -> ConstraintSource
CtInst (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e)
      ConstraintSource
CtSelector      -> ConstraintSource
src
      ConstraintSource
CtExactType     -> ConstraintSource
src
      ConstraintSource
CtEnumeration   -> ConstraintSource
src
      ConstraintSource
CtDefaulting    -> ConstraintSource
src
      CtPartialTypeFun Name
_ -> ConstraintSource
src
      ConstraintSource
CtImprovement    -> ConstraintSource
src
      CtPattern TypeSource
_      -> ConstraintSource
src
      CtModuleInstance Range
_ -> ConstraintSource
src
      CtPropGuardsExhaustive Name
_ -> ConstraintSource
src
      CtFFI Name
_          -> ConstraintSource
src


instance FVS Goal where
  fvs :: Goal -> Set TVar
fvs Goal
g = forall t. FVS t => t -> Set TVar
fvs (Goal -> Prop
goal Goal
g)

instance FVS DelayedCt where
  fvs :: DelayedCt -> Set TVar
fvs DelayedCt
d = forall t. FVS t => t -> Set TVar
fvs (DelayedCt -> [Prop]
dctAsmps DelayedCt
d, DelayedCt -> [Goal]
dctGoals DelayedCt
d) forall a. Ord a => Set a -> Set a -> Set a
`Set.difference`
                            forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar (DelayedCt -> [TParam]
dctForall DelayedCt
d))


instance TVars Goals where
  -- XXX: could be more efficient
  apSubst :: Subst -> Goals -> Goals
apSubst Subst
su Goals
gs = case forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust Goal -> Maybe Goal
apG (Goals -> [Goal]
fromGoals Goals
gs) of
                    Maybe [Goal]
Nothing  -> Goals
gs
                    Just [Goal]
gs1 -> [Goal] -> Goals
goalsFromList (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Goal -> [Goal]
norm [Goal]
gs1)
    where
    norm :: Goal -> [Goal]
norm Goal
g = [ Goal
g { goal :: Prop
goal = Prop
p } | Prop
p <- Prop -> [Prop]
pSplitAnd (Goal -> Prop
goal Goal
g) ]
    apG :: Goal -> Maybe Goal
apG Goal
g  = Goal -> Prop -> Goal
mk Goal
g forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Subst -> Prop -> Maybe Prop
apSubstMaybe Subst
su (Goal -> Prop
goal Goal
g)
    mk :: Goal -> Prop -> Goal
mk Goal
g Prop
p = Goal
g { goal :: Prop
goal = Prop
p }


instance TVars Goal where
  apSubst :: Subst -> Goal -> Goal
apSubst Subst
su Goal
g = Goal { goalSource :: ConstraintSource
goalSource = forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Goal -> ConstraintSource
goalSource Goal
g)
                      , goalRange :: Range
goalRange  = Goal -> Range
goalRange Goal
g
                      , goal :: Prop
goal       = forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Goal -> Prop
goal Goal
g)
                      }

instance TVars HasGoal where
  apSubst :: Subst -> HasGoal -> HasGoal
apSubst Subst
su HasGoal
h = HasGoal
h { hasGoal :: Goal
hasGoal = forall t. TVars t => Subst -> t -> t
apSubst Subst
su (HasGoal -> Goal
hasGoal HasGoal
h) }

instance TVars DelayedCt where
  apSubst :: Subst -> DelayedCt -> DelayedCt
apSubst Subst
su DelayedCt
g
    | forall a. Set a -> Bool
Set.null Set TVar
captured =
       DelayedCt { dctSource :: Maybe Name
dctSource = DelayedCt -> Maybe Name
dctSource DelayedCt
g
                 , dctForall :: [TParam]
dctForall = DelayedCt -> [TParam]
dctForall DelayedCt
g
                 , dctAsmps :: [Prop]
dctAsmps  = forall t. TVars t => Subst -> t -> t
apSubst Subst
su (DelayedCt -> [Prop]
dctAsmps DelayedCt
g)
                 , dctGoals :: [Goal]
dctGoals  = forall t. TVars t => Subst -> t -> t
apSubst Subst
su (DelayedCt -> [Goal]
dctGoals DelayedCt
g)
                 }

    | Bool
otherwise = forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"Cryptol.TypeCheck.Subst.apSubst (DelayedCt)"
                    [ FilePath
"Captured quantified variables:"
                    , FilePath
"Substitution: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show Subst
su
                    , FilePath
"Variables:    " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show Set TVar
captured
                    , FilePath
"Constraint:   " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show DelayedCt
g
                    ]

    where
    captured :: Set TVar
captured = forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar (DelayedCt -> [TParam]
dctForall DelayedCt
g))
               forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection`
               Set TVar
subVars
    subVars :: Set TVar
subVars = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
                forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t. FVS t => t -> Set TVar
fvs forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> TVar -> Maybe Prop
applySubstToVar Subst
su)
                forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set TVar
used
    used :: Set TVar
used = forall t. FVS t => t -> Set TVar
fvs (DelayedCt -> [Prop]
dctAsmps DelayedCt
g, forall a b. (a -> b) -> [a] -> [b]
map Goal -> Prop
goal (DelayedCt -> [Goal]
dctGoals DelayedCt
g)) forall a. Ord a => Set a -> Set a -> Set a
`Set.difference`
                forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar (DelayedCt -> [TParam]
dctForall DelayedCt
g))

-- | For use in error messages
cppKind :: Kind -> Doc
cppKind :: Kind -> Doc
cppKind Kind
ki =
  case Kind
ki of
    Kind
KNum  -> FilePath -> Doc
text FilePath
"a numeric type"
    Kind
KType -> FilePath -> Doc
text FilePath
"a value type"
    Kind
KProp -> FilePath -> Doc
text FilePath
"a constraint"
    Kind
_     -> forall a. PP a => a -> Doc
pp Kind
ki

addTVarsDescsAfter :: FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter :: forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
nm t
t Doc
d
  | forall a. Set a -> Bool
Set.null Set TVar
vs = Doc
d
-- TODO? use `hang` here instead to indent things after "where"
  | Bool
otherwise   = Doc
d Doc -> Doc -> Doc
$$ FilePath -> Doc
text FilePath
"where" Doc -> Doc -> Doc
$$ [Doc] -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map TVar -> Doc
desc (forall a. Set a -> [a]
Set.toList Set TVar
vs))
  where
  vs :: Set TVar
vs     = forall t. FVS t => t -> Set TVar
fvs t
t
  desc :: TVar -> Doc
desc TVar
v = forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm TVar
v Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"is" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (TVar -> TVarInfo
tvInfo TVar
v)

addTVarsDescsBefore :: FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsBefore :: forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsBefore NameMap
nm t
t Doc
d = [Doc] -> Doc
vcat ([Doc]
frontMsg forall a. [a] -> [a] -> [a]
++ [Doc
d] forall a. [a] -> [a] -> [a]
++ [Doc]
backMsg)
  where
  (Set TVar
vs1,Set TVar
vs2)  = forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition TVar -> Bool
isFreeTV (forall t. FVS t => t -> Set TVar
fvs t
t)

  frontMsg :: [Doc]
frontMsg | forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set TVar
vs1  = []
           | Bool
otherwise = [Doc -> Int -> Doc -> Doc
hang Doc
"Failed to infer the following types:"
                             Int
2 ([Doc] -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map TVar -> Doc
desc1 (forall a. Set a -> [a]
Set.toList Set TVar
vs1)))]
  desc1 :: TVar -> Doc
desc1 TVar
v    = Doc
"•" Doc -> Doc -> Doc
<+> forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm TVar
v Doc -> Doc -> Doc
<.> Doc
comma Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (TVar -> TVarInfo
tvInfo TVar
v)

  backMsg :: [Doc]
backMsg  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set TVar
vs2  = []
           | Bool
otherwise = [Doc -> Int -> Doc -> Doc
hang Doc
"where"
                             Int
2 ([Doc] -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map TVar -> Doc
desc2 (forall a. Set a -> [a]
Set.toList Set TVar
vs2)))]
  desc2 :: TVar -> Doc
desc2 TVar
v    = forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm TVar
v Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"is" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (TVar -> TVarInfo
tvInfo TVar
v)



instance PP ConstraintSource where
  ppPrec :: Int -> ConstraintSource -> Doc
ppPrec Int
_ ConstraintSource
src =
    case ConstraintSource
src of
      ConstraintSource
CtComprehension -> Doc
"list comprehension"
      ConstraintSource
CtSplitPat      -> Doc
"split (#) pattern"
      ConstraintSource
CtTypeSig       -> Doc
"type signature"
      CtInst Expr
e        -> Doc
"use of" Doc -> Doc -> Doc
<+> Expr -> Doc
ppUse Expr
e
      ConstraintSource
CtSelector      -> Doc
"use of selector"
      ConstraintSource
CtExactType     -> Doc
"matching types"
      ConstraintSource
CtEnumeration   -> Doc
"list enumeration"
      ConstraintSource
CtDefaulting    -> Doc
"defaulting"
      CtPartialTypeFun Name
f -> Doc
"use of partial type function" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Name
f
      ConstraintSource
CtImprovement   -> Doc
"examination of collected goals"
      CtPattern TypeSource
ad    -> Doc
"checking a pattern:" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp TypeSource
ad
      CtModuleInstance Range
r -> Doc
"module instantiation at" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Range
r
      CtPropGuardsExhaustive Name
n -> Doc
"exhaustion check for prop guards used in defining" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Name
n
      CtFFI Name
f         -> Doc
"declaration of foreign function" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Name
f

ppUse :: Expr -> Doc
ppUse :: Expr -> Doc
ppUse Expr
expr =
  case Expr
expr of
    EVar (Name -> Maybe Text
isPrelPrim -> Just Text
prim)
      | Text
prim forall a. Eq a => a -> a -> Bool
== Text
"number"       -> Doc
"literal or demoted expression"
      | Text
prim forall a. Eq a => a -> a -> Bool
== Text
"fraction"     -> Doc
"fractional literal"
      | Text
prim forall a. Eq a => a -> a -> Bool
== Text
"infFrom"      -> Doc
"infinite enumeration"
      | Text
prim forall a. Eq a => a -> a -> Bool
== Text
"infFromThen"  -> Doc
"infinite enumeration (with step)"
      | Text
prim forall a. Eq a => a -> a -> Bool
== Text
"fromTo"       -> Doc
"finite enumeration"
      | Text
prim forall a. Eq a => a -> a -> Bool
== Text
"fromThenTo"   -> Doc
"finite enumeration"
    Expr
_                          -> Doc
"expression" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Expr
expr
  where
  isPrelPrim :: Name -> Maybe Text
isPrelPrim Name
x = do PrimIdent ModName
p Text
i <- Name -> Maybe PrimIdent
asPrim Name
x
                    forall (f :: * -> *). Alternative f => Bool -> f ()
guard (ModName
p forall a. Eq a => a -> a -> Bool
== ModName
preludeName)
                    forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
i

instance PP (WithNames Goal) where
  ppPrec :: Int -> WithNames Goal -> Doc
ppPrec Int
_ (WithNames Goal
g NameMap
names) =
      Doc -> Int -> Doc -> Doc
hang (forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names (Goal -> Prop
goal Goal
g))
         Int
2 (FilePath -> Doc
text FilePath
"arising from" Doc -> Doc -> Doc
$$
            forall a. PP a => a -> Doc
pp (Goal -> ConstraintSource
goalSource Goal
g)   Doc -> Doc -> Doc
$$
            FilePath -> Doc
text FilePath
"at" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (Goal -> Range
goalRange Goal
g))

instance PP (WithNames DelayedCt) where
  ppPrec :: Int -> WithNames DelayedCt -> Doc
ppPrec Int
_ (WithNames DelayedCt
d NameMap
names) =
    Doc
sig Doc -> Doc -> Doc
$$
    Doc -> Int -> Doc -> Doc
hang Doc
"we need to show that"
       Int
2 ([Doc] -> Doc
vcat ( [Doc]
vars forall a. [a] -> [a] -> [a]
++ [Doc]
asmps forall a. [a] -> [a] -> [a]
++ 
               [ Doc -> Int -> Doc -> Doc
hang Doc
"the following constraints hold:"
                    Int
2 ([Doc] -> Doc
vcat
                       forall a b. (a -> b) -> a -> b
$ [Doc] -> [Doc]
bullets
                       forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1)
                       forall a b. (a -> b) -> a -> b
$ DelayedCt -> [Goal]
dctGoals DelayedCt
d )]))
    where
    bullets :: [Doc] -> [Doc]
bullets [Doc]
xs = [ Doc
"•" Doc -> Doc -> Doc
<+> Doc
x | Doc
x <- [Doc]
xs ]

    sig :: Doc
sig = case Maybe Name
name of
            Just Name
n -> Doc
"in the definition of" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (forall a. PP a => a -> Doc
pp Name
n) Doc -> Doc -> Doc
<.>
                      Doc
comma Doc -> Doc -> Doc
<+> Doc
"at" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (Name -> Range
nameLoc Name
n) Doc -> Doc -> Doc
<.> Doc
comma
            Maybe Name
Nothing -> Doc
"when checking the module's parameters,"

    name :: Maybe Name
name  = DelayedCt -> Maybe Name
dctSource DelayedCt
d
    vars :: [Doc]
vars = case DelayedCt -> [TParam]
dctForall DelayedCt
d of
             [] -> []
             [TParam]
xs -> [Doc
"for any type" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [TParam]
xs)]
    asmps :: [Doc]
asmps = case DelayedCt -> [Prop]
dctAsmps DelayedCt
d of
              [] -> []
              [Prop]
xs -> [Doc -> Int -> Doc -> Doc
hang Doc
"assuming"
                       Int
2 ([Doc] -> Doc
vcat ([Doc] -> [Doc]
bullets (forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [Prop]
xs)))]

    ns1 :: NameMap
ns1 = [TParam] -> NameMap -> NameMap
addTNames (DelayedCt -> [TParam]
dctForall DelayedCt
d) NameMap
names