    {-# LANGUAGE Safe, PatternGuards, MultiWayIf #-}
    module Cryptol.TypeCheck.Solver.Numeric
      ( cryIsEqual, cryIsNotEqual, cryIsGeq
      ) where

    import           Control.Applicative(Alternative(..))
    import           Control.Monad (guard,mzero)
    import           Data.List (sortBy)

    import Cryptol.Utils.Patterns
    import Cryptol.TypeCheck.PP
    import Cryptol.TypeCheck.Type hiding (tMul)
    import Cryptol.TypeCheck.TypePat
    import Cryptol.TypeCheck.Solver.Types
    import Cryptol.TypeCheck.Solver.InfNat
    import Cryptol.TypeCheck.Solver.Numeric.Interval
    import Cryptol.TypeCheck.SimpType as Simp

    {- Convention for comments:

      K1, K2 ...          Concrete constants
      s1, s2, t1, t2 ...  Arbitrary type expressions
      a, b, c ...         Type variables

    -}

    -- | Try to solve @t1 = t2@
    cryIsEqual :: Ctxt -> Type -> Type -> Solved
    cryIsEqual :: Ctxt -> Type -> Type -> Solved
    cryIsEqual ctxt :: Ctxt
    ctxt t1 :: Type
    t1 t2 :: Type
    t2 =
      Solved -> Match Solved -> Solved
    forall a. a -> Match a -> a
    matchDefault Solved
    Unsolved (Match Solved -> Solved) -> Match Solved -> Solved
    forall a b. (a -> b) -> a -> b
    $
            (PC -> (Nat' -> Nat' -> Bool) -> Type -> Type -> Match Solved
    pBin PC
    PEqual Nat' -> Nat' -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) Type
    t1 Type
    t2)
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (Pat Type Nat'
    aNat' Type
    t1 Match Nat' -> (Nat' -> Match Solved) -> Match Solved
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Ctxt -> Type -> Nat' -> Match Solved
    tryEqK Ctxt
    ctxt Type
    t2)
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (Pat Type Nat'
    aNat' Type
    t2 Match Nat' -> (Nat' -> Match Solved) -> Match Solved
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Ctxt -> Type -> Nat' -> Match Solved
    tryEqK Ctxt
    ctxt Type
    t1)
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (Pat Type TVar
    aTVar Type
    t1 Match TVar -> (TVar -> Match Solved) -> Match Solved
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Type -> TVar -> Match Solved
    tryEqVar Type
    t2)
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (Pat Type TVar
    aTVar Type
    t2 Match TVar -> (TVar -> Match Solved) -> Match Solved
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Type -> TVar -> Match Solved
    tryEqVar Type
    t1)
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> ( Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type
    t1 Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    t2) Match () -> Match Solved -> Match Solved
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type] -> Solved
    SolvedIf []))
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Type -> Match Solved
    tryEqMin Type
    t1 Type
    t2
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Type -> Match Solved
    tryEqMin Type
    t2 Type
    t1
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Type -> Match Solved
    tryEqMins Type
    t1 Type
    t2
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Type -> Match Solved
    tryEqMins Type
    t2 Type
    t1
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Type -> Match Solved
    tryEqMulConst Type
    t1 Type
    t2
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Ctxt -> Type -> Type -> Match Solved
    tryEqAddInf Ctxt
    ctxt Type
    t1 Type
    t2
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (Type -> Type -> Type) -> Type -> Type -> Match Solved
    tryAddConst Type -> Type -> Type
    (=#=) Type
    t1 Type
    t2
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Ctxt -> (Type -> Type -> Type) -> Type -> Type -> Match Solved
    tryCancelVar Ctxt
    ctxt Type -> Type -> Type
    (=#=) Type
    t1 Type
    t2
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Type -> Match Solved
    tryLinearSolution Type
    t1 Type
    t2
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Type -> Match Solved
    tryLinearSolution Type
    t2 Type
    t1

    -- | Try to solve @t1 /= t2@
    cryIsNotEqual :: Ctxt -> Type -> Type -> Solved
    cryIsNotEqual :: Ctxt -> Type -> Type -> Solved
    cryIsNotEqual _i :: Ctxt
    _i t1 :: Type
    t1 t2 :: Type
    t2 = Solved -> Match Solved -> Solved
    forall a. a -> Match a -> a
    matchDefault Solved
    Unsolved (PC -> (Nat' -> Nat' -> Bool) -> Type -> Type -> Match Solved
    pBin PC
    PNeq Nat' -> Nat' -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=) Type
    t1 Type
    t2)

    -- | Try to solve @t1 >= t2@
    cryIsGeq :: Ctxt -> Type -> Type -> Solved
    cryIsGeq :: Ctxt -> Type -> Type -> Solved
    cryIsGeq i :: Ctxt
    i t1 :: Type
    t1 t2 :: Type
    t2 =
      Solved -> Match Solved -> Solved
    forall a. a -> Match a -> a
    matchDefault Solved
    Unsolved (Match Solved -> Solved) -> Match Solved -> Solved
    forall a b. (a -> b) -> a -> b
    $
            (PC -> (Nat' -> Nat' -> Bool) -> Type -> Type -> Match Solved
    pBin PC
    PGeq Nat' -> Nat' -> Bool
    forall a. Ord a => a -> a -> Bool
    (>=) Type
    t1 Type
    t2)
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (Pat Type Nat'
    aNat' Type
    t1 Match Nat' -> (Nat' -> Match Solved) -> Match Solved
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Ctxt -> Type -> Nat' -> Match Solved
    tryGeqKThan Ctxt
    i Type
    t2)
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (Pat Type Nat'
    aNat' Type
    t2 Match Nat' -> (Nat' -> Match Solved) -> Match Solved
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Ctxt -> Type -> Nat' -> Match Solved
    tryGeqThanK Ctxt
    i Type
    t1)
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (Pat Type TVar
    aTVar Type
    t2 Match TVar -> (TVar -> Match Solved) -> Match Solved
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Ctxt -> Type -> TVar -> Match Solved
    tryGeqThanVar Ctxt
    i Type
    t1)
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Ctxt -> Type -> Type -> Match Solved
    tryGeqThanSub Ctxt
    i Type
    t1 Type
    t2
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (Ctxt -> Type -> Type -> Match Solved
    geqByInterval Ctxt
    i Type
    t1 Type
    t2)
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type
    t1 Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    t2) Match () -> Match Solved -> Match Solved
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type] -> Solved
    SolvedIf []))
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (Type -> Type -> Type) -> Type -> Type -> Match Solved
    tryAddConst Type -> Type -> Type
    (>==) Type
    t1 Type
    t2
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Ctxt -> (Type -> Type -> Type) -> Type -> Type -> Match Solved
    tryCancelVar Ctxt
    i Type -> Type -> Type
    (>==) Type
    t1 Type
    t2
        Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Type -> Match Solved
    tryMinIsGeq Type
    t1 Type
    t2
        -- XXX: k >= width e
        -- XXX: width e >= k

      -- XXX: max t 10 >= 2 --> True
      -- XXX: max t 2 >= 10 --> a >= 10

    -- | Try to solve something by evaluation.
    pBin :: PC -> (Nat' -> Nat' -> Bool) -> Type -> Type -> Match Solved
    pBin :: PC -> (Nat' -> Nat' -> Bool) -> Type -> Type -> Match Solved
    pBin tf :: PC
    tf p :: Nat' -> Nat' -> Bool
    p t1 :: Type
    t1 t2 :: Type
    t2 =
          TCErrorMessage -> Solved
    Unsolvable (TCErrorMessage -> Solved) -> Match TCErrorMessage -> Match Solved
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Kind -> Pat Type TCErrorMessage
    anError Kind
    KNum Type
    t1
      Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> TCErrorMessage -> Solved
    Unsolvable (TCErrorMessage -> Solved) -> Match TCErrorMessage -> Match Solved
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Kind -> Pat Type TCErrorMessage
    anError Kind
    KNum Type
    t2
      Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (do Nat'
    x <- Pat Type Nat'
    aNat' Type
    t1
              Nat'
    y <- Pat Type Nat'
    aNat' Type
    t2
              Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solved -> Match Solved) -> Solved -> Match Solved
    forall a b. (a -> b) -> a -> b
    $ if Nat' -> Nat' -> Bool
    p Nat'
    x Nat'
    y
                          then [Type] -> Solved
    SolvedIf []
                          else TCErrorMessage -> Solved
    Unsolvable (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
    forall a b. (a -> b) -> a -> b
    $ String -> TCErrorMessage
    TCErrorMessage
                            (String -> TCErrorMessage) -> String -> TCErrorMessage
    forall a b. (a -> b) -> a -> b
    $ "Unsolvable constraint: " 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 (PC -> TCon
    PC PC
    tf) [ Nat' -> Type
    tNat' Nat'
    x, Nat' -> Type
    tNat' Nat'
    y ])))

    --------------------------------------------------------------------------------
    -- GEQ

    -- | Try to solve @K >= t@
    tryGeqKThan :: Ctxt -> Type -> Nat' -> Match Solved
    tryGeqKThan :: Ctxt -> Type -> Nat' -> Match Solved
    tryGeqKThan _ _ Inf = Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type] -> Solved
    SolvedIf [])
    tryGeqKThan _ ty :: Type
    ty (Nat n :: Integer
    n) =

      -- K1 >= K2 * t
      do (a :: Type
    a,b :: Type
    b) <- Pat Type (Type, Type)
    aMul Type
    ty
         Nat'
    m     <- Pat Type Nat'
    aNat' Type
    a
         Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solved -> Match Solved) -> Solved -> Match Solved
    forall a b. (a -> b) -> a -> b
    $ [Type] -> Solved
    SolvedIf
                ([Type] -> Solved) -> [Type] -> Solved
    forall a b. (a -> b) -> a -> b
    $ case Nat'
    m of
                    Inf   -> [ Type
    b Type -> Type -> Type
    =#= Type
    tZero ]
                    Nat 0 -> []
                    Nat k :: Integer
    k -> [ Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div Integer
    n Integer
    k) Type -> Type -> Type
    >== Type
    b ]

    -- | Try to solve @t >= K@
    tryGeqThanK :: Ctxt -> Type -> Nat' -> Match Solved
    tryGeqThanK :: Ctxt -> Type -> Nat' -> Match Solved
    tryGeqThanK _ t :: Type
    t Inf = Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type] -> Solved
    SolvedIf [ Type
    t Type -> Type -> Type
    =#= Type
    tInf ])
    tryGeqThanK _ t :: Type
    t (Nat k :: Integer
    k) =

      -- K1 + t >= K2
      do (a :: Type
    a,b :: Type
    b) <- Pat Type (Type, Type)
    anAdd Type
    t
         Integer
    n     <- Pat Type Integer
    aNat Type
    a
         Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solved -> Match Solved) -> Solved -> Match Solved
    forall a b. (a -> b) -> a -> b
    $ [Type] -> Solved
    SolvedIf ([Type] -> Solved) -> [Type] -> Solved
    forall a b. (a -> b) -> a -> b
    $ if Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    k
                                then []
                                else [ Type
    b Type -> Type -> Type
    >== Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer
    k Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    n) ]
      -- XXX: K1 ^^ n >= K2

    tryGeqThanSub :: Ctxt -> Type -> Type -> Match Solved
    tryGeqThanSub :: Ctxt -> Type -> Type -> Match Solved
    tryGeqThanSub _ x :: Type
    x y :: Type
    y =

      -- t1 >= t1 - t2
      do (a :: Type
    a,_) <- 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
    a)
         Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type] -> Solved
    SolvedIf [])

    tryGeqThanVar :: Ctxt -> Type -> TVar -> Match Solved
    tryGeqThanVar :: Ctxt -> Type -> TVar -> Match Solved
    tryGeqThanVar _ctxt :: Ctxt
    _ctxt ty :: Type
    ty x :: TVar
    x =
      -- (t + a) >= a
      do (a :: Type
    a,b :: Type
    b) <- Pat Type (Type, Type)
    anAdd Type
    ty
         let check :: Type -> Match Solved
    check y :: Type
    y = do TVar
    x' <- Pat Type TVar
    aTVar Type
    y
                          Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (TVar
    x TVar -> TVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TVar
    x')
                          Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type] -> Solved
    SolvedIf [])
         Type -> Match Solved
    check Type
    a Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Match Solved
    check Type
    b

    -- | Try to prove GEQ by considering the known intervals for the given types.
    geqByInterval :: Ctxt -> Type -> Type -> Match Solved
    geqByInterval :: Ctxt -> Type -> Type -> Match Solved
    geqByInterval ctxt :: Ctxt
    ctxt x :: Type
    x y :: Type
    y =
      let ix :: Interval
    ix = Ctxt -> Type -> Interval
    typeInterval Ctxt
    ctxt Type
    x
          iy :: Interval
    iy = Ctxt -> Type -> Interval
    typeInterval Ctxt
    ctxt Type
    y
      in case (Interval -> Nat'
    iLower Interval
    ix, Interval -> Maybe Nat'
    iUpper Interval
    iy) of
           (l :: Nat'
    l,Just n :: Nat'
    n) | Nat'
    l Nat' -> Nat' -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Nat'
    n -> Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type] -> Solved
    SolvedIf [])
           _                   -> Match Solved
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    -- min K1 t >= K2 ~~> t >= K2, if K1 >= K2;  Err otherwise
    tryMinIsGeq :: Type -> Type -> Match Solved
    tryMinIsGeq :: Type -> Type -> Match Solved
    tryMinIsGeq t1 :: Type
    t1 t2 :: Type
    t2 =
      do (a :: Type
    a,b :: Type
    b) <- Pat Type (Type, Type)
    aMin Type
    t1
         Integer
    k1    <- Pat Type Integer
    aNat Type
    a
         Integer
    k2    <- Pat Type Integer
    aNat Type
    t2
         Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solved -> Match Solved) -> Solved -> Match Solved
    forall a b. (a -> b) -> a -> b
    $ if Integer
    k1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    k2
                   then [Type] -> Solved
    SolvedIf [ Type
    b Type -> Type -> Type
    >== Type
    t2 ]
                   else TCErrorMessage -> Solved
    Unsolvable (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
    forall a b. (a -> b) -> a -> b
    $ String -> TCErrorMessage
    TCErrorMessage (String -> TCErrorMessage) -> String -> TCErrorMessage
    forall a b. (a -> b) -> a -> b
    $
                          Integer -> String
    forall a. Show a => a -> String
    show Integer
    k1 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " can't be greater than " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    k2

    --------------------------------------------------------------------------------

    -- | Cancel finite positive variables from both sides.
    -- @(fin a, a >= 1) =>  a * t1 == a * t2 ~~~> t1 == t2@
    -- @(fin a, a >= 1) =>  a * t1 >= a * t2 ~~~> t1 >= t2@
    tryCancelVar :: Ctxt -> (Type -> Type -> Prop) -> Type -> Type -> Match Solved
    tryCancelVar :: Ctxt -> (Type -> Type -> Type) -> Type -> Type -> Match Solved
    tryCancelVar ctxt :: Ctxt
    ctxt p :: Type -> Type -> Type
    p t1 :: Type
    t1 t2 :: Type
    t2 =
      let lhs :: [(Type, Maybe TVar)]
    lhs = Type -> [(Type, Maybe TVar)]
    preproc Type
    t1
          rhs :: [(Type, Maybe TVar)]
    rhs = Type -> [(Type, Maybe TVar)]
    preproc Type
    t2
      in case [Type]
    -> [Type]
    -> [(Type, Maybe TVar)]
    -> [(Type, Maybe TVar)]
    -> Maybe Solved
    forall a.
    Ord a =>
    [Type]
    -> [Type] -> [(Type, Maybe a)] -> [(Type, Maybe a)] -> Maybe Solved
    check [] [] [(Type, Maybe TVar)]
    lhs [(Type, Maybe TVar)]
    rhs of
           Nothing -> String -> Match Solved
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail ""
           Just x :: Solved
    x  -> Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return Solved
    x

      where
      check :: [Type]
    -> [Type] -> [(Type, Maybe a)] -> [(Type, Maybe a)] -> Maybe Solved
    check doneLHS :: [Type]
    doneLHS doneRHS :: [Type]
    doneRHS lhs :: [(Type, Maybe a)]
    lhs@((a :: Type
    a,mbA :: Maybe a
    mbA) : moreLHS :: [(Type, Maybe a)]
    moreLHS) rhs :: [(Type, Maybe a)]
    rhs@((b :: Type
    b, mbB :: Maybe a
    mbB) : moreRHS :: [(Type, Maybe a)]
    moreRHS) =
        do a
    x <- Maybe a
    mbA
           a
    y <- Maybe a
    mbB
           case a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare a
    x a
    y of
             LT -> [Type]
    -> [Type] -> [(Type, Maybe a)] -> [(Type, Maybe a)] -> Maybe Solved
    check (Type
    a Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    : [Type]
    doneLHS) [Type]
    doneRHS [(Type, Maybe a)]
    moreLHS [(Type, Maybe a)]
    rhs
             EQ -> Solved -> Maybe Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solved -> Maybe Solved) -> Solved -> Maybe Solved
    forall a b. (a -> b) -> a -> b
    $ [Type] -> Solved
    SolvedIf [ Type -> Type -> Type
    p ([Type] -> Type
    term ([Type]
    doneLHS [Type] -> [Type] -> [Type]
    forall a. [a] -> [a] -> [a]
    ++ ((Type, Maybe a) -> Type) -> [(Type, Maybe a)] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (Type, Maybe a) -> Type
    forall a b. (a, b) -> a
    fst [(Type, Maybe a)]
    moreLHS))
                                         ([Type] -> Type
    term ([Type]
    doneRHS [Type] -> [Type] -> [Type]
    forall a. [a] -> [a] -> [a]
    ++ ((Type, Maybe a) -> Type) -> [(Type, Maybe a)] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (Type, Maybe a) -> Type
    forall a b. (a, b) -> a
    fst [(Type, Maybe a)]
    moreRHS)) ]
             GT -> [Type]
    -> [Type] -> [(Type, Maybe a)] -> [(Type, Maybe a)] -> Maybe Solved
    check [Type]
    doneLHS (Type
    b Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    : [Type]
    doneRHS) [(Type, Maybe a)]
    lhs [(Type, Maybe a)]
    moreRHS
      check _ _ _ _ = Maybe Solved
    forall a. Maybe a
    Nothing

      term :: [Type] -> Type
    term xs :: [Type]
    xs = case [Type]
    xs of
                  [] -> Int -> Type
    forall a. Integral a => a -> Type
    tNum (1::Int)
                  _  -> (Type -> Type -> Type) -> [Type] -> Type
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 Type -> Type -> Type
    tMul [Type]
    xs

      preproc :: Type -> [(Type, Maybe TVar)]
    preproc t :: Type
    t = let fs :: [Type]
    fs = Type -> [Type] -> [Type]
    splitMul Type
    t []
                  in ((Type, Maybe TVar) -> (Type, Maybe TVar) -> Ordering)
    -> [(Type, Maybe TVar)] -> [(Type, Maybe TVar)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (Type, Maybe TVar) -> (Type, Maybe TVar) -> Ordering
    forall a a a. Ord a => (a, Maybe a) -> (a, Maybe a) -> Ordering
    cmpFact ([Type] -> [Maybe TVar] -> [(Type, Maybe TVar)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Type]
    fs ((Type -> Maybe TVar) -> [Type] -> [Maybe TVar]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Maybe TVar
    cancelVar [Type]
    fs))

      splitMul :: Type -> [Type] -> [Type]
    splitMul t :: Type
    t rest :: [Type]
    rest = case Match (Type, Type) -> Maybe (Type, Type)
    forall a. Match a -> Maybe a
    matchMaybe (Pat Type (Type, Type)
    aMul Type
    t) of
                          Just (a :: Type
    a,b :: Type
    b) -> Type -> [Type] -> [Type]
    splitMul Type
    a (Type -> [Type] -> [Type]
    splitMul Type
    b [Type]
    rest)
                          Nothing    -> Type
    t Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    : [Type]
    rest

      cancelVar :: Type -> Maybe TVar
    cancelVar t :: Type
    t = Match TVar -> Maybe TVar
    forall a. Match a -> Maybe a
    matchMaybe (Match TVar -> Maybe TVar) -> Match TVar -> Maybe TVar
    forall a b. (a -> b) -> a -> b
    $ do TVar
    x <- Pat Type TVar
    aTVar Type
    t
                                    Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Interval -> Bool
    iIsPosFin (Ctxt -> TVar -> Interval
    tvarInterval Ctxt
    ctxt TVar
    x))
                                    TVar -> Match TVar
    forall (m :: * -> *) a. Monad m => a -> m a
    return TVar
    x

      -- cancellable variables go first, sorted alphabetically
      cmpFact :: (a, Maybe a) -> (a, Maybe a) -> Ordering
    cmpFact (_,mbA :: Maybe a
    mbA) (_,mbB :: Maybe a
    mbB) =
        case (Maybe a
    mbA,Maybe a
    mbB) of
          (Just x :: a
    x, Just y :: a
    y)  -> a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare a
    x a
    y
          (Just _, Nothing) -> Ordering
    LT
          (Nothing, Just _) -> Ordering
    GT
          _                 -> Ordering
    EQ

    -- min t1 t2 = t1 ~> t1 <= t2
    tryEqMin :: Type -> Type -> Match Solved
    tryEqMin :: Type -> Type -> Match Solved
    tryEqMin x :: Type
    x y :: Type
    y =
      do (a :: Type
    a,b :: Type
    b) <- Pat Type (Type, Type)
    aMin Type
    x
         let check :: Type -> Type -> m Solved
    check m1 :: Type
    m1 m2 :: Type
    m2 = do Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type
    m1 Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    y)
                              Solved -> m Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solved -> m Solved) -> Solved -> m Solved
    forall a b. (a -> b) -> a -> b
    $ [Type] -> Solved
    SolvedIf [ Type
    m2 Type -> Type -> Type
    >== Type
    m1 ]
         Type -> Type -> Match Solved
    forall (m :: * -> *).
    (Monad m, Alternative m) =>
    Type -> Type -> m Solved
    check Type
    a Type
    b Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Type -> Match Solved
    forall (m :: * -> *).
    (Monad m, Alternative m) =>
    Type -> Type -> m Solved
    check Type
    b Type
    a

    -- t1 == min (K + t1) t2 ~~> t1 == t2, if K >= 1
    -- (also if (K + t1) is one term in a multi-way min)
    tryEqMins :: Type -> Type -> Match Solved
    tryEqMins :: Type -> Type -> Match Solved
    tryEqMins x :: Type
    x y :: Type
    y =
      do (a :: Type
    a, b :: Type
    b) <- Pat Type (Type, Type)
    aMin Type
    y
         let ys :: [Type]
    ys = Type -> [Type]
    splitMin Type
    a [Type] -> [Type] -> [Type]
    forall a. [a] -> [a] -> [a]
    ++ Type -> [Type]
    splitMin Type
    b
         let ys' :: [Type]
    ys' = (Type -> Bool) -> [Type] -> [Type]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (Type -> Bool) -> Type -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Bool
    isGt) [Type]
    ys
         let y' :: Type
    y' = if [Type] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Type]
    ys' then Type
    tInf else (Type -> Type -> Type) -> [Type] -> Type
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 Type -> Type -> Type
    Simp.tMin [Type]
    ys'
         Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solved -> Match Solved) -> Solved -> Match Solved
    forall a b. (a -> b) -> a -> b
    $ if [Type] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type]
    ys' Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < [Type] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type]
    ys
                  then [Type] -> Solved
    SolvedIf [Type
    x Type -> Type -> Type
    =#= Type
    y']
                  else Solved
    Unsolved
      where
        splitMin :: Type -> [Type]
        splitMin :: Type -> [Type]
    splitMin ty :: Type
    ty =
          case Match (Type, Type) -> Maybe (Type, Type)
    forall a. Match a -> Maybe a
    matchMaybe (Pat Type (Type, Type)
    aMin Type
    ty) of
            Just (t1 :: Type
    t1, t2 :: Type
    t2) -> Type -> [Type]
    splitMin Type
    t1 [Type] -> [Type] -> [Type]
    forall a. [a] -> [a] -> [a]
    ++ Type -> [Type]
    splitMin Type
    t2
            Nothing       -> [Type
    ty]

        isGt :: Type -> Bool
        isGt :: Type -> Bool
    isGt t :: Type
    t =
          case Match (Integer, Type) -> Maybe (Integer, Type)
    forall a. Match a -> Maybe a
    matchMaybe (Type -> Match (Integer, Type)
    asAddK Type
    t) of
            Just (k :: Integer
    k, t' :: Type
    t') -> Integer
    k Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > 0 Bool -> Bool -> Bool
    && Type
    t' Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    x
            Nothing      -> Bool
    False

        asAddK :: Type -> Match (Integer, Type)
        asAddK :: Type -> Match (Integer, Type)
    asAddK t :: Type
    t =
          do (t1 :: Type
    t1, t2 :: Type
    t2) <- Pat Type (Type, Type)
    anAdd Type
    t
             Integer
    k <- Pat Type Integer
    aNat Type
    t1
             (Integer, Type) -> Match (Integer, Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    k, Type
    t2)

    tryEqVar :: Type -> TVar -> Match Solved
    tryEqVar :: Type -> TVar -> Match Solved
    tryEqVar ty :: Type
    ty x :: TVar
    x =

      -- a = K + a --> x = inf
      (do (k :: Integer
    k,tv :: TVar
    tv) <- Type
    -> (Pat Type (Type, Type), Pat Type Integer, Pat Type TVar)
    -> Match (Integer, TVar)
    forall thing pats res.
    Matches thing pats res =>
    thing -> pats -> Match res
    matches Type
    ty (Pat Type (Type, Type)
    anAdd, Pat Type Integer
    aNat, Pat Type TVar
    aTVar)
          Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (TVar
    tv TVar -> TVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TVar
    x Bool -> Bool -> Bool
    && Integer
    k Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 1)

          Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solved -> Match Solved) -> Solved -> Match Solved
    forall a b. (a -> b) -> a -> b
    $ [Type] -> Solved
    SolvedIf [ TVar -> Type
    TVar TVar
    x Type -> Type -> Type
    =#= Type
    tInf ]
      )
      Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>

      -- a = min (K + a) t --> a = t
      (do (l :: Type
    l,r :: Type
    r) <- Pat Type (Type, Type)
    aMin Type
    ty
          let check :: Type -> Type -> Match Solved
    check this :: Type
    this other :: Type
    other =
                do (k :: Nat'
    k,x' :: TVar
    x') <- Type
    -> (Pat Type (Type, Type), Pat Type Nat', Pat Type TVar)
    -> Match (Nat', TVar)
    forall thing pats res.
    Matches thing pats res =>
    thing -> pats -> Match res
    matches Type
    this (Pat Type (Type, Type)
    anAdd, Pat Type Nat'
    aNat', Pat Type TVar
    aTVar)
                   Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (TVar
    x TVar -> TVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TVar
    x' Bool -> Bool -> Bool
    && Nat'
    k Nat' -> Nat' -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer -> Nat'
    Nat 1)
                   Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solved -> Match Solved) -> Solved -> Match Solved
    forall a b. (a -> b) -> a -> b
    $ [Type] -> Solved
    SolvedIf [ TVar -> Type
    TVar TVar
    x Type -> Type -> Type
    =#= Type
    other ]
          Type -> Type -> Match Solved
    check Type
    l Type
    r Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Type -> Match Solved
    check Type
    r Type
    l
      )
      Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
      -- a = K + min t a
      (do (k :: Integer
    k,(l :: Type
    l,r :: Type
    r)) <- Type
    -> (Pat Type (Type, Type), Pat Type Integer, Pat Type (Type, Type))
    -> Match (Integer, (Type, Type))
    forall thing pats res.
    Matches thing pats res =>
    thing -> pats -> Match res
    matches Type
    ty (Pat Type (Type, Type)
    anAdd, Pat Type Integer
    aNat, Pat Type (Type, Type)
    aMin)
          Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Integer
    k Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 1)
          let check :: Type -> Type -> Match Solved
    check a :: Type
    a b :: Type
    b = do TVar
    x' <- Pat Type TVar
    aTVar Type
    a
                             Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (TVar
    x' TVar -> TVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TVar
    x)
                             Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type] -> Solved
    SolvedIf [ TVar -> Type
    TVar TVar
    x Type -> Type -> Type
    =#= Type -> Type -> Type
    tAdd (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    k) Type
    b ])
          Type -> Type -> Match Solved
    check Type
    l Type
    r Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Type -> Match Solved
    check Type
    r Type
    l
      )

    -- e.g., 10 = t
    tryEqK :: Ctxt -> Type -> Nat' -> Match Solved
    tryEqK :: Ctxt -> Type -> Nat' -> Match Solved
    tryEqK ctxt :: Ctxt
    ctxt ty :: Type
    ty lk :: Nat'
    lk =

      -- (t1 + t2 = inf, fin t1) ~~~> t2 = inf
      do Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Nat'
    lk Nat' -> Nat' -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat'
    Inf)
         (a :: Type
    a,b :: Type
    b) <- Pat Type (Type, Type)
    anAdd Type
    ty
         let check :: Type -> Type -> m Solved
    check x :: Type
    x y :: Type
    y = do Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Interval -> Bool
    iIsFin (Ctxt -> Type -> Interval
    typeInterval Ctxt
    ctxt Type
    x))
                            Solved -> m Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solved -> m Solved) -> Solved -> m Solved
    forall a b. (a -> b) -> a -> b
    $ [Type] -> Solved
    SolvedIf [ Type
    y Type -> Type -> Type
    =#= Type
    tInf ]
         Type -> Type -> Match Solved
    forall (m :: * -> *).
    (Monad m, Alternative m) =>
    Type -> Type -> m Solved
    check Type
    a Type
    b Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Type -> Match Solved
    forall (m :: * -> *).
    (Monad m, Alternative m) =>
    Type -> Type -> m Solved
    check Type
    b Type
    a
      Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>

      -- (K1 + t = K2, K2 >= K1) ~~~> t = (K2 - K1)
      do (rk :: Nat'
    rk, b :: Type
    b) <- Type
    -> (Pat Type (Type, Type), Pat Type Nat', Pat Type Type)
    -> Match (Nat', Type)
    forall thing pats res.
    Matches thing pats res =>
    thing -> pats -> Match res
    matches Type
    ty (Pat Type (Type, Type)
    anAdd, Pat Type Nat'
    aNat', Pat Type Type
    forall a. Pat a a
    __)
         Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solved -> Match Solved) -> Solved -> Match Solved
    forall a b. (a -> b) -> a -> b
    $
           case Nat' -> Nat' -> Maybe Nat'
    nSub Nat'
    lk Nat'
    rk of
             -- NOTE: (Inf - Inf) shouldn't be possible
             Nothing -> TCErrorMessage -> Solved
    Unsolvable
                          (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
    forall a b. (a -> b) -> a -> b
    $ String -> TCErrorMessage
    TCErrorMessage
                          (String -> TCErrorMessage) -> String -> TCErrorMessage
    forall a b. (a -> b) -> a -> b
    $ "Adding " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Nat' -> String
    showNat' Nat'
    rk String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " will always exceed "
                                      String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Nat' -> String
    showNat' Nat'
    lk

             Just r :: Nat'
    r -> [Type] -> Solved
    SolvedIf [ Type
    b Type -> Type -> Type
    =#= Nat' -> Type
    tNat' Nat'
    r ]
      Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>

      -- (lk = t - rk) ~~> t = lk + rk
      do (t :: Type
    t,rk :: Nat'
    rk) <- Type
    -> (Pat Type (Type, Type), Pat Type Type, Pat Type Nat')
    -> Match (Type, Nat')
    forall thing pats res.
    Matches thing pats res =>
    thing -> pats -> Match res
    matches Type
    ty (Pat Type (Type, Type)
    (|-|) , Pat Type Type
    forall a. Pat a a
    __, Pat Type Nat'
    aNat')
         Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type] -> Solved
    SolvedIf [ Type
    t Type -> Type -> Type
    =#= Nat' -> Type
    tNat' (Nat' -> Nat' -> Nat'
    nAdd Nat'
    lk Nat'
    rk) ])

      Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
      do (rk :: Nat'
    rk, b :: Type
    b) <- Type
    -> (Pat Type (Type, Type), Pat Type Nat', Pat Type Type)
    -> Match (Nat', Type)
    forall thing pats res.
    Matches thing pats res =>
    thing -> pats -> Match res
    matches Type
    ty (Pat Type (Type, Type)
    aMul, Pat Type Nat'
    aNat', Pat Type Type
    forall a. Pat a a
    __)
         Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solved -> Match Solved) -> Solved -> Match Solved
    forall a b. (a -> b) -> a -> b
    $
           case (Nat'
    lk,Nat'
    rk) of
             -- Inf * t = Inf ~~~>  t >= 1
             (Inf,Inf)    -> [Type] -> Solved
    SolvedIf [ Type
    b Type -> Type -> Type
    >== Type
    tOne ]

             -- K * t = Inf ~~~> t = Inf
             (Inf,Nat _)  -> [Type] -> Solved
    SolvedIf [ Type
    b Type -> Type -> Type
    =#= Type
    tInf ]

             -- Inf * t = 0 ~~~> t = 0
             (Nat 0, Inf) -> [Type] -> Solved
    SolvedIf [ Type
    b Type -> Type -> Type
    =#= Type
    tZero ]

             -- Inf * t = K ~~~> ERR      (K /= 0)
             (Nat k :: Integer
    k, Inf) -> TCErrorMessage -> Solved
    Unsolvable
                           (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
    forall a b. (a -> b) -> a -> b
    $ String -> TCErrorMessage
    TCErrorMessage
                           (String -> TCErrorMessage) -> String -> TCErrorMessage
    forall a b. (a -> b) -> a -> b
    $ Integer -> String
    forall a. Show a => a -> String
    show Integer
    k String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " != inf * anything"

             (Nat lk' :: Integer
    lk', Nat rk' :: Integer
    rk')
               -- 0 * t = K2 ~~> K2 = 0
               | Integer
    rk' Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0 -> [Type] -> Solved
    SolvedIf [ Nat' -> Type
    tNat' Nat'
    lk Type -> Type -> Type
    =#= Type
    tZero ]
                  -- shouldn't happen, as `0 * t = t` should have been simplified

               -- K1 * t = K2 ~~> t = K2/K1
               | (q :: Integer
    q,0) <- Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    divMod Integer
    lk' Integer
    rk' -> [Type] -> Solved
    SolvedIf [ Type
    b Type -> Type -> Type
    =#= Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    q ]
               | Bool
    otherwise ->
                   TCErrorMessage -> Solved
    Unsolvable
                 (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
    forall a b. (a -> b) -> a -> b
    $ String -> TCErrorMessage
    TCErrorMessage
                 (String -> TCErrorMessage) -> String -> TCErrorMessage
    forall a b. (a -> b) -> a -> b
    $ Nat' -> String
    showNat' Nat'
    lk String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " != " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Nat' -> String
    showNat' Nat'
    rk String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " * anything"

      Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
      -- K1 == K2 ^^ t    ~~> t = logBase K2 K1
      do (rk :: Integer
    rk, b :: Type
    b) <- Type
    -> (Pat Type (Type, Type), Pat Type Integer, Pat Type Type)
    -> Match (Integer, Type)
    forall thing pats res.
    Matches thing pats res =>
    thing -> pats -> Match res
    matches Type
    ty (Pat Type (Type, Type)
    (|^|), Pat Type Integer
    aNat, Pat Type Type
    forall a. Pat a a
    __)
         Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solved -> Match Solved) -> Solved -> Match Solved
    forall a b. (a -> b) -> a -> b
    $ case Nat'
    lk of
                    Inf | Integer
    rk Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > 1 -> [Type] -> Solved
    SolvedIf [ Type
    b Type -> Type -> Type
    =#= Type
    tInf ]
                    Nat n :: Integer
    n | Just (a :: Integer
    a,True) <- Integer -> Integer -> Maybe (Integer, Bool)
    genLog Integer
    n Integer
    rk -> [Type] -> Solved
    SolvedIf [ Type
    b Type -> Type -> Type
    =#= Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    a]
                    _ -> TCErrorMessage -> Solved
    Unsolvable (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
    forall a b. (a -> b) -> a -> b
    $ String -> TCErrorMessage
    TCErrorMessage
                           (String -> TCErrorMessage) -> String -> TCErrorMessage
    forall a b. (a -> b) -> a -> b
    $ Integer -> String
    forall a. Show a => a -> String
    show Integer
    rk String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " ^^ anything != " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Nat' -> String
    showNat' Nat'
    lk

      -- XXX: Min, Max, etx
      -- 2  = min (10,y)  --> y = 2
      -- 2  = min (2,y)   --> y >= 2
      -- 10 = min (2,y)   --> impossible

    -- | K1 * t1 + K2 * t2 + ... = K3 * t3 + K4 * t4 + ...
    tryEqMulConst :: Type -> Type -> Match Solved
    tryEqMulConst :: Type -> Type -> Match Solved
    tryEqMulConst l :: Type
    l r :: Type
    r =
      do (lc :: Integer
    lc,ls :: [(Integer, Type)]
    ls) <- Pat Type (Integer, [(Integer, Type)])
    matchLinear Type
    l
         (rc :: Integer
    rc,rs :: [(Integer, Type)]
    rs) <- Pat Type (Integer, [(Integer, Type)])
    matchLinear Type
    r
         let d :: Integer
    d = (Integer -> Integer -> Integer) -> [Integer] -> Integer
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    gcd (Integer
    lc Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    : Integer
    rc Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    : ((Integer, Type) -> Integer) -> [(Integer, Type)] -> [Integer]
    forall a b. (a -> b) -> [a] -> [b]
    map (Integer, Type) -> Integer
    forall a b. (a, b) -> a
    fst ([(Integer, Type)]
    ls [(Integer, Type)] -> [(Integer, Type)] -> [(Integer, Type)]
    forall a. [a] -> [a] -> [a]
    ++ [(Integer, Type)]
    rs))
         Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Integer
    d Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > 1)
         Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type] -> Solved
    SolvedIf [Integer -> Integer -> [(Integer, Type)] -> Type
    forall a. Integral a => a -> a -> [(a, Type)] -> Type
    build Integer
    d Integer
    lc [(Integer, Type)]
    ls Type -> Type -> Type
    =#= Integer -> Integer -> [(Integer, Type)] -> Type
    forall a. Integral a => a -> a -> [(a, Type)] -> Type
    build Integer
    d Integer
    rc [(Integer, Type)]
    rs])
      where
      build :: a -> a -> [(a, Type)] -> Type
    build d :: a
    d k :: a
    k ts :: [(a, Type)]
    ts   = (Type -> Type -> Type) -> Type -> [Type] -> Type
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Type -> Type -> Type
    tAdd (a -> a -> Type
    forall a. Integral a => a -> a -> Type
    cancel a
    d a
    k) (((a, Type) -> Type) -> [(a, Type)] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (a -> (a, Type) -> Type
    forall a. Integral a => a -> (a, Type) -> Type
    buildS a
    d) [(a, Type)]
    ts)
      buildS :: a -> (a, Type) -> Type
    buildS d :: a
    d (k :: a
    k,t :: Type
    t) = Type -> Type -> Type
    tMul (a -> a -> Type
    forall a. Integral a => a -> a -> Type
    cancel a
    d a
    k) Type
    t
      cancel :: a -> a -> Type
    cancel d :: a
    d x :: a
    x     = a -> Type
    forall a. Integral a => a -> Type
    tNum (a -> a -> a
    forall a. Integral a => a -> a -> a
    div a
    x a
    d)

    -- | @(t1 + t2 = Inf, fin t1)  ~~> t2 = Inf@
    tryEqAddInf :: Ctxt -> Type -> Type -> Match Solved
    tryEqAddInf :: Ctxt -> Type -> Type -> Match Solved
    tryEqAddInf ctxt :: Ctxt
    ctxt l :: Type
    l r :: Type
    r = Type -> Type -> Match Solved
    check Type
    l Type
    r Match Solved -> Match Solved -> Match Solved
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Type -> Type -> Match Solved
    check Type
    r Type
    l
      where

      -- check for x = a + b /\ x = inf
      check :: Type -> Type -> Match Solved
    check x :: Type
    x y :: Type
    y =
        do (x1 :: Type
    x1,x2 :: Type
    x2) <- Pat Type (Type, Type)
    anAdd Type
    x
           Pat Type ()
    aInf Type
    y

           let x1Fin :: Bool
    x1Fin = Interval -> Bool
    iIsFin (Ctxt -> Type -> Interval
    typeInterval Ctxt
    ctxt Type
    x1)
           let x2Fin :: Bool
    x2Fin = Interval -> Bool
    iIsFin (Ctxt -> Type -> Interval
    typeInterval Ctxt
    ctxt Type
    x2)

           Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solved -> Match Solved) -> Solved -> Match Solved
    forall a b. (a -> b) -> a -> b
    $!
             if | Bool
    x1Fin ->
                  [Type] -> Solved
    SolvedIf [ Type
    x2 Type -> Type -> Type
    =#= Type
    y ]

                | Bool
    x2Fin ->
                  [Type] -> Solved
    SolvedIf [ Type
    x1 Type -> Type -> Type
    =#= Type
    y ]

                | Bool
    otherwise ->
                  Solved
    Unsolved

    -- | Check for addition of constants to both sides of a relation.
    --  @((K1 + K2) + t1) `R` (K1 + t2)  ~~>   (K2 + t1) `R` t2@
    --
    -- This relies on the fact that constants are floated left during
    -- simplification.
    tryAddConst :: (Type -> Type -> Prop) -> Type -> Type -> Match Solved
    tryAddConst :: (Type -> Type -> Type) -> Type -> Type -> Match Solved
    tryAddConst rel :: Type -> Type -> Type
    rel l :: Type
    l r :: Type
    r =
      do (x1 :: Type
    x1,x2 :: Type
    x2) <- Pat Type (Type, Type)
    anAdd Type
    l
         (y1 :: Type
    y1,y2 :: Type
    y2) <- Pat Type (Type, Type)
    anAdd Type
    r

         Integer
    k1 <- Pat Type Integer
    aNat Type
    x1
         Integer
    k2 <- Pat Type Integer
    aNat Type
    y1

         if Integer
    k1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    k2
            then Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type] -> Solved
    SolvedIf [ Type -> Type -> Type
    tAdd (Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer
    k1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    k2)) Type
    x2 Type -> Type -> Type
    `rel` Type
    y2 ])
            else Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type] -> Solved
    SolvedIf [ Type
    x2 Type -> Type -> Type
    `rel` Type -> Type -> Type
    tAdd (Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Integer
    k2 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    k1)) Type
    y2 ])

    -- | Check for situations where a unification variable is involved in
    --   a sum of terms not containing additional unification variables,
    --   and replace it with a solution and an inequality.
    --   @s1 = ?a + s2 ~~> (?a = s1 - s2, s1 >= s2)@
    tryLinearSolution :: Type -> Type -> Match Solved
    tryLinearSolution :: Type -> Type -> Match Solved
    tryLinearSolution s1 :: Type
    s1 t :: Type
    t =
      do (a :: TVar
    a,xs :: [Type]
    xs) <- Pat Type (TVar, [Type])
    matchLinearUnifier Type
    t
         Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type -> Bool
    forall t. FVS t => t -> Bool
    noFreeVariables Type
    s1)

         -- NB: matchLinearUnifier only matches if xs is nonempty
         let s2 :: Type
    s2 = (Type -> Type -> Type) -> [Type] -> Type
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 Type -> Type -> Type
    Simp.tAdd [Type]
    xs
         Solved -> Match Solved
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Type] -> Solved
    SolvedIf [ TVar -> Type
    TVar TVar
    a Type -> Type -> Type
    =#= (Type -> Type -> Type
    Simp.tSub Type
    s1 Type
    s2), Type
    s1 Type -> Type -> Type
    >== Type
    s2 ])

    -- | Match a sum of the form @(s1 + ... + ?a + ... sn)@ where
    --   @s1@ through @sn@ do not contain any free variables.
    --
    --   Note: a successful match should only occur if @s1 ... sn@ is
    --   not empty.
    matchLinearUnifier :: Pat Type (TVar,[Type])
    matchLinearUnifier :: Pat Type (TVar, [Type])
    matchLinearUnifier = [Type] -> Pat Type (TVar, [Type])
    go []
     where
      go :: [Type] -> Pat Type (TVar, [Type])
    go xs :: [Type]
    xs t :: Type
    t =
        -- Case where a free variable occurs at the end of a sequence of additions.
        -- NB: match fails if @xs@ is empty
        do TVar
    v <- Pat Type TVar
    aFreeTVar Type
    t
           Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Bool
    not (Bool -> Bool) -> ([Type] -> Bool) -> [Type] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Type] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null ([Type] -> Bool) -> [Type] -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Type]
    xs)
           (TVar, [Type]) -> Match (TVar, [Type])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVar
    v, [Type]
    xs)
        Match (TVar, [Type])
    -> Match (TVar, [Type]) -> Match (TVar, [Type])
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
        -- Next symbol is an addition
        do (x :: Type
    x, y :: Type
    y) <- Pat Type (Type, Type)
    anAdd Type
    t

            -- Case where a free variable occurs in the middle of an expression
           (do TVar
    v <- Pat Type TVar
    aFreeTVar Type
    x
               Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type -> Bool
    forall t. FVS t => t -> Bool
    noFreeVariables Type
    y)
               (TVar, [Type]) -> Match (TVar, [Type])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVar
    v, [Type] -> [Type]
    forall a. [a] -> [a]
    reverse (Type
    yType -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[Type]
    xs))

            Match (TVar, [Type])
    -> Match (TVar, [Type]) -> Match (TVar, [Type])
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
             -- Non-free-variable recursive case
            do Bool -> Match ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type -> Bool
    forall t. FVS t => t -> Bool
    noFreeVariables Type
    x)
               [Type] -> Pat Type (TVar, [Type])
    go (Type
    xType -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[Type]
    xs) Type
    y)

    -- | Is this a sum of products, where the products have constant coefficients?
    matchLinear :: Pat Type (Integer, [(Integer,Type)])
    matchLinear :: Pat Type (Integer, [(Integer, Type)])
    matchLinear = (Integer, [(Integer, Type)])
    -> Pat Type (Integer, [(Integer, Type)])
    go (0, [])
      where
      go :: (Integer, [(Integer, Type)])
    -> Pat Type (Integer, [(Integer, Type)])
    go (c :: Integer
    c,ts :: [(Integer, Type)]
    ts) t :: Type
    t =
        do Integer
    n <- Pat Type Integer
    aNat Type
    t
           (Integer, [(Integer, Type)]) -> Match (Integer, [(Integer, Type)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    c, [(Integer, Type)]
    ts)
        Match (Integer, [(Integer, Type)])
    -> Match (Integer, [(Integer, Type)])
    -> Match (Integer, [(Integer, Type)])
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
        do (x :: Type
    x,y :: Type
    y) <- Pat Type (Type, Type)
    aMul Type
    t
           Integer
    n     <- Pat Type Integer
    aNat Type
    x
           (Integer, [(Integer, Type)]) -> Match (Integer, [(Integer, Type)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    c, (Integer
    n,Type
    y) (Integer, Type) -> [(Integer, Type)] -> [(Integer, Type)]
    forall a. a -> [a] -> [a]
    : [(Integer, Type)]
    ts)
        Match (Integer, [(Integer, Type)])
    -> Match (Integer, [(Integer, Type)])
    -> Match (Integer, [(Integer, Type)])
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
        do (l :: Type
    l,r :: Type
    r) <- Pat Type (Type, Type)
    anAdd Type
    t
           (c' :: Integer
    c',ts' :: [(Integer, Type)]
    ts') <- (Integer, [(Integer, Type)])
    -> Pat Type (Integer, [(Integer, Type)])
    go (Integer
    c,[(Integer, Type)]
    ts) Type
    l
           (Integer, [(Integer, Type)])
    -> Pat Type (Integer, [(Integer, Type)])
    go (Integer
    c',[(Integer, Type)]
    ts') Type
    r

    showNat' :: Nat' -> String
    showNat' :: Nat' -> String
    showNat' Inf = "inf"
    showNat' (Nat n :: Integer
    n) = Integer -> String
    forall a. Show a => a -> String
    show Integer
    n