GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-23 03:48:46 +03:00
Code Issues Projects Releases Wiki Activity

Add a new Eq typeclass for types that have equality tests.

Browse Source 
The `(==)` and `(!=)` operators move into the new `Eq` typeclass,
which becomes a superclass of `Cmp` and `SignedCmp`.
This commit is contained in:
Rob Dockins 2020-06-16 19:04:03 -07:00 committed by robdockins
parent 4248560e39
commit 6bedcbb4b3
8 changed files with 100 additions and 138 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

50
lib/Cryptol.cry
View File

@ -404,6 +404,34 @@ primitive trunc : {a} (Round a) => a -> Integer
primitive round : {a} (Round a) => a -> Integer
// The Eq class ----------------------------------------------------
/** Value types that support equality comparisons. */
primitive type Eq : * -> Prop
/**
* Compares any two values of the same type for equality.
*/
primitive (==) : {a} (Eq a) => a -> a -> Bit
/**
* Compares any two values of the same type for inequality.
*/
primitive (!=) : {a} (Eq a) => a -> a -> Bit
/**
* Compare the outputs of two functions for equality.
*/
(===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
f === g = \ x -> f x == g x
/**
* Compare the outputs of two functions for inequality.
*/
(!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
f !== g = \x -> f x != g x
// The Cmp class ---------------------------------------------------
/** Value types that support equality and ordering comparisons. */
@ -437,28 +465,6 @@ primitive (<=) : {a} (Cmp a) => a -> a -> Bit
*/
primitive (>=) : {a} (Cmp a) => a -> a -> Bit
/**
* Compares any two values of the same type for equality.
*/
primitive (==) : {a} (Cmp a) => a -> a -> Bit
/**
* Compares any two values of the same type for inequality.
*/
primitive (!=) : {a} (Cmp a) => a -> a -> Bit
/**
* Compare the outputs of two functions for equality.
*/
(===) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> (a -> Bit)
f === g = \ x -> f x == g x
/**
* Compare the outputs of two functions for inequality.
*/
(!==) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> (a -> Bit)
f !== g = \x -> f x != g x
/**
* Returns the smaller of two comparable arguments.
* Bitvectors are compared using unsigned arithmetic.

6
src/Cryptol/TypeCheck/SimpleSolver.hs
View File

@ -9,7 +9,8 @@ import Cryptol.TypeCheck.Solver.Numeric(cryIsEqual, cryIsNotEqual, cryIsGeq)
import Cryptol.TypeCheck.Solver.Class
( solveZeroInst, solveLogicInst, solveRingInst
, solveIntegralInst, solveFieldInst, solveRoundInst
, solveCmpInst, solveSignedCmpInst, solveLiteralInst )
, solveEqInst, solveCmpInst, solveSignedCmpInst
, solveLiteralInst )
import Cryptol.Utils.Debug(ppTrace)
import Cryptol.TypeCheck.PP
@ -46,7 +47,8 @@ simplifyStep ctxt prop =
TCon (PC PIntegral) [ty] -> solveIntegralInst ty
TCon (PC PRound) [ty] -> solveRoundInst ty
TCon (PC PCmp) [ty] -> solveCmpInst ty
TCon (PC PEq) [ty] -> solveEqInst ty
TCon (PC PCmp) [ty] -> solveCmpInst ty
TCon (PC PSignedCmp) [ty] -> solveSignedCmpInst ty
TCon (PC PLiteral) [t1,t2] -> solveLiteralInst t1 t2

129
src/Cryptol/TypeCheck/Solver/Class.hs
View File

@ -16,10 +16,10 @@ module Cryptol.TypeCheck.Solver.Class
, solveFieldInst
, solveIntegralInst
, solveRoundInst
, solveEqInst
, solveCmpInst
, solveSignedCmpInst
, solveLiteralInst
, expandProp
) where
import Cryptol.TypeCheck.Type
@ -206,6 +206,41 @@ solveRoundInst ty = case tNoUser ty of
-- | Solve Eq constraints.
solveEqInst :: Type -> Solved
solveEqInst ty = case tNoUser ty of
-- Eq Error -> fails
TCon (TError _ e) _ -> Unsolvable e
-- eq Bit
TCon (TC TCBit) [] -> SolvedIf []
-- Eq Integer
TCon (TC TCInteger) [] -> SolvedIf []
-- Eq Rational
TCon (TC TCRational) [] -> SolvedIf []
-- Eq (Z n)
TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne ]
-- (fin n, Eq a) => Eq [n]a
TCon (TC TCSeq) [n,a] -> SolvedIf [ pFin n, pEq a ]
-- (Eq a, Eq b) => Eq (a,b)
TCon (TC (TCTuple _)) es -> SolvedIf (map pEq es)
-- Eq (a -> b) fails
TCon (TC TCFun) [_,_] ->
Unsolvable $ TCErrorMessage "Comparisons may not be performed on functions."
-- (Eq a, Eq b) => Eq { x:a, y:b }
TRec fs -> SolvedIf [ pEq e | (_,e) <- fs ]
_ -> Unsolved
-- | Solve Cmp constraints.
solveCmpInst :: Type -> Solved
solveCmpInst ty = case tNoUser ty of
@ -314,95 +349,3 @@ solveLiteralInst val ty
_ -> Unsolvable $ TCErrorMessage $ show
$ "Type" <+> quotes (pp ty) <+> "does not support literals."
-- | Add propositions that are implied by the given one.
-- The result contains the orignal proposition, and maybe some more.
expandProp :: Prop -> [Prop]
expandProp prop =
prop : subclasses ++ substructure
where
subclasses =
case tNoUser prop of
TCon (PC pc) [ty] ->
case pc of
-- Ring a => Zero a
PRing -> expandProp (pZero ty)
-- Logic a => Zero a
PLogic -> expandProp (pZero ty)
-- Integral a => Ring a
PIntegral -> expandProp (pRing ty)
-- Field a => Ring a
PField -> expandProp (pRing ty)
-- Round a => (Cmp a, Field a)
PRound -> expandProp (pCmp ty) ++ expandProp (pField ty)
_ -> []
_ -> []
substructure =
case tNoUser prop of
TCon (PC pc) [ty] ->
case (pc, tNoUser ty) of
-- Logic [n]a => Logic a
(PLogic, TCon (TC TCSeq) [_n,a]) -> expandProp (pLogic a)
-- Logic (a -> b) => Logic b
(PLogic, TCon (TC TCFun) [_a,b]) -> expandProp (pLogic b)
-- Logic (a,b) => (Logic a, Logic b)
(PLogic, TCon (TC (TCTuple _)) ts) -> concatMap (expandProp . pLogic) ts
-- Logic { x1 : a, x2 : b } => (Logic a, Logic b)
(PLogic, TRec fs) -> concatMap (expandProp . pLogic . snd) fs
-- Ring [n]Bit => fin n
-- (Ring [n]a, a/=Bit) => Ring a
(PRing, TCon (TC TCSeq) [n,a])
| TCon (TC TCBit) _ <- ty1 -> [pFin n]
| TCon _ _ <- ty1 -> expandProp (pRing ty1)
| TRec {} <- ty1 -> expandProp (pRing ty1)
where
ty1 = tNoUser a
-- Ring (a -> b) => Ring b
(PRing, TCon (TC TCFun) [_,b]) -> expandProp (pRing b)
-- Ring (a,b) => (Ring a, Ring b)
(PRing, TCon (TC (TCTuple _)) ts) -> concatMap (expandProp . pRing) ts
-- Ring { x1 : a, x2 : b } => (Ring a, Ring b)
(PRing, TRec fs) -> concatMap (expandProp . pRing. snd) fs
-- Cmp [n]a => (fin n, Cmp a)
(PCmp, TCon (TC TCSeq) [n,a]) -> pFin n : expandProp (pCmp a)
-- Cmp (a,b) => (Cmp a, Cmp b)
(PCmp, TCon (TC (TCTuple _)) ts) -> concatMap (expandProp . pCmp) ts
-- Cmp { x:a, y:b } => (Cmp a, Cmp b)
(PCmp, TRec fs) -> concatMap (expandProp . pCmp . snd) fs
-- SignedCmp [n]Bit => (fin n, n >= 1)
-- (SignedCmp [n]a, a /= Bit) => SignedCmp a
(PSignedCmp, TCon (TC TCSeq) [n,a])
| TCon (TC TCBit) _ <- ty1 -> [pFin n, n >== tOne]
| TCon _ _ <- ty1 -> expandProp (pSignedCmp ty1)
| TRec {} <- ty1 -> expandProp (pSignedCmp ty1)
where
ty1 = tNoUser a
-- SignedCmp (a,b) => (SignedCmp a, SignedCmp b)
(PSignedCmp, TCon (TC (TCTuple _)) ts) -> concatMap (expandProp . pSignedCmp) ts
-- Cmp { x:a, y:b } => (Cmp a, Cmp b)
(PSignedCmp, TRec fs) -> concatMap (expandProp . pSignedCmp . snd) fs
_ -> []
_ -> []

4
src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs
View File

@ -108,11 +108,11 @@ propInterval varInts prop = catMaybes
x <- tIsVar ty
return (x,iAnyFin)
, do (l,r) <- pIsEq prop
, do (l,r) <- pIsEqual prop
x <- tIsVar l
return (x,typeInterval varInts r)
, do (l,r) <- pIsEq prop
, do (l,r) <- pIsEqual prop
x <- tIsVar r
return (x,typeInterval varInts l)

6
src/Cryptol/TypeCheck/TCon.hs
View File

@ -67,6 +67,7 @@ builtInType nm =
, "Integral" ~> PC PIntegral
, "Field" ~> PC PField
, "Round" ~> PC PRound
, "Eq" ~> PC PEq
, "Cmp" ~> PC PCmp
, "SignedCmp" ~> PC PSignedCmp
, "Literal" ~> PC PLiteral
@ -147,6 +148,7 @@ instance HasKind PC where
PIntegral -> KType :-> KProp
PField -> KType :-> KProp
PRound -> KType :-> KProp
PEq -> KType :-> KProp
PCmp -> KType :-> KProp
PSignedCmp -> KType :-> KProp
PLiteral -> KNum :-> KType :-> KProp
@ -193,6 +195,7 @@ data PC = PEqual -- ^ @_ == _@
| PIntegral -- ^ @Integral _@
| PField -- ^ @Field _@
| PRound -- ^ @Round _@
| PEq -- ^ @Eq _@
| PCmp -- ^ @Cmp _@
| PSignedCmp -- ^ @SignedCmp _@
| PLiteral -- ^ @Literal _ _@
@ -295,6 +298,7 @@ instance PP PC where
PIntegral -> text "Integral"
PField -> text "Field"
PRound -> text "Round"
PEq -> text "Eq"
PCmp -> text "Cmp"
PSignedCmp -> text "SignedCmp"
PLiteral -> text "Literal"
@ -337,5 +341,3 @@ instance PP TFun where
TCCeilDiv -> text "/^"
TCCeilMod -> text "%^"
TCLenFromThenTo -> text "lengthFromThenTo"

30
src/Cryptol/TypeCheck/Type.hs
View File

@ -290,13 +290,13 @@ superclassSet (TCon (PC p0) [t]) = go p0
where
super p = Set.insert (TCon (PC p) [t]) (go p)
go PRing = super PZero
go PLogic = super PZero
go PField = super PRing
go PIntegral = super PRing
go PRound = super PField <> super PCmp
-- go PCmp = super PEq
-- go PSignedCmp = super PEq
go PRing = super PZero
go PLogic = super PZero
go PField = super PRing
go PIntegral = super PRing
go PRound = super PField <> super PCmp
go PCmp = super PEq
go PSignedCmp = super PEq
go _ = mempty
superclassSet _ = mempty
@ -430,10 +430,10 @@ pIsGeq ty = case tNoUser ty of
TCon (PC PGeq) [t1,t2] -> Just (t1,t2)
_ -> Nothing
pIsEq :: Prop -> Maybe (Type,Type)
pIsEq ty = case tNoUser ty of
TCon (PC PEqual) [t1,t2] -> Just (t1,t2)
_ -> Nothing
pIsEqual :: Prop -> Maybe (Type,Type)
pIsEqual ty = case tNoUser ty of
TCon (PC PEqual) [t1,t2] -> Just (t1,t2)
_ -> Nothing
pIsZero :: Prop -> Maybe Type
pIsZero ty = case tNoUser ty of
@ -465,6 +465,11 @@ pIsRound ty = case tNoUser ty of
TCon (PC PRound) [t1] -> Just t1
_ -> Nothing
pIsEq :: Prop -> Maybe Type
pIsEq ty = case tNoUser ty of
TCon (PC PEq) [t1] -> Just t1
_ -> Nothing
pIsCmp :: Prop -> Maybe Type
pIsCmp ty = case tNoUser ty of
TCon (PC PCmp) [t1] -> Just t1
@ -644,6 +649,9 @@ pField t = TCon (PC PField) [t]
pRound :: Type -> Prop
pRound t = TCon (PC PRound) [t]
pEq :: Type -> Prop
pEq t = TCon (PC PEq) [t]
pCmp :: Type -> Prop
pCmp t = TCon (PC PCmp) [t]

9
tests/issues/issue226.icry.stdout
View File

@ -43,6 +43,7 @@ Primitive Types
(^^) : # -> # -> #
Bit : *
Cmp : * -> Prop
Eq : * -> Prop
Field : * -> Prop
fin : # -> Prop
Integer : *
@ -76,10 +77,10 @@ Symbols
(==>) : Bit -> Bit -> Bit
(\/) : Bit -> Bit -> Bit
(/\) : Bit -> Bit -> Bit
(!=) : {a} (Cmp a) => a -> a -> Bit
(!==) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
(==) : {a} (Cmp a) => a -> a -> Bit
(===) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
(!=) : {a} (Eq a) => a -> a -> Bit
(!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit
(==) : {a} (Eq a) => a -> a -> Bit
(===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit
(<) : {a} (Cmp a) => a -> a -> Bit
(<$) : {a} (SignedCmp a) => a -> a -> Bit
(<=) : {a} (Cmp a) => a -> a -> Bit

4
tests/regression/superclass.icry.stdout
View File

@ -5,6 +5,6 @@ Loading module Main
(trunc (recip (fromInteger 5))) : {a} (Round a) => Integer
(\x -> x < fromInteger (floor (recip x))) : {a} (Round a) =>
a -> Bit
(\x -> x == zero /. x) : {a} (Cmp a, Field a) => a -> Bit
(zero == ~zero) : {a} (Cmp a, Logic a) => Bit
(\x -> x == zero /. x) : {a} (Eq a, Field a) => a -> Bit
(zero == ~zero) : {a} (Eq a, Logic a) => Bit
(\x -> toInteger (x + zero)) : {a} (Integral a) => a -> Integer