    -- |
    -- 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
    _,Prop
    _])   -> [Prop] -> Solved
    SolvedIf []
            (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
    t1,Prop
    _])       -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pFin Prop
    t1 ]
            (TFun
    TCCeilMod, [Prop
    _,Prop
    _])        -> [Prop] -> Solved
    SolvedIf []
            (TFun
    TCLenFromThenTo,[Prop
    _,Prop
    _,Prop
    _]) -> [Prop] -> Solved
    SolvedIf []

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

        Prop
    _ -> Solved
    Unsolved