cryptol/lib/Cryptol.cry

50 lines
1.1 KiB
Plaintext
Raw Normal View History

2014-04-18 02:34:25 +04:00
/*
2015-03-24 21:19:52 +03:00
* Copyright (c) 2013-2015 Galois, Inc.
2014-04-18 02:34:25 +04:00
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
module Cryptol where
infixl 6 +
/**
* (+) : {a} (Arith a) => a -> a -> a
*
* Add two values.
* * For words, addition uses modulo arithmetic.
* * Structured values are added element-wise.
*/
primitive (+) : {a} (Arith a) => a -> a -> a
2014-04-18 02:34:25 +04:00
type Bool = Bit
primitive True : Bit
primitive False : Bit
2014-04-18 02:34:25 +04:00
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}