module Cryptol.TypeCheck.Default where
import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Maybe(mapMaybe)
import Data.List((\\),nub)
import Control.Monad(guard)
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.SimpType(tMax,tWidth)
import Cryptol.TypeCheck.Error(Warning(..))
import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,singleSubst)
import Cryptol.TypeCheck.InferTypes(Goal,goal,Goals(..),goalsFromList)
import Cryptol.TypeCheck.Solver.SMT(Solver,tryGetModel,shrinkModel)
import Cryptol.Utils.Panic(panic)
defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
defaultLiterals as :: [TVar]
as gs :: [Goal]
gs = let (binds :: [(TVar, Type)]
binds,warns :: [Warning]
warns) = [((TVar, Type), Warning)] -> ([(TVar, Type)], [Warning])
forall a b. [(a, b)] -> ([a], [b])
unzip ((TVar -> Maybe ((TVar, Type), Warning))
-> [TVar] -> [((TVar, Type), Warning)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TVar -> Maybe ((TVar, Type), Warning)
tryDefVar [TVar]
as)
in ([TVar]
as [TVar] -> [TVar] -> [TVar]
forall a. Eq a => [a] -> [a] -> [a]
\\ ((TVar, Type) -> TVar) -> [(TVar, Type)] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Type) -> TVar
forall a b. (a, b) -> a
fst [(TVar, Type)]
binds, [(TVar, Type)] -> Subst
listSubst [(TVar, Type)]
binds, [Warning]
warns)
where
gSet :: Goals
gSet = [Goal] -> Goals
goalsFromList [Goal]
gs
tryDefVar :: TVar -> Maybe ((TVar, Type), Warning)
tryDefVar a :: TVar
a =
do Goal
gt <- TVar -> Map TVar Goal -> Maybe Goal
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TVar
a (Goals -> Map TVar Goal
literalGoals Goals
gSet)
let d :: TVarInfo
d = TVar -> TVarInfo
tvInfo TVar
a
defT :: Type
defT = Type -> Type
tWord (Type -> Type
tWidth (Goal -> Type
goal Goal
gt))
w :: Warning
w = TVarInfo -> Type -> Warning
DefaultingTo TVarInfo
d Type
defT
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member TVar
a (Type -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Type
defT)))
((TVar, Type), Warning) -> Maybe ((TVar, Type), Warning)
forall (m :: * -> *) a. Monad m => a -> m a
return ((TVar
a,Type
defT),Warning
w)
improveByDefaultingWithPure :: [TVar] -> [Goal] ->
( [TVar]
, [Goal]
, Subst
, [Warning]
)
improveByDefaultingWithPure :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
improveByDefaultingWithPure as :: [TVar]
as ps :: [Goal]
ps =
Map TVar ([(Type, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
classify ([(TVar, ([(Type, Goal)], Set TVar))]
-> Map TVar ([(Type, Goal)], Set TVar)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (TVar
a,([],Set TVar
forall a. Set a
Set.empty)) | TVar
a <- [TVar]
as ]) [] [] [Goal]
ps
where
classify :: Map TVar ([(Type, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
classify leqs :: Map TVar ([(Type, Goal)], Set TVar)
leqs fins :: [Goal]
fins others :: [Goal]
others [] =
let
(defs :: [(TVar, Type)]
defs, newOthers :: [Goal]
newOthers) = [(TVar, Type)]
-> [Goal]
-> Set TVar
-> [(TVar, ([(Type, Goal)], Set TVar))]
-> ([(TVar, Type)], [Goal])
forall b.
TVars b =>
[(TVar, Type)]
-> [b]
-> Set TVar
-> [(TVar, ([(Type, b)], Set TVar))]
-> ([(TVar, Type)], [b])
select [] [] ([Goal] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs [Goal]
others) (Map TVar ([(Type, Goal)], Set TVar)
-> [(TVar, ([(Type, Goal)], Set TVar))]
forall k a. Map k a -> [(k, a)]
Map.toList Map TVar ([(Type, Goal)], Set TVar)
leqs)
su :: Subst
su = [(TVar, Type)] -> Subst
listSubst [(TVar, Type)]
defs
warn :: (TVar, Type) -> Warning
warn (x :: TVar
x,t :: Type
t) =
case TVar
x of
TVFree _ _ _ d :: TVarInfo
d -> TVarInfo -> Type -> Warning
DefaultingTo TVarInfo
d Type
t
TVBound {} -> String -> [String] -> Warning
forall a. HasCallStack => String -> [String] -> a
panic "Crypto.TypeCheck.Infer"
[ "tryDefault attempted to default a quantified variable."
]
names :: Set TVar
names = Subst -> Set TVar
substBinds Subst
su
in ( [ TVar
a | TVar
a <- [TVar]
as, Bool -> Bool
not (TVar
a TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
names) ]
, [Goal]
newOthers [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ [Goal]
others [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ [Goal] -> [Goal]
forall a. Eq a => [a] -> [a]
nub (Subst -> [Goal] -> [Goal]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Goal]
fins)
, Subst
su
, ((TVar, Type) -> Warning) -> [(TVar, Type)] -> [Warning]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Type) -> Warning
warn [(TVar, Type)]
defs
)
classify leqs :: Map TVar ([(Type, Goal)], Set TVar)
leqs fins :: [Goal]
fins others :: [Goal]
others (prop :: Goal
prop : more :: [Goal]
more) =
case Type -> Type
tNoUser (Goal -> Type
goal Goal
prop) of
TCon (PC PFin) [ _ ] -> Map TVar ([(Type, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
classify Map TVar ([(Type, Goal)], Set TVar)
leqs (Goal
prop Goal -> [Goal] -> [Goal]
forall a. a -> [a] -> [a]
: [Goal]
fins) [Goal]
others [Goal]
more
TCon (PC PGeq) [ TVar x :: TVar
x, t :: Type
t ]
| TVar
x TVar -> [TVar] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TVar]
as Bool -> Bool -> Bool
&& TVar
x TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set TVar
freeRHS ->
Map TVar ([(Type, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
classify Map TVar ([(Type, Goal)], Set TVar)
leqs' [Goal]
fins [Goal]
others [Goal]
more
where freeRHS :: Set TVar
freeRHS = Type -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Type
t
add :: ([a], Set a) -> ([a], Set a) -> ([a], Set a)
add (xs1 :: [a]
xs1,vs1 :: Set a
vs1) (xs2 :: [a]
xs2,vs2 :: Set a
vs2) = ([a]
xs1 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
xs2, Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set a
vs1 Set a
vs2)
leqs' :: Map TVar ([(Type, Goal)], Set TVar)
leqs' = (([(Type, Goal)], Set TVar)
-> ([(Type, Goal)], Set TVar) -> ([(Type, Goal)], Set TVar))
-> TVar
-> ([(Type, Goal)], Set TVar)
-> Map TVar ([(Type, Goal)], Set TVar)
-> Map TVar ([(Type, Goal)], Set TVar)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith ([(Type, Goal)], Set TVar)
-> ([(Type, Goal)], Set TVar) -> ([(Type, Goal)], Set TVar)
forall a a. Ord a => ([a], Set a) -> ([a], Set a) -> ([a], Set a)
add TVar
x ([(Type
t,Goal
prop)],Set TVar
freeRHS) Map TVar ([(Type, Goal)], Set TVar)
leqs
_ -> Map TVar ([(Type, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
classify Map TVar ([(Type, Goal)], Set TVar)
leqs [Goal]
fins (Goal
prop Goal -> [Goal] -> [Goal]
forall a. a -> [a] -> [a]
: [Goal]
others) [Goal]
more
select :: [(TVar, Type)]
-> [b]
-> Set TVar
-> [(TVar, ([(Type, b)], Set TVar))]
-> ([(TVar, Type)], [b])
select yes :: [(TVar, Type)]
yes no :: [b]
no _ [] = ([ (TVar
x, Type
t) | (x :: TVar
x,t :: Type
t) <- [(TVar, Type)]
yes ] ,[b]
no)
select yes :: [(TVar, Type)]
yes no :: [b]
no otherFree :: Set TVar
otherFree ((x :: TVar
x,(rhsG :: [(Type, b)]
rhsG,vs :: Set TVar
vs)) : more :: [(TVar, ([(Type, b)], Set TVar))]
more) =
[(TVar, Type)]
-> [b]
-> Set TVar
-> [(TVar, ([(Type, b)], Set TVar))]
-> ([(TVar, Type)], [b])
select [(TVar, Type)]
newYes [b]
newNo Set TVar
newFree [(TVar, ([(Type, b)], Set TVar))]
newMore
where
(ts :: [Type]
ts,gs :: [b]
gs) = [(Type, b)] -> ([Type], [b])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Type, b)]
rhsG
(newYes :: [(TVar, Type)]
newYes,newNo :: [b]
newNo,newFree :: Set TVar
newFree,newMore :: [(TVar, ([(Type, b)], Set TVar))]
newMore)
| TVar
x TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
otherFree = ([(TVar, Type)], [b], Set TVar, [(TVar, ([(Type, b)], Set TVar))])
noDefaulting
| Bool
otherwise =
let deps :: [TVar]
deps = [ TVar
y | (y :: TVar
y,(_,yvs :: Set TVar
yvs)) <- [(TVar, ([(Type, b)], Set TVar))]
more, TVar
x TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
yvs ]
recs :: [TVar]
recs = (TVar -> Bool) -> [TVar] -> [TVar]
forall a. (a -> Bool) -> [a] -> [a]
filter (TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
vs) [TVar]
deps
in if Bool -> Bool
not ([TVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TVar]
recs) Bool -> Bool -> Bool
|| TVar -> Bool
isBoundTV TVar
x
then ([(TVar, Type)], [b], Set TVar, [(TVar, ([(Type, b)], Set TVar))])
noDefaulting
else ([(TVar, Type)], [b], Set TVar, [(TVar, ([(Type, b)], Set TVar))])
yesDefaulting
where
noDefaulting :: ([(TVar, Type)], [b], Set TVar, [(TVar, ([(Type, b)], Set TVar))])
noDefaulting = ( [(TVar, Type)]
yes, [b]
gs [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ [b]
no, Set TVar
vs Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set TVar
otherFree, [(TVar, ([(Type, b)], Set TVar))]
more )
yesDefaulting :: ([(TVar, Type)], [b], Set TVar, [(TVar, ([(Type, b)], Set TVar))])
yesDefaulting =
let ty :: Type
ty = case [Type]
ts of
[] -> Int -> Type
forall a. Integral a => a -> Type
tNum (0::Int)
_ -> (Type -> Type -> Type) -> [Type] -> Type
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
tMax [Type]
ts
su1 :: Subst
su1 = TVar -> Type -> Subst
singleSubst TVar
x Type
ty
in ( (TVar
x,Type
ty) (TVar, Type) -> [(TVar, Type)] -> [(TVar, Type)]
forall a. a -> [a] -> [a]
: [ (TVar
y,Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 Type
t) | (y :: TVar
y,t :: Type
t) <- [(TVar, Type)]
yes ]
, [b]
no
, Set TVar
otherFree
, [ (TVar
y, (Subst -> [(Type, b)] -> [(Type, b)]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 [(Type, b)]
ts1, Set TVar
vs1)) | (y :: TVar
y,(ts1 :: [(Type, b)]
ts1,vs1 :: Set TVar
vs1)) <- [(TVar, ([(Type, b)], Set TVar))]
more ]
)
defaultReplExpr' :: Solver -> [TParam] -> [Prop] -> IO (Maybe [ (TParam,Type) ])
defaultReplExpr' :: Solver -> [TParam] -> [Type] -> IO (Maybe [(TParam, Type)])
defaultReplExpr' sol :: Solver
sol as :: [TParam]
as props :: [Type]
props =
do let params :: [TVar]
params = (TParam -> TVar) -> [TParam] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar [TParam]
as
Maybe [(TVar, Nat')]
mb <- Solver -> [TVar] -> [Type] -> IO (Maybe [(TVar, Nat')])
tryGetModel Solver
sol [TVar]
params [Type]
props
case Maybe [(TVar, Nat')]
mb of
Nothing -> Maybe [(TParam, Type)] -> IO (Maybe [(TParam, Type)])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [(TParam, Type)]
forall a. Maybe a
Nothing
Just mdl0 :: [(TVar, Nat')]
mdl0 ->
do [(TVar, Nat')]
mdl <- Solver -> [TVar] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
shrinkModel Solver
sol [TVar]
params [Type]
props [(TVar, Nat')]
mdl0
let su :: Subst
su = [(TVar, Type)] -> Subst
listSubst [ (TVar
x, Nat' -> Type
tNat' Nat'
n) | (x :: TVar
x,n :: Nat'
n) <- [(TVar, Nat')]
mdl ]
Maybe [(TParam, Type)] -> IO (Maybe [(TParam, Type)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [(TParam, Type)] -> IO (Maybe [(TParam, Type)]))
-> Maybe [(TParam, Type)] -> IO (Maybe [(TParam, Type)])
forall a b. (a -> b) -> a -> b
$
do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ([Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((Type -> [Type]) -> [Type] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
pSplitAnd (Subst -> [Type] -> [Type]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Type]
props)))
[Type]
tys <- (TVar -> Maybe Type) -> [TVar] -> Maybe [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Subst -> TVar -> Maybe Type
forall (m :: * -> *).
(Monad m, Alternative m) =>
Subst -> TVar -> m Type
bindParam Subst
su) [TVar]
params
[(TParam, Type)] -> Maybe [(TParam, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TParam] -> [Type] -> [(TParam, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TParam]
as [Type]
tys)
where
bindParam :: Subst -> TVar -> m Type
bindParam su :: Subst
su tp :: TVar
tp =
do let ty :: Type
ty = TVar -> Type
TVar TVar
tp
ty' :: Type
ty' = Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
ty
Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type
ty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
ty')
Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty'