{-# 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
(Int -> SolverConfig -> ShowS)
-> (SolverConfig -> FilePath)
-> ([SolverConfig] -> ShowS)
-> Show SolverConfig
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SolverConfig -> ShowS
showsPrec :: Int -> SolverConfig -> ShowS
$cshow :: SolverConfig -> FilePath
show :: SolverConfig -> FilePath
$cshowList :: [SolverConfig] -> ShowS
showList :: [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
$cfrom :: forall x. SolverConfig -> Rep SolverConfig x
from :: forall x. SolverConfig -> Rep SolverConfig x
$cto :: forall x. Rep SolverConfig x -> SolverConfig
to :: forall x. Rep SolverConfig x -> SolverConfig
Generic, SolverConfig -> ()
(SolverConfig -> ()) -> NFData SolverConfig
forall a. (a -> ()) -> NFData a
$crnf :: SolverConfig -> ()
rnf :: 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
(Int -> Goals -> ShowS)
-> (Goals -> FilePath) -> ([Goals] -> ShowS) -> Show Goals
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Goals -> ShowS
showsPrec :: Int -> Goals -> ShowS
$cshow :: Goals -> FilePath
show :: Goals -> FilePath
$cshowList :: [Goals] -> ShowS
showList :: [Goals] -> ShowS
Show)
type LitGoal = Goal
litGoalToGoal :: (TVar,LitGoal) -> Goal
litGoalToGoal :: (TVar, Goal) -> Goal
litGoalToGoal (TVar
a,Goal
g) = Goal
g { goal = pLiteral (goal g) (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 a. a -> Match a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
tn,TVar
a)
(TVar, Goal) -> Maybe (TVar, Goal)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
a, Goal
g { goal = tn })
litLessThanGoalToGoal :: (TVar,LitGoal) -> Goal
litLessThanGoalToGoal :: (TVar, Goal) -> Goal
litLessThanGoalToGoal (TVar
a,Goal
g) = Goal
g { goal = pLiteralLessThan (goal g) (TVar a) }
goalToLitLessThanGoal :: Goal -> Maybe (TVar,LitGoal)
goalToLitLessThanGoal :: Goal -> Maybe (TVar, Goal)
goalToLitLessThanGoal 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)
aLiteralLessThan (Goal -> Prop
goal Goal
g)
TVar
a <- Pat Prop TVar
aTVar Prop
b
(Prop, TVar) -> Match (Prop, TVar)
forall a. a -> Match a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
tn,TVar
a)
(TVar, Goal) -> Maybe (TVar, Goal)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
a, Goal
g { goal = tn })
emptyGoals :: Goals
emptyGoals :: Goals
emptyGoals =
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
, literalLessThanGoals :: Map TVar Goal
literalLessThanGoals = 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) Bool -> Bool -> Bool
&&
Map TVar Goal -> 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 = ((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]
++
((TVar, Goal) -> Goal) -> [(TVar, Goal)] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Goal) -> Goal
litLessThanGoalToGoal (Map TVar Goal -> [(TVar, Goal)]
forall k a. Map k a -> [(k, a)]
Map.toList (Goals -> Map TVar Goal
literalLessThanGoals 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 a b. (a -> b -> b) -> b -> [a] -> b
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 = tMax (goal g1) (goal g2) } in
Goals
gls { literalGoals = Map.insertWith jn a newG (literalGoals gls)
, saturatedPropSet = Set.insert (pFin (TVar a)) (saturatedPropSet 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 = tMax (goal g1) (goal g2) } in
Goals
gls { literalLessThanGoals = Map.insertWith jn a newG (literalLessThanGoals gls)
}
| 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
| Bool
otherwise =
Goals
gls { goalSet = gs', saturatedPropSet = 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 = p}) Set Prop
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)
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)
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
$cshowsPrec :: Int -> Goal -> ShowS
showsPrec :: Int -> Goal -> ShowS
$cshow :: Goal -> FilePath
show :: Goal -> FilePath
$cshowList :: [Goal] -> ShowS
showList :: [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
$cfrom :: forall x. Goal -> Rep Goal x
from :: forall x. Goal -> Rep Goal x
$cto :: forall x. Rep Goal x -> Goal
to :: forall x. Rep Goal x -> Goal
Generic, Goal -> ()
(Goal -> ()) -> NFData Goal
forall a. (a -> ()) -> NFData a
$crnf :: Goal -> ()
rnf :: 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
$cshowsPrec :: Int -> HasGoal -> ShowS
showsPrec :: Int -> HasGoal -> ShowS
$cshow :: HasGoal -> FilePath
show :: HasGoal -> FilePath
$cshowList :: [HasGoal] -> ShowS
showList :: [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
$cshowsPrec :: Int -> DelayedCt -> ShowS
showsPrec :: Int -> DelayedCt -> ShowS
$cshow :: DelayedCt -> FilePath
show :: DelayedCt -> FilePath
$cshowList :: [DelayedCt] -> ShowS
showList :: [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
$cfrom :: forall x. DelayedCt -> Rep DelayedCt x
from :: forall x. DelayedCt -> Rep DelayedCt x
$cto :: forall x. Rep DelayedCt x -> DelayedCt
to :: forall x. Rep DelayedCt x -> DelayedCt
Generic, DelayedCt -> ()
(DelayedCt -> ()) -> NFData DelayedCt
forall a. (a -> ()) -> NFData a
$crnf :: DelayedCt -> ()
rnf :: 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
(Int -> ConstraintSource -> ShowS)
-> (ConstraintSource -> FilePath)
-> ([ConstraintSource] -> ShowS)
-> Show ConstraintSource
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConstraintSource -> ShowS
showsPrec :: Int -> ConstraintSource -> ShowS
$cshow :: ConstraintSource -> FilePath
show :: ConstraintSource -> FilePath
$cshowList :: [ConstraintSource] -> ShowS
showList :: [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
$cfrom :: forall x. ConstraintSource -> Rep ConstraintSource x
from :: forall x. ConstraintSource -> Rep ConstraintSource x
$cto :: forall x. Rep ConstraintSource x -> ConstraintSource
to :: forall x. Rep ConstraintSource x -> ConstraintSource
Generic, ConstraintSource -> ()
(ConstraintSource -> ()) -> NFData ConstraintSource
forall a. (a -> ()) -> NFData a
$crnf :: ConstraintSource -> ()
rnf :: 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 Range
_ -> ConstraintSource
src
CtPropGuardsExhaustive Name
_ -> ConstraintSource
src
CtFFI Name
_ -> 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
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 = 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 = p }
instance TVars Goal where
apSubst :: Subst -> Goal -> Goal
apSubst Subst
su Goal
g = 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 = apSubst su (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 { 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))
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 :: forall t. FVS t => 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 :: forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsBefore NameMap
nm t
t Doc
d = [Doc] -> Doc
vcat ([Doc]
frontMsg [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
d] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [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 a. Set a -> Bool
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 ((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 a. Set a -> Bool
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 ((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 Range
r -> Doc
"module instantiation at" Doc -> Doc -> Doc
<+> Range -> 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
<+> Name -> Doc
forall a. PP a => a -> Doc
pp Name
n
CtFFI Name
f -> Doc
"declaration of foreign function" Doc -> Doc -> Doc
<+> Name -> 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 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 a. a -> Maybe a
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 (NameMap -> Prop -> Doc
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
$$
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 -> Int -> Doc -> Doc
hang Doc
"we need to show that"
Int
2 ([Doc] -> Doc
vcat ( [Doc]
vars [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
asmps [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
[ Doc -> Int -> Doc -> Doc
hang Doc
"the following constraints hold:"
Int
2 ([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
[] -> []
[TParam]
xs -> [Doc
"for any type" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep ((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
[] -> []
[Prop]
xs -> [Doc -> Int -> Doc -> Doc
hang Doc
"assuming"
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