{-# 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)


tRebuild' :: Bool -> Type -> Type
tRebuild' :: Bool -> Type -> Type
tRebuild' Bool
withUser = Type -> Type
go
  where
  go :: Type -> Type
go Type
ty =
    case Type
ty of
      TUser Name
x [Type]
xs 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 TVar
_        -> Type
ty
      TRec RecordMap Ident Type
xs       -> RecordMap Ident Type -> Type
TRec ((Type -> Type) -> RecordMap Ident Type -> RecordMap Ident Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> Type
go RecordMap Ident Type
xs)
      TCon TCon
tc [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 TCon
tc [Type]
ts =
  case TCon
tc of
    TF TFun
f ->
      case (TFun
f, [Type]
ts) of
        (TFun
TCAdd, [Type
x, Type
y]) -> Type -> Type -> Type
tAdd Type
x Type
y
        (TFun
TCSub, [Type
x, Type
y]) -> Type -> Type -> Type
tSub Type
x Type
y
        (TFun
TCMul, [Type
x, Type
y]) -> Type -> Type -> Type
tMul Type
x Type
y
        (TFun
TCExp, [Type
x, Type
y]) -> Type -> Type -> Type
tExp Type
x Type
y
        (TFun
TCDiv, [Type
x, Type
y]) -> Type -> Type -> Type
tDiv Type
x Type
y
        (TFun
TCMod, [Type
x, Type
y]) -> Type -> Type -> Type
tMod Type
x Type
y
        (TFun
TCMin, [Type
x, Type
y]) -> Type -> Type -> Type
tMin Type
x Type
y
        (TFun
TCMax, [Type
x, Type
y]) -> Type -> Type -> Type
tMax Type
x Type
y
        (TFun
TCWidth, [Type
x]) -> Type -> Type
tWidth Type
x
        (TFun
TCCeilDiv, [Type
x, Type
y]) -> Type -> Type -> Type
tCeilDiv Type
x Type
y
        (TFun
TCCeilMod, [Type
x, Type
y]) -> Type -> Type -> Type
tCeilMod Type
x Type
y
        (TFun
TCLenFromThenTo, [Type
x, Type
y, Type
z]) -> Type -> Type -> Type -> Type
tLenFromThenTo Type
x Type
y Type
z
        (TFun, [Type])
_ -> TCon -> [Type] -> Type
TCon TCon
tc [Type]
ts
    TCon
_ -> TCon -> [Type] -> Type
TCon TCon
tc [Type]
ts

-- Normal: constants to the left
tAdd :: Type -> Type -> Type
tAdd :: Type -> Type -> Type
tAdd Type
x Type
y
  | Just 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 Integer
n <- Type -> Maybe Integer
tIsNum Type
x  = Integer -> Type -> Type
addK Integer
n Type
y
  | Just Integer
n <- Type -> Maybe Integer
tIsNum Type
y  = Integer -> Type -> Type
addK Integer
n Type
x
  | Just (Integer
n,Type
x1) <- Type -> Maybe (Integer, Type)
isSumK Type
x = Integer -> Type -> Type
addK Integer
n (Type -> Type -> Type
tAdd Type
x1 Type
y)
  | Just (Integer
n,Type
y1) <- Type -> Maybe (Integer, Type)
isSumK Type
y = Integer -> Type -> Type
addK Integer
n (Type -> Type -> Type
tAdd Type
x Type
y1)
  | Just Type
v <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe (do (Type
a,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 Type
v <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe (do (Type
a,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 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 Type
t = case Type -> Type
tNoUser Type
t of
               TCon (TF TFun
TCAdd) [ Type
l, 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)
               Type
_ -> Maybe (Integer, Type)
forall a. Maybe a
Nothing

  addK :: Integer -> Type -> Type
addK Integer
0 Type
t = Type
t
  addK Integer
n Type
t | Just (Integer
m,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 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 (Type
a,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
                                         Ordering
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
                                         Ordering
EQ -> Type
a
                                         Ordering
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 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 (Type
a,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 (Type
a,Type
b1)  <- Pat Type (Type, Type)
aMul Type
x
              (Type
a',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 (Int
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 Type
x Type
y
  | Just 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  = Type -> Type
tError (TFun -> Type -> Type -> Type
tf2 TFun
TCSub Type
x Type
y)
  | Just Integer
0 <- Maybe Integer
yNum = Type
x
  | Just Integer
k <- Maybe Integer
yNum
  , TCon (TF TFun
TCAdd) [Type
a,Type
b] <- Type -> Type
tNoUser Type
x
  , Just 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
                           Ordering
EQ -> Type
b
                           Ordering
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
                           Ordering
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 Type
v <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe (do (Type
a,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 Type
v <- Match Type -> Maybe Type
forall a. Match a -> Maybe a
matchMaybe (do (Type
a,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 Type
x Type
y
  | Just 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 Integer
n <- Type -> Maybe Integer
tIsNum Type
x  = Integer -> Type -> Type
mulK Integer
n Type
y
  | Just Integer
n <- Type -> Maybe Integer
tIsNum Type
y  = Integer -> Type -> Type
mulK Integer
n Type
x
  | Just 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 Integer
0 Type
_ = Int -> Type
forall a. Integral a => a -> Type
tNum (Int
0 :: Int)
  mulK Integer
1 Type
t = Type
t
  mulK Integer
n Type
t | TCon (TF TFun
TCMul) [Type
a,Type
b] <- Type
t'
           , Just Nat'
a' <- Type -> Maybe Nat'
tIsNat' Type
a = case Nat'
a' of
                                     Nat'
Inf   -> Type
t
                                     Nat 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 TFun
TCDiv) [Type
a,Type
b] <- Type
t'
           , Just 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 Type
x Type
y
  | Just 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 = Type
bad
  | Just Integer
0 <- Type -> Maybe Integer
tIsNum Type
y = Type
bad
  | Bool
otherwise = TFun -> Type -> Type -> Type
tf2 TFun
TCDiv Type
x Type
y
    where bad :: Type
bad = Type -> Type
tError (TFun -> Type -> Type -> Type
tf2 TFun
TCDiv Type
x Type
y)

tMod :: Type -> Type -> Type
tMod :: Type -> Type -> Type
tMod Type
x Type
y
  | Just 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 = Type
bad
  | Just Integer
0 <- Type -> Maybe Integer
tIsNum Type
y = Type
bad
  | Bool
otherwise = TFun -> Type -> Type -> Type
tf2 TFun
TCMod Type
x Type
y
    where bad :: Type
bad = Type -> Type
tError (TFun -> Type -> Type -> Type
tf2 TFun
TCMod Type
x Type
y)

tCeilDiv :: Type -> Type -> Type
tCeilDiv :: Type -> Type -> Type
tCeilDiv Type
x Type
y
  | Just 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 = Type
bad
  | Type -> Bool
tIsInf Type
y = Type
bad
  | Just Integer
0 <- Type -> Maybe Integer
tIsNum Type
y = Type
bad
  | Bool
otherwise = TFun -> Type -> Type -> Type
tf2 TFun
TCCeilDiv Type
x Type
y
    where bad :: Type
bad = Type -> Type
tError (TFun -> Type -> Type -> Type
tf2 TFun
TCCeilDiv Type
x Type
y)

tCeilMod :: Type -> Type -> Type
tCeilMod :: Type -> Type -> Type
tCeilMod Type
x Type
y
  | Just 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 = Type
bad
  | Type -> Bool
tIsInf Type
y = Type
bad
  | Just Integer
0 <- Type -> Maybe Integer
tIsNum Type
x = Type
bad
  | Bool
otherwise = TFun -> Type -> Type -> Type
tf2 TFun
TCCeilMod Type
x Type
y
    where bad :: Type
bad = Type -> Type
tError (TFun -> Type -> Type -> Type
tf2 TFun
TCCeilMod Type
x Type
y)


tExp :: Type -> Type -> Type
tExp :: Type -> Type -> Type
tExp Type
x Type
y
  | Just 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 Integer
0 <- Type -> Maybe Integer
tIsNum Type
y = Int -> Type
forall a. Integral a => a -> Type
tNum (Int
1 :: Int)
  | TCon (TF TFun
TCExp) [Type
a,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 Type
x Type
y
  | Just 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 Nat'
n <- Type -> Maybe Nat'
tIsNat' Type
x = Nat' -> Type -> Type
minK Nat'
n Type
y
  | Just Nat'
n <- Type -> Maybe Nat'
tIsNat' Type
y = Nat' -> Type -> Type
minK Nat'
n Type
x
  | Just 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 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 (Nat'
k,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 (Nat'
k,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 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 (Integer
k1,Type
a) <- Type -> Match (Integer, Type)
isAddK Type
x
                              (Integer
k2,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 Type
ty = do (Type
a,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 Type
ty = do (Type
a,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 Type
a Type
b = do (Integer
k,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
>= Integer
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 Nat'
Inf Type
t      = Type
t
  minK (Nat Integer
0) Type
_  = Int -> Type
forall a. Integral a => a -> Type
tNum (Int
0 :: Int)
  minK (Nat Integer
k) Type
t
    | TCon (TF TFun
TCMin) [Type
a,Type
b] <- Type
t'
    , Just 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 Type
x Type
y
  | Just 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 Nat'
n <- Type -> Maybe Nat'
tIsNat' Type
x = Nat' -> Type -> Type
maxK Nat'
n Type
y
  | Just 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 Nat'
Inf Type
_     = Type
tInf
  maxK (Nat Integer
0) Type
t = Type
t
  maxK (Nat Integer
k) Type
t

    | TCon (TF TFun
TCAdd) [Type
a,Type
b] <- Type
t'
    , Just 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 TFun
TCSub) [Type
a,Type
b] <- Type
t'
    , Just Nat'
n <- Type -> Maybe Nat'
tIsNat' Type
a =
      case Nat'
n of
        Nat'
Inf   -> Type
t
        Nat 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 TFun
TCMax) [Type
a,Type
b] <- Type
t'
    , Just 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 Type
x
  | Just 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 Type
x Type
y Type
z
  | Just 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 [Nat'] -> Nat'
f [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 a -> b
f ~[a
x] = a -> b
f a
x

op2 :: (a -> a -> b) -> [a] -> b
op2 :: (a -> a -> b) -> [a] -> b
op2 a -> a -> b
f ~[a
x,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 a -> a -> a -> b
f ~[a
x,a
y,a
z] = a -> a -> a -> b
f a
x a
y a
z

-- | Common checks: check for error, or simple full evaluation.
-- We assume that input kinds and the result kind are the same (i.e., Nat)
tOp :: TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp :: TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type
tOp TFun
tf [Nat'] -> Maybe Nat'
f [Type]
ts
  | Just Type
t <- [Maybe Type] -> Maybe Type
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ((Type -> Maybe Type) -> [Type] -> [Maybe Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Maybe Type
tIsError [Type]
ts) = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Type
tError Type
t)
    -- assumes result kind the same as input kind

  | Just [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
               Maybe Nat'
Nothing -> Type -> Type
tError (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))
               Just Nat'
n  -> Nat' -> Type
tNat' Nat'
n
  | Bool
otherwise = Maybe Type
forall a. Maybe a
Nothing