Merge branch 'master' into release-2.9.0

CHANGES.md

@@ -16,25 +16,25 @@
   class.  `Integral` contains the bitvector types and `Integer`.
 
   The new `Field` class contains types representing mathematical
-  fields (or types that are approximately fields). For now, it is
-  inhabited only by the new `Rational` type, but will eventually
-  contain `Real` and floating-point types. It has the operation
-  `recip` for reciprocal and `(/.)` for field division (not to be
-  confused for `(/)`, which is Euclidean integral division).
+  fields (or types that are approximately fields). It is currently
+  inhabited by the new `Rational` type, and the `Float`
+  family of types.  It will  eventually also contain the
+  `Real` type. It has the operation `recip` for reciprocal
+  and `(/.)` for field division (not to be confused for `(/)`,
+  which is Euclidean integral division).
 
   There is also a new `Round` class for types that can sensibly be
   rounded to integers.  This class has the methods `floor`, `ceiling`,
   `trunc`, `roundToEven`  and `roundAway` for performing different
-  kinds of integer rounding.  Currently `Rational` is the only member
-  of `Round`.
+  kinds of integer rounding.  `Rational` and `Float` inhabit `Round`.
 
   The type of `(^^)` is modified to be
   `{a, e} (Ring a, Integral e) => a -> e -> a`. This makes it clear
   that the semantics are iterated multiplication, which makes sense
   in any ring.
 
   Finally, the `lg2`, `(/$)` and `(%$)` methods of Arith have
-  had their types specialized so operate only on bitvectors.
+  had their types specialized so they operate only on bitvectors.
 
 * Added an `Eq` class, and moved the equality operations
   from `Cmp` into `Eq`. The `Z` type becomes a member of `Eq`
@@ -233,18 +233,3 @@ pattern and the `-` and `~` operators by creating local definitions
 of functions that they expand to (issue #568).
 
 * Closed issues #498, #547, #551, #562, and #563.
-
-## Solver versions
-
-Cryptol can interact with a variety of external SMT solvers to
-support the `:prove` and `:sat` commands, and requires Z3 for its
-type checker. Many versions of these solvers will work correctly, but
-for Yices and Z3 we recommend the following specific versions.
-
-* Z3 4.7.1
-* Yices 2.6.1
-
-For Yices, this is the latest version at the time of this writing.
-For Z3, it is not, and the latest versions (4.8.x) include changes
-that cause some examples that previously succeeded to time out when
-type checking.

lib/Float.cry

@@ -27,6 +27,17 @@ type Float256 = Float 19 237
  * Rounding modes (this should be an enumeration type, when we add these)
  *---------------------------------------------------------------------- */
 
+/**
+ * A 'RoundingMode' is used to specify the precise behavior of some
+ * floating point primitives.
+ *
+ * There are five valid 'RoundingMode' values:
+ *  * roundNearestEven
+ *  * roundNearestAway
+ *  * roundPositive
+ *  * roundNegative
+ *  * roundZero
+ */
 type RoundingMode = [3]
 
 /** Round toward nearest, ties go to even. */

src/Cryptol/TypeCheck/Solver/Class.hs

@@ -112,6 +112,26 @@ solveLogicInst ty = case tNoUser ty of
   -- Logic Bit
   TCon (TC TCBit) [] -> SolvedIf []
 
+  -- Logic Integer fails
+  TCon (TC TCInteger) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Integer' does not support logical operations."
+
+  -- Logic (Z n) fails
+  TCon (TC TCIntMod) [_] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Z' does not support logical operations."
+
+  -- Logic Rational fails
+  TCon (TC TCRational) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Rational' does not support logical operations."
+
+  -- Logic (Float e p) fails
+  TCon (TC TCFloat) [_, _] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Float' does not support logical operations."
+
   -- Logic a => Logic [n]a
   TCon (TC TCSeq) [_, a] -> SolvedIf [ pLogic a ]
 
@@ -144,7 +164,7 @@ solveRingInst ty = case tNoUser ty of
 
   -- Ring Bit fails
   TCon (TC TCBit) [] ->
-    Unsolvable $ TCErrorMessage "Arithmetic cannot be done on individual bits."
+    Unsolvable $ TCErrorMessage "Type 'Bit' does not support ring operations."
 
   -- Ring Integer
   TCon (TC TCInteger) [] -> SolvedIf []
@@ -193,7 +213,7 @@ solveIntegralInst ty = case tNoUser ty of
 
   -- Integral Bit fails
   TCon (TC TCBit) [] ->
-    Unsolvable $ TCErrorMessage "Arithmetic cannot be done on individual bits."
+    Unsolvable $ TCErrorMessage "Type 'Bit' is not an integral type."
 
   -- Integral Integer
   TCon (TC TCInteger) [] -> SolvedIf []
@@ -204,12 +224,12 @@ solveIntegralInst ty = case tNoUser ty of
       TCon (TC TCBit) [] -> SolvedIf [ pFin n ]
       TVar _ -> Unsolved
       _ -> Unsolvable $ TCErrorMessage $ show
-          $ "Type" <+> quotes (pp ty) <+> "is not an intergral type."
+          $ "Type" <+> quotes (pp ty) <+> "is not an integral type."
 
   TVar _ -> Unsolved
 
   _ -> Unsolvable $ TCErrorMessage $ show
-          $ "Type" <+> quotes (pp ty) <+> "is not an intergral type."
+          $ "Type" <+> quotes (pp ty) <+> "is not an integral type."
 
 
 -- | Solve a Field constraint by instance, if possible.
@@ -219,16 +239,50 @@ solveFieldInst ty = case tNoUser ty of
   -- Field Error -> fails
   TCon (TError _ e) _ -> Unsolvable e
 
+  -- Field Bit fails
+  TCon (TC TCBit) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Bit' does not support field operations."
+
+  -- Field Integer fails
+  TCon (TC TCInteger) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Integer' does not support field operations."
+
   -- Field Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
   -- ValidFloat e p => Field (Float e p)
   TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
 
   -- Field Real
-  -- Field (Z n)
+
+  -- Field (Z n) fails for now (to be added later with a 'prime n' requirement)
+  TCon (TC TCIntMod) [_] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Z' does not support field operations."
 --  TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne, pPrime n ]
 
+  -- Field ([n]a) fails
+  TCon (TC TCSeq) [_, _] ->
+    Unsolvable $
+    TCErrorMessage "Sequence types do not support field operations."
+
+  -- Field (a -> b) fails
+  TCon (TC TCFun) [_, _] ->
+    Unsolvable $
+    TCErrorMessage "Function types do not support field operations."
+
+  -- Field (a, b, ...) fails
+  TCon (TC (TCTuple _)) _ ->
+    Unsolvable $
+    TCErrorMessage "Tuple types do not support field operations."
+
+  -- Field {x : a, y : b, ...} fails
+  TRec _ ->
+    Unsolvable $
+    TCErrorMessage "Record types do not support field operations."
+
   _ -> Unsolved
 
 
@@ -239,6 +293,21 @@ solveRoundInst ty = case tNoUser ty of
   -- Round Error -> fails
   TCon (TError _ e) _ -> Unsolvable e
 
+  -- Round Bit fails
+  TCon (TC TCBit) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Bit' does not support rounding operations."
+
+  -- Round Integer fails
+  TCon (TC TCInteger) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Integer' does not support rounding operations."
+
+  -- Round (Z n) fails
+  TCon (TC TCIntMod) [_] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Z' does not support rounding operations."
+
   -- Round Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
@@ -247,6 +316,26 @@ solveRoundInst ty = case tNoUser ty of
 
   -- Round Real
 
+  -- Round ([n]a) fails
+  TCon (TC TCSeq) [_, _] ->
+    Unsolvable $
+    TCErrorMessage "Sequence types do not support rounding operations."
+
+  -- Round (a -> b) fails
+  TCon (TC TCFun) [_, _] ->
+    Unsolvable $
+    TCErrorMessage "Function types do not support rounding operations."
+
+  -- Round (a, b, ...) fails
+  TCon (TC (TCTuple _)) _ ->
+    Unsolvable $
+    TCErrorMessage "Tuple types do not support rounding operations."
+
+  -- Round {x : a, y : b, ...} fails
+  TRec _ ->
+    Unsolvable $
+    TCErrorMessage "Record types do not support rounding operations."
+
   _ -> Unsolved
 
 
@@ -281,7 +370,7 @@ solveEqInst ty = case tNoUser ty of
 
   -- Eq (a -> b) fails
   TCon (TC TCFun) [_,_] ->
-    Unsolvable $ TCErrorMessage "Comparisons may not be performed on functions."
+    Unsolvable $ TCErrorMessage "Function types do not support comparisons."
 
   -- (Eq a, Eq b) => Eq { x:a, y:b }
   TRec fs -> SolvedIf [ pEq e | e <- recordElements fs ]
@@ -307,7 +396,7 @@ solveCmpInst ty = case tNoUser ty of
 
   -- Cmp (Z n) fails
   TCon (TC TCIntMod) [_] ->
-    Unsolvable $ TCErrorMessage "Values of Z_n type cannot be compared for order"
+    Unsolvable $ TCErrorMessage "Type 'Z' does not support order comparisons."
 
   -- ValidFloat e p => Cmp (Float e p)
   TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
@@ -320,7 +409,7 @@ solveCmpInst ty = case tNoUser ty of
 
   -- Cmp (a -> b) fails
   TCon (TC TCFun) [_,_] ->
-    Unsolvable $ TCErrorMessage "Comparisons may not be performed on functions."
+    Unsolvable $ TCErrorMessage "Function types do not support order comparisons."
 
   -- (Cmp a, Cmp b) => Cmp { x:a, y:b }
   TRec fs -> SolvedIf [ pCmp e | e <- recordElements fs ]
@@ -350,8 +439,30 @@ solveSignedCmpInst ty = case tNoUser ty of
   -- SignedCmp Error -> fails
   TCon (TError _ e) _ -> Unsolvable e
 
-  -- SignedCmp Bit
-  TCon (TC TCBit) [] -> Unsolvable $ TCErrorMessage "Signed comparisons may not be performed on bits"
+  -- SignedCmp Bit fails
+  TCon (TC TCBit) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Bit' does not support signed comparisons."
+
+  -- SignedCmp Integer fails
+  TCon (TC TCInteger) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Integer' does not support signed comparisons."
+
+  -- SignedCmp (Z n) fails
+  TCon (TC TCIntMod) [_] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Z' does not support signed comparisons."
+
+  -- SignedCmp Rational fails
+  TCon (TC TCRational) [] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Rational' does not support signed comparisons."
+
+  -- SignedCmp (Float e p) fails
+  TCon (TC TCFloat) [_, _] ->
+    Unsolvable $
+    TCErrorMessage "Type 'Float' does not support signed comparisons."
 
   -- SignedCmp for sequences
   TCon (TC TCSeq) [n,a] -> solveSignedCmpSeq n a
@@ -361,7 +472,8 @@ solveSignedCmpInst ty = case tNoUser ty of
 
   -- SignedCmp (a -> b) fails
   TCon (TC TCFun) [_,_] ->
-    Unsolvable $ TCErrorMessage "Signed comparisons may not be performed on functions."
+    Unsolvable $
+    TCErrorMessage "Function types do not support signed comparisons."
 
   -- (SignedCmp a, SignedCmp b) => SignedCmp { x:a, y:b }
   TRec fs -> SolvedIf [ pSignedCmp e | e <- recordElements fs ]
@@ -386,10 +498,14 @@ solveFLiteralInst numT denT rndT ty
 
       TCon (TError _ e) _ -> Unsolvable e
 
-      TCon (TC TCRational) [] -> SolvedIf []
+      TCon (TC TCRational) [] ->
+        SolvedIf [ pFin numT, pFin denT, denT >== tOne ]
 
       TCon (TC TCFloat) [e,p]
-        | Just 0    <- tIsNum rndT -> SolvedIf [ pValidFloat e p ]
+        | Just 0    <- tIsNum rndT ->
+          SolvedIf [ pValidFloat e p
+                   , pFin numT, pFin denT, denT >== tOne ]
+
         | Just _    <- tIsNum rndT
         , Just opts <- knownSupportedFloat e p
         , Just n    <- tIsNum numT

src/Cryptol/TypeCheck/Type.hs

@@ -834,7 +834,16 @@ instance PP (WithNames Newtype) where
 
 
 
-
+-- | The precedence levels used by this pretty-printing instance
+-- correspond with parser non-terminals as follows:
+--
+--   * 0-1: @type@
+--
+--   * 2: @infix_type@
+--
+--   * 3: @app_type@
+--
+--   * 4: @atype@
 instance PP (WithNames Type) where
   ppPrec prec ty0@(WithNames ty nmMap) =
     case ty of
@@ -867,7 +876,7 @@ instance PP (WithNames Type) where
 
           (TCTuple _, fs)     -> parens $ fsep $ punctuate comma $ map (go 0) fs
 
-          (_, _)              -> pp tc <+> fsep (map (go 5) ts)
+          (_, _)              -> optParens (prec > 3) $ pp tc <+> fsep (map (go 4) ts)
 
       TCon (PC pc) ts ->
         case (pc,ts) of

tests/issues/issue835.icry

@@ -0,0 +1,2 @@
+:m Float
+:t (zero : Float 5 11) <$ zero

tests/issues/issue835.icry.stdout

@@ -0,0 +1,11 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Float
+
+[error] at <interactive>:1:1--1:28:
+  Unsolvable constraints:
+    • SignedCmp (Float 5 11)
+        arising from
+        use of expression (<$)
+        at <interactive>:1:1--1:28
+    • Reason: Type 'Float' does not support signed comparisons.

tests/issues/issue845.cry

@@ -0,0 +1,2 @@
+rfrac : {m, n} Rational
+rfrac = fraction`{m, n, 0, Rational}

tests/issues/issue845.icry

@@ -0,0 +1,11 @@
+:l issue845.cry
+fraction`{1,2,0,Rational}
+fraction`{1,0,0,Rational}
+fraction`{inf,2,0,Rational}
+:m Float
+fraction`{1,2,0,Float64}
+fraction`{1,0,0,Float64}
+fraction`{inf,2,0,Float64}
+fraction`{1,10,0,Float 3 2}
+fraction`{1,10,1,Float 3 2}
+