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