-- |
-- 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 (ModName, 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
(Int -> SolverConfig -> ShowS)
-> (SolverConfig -> FilePath)
-> ([SolverConfig] -> ShowS)
-> Show SolverConfig
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. SolverConfig -> Rep SolverConfig x)
-> (forall x. Rep SolverConfig x -> SolverConfig)
-> Generic SolverConfig
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 -> ()
(SolverConfig -> ()) -> NFData SolverConfig
forall a. (a -> ()) -> NFData a
rnf :: SolverConfig -> ()
$crnf :: SolverConfig -> ()
NFData)

-- | 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@.
  } deriving (Int -> Goals -> ShowS
[Goals] -> ShowS
Goals -> FilePath
(Int -> Goals -> ShowS)
-> (Goals -> FilePath) -> ([Goals] -> ShowS) -> Show Goals
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) <- Match (Prop, TVar) -> Maybe (Prop, TVar)
forall a. Match a -> Maybe a
matchMaybe (Match (Prop, TVar) -> Maybe (Prop, TVar))
-> Match (Prop, TVar) -> Maybe (Prop, TVar)
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
                               (Prop, TVar) -> Match (Prop, TVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
tn,TVar
a)
     (TVar, Goal) -> Maybe (TVar, Goal)
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
a, Goal
g { goal :: Prop
goal = Prop
tn })



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

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

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

goalsFromList :: [Goal] -> Goals
goalsFromList :: [Goal] -> Goals
goalsFromList = (Goal -> Goals -> Goals) -> Goals -> [Goal] -> Goals
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 = (Goal -> Goal -> Goal)
-> TVar -> Goal -> Map TVar Goal -> Map TVar Goal
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 = Prop -> Set Prop -> Set Prop
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)
           }

  -- If the goal is already implied by some other goal, skip it
  | Prop -> Set Prop -> Bool
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  = (Prop -> Goal) -> Set Prop -> Set Goal
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'  = Goal -> Set Goal -> Set Goal
forall a. Ord a => a -> Set a -> Set a
Set.insert Goal
g (Set Goal -> Set Goal -> Set Goal
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' = Prop -> Set Prop -> Set Prop
forall a. Ord a => a -> Set a -> Set a
Set.insert (Goal -> Prop
goal Goal
g) (Set Prop -> Set Prop -> Set Prop
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
(Int -> Goal -> ShowS)
-> (Goal -> FilePath) -> ([Goal] -> ShowS) -> Show Goal
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. Goal -> Rep Goal x)
-> (forall x. Rep Goal x -> Goal) -> Generic Goal
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 -> ()
(Goal -> ()) -> NFData 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 Prop -> Prop -> Bool
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 = Prop -> Prop -> Ordering
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
  , HasGoal -> Goal
hasGoal :: Goal
  } deriving Int -> HasGoal -> ShowS
[HasGoal] -> ShowS
HasGoal -> FilePath
(Int -> HasGoal -> ShowS)
-> (HasGoal -> FilePath) -> ([HasGoal] -> ShowS) -> Show HasGoal
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
(Int -> DelayedCt -> ShowS)
-> (DelayedCt -> FilePath)
-> ([DelayedCt] -> ShowS)
-> Show DelayedCt
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. DelayedCt -> Rep DelayedCt x)
-> (forall x. Rep DelayedCt x -> DelayedCt) -> Generic DelayedCt
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 -> ()
(DelayedCt -> ()) -> NFData 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 ModName -- ^ Instantiating a parametrized module
    deriving (Int -> ConstraintSource -> ShowS
[ConstraintSource] -> ShowS
ConstraintSource -> FilePath
(Int -> ConstraintSource -> ShowS)
-> (ConstraintSource -> FilePath)
-> ([ConstraintSource] -> ShowS)
-> Show ConstraintSource
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. ConstraintSource -> Rep ConstraintSource x)
-> (forall x. Rep ConstraintSource x -> ConstraintSource)
-> Generic ConstraintSource
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 -> ()
(ConstraintSource -> ()) -> NFData 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 (Subst -> Expr -> Expr
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 ModName
_ -> ConstraintSource
src


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

instance FVS DelayedCt where
  fvs :: DelayedCt -> Set TVar
fvs DelayedCt
d = ([Prop], [Goal]) -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (DelayedCt -> [Prop]
dctAsmps DelayedCt
d, DelayedCt -> [Goal]
dctGoals DelayedCt
d) Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference`
                            [TVar] -> Set TVar
forall a. Ord a => [a] -> Set a
Set.fromList ((TParam -> TVar) -> [TParam] -> [TVar]
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 (Goal -> Maybe Goal) -> [Goal] -> Maybe [Goal]
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 ((Goal -> [Goal]) -> [Goal] -> [Goal]
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 (Prop -> Goal) -> Maybe Prop -> Maybe Goal
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 :: ConstraintSource -> Range -> Prop -> Goal
Goal { goalSource :: ConstraintSource
goalSource = Subst -> ConstraintSource -> ConstraintSource
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       = Subst -> Prop -> Prop
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 = Subst -> Goal -> Goal
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
    | Set TVar -> Bool
forall a. Set a -> Bool
Set.null Set TVar
captured =
       DelayedCt :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> DelayedCt
DelayedCt { dctSource :: Maybe Name
dctSource = DelayedCt -> Maybe Name
dctSource DelayedCt
g
                 , dctForall :: [TParam]
dctForall = DelayedCt -> [TParam]
dctForall DelayedCt
g
                 , dctAsmps :: [Prop]
dctAsmps  = Subst -> [Prop] -> [Prop]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (DelayedCt -> [Prop]
dctAsmps DelayedCt
g)
                 , dctGoals :: [Goal]
dctGoals  = Subst -> [Goal] -> [Goal]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (DelayedCt -> [Goal]
dctGoals DelayedCt
g)
                 }

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

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

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

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

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

  backMsg :: Doc
backMsg  | Set TVar -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set TVar
vs2  = Doc
empty
           | Bool
otherwise = Doc
"where"
                         Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
vcat ((TVar -> Doc) -> [TVar] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TVar -> Doc
desc2 (Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList Set TVar
vs2)))
  desc2 :: TVar -> Doc
desc2 TVar
v    = NameMap -> TVar -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm TVar
v Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"is" Doc -> Doc -> Doc
<+> TVarInfo -> 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
<+> Name -> 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
<+> TypeSource -> Doc
forall a. PP a => a -> Doc
pp TypeSource
ad
      CtModuleInstance ModName
n -> Doc
"module instantiation" Doc -> Doc -> Doc
<+> ModName -> Doc
forall a. PP a => a -> Doc
pp ModName
n

ppUse :: Expr -> Doc
ppUse :: Expr -> Doc
ppUse Expr
expr =
  case Expr
expr of
    EVar (Name -> Maybe Text
isPrelPrim -> Just Text
prim)
      | Text
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"number"       -> Doc
"literal or demoted expression"
      | Text
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"fraction"     -> Doc
"fractional literal"
      | Text
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"infFrom"      -> Doc
"infinite enumeration"
      | Text
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"infFromThen"  -> Doc
"infinite enumeration (with step)"
      | Text
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"fromTo"       -> Doc
"finite enumeration"
      | Text
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"fromThenTo"   -> Doc
"finite enumeration"
    Expr
_                                    -> Doc
"expression" Doc -> Doc -> Doc
<+> Expr -> 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
                    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (ModName
p ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
preludeName)
                    Text -> Maybe Text
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) =
      (NameMap -> Prop -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names (Goal -> Prop
goal Goal
g)) Doc -> Doc -> Doc
$$
               Int -> Doc -> Doc
nest Int
2 (FilePath -> Doc
text FilePath
"arising from" Doc -> Doc -> Doc
$$
                       ConstraintSource -> Doc
forall a. PP a => a -> Doc
pp (Goal -> ConstraintSource
goalSource Goal
g)   Doc -> Doc -> Doc
$$
                       FilePath -> Doc
text FilePath
"at" Doc -> Doc -> Doc
<+> Range -> 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
"we need to show that" Doc -> Doc -> Doc
$$
    Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
vcat [ Doc
vars, Doc
asmps, Doc
"the following constraints hold:"
                 , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat
                          ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> [Doc]
bullets
                          ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Goal -> Doc) -> [Goal] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> Goal -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1)
                          ([Goal] -> [Doc]) -> [Goal] -> [Doc]
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 (Name -> Doc
forall a. PP a => a -> Doc
pp Name
n) Doc -> Doc -> Doc
<.>
                      Doc
comma Doc -> Doc -> Doc
<+> Doc
"at" Doc -> Doc -> Doc
<+> Range -> 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
             [] -> Doc
empty
             [TParam]
xs -> Doc
"for any type" Doc -> Doc -> Doc
<+>
                      [Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((TParam -> Doc) -> [TParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 ) [TParam]
xs))
    asmps :: Doc
asmps = case DelayedCt -> [Prop]
dctAsmps DelayedCt
d of
              [] -> Doc
empty
              [Prop]
xs -> Doc
"assuming" Doc -> Doc -> Doc
$$
                    Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
vcat ([Doc] -> [Doc]
bullets ((Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> Prop -> Doc
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