From 6bedcbb4b3300af974f3f8f4a47c5dcbe62c6e07 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 16 Jun 2020 19:04:03 -0700 Subject: [PATCH] Add a new `Eq` typeclass for types that have equality tests. The `(==)` and `(!=)` operators move into the new `Eq` typeclass, which becomes a superclass of `Cmp` and `SignedCmp`. --- lib/Cryptol.cry | 50 ++++--- src/Cryptol/TypeCheck/SimpleSolver.hs | 6 +- src/Cryptol/TypeCheck/Solver/Class.hs | 129 +++++------------- .../TypeCheck/Solver/Numeric/Interval.hs | 4 +- src/Cryptol/TypeCheck/TCon.hs | 6 +- src/Cryptol/TypeCheck/Type.hs | 30 ++-- tests/issues/issue226.icry.stdout | 9 +- tests/regression/superclass.icry.stdout | 4 +- 8 files changed, 100 insertions(+), 138 deletions(-) diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index f343aca7..02dacf11 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -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. diff --git a/src/Cryptol/TypeCheck/SimpleSolver.hs b/src/Cryptol/TypeCheck/SimpleSolver.hs index d998dacb..f6a5df7e 100644 --- a/src/Cryptol/TypeCheck/SimpleSolver.hs +++ b/src/Cryptol/TypeCheck/SimpleSolver.hs @@ -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 diff --git a/src/Cryptol/TypeCheck/Solver/Class.hs b/src/Cryptol/TypeCheck/Solver/Class.hs index fe977e0d..e986e976 100644 --- a/src/Cryptol/TypeCheck/Solver/Class.hs +++ b/src/Cryptol/TypeCheck/Solver/Class.hs @@ -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 - - _ -> [] - - _ -> [] diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs index ba1929db..fcc4a935 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs @@ -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) diff --git a/src/Cryptol/TypeCheck/TCon.hs b/src/Cryptol/TypeCheck/TCon.hs index da543fe1..b0f7368d 100644 --- a/src/Cryptol/TypeCheck/TCon.hs +++ b/src/Cryptol/TypeCheck/TCon.hs @@ -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" - - diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index 4212e919..cef0c36a 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -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] diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout index ff767698..042f2020 100644 --- a/tests/issues/issue226.icry.stdout +++ b/tests/issues/issue226.icry.stdout @@ -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 diff --git a/tests/regression/superclass.icry.stdout b/tests/regression/superclass.icry.stdout index dc9c04ec..da5da486 100644 --- a/tests/regression/superclass.icry.stdout +++ b/tests/regression/superclass.icry.stdout @@ -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