(* 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