```-- |
-- Module      :  Cryptol.TypeCheck.Solver.Numeric.Fin
-- Copyright   :  (c) 2015-2016 Galois, Inc.
-- 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
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

```