1structure DecimalFractionPP :> DecimalFractionPP =
2struct
3
4open HolKernel Parse term_pp_types
5
6fun isconst thy name t = let
7  val {Thy,Name,...} = dest_thy_const t
8in
9  Thy = thy andalso name = Name
10end handle HOL_ERR _ => false
11
12val ten = Arbnum.fromInt 10
13
14fun power_of10 n = let
15  open Arbnum
16  fun recurse (m,acc) =
17      if m = one then SOME acc
18      else let
19        val (q, r) = divmod (m, ten)
20      in
21        if r = zero then recurse (q,acc+one)
22        else NONE
23      end
24in
25  if n > one then recurse(n,zero) else NONE
26end
27
28fun fraction {Thy,Division,fromNum} Gs backend sysp ppfns gravs depth t = let
29  val {add_string,...}  = ppfns : ppstream_funs
30  val (f, args) = strip_comb t
31  val _ = length args = 2 orelse raise UserPP_Failed
32  val _ = isconst Thy Division f orelse raise UserPP_Failed
33  fun getNum t =
34      case dest_term t of
35        COMB(t1, t2) => let
36          val _ = isconst Thy fromNum t1 orelse raise UserPP_Failed
37        in
38          numSyntax.dest_numeral t2 handle HOL_ERR _ => raise UserPP_Failed
39        end
40      | _ => raise UserPP_Failed
41  val nums = map getNum args
42  val numerator = hd nums
43  val denominator = hd (tl nums)
44  val places = case power_of10 denominator of NONE => raise UserPP_Failed
45                                            | SOME n => Arbnum.toInt n
46  val (q,r) = Arbnum.divmod(numerator, denominator)
47  val qstr = Arbnum.toString q
48  val rstr = StringCvt.padLeft #"0" places (Arbnum.toString r)
49in
50  add_string (qstr ^ "." ^ rstr)
51end
52
53end
54