From 3bbfd455d72eefd607077e8f2c842ad2ffdec292 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Thu, 17 Nov 2022 09:33:42 -0800 Subject: [PATCH] Improve the documentation of `fromInteger`. Fixes #1465 --- cryptol.cabal | 1 + lib/Cryptol.cry | 20 +++++++++++++++----- 2 files changed, 16 insertions(+), 5 deletions(-) diff --git a/cryptol.cabal b/cryptol.cabal index 3b91b2683..61d813e8e 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -14,6 +14,7 @@ Category: Language Build-type: Simple extra-source-files: bench/data/*.cry CHANGES.md + lib/*.cry lib/*.z3 data-files: **/*.cry **/*.z3 data-dir: lib diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index ca99aad74..b00e6e43c 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -339,11 +339,21 @@ primitive complement : {a} (Logic a) => a -> a primitive type Ring : * -> Prop /** - * Converts an unbounded integer to a value in a Ring. When converting - * to the bitvector type [n], the value is reduced modulo 2^^n. Likewise, - * when converting to Z n, the value is reduced modulo n. When converting - * to a floating-point value, the value is rounded to the nearest - * representable value. + * Converts an unbounded integer to a value in a Ring using the following rules: + * * to bitvector type [n]: + * the value is reduced modulo 2^^n, + * * to Z n: + * the value is reduced modulo n, + * * floating point types: + * the value is rounded to the nearest representable value, + * * sequences other than bitvectors: + * elements are computed by using `fromInteger` pointwise + * Example: (fromInteger 2 : [3][8]) === [ 0x02, 0x02, 0x02 ] + * * tuples and records: + * elements are computed by using `fromInteger` pointwise + * Example: (fromInteger 2 : (Integer,[3][8])) === (2, [ 0x2, 0x2, 0x2 ]) + * * functions: + * a constant function returning `fromInteger` on the result type */ primitive fromInteger : {a} (Ring a) => Integer -> a