[isabelle] Rational numbers in Isabelle/ML



Hallo,

I noticed that there is an ML implementation of rational numbers in the Isabelle distribution (~~/src/Tools/rat.ML).

There are a few issues with this:
â for some reason, it does not use operator overloading for addition/multiplication/equality/etc. on rational numbers, but introduces a "+/", "*/" etc. syntax for it. â pretty printing displays 1/3 and 1 as "Rat (1, 3)" and "Rat (1, 0)", respectively instead of "1 / 3" and "1". One could argue that "Rat (1, 3)" is the better choice since that means one can copy-paste output directly back as ML source again; however, it also makes output more difficult to read, in my opinion. At the very least, there should be a function that converts a rational number to such a string. â there is no functionality for parsing rational numbers at all (at least I couldn't find something like that)

I have already implemented all of these things in my own little version of rational numbers (see attachment) and could merge any of them into the distribution if there is a consensus that that should be done.


Any opinions?


Cheers,

Manuel
signature MYRAT =
sig
  type rat
  
  val of_quotient : int * int -> rat
  val to_quotient  : rat -> int * int
  val from_int : int -> rat
  val to_real : rat -> real
  val from_string : string -> rat option
  val to_string : rat -> string
  val pretty : rat -> string

  val compare : rat * rat -> General.order
  val rneg : rat -> rat
  val radd : (rat * rat) -> rat
  val rsub : (rat * rat) -> rat
  val rmult : (rat * rat) -> rat
  val inv : rat -> rat
  val rdiv : (rat * rat) -> rat
  val rleq : (rat * rat) -> bool
  val rless : (rat * rat) -> bool
  val rgt : (rat * rat) -> bool
  val rgeq : (rat * rat) -> bool

  val mult_int : rat -> int -> rat
  val div_int : rat -> int -> rat
  val sign : rat -> int
  val abs : rat -> rat

  val floor : rat -> int
  val ceil : rat -> int

  val dest_rat_numeral : term -> rat

end

structure MyRat : MYRAT = 
struct

datatype rat = Rat of int * int;

fun gcd a b = 
  let fun gcd' a 0 = a 
        | gcd' a b = gcd b (a mod b)
  in  gcd' (abs a) (abs b)
  end;

fun of_quotient (_, 0) = raise Div
  | of_quotient (a, b) = 
  let val g = gcd a b 
      val (a', b') = if b<0 then (~a,~b) else (a,b)
  in  Rat (a' div g, b' div g)
  end;

fun to_quotient (Rat x) = x

fun from_int a = Rat (a, 1)

fun to_string (Rat (a, 1)) = Int.toString a
  | to_string (Rat (a, b)) = 
      (if a < 0 then "~ " else "") ^ Int.toString (abs a) ^ " / " ^ Int.toString b

fun pretty (Rat (a, 1)) = (if a < 0 then "-" else "") ^ Int.toString a
  | pretty (Rat (a, b)) = 
      (if a < 0 then "- " else "") ^ Int.toString (abs a) ^ " / " ^ Int.toString b


fun from_string s =
  let
    val (s1, s2') = s |> Substring.full |> Substring.splitl (fn x => x <> #"/") 
    val (s1, s2) = (s1, s2') |> apsnd (Substring.triml 1) |> apply2 Substring.string
  in
    if Substring.isEmpty s2' then
      Option.map from_int (Int.fromString s1)
    else
      Option.mapPartial (fn x => Option.map (fn y => of_quotient (x, y)) 
        (Int.fromString s2)) (Int.fromString s1)
  end

fun to_real (Rat (a, b)) = Real.fromInt a / Real.fromInt b
fun sign (Rat (a,_)) = Int.sign a;
fun abs (Rat (a,b)) = Rat (Int.abs a, b)

fun radd (Rat (a1,b1), Rat (a2,b2)) = of_quotient (a1*b2+a2*b1,b1*b2);
fun rneg (Rat (a1, b1)) = Rat (~a1, b1)
fun rmult (Rat (a1,b1), Rat (a2,b2)) = of_quotient (a1*a2, b1*b2);
fun rdiv (Rat (a1,b1), Rat (a2,b2)) = of_quotient (a1*b2,b1*a2);
fun inv (Rat (a, b)) = if a < 0 then Rat (~b, a) else Rat (b, a)
fun rsub (Rat (a1,b1), Rat (a2,b2)) = of_quotient (a1*b2-a2*b1,b1*b2);
fun rless (Rat (a1,b1), Rat (a2,b2)) = a1*b2 < a2*b1;
fun rleq (Rat (a1,b1), Rat (a2,b2)) = a1*b2 <= a2*b1;
fun rgt (Rat (a1,b1), Rat (a2,b2)) = a1*b2 > a2*b1;
fun rgeq (Rat (a1,b1), Rat (a2,b2)) = a1*b2 >= a2*b1;

fun div_int (Rat (a1,b1)) c = of_quotient (a1,b1*c);
fun mult_int (Rat (a1,b1)) c = of_quotient (a1*c,b1);

fun floor (Rat (x, y)) = x div y
fun ceil (Rat (x, y)) = 
  case Integer.div_mod x y of
    (q, r) => if r = 0 then q else q + 1

fun compare (Rat (a,b), Rat (c,d)) = Int.compare (a * d, b * c)

(* Destructors for rational numbers / polynomials *)

fun dest_num x = 
  case x of 
    Const ("Code_Numeral.int_of_integer", _) $ x => dest_num x
  | _ => HOLogic.dest_number x

fun dest_rat_numeral t =
  case t of 
    (Const ("Rings.divide_class.divide",_)) $ a $ b
      => of_quotient (snd (dest_num a), snd (dest_num b))
  | (Const ("Groups.uminus_class.uminus",_)) $ a 
      => rneg (dest_rat_numeral a)
  | (Const ("Rat.field_char_0_class.of_rat",_)) $ a => dest_rat_numeral a
  |  (Const ("Rat.Frct", _) $ (Const ("Product_Type.Pair", _) $ a $ b))
      => of_quotient (snd (dest_num a), snd (dest_num b))
  | _ => from_int (snd (dest_num t));

end

val _ = PolyML.addPrettyPrinter (K (K (PolyML.PrettyString o MyRat.to_string)));

val () = RunCall.addOverload MyRat.rneg "~";
val () = RunCall.addOverload MyRat.radd "+";
val () = RunCall.addOverload MyRat.rsub "-";
val () = RunCall.addOverload MyRat.rmult "*";
val () = RunCall.addOverload MyRat.rdiv "/";
val () = RunCall.addOverload MyRat.rless "<";
val () = RunCall.addOverload MyRat.rgt ">";
val () = RunCall.addOverload MyRat.rleq "<=";
val () = RunCall.addOverload MyRat.rgeq ">=";
val () = RunCall.addOverload MyRat.abs "abs";


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.