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