@@ -0,0 +1,38 @@
1+import System
2+
3+data F = mkF Integer Integer Integer
4+
5+loop : Nat -> Nat -> List Integer -> IO()
6+loop n k' Nil = putStrLn $ (pack $ Vect.replicate n ' ') ++ "\t:" ++ show k'
7+loop Z k' xs = do putStrLn ("\t:"++show k')
8+ loop 10 k' xs
9+loop (S k) k' (x::xs) = do putStr (show x)
10+ loop k (S k') xs
11+
12+fn : Integer -> F
13+fn k = mkF k (4*k+2) (2*k+1)
14+
15+flr : Integer -> F -> Integer
16+flr x (mkF q r t) = (q*x + r) `div` t
17+
18+comp : F -> F -> F
19+comp (mkF q r t) (mkF u v x) = mkF (q*u) (q*v+r*x) (t*x)
20+
21+str : F -> Integer -> Nat -> List Integer
22+str _ _ Z = Nil
23+str z k (S n) = if(y == flr 4 z)
24+ then y :: str (comp (mkF 10 (-10*y) 1) z ) k n
25+ else str (comp z (fn k)) (k+1) (S n)
26+ where y = flr 3 z
27+
28+pidigit : IO()
29+pidigit = do
30+ [_,a] <- getArgs
31+ let n = fromIntegerNat (the Integer (cast a))
32+ let l = str (mkF 1 0 1) 1 n
33+ loop 10 0 l
34+ return ()
35+
36+main : IO ()
37+main = pidigit
38+