content: -- 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
    , aBit
    , aSeq
    , aWord
    , aChar
    , aTuple
    , aRec
    , (|->|)
  
    , aFin, aPrime, (|=|), (|/=|), (|>=|)
    , 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 f p = \ty -> case tNoUser ty of
                      TCon c ts | f == c -> return (p ts)
                      _                  -> mzero
  
  ar0 :: [a] -> ()
  ar0 ~[] = ()
  
  ar1 :: [a] -> a
  ar1 ~[a] = a
  
  ar2 :: [a] -> (a,a)
  ar2 ~[a,b] = (a,b)
  
  ar3 :: [a] -> (a,a,a)
  ar3 ~[a,b,c] = (a,b,c)
  
  tf :: TFun -> ([Type] -> a) -> Pat Type a
  tf f ar = tcon (TF f) ar
  
  tc :: TC -> ([Type] -> a) -> Pat Type a
  tc f ar = tcon (TC f) ar
  
  tp :: PC -> ([Type] -> a) -> Pat Prop a
  tp f ar = tcon (PC f) ar
  
  
  --------------------------------------------------------------------------------
  
  aInf :: Pat Type ()
  aInf = tc TCInf ar0
  
  aNat :: Pat Type Integer
  aNat = \a -> case tNoUser a of
                 TCon (TC (TCNum n)) _ -> return n
                 _                     -> mzero
  
  aNat' :: Pat Type Nat'
  aNat' = \a -> (Inf <$  aInf a)
            <|> (Nat <$> aNat a)
  
  anAdd :: Pat Type (Type,Type)
  anAdd = tf TCAdd ar2
  
  (|-|) :: Pat Type (Type,Type)
  (|-|) = tf TCSub ar2
  
  aMul :: Pat Type (Type,Type)
  aMul = tf TCMul ar2
  
  (|^|) :: Pat Type (Type,Type)
  (|^|) = tf TCExp ar2
  
  (|/|) :: Pat Type (Type,Type)
  (|/|) = tf TCDiv ar2
  
  (|%|) :: Pat Type (Type,Type)
  (|%|) = tf TCMod ar2
  
  aMin :: Pat Type (Type,Type)
  aMin = tf TCMin ar2
  
  aMax :: Pat Type (Type,Type)
  aMax = tf TCMax ar2
  
  aWidth :: Pat Type Type
  aWidth = tf TCWidth ar1
  
  aCeilDiv :: Pat Type (Type,Type)
  aCeilDiv = tf TCCeilDiv ar2
  
  aCeilMod :: Pat Type (Type,Type)
  aCeilMod = tf TCCeilMod ar2
  
  aLenFromThenTo :: Pat Type (Type,Type,Type)
  aLenFromThenTo = tf TCLenFromThenTo ar3
  
  --------------------------------------------------------------------------------
  aTVar :: Pat Type TVar
  aTVar = \a -> case tNoUser a of
                  TVar x -> return x
                  _      -> mzero
  
  aFreeTVar :: Pat Type TVar
  aFreeTVar t =
    do v <- aTVar t
       guard (isFreeTV v)
       return v
  
  aBit :: Pat Type ()
  aBit = tc TCBit ar0
  
  aSeq :: Pat Type (Type,Type)
  aSeq = tc TCSeq ar2
  
  aWord :: Pat Type Type
  aWord = \a -> do (l,t) <- aSeq a
                   aBit t
                   return l
  
  aChar :: Pat Type ()
  aChar = \a -> do (l,t) <- aSeq a
                   n     <- aNat l
                   guard (n == 8)
                   aBit t
  
  aTuple :: Pat Type [Type]
  aTuple = \a -> case tNoUser a of
                   TCon (TC (TCTuple _)) ts -> return ts
                   _                        -> mzero
  
  aRec :: Pat Type (RecordMap Ident Type)
  aRec = \a -> case tNoUser a of
                 TRec fs -> return fs
                 _       -> mzero
  
  (|->|) :: Pat Type (Type,Type)
  (|->|) = tc TCFun ar2
  --------------------------------------------------------------------------------
  
  aFin :: Pat Prop Type
  aFin = tp PFin ar1
  
  aPrime :: Pat Prop Type
  aPrime = tp PPrime ar1
  
  (|=|) :: Pat Prop (Type,Type)
  (|=|) = tp PEqual ar2
  
  (|/=|) :: Pat Prop (Type,Type)
  (|/=|) = tp PNeq ar2
  
  (|>=|) :: Pat Prop (Type,Type)
  (|>=|) = tp PGeq ar2
  
  aAnd :: Pat Prop (Prop,Prop)
  aAnd = tp PAnd ar2
  
  aTrue :: Pat Prop ()
  aTrue = tp PTrue ar0
  
  aLiteral :: Pat Prop (Type,Type)
  aLiteral = tp PLiteral ar2
  
  aLiteralLessThan :: Pat Prop (Type,Type)
  aLiteralLessThan = tp PLiteralLessThan ar2
  
  aLogic :: Pat Prop Type
  aLogic = tp PLogic ar1
  
  --------------------------------------------------------------------------------
  anError :: Kind -> Pat Type ()
  anError k = \a -> case tNoUser a of
                      TCon (TError (_ :-> k1) ) _ | k == k1 -> return ()
                      _                                     -> 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.
  -}
  