word8.lem

(*
  Copyright 2016 Sami Mäkelä

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

open import Pervasives
open import Word

type word8 = W8 of integer
declare isabelle target_rep type word8 = `word` 8

(* perhaps should truncate here? *)
val bs_to_w8 : bitSequence -> word8
let bs_to_w8 seq = W8 (integerFromBitSeq seq)
declare isabelle target_rep function bs_to_w8 = (fun w -> `word_of_int` (integerFromBitSeq w))

val w8_to_bs : word8 -> bitSequence
let w8_to_bs (W8 i) = bitSeqFromInteger (Just 8) i

val base : integer
let base = 2**8

val word8BinTest : forall 'a. (integer -> integer -> 'a) -> word8 -> word8 -> 'a
let word8BinTest binop (W8 w1) (W8 w2) = binop (w1 mod base) (w2 mod base)

val word8BBinTest : forall 'a. (bitSequence -> bitSequence -> 'a) -> word8 -> word8 -> 'a
let word8BBinTest binop w1 w2 = binop (w8_to_bs w1) (w8_to_bs w2)

val word8BinOp : (integer -> integer -> integer) -> word8 -> word8 -> word8
let word8BinOp binop (W8 w1) (W8 w2) = W8 (binop (w1 mod base) (w2 mod base) mod base)

val word8BBinOp : (bitSequence -> bitSequence -> bitSequence) -> word8 -> word8 -> word8
let word8BBinOp binop w1 w2 = bs_to_w8 (binop (w8_to_bs w1) (w8_to_bs w2))

val word8NatOp : (integer -> nat -> integer) -> word8 -> nat -> word8
let word8NatOp binop (W8 w1) n = W8  (binop (w1 mod base) n mod base)

val word8BNatOp : (bitSequence -> nat -> bitSequence) -> word8 -> nat -> word8
let word8BNatOp binop w1 n = bs_to_w8 (binop (w8_to_bs w1) n)

val word8BUnaryOp : (bitSequence -> bitSequence) -> word8 -> word8
let word8BUnaryOp op w = bs_to_w8 (op (w8_to_bs w))

val word8UnaryOp : (integer -> integer) -> word8 -> word8
let word8UnaryOp op (W8 w) = W8 (op w mod base)

val word8ToNat : word8 -> nat
let word8ToNat w = natFromInteger (integerFromBitSeq (w8_to_bs w))
declare isabelle target_rep function word8ToNat = `unat`

val word8ToInt : word8 -> int
let word8ToInt w = intFromInteger (integerFromBitSeq (w8_to_bs w))
declare isabelle target_rep function word8ToInt = `sint`

declare isabelle target_rep function w8_to_bs = (fun w -> bitSeqFromInteger (Just 8) (integerFromInt (word8ToInt w)))

val word8FromInteger : integer -> word8
let word8FromInteger i = W8 (i mod base)
declare isabelle target_rep function word8FromInteger = (fun i -> `word_of_int` (intFromInteger i))

val word8FromInt : int -> word8
let word8FromInt i = W8 (integerFromInt i mod base)
declare isabelle target_rep function word8FromInt = `word_of_int`

val word8FromNat : nat -> word8
let word8FromNat i = word8FromInteger (integerFromNat i)

val word8FromBoollist : list bool -> word8
let word8FromBoollist lst = match bitSeqFromBoolList lst with
 | Nothing -> bs_to_w8 0
 | Just a -> bs_to_w8 a
end
declare isabelle target_rep function word8FromBoollist = `of_bl`

val boolListFromWord8 : word8 -> list bool
let boolListFromWord8 w = boolListFrombitSeq 8 (w8_to_bs w)
declare isabelle target_rep function boolListFromWord8 = `to_bl`

val word8FromNumeral : numeral -> word8
let word8FromNumeral w = W8 (integerFromNumeral w mod base)

instance (Numeral word8)
  let fromNumeral = word8FromNumeral
end

val w8Eq : word8 -> word8 -> bool
let w8Eq = unsafe_structural_equality

val w8Less : word8 -> word8 -> bool
let w8Less bs1 bs2 = word8BinTest (<) bs1 bs2

val w8LessEqual : word8 -> word8 -> bool
let w8LessEqual bs1 bs2 = word8BinTest (<=) bs1 bs2

val w8Greater : word8 -> word8 -> bool
let w8Greater bs1 bs2 = word8BinTest (>) bs1 bs2

val w8GreaterEqual : word8 -> word8 -> bool
let w8GreaterEqual bs1 bs2 = word8BinTest (>=) bs1 bs2

val w8Compare : word8 -> word8 -> ordering
let w8Compare bs1 bs2 = word8BinTest compare bs1 bs2

instance (Ord word8)
  let compare = w8Compare
  let (<) = w8Less
  let (<=) = w8LessEqual
  let (>) = w8Greater
  let (>=) = w8GreaterEqual
end

instance (SetType word8)
  let setElemCompare = w8Compare
end

val word8Negate : word8 -> word8
let word8Negate = word8UnaryOp ~

val word8Succ : word8 -> word8
let word8Succ = word8UnaryOp succ

val word8Pred : word8 -> word8
let word8Pred = word8UnaryOp pred

val word8Lnot : word8 -> word8
let word8Lnot = word8UnaryOp lnot

val word8Add : word8 -> word8 -> word8
let word8Add = word8BinOp (+)

val word8Minus : word8 -> word8 -> word8
let word8Minus = word8BinOp (-)

val word8Mult : word8 -> word8 -> word8
let word8Mult = word8BinOp ( * )

val word8IntegerDivision : word8 -> word8 -> word8
let word8IntegerDivision = word8BinOp (/)

val word8Division : word8 -> word8 -> word8
let word8Division = word8BinOp (div)

val word8Remainder : word8 -> word8 -> word8
let word8Remainder = word8BinOp (mod)

val word8Land : word8 -> word8 -> word8
let word8Land = word8BinOp (land)

val word8Lor : word8 -> word8 -> word8
let word8Lor = word8BinOp (lor)

val word8Lxor : word8 -> word8 -> word8
let word8Lxor = word8BinOp (lxor)

val word8Min : word8 -> word8 -> word8
let word8Min = word8BinOp (min)

val word8Max : word8 -> word8 -> word8
let word8Max = word8BinOp (max)

val word8Power : word8 -> nat -> word8
let word8Power = word8NatOp ( ** )

val word8Asr : word8 -> nat -> word8
let word8Asr = word8NatOp (asr)

val word8Lsr : word8 -> nat -> word8
let word8Lsr = word8NatOp (lsr)

val word8Lsl : word8 -> nat -> word8
let word8Lsl = word8NatOp (lsl)

declare isabelle target_rep function word8Lnot w = (`NOT` w)
declare isabelle target_rep function word8Lor = infix `OR`
declare isabelle target_rep function word8Lxor = infix `XOR`
declare isabelle target_rep function word8Land = infix `AND`
declare isabelle target_rep function word8Lsl = infix `<<`
declare isabelle target_rep function word8Lsr = infix `>>`
declare isabelle target_rep function word8Asr = infix `>>>`


instance (NumNegate word8)
  let ~ = word8Negate
end

instance (NumAdd word8)
  let (+) = word8Add
end

instance (NumMinus word8)
  let (-) = word8Minus
end

instance (NumSucc word8)
  let succ = word8Succ
end

instance (NumPred word8)
  let pred = word8Pred
end

instance (NumMult word8)
  let ( * ) = word8Mult
end

instance (NumPow word8)
  let ( ** ) = word8Power
end

instance ( NumIntegerDivision word8) 
  let (div) = word8IntegerDivision
end

instance ( NumDivision word8 ) 
  let (/) = word8Division
end

instance (NumRemainder word8) 
  let (mod) = word8Remainder
end

instance (OrdMaxMin word8) 
  let max = word8Max
  let min = word8Min
end

instance (WordNot word8) 
  let lnot = word8Lnot
end

instance (WordAnd word8) 
  let (land) = word8Land
end

instance (WordOr word8) 
  let (lor) = word8Lor
end

instance (WordXor word8) 
  let (lxor) = word8Lxor
end

instance (WordLsl word8) 
  let (lsl) = word8Lsl
end

instance (WordLsr word8)
  let (lsr) = word8Lsr
end

instance (WordAsr word8)
  let (asr) = word8Asr
end

val word8UGT : word8 -> word8 -> bool
let word8UGT a b = word8ToNat a > word8ToNat b
declare isabelle target_rep function word8UGT = infix `>`

declare isabelle target_rep function word8FromNumeral n = ((`word_of_int` n) : word8)
declare isabelle target_rep function w8Less = `word_sless`
declare isabelle target_rep function w8LessEqual = `word_sle`
declare isabelle target_rep function w8Greater x y = w8Less y x
declare isabelle target_rep function w8GreaterEqual x y = w8LessEqual y x
declare isabelle target_rep function w8Compare = genericCompare w8Less w8Eq

declare isabelle target_rep function word8Negate i = `-` i
declare isabelle target_rep function word8Add = infix `+`
declare isabelle target_rep function word8Minus = infix `-`
declare isabelle target_rep function word8Succ n = n + 1
declare isabelle target_rep function word8Pred n = n - 1
declare isabelle target_rep function word8Mult = infix `*`
declare isabelle target_rep function word8Power = infix `^`
declare isabelle target_rep function word8Division = infix `div`
declare isabelle target_rep function word8IntegerDivision = infix `div`
declare isabelle target_rep function word8Remainder = infix `mod`
declare isabelle target_rep function word8Min = `min`
declare isabelle target_rep function word8Max = `max`