-- |
-- Module      :  Cryptol.TypeCheck.Solver.Numeric.Fin
-- Copyright   :  (c) 2015-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
--
-- Simplification of `fin` constraints.

{-# LANGUAGE PatternGuards #-}
module Cryptol.TypeCheck.Solver.Numeric.Fin where

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 :: Ctxt -> Prop -> Solved
cryIsFin :: Ctxt -> Prop -> Solved
cryIsFin Ctxt
ctxt Prop
p =
  case Prop -> Maybe Prop
pIsFin Prop
p of
    Just Prop
ty -> Ctxt -> Prop -> Solved
cryIsFinType Ctxt
ctxt Prop
ty
    Maybe Prop
Nothing -> Solved
Unsolved

cryIsFinType :: Ctxt -> Type -> Solved
cryIsFinType :: Ctxt -> Prop -> Solved
cryIsFinType Ctxt
ctxt Prop
ty =
  let varInfo :: Map TVar Interval
varInfo = Ctxt -> Map TVar Interval
intervals Ctxt
ctxt in
  case Prop -> Prop
tNoUser Prop
ty of

    TVar TVar
x | Just 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) []
      | TCNum Integer
_ <- TC
tc -> [Prop] -> Solved
SolvedIf []
      | TC
TCInf   <- TC
tc -> Solved
Unsolvable

    TCon (TF TFun
f) [Prop]
ts ->
      case (TFun
f,[Prop]
ts) of
        (TFun
TCAdd,[Prop
t1,Prop
t2]) -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1, Prop -> Prop
pFin Prop
t2 ]
        (TFun
TCSub,[Prop
t1,Prop
_ ]) -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1 ]

        -- fin (x * y)
        (TFun
TCMul,[Prop
t1,Prop
t2])
          | Interval -> Nat'
iLower Interval
i1 Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Nat'
Nat Integer
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 Integer
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 Integer
1 Bool -> Bool -> Bool
&&
            Interval -> Nat'
iLower Interval
i2 Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Nat'
Nat Integer
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


        (TFun
TCDiv, [Prop
t1,Prop
_])  -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1 ]
        (TFun
TCMod, [Prop
_,Prop
_])   -> [Prop] -> Solved
SolvedIf []

        -- fin (x ^ y)
        (TFun
TCExp, [Prop
t1,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 Integer
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 Integer
1 -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1, Prop -> Prop
pFin Prop
t2 ]

          | Just Nat'
x <- Interval -> Maybe Nat'
iUpper Interval
i1, Nat'
x Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer -> Nat'
Nat Integer
1 -> [Prop] -> Solved
SolvedIf []
          | Just (Nat Integer
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

        -- fin (min x y)
        (TFun
TCMin, [Prop
t1,Prop
t2])
          | Interval -> Bool
iIsFin Interval
i1  -> [Prop] -> Solved
SolvedIf []
          | Interval -> Bool
iIsFin Interval
i2  -> [Prop] -> Solved
SolvedIf []
          | Just 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 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

        (TFun
TCMax, [Prop
t1,Prop
t2])          -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1, Prop -> Prop
pFin Prop
t2 ]
        (TFun
TCWidth, [Prop
t1])           -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
t1 ]
        (TFun
TCCeilDiv, [Prop
_,Prop
_])        -> [Prop] -> Solved
SolvedIf []
        (TFun
TCCeilMod, [Prop
_,Prop
_])        -> [Prop] -> Solved
SolvedIf []
        (TFun
TCLenFromThenTo,[Prop
_,Prop
_,Prop
_]) -> [Prop] -> Solved
SolvedIf []

        (TFun, [Prop])
_ -> Solved
Unsolved

    Prop
_ -> Solved
Unsolved