{-# 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
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
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)
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
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 ])))
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) =
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 ]
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) =
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) ]
tryGeqThanSub :: Ctxt -> Type -> Type -> Match Solved
tryGeqThanSub :: Ctxt -> Type -> Type -> Match Solved
tryGeqThanSub _ x :: Type
x y :: Type
y =
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 =
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
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
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
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
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
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
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 =
(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
<|>
(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
<|>
(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
)
tryEqK :: Ctxt -> Type -> Nat' -> Match Solved
tryEqK :: Ctxt -> Type -> Nat' -> Match Solved
tryEqK ctxt :: Ctxt
ctxt ty :: Type
ty lk :: Nat'
lk =
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
<|>
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
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
<|>
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,Inf) -> [Type] -> Solved
SolvedIf [ Type
b Type -> Type -> Type
>== Type
tOne ]
(Inf,Nat _) -> [Type] -> Solved
SolvedIf [ Type
b Type -> Type -> Type
=#= Type
tInf ]
(Nat 0, Inf) -> [Type] -> Solved
SolvedIf [ Type
b Type -> Type -> Type
=#= Type
tZero ]
(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')
| 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 ]
| (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
<|>
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
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)
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 :: 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
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 ])
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)
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 ])
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 =
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
<|>
do (x :: Type
x, y :: Type
y) <- Pat Type (Type, Type)
anAdd Type
t
(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
<|>
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)
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