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