Add regression tests for superclass inference and solving

This commit is contained in:
Rob Dockins 2020-06-16 18:04:35 -07:00 committed by robdockins
parent 22e2e483d4
commit ff199bf43e
3 changed files with 47 additions and 0 deletions

View File

@ -0,0 +1,29 @@
//zeroRing : {a} (Ring a) => a
zeroRing = zero
zeroLogic : {a} (Logic a) => a
zeroLogic = zero
zeroIntegral : {a} (Integral a) => a
zeroIntegral = zero
zeroField : {a} (Field a) => a
zeroField = zero
zeroRound : {a} (Round a) => a
zeroRound = zero
fromIntIntegral : {a} (Integral a) => a
fromIntIntegral = fromInteger 42
fromIntField : {a} (Field a) => a
fromIntField = fromInteger 42
fromIntRound : {a} (Round a) => a
fromIntRound = fromInteger 42
recipRound : {a} (Round a) => a -> Integer
recipRound x = trunc (recip x)
compareRound : {a} (Round a) => a -> a -> Bit
compareRound x y = x < y

View File

@ -0,0 +1,8 @@
:l superclass.cry
:t (fromInteger 42 + zero)
:t (trunc (recip (fromInteger 5)))
:t (\x -> x < fromInteger (floor (recip x)))
:t (\x -> x == zero /. x)
:t (zero == ~zero)
:t (\x -> toInteger (x + zero))

View File

@ -0,0 +1,10 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
(fromInteger 42 + zero) : {a} (Ring a) => a
(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 -> toInteger (x + zero)) : {a} (Integral a) => a -> Integer