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