-- |
-- 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 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 ]

        -- fin (x * y)
        (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 []

        -- fin (x ^ y)
        (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

        -- fin (min x y)
        (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