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