module Cryptol.TypeCheck.Solver.Numeric
( numericStep
, simpFin
, goalOrderModel
) where
import Cryptol.Utils.Panic(panic)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Unify(mgu,Result(..))
import Cryptol.TypeCheck.Subst(fvs)
import Cryptol.TypeCheck.InferTypes(Goal(..), Solved(..))
import Cryptol.TypeCheck.Solver.FinOrd(OrdFacts, AssertResult(..),addFact)
import Cryptol.TypeCheck.Solver.Interval(Interval(..),iDisjoint)
import Cryptol.TypeCheck.Solver.Eval(typeInterval,simpType,
typeKnownFin,typeKnownLeq,
assumedOrderModel,
derivedOrd
)
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
import Cryptol.TypeCheck.Solver.Utils
import Control.Monad(guard,msum)
import qualified Data.Set as Set
numericStep :: OrdFacts -> Goal -> Solved
numericStep m g =
case tNoUser (simpType m (goal g)) of
TCon (PC PEqual) [t1,t2]
| OK (su,[]) <- unifier -> solvedS (Just su) []
| Error _ <- unifier -> Unsolvable
where unifier = mgu t1 t2
TCon (PC PEqual) [t1,t2]
| Just prop <- checkOnlyInf m t1 t2 -> solved [prop]
| Just (k1,t1') <- splitConstSummand t1
, Just (k2,t2') <- splitConstSummand t2 ->
let sub = case compare k1 k2 of
EQ -> t1' =#= t2'
LT -> t1' =#= (tNum (k2 k1) .+. t2')
GT -> (tNum (k1 k2) .+. t1') =#= t2'
in solved [sub]
| Just p <- eqByCancel m t1 t2 -> solved [p]
| Just (k1,t1') <- splitConstFactor t1
, Just (k2,t2') <- splitConstFactor t2
, let c = gcd k1 k2
, c > 1 -> solved [ tNum (div k1 c) .*. t1' =#= tNum (div k2 c) .*. t2' ]
| TCon (TF TCMin) [a,b] <- t1
, Just ps <- simpEqMin m t2 a b -> solved ps
| TCon (TF TCMin) [a,b] <- t2
, Just ps <- simpEqMin m t1 a b -> solved ps
| TVar a <- tNoUser t1
, Just ps <- aIsMin m a (splitMins t2) -> solved ps
| TVar a <- tNoUser t2
, Just ps <- aIsMin m a (splitMins t1) -> solved ps
| Just ps <- eqBySub m t1 t2 -> solved ps
| iDisjoint i1 i2 -> Unsolvable
where i1 = typeInterval m t1
i2 = typeInterval m t2
TCon (PC PGeq) [t1,t2]
| typeKnownLeq m t2 t1 -> solved []
| otherwise -> Unsolved
prop | Just ps <- simpFin m prop -> solved ps
_ -> Unsolved
where
solved = solvedS Nothing
solvedS su xs = Solved su [ g { goal = x } | x <- xs ]
simpEqMin :: OrdFacts -> Type -> Type -> Type -> Maybe [Prop]
simpEqMin m t1 t2 t3
| t1 == t2 = Just [ t3 >== t1 ]
| t1 == t3 = Just [ t2 >== t1 ]
| knownSmaller m t1 t2 = Just [ t1 =#= t3 ]
| knownSmaller m t1 t3 = Just [ t1 =#= t2 ]
| otherwise = Nothing
knownSmaller :: OrdFacts -> Type -> Type -> Bool
knownSmaller m t1 t2
| Just (_,t2') <- splitConstSummand t2
, isFinite (typeInterval m t1)
, t1 == t2' = True
knownSmaller _ _ _ = False
simpFin :: OrdFacts -> Prop -> Maybe [Prop]
simpFin m prop =
case tNoUser prop of
TCon (PC PFin) [ty] -> simpFinTy m ty
_ -> Nothing
simpFinTy :: OrdFacts -> Type -> Maybe [Prop]
simpFinTy _ ty | TCon (TC (TCNum _)) _ <- tNoUser ty = Just []
simpFinTy m ty | typeKnownFin m ty = Just []
simpFinTy m ty =
case tNoUser ty of
TCon (TF tf) [t1]
| TCLg2 <- tf -> Just [pFin t1]
| TCWidth <- tf -> Just [pFin t1]
TCon (TF tf) [t1,t2]
| TCAdd <- tf -> Just [pFin t1, pFin t2]
| TCSub <- tf -> Just [pFin t1]
| TCMul <- tf
, Nat n1 <- lowerBound i1, n1 >= 1
, Nat n2 <- lowerBound i2, n2 >= 1
-> Just [pFin t1, pFin t2]
| TCDiv <- tf -> Just [pFin t1]
| TCMod <- tf -> Just []
| TCExp <- tf -> Just [pFin t1, pFin t2]
| TCMin <- tf -> Nothing
| TCMax <- tf -> Just [pFin t1, pFin t2]
where i1 = typeInterval m t1
i2 = typeInterval m t2
TCon (TF tf) [_,_,_]
| TCLenFromThen <- tf -> Just []
| TCLenFromThenTo <- tf -> Just []
_ -> Nothing
checkOnlyInf :: OrdFacts -> Type -> Type -> Maybe Prop
checkOnlyInf ordM t1 t2 =
case (tNoUser t1, tNoUser t2) of
(TCon (TC TCInf) _, ty) -> checkInf ty
(ty, TCon (TC TCInf) _) -> checkInf ty
(TVar x, ty) -> checkVar x ty
(ty, TVar x) -> checkVar x ty
(_,_) -> Nothing
where
checkVar a ty =
do ty1 <- splitVarSummand a ty
guard (validP 1 ty1)
return (TVar a =#= tInf)
validP lb p = let i = typeInterval ordM p
in isFinite i && lowerBound i >= Nat lb
checkInf ty = case ty of
TCon (TF TCAdd) [l,r]
| validP 0 l -> Just (r =#= tInf)
| validP 0 r -> Just (l =#= tInf)
TCon (TF TCMul) [l,r]
| validP 1 l -> Just (r =#= tInf)
| validP 1 r -> Just (l =#= tInf)
_ -> Nothing
eqBySub :: OrdFacts -> Type -> Type -> Maybe [Prop]
eqBySub ordM t1 t2 = msum $ zipWith attempt (splitVarSummands t1) (repeat t2) ++
zipWith attempt (splitVarSummands t2) (repeat t1)
where
attempt (x,s) t
| not (x `Set.member` fvs (s,t)) && typeKnownFin ordM s =
Just [ TVar x =#= (t .-. s), t >== s ]
| otherwise = Nothing
eqByCancel :: OrdFacts -> Type -> Type -> Maybe Prop
eqByCancel ordM t1 t2 =
msum [ check x | x <- Set.toList (fvs t1), typeKnownFin ordM (TVar x) ]
where
check x = do t1' <- splitVarSummand x t1
t2' <- splitVarSummand x t2
return (t1' =#= t2')
aIsMin :: OrdFacts -> TVar -> [Type] -> Maybe [Prop]
aIsMin _ _ [] = Nothing
aIsMin _ _ [_] = Nothing
aIsMin m a ts0 = attempt [] ts0
where
tMins [] = panic "Cryptol.TypeCheck.Solver.Numeric" [ "tMins []" ]
tMins [t] = t
tMins ts = foldr1 tMin ts
attempt _ [] = Nothing
attempt others (t:ts)
| isAparat m a t = Just [ TVar a =#= tMins (ts ++ others) ]
| otherwise = attempt (t:others) ts
isAparat :: OrdFacts -> TVar -> Type -> Bool
isAparat m x ty = case splitVarSummand x ty of
Just t1 -> typeKnownLeq m (tNum (1::Int)) t1
_ -> False
goalOrderModel :: OrdFacts -> [Goal] -> (OrdFacts, [Goal], [Goal])
goalOrderModel m0 todo =
go m0 [] [] False [ g { goal = simpType m0 (goal g) } | g <- todo ]
where
go m bad others changes []
| changes = let (m1,newBad,newOthers) = goalOrderModel m others
in (m1, newBad ++ bad, newOthers)
| otherwise = case concatMap (derivedOrd m) (map goal others) of
[] -> (m,bad,others)
der -> case assumedOrderModel m der of
Left _err -> (m,bad,others)
Right (m1,_) -> (m1,bad,others)
go m bad others changes (g : gs)
| Just ps <- simpFin m (goal g) =
go m bad others changes ([ g { goal = p } | p <- ps ] ++ gs)
go m bad others changes (g : gs) =
case addFact g m of
OrdAlreadyKnown -> go m bad others changes gs
OrdAdded m1 -> go m1 bad others True gs
OrdCannot -> go m bad (g : others) changes gs
OrdImprove t1 t2 -> go m bad (g { goal = t1 =#= t2 } : others) changes gs
OrdImpossible -> go m (g : bad) others changes gs