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