{-# 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
, SolverConfig -> [FilePath]
solverArgs :: [String]
, SolverConfig -> Int
solverVerbose :: Int
, SolverConfig -> [FilePath]
solverPreludePath :: [FilePath]
} 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)
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
}
data VarType = ExtVar Schema
| CurSCC Expr Type
data Goals = Goals
{ Goals -> Set Goal
goalSet :: Set Goal
, Goals -> Set Prop
saturatedPropSet :: Set Prop
, Goals -> Map TVar Goal
literalGoals :: Map TVar LitGoal
, Goals -> Map TVar Goal
literalLessThanGoals :: Map TVar LitGoal
} 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)
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 =
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)
}
| forall a. Ord a => a -> Set a -> Bool
Set.member (Goal -> Prop
goal Goal
g) (Goals -> Set Prop
saturatedPropSet Goals
gls) = Goals
gls
| 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
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)
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)
data Goal = Goal
{ Goal -> ConstraintSource
goalSource :: ConstraintSource
, Goal -> Range
goalRange :: Range
, Goal -> Prop
goal :: Prop
} 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
, 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
data HasGoalSln = HasGoalSln
{ HasGoalSln -> Expr -> Expr
hasDoSelect :: Expr -> Expr
, HasGoalSln -> Expr -> Expr -> Expr
hasDoSet :: Expr -> Expr -> Expr
}
data DelayedCt = DelayedCt
{ DelayedCt -> Maybe Name
dctSource :: Maybe Name
, 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)
data ConstraintSource
= CtComprehension
| CtSplitPat
| CtTypeSig
| CtInst Expr
| CtSelector
| CtExactType
| CtEnumeration
| CtDefaulting
| CtPartialTypeFun Name
| CtImprovement
| CtPattern TypeSource
| CtModuleInstance Range
| CtPropGuardsExhaustive Name
| CtFFI Name
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
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))
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
| 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