Theory Code_Target_Rat

(* Author: Fabian Immler, Alexander Maletzky *)

theory Code_Target_Rat
  imports Complex_Main "HOL-Library.Code_Target_Numeral"
begin

text ‹Mapping type @{typ rat} to type "Rat.rat" in Isabelle/ML. Serialization for other target
  languages will be provided in the future.›

(* For testing only. *)
(*
primrec logistic' :: "rat ⇒ rat ⇒ nat ⇒ rat" where "logistic' r x 0 = x"
  | "logistic' r x (Suc n) = logistic' r (r * x * (rat_of_int 1 - x)) n"
definition "logistic n = logistic' (3.6) (0.5) (nat_of_integer n)"
ML ‹val logistic_int = @{code logistic}›
ML ‹
fun logistic' r x n = (if n = 0 then x else logistic' r (r * x * (Rat.of_int 1 - x)) (n - 1))
fun logistic_ml n = logistic' (Rat.make (36, 10)) (Rat.make (5, 10)) n
›
*)

context includes integer.lifting begin

lift_definition rat_of_integer :: "integer ⇒ rat" is Rat.of_int .

lift_definition quotient_of' :: "rat ⇒ integer × integer" is quotient_of .

lemma [code]: "Rat.of_int (int_of_integer x) = rat_of_integer x"
  by transfer simp

lemma [code_unfold]: "quotient_of = (λx. map_prod int_of_integer int_of_integer (quotient_of' x))"
  by transfer simp

end

code_printing
  type_constructor rat ⇀
    (SML) "Rat.rat" |
  constant "plus :: rat ⇒ _ ⇒ _" ⇀
    (SML) "Rat.add" |
  constant "minus :: rat ⇒ _ ⇒ _" ⇀
    (SML) "Rat.add ((_)) (Rat.neg ((_)))" |
  constant "times :: rat ⇒ _ ⇒ _" ⇀
    (SML) "Rat.mult" |
  constant "inverse :: rat ⇒ _" ⇀
    (SML) "Rat.inv" |
  constant "divide :: rat ⇒ _ ⇒ _" ⇀
    (SML) "Rat.mult ((_)) (Rat.inv ((_)))" |
  constant "rat_of_integer :: integer ⇒ rat" ⇀
    (SML) "Rat.of'_int" |
  constant "abs :: rat ⇒ _" ⇀
    (SML) "Rat.abs" |
  constant "0 :: rat" ⇀
    (SML) "!(Rat.make (0, 1))" |
  constant "1 :: rat" ⇀
    (SML) "!(Rat.make (1, 1))" |
  constant "uminus :: rat ⇒ rat" ⇀
    (SML) "Rat.neg" |
  constant "HOL.equal :: rat ⇒ _" ⇀
    (SML) "!((_ : Rat.rat) = _)" |
  constant "quotient_of'" ⇀
    (SML) "Rat.dest"

(* For testing only. *)
(*
ML ‹val logistic_rat = @{code logistic}›
ML ‹timeap (fn n => let val r = logistic_int n in r end) 16› (* 2.534s cpu time *)
ML ‹timeap (fn n => let val r = logistic_ml n in r end) 16› (* 0.021s cpu time *)
ML ‹timeap (fn n => let val r = logistic_rat n in r end) 16› (* 0.021s cpu time *)
*)

end (* theory *)