GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-15 10:46:37 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #602 from GaloisInc/issue601

Browse Source 
Update doc-strings for Cryptol prelude arithmetic operators.
This commit is contained in:
brianhuffman 2019-06-03 11:04:25 -07:00 committed by GitHub
commit 019a79c0c3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 27 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
lib/Cryptol.cry
View File

@ -33,44 +33,50 @@ infixl 100 @, @@, !, !!
/** /**
* Add two values. * Add two values.
* * For words, addition uses modulo arithmetic. * * For type [n], addition is modulo 2^^n.
* * Structured values are added element-wise. * * Structured values are added element-wise.
*/ */
primitive (+) : {a} (Arith a) => a -> a -> a primitive (+) : {a} (Arith a) => a -> a -> a
/** /**
* For words, subtraction uses modulo arithmetic. * Subtract two values.
* Structured values are subtracted element-wise. Defined as: * * For type [n], subtraction is modulo 2^^n.
* a - b = a + negate b * * Structured values are subtracted element-wise.
* See also: `negate'. * * Satisfies 'a - b = a + negate b'.
* See also: 'negate'.
*/ */
primitive (-) : {a} (Arith a) => a -> a -> a primitive (-) : {a} (Arith a) => a -> a -> a
/** /**
* For words, multiplies two words, modulus 2^^a. * Multiply two values.
* Structured values are multiplied element-wise. * * For type [n], multiplication is modulo 2^^n.
* * Structured values are multiplied element-wise.
*/ */
primitive (*) : {a} (Arith a) => a -> a -> a primitive (*) : {a} (Arith a) => a -> a -> a
/** /**
* For words, divides two words, modulus 2^^a. * Divide two values, rounding down.
* Structured values are divided element-wise. * * For type [n], the arguments are treated as unsigned.
* * Structured values are divided element-wise.
* * Division by zero is undefined.
*/ */
primitive (/) : {a} (Arith a) => a -> a -> a primitive (/) : {a} (Arith a) => a -> a -> a
/** /**
* For words, takes the modulus of two words, modulus 2^^a. * Compute the remainder from dividing two values.
* Over structured values, operates element-wise. * * For type [n], the arguments are treated as unsigned.
* Be careful, as this will often give unexpected results due to interaction of * * Structured values are combined element-wise.
* the two moduli. * * Remainder of division by zero is undefined.
* * Satisfies 'x % y == x - (x / y) * y'.
*/ */
primitive (%) : {a} (Arith a) => a -> a -> a primitive (%) : {a} (Arith a) => a -> a -> a
/** /**
* For words, takes the exponent of two words, modulus 2^^a. * Compute the exponentiation of two values.
* Over structured values, operates element-wise. * * For type [n], the exponent is treated as unsigned,
* Be careful, due to its fast-growing nature, exponentiation is prone to * and the result is reduced modulo 2^^n.
* interacting poorly with defaulting. * * For type Integer, negative powers are undefined.
* * Structured values are combined element-wise.
*/ */
primitive (^^) : {a} (Arith a) => a -> a -> a primitive (^^) : {a} (Arith a) => a -> a -> a
@ -96,9 +102,11 @@ primitive True : Bit
primitive False : Bit primitive False : Bit
/** /**
* Returns the twos complement of its argument. * Returns the two's complement of its argument.
* Over structured values, operates element-wise. * Over structured values, operates element-wise.
* negate a = ~a + 1 * The prefix notation '- x' is syntactic sugar
* for 'negate x'.
* Satisfies 'negate a = ~a + 1'.
*/ */
primitive negate : {a} (Arith a) => a -> a primitive negate : {a} (Arith a) => a -> a