{-# LANGUAGE PatternGuards, OverloadedStrings #-}
module Cryptol.TypeCheck.Solver.Class
( classStep
, solveZeroInst
, solveLogicInst
, solveArithInst
, solveCmpInst
, solveSignedCmpInst
, solveLiteralInst
, expandProp
) where
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.SimpType (tAdd,tWidth)
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.PP
classStep :: Prop -> Solved
classStep :: Prop -> Solved
classStep p :: Prop
p = case Prop -> Prop
tNoUser Prop
p of
TCon (PC PLogic) [ty :: Prop
ty] -> Prop -> Solved
solveLogicInst (Prop -> Prop
tNoUser Prop
ty)
TCon (PC PArith) [ty :: Prop
ty] -> Prop -> Solved
solveArithInst (Prop -> Prop
tNoUser Prop
ty)
TCon (PC PCmp) [ty :: Prop
ty] -> Prop -> Solved
solveCmpInst (Prop -> Prop
tNoUser Prop
ty)
_ -> Solved
Unsolved
solveZeroInst :: Type -> Solved
solveZeroInst :: Prop -> Solved
solveZeroInst ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TError _ e :: TCErrorMessage
e) _ -> TCErrorMessage -> Solved
Unsolvable TCErrorMessage
e
TCon (TC TCBit) [] -> [Prop] -> Solved
SolvedIf []
TCon (TC TCInteger) [] -> [Prop] -> Solved
SolvedIf []
TCon (TC TCIntMod) [n :: Prop
n] -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
n, Prop
n Prop -> Prop -> Prop
>== Prop
tOne ]
TCon (TC TCSeq) [_, a :: Prop
a] -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pZero Prop
a ]
TCon (TC TCFun) [_, b :: Prop
b] -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pZero Prop
b ]
TCon (TC (TCTuple _)) es :: [Prop]
es -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pZero Prop
e | Prop
e <- [Prop]
es ]
TRec fs :: [(Ident, Prop)]
fs -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pZero Prop
ety | (_,ety :: Prop
ety) <- [(Ident, Prop)]
fs ]
_ -> Solved
Unsolved
solveLogicInst :: Type -> Solved
solveLogicInst :: Prop -> Solved
solveLogicInst ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TError _ e :: TCErrorMessage
e) _ -> TCErrorMessage -> Solved
Unsolvable TCErrorMessage
e
TCon (TC TCBit) [] -> [Prop] -> Solved
SolvedIf []
TCon (TC TCSeq) [_, a :: Prop
a] -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pLogic Prop
a ]
TCon (TC TCFun) [_, b :: Prop
b] -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pLogic Prop
b ]
TCon (TC (TCTuple _)) es :: [Prop]
es -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pLogic Prop
e | Prop
e <- [Prop]
es ]
TRec fs :: [(Ident, Prop)]
fs -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pLogic Prop
ety | (_,ety :: Prop
ety) <- [(Ident, Prop)]
fs ]
_ -> Solved
Unsolved
solveArithInst :: Type -> Solved
solveArithInst :: Prop -> Solved
solveArithInst ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TError _ e :: TCErrorMessage
e) _ -> TCErrorMessage -> Solved
Unsolvable TCErrorMessage
e
TCon (TC TCSeq) [n :: Prop
n, e :: Prop
e] -> Prop -> Prop -> Solved
solveArithSeq Prop
n Prop
e
TCon (TC TCFun) [_,b :: Prop
b] -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pArith Prop
b ]
TCon (TC (TCTuple _)) es :: [Prop]
es -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pArith Prop
e | Prop
e <- [Prop]
es ]
TCon (TC TCBit) [] ->
TCErrorMessage -> Solved
Unsolvable (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "Arithmetic cannot be done on individual bits."
TCon (TC TCInteger) [] -> [Prop] -> Solved
SolvedIf []
TCon (TC TCIntMod) [n :: Prop
n] -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
n, Prop
n Prop -> Prop -> Prop
>== Prop
tOne ]
TRec fs :: [(Ident, Prop)]
fs -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pArith Prop
ety | (_,ety :: Prop
ety) <- [(Ident, Prop)]
fs ]
_ -> Solved
Unsolved
solveArithSeq :: Type -> Type -> Solved
solveArithSeq :: Prop -> Prop -> Solved
solveArithSeq n :: Prop
n ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TC TCBit) [] -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
n ]
TVar {} -> case Prop -> Prop
tNoUser Prop
n of
TCon (TC TCInf) [] -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pArith Prop
ty ]
_ -> Solved
Unsolved
_ -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pArith Prop
ty ]
solveCmpInst :: Type -> Solved
solveCmpInst :: Prop -> Solved
solveCmpInst ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TError _ e :: TCErrorMessage
e) _ -> TCErrorMessage -> Solved
Unsolvable TCErrorMessage
e
TCon (TC TCBit) [] -> [Prop] -> Solved
SolvedIf []
TCon (TC TCInteger) [] -> [Prop] -> Solved
SolvedIf []
TCon (TC TCIntMod) [n :: Prop
n] -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
n, Prop
n Prop -> Prop -> Prop
>== Prop
tOne ]
TCon (TC TCSeq) [n :: Prop
n,a :: Prop
a] -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
n, Prop -> Prop
pCmp Prop
a ]
TCon (TC (TCTuple _)) es :: [Prop]
es -> [Prop] -> Solved
SolvedIf ((Prop -> Prop) -> [Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Prop
pCmp [Prop]
es)
TCon (TC TCFun) [_,_] ->
TCErrorMessage -> Solved
Unsolvable (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "Comparisons may not be performed on functions."
TRec fs :: [(Ident, Prop)]
fs -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pCmp Prop
e | (_,e :: Prop
e) <- [(Ident, Prop)]
fs ]
_ -> Solved
Unsolved
solveSignedCmpSeq :: Type -> Type -> Solved
solveSignedCmpSeq :: Prop -> Prop -> Solved
solveSignedCmpSeq n :: Prop
n ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TC TCBit) [] -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
n, Prop
n Prop -> Prop -> Prop
>== Integer -> Prop
forall a. Integral a => a -> Prop
tNum (1 :: Integer) ]
TVar {} -> Solved
Unsolved
_ -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
n, Prop -> Prop
pSignedCmp Prop
ty ]
solveSignedCmpInst :: Type -> Solved
solveSignedCmpInst :: Prop -> Solved
solveSignedCmpInst ty :: Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
TCon (TError _ e :: TCErrorMessage
e) _ -> TCErrorMessage -> Solved
Unsolvable TCErrorMessage
e
TCon (TC TCBit) [] -> TCErrorMessage -> Solved
Unsolvable (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "Signed comparisons may not be performed on bits"
TCon (TC TCSeq) [n :: Prop
n,a :: Prop
a] -> Prop -> Prop -> Solved
solveSignedCmpSeq Prop
n Prop
a
TCon (TC (TCTuple _)) es :: [Prop]
es -> [Prop] -> Solved
SolvedIf ((Prop -> Prop) -> [Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Prop
pSignedCmp [Prop]
es)
TCon (TC TCFun) [_,_] ->
TCErrorMessage -> Solved
Unsolvable (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage "Signed comparisons may not be performed on functions."
TRec fs :: [(Ident, Prop)]
fs -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pSignedCmp Prop
e | (_,e :: Prop
e) <- [(Ident, Prop)]
fs ]
_ -> Solved
Unsolved
solveLiteralInst :: Type -> Type -> Solved
solveLiteralInst :: Prop -> Prop -> Solved
solveLiteralInst val :: Prop
val ty :: Prop
ty
| TCon (TError _ e :: TCErrorMessage
e) _ <- Prop -> Prop
tNoUser Prop
val = TCErrorMessage -> Solved
Unsolvable TCErrorMessage
e
| Bool
otherwise =
case Prop -> Prop
tNoUser Prop
ty of
TCon (TError _ e :: TCErrorMessage
e) _ -> TCErrorMessage -> Solved
Unsolvable TCErrorMessage
e
TCon (TC TCInteger) [] -> [Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
val ]
TCon (TC TCIntMod) [modulus :: Prop
modulus] ->
[Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
val, Prop -> Prop
pFin Prop
modulus, Prop
modulus Prop -> Prop -> Prop
>== Prop -> Prop -> Prop
tAdd Prop
val Prop
tOne ]
TCon (TC TCSeq) [bits :: Prop
bits, elTy :: Prop
elTy]
| TCon (TC TCBit) [] <- Prop
ety ->
[Prop] -> Solved
SolvedIf [ Prop -> Prop
pFin Prop
val, Prop -> Prop
pFin Prop
bits, Prop
bits Prop -> Prop -> Prop
>== Prop -> Prop
tWidth Prop
val ]
| TVar _ <- Prop
ety -> Solved
Unsolved
where ety :: Prop
ety = Prop -> Prop
tNoUser Prop
elTy
TVar _ -> Solved
Unsolved
_ -> TCErrorMessage -> Solved
Unsolvable (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
forall a b. (a -> b) -> a -> b
$ String -> TCErrorMessage
TCErrorMessage (String -> TCErrorMessage) -> String -> TCErrorMessage
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show
(Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ "Type" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (Prop -> Doc
forall a. PP a => a -> Doc
pp Prop
ty) Doc -> Doc -> Doc
<+> "does not support literals."
expandProp :: Prop -> [Prop]
expandProp :: Prop -> [Prop]
expandProp prop :: Prop
prop =
Prop
prop Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
:
case Prop -> Prop
tNoUser Prop
prop of
TCon (PC pc :: PC
pc) [ty :: Prop
ty] ->
case (PC
pc, Prop -> Prop
tNoUser Prop
ty) of
(PArith, TCon (TC TCSeq) [n :: Prop
n,a :: Prop
a])
| TCon (TC TCBit) _ <- Prop
ty1 -> [Prop -> Prop
pFin Prop
n]
| TCon _ _ <- Prop
ty1 -> Prop -> [Prop]
expandProp (Prop -> Prop
pArith Prop
ty1)
| TRec {} <- Prop
ty1 -> Prop -> [Prop]
expandProp (Prop -> Prop
pArith Prop
ty1)
where
ty1 :: Prop
ty1 = Prop -> Prop
tNoUser Prop
a
(PArith, TCon (TC TCFun) [_,b :: Prop
b]) -> Prop -> [Prop]
expandProp (Prop -> Prop
pArith Prop
b)
(PArith, TCon (TC (TCTuple _)) ts :: [Prop]
ts) -> (Prop -> [Prop]) -> [Prop] -> [Prop]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Prop -> [Prop]
expandProp (Prop -> [Prop]) -> (Prop -> Prop) -> Prop -> [Prop]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop -> Prop
pArith) [Prop]
ts
(PArith, TRec fs :: [(Ident, Prop)]
fs) -> ((Ident, Prop) -> [Prop]) -> [(Ident, Prop)] -> [Prop]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Prop -> [Prop]
expandProp (Prop -> [Prop])
-> ((Ident, Prop) -> Prop) -> (Ident, Prop) -> [Prop]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop -> Prop
pArith(Prop -> Prop) -> ((Ident, Prop) -> Prop) -> (Ident, Prop) -> Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ident, Prop) -> Prop
forall a b. (a, b) -> b
snd) [(Ident, Prop)]
fs
(PCmp, TCon (TC TCSeq) [n :: Prop
n,a :: Prop
a]) -> Prop -> Prop
pFin Prop
n Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: Prop -> [Prop]
expandProp (Prop -> Prop
pCmp Prop
a)
(PCmp, TCon (TC (TCTuple _)) ts :: [Prop]
ts) -> (Prop -> [Prop]) -> [Prop] -> [Prop]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Prop -> [Prop]
expandProp (Prop -> [Prop]) -> (Prop -> Prop) -> Prop -> [Prop]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop -> Prop
pCmp) [Prop]
ts
(PCmp, TRec fs :: [(Ident, Prop)]
fs) -> ((Ident, Prop) -> [Prop]) -> [(Ident, Prop)] -> [Prop]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Prop -> [Prop]
expandProp (Prop -> [Prop])
-> ((Ident, Prop) -> Prop) -> (Ident, Prop) -> [Prop]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop -> Prop
pCmp (Prop -> Prop) -> ((Ident, Prop) -> Prop) -> (Ident, Prop) -> Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ident, Prop) -> Prop
forall a b. (a, b) -> b
snd) [(Ident, Prop)]
fs
_ -> []
_ -> []