1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
data Bool :: * = False :: Bool ; True :: Bool
data List (a :: *) :: * = Nil :: List a ; Cons :: a -> List a -> List a
primitive primAdd :: Int -> Int -> Int
primitive primSub :: Int -> Int -> Int
primitive primMod :: Int -> Int -> Int
primitive primSqrt :: Int -> Int
primitive primIntEq :: Int -> Int -> Bool
primitive primIntLess :: Int -> Int -> Bool
primitive primFix :: forall {i :: Int} . forall {{a :: *}} . (a -> a) -> a
{-
let int' =
(fix (Int -> List Int -> Int)
(\f n xs -> -- ((f, n, xs); xs, n)
boolCase (\ _ -> Int)
(f (primSub n #1)
(listCase Int (\ _ -> List Int)
(fix (List Int) (\u -> u))
(\ x xs -> xs)
xs))
(listCase Int (\ _ -> Int)
(fix Int (\u -> u))
(\ x xs -> x)
xs)
(primIntEq #0 n)))
#10000
(fix (List Int)
(\primes -> -- primes
(Cons Int #2 (Cons Int #3
(fix (List Int -> List Int)
(\fil -> -- (fil + primes)
listCase Int (\ _ -> List Int)
(Nil Int)
(\ x' xs' -> -- ((fil, xs'); (x', (fil, xs')), (x', primes))
boolCase (\ _ -> List Int)
(fil xs')
(Cons Int x' (fil xs'))
(fix (List Int -> Bool)
(\al -> -- (al, x')
listCase Int (\ _ -> Bool)
True
(\ x'' xs -> -- (;(al, xs), (x', x''))
boolCase (\ _ -> Bool)
False
(al xs)
(boolCase (\ _ -> Bool)
True
False
(primIntEq #0 (primMod x' x'')))))
(fix (List Int -> List Int)
(\tw -> -- (tw + x')
listCase Int (\ _ -> List Int)
(Nil Int)
(\ x xs -> -- (;(x, (tw, xs)), (x + x'))
boolCase (\ _ -> List Int)
(Nil Int)
(Cons Int x (tw xs))
(((\m -> -- (((x, m);, (x, m)), x')
boolCase (\ _ -> Bool)
(primIntEq !x !m)
True
(primIntLess !x !m)) :: Int -> Bool)
(primSqrt x'))))
primes))))
(fix (Int -> List Int)
!(\ f n -> -- (n, (f, n))
Cons Int n (f !(primAdd #1 !n))) !#5))))))
-}
let filter =
\{a :: *} (p :: a -> Bool) -> fix (List a -> List a) (\fil -> listCase a (\ _ -> List a) (Nil a)
(\x xs -> boolCase (\ _ -> List a)
(fil xs)
(Cons a x (fil xs))
(p x)))
let fromThen = \(d :: Int) -> fix (Int -> List Int) (\f n -> Cons Int n (f (primAdd d n)))
let undefined = \{a :: *} -> fix a (\u -> u)
let head =
\{a :: *} (xs :: List a) -> listCase a (\ _ -> a) (undefined a) (\ x xs -> x) xs
let tail =
\{a :: *} (xs :: List a) -> listCase a (\ _ -> List a) (undefined (List a)) (\ x xs -> xs) xs
let nth =
\{a :: *} -> fix (Int -> List a -> a) (\f n xs -> boolCase (\ _ -> a)
(listCase a (\ _ -> a) (undefined a) (\x xs -> f (primSub n #1) xs) xs)
(head a xs)
(primIntEq #0 n))
let takeWhile =
\{a :: *} (p :: a -> Bool) -> fix (List a -> List a) (\tw -> listCase a (\ _ -> List a) (Nil a)
(\x xs -> boolCase (\ _ -> List a)
(Nil a)
(Cons a x (tw xs))
(p x)))
let and = \(a :: Bool) (b :: Bool) -> boolCase (\ _ -> Bool) False b a
let or = \(a :: Bool) (b :: Bool) -> boolCase (\ _ -> Bool) b True a
let not = boolCase (\ _ -> Bool) True False
let all =
\{a :: *} (p :: a -> Bool) -> fix (List a -> Bool) (\al -> listCase a (\ _ -> Bool) True
(\x xs -> and (p x) (al xs)))
let intLEq = \(n :: Int) (m :: Int) -> or (primIntLess n m) (primIntEq n m)
let primes = fix (List Int) (\primes ->
(Cons Int #2 (Cons Int #3 (filter Int (\ x -> all Int (\ i -> not (primIntEq #0 (primMod x i))) (
takeWhile Int (\p -> (\(m :: Int) -> or (primIntLess p m) (primIntEq p m)) (primSqrt x)) primes
)) (fromThen #2 #5)))
))
let nthPrimes = \(n :: Int) -> nth Int n primes
let main = nthPrimes
|
