{-# LANGUAGE PatternGuards #-}
module Cryptol.TypeCheck.SimpType where

import Control.Applicative((<|>))
import Cryptol.TypeCheck.Type hiding
  (tSub,tMul,tDiv,tMod,tExp,tMin,tCeilDiv,tCeilMod,tLenFromThenTo)
import Cryptol.TypeCheck.TypePat
import Cryptol.TypeCheck.Solver.InfNat
import Control.Monad(msum,guard)
import Cryptol.TypeCheck.PP(pp)


tRebuild' :: Bool -> Type -> Type
tRebuild' :: Bool -> Type -> Type
tRebuild' withUser :: Bool
withUser = Type -> Type
go
  where
  go :: Type -> Type
go ty :: Type
ty =
    case Type
ty of
      TUser x :: Name
x xs :: [Type]
xs t :: Type
t
        | Bool
withUser  -> Name -> [Type] -> Type -> Type
TUser Name
x [Type]
xs (Type -> Type
go Type
t)
        | Bool
otherwise -> Type -> Type
go Type
t
      TVar _        -> Type
ty
      TRec xs :: [(Ident, Type)]
xs       -> [(Ident, Type)] -> Type
TRec [ (Ident
x, Type -> Type
go Type
y) | (x :: Ident
x, y :: Type
y) <- [(Ident, Type)]
xs ]
      TCon tc :: TCon
tc ts :: [Type]
ts    -> TCon -> [Type] -> Type
tCon TCon
tc ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
go [Type]
ts)

tRebuild :: Type -> Type
tRebuild :: Type -> Type
tRebuild = Bool -> Type -> Type
tRebuild' Bool
True

tCon :: TCon -> [Type] -> Type
tCon :: TCon -> [Type] -> Type
tCon tc :: TCon
tc ts :: [Type]
ts =
  case TCon
tc of
    TF f :: TFun
f ->
      case (TFun
f, [Type]
ts) of
        (TCAdd, [x :: Type
x, y :: Type
y]) -> Type -> Type -> Type
tAdd Type
x Type
y
        (TCSub, [x :: Type
x, y :: Type
y]) -> Type -> Type -> Type
tSub Type
x Type
y
        (TCMul, [x :: Type
x, y :: Type
y]) -> Type -> Type -> Type
tMul Type
x Type
y
        (TCExp, [x :: Type
x, y :: Type
y]) -> Type -> Type -> Type
tExp Type
x Type
y
        (TCDiv, [x :: Type
x, y :: Type
y]) -> Type -> Type -> Type
tDiv Type
x Type
y
        (TCMod, [x :: Type
x, y :: Type
y]) -> Type -> Type -> Type
tMod Type
x Type
y
        (TCMin, [x :: Type
x, y :: Type
y]) -> Type -> Type -> Type
tMin Type
x Type
y
        (TCMax, [x :: Type
x, y :: Type
y]) -> Type -> Type -> Type
tMax Type
x Type
y
        (TCWidth, [x :: Type
x]) -> Type -> Type
tWidth Type
x
        (TCCeilDiv, [x :: Type
x, y :: Type
y]) -> Type -> Type -> Type
tCeilDiv Type
x Type
y
        (TCCeilMod, [x :: Type
x, y :: Type
y]) -> Type -> Type -> Type
tCeilMod Type
x Type
y
        (TCLenFromThenTo, [x :: Type
x, y :: Type
y, z :: Type
z]) -> Type -> Type -> Type -> Type
tLenFromThenTo Type
x Type
y Type
z
        _ -> TCon -> [Type] -> Type
TCon TCon
tc [Type]
ts
    _ -> TCon -> [Type] -> Type
TCon TCon
tc [Type]
ts

-- Normal: constants to the left
tAdd :: Type -> Type -> Type
tAdd :: Type -> Type -> Type
tAdd x :: Type
x y :: Type
y
  | Just t :: Type
t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp TFun
TCAdd (([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
total ((Nat' -> Nat' -> Nat') -> [Nat'] -> Nat'
forall a b. (a -> a -> b) -> [a] -> b
op2 Nat' -> Nat' -> Nat'
nAdd)) [Type
x,Type
y] = Type
t
  | Type -> Bool
tIsInf Type
x            = Type
tInf
  | Type -> Bool
tIsInf Type
y            = Type
tInf
  | Just n :: Integer
n <- Type -> Maybe Integer
tIsNum Type
x  = Integer -> Type -> Type
addK Integer
n Type
y
  | Just n :: Integer
n <- Type -> Maybe Integer
tIsNum Type
y  = Integer -> Type -> Type
addK Integer
n Type
x
  | Just (n :: Integer
n,x1 :: Type
x1) <- Type -> Maybe (Integer, Type)
isSumK Type
x = Integer -> Type -> Type
addK Integer
n (Type -> Type -> Type
tAdd Type
x1 Type
y)
  | Just (n :: Integer
n,y1 :: Type
y1) <- Type -> Maybe (Integer, Type)
isSumK Type
y = Integer -> Type -> Type
addK Integer
n (Type -> Type -> Type
tAdd Type
x Type
y1)
  | Just v :: Type
v <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe (do (a :: Type
a,b :: Type
b) <- Pat Type (Type, Type)
(|-|) Type
y
                             Bool -> Match ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type
x Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
b)
                             Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
a) = Type
v
  | Just v :: Type
v <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe (do (a :: Type
a,b :: Type
b) <- Pat Type (Type, Type)
(|-|) Type
x
                             Bool -> Match ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type
b Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
y)
                             Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
a) = Type
v

  | Just v :: Type
v <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe (Match Type
factor Match Type -> Match Type -> Match Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Match Type
same Match Type -> Match Type -> Match Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Match Type
swapVars) = Type
v

  | Bool
otherwise           = TFun -> Type -> Type -> Type
tf2 TFun
TCAdd Type
x Type
y
  where
  isSumK :: Type -> Maybe (Integer, Type)
isSumK t :: Type
t = case Type -> Type
tNoUser Type
t of
               TCon (TF TCAdd) [ l :: Type
l, r :: Type
r ] ->
                 do Integer
n <- Type -> Maybe Integer
tIsNum Type
l
                    (Integer, Type) -> Maybe (Integer, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
n, Type
r)
               _ -> Maybe (Integer, Type)
forall a. Maybe a
Nothing

  addK :: Integer -> Type -> Type
addK 0 t :: Type
t = Type
t
  addK n :: Integer
n t :: Type
t | Just (m :: Integer
m,b :: Type
b) <- Type -> Maybe (Integer, Type)
isSumK Type
t = TFun -> Type -> Type -> Type
tf2 TFun
TCAdd (Integer -> Type
forall a. Integral a => a -> Type
tNum (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m)) Type
b
           | Just v :: Type
v <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe
                     (Match Type -> Maybe Type) -> Match Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ do (a :: Type
a,b :: Type
b) <- Pat Type (Type, Type)
(|-|) Type
t
                          (do Integer
m <- Pat Type Integer
aNat Type
b
                              Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Match Type) -> Type -> Match Type
forall a b. (a -> b) -> a -> b
$ case Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
n Integer
m of
                                         GT -> Type -> Type -> Type
tAdd (Integer -> Type
forall a. Integral a => a -> Type
tNum (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
m)) Type
a
                                         EQ -> Type
a
                                         LT -> Type -> Type -> Type
tSub Type
a (Integer -> Type
forall a. Integral a => a -> Type
tNum (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
n)))
                            Match Type -> Match Type -> Match Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                            (do Integer
m <- Pat Type Integer
aNat Type
a
                                Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
tSub (Integer -> Type
forall a. Integral a => a -> Type
tNum (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
n)) Type
b))
                      = Type
v
           -- K + min a b ~> min (K + a) (K + b)
           | Just v :: Type
v <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe
                    (Match Type -> Maybe Type) -> Match Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ do (a :: Type
a,b :: Type
b) <- Pat Type (Type, Type)
aMin Type
t
                         Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Match Type) -> Type -> Match Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
tMin (Type -> Type -> Type
tAdd (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
n) Type
a) (Type -> Type -> Type
tAdd (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
n) Type
b)
              = Type
v

           | Bool
otherwise              = TFun -> Type -> Type -> Type
tf2 TFun
TCAdd (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
n) Type
t

  factor :: Match Type
factor = do (a :: Type
a,b1 :: Type
b1)  <- Pat Type (Type, Type)
aMul Type
x
              (a' :: Type
a',b2 :: Type
b2) <- Pat Type (Type, Type)
aMul Type
y
              Bool -> Match ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type
a Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
a')
              Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
tMul Type
a (Type -> Type -> Type
tAdd Type
b1 Type
b2))

  same :: Match Type
same = do Bool -> Match ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type
x Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
y)
            Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
tMul (Int -> Type
forall a. Integral a => a -> Type
tNum (2 :: Int)) Type
x)

  swapVars :: Match Type
swapVars = do TVar
a <- Pat Type TVar
aTVar Type
x
                TVar
b <- Pat Type TVar
aTVar Type
y
                Bool -> Match ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TVar
b TVar -> TVar -> Bool
forall a. Ord a => a -> a -> Bool
< TVar
a)
                Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return (TFun -> Type -> Type -> Type
tf2 TFun
TCAdd Type
y Type
x)

tSub :: Type -> Type -> Type
tSub :: Type -> Type -> Type
tSub x :: Type
x y :: Type
y
  | Just t :: Type
t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp TFun
TCSub ((Nat' -> Nat' -> Maybe Nat') -> [Nat'] -> Maybe Nat'
forall a b. (a -> a -> b) -> [a] -> b
op2 Nat' -> Nat' -> Maybe Nat'
nSub) [Type
x,Type
y] = Type
t
  | Type -> Bool
tIsInf Type
y  = TCErrorMessage -> Type
tBadNumber (TCErrorMessage -> Type) -> TCErrorMessage -> Type
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "Subtraction of `inf`."
  | Just 0 <- Maybe Integer
yNum = Type
x
  | Just k :: Integer
k <- Maybe Integer
yNum
  , TCon (TF TCAdd) [a :: Type
a,b :: Type
b] <- Type -> Type
tNoUser Type
x
  , Just n :: Integer
n <- Type -> Maybe Integer
tIsNum Type
a = case Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
k Integer
n of
                           EQ -> Type
b
                           LT -> TFun -> Type -> Type -> Type
tf2 TFun
TCAdd (Integer -> Type
forall a. Integral a => a -> Type
tNum (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
k)) Type
b
                           GT -> Type -> Type -> Type
tSub Type
b (Integer -> Type
forall a. Integral a => a -> Type
tNum (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
n))

  | Just v :: Type
v <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe (do (a :: Type
a,b :: Type
b) <- Pat Type (Type, Type)
anAdd Type
x
                             (Bool -> Match ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type
a Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
y) Match () -> Match Type -> Match Type
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
b)
                                Match Type -> Match Type -> Match Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Bool -> Match ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type
b Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
y) Match () -> Match Type -> Match Type
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
a))
                       = Type
v

  | Just v :: Type
v <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe (do (a :: Type
a,b :: Type
b) <- Pat Type (Type, Type)
(|-|) Type
y
                             Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
tSub (Type -> Type -> Type
tAdd Type
x Type
b) Type
a)) = Type
v

  | Bool
otherwise = TFun -> Type -> Type -> Type
tf2 TFun
TCSub Type
x Type
y
  where
  yNum :: Maybe Integer
yNum = Type -> Maybe Integer
tIsNum Type
y



-- Normal: constants to the left
tMul :: Type -> Type -> Type
tMul :: Type -> Type -> Type
tMul x :: Type
x y :: Type
y
  | Just t :: Type
t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp TFun
TCMul (([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
total ((Nat' -> Nat' -> Nat') -> [Nat'] -> Nat'
forall a b. (a -> a -> b) -> [a] -> b
op2 Nat' -> Nat' -> Nat'
nMul)) [Type
x,Type
y] = Type
t
  | Just n :: Integer
n <- Type -> Maybe Integer
tIsNum Type
x  = Integer -> Type -> Type
mulK Integer
n Type
y
  | Just n :: Integer
n <- Type -> Maybe Integer
tIsNum Type
y  = Integer -> Type -> Type
mulK Integer
n Type
x
  | Just v :: Type
v <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe Match Type
swapVars = Type
v
  | Bool
otherwise           = TFun -> Type -> Type -> Type
tf2 TFun
TCMul Type
x Type
y
  where
  mulK :: Integer -> Type -> Type
mulK 0 _ = Int -> Type
forall a. Integral a => a -> Type
tNum (0 :: Int)
  mulK 1 t :: Type
t = Type
t
  mulK n :: Integer
n t :: Type
t | TCon (TF TCMul) [a :: Type
a,b :: Type
b] <- Type
t'
           , Just a' :: Nat'
a' <- Type -> Maybe Nat'
tIsNat' Type
a = case Nat'
a' of
                                     Inf   -> Type
t
                                     Nat m :: Integer
m -> TFun -> Type -> Type -> Type
tf2 TFun
TCMul (Integer -> Type
forall a. Integral a => a -> Type
tNum (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m)) Type
b
           | TCon (TF TCDiv) [a :: Type
a,b :: Type
b] <- Type
t'
           , Just b' :: Integer
b' <- Type -> Maybe Integer
tIsNum Type
b
           -- XXX: similar for a = b * k?
           , Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
b' = Type -> Type -> Type
tSub Type
a (Type -> Type -> Type
tMod Type
a Type
b)


           | Bool
otherwise = TFun -> Type -> Type -> Type
tf2 TFun
TCMul (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
n) Type
t
    where t' :: Type
t' = Type -> Type
tNoUser Type
t

  swapVars :: Match Type
swapVars = do TVar
a <- Pat Type TVar
aTVar Type
x
                TVar
b <- Pat Type TVar
aTVar Type
y
                Bool -> Match ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TVar
b TVar -> TVar -> Bool
forall a. Ord a => a -> a -> Bool
< TVar
a)
                Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return (TFun -> Type -> Type -> Type
tf2 TFun
TCMul Type
y Type
x)



tDiv :: Type -> Type -> Type
tDiv :: Type -> Type -> Type
tDiv x :: Type
x y :: Type
y
  | Just t :: Type
t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp TFun
TCDiv ((Nat' -> Nat' -> Maybe Nat') -> [Nat'] -> Maybe Nat'
forall a b. (a -> a -> b) -> [a] -> b
op2 Nat' -> Nat' -> Maybe Nat'
nDiv) [Type
x,Type
y] = Type
t
  | Type -> Bool
tIsInf Type
x = TCErrorMessage -> Type
tBadNumber (TCErrorMessage -> Type) -> TCErrorMessage -> Type
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "Division of `inf`."
  | Just 0 <- Type -> Maybe Integer
tIsNum Type
y = TCErrorMessage -> Type
tBadNumber (TCErrorMessage -> Type) -> TCErrorMessage -> Type
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "Division by 0."
  | Bool
otherwise = TFun -> Type -> Type -> Type
tf2 TFun
TCDiv Type
x Type
y

tMod :: Type -> Type -> Type
tMod :: Type -> Type -> Type
tMod x :: Type
x y :: Type
y
  | Just t :: Type
t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp TFun
TCMod ((Nat' -> Nat' -> Maybe Nat') -> [Nat'] -> Maybe Nat'
forall a b. (a -> a -> b) -> [a] -> b
op2 Nat' -> Nat' -> Maybe Nat'
nMod) [Type
x,Type
y] = Type
t
  | Type -> Bool
tIsInf Type
x = TCErrorMessage -> Type
tBadNumber (TCErrorMessage -> Type) -> TCErrorMessage -> Type
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "Modulus of `inf`."
  | Just 0 <- Type -> Maybe Integer
tIsNum Type
x = TCErrorMessage -> Type
tBadNumber (TCErrorMessage -> Type) -> TCErrorMessage -> Type
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "Modulus by 0."
  | Bool
otherwise = TFun -> Type -> Type -> Type
tf2 TFun
TCMod Type
x Type
y

tCeilDiv :: Type -> Type -> Type
tCeilDiv :: Type -> Type -> Type
tCeilDiv x :: Type
x y :: Type
y
  | Just t :: Type
t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp TFun
TCCeilDiv ((Nat' -> Nat' -> Maybe Nat') -> [Nat'] -> Maybe Nat'
forall a b. (a -> a -> b) -> [a] -> b
op2 Nat' -> Nat' -> Maybe Nat'
nCeilDiv) [Type
x,Type
y] = Type
t
  | Type -> Bool
tIsInf Type
x = TCErrorMessage -> Type
tBadNumber (TCErrorMessage -> Type) -> TCErrorMessage -> Type
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "CeilDiv of `inf`."
  | Type -> Bool
tIsInf Type
y = TCErrorMessage -> Type
tBadNumber (TCErrorMessage -> Type) -> TCErrorMessage -> Type
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "CeilDiv by `inf`."
  | Just 0 <- Type -> Maybe Integer
tIsNum Type
y = TCErrorMessage -> Type
tBadNumber (TCErrorMessage -> Type) -> TCErrorMessage -> Type
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "CeilDiv by 0."
  | Bool
otherwise = TFun -> Type -> Type -> Type
tf2 TFun
TCCeilDiv Type
x Type
y

tCeilMod :: Type -> Type -> Type
tCeilMod :: Type -> Type -> Type
tCeilMod x :: Type
x y :: Type
y
  | Just t :: Type
t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp TFun
TCCeilMod ((Nat' -> Nat' -> Maybe Nat') -> [Nat'] -> Maybe Nat'
forall a b. (a -> a -> b) -> [a] -> b
op2 Nat' -> Nat' -> Maybe Nat'
nCeilMod) [Type
x,Type
y] = Type
t
  | Type -> Bool
tIsInf Type
x = TCErrorMessage -> Type
tBadNumber (TCErrorMessage -> Type) -> TCErrorMessage -> Type
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "CeilMod of `inf`."
  | Type -> Bool
tIsInf Type
y = TCErrorMessage -> Type
tBadNumber (TCErrorMessage -> Type) -> TCErrorMessage -> Type
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "CeilMod by `inf`."
  | Just 0 <- Type -> Maybe Integer
tIsNum Type
x = TCErrorMessage -> Type
tBadNumber (TCErrorMessage -> Type) -> TCErrorMessage -> Type
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "CeilMod to size 0."
  | Bool
otherwise = TFun -> Type -> Type -> Type
tf2 TFun
TCCeilMod Type
x Type
y

tExp :: Type -> Type -> Type
tExp :: Type -> Type -> Type
tExp x :: Type
x y :: Type
y
  | Just t :: Type
t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp TFun
TCExp (([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
total ((Nat' -> Nat' -> Nat') -> [Nat'] -> Nat'
forall a b. (a -> a -> b) -> [a] -> b
op2 Nat' -> Nat' -> Nat'
nExp)) [Type
x,Type
y] = Type
t
  | Just 0 <- Type -> Maybe Integer
tIsNum Type
y = Int -> Type
forall a. Integral a => a -> Type
tNum (1 :: Int)
  | TCon (TF TCExp) [a :: Type
a,b :: Type
b] <- Type -> Type
tNoUser Type
y = Type -> Type -> Type
tExp Type
x (Type -> Type -> Type
tMul Type
a Type
b)
  | Bool
otherwise = TFun -> Type -> Type -> Type
tf2 TFun
TCExp Type
x Type
y


-- Normal: constants to the left
tMin :: Type -> Type -> Type
tMin :: Type -> Type -> Type
tMin x :: Type
x y :: Type
y
  | Just t :: Type
t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp TFun
TCMin (([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
total ((Nat' -> Nat' -> Nat') -> [Nat'] -> Nat'
forall a b. (a -> a -> b) -> [a] -> b
op2 Nat' -> Nat' -> Nat'
nMin)) [Type
x,Type
y] = Type
t
  | Just n :: Nat'
n <- Type -> Maybe Nat'
tIsNat' Type
x = Nat' -> Type -> Type
minK Nat'
n Type
y
  | Just n :: Nat'
n <- Type -> Maybe Nat'
tIsNat' Type
y = Nat' -> Type -> Type
minK Nat'
n Type
x
  | Just n :: Type
n <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe (Type -> Type -> Match Type
minPlusK Type
x Type
y Match Type -> Match Type -> Match Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type -> Type -> Match Type
minPlusK Type
y Type
x) = Type
n
  | Just n :: Type
n <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe (Match Type -> Maybe Type) -> Match Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ do (k :: Nat'
k,a :: Type
a) <- Type -> Match (Nat', Type)
isMinK Type
x
                              Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Match Type) -> Type -> Match Type
forall a b. (a -> b) -> a -> b
$ Nat' -> Type -> Type
minK Nat'
k (Type -> Type -> Type
tMin Type
a Type
y)
                          Match Type -> Match Type -> Match Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                          do (k :: Nat'
k,a :: Type
a) <- Type -> Match (Nat', Type)
isMinK Type
y
                             Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Match Type) -> Type -> Match Type
forall a b. (a -> b) -> a -> b
$ Nat' -> Type -> Type
minK Nat'
k (Type -> Type -> Type
tMin Type
x Type
a)
    = Type
n

  | Just n :: Type
n <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe (Match Type -> Maybe Type) -> Match Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ do (k1 :: Integer
k1,a :: Type
a) <- Type -> Match (Integer, Type)
isAddK Type
x
                              (k2 :: Integer
k2,b :: Type
b) <- Type -> Match (Integer, Type)
isAddK Type
y
                              Bool -> Match ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type
a Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
b)
                              Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Match Type) -> Type -> Match Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
tAdd (Integer -> Type
forall a. Integral a => a -> Type
tNum (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
k1 Integer
k2)) Type
a
    = Type
n

  | Type
x Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
y              = Type
x
  -- XXX: min (k + t) t -> t
  | Bool
otherwise           = TFun -> Type -> Type -> Type
tf2 TFun
TCMin Type
x Type
y
  where
  isAddK :: Type -> Match (Integer, Type)
isAddK ty :: Type
ty = do (a :: Type
a,b :: Type
b) <- Pat Type (Type, Type)
anAdd Type
ty
                 Integer
k     <- Pat Type Integer
aNat Type
a
                 (Integer, Type) -> Match (Integer, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
k,Type
b)

  isMinK :: Type -> Match (Nat', Type)
isMinK ty :: Type
ty = do (a :: Type
a,b :: Type
b) <- Pat Type (Type, Type)
aMin Type
ty
                 Nat'
k     <- Pat Type Nat'
aNat' Type
a
                 (Nat', Type) -> Match (Nat', Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Nat'
k,Type
b)

  minPlusK :: Type -> Type -> Match Type
minPlusK a :: Type
a b :: Type
b = do (k :: Integer
k,r :: Type
r) <- Type -> Match (Integer, Type)
isAddK Type
a
                    Bool -> Match ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= 1 Bool -> Bool -> Bool
&& Type
b Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
r)
                    Type -> Match Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
b


  minK :: Nat' -> Type -> Type
minK Inf t :: Type
t      = Type
t
  minK (Nat 0) _  = Int -> Type
forall a. Integral a => a -> Type
tNum (0 :: Int)
  minK (Nat k :: Integer
k) t :: Type
t
    | TCon (TF TCMin) [a :: Type
a,b :: Type
b] <- Type
t'
    , Just n :: Integer
n <- Type -> Maybe Integer
tIsNum Type
a   = TFun -> Type -> Type -> Type
tf2 TFun
TCMin (Integer -> Type
forall a. Integral a => a -> Type
tNum (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
k Integer
n)) Type
b

    | Bool
otherwise = TFun -> Type -> Type -> Type
tf2 TFun
TCMin (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
k) Type
t
    where t' :: Type
t' = Type -> Type
tNoUser Type
t

-- Normal: constants to the left
tMax :: Type -> Type -> Type
tMax :: Type -> Type -> Type
tMax x :: Type
x y :: Type
y
  | Just t :: Type
t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp TFun
TCMax (([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
total ((Nat' -> Nat' -> Nat') -> [Nat'] -> Nat'
forall a b. (a -> a -> b) -> [a] -> b
op2 Nat' -> Nat' -> Nat'
nMax)) [Type
x,Type
y] = Type
t
  | Just n :: Nat'
n <- Type -> Maybe Nat'
tIsNat' Type
x = Nat' -> Type -> Type
maxK Nat'
n Type
y
  | Just n :: Nat'
n <- Type -> Maybe Nat'
tIsNat' Type
y = Nat' -> Type -> Type
maxK Nat'
n Type
x
  | Bool
otherwise           = TFun -> Type -> Type -> Type
tf2 TFun
TCMax Type
x Type
y
  where
  maxK :: Nat' -> Type -> Type
maxK Inf _     = Type
tInf
  maxK (Nat 0) t :: Type
t = Type
t
  maxK (Nat k :: Integer
k) t :: Type
t

    | TCon (TF TCAdd) [a :: Type
a,b :: Type
b] <- Type
t'
    , Just n :: Integer
n <- Type -> Maybe Integer
tIsNum Type
a = if Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n
                             then Type
t
                             else Type -> Type -> Type
tAdd (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
n) (Type -> Type -> Type
tMax (Integer -> Type
forall a. Integral a => a -> Type
tNum (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
n)) Type
b)

    | TCon (TF TCSub) [a :: Type
a,b :: Type
b] <- Type
t'
    , Just n :: Nat'
n <- Type -> Maybe Nat'
tIsNat' Type
a =
      case Nat'
n of
        Inf   -> Type
t
        Nat m :: Integer
m -> if Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
m then Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
k else Type -> Type -> Type
tSub Type
a (Type -> Type -> Type
tMin (Integer -> Type
forall a. Integral a => a -> Type
tNum (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
k)) Type
b)

    | TCon (TF TCMax) [a :: Type
a,b :: Type
b] <- Type
t'
    , Just n :: Integer
n <- Type -> Maybe Integer
tIsNum Type
a  = TFun -> Type -> Type -> Type
tf2 TFun
TCMax (Integer -> Type
forall a. Integral a => a -> Type
tNum (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
k Integer
n)) Type
b

    | Bool
otherwise = TFun -> Type -> Type -> Type
tf2 TFun
TCMax (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
k) Type
t
    where t' :: Type
t' = Type -> Type
tNoUser Type
t


tWidth :: Type -> Type
tWidth :: Type -> Type
tWidth x :: Type
x
  | Just t :: Type
t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp TFun
TCWidth (([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
total ((Nat' -> Nat') -> [Nat'] -> Nat'
forall a b. (a -> b) -> [a] -> b
op1 Nat' -> Nat'
nWidth)) [Type
x] = Type
t
  | Bool
otherwise = TFun -> Type -> Type
tf1 TFun
TCWidth Type
x

tLenFromThenTo :: Type -> Type -> Type -> Type
tLenFromThenTo :: Type -> Type -> Type -> Type
tLenFromThenTo x :: Type
x y :: Type
y z :: Type
z
  | Just t :: Type
t <- TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp TFun
TCLenFromThenTo ((Nat' -> Nat' -> Nat' -> Maybe Nat') -> [Nat'] -> Maybe Nat'
forall a b. (a -> a -> a -> b) -> [a] -> b
op3 Nat' -> Nat' -> Nat' -> Maybe Nat'
nLenFromThenTo) [Type
x,Type
y,Type
z] = Type
t
  | Bool
otherwise = TFun -> Type -> Type -> Type -> Type
tf3 TFun
TCLenFromThenTo Type
x Type
y Type
z

total :: ([Nat'] -> Nat') -> ([Nat'] -> Maybe Nat')
total :: ([Nat'] -> Nat') -> [Nat'] -> Maybe Nat'
total f :: [Nat'] -> Nat'
f xs :: [Nat']
xs = Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just ([Nat'] -> Nat'
f [Nat']
xs)

op1 :: (a -> b) -> [a] -> b
op1 :: (a -> b) -> [a] -> b
op1 f :: a -> b
f ~[x :: a
x] = a -> b
f a
x

op2 :: (a -> a -> b) -> [a] -> b
op2 :: (a -> a -> b) -> [a] -> b
op2 f :: a -> a -> b
f ~[x :: a
x,y :: a
y] = a -> a -> b
f a
x a
y

op3 :: (a -> a -> a -> b) -> [a] -> b
op3 :: (a -> a -> a -> b) -> [a] -> b
op3 f :: a -> a -> a -> b
f ~[x :: a
x,y :: a
y,z :: a
z] = a -> a -> a -> b
f a
x a
y a
z

-- | Common checks: check for error, or simple full evaluation.
tOp :: TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp :: TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp tf :: TFun
tf f :: [Nat'] -> Maybe Nat'
f ts :: [Type]
ts
  | Just e :: TCErrorMessage
e  <- [Maybe TCErrorMessage] -> Maybe TCErrorMessage
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ((Type -> Maybe TCErrorMessage) -> [Type] -> [Maybe TCErrorMessage]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Maybe TCErrorMessage
tIsError [Type]
ts) = Type -> Maybe Type
forall a. a -> Maybe a
Just (TCErrorMessage -> Type
tBadNumber TCErrorMessage
e)
  | Just xs :: [Nat']
xs <- (Type -> Maybe Nat') -> [Type] -> Maybe [Nat']
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> Maybe Nat'
tIsNat' [Type]
ts =
      Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ case [Nat'] -> Maybe Nat'
f [Nat']
xs of
               Nothing -> TCErrorMessage -> Type
tBadNumber ([Nat'] -> TCErrorMessage
err [Nat']
xs)
               Just n :: Nat'
n  -> Nat' -> Type
tNat' Nat'
n
  | Bool
otherwise = Maybe Type
forall a. Maybe a
Nothing
  where
  err :: [Nat'] -> TCErrorMessage
err xs :: [Nat']
xs = String -> TCErrorMessage
TCErrorMessage (String -> TCErrorMessage) -> String -> TCErrorMessage
forall a b. (a -> b) -> a -> b
$
              "Invalid type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. PP a => a -> Doc
pp (TCon -> [Type] -> Type
TCon (TFun -> TCon
TF TFun
tf) ((Nat' -> Type) -> [Nat'] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Nat' -> Type
tNat' [Nat']
xs)))