-- See Note [-Wincomplete-uni-patterns and irrefutable patterns]
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.TypePat
  ( aInf, aNat, aNat'

  , anAdd, (|-|), aMul, (|^|), (|/|), (|%|)
  , aMin, aMax
  , aWidth
  , aCeilDiv, aCeilMod
  , aLenFromThenTo

  , aLiteral
  , aLiteralLessThan
  , aLogic

  , aTVar
  , aFreeTVar
  , anAbstractType
  , aBit
  , aSeq
  , aWord
  , aChar
  , aTuple
  , aRec
  , (|->|)

  , aFin, (|=|), (|/=|), (|>=|)
  , aAnd
  , aTrue

  , anError

  , module Cryptol.Utils.Patterns
  ) where

import Control.Applicative((<|>))
import Control.Monad
import Cryptol.Utils.Ident (Ident)
import Cryptol.Utils.Patterns
import Cryptol.Utils.RecordMap
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.Solver.InfNat


tcon :: TCon -> ([Type] -> a) -> Pat Type a
tcon :: forall a. TCon -> ([Type] -> a) -> Pat Type a
tcon TCon
f [Type] -> a
p = \Type
ty -> case Type -> Type
tNoUser Type
ty of
                    TCon TCon
c [Type]
ts | TCon
f forall a. Eq a => a -> a -> Bool
== TCon
c -> forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> a
p [Type]
ts)
                    Type
_                  -> forall (m :: * -> *) a. MonadPlus m => m a
mzero

ar0 :: [a] -> ()
ar0 :: forall a. [a] -> ()
ar0 ~[] = ()

ar1 :: [a] -> a
ar1 :: forall a. [a] -> a
ar1 ~[a
a] = a
a

ar2 :: [a] -> (a,a)
ar2 :: forall a. [a] -> (a, a)
ar2 ~[a
a,a
b] = (a
a,a
b)

ar3 :: [a] -> (a,a,a)
ar3 :: forall a. [a] -> (a, a, a)
ar3 ~[a
a,a
b,a
c] = (a
a,a
b,a
c)

tf :: TFun -> ([Type] -> a) -> Pat Type a
tf :: forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
f [Type] -> a
ar = forall a. TCon -> ([Type] -> a) -> Pat Type a
tcon (TFun -> TCon
TF TFun
f) [Type] -> a
ar

tc :: TC -> ([Type] -> a) -> Pat Type a
tc :: forall a. TC -> ([Type] -> a) -> Pat Type a
tc TC
f [Type] -> a
ar = forall a. TCon -> ([Type] -> a) -> Pat Type a
tcon (TC -> TCon
TC TC
f) [Type] -> a
ar

tp :: PC -> ([Type] -> a) -> Pat Prop a
tp :: forall a. PC -> ([Type] -> a) -> Pat Type a
tp PC
f [Type] -> a
ar = forall a. TCon -> ([Type] -> a) -> Pat Type a
tcon (PC -> TCon
PC PC
f) [Type] -> a
ar


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

aInf :: Pat Type ()
aInf :: Pat Type ()
aInf = forall a. TC -> ([Type] -> a) -> Pat Type a
tc TC
TCInf forall a. [a] -> ()
ar0

aNat :: Pat Type Integer
aNat :: Pat Type Integer
aNat = \Type
a -> case Type -> Type
tNoUser Type
a of
               TCon (TC (TCNum Integer
n)) [Type]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Integer
n
               Type
_                     -> forall (m :: * -> *) a. MonadPlus m => m a
mzero

aNat' :: Pat Type Nat'
aNat' :: Pat Type Nat'
aNat' = \Type
a -> (Nat'
Inf forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$  Pat Type ()
aInf Type
a)
          forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Integer -> Nat'
Nat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pat Type Integer
aNat Type
a)

anAdd :: Pat Type (Type,Type)
anAdd :: Pat Type (Type, Type)
anAdd = forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
TCAdd forall a. [a] -> (a, a)
ar2

(|-|) :: Pat Type (Type,Type)
|-| :: Pat Type (Type, Type)
(|-|) = forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
TCSub forall a. [a] -> (a, a)
ar2

aMul :: Pat Type (Type,Type)
aMul :: Pat Type (Type, Type)
aMul = forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
TCMul forall a. [a] -> (a, a)
ar2

(|^|) :: Pat Type (Type,Type)
|^| :: Pat Type (Type, Type)
(|^|) = forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
TCExp forall a. [a] -> (a, a)
ar2

(|/|) :: Pat Type (Type,Type)
|/| :: Pat Type (Type, Type)
(|/|) = forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
TCDiv forall a. [a] -> (a, a)
ar2

(|%|) :: Pat Type (Type,Type)
|%| :: Pat Type (Type, Type)
(|%|) = forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
TCMod forall a. [a] -> (a, a)
ar2

aMin :: Pat Type (Type,Type)
aMin :: Pat Type (Type, Type)
aMin = forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
TCMin forall a. [a] -> (a, a)
ar2

aMax :: Pat Type (Type,Type)
aMax :: Pat Type (Type, Type)
aMax = forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
TCMax forall a. [a] -> (a, a)
ar2

aWidth :: Pat Type Type
aWidth :: Pat Type Type
aWidth = forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
TCWidth forall a. [a] -> a
ar1

aCeilDiv :: Pat Type (Type,Type)
aCeilDiv :: Pat Type (Type, Type)
aCeilDiv = forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
TCCeilDiv forall a. [a] -> (a, a)
ar2

aCeilMod :: Pat Type (Type,Type)
aCeilMod :: Pat Type (Type, Type)
aCeilMod = forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
TCCeilMod forall a. [a] -> (a, a)
ar2

aLenFromThenTo :: Pat Type (Type,Type,Type)
aLenFromThenTo :: Pat Type (Type, Type, Type)
aLenFromThenTo = forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
TCLenFromThenTo forall a. [a] -> (a, a, a)
ar3

--------------------------------------------------------------------------------
aTVar :: Pat Type TVar
aTVar :: Pat Type TVar
aTVar = \Type
a -> case Type -> Type
tNoUser Type
a of
                TVar TVar
x -> forall (m :: * -> *) a. Monad m => a -> m a
return TVar
x
                Type
_      -> forall (m :: * -> *) a. MonadPlus m => m a
mzero

anAbstractType :: Pat Type UserTC
anAbstractType :: Pat Type UserTC
anAbstractType = \Type
a -> case Type -> Type
tNoUser Type
a of
                         TCon (TC (TCAbstract UserTC
ut)) [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure UserTC
ut
                         Type
_                            -> forall (m :: * -> *) a. MonadPlus m => m a
mzero

aFreeTVar :: Pat Type TVar
aFreeTVar :: Pat Type TVar
aFreeTVar Type
t =
  do TVar
v <- Pat Type TVar
aTVar Type
t
     forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TVar -> Bool
isFreeTV TVar
v)
     forall (m :: * -> *) a. Monad m => a -> m a
return TVar
v

aBit :: Pat Type ()
aBit :: Pat Type ()
aBit = forall a. TC -> ([Type] -> a) -> Pat Type a
tc TC
TCBit forall a. [a] -> ()
ar0

aSeq :: Pat Type (Type,Type)
aSeq :: Pat Type (Type, Type)
aSeq = forall a. TC -> ([Type] -> a) -> Pat Type a
tc TC
TCSeq forall a. [a] -> (a, a)
ar2

aWord :: Pat Type Type
aWord :: Pat Type Type
aWord = \Type
a -> do (Type
l,Type
t) <- Pat Type (Type, Type)
aSeq Type
a
                 Pat Type ()
aBit Type
t
                 forall (m :: * -> *) a. Monad m => a -> m a
return Type
l

aChar :: Pat Type ()
aChar :: Pat Type ()
aChar = \Type
a -> do (Type
l,Type
t) <- Pat Type (Type, Type)
aSeq Type
a
                 Integer
n     <- Pat Type Integer
aNat Type
l
                 forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
n forall a. Eq a => a -> a -> Bool
== Integer
8)
                 Pat Type ()
aBit Type
t

aTuple :: Pat Type [Type]
aTuple :: Pat Type [Type]
aTuple = \Type
a -> case Type -> Type
tNoUser Type
a of
                 TCon (TC (TCTuple Int
_)) [Type]
ts -> forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
ts
                 Type
_                        -> forall (m :: * -> *) a. MonadPlus m => m a
mzero

aRec :: Pat Type (RecordMap Ident Type)
aRec :: Pat Type (RecordMap Ident Type)
aRec = \Type
a -> case Type -> Type
tNoUser Type
a of
               TRec RecordMap Ident Type
fs -> forall (m :: * -> *) a. Monad m => a -> m a
return RecordMap Ident Type
fs
               Type
_       -> forall (m :: * -> *) a. MonadPlus m => m a
mzero

(|->|) :: Pat Type (Type,Type)
|->| :: Pat Type (Type, Type)
(|->|) = forall a. TC -> ([Type] -> a) -> Pat Type a
tc TC
TCFun forall a. [a] -> (a, a)
ar2
--------------------------------------------------------------------------------

aFin :: Pat Prop Type
aFin :: Pat Type Type
aFin = forall a. PC -> ([Type] -> a) -> Pat Type a
tp PC
PFin forall a. [a] -> a
ar1

(|=|) :: Pat Prop (Type,Type)
|=| :: Pat Type (Type, Type)
(|=|) = forall a. PC -> ([Type] -> a) -> Pat Type a
tp PC
PEqual forall a. [a] -> (a, a)
ar2

(|/=|) :: Pat Prop (Type,Type)
|/=| :: Pat Type (Type, Type)
(|/=|) = forall a. PC -> ([Type] -> a) -> Pat Type a
tp PC
PNeq forall a. [a] -> (a, a)
ar2

(|>=|) :: Pat Prop (Type,Type)
|>=| :: Pat Type (Type, Type)
(|>=|) = forall a. PC -> ([Type] -> a) -> Pat Type a
tp PC
PGeq forall a. [a] -> (a, a)
ar2

aAnd :: Pat Prop (Prop,Prop)
aAnd :: Pat Type (Type, Type)
aAnd = forall a. PC -> ([Type] -> a) -> Pat Type a
tp PC
PAnd forall a. [a] -> (a, a)
ar2

aTrue :: Pat Prop ()
aTrue :: Pat Type ()
aTrue = forall a. PC -> ([Type] -> a) -> Pat Type a
tp PC
PTrue forall a. [a] -> ()
ar0

aLiteral :: Pat Prop (Type,Type)
aLiteral :: Pat Type (Type, Type)
aLiteral = forall a. PC -> ([Type] -> a) -> Pat Type a
tp PC
PLiteral forall a. [a] -> (a, a)
ar2

aLiteralLessThan :: Pat Prop (Type,Type)
aLiteralLessThan :: Pat Type (Type, Type)
aLiteralLessThan = forall a. PC -> ([Type] -> a) -> Pat Type a
tp PC
PLiteralLessThan forall a. [a] -> (a, a)
ar2

aLogic :: Pat Prop Type
aLogic :: Pat Type Type
aLogic = forall a. PC -> ([Type] -> a) -> Pat Type a
tp PC
PLogic forall a. [a] -> a
ar1

--------------------------------------------------------------------------------
anError :: Kind -> Pat Type ()
anError :: Kind -> Pat Type ()
anError Kind
k = \Type
a -> case Type -> Type
tNoUser Type
a of
                    TCon (TError (Kind
_ :-> Kind
k1) ) [Type]
_ | Kind
k forall a. Eq a => a -> a -> Bool
== Kind
k1 -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
                    Type
_                                     -> forall (m :: * -> *) a. MonadPlus m => m a
mzero


{-
Note [-Wincomplete-uni-patterns and irrefutable patterns]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Various parts of Cryptol use irrefutable patterns in functions that assume that
their arguments have particular shapes. For example, the `ar1 ~[a] = a`
function in this module uses an irrefutable pattern because it assumes the
invariant that the argument list will have exactly one element. This lets ar1
be slightly lazier when evaluated.

Unfortunately, this use of irrefutable patterns is at odds with the
-Wincomplete-uni-patterns warning. At present, -Wincomplete-uni-patterns will
produce a warning for any irrefutable pattern that does not cover all possible
data constructors. While we could rewrite functions like `ar1` to explicitly
provide a fall-through case, that would change its strictness properties. As
a result, we simply disable -Wincomplete-uni-patterns warnings in each part
of Cryptol that uses irrefutable patterns.

Arguably, -Wincomplete-uni-patterns shouldn't be producing warnings for
irrefutable patterns at all. GHC issue #14800
(https://gitlab.haskell.org/ghc/ghc/-/issues/14800) proposes this idea.
If that issue is fixed in the future, we may want to reconsider whether we want
to disable -Wincomplete-uni-patterns.
-}