(* How many integers 0 <= n < 10^18 have the property that the sum 
   of the digits of n equals the sum of digits of 137n? *)

(* answer: 20444710234716473 *)

{ 
  use import int.EuclideanDivision
  use import int.Power
  
  logic sum_digits (n:int) : int =
    if n = 0 then 0 else sum_digits (div n 10) + mod n 10

  logic p (n:int) = sum_digits(n) = sum_digits(137 * n)
  clone int.NumOf as P with logic pr = p

  type int2 = (int,int)
  logic q (d:int2) (n:int) = 
    let (a,b) = d in sum_digits(n) = sum_digits(137 * n + a) = b
  clone int.NumOfParam as Q with type param = int2, logic pr = q

  type int3 = (int,int,int)
  logic r (d:int3) (n:int) = 
    let (a,b,c) = d in 
    0 <= mod n 10 < c and sum_digits(n) = sum_digits(137 * n + a) = b
  clone int.NumOfParam as R with type param = int3, logic pr = r

  goal Test : forall n:int. 0 <= n < power 10 0 -> n = 0 
}

{
  (* use import int.ComputerDivision *)
}

let rec sd n =
  { n >= 0 }
  if n = 0 then 0 else sd (div n 10) + mod n 10
  { result = sum_digits n }

(* f(m,a,b) = the number of 0 <= n < 10^m such that 
   digitsum(n) = digitsum(137n+a) + b. *)
let rec f m a b =
  { 0 <= m }
  if m = 0 then begin
    (* only n = 0 is possible *)
    if sum_digits a + b = 0 then 1 else 0
  end else begin
    let sum = ref 0 in
    let c = ref 0 in
    while !c <= 9 do (* n = 10n' + c *)
      invariant { 0 <= !c <= 10 } 
      variant { !c }
      let x = 137 * !c + a in
      let a' = div x 10 in
      let c' = mod x 10 in
      sum := !sum + f (m-1) a' (c' + b - !c);
      c := !c + 1
    done;
    !sum
  end
  { result = Q.num_of (a,b) 0 (power 10 m) }
    

(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. examples/programs/talk290"
End: 
*)