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