-- |
-- 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           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, identText)
import           Cryptol.Utils.Panic(panic)
import           Cryptol.Utils.Misc(anyJust)
import           Cryptol.Utils.Patterns(matchMaybe)

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 -> 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 (a :: TVar
a,g :: 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 g :: Goal
g =
  do (tn :: Prop
tn,a :: 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 (tn :: Prop
tn,b :: 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 -> Map TVar Goal -> Goals
Goals { goalSet :: Set Goal
goalSet = Set Goal
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 gs :: 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 gs :: 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 g :: Goal
g gs :: Goals
gs
  | Just (a :: TVar
a,newG :: Goal
newG) <- Goal -> Maybe (TVar, Goal)
goalToLitGoal Goal
g =
                Goals
gs { 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
gs) }
  | Bool
otherwise = Goals
gs { goalSet :: Set Goal
goalSet = Goal -> Set Goal -> Set Goal
forall a. Ord a => a -> Set a -> Set a
Set.insert Goal
g (Goals -> Set Goal
goalSet Goals
gs) }

  where
  jn :: Goal -> Goal -> Goal
jn g1 :: Goal
g1 g2 :: Goal
g2 = Goal
g1 { goal :: Prop
goal = Prop -> Prop -> Prop
tMax (Goal -> Prop
goal Goal
g1) (Goal -> Prop
goal Goal
g2) }
  -- XXX: here we are arbitrarily using the info of the first goal,
  -- which could lead to a confusing location for a constraint.

-- | 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
  x :: Goal
x == :: Goal -> Goal -> Bool
== y :: 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 x :: Goal
x y :: 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 Doc         -- ^ 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)



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


instance FVS Goal where
  fvs :: Goal -> Set TVar
fvs g :: 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 d :: 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 su :: Subst
su gs :: 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
                    Nothing  -> Goals
gs
                    Just gs1 :: [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 g :: Goal
g = [ Goal
g { goal :: Prop
goal = Prop
p } | Prop
p <- Prop -> [Prop]
pSplitAnd (Goal -> Prop
goal Goal
g) ]
    apG :: Goal -> Maybe Goal
apG g :: 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 g :: Goal
g p :: Prop
p = Goal
g { goal :: Prop
goal = Prop
p }


instance TVars Goal where
  apSubst :: Subst -> Goal -> Goal
apSubst su :: Subst
su g :: 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 su :: Subst
su h :: 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 su :: Subst
su g :: 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 "Cryptol.TypeCheck.Subst.apSubst (DelayedCt)"
                    [ "Captured quantified variables:"
                    , "Substitution: " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Subst -> FilePath
forall a. Show a => a -> FilePath
show Subst
su
                    , "Variables:    " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Set TVar -> FilePath
forall a. Show a => a -> FilePath
show Set TVar
captured
                    , "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 ki :: Kind
ki =
  case Kind
ki of
    KNum  -> FilePath -> Doc
text "a numeric type"
    KType -> FilePath -> Doc
text "a value type"
    KProp -> FilePath -> Doc
text "a constraint"
    _     -> Kind -> Doc
forall a. PP a => a -> Doc
pp Kind
ki

addTVarsDescsAfter :: FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter :: NameMap -> t -> Doc -> Doc
addTVarsDescsAfter nm :: NameMap
nm t :: t
t d :: 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 "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 v :: TVar
v = NameMap -> TVar -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm TVar
v Doc -> Doc -> Doc
<+> FilePath -> Doc
text "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 nm :: NameMap
nm t :: t
t d :: Doc
d = Doc
frontMsg Doc -> Doc -> Doc
$$ Doc
d Doc -> Doc -> Doc
$$ Doc
backMsg
  where
  (vs1 :: Set TVar
vs1,vs2 :: 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 = "Failed to infer the following types:"
                         Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 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 v :: TVar
v    = "•" 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 = "where"
                         Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 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 v :: TVar
v    = NameMap -> TVar -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm TVar
v Doc -> Doc -> Doc
<+> FilePath -> Doc
text "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 _ src :: ConstraintSource
src =
    case ConstraintSource
src of
      CtComprehension -> "list comprehension"
      CtSplitPat      -> "split (#) pattern"
      CtTypeSig       -> "type signature"
      CtInst e :: Expr
e        -> "use of" Doc -> Doc -> Doc
<+> Expr -> Doc
ppUse Expr
e
      CtSelector      -> "use of selector"
      CtExactType     -> "matching types"
      CtEnumeration   -> "list enumeration"
      CtDefaulting    -> "defaulting"
      CtPartialTypeFun f :: Name
f -> "use of partial type function" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp Name
f
      CtImprovement   -> "examination of collected goals"
      CtPattern desc :: Doc
desc  -> "checking a pattern:" Doc -> Doc -> Doc
<+> Doc
desc
      CtModuleInstance n :: ModName
n -> "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
expr =
  case Expr
expr of
    EVar (Name -> Maybe Ident
asPrim -> Just prim :: Ident
prim)
      | Ident -> Text
identText Ident
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== "number"       -> "literal or demoted expression"
      | Ident -> Text
identText Ident
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== "infFrom"      -> "infinite enumeration"
      | Ident -> Text
identText Ident
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== "infFromThen"  -> "infinite enumeration (with step)"
      | Ident -> Text
identText Ident
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== "fromTo"       -> "finite enumeration"
      | Ident -> Text
identText Ident
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== "fromThenTo"   -> "finite enumeration"
    _                                    -> "expression" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
expr

instance PP (WithNames Goal) where
  ppPrec :: Int -> WithNames Goal -> Doc
ppPrec _ (WithNames g :: Goal
g names :: 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 2 (FilePath -> Doc
text "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 "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 _ (WithNames d :: DelayedCt
d names :: NameMap
names) =
    Doc
sig Doc -> Doc -> Doc
$$ "we need to show that" Doc -> Doc -> Doc
$$
    Int -> Doc -> Doc
nest 2 ([Doc] -> Doc
vcat [ Doc
vars, Doc
asmps, "the following constraints hold:"
                 , Int -> Doc -> Doc
nest 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 xs :: [Doc]
xs = [ "•" Doc -> Doc -> Doc
<+> Doc
x | Doc
x <- [Doc]
xs ]

    sig :: Doc
sig = case Maybe Name
name of
            Just n :: Name
n -> "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
<+> "at" Doc -> Doc -> Doc
<+> Range -> Doc
forall a. PP a => a -> Doc
pp (Name -> Range
nameLoc Name
n) Doc -> Doc -> Doc
<.> Doc
comma
            Nothing -> "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
             xs :: [TParam]
xs -> "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
              xs :: [Prop]
xs -> "assuming" Doc -> Doc -> Doc
$$
                    Int -> Doc -> Doc
nest 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