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

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

  , aLiteral
  , aLiteralLessThan
  , aLogic

  , aTVar
  , aFreeTVar
  , 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 :: 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 TCon -> TCon -> Bool
forall a. Eq a => a -> a -> Bool
== TCon
c -> a -> Match a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> a
p [Type]
ts)
                    Type
_                  -> Match a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

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

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

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

ar3 :: [a] -> (a,a,a)
ar3 :: [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 :: TFun -> ([Type] -> a) -> Pat Type a
tf TFun
f [Type] -> a
ar = TCon -> ([Type] -> a) -> Pat Type a
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 :: TC -> ([Type] -> a) -> Pat Type a
tc TC
f [Type] -> a
ar = TCon -> ([Type] -> a) -> Pat Type a
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 :: PC -> ([Type] -> a) -> Pat Type a
tp PC
f [Type] -> a
ar = TCon -> ([Type] -> a) -> Pat Type a
forall a. TCon -> ([Type] -> a) -> Pat Type a
tcon (PC -> TCon
PC PC
f) [Type] -> a
ar


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

aInf :: Pat Type ()
aInf :: Pat Type ()
aInf = TC -> ([Type] -> ()) -> Pat Type ()
forall a. TC -> ([Type] -> a) -> Pat Type a
tc TC
TCInf [Type] -> ()
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]
_ -> Integer -> Match Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
n
               Type
_                     -> Match Integer
forall (m :: * -> *) a. MonadPlus m => m a
mzero

aNat' :: Pat Type Nat'
aNat' :: Pat Type Nat'
aNat' = \Type
a -> (Nat'
Inf Nat' -> Match () -> Match Nat'
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$  Pat Type ()
aInf Type
a)
          Match Nat' -> Match Nat' -> Match Nat'
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Integer -> Nat'
Nat (Integer -> Nat') -> Match Integer -> Match 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 = TFun -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
TCAdd [Type] -> (Type, Type)
forall a. [a] -> (a, a)
ar2

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

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

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

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

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

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

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

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

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

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

aLenFromThenTo :: Pat Type (Type,Type,Type)
aLenFromThenTo :: Pat Type (Type, Type, Type)
aLenFromThenTo = TFun
-> ([Type] -> (Type, Type, Type)) -> Pat Type (Type, Type, Type)
forall a. TFun -> ([Type] -> a) -> Pat Type a
tf TFun
TCLenFromThenTo [Type] -> (Type, Type, Type)
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 -> TVar -> Match TVar
forall (m :: * -> *) a. Monad m => a -> m a
return TVar
x
                Type
_      -> Match TVar
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
     Bool -> Match ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TVar -> Bool
isFreeTV TVar
v)
     TVar -> Match TVar
forall (m :: * -> *) a. Monad m => a -> m a
return TVar
v

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

aSeq :: Pat Type (Type,Type)
aSeq :: Pat Type (Type, Type)
aSeq = TC -> ([Type] -> (Type, Type)) -> Pat Type (Type, Type)
forall a. TC -> ([Type] -> a) -> Pat Type a
tc TC
TCSeq [Type] -> (Type, Type)
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
                 Pat Type Type
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
                 Bool -> Match ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
n Integer -> Integer -> Bool
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 -> [Type] -> Match [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
ts
                 Type
_                        -> Match [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 -> RecordMap Ident Type -> Match (RecordMap Ident Type)
forall (m :: * -> *) a. Monad m => a -> m a
return RecordMap Ident Type
fs
               Type
_       -> Match (RecordMap Ident Type)
forall (m :: * -> *) a. MonadPlus m => m a
mzero

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

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

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

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

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

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

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

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

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

aLogic :: Pat Prop Type
aLogic :: Pat Type Type
aLogic = PC -> ([Type] -> Type) -> Pat Type Type
forall a. PC -> ([Type] -> a) -> Pat Type a
tp PC
PLogic [Type] -> Type
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 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k1 -> () -> Match ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                    Type
_                                     -> Match ()
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.
-}