{-# LANGUAGE PatternGuards #-}
module Cryptol.TypeCheck.Solver.Numeric.Fin where
import Data.Map (Map)
import qualified Data.Map as Map
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.Solver.Numeric.Interval
import Cryptol.TypeCheck.Solver.InfNat
cryIsFin :: Map TVar Interval -> Prop -> Solved
cryIsFin :: Map TVar Interval -> Prop -> Solved
cryIsFin varInfo :: Map TVar Interval
varInfo p :: Prop
p =
case Prop -> Maybe Prop
pIsFin Prop
p of
Just ty :: Prop
ty -> Map TVar Interval -> Prop -> Solved
cryIsFinType Map TVar Interval
varInfo Prop
ty
Nothing -> Solved
Unsolved
cryIsFinType :: Map TVar Interval -> Type -> Solved
cryIsFinType :: Map TVar Interval -> Prop -> Solved
cryIsFinType varInfo :: Map TVar Interval
varInfo ty :: Prop
ty =
case Prop -> Prop
tNoUser Prop
ty of
TVar x :: TVar
x | Just i :: Interval
i <- TVar -> Map TVar Interval -> Maybe Interval
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TVar
x Map TVar Interval
varInfo
, Interval -> Bool
iIsFin Interval
i -> [Prop] -> Solved
SolvedIf []
TCon (TC tc :: TC
tc) []
| TCNum _ <- TC
tc -> [Prop] -> Solved
SolvedIf []
| TC
TCInf <- TC
tc ->
TCErrorMessage -> Solved
Unsolvable (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "Expected a finite type, but found `inf`."
TCon (TF f :: TFun
f) ts :: [Prop]
ts ->
case (TFun
f,[Prop]
ts) of
(TCAdd,[t1 :: Prop
t1,t2 :: Prop
t2]) -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1, Prop -> Prop
pFin Prop
t2 ]
(TCSub,[t1 :: Prop
t1,_ ]) -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1 ]
(TCMul,[t1 :: Prop
t1,t2 :: Prop
t2])
| Interval -> Nat'
iLower Interval
i1 Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Nat'
Nat 1 Bool -> Bool -> Bool
&& Interval -> Bool
iIsFin Interval
i1 -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t2 ]
| Interval -> Nat'
iLower Interval
i2 Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Nat'
Nat 1 Bool -> Bool -> Bool
&& Interval -> Bool
iIsFin Interval
i2 -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1 ]
| Interval -> Nat'
iLower Interval
i1 Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Nat'
Nat 1 Bool -> Bool -> Bool
&&
Interval -> Nat'
iLower Interval
i2 Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Nat'
Nat 1 -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1, Prop -> Prop
pFin Prop
t2 ]
| Interval -> Bool
iIsFin Interval
i1 Bool -> Bool -> Bool
&& Interval -> Bool
iIsFin Interval
i2 -> [Prop] -> Solved
SolvedIf []
where
i1 :: Interval
i1 = Map TVar Interval -> Prop -> Interval
typeInterval Map TVar Interval
varInfo Prop
t1
i2 :: Interval
i2 = Map TVar Interval -> Prop -> Interval
typeInterval Map TVar Interval
varInfo Prop
t2
(TCDiv, [t1 :: Prop
t1,_]) -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1 ]
(TCMod, [_,_]) -> [Prop] -> Solved
SolvedIf []
(TCExp, [t1 :: Prop
t1,t2 :: Prop
t2])
| Interval -> Nat'
iLower Interval
i1 Nat' -> Nat' -> Bool
forall a. Eq a => a -> a -> Bool
== Nat'
Inf -> [Prop] -> Solved
SolvedIf [ Prop
t2 Prop -> Prop -> Prop
=#= Prop
tZero ]
| Interval -> Nat'
iLower Interval
i2 Nat' -> Nat' -> Bool
forall a. Eq a => a -> a -> Bool
== Nat'
Inf -> [Prop] -> Solved
SolvedIf [ Prop
tOne Prop -> Prop -> Prop
>== Prop
t1 ]
| Interval -> Nat'
iLower Interval
i1 Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Nat'
Nat 2 -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1, Prop -> Prop
pFin Prop
t2 ]
| Interval -> Nat'
iLower Interval
i2 Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Nat'
Nat 1 -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1, Prop -> Prop
pFin Prop
t2 ]
| Just x :: Nat'
x <- Interval -> Maybe Nat'
iUpper Interval
i1, Nat'
x Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer -> Nat'
Nat 1 -> [Prop] -> Solved
SolvedIf []
| Just (Nat 0) <- Interval -> Maybe Nat'
iUpper Interval
i2 -> [Prop] -> Solved
SolvedIf []
where
i1 :: Interval
i1 = Map TVar Interval -> Prop -> Interval
typeInterval Map TVar Interval
varInfo Prop
t1
i2 :: Interval
i2 = Map TVar Interval -> Prop -> Interval
typeInterval Map TVar Interval
varInfo Prop
t2
(TCMin, [t1 :: Prop
t1,t2 :: Prop
t2])
| Interval -> Bool
iIsFin Interval
i1 -> [Prop] -> Solved
SolvedIf []
| Interval -> Bool
iIsFin Interval
i2 -> [Prop] -> Solved
SolvedIf []
| Just x :: Nat'
x <- Interval -> Maybe Nat'
iUpper Interval
i1, Nat'
x Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
<= Interval -> Nat'
iLower Interval
i2 -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1 ]
| Just x :: Nat'
x <- Interval -> Maybe Nat'
iUpper Interval
i2, Nat'
x Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
<= Interval -> Nat'
iLower Interval
i1 -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t2 ]
where
i1 :: Interval
i1 = Map TVar Interval -> Prop -> Interval
typeInterval Map TVar Interval
varInfo Prop
t1
i2 :: Interval
i2 = Map TVar Interval -> Prop -> Interval
typeInterval Map TVar Interval
varInfo Prop
t2
(TCMax, [t1 :: Prop
t1,t2 :: Prop
t2]) -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1, Prop -> Prop
pFin Prop
t2 ]
(TCWidth, [t1 :: Prop
t1]) -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1 ]
(TCCeilDiv, [_,_]) -> [Prop] -> Solved
SolvedIf []
(TCCeilMod, [_,_]) -> [Prop] -> Solved
SolvedIf []
(TCLenFromThenTo,[_,_,_]) -> [Prop] -> Solved
SolvedIf []
_ -> Solved
Unsolved
_ -> Solved
Unsolved