-- |
-- Module      :  Cryptol.TypeCheck.Solver.Class
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
--
-- Solving class constraints.

{-# LANGUAGE PatternGuards #-}
module Cryptol.TypeCheck.Solver.Class
  ( solveZeroInst
  , solveLogicInst
  , solveRingInst
  , solveFieldInst
  , solveIntegralInst
  , solveRoundInst
  , solveEqInst
  , solveCmpInst
  , solveSignedCmpInst
  , solveLiteralInst
  , solveFLiteralInst
  , solveValidFloat
  ) where

import qualified LibBF as FP

import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.SimpType (tAdd,tWidth)
import Cryptol.TypeCheck.Solver.Types
import Cryptol.Utils.RecordMap

{- | This places constraints on the floating point numbers that
we can work with.  This is a bit of an odd check, as it is really
a limitiation of the backend, and not the language itself.

On the other hand, it helps us give sane results if one accidentally
types a polymorphic float at the REPL.  Hopefully, most users will
stick to particular FP sizes, so this should be quite transparent.
-}
solveValidFloat :: Type -> Type -> Solved
solveValidFloat :: Type -> Type -> Solved
solveValidFloat Type
e Type
p
  | Just BFOpts
_ <- Type -> Type -> Maybe BFOpts
knownSupportedFloat Type
e Type
p = [Type] -> Solved
SolvedIf []
  | Bool
otherwise = Solved
Unsolved

-- | Check that the type parameters correspond to a float that
-- we support, and if so make the precision settings for the BigFloat library.
knownSupportedFloat :: Type -> Type -> Maybe FP.BFOpts
knownSupportedFloat :: Type -> Type -> Maybe BFOpts
knownSupportedFloat Type
et Type
pt
  | Just Integer
e <- Type -> Maybe Integer
tIsNum Type
et, Just Integer
p <- Type -> Maybe Integer
tIsNum Type
pt
  , Integer
minExp Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
e Bool -> Bool -> Bool
&& Integer
e Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
maxExp Bool -> Bool -> Bool
&& Integer
minPrec Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
p Bool -> Bool -> Bool
&& Integer
p Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
maxPrec =
    BFOpts -> Maybe BFOpts
forall a. a -> Maybe a
Just (Int -> BFOpts
FP.expBits (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
e) BFOpts -> BFOpts -> BFOpts
forall a. Semigroup a => a -> a -> a
<> Int -> BFOpts
FP.precBits (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
p)
                                     BFOpts -> BFOpts -> BFOpts
forall a. Semigroup a => a -> a -> a
<> BFOpts
FP.allowSubnormal)
  | Bool
otherwise = Maybe BFOpts
forall a. Maybe a
Nothing
  where
  minExp :: Integer
minExp  = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
2 (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
FP.expBitsMin)
  maxExp :: Integer
maxExp  = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
FP.expBitsMax

  minPrec :: Integer
minPrec = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
2 (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
FP.precBitsMin)
  maxPrec :: Integer
maxPrec = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
FP.precBitsMax




-- | Solve a Zero constraint by instance, if possible.
solveZeroInst :: Type -> Solved
solveZeroInst :: Type -> Solved
solveZeroInst Type
ty = case Type -> Type
tNoUser Type
ty of

  -- Zero Error -> fails
  TCon (TError {}) [Type]
_ -> Solved
Unsolvable

  -- Zero Bit
  TCon (TC TC
TCBit) [] -> [Type] -> Solved
SolvedIf []

  -- Zero Integer
  TCon (TC TC
TCInteger) [] -> [Type] -> Solved
SolvedIf []

  -- Zero (Z n)
  TCon (TC TC
TCIntMod) [Type
n] -> [Type] -> Solved
SolvedIf [ Type -> Type
pFin Type
n, Type
n Type -> Type -> Type
>== Type
tOne ]

  -- Zero Real

  -- Zero Rational
  TCon (TC TC
TCRational) [] -> [Type] -> Solved
SolvedIf []

  -- ValidVloat e p => Zero (Float e p)
  TCon (TC TC
TCFloat) [Type
e,Type
p] -> [Type] -> Solved
SolvedIf [ Type -> Type -> Type
pValidFloat Type
e Type
p ]

  -- Zero a => Zero [n]a
  TCon (TC TC
TCSeq) [Type
_, Type
a] -> [Type] -> Solved
SolvedIf [ Type -> Type
pZero Type
a ]

  -- Zero b => Zero (a -> b)
  TCon (TC TC
TCFun) [Type
_, Type
b] -> [Type] -> Solved
SolvedIf [ Type -> Type
pZero Type
b ]

  -- (Zero a, Zero b) => Zero (a,b)
  TCon (TC (TCTuple Int
_)) [Type]
es -> [Type] -> Solved
SolvedIf [ Type -> Type
pZero Type
e | Type
e <- [Type]
es ]

  -- (Zero a, Zero b) => Zero { x1 : a, x2 : b }
  TRec RecordMap Ident Type
fs -> [Type] -> Solved
SolvedIf [ Type -> Type
pZero Type
ety | Type
ety <- RecordMap Ident Type -> [Type]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs ]

  Type
_ -> Solved
Unsolved

-- | Solve a Logic constraint by instance, if possible.
solveLogicInst :: Type -> Solved
solveLogicInst :: Type -> Solved
solveLogicInst Type
ty = case Type -> Type
tNoUser Type
ty of

  -- Logic Error -> fails
  TCon (TError {}) [Type]
_ -> Solved
Unsolvable

  -- Logic Bit
  TCon (TC TC
TCBit) [] -> [Type] -> Solved
SolvedIf []

  -- Logic Integer fails
  TCon (TC TC
TCInteger) [] -> Solved
Unsolvable

  -- Logic (Z n) fails
  TCon (TC TC
TCIntMod) [Type
_] -> Solved
Unsolvable

  -- Logic Rational fails
  TCon (TC TC
TCRational) [] -> Solved
Unsolvable

  -- Logic (Float e p) fails
  TCon (TC TC
TCFloat) [Type
_, Type
_] -> Solved
Unsolvable

  -- Logic a => Logic [n]a
  TCon (TC TC
TCSeq) [Type
_, Type
a] -> [Type] -> Solved
SolvedIf [ Type -> Type
pLogic Type
a ]

  -- Logic b => Logic (a -> b)
  TCon (TC TC
TCFun) [Type
_, Type
b] -> [Type] -> Solved
SolvedIf [ Type -> Type
pLogic Type
b ]

  -- (Logic a, Logic b) => Logic (a,b)
  TCon (TC (TCTuple Int
_)) [Type]
es -> [Type] -> Solved
SolvedIf [ Type -> Type
pLogic Type
e | Type
e <- [Type]
es ]

  -- (Logic a, Logic b) => Logic { x1 : a, x2 : b }
  TRec RecordMap Ident Type
fs -> [Type] -> Solved
SolvedIf [ Type -> Type
pLogic Type
ety | Type
ety <- RecordMap Ident Type -> [Type]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs ]

  Type
_ -> Solved
Unsolved


-- | Solve a Ring constraint by instance, if possible.
solveRingInst :: Type -> Solved
solveRingInst :: Type -> Solved
solveRingInst Type
ty = case Type -> Type
tNoUser Type
ty of

  -- Ring Error -> fails
  TCon (TError {}) [Type]
_ -> Solved
Unsolvable

  -- Ring [n]e
  TCon (TC TC
TCSeq) [Type
n, Type
e] -> Type -> Type -> Solved
solveRingSeq Type
n Type
e

  -- Ring b => Ring (a -> b)
  TCon (TC TC
TCFun) [Type
_,Type
b] -> [Type] -> Solved
SolvedIf [ Type -> Type
pRing Type
b ]

  -- (Ring a, Ring b) => Arith (a,b)
  TCon (TC (TCTuple Int
_)) [Type]
es -> [Type] -> Solved
SolvedIf [ Type -> Type
pRing Type
e | Type
e <- [Type]
es ]

  -- Ring Bit fails
  TCon (TC TC
TCBit) [] -> Solved
Unsolvable

  -- Ring Integer
  TCon (TC TC
TCInteger) [] -> [Type] -> Solved
SolvedIf []

  -- Ring (Z n)
  TCon (TC TC
TCIntMod) [Type
n] -> [Type] -> Solved
SolvedIf [ Type -> Type
pFin Type
n, Type
n Type -> Type -> Type
>== Type
tOne ]

  -- Ring Rational
  TCon (TC TC
TCRational) [] -> [Type] -> Solved
SolvedIf []

  -- ValidFloat e p => Ring (Float e p)
  TCon (TC TC
TCFloat) [Type
e,Type
p] -> [Type] -> Solved
SolvedIf [ Type -> Type -> Type
pValidFloat Type
e Type
p ]

  -- (Ring a, Ring b) => Ring { x1 : a, x2 : b }
  TRec RecordMap Ident Type
fs -> [Type] -> Solved
SolvedIf [ Type -> Type
pRing Type
ety | Type
ety <- RecordMap Ident Type -> [Type]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs ]

  Type
_ -> Solved
Unsolved


-- | Solve a Ring constraint for a sequence.  The type passed here is the
-- element type of the sequence.
solveRingSeq :: Type -> Type -> Solved
solveRingSeq :: Type -> Type -> Solved
solveRingSeq Type
n Type
ty = case Type -> Type
tNoUser Type
ty of

  -- fin n => Ring [n]Bit
  TCon (TC TC
TCBit) [] -> [Type] -> Solved
SolvedIf [ Type -> Type
pFin Type
n ]

  -- variables are not solvable.
  TVar {} -> case Type -> Type
tNoUser Type
n of
                {- We are sure that the lenght is not `fin`, so the
                special case for `Bit` does not apply.
                Arith ty => Arith [n]ty -}
                TCon (TC TC
TCInf) [] -> [Type] -> Solved
SolvedIf [ Type -> Type
pRing Type
ty ]
                Type
_                  -> Solved
Unsolved

  -- Ring ty => Ring [n]ty
  Type
_ -> [Type] -> Solved
SolvedIf [ Type -> Type
pRing Type
ty ]


-- | Solve an Integral constraint by instance, if possible.
solveIntegralInst :: Type -> Solved
solveIntegralInst :: Type -> Solved
solveIntegralInst Type
ty = case Type -> Type
tNoUser Type
ty of

  -- Integral Error -> fails
  TCon (TError {}) [Type]
_ -> Solved
Unsolvable

  -- Integral Bit fails
  TCon (TC TC
TCBit) [] -> Solved
Unsolvable

  -- Integral Integer
  TCon (TC TC
TCInteger) [] -> [Type] -> Solved
SolvedIf []

  -- fin n => Integral [n]
  TCon (TC TC
TCSeq) [Type
n, Type
elTy] ->
    case Type -> Type
tNoUser Type
elTy of
      TCon (TC TC
TCBit) [] -> [Type] -> Solved
SolvedIf [ Type -> Type
pFin Type
n ]
      TVar TVar
_ -> Solved
Unsolved
      Type
_ -> Solved
Unsolvable

  TVar TVar
_ -> Solved
Unsolved

  Type
_ -> Solved
Unsolvable


-- | Solve a Field constraint by instance, if possible.
solveFieldInst :: Type -> Solved
solveFieldInst :: Type -> Solved
solveFieldInst Type
ty = case Type -> Type
tNoUser Type
ty of

  -- Field Error -> fails
  TCon (TError {}) [Type]
_ -> Solved
Unsolvable

  -- Field Bit fails
  TCon (TC TC
TCBit) [] -> Solved
Unsolvable

  -- Field Integer fails
  TCon (TC TC
TCInteger) [] -> Solved
Unsolvable

  -- Field Rational
  TCon (TC TC
TCRational) [] -> [Type] -> Solved
SolvedIf []

  -- ValidFloat e p => Field (Float e p)
  TCon (TC TC
TCFloat) [Type
e,Type
p] -> [Type] -> Solved
SolvedIf [ Type -> Type -> Type
pValidFloat Type
e Type
p ]

  -- Field Real

  -- Field (Z n)
  TCon (TC TC
TCIntMod) [Type
n] -> [Type] -> Solved
SolvedIf [ Type -> Type
pPrime Type
n ]

  -- Field ([n]a) fails
  TCon (TC TC
TCSeq) [Type
_, Type
_] -> Solved
Unsolvable

  -- Field (a -> b) fails
  TCon (TC TC
TCFun) [Type
_, Type
_] -> Solved
Unsolvable

  -- Field (a, b, ...) fails
  TCon (TC (TCTuple Int
_)) [Type]
_ -> Solved
Unsolvable

  -- Field {x : a, y : b, ...} fails
  TRec RecordMap Ident Type
_ -> Solved
Unsolvable

  Type
_ -> Solved
Unsolved


-- | Solve a Round constraint by instance, if possible.
solveRoundInst :: Type -> Solved
solveRoundInst :: Type -> Solved
solveRoundInst Type
ty = case Type -> Type
tNoUser Type
ty of

  -- Round Error -> fails
  TCon (TError {}) [Type]
_ -> Solved
Unsolvable

  -- Round Bit fails
  TCon (TC TC
TCBit) [] -> Solved
Unsolvable

  -- Round Integer fails
  TCon (TC TC
TCInteger) [] -> Solved
Unsolvable

  -- Round (Z n) fails
  TCon (TC TC
TCIntMod) [Type
_] -> Solved
Unsolvable

  -- Round Rational
  TCon (TC TC
TCRational) [] -> [Type] -> Solved
SolvedIf []

  -- ValidFloat e p => Round (Float e p)
  TCon (TC TC
TCFloat) [Type
e,Type
p] -> [Type] -> Solved
SolvedIf [ Type -> Type -> Type
pValidFloat Type
e Type
p ]

  -- Round Real

  -- Round ([n]a) fails
  TCon (TC TC
TCSeq) [Type
_, Type
_] -> Solved
Unsolvable

  -- Round (a -> b) fails
  TCon (TC TC
TCFun) [Type
_, Type
_] -> Solved
Unsolvable

  -- Round (a, b, ...) fails
  TCon (TC (TCTuple Int
_)) [Type]
_ -> Solved
Unsolvable

  -- Round {x : a, y : b, ...} fails
  TRec RecordMap Ident Type
_ -> Solved
Unsolvable

  Type
_ -> Solved
Unsolved



-- | Solve Eq constraints.
solveEqInst :: Type -> Solved
solveEqInst :: Type -> Solved
solveEqInst Type
ty = case Type -> Type
tNoUser Type
ty of

  -- Eq Error -> fails
  TCon (TError {}) [Type]
_ -> Solved
Unsolvable

  -- eq Bit
  TCon (TC TC
TCBit) [] -> [Type] -> Solved
SolvedIf []

  -- Eq Integer
  TCon (TC TC
TCInteger) [] -> [Type] -> Solved
SolvedIf []

  -- Eq Rational
  TCon (TC TC
TCRational) [] -> [Type] -> Solved
SolvedIf []

  -- ValidFloat e p => Eq (Float e p)
  TCon (TC TC
TCFloat) [Type
e,Type
p] -> [Type] -> Solved
SolvedIf [ Type -> Type -> Type
pValidFloat Type
e Type
p ]

  -- Eq (Z n)
  TCon (TC TC
TCIntMod) [Type
n] -> [Type] -> Solved
SolvedIf [ Type -> Type
pFin Type
n, Type
n Type -> Type -> Type
>== Type
tOne ]

  -- (fin n, Eq a) => Eq [n]a
  TCon (TC TC
TCSeq) [Type
n,Type
a] -> [Type] -> Solved
SolvedIf [ Type -> Type
pFin Type
n, Type -> Type
pEq Type
a ]

  -- (Eq a, Eq b) => Eq (a,b)
  TCon (TC (TCTuple Int
_)) [Type]
es -> [Type] -> Solved
SolvedIf ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
pEq [Type]
es)

  -- Eq (a -> b) fails
  TCon (TC TC
TCFun) [Type
_,Type
_] -> Solved
Unsolvable

  -- (Eq a, Eq b) => Eq { x:a, y:b }
  TRec RecordMap Ident Type
fs -> [Type] -> Solved
SolvedIf [ Type -> Type
pEq Type
e | Type
e <- RecordMap Ident Type -> [Type]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs ]

  Type
_ -> Solved
Unsolved


-- | Solve Cmp constraints.
solveCmpInst :: Type -> Solved
solveCmpInst :: Type -> Solved
solveCmpInst Type
ty = case Type -> Type
tNoUser Type
ty of

  -- Cmp Error -> fails
  TCon (TError {}) [Type]
_ -> Solved
Unsolvable

  -- Cmp Bit
  TCon (TC TC
TCBit) [] -> [Type] -> Solved
SolvedIf []

  -- Cmp Integer
  TCon (TC TC
TCInteger) [] -> [Type] -> Solved
SolvedIf []

  -- Cmp Rational
  TCon (TC TC
TCRational) [] -> [Type] -> Solved
SolvedIf []

  -- Cmp (Z n) fails
  TCon (TC TC
TCIntMod) [Type
_] -> Solved
Unsolvable

  -- ValidFloat e p => Cmp (Float e p)
  TCon (TC TC
TCFloat) [Type
e,Type
p] -> [Type] -> Solved
SolvedIf [ Type -> Type -> Type
pValidFloat Type
e Type
p ]

  -- (fin n, Cmp a) => Cmp [n]a
  TCon (TC TC
TCSeq) [Type
n,Type
a] -> [Type] -> Solved
SolvedIf [ Type -> Type
pFin Type
n, Type -> Type
pCmp Type
a ]

  -- (Cmp a, Cmp b) => Cmp (a,b)
  TCon (TC (TCTuple Int
_)) [Type]
es -> [Type] -> Solved
SolvedIf ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
pCmp [Type]
es)

  -- Cmp (a -> b) fails
  TCon (TC TC
TCFun) [Type
_,Type
_] -> Solved
Unsolvable

  -- (Cmp a, Cmp b) => Cmp { x:a, y:b }
  TRec RecordMap Ident Type
fs -> [Type] -> Solved
SolvedIf [ Type -> Type
pCmp Type
e | Type
e <- RecordMap Ident Type -> [Type]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs ]

  Type
_ -> Solved
Unsolved


-- | Solve a SignedCmp constraint for a sequence.  The type passed here is the
-- element type of the sequence.
solveSignedCmpSeq :: Type -> Type -> Solved
solveSignedCmpSeq :: Type -> Type -> Solved
solveSignedCmpSeq Type
n Type
ty = case Type -> Type
tNoUser Type
ty of

  -- (fin n, n >=1 ) => SignedCmp [n]Bit
  TCon (TC TC
TCBit) [] -> [Type] -> Solved
SolvedIf [ Type -> Type
pFin Type
n, Type
n Type -> Type -> Type
>== Integer -> Type
forall a. Integral a => a -> Type
tNum (Integer
1 :: Integer) ]

  -- variables are not solvable.
  TVar {} -> Solved
Unsolved

  -- (fin n, SignedCmp ty) => SignedCmp [n]ty, when ty != Bit
  Type
_ -> [Type] -> Solved
SolvedIf [ Type -> Type
pFin Type
n, Type -> Type
pSignedCmp Type
ty ]


-- | Solve SignedCmp constraints.
solveSignedCmpInst :: Type -> Solved
solveSignedCmpInst :: Type -> Solved
solveSignedCmpInst Type
ty = case Type -> Type
tNoUser Type
ty of

  -- SignedCmp Error -> fails
  TCon (TError {}) [Type]
_ -> Solved
Unsolvable

  -- SignedCmp Bit fails
  TCon (TC TC
TCBit) [] -> Solved
Unsolvable

  -- SignedCmp Integer fails
  TCon (TC TC
TCInteger) [] -> Solved
Unsolvable

  -- SignedCmp (Z n) fails
  TCon (TC TC
TCIntMod) [Type
_] -> Solved
Unsolvable

  -- SignedCmp Rational fails
  TCon (TC TC
TCRational) [] -> Solved
Unsolvable

  -- SignedCmp (Float e p) fails
  TCon (TC TC
TCFloat) [Type
_, Type
_] -> Solved
Unsolvable

  -- SignedCmp for sequences
  TCon (TC TC
TCSeq) [Type
n,Type
a] -> Type -> Type -> Solved
solveSignedCmpSeq Type
n Type
a

  -- (SignedCmp a, SignedCmp b) => SignedCmp (a,b)
  TCon (TC (TCTuple Int
_)) [Type]
es -> [Type] -> Solved
SolvedIf ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
pSignedCmp [Type]
es)

  -- SignedCmp (a -> b) fails
  TCon (TC TC
TCFun) [Type
_,Type
_] -> Solved
Unsolvable

  -- (SignedCmp a, SignedCmp b) => SignedCmp { x:a, y:b }
  TRec RecordMap Ident Type
fs -> [Type] -> Solved
SolvedIf [ Type -> Type
pSignedCmp Type
e | Type
e <- RecordMap Ident Type -> [Type]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs ]

  Type
_ -> Solved
Unsolved


-- | Solving fractional literal constraints.
solveFLiteralInst :: Type -> Type -> Type -> Type -> Solved
solveFLiteralInst :: Type -> Type -> Type -> Type -> Solved
solveFLiteralInst Type
numT Type
denT Type
rndT Type
ty
  | TCon (TError {}) [Type]
_ <- Type -> Type
tNoUser Type
numT = Solved
Unsolvable
  | TCon (TError {}) [Type]
_ <- Type -> Type
tNoUser Type
denT = Solved
Unsolvable
  | Type -> Bool
tIsInf Type
numT Bool -> Bool -> Bool
|| Type -> Bool
tIsInf Type
denT Bool -> Bool -> Bool
|| Type -> Bool
tIsInf Type
rndT = Solved
Unsolvable
  | Just Integer
0 <- Type -> Maybe Integer
tIsNum Type
denT = Solved
Unsolvable

  | Bool
otherwise =
    case Type -> Type
tNoUser Type
ty of
      TVar {} -> Solved
Unsolved

      TCon (TError {}) [Type]
_ -> Solved
Unsolvable

      TCon (TC TC
TCRational) [] ->
        [Type] -> Solved
SolvedIf [ Type -> Type
pFin Type
numT, Type -> Type
pFin Type
denT, Type
denT Type -> Type -> Type
>== Type
tOne ]

      TCon (TC TC
TCFloat) [Type
e,Type
p]
        | Just Integer
0    <- Type -> Maybe Integer
tIsNum Type
rndT ->
          [Type] -> Solved
SolvedIf [ Type -> Type -> Type
pValidFloat Type
e Type
p
                   , Type -> Type
pFin Type
numT, Type -> Type
pFin Type
denT, Type
denT Type -> Type -> Type
>== Type
tOne ]

        | Just Integer
_    <- Type -> Maybe Integer
tIsNum Type
rndT
        , Just BFOpts
opts <- Type -> Type -> Maybe BFOpts
knownSupportedFloat Type
e Type
p
        , Just Integer
n    <- Type -> Maybe Integer
tIsNum Type
numT
        , Just Integer
d    <- Type -> Maybe Integer
tIsNum Type
denT
         -> case BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
FP.bfDiv BFOpts
opts (Integer -> BigFloat
FP.bfFromInteger Integer
n) (Integer -> BigFloat
FP.bfFromInteger Integer
d) of
              (BigFloat
_, Status
FP.Ok) -> [Type] -> Solved
SolvedIf []
              (BigFloat, Status)
_ -> Solved
Unsolvable

        | Bool
otherwise -> Solved
Unsolved

      Type
_ -> Solved
Unsolvable

-- | Solve Literal constraints.
solveLiteralInst :: Type -> Type -> Solved
solveLiteralInst :: Type -> Type -> Solved
solveLiteralInst Type
val Type
ty
  | TCon (TError {}) [Type]
_ <- Type -> Type
tNoUser Type
val = Solved
Unsolvable
  | Bool
otherwise =
    case Type -> Type
tNoUser Type
ty of

      -- Literal n Error -> fails
      TCon (TError {}) [Type]
_ -> Solved
Unsolvable

      -- (1 >= val) => Literal val Bit
      TCon (TC TC
TCBit) [] -> [Type] -> Solved
SolvedIf [ Type
tOne Type -> Type -> Type
>== Type
val ]

      -- (fin val) => Literal val Integer
      TCon (TC TC
TCInteger) [] -> [Type] -> Solved
SolvedIf [ Type -> Type
pFin Type
val ]

      -- (fin val) => Literal val Rational
      TCon (TC TC
TCRational) [] -> [Type] -> Solved
SolvedIf [ Type -> Type
pFin Type
val ]

      -- ValidFloat e p => Literal val (Float e p)   if `val` is representable
      TCon (TC TC
TCFloat) [Type
e,Type
p]
        | Just Integer
n    <- Type -> Maybe Integer
tIsNum Type
val
        , Just BFOpts
opts <- Type -> Type -> Maybe BFOpts
knownSupportedFloat Type
e Type
p ->
          let bf :: BigFloat
bf = Integer -> BigFloat
FP.bfFromInteger Integer
n
          in case BFOpts -> BigFloat -> (BigFloat, Status)
FP.bfRoundFloat BFOpts
opts BigFloat
bf of
               (BigFloat
bf1,Status
FP.Ok) | BigFloat
bf BigFloat -> BigFloat -> Bool
forall a. Eq a => a -> a -> Bool
== BigFloat
bf1 -> [Type] -> Solved
SolvedIf []
               (BigFloat, Status)
_ -> Solved
Unsolvable

        | Bool
otherwise -> Solved
Unsolved



      -- (fin val, fin m, m >= val + 1) => Literal val (Z m)
      TCon (TC TC
TCIntMod) [Type
modulus] ->
        [Type] -> Solved
SolvedIf [ Type -> Type
pFin Type
val, Type -> Type
pFin Type
modulus, Type
modulus Type -> Type -> Type
>== Type -> Type -> Type
tAdd Type
val Type
tOne ]

      -- (fin bits, bits => width n) => Literal n [bits]
      TCon (TC TC
TCSeq) [Type
bits, Type
elTy]
        | TCon (TC TC
TCBit) [] <- Type
ety ->
            [Type] -> Solved
SolvedIf [ Type -> Type
pFin Type
val, Type -> Type
pFin Type
bits, Type
bits Type -> Type -> Type
>== Type -> Type
tWidth Type
val ]
        | TVar TVar
_ <- Type
ety -> Solved
Unsolved
        where ety :: Type
ety = Type -> Type
tNoUser Type
elTy

      TVar TVar
_ -> Solved
Unsolved

      Type
_ -> Solved
Unsolvable