Merge pull request #1468 from GaloisInc/T1465

Improve the documentation of `fromInteger`

CHANGES.md

@@ -42,6 +42,8 @@
 * Fix a bug that caused finite bitvector enumerations to panic when used in
   combination with `(#)` (e.g., `[0..1] # 0`).
 
+* Improve documentation for `fromInteger` (#1465)
+
 # 2.13.0
 
 ## Language changes

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

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -791,7 +791,7 @@ \subsection{Appending and indexing}
   []
   invalid sequence index: 12
    -- Backtrace --
-  (Cryptol::@) called at Cryptol:875:14--875:20
+  (Cryptol::@) called at Cryptol:885:14--885:20
   (Cryptol::@@) called at <interactive>:9:1--9:28
   [9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
   9

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
 

tests/issues/issue103.icry.stdout

@@ -2,7 +2,7 @@ Loading module Cryptol
 
 Run-time error: undefined
 -- Backtrace --
-Cryptol::error called at Cryptol:1033:13--1033:18
+Cryptol::error called at Cryptol:1043:13--1043:18
 Cryptol::undefined called at issue103.icry:1:9--1:18
 Using exhaustive testing.
 Testing... ERROR for the following inputs:

tests/modsys/T16.icry.stdout

@@ -5,5 +5,5 @@ Loading module T16::B
 
 [error] at T16/B.cry:5:5--5:11
     Multiple definitions for symbol: update
-    (at Cryptol:899:11--899:17, update)
+    (at Cryptol:909:11--909:17, update)
     (at ./T16/A.cry:3:1--3:7, T16::A::update)

tests/modsys/T16.icry.stdout.mingw32

@@ -5,5 +5,5 @@ Loading module T16::B
 
 [error] at T16\B.cry:5:5--5:11
     Multiple definitions for symbol: update
-    (at Cryptol:899:11--899:17, update)
+    (at Cryptol:909:11--909:17, update)
     (at .\T16\A.cry:3:1--3:7, T16::A::update)

tests/regression/safety.icry.stdout

@@ -3,7 +3,7 @@ Counterexample
 (\x -> assert x "asdf" "asdf") False ~> ERROR
 Run-time error: asdf
 -- Backtrace --
-Cryptol::error called at Cryptol:1041:41--1041:46
+Cryptol::error called at Cryptol:1051:41--1051:46
 Cryptol::assert called at safety.icry:3:14--3:20
 <interactive>::it called at safety.icry:3:7--3:37
 Counterexample