mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-17 13:01:31 +03:00
109 lines
2.5 KiB
Plaintext
109 lines
2.5 KiB
Plaintext
/*
|
|
* Copyright (c) 2013-2015 Galois, Inc.
|
|
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
|
*/
|
|
|
|
module Cryptol where
|
|
|
|
/**
|
|
* The value corresponding to a numeric type.
|
|
*/
|
|
primitive demote : {val, bits} (fin val, fin bits, bits >= width val) => [bits]
|
|
|
|
infixl 6 +, -
|
|
infixl 7 *, /
|
|
infixr 8 ^^
|
|
|
|
/**
|
|
* Add two values.
|
|
* * For words, addition uses modulo arithmetic.
|
|
* * Structured values are added element-wise.
|
|
*/
|
|
primitive (+) : {a} (Arith a) => a -> a -> a
|
|
|
|
/**
|
|
* For words, subtraction uses modulo arithmetic.
|
|
* Structured values are subtracted element-wise. Defined as:
|
|
* a - b = a + negate b
|
|
* See also: `negate'.
|
|
*/
|
|
primitive (-) : {a} (Arith a) => a -> a -> a
|
|
|
|
/**
|
|
* For words, multiplies two words, modulus 2^^a.
|
|
* Structured values are multiplied element-wise.
|
|
*/
|
|
primitive (*) : {a} (Arith a) => a -> a -> a
|
|
|
|
/**
|
|
* For words, divides two words, modulus 2^^a.
|
|
* Structured values are divided element-wise.
|
|
*/
|
|
primitive (/) : {a} (Arith a) => a -> a -> a
|
|
|
|
/**
|
|
* For words, takes the modulus of two words, modulus 2^^a.
|
|
* Over structured values, operates element-wise.
|
|
* Be careful, as this will often give unexpected results due to interaction of
|
|
* the two moduli.
|
|
*/
|
|
primitive (%) : {a} (Arith a) => a -> a -> a
|
|
|
|
/**
|
|
* For words, takes the exponent of two words, modulus 2^^a.
|
|
* Over structured values, operates element-wise.
|
|
* Be careful, due to its fast-growing nature, exponentiation is prone to
|
|
* interacting poorly with defaulting.
|
|
*/
|
|
primitive (^^) : {a} (Arith a) => a -> a -> a
|
|
|
|
/*
|
|
* Log base two.
|
|
*
|
|
* For words, computes the ceiling of log, base 2, of a number.
|
|
* Over structured values, operates element-wise.
|
|
*/
|
|
/* primitive lg2 : {a} (Arith a) => a -> a */
|
|
|
|
|
|
type Bool = Bit
|
|
|
|
/**
|
|
* The constant True. Corresponds to the bit value 1.
|
|
*/
|
|
primitive True : Bit
|
|
|
|
/**
|
|
* The constant False. Corresponds to the bit value 0.
|
|
*/
|
|
primitive False : Bit
|
|
|
|
|
|
type String n = [n][8]
|
|
type Word n = [n]
|
|
type Char = [8]
|
|
|
|
take : {front,back,elem} (fin front) => [front + back] elem -> [front] elem
|
|
take (x # _) = x
|
|
|
|
drop : {front,back,elem} (fin front) => [front + back] elem -> [back] elem
|
|
drop ((_ : [front] _) # y) = y
|
|
|
|
tail : {a, b} [1 + a]b -> [a]b
|
|
tail xs = drop`{1} xs
|
|
|
|
width : {bits,len,elem} (fin len, fin bits, bits >= width len) => [len] elem -> [bits]
|
|
width _ = `len
|
|
|
|
undefined : {a} a
|
|
undefined = error "undefined"
|
|
|
|
splitBy : {parts,each,elem} (fin each) =>
|
|
[parts * each] elem -> [parts][each]elem
|
|
splitBy = split
|
|
|
|
groupBy : {each,parts,elem} (fin each) =>
|
|
[parts * each] elem -> [parts][each]elem
|
|
groupBy = split`{parts=parts}
|
|
|