Theory Code_Bit

header{*Code Generation for Bits*}

theory Code_Bit
imports "$ISABELLE_HOME/src/HOL/Library/Bit"
begin

(*  
    Title:      Code_Bit.thy
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
*)


text{*Implementation for the field of integer numbers module 2.
Experimentally we have checked that this implementation is faster than 
using booleans or implementing the operations by tables.*}

code_datatype "0::bit" "(1::bit)"

code_printing
  type_constructor bit \<rightharpoonup> (SML) "IntInf.int"
 | constant "0::bit" \<rightharpoonup> (SML) "0"
 | constant "1::bit" \<rightharpoonup> (SML) "1"
 | constant "op + :: bit => bit => bit" \<rightharpoonup> (SML) "IntInf.rem ((IntInf.+ ((_), (_))), 2)"
 | constant "op * :: bit => bit => bit" \<rightharpoonup> (SML) "IntInf.* ((_), (_))"
 | constant "op / :: bit => bit => bit" \<rightharpoonup> (SML) "IntInf.* ((_), (_))"

code_printing
  type_constructor bit \<rightharpoonup> (Haskell) "Integer"
 | constant "0::bit" \<rightharpoonup> (Haskell) "0"
 | constant "1::bit" \<rightharpoonup> (Haskell) "1"
 | constant "op + :: bit => bit => bit" \<rightharpoonup> (Haskell) "Prelude.rem ((_) + (_))  2"
 | constant "op * :: bit => bit => bit" \<rightharpoonup> (Haskell) "(_) * (_)"
 | constant "op / :: bit => bit => bit" \<rightharpoonup> (Haskell) "(_) * (_)"
 | class_instance bit :: "HOL.equal" => (Haskell) - (*This is necessary. See the tutorial on code generation, page 29*)

end