{-# 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
, SolverConfig -> [FilePath]
solverArgs :: [String]
, SolverConfig -> Int
solverVerbose :: Int
, SolverConfig -> [FilePath]
solverPreludePath :: [FilePath]
} 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)
data VarType = ExtVar Schema
| CurSCC Expr Type
data Goals = Goals
{ Goals -> Set Goal
goalSet :: Set Goal
, Goals -> Map TVar Goal
literalGoals :: Map TVar LitGoal
} 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)
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) }
data Goal = Goal
{ Goal -> ConstraintSource
goalSource :: ConstraintSource
, Goal -> Range
goalRange :: Range
, Goal -> Prop
goal :: Prop
} 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
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
(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)
data ConstraintSource
= CtComprehension
| CtSplitPat
| CtTypeSig
| CtInst Expr
| CtSelector
| CtExactType
| CtEnumeration
| CtDefaulting
| CtPartialTypeFun Name
| CtImprovement
| CtPattern Doc
| CtModuleInstance ModName
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
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))
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