Theory Code_Z2

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

section‹Code Generation for Z2›

theory Code_Z2
imports "HOL-Library.Z2"
begin

text‹Implementation for the field of integer numbers module 2.
Experimentally we have checked that the implementation by means of booleans is the fastest one.›

code_datatype "0::bit" "(1::bit)"
code_printing
  type_constructor bit ⇀ (SML) "Bool.bool"
 | constant "0::bit" ⇀ (SML) "false"
 | constant "1::bit" ⇀ (SML) "true"

code_printing
  type_constructor bit ⇀ (Haskell) "Bool"
 | constant "0::bit" ⇀ (Haskell) "False"
 | constant "1::bit" ⇀ (Haskell) "True"
 | class_instance bit :: "HOL.equal" => (Haskell) - (*This is necessary. See the tutorial on code generation, page 29*)


(*Other possible serialisation to Integers with arbitrary precision (performance is similar in PolyML, 
  worse in MLton and Haskell):*)
(*
code_printing
  type_constructor bit ⇀ (SML) "IntInf.int"
 | constant "0::bit" ⇀ (SML) "0"
 | constant "1::bit" ⇀ (SML) "1"
 | constant "(+) :: bit => bit => bit" ⇀ (SML) "IntInf.rem ((IntInf.+ ((_), (_))), 2)"
 | constant "( * ) :: bit => bit => bit" ⇀ (SML) "IntInf.* ((_), (_))"
 | constant "(/) :: bit => bit => bit" ⇀ (SML) "IntInf.* ((_), (_))"
*)
(*
code_printing
  type_constructor bit ⇀ (Haskell) "Integer"
 | constant "0::bit" ⇀ (Haskell) "0"
 | constant "1::bit" ⇀ (Haskell) "1"
 | constant "(+) :: bit => bit => bit" ⇀ (Haskell) "Prelude.rem ((_) + (_))  2"
 | constant "( * ) :: bit => bit => bit" ⇀ (Haskell) "(_) * (_)"
 | constant "(/) :: bit => bit => bit" ⇀ (Haskell) "(_) * (_)"
 | class_instance bit :: "HOL.equal" => (Haskell) - (*This is necessary. See the tutorial on code generation, page 29*)
*)


(*Other possible serialisation to Integers with finite precision (performance is worse):*)
(*
code_printing
  type_constructor bit ⇀ (SML) "Int.int"
 | constant "0::bit" ⇀ (SML) "0"
 | constant "1::bit" ⇀ (SML) "1"
 | constant "(+) :: bit => bit => bit" ⇀ (SML) "Int.rem ((Int.+ ((_), (_))), 2)"
 | constant "( * ) :: bit => bit => bit" ⇀ (SML) "Int.* ((_), (_))"
 | constant "(/) :: bit => bit => bit" ⇀ (SML) "Int.* ((_), (_))"
*)
end