    module Cryptol.TypeCheck.TypePat
      ( aInf, aNat, aNat'

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

      , aLiteral, aLogic

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

      , aFin, (|=|), (|/=|), (|>=|)
      , aCmp, aArith

      , 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.TypeCheck.Type
    import Cryptol.TypeCheck.Solver.InfNat

    tcon :: TCon -> ([Type] -> a) -> Pat Type a
    tcon :: TCon -> ([Type] -> a) -> Pat Type a
    tcon f :: TCon
    f p :: [Type] -> a
    p = \ty :: Type
    ty -> case Type -> Type
    tNoUser Type
    ty of
                        TCon c :: TCon
    c ts :: [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)
                        _                  -> 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
    a

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

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

    tf :: TFun -> ([Type] -> a) -> Pat Type a
    tf :: TFun -> ([Type] -> a) -> Pat Type a
    tf f :: TFun
    f ar :: [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 f :: TC
    f ar :: [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 f :: PC
    f ar :: [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 = \a :: Type
    a -> case Type -> Type
    tNoUser Type
    a of
                   TCon (TC (TCNum n :: Integer
    n)) _ -> Integer -> Match Integer
    forall (m :: * -> *) a. Monad m => a -> m a
    return Integer
    n
                   _                     -> Match Integer
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    aNat' :: Pat Type Nat'
    aNat' :: Pat Type Nat'
    aNat' = \a :: 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 = \a :: Type
    a -> case Type -> Type
    tNoUser Type
    a of
                    TVar x :: TVar
    x -> TVar -> Match TVar
    forall (m :: * -> *) a. Monad m => a -> m a
    return TVar
    x
                    _      -> Match TVar
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    aFreeTVar :: Pat Type TVar
    aFreeTVar :: Pat Type TVar
    aFreeTVar t :: 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 = \a :: Type
    a -> do (l :: Type
    l,t :: 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 = \a :: Type
    a -> do (l :: Type
    l,t :: 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
    == 8)
                     Pat Type ()
    aBit Type
    t

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

    aRec :: Pat Type [(Ident, Type)]
    aRec :: Pat Type [(Ident, Type)]
    aRec = \a :: Type
    a -> case Type -> Type
    tNoUser Type
    a of
                   TRec fs :: [(Ident, Type)]
    fs -> [(Ident, Type)] -> Match [(Ident, Type)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Ident, Type)]
    fs
                   _       -> Match [(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

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

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

    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

    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 TCErrorMessage
    anError :: Kind -> Pat Type TCErrorMessage
    anError k :: Kind
    k = \a :: Type
    a -> case Type -> Type
    tNoUser Type
    a of
                        TCon (TError k1 :: Kind
    k1 err :: TCErrorMessage
    err) _ | Kind
    k Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    k1 -> TCErrorMessage -> Match TCErrorMessage
    forall (m :: * -> *) a. Monad m => a -> m a
    return TCErrorMessage
    err
                        _                     -> Match TCErrorMessage
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero