Theory Code_Rational

header{*Code Generation for rational numbers in Haskell*}

theory Code_Rational
imports
  Rat
  "~~/src/HOL/Library/Code_Target_Int"
begin

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

subsection{*Serializations*}

text{*The following @{text "code_include"} module is the usual way to import libraries in Haskell. In this case, we 
rebind some functions from Data.Ratio. See \url{https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-June/msg00007.html}*}

code_include Haskell Rational {*
 import qualified Data.Ratio;
 fract a b = a Data.Ratio.% b;
 numerator a = Data.Ratio.numerator a;
 denominator a = Data.Ratio.denominator a;
*}


text{*@{term "Frct"} has been serialized to a function in Haskell that makes use of @{term "integer_of_int"}.
The problem is that @{text "integer_of_int"} is an Isabelle's function that it is not always automatically generated to Haskell.
Then, sometimes we will have to add it when we will export code. See the example at the end of this file.*}

(*TODO: This is an attempt to avoid the use of integer_of_int in the serialization, but it doesn't work.
definition "Frct' p = Fract (int_of_integer (fst p)) (int_of_integer (snd p))"
lemma[code]: "Frct p = Frct' (integer_of_int (fst p), integer_of_int (snd p))"
  unfolding Frct_def Frct'_def by simp
*)

code_printing
  type_constructor rat \<rightharpoonup> (Haskell) "Prelude.Rational"
  | class_instance rat :: "HOL.equal" => (Haskell) - (*This is necessary. See the tutorial on code generation, page 29*)

  | constant "0 :: rat" \<rightharpoonup> (Haskell) "(Prelude.toRational (0::Integer))"
  | constant "1 :: rat" \<rightharpoonup> (Haskell) "(Prelude.toRational (1::Integer))"
  | constant "Frct" \<rightharpoonup> (Haskell) "(let (x,y) = _ in (Rational.fract (integer'_of'_int x) (integer'_of'_int y)))"
  | constant "quotient_of" \<rightharpoonup> (Haskell) "(let x = _ in (Int'_of'_integer (Rational.numerator x), Int'_of'_integer (Rational.denominator x)))"
  | constant "HOL.equal :: rat => rat => bool" \<rightharpoonup>
    (Haskell) "(_) == (_)"
  |  constant "op < :: rat => rat => bool" \<rightharpoonup>
    (Haskell) "_ < _"
  |  constant "op ≤ :: rat => rat => bool" \<rightharpoonup>
    (Haskell) "_ <= _"
  | constant "op + :: rat => rat => rat" \<rightharpoonup>
    (Haskell) "(_) + (_)"
  | constant "op - :: rat => rat => rat" \<rightharpoonup>
    (Haskell) "(_) - (_)"
  | constant "op * :: rat => rat => rat" \<rightharpoonup>
    (Haskell) "(_) * (_)"
  | constant "op / :: rat => rat => rat" \<rightharpoonup>
    (Haskell) " (_) '/ (_)"
 | constant "uminus :: rat => rat" \<rightharpoonup>
    (Haskell) "Prelude.negate"

(*
definition "test1 = (3::rat)"
definition "test2 = (3/9::rat)"
definition "test3 = (3/8 + 8/7::rat)"
definition "test4 = (3/8 - 8/7::rat)"
definition "test5 = (3/8 * 8/7::rat)"
definition "test6 = (3/8 / 8/7::rat)"
definition "test7 = (34 < (53 :: rat))"
definition "test8 = (34 <= (53 :: rat))"

export_code
  int_of_integer (*VERY IMPORTANT!*)
  test1
  test2
  test3
  test4
  test5
  test6
  test7
  test8
  in Haskell
  module_name "Rational_Haskell"
  file "Rational"
*)

end